fof(l9_arithm,theorem,(
    k5_xcmplx_0(1) = 1 ),
    inference(mizar_proof,[status(thm)],[t3_arithm,d7_xcmplx_0]),
    [file(arithm,l9_arithm),interesting(1.00)]).

fof(l2_arithm,theorem,(
    k4_xcmplx_0(0) = 0 ),
    inference(mizar_proof,[status(thm)],[t1_arithm,d6_xcmplx_0]),
    [file(arithm,l2_arithm),interesting(0.87)]).

fof(l5_arithm,theorem,(
    k4_ordinal2 = 1 ),
    inference(mizar_proof,[status(thm)],[d4_ordinal2]),
    [file(arithm,l5_arithm),interesting(0.75)]).

fof(l3_arithm,theorem,(
    k3_arytm_0(0) = 0 ),
    inference(mizar_proof,[status(thm)],[t13_arytm_0,d4_arytm_0]),
    [file(arithm,l3_arithm),interesting(0.74)]).

fof(t3_arithm,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(1,A) = A ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,t11_arytm_0,d7_arytm_0,d5_xcmplx_0,t14_arytm_0,l5_arithm,t21_arytm_0,l5_arithm,t21_arytm_0,l3_arithm,t14_arytm_0,t13_arytm_0,t13_arytm_0]),
    [file(arithm,t3_arithm),interesting(0.53)]).

fof(t6_arithm,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(A,1) = A ) ),
    inference(mizar_proof,[status(thm)],[l9_arithm,d9_xcmplx_0,t3_arithm]),
    [file(arithm,t6_arithm),interesting(0.51)]).

fof(t1_arithm,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k2_xcmplx_0(A,0) = A ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,t11_arytm_0,d7_arytm_0,d4_xcmplx_0,t13_arytm_0,t13_arytm_0]),
    [file(arithm,t1_arithm),interesting(0.40)]).

fof(t2_arithm,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k3_xcmplx_0(A,0) = 0 ) ),
    inference(mizar_proof,[status(thm)],[d2_xcmplx_0,t11_arytm_0,d7_arytm_0,d5_xcmplx_0,t14_arytm_0,t14_arytm_0,t14_arytm_0,t14_arytm_0,t13_arytm_0,t13_arytm_0,l3_arithm,d7_arytm_0]),
    [file(arithm,t2_arithm),interesting(0.28)]).

fof(t4_arithm,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k6_xcmplx_0(A,0) = A ) ),
    inference(mizar_proof,[status(thm)],[l2_arithm,d8_xcmplx_0,t1_arithm]),
    [file(arithm,t4_arithm),interesting(0.27)]).

fof(d2_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
    <=> r2_hidden(A,k2_numbers) ) ),
    file(xcmplx_0,d2_xcmplx_0),
    [interesting(0.00)]).

fof(t11_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k2_numbers)
     => ? [B] : 
          ( m1_subset_1(B,k1_numbers)
          & ? [C] : 
              ( m1_subset_1(C,k1_numbers)
              & A = k5_arytm_0(B,C) ) ) ) ),
    file(arytm_0,t11_arytm_0),
    [interesting(0.00)]).

fof(d7_arytm_0,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( ( B = 0
             => k5_arytm_0(A,B) = A )
            & ( B != 0
             => k5_arytm_0(A,B) = k5_funct_4(k1_numbers,0,k13_arytm_3,A,B) ) ) ) ) ),
    file(arytm_0,d7_arytm_0),
    [interesting(0.00)]).

fof(d4_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( C = k2_xcmplx_0(A,B)
            <=> ? [D] : 
                  ( m1_subset_1(D,k1_numbers)
                  & ? [E] : 
                      ( m1_subset_1(E,k1_numbers)
                      & ? [F] : 
                          ( m1_subset_1(F,k1_numbers)
                          & ? [G] : 
                              ( m1_subset_1(G,k1_numbers)
                              & A = k5_arytm_0(D,E)
                              & B = k5_arytm_0(F,G)
                              & C = k5_arytm_0(k1_arytm_0(D,F),k1_arytm_0(E,G)) ) ) ) ) ) ) ) ),
    file(xcmplx_0,d4_xcmplx_0),
    [interesting(0.00)]).

fof(t13_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = 0
           => k1_arytm_0(A,B) = A ) ) ) ),
    file(arytm_0,t13_arytm_0),
    [interesting(0.00)]).

fof(d6_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( B = k4_xcmplx_0(A)
          <=> k2_xcmplx_0(A,B) = 0 ) ) ) ),
    file(xcmplx_0,d6_xcmplx_0),
    [interesting(0.00)]).

fof(d8_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k6_xcmplx_0(A,B) = k2_xcmplx_0(A,k4_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d8_xcmplx_0),
    [interesting(0.00)]).

fof(d9_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d9_xcmplx_0),
    [interesting(0.00)]).

fof(d5_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( C = k3_xcmplx_0(A,B)
            <=> ? [D] : 
                  ( m1_subset_1(D,k1_numbers)
                  & ? [E] : 
                      ( m1_subset_1(E,k1_numbers)
                      & ? [F] : 
                          ( m1_subset_1(F,k1_numbers)
                          & ? [G] : 
                              ( m1_subset_1(G,k1_numbers)
                              & A = k5_arytm_0(D,E)
                              & B = k5_arytm_0(F,G)
                              & C = k5_arytm_0(k1_arytm_0(k2_arytm_0(D,F),k3_arytm_0(k2_arytm_0(E,G))),k1_arytm_0(k2_arytm_0(D,G),k2_arytm_0(E,F))) ) ) ) ) ) ) ) ),
    file(xcmplx_0,d5_xcmplx_0),
    [interesting(0.00)]).

fof(t14_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = 0
           => k2_arytm_0(A,B) = 0 ) ) ) ),
    file(arytm_0,t14_arytm_0),
    [interesting(0.00)]).

fof(d4_arytm_0,definition,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = k3_arytm_0(A)
          <=> k1_arytm_0(A,B) = 0 ) ) ) ),
    file(arytm_0,d4_arytm_0),
    [interesting(0.00)]).

fof(t5_arithm,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k7_xcmplx_0(0,A) = 0 ) ),
    inference(mizar_proof,[status(thm)],[d9_xcmplx_0,t2_arithm]),
    [file(arithm,t5_arithm),interesting(0.00)]).

fof(d4_ordinal2,definition,(
    k4_ordinal2 = k1_ordinal1(k1_xboole_0) ),
    file(ordinal2,d4_ordinal2),
    [interesting(0.00)]).

fof(t21_arytm_0,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ( B = k13_arytm_3
           => k2_arytm_0(A,B) = A ) ) ) ),
    file(arytm_0,t21_arytm_0),
    [interesting(0.00)]).

fof(d7_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( A != 0
             => ( B = k5_xcmplx_0(A)
              <=> k3_xcmplx_0(A,B) = 1 ) )
            & ( A = 0
             => ( B = k5_xcmplx_0(A)
              <=> B = 0 ) ) ) ) ) ),
    file(xcmplx_0,d7_xcmplx_0),
    [interesting(0.00)]).