fof(l14_xcmplx_0,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k3_xcmplx_0(A,k3_xcmplx_0(B,C)) = k3_xcmplx_0(k3_xcmplx_0(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_xcmplx_0,d5_xcmplx_0,t12_arytm_0,d5_xcmplx_0,t12_arytm_0,d5_xcmplx_0,t12_arytm_0,t12_arytm_0,t12_arytm_0,t15_arytm_0,t15_arytm_0,t15_arytm_0,t17_arytm_0,t17_arytm_0,t25_arytm_0,t17_arytm_0,t17_arytm_0,t16_arytm_0,t16_arytm_0,t25_arytm_0,t25_arytm_0,t15_arytm_0,t16_arytm_0,t17_arytm_0,t17_arytm_0,t17_arytm_0,t17_arytm_0,t27_arytm_0,t16_arytm_0,t17_arytm_0,t17_arytm_0,t17_arytm_0,t17_arytm_0,t15_arytm_0,t15_arytm_0,t17_arytm_0,t16_arytm_0,t25_arytm_0,t15_arytm_0,t16_arytm_0,t16_arytm_0,t25_arytm_0,t15_arytm_0,t25_arytm_0,t16_arytm_0]), [file(xcmplx_0,l14_xcmplx_0),interesting(1.00)]). fof(l8_xcmplx_0,theorem,( m1_subset_1(k4_ordinal2,k1_numbers) ), inference(mizar_proof,[status(thm)],[t1_arytm_0,t21_arytm_2]), [file(xcmplx_0,l8_xcmplx_0),interesting(0.82)]). fof(l1_xcmplx_0,theorem,( k4_ordinal2 = 1 ), inference(mizar_proof,[status(thm)],[d4_ordinal2]), [file(xcmplx_0,l1_xcmplx_0),interesting(0.80)]). fof(l15_xcmplx_0,theorem,( r1_tarski(k1_numbers,k2_numbers) ), inference(mizar_proof,[status(thm)],[d2_numbers,t7_xboole_1]), [file(xcmplx_0,l15_xcmplx_0),interesting(0.74)]). fof(l7_xcmplx_0,theorem,( 0 = k5_arytm_0(0,0) ), inference(mizar_proof,[status(thm)],[d7_arytm_0]), [file(xcmplx_0,l7_xcmplx_0),interesting(0.72)]). 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(t12_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( k5_arytm_0(A,B) = k5_arytm_0(C,D) => ( A = C & B = D ) ) ) ) ) ) ), file(arytm_0,t12_arytm_0), [interesting(0.00)]). fof(t15_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k2_arytm_0(A,k2_arytm_0(B,C)) = k2_arytm_0(k2_arytm_0(A,B),C) ) ) ) ), file(arytm_0,t15_arytm_0), [interesting(0.00)]). fof(t17_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k2_arytm_0(k3_arytm_0(A),B) = k3_arytm_0(k2_arytm_0(A,B)) ) ) ), file(arytm_0,t17_arytm_0), [interesting(0.00)]). fof(t25_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k1_arytm_0(A,k1_arytm_0(B,C)) = k1_arytm_0(k1_arytm_0(A,B),C) ) ) ) ), file(arytm_0,t25_arytm_0), [interesting(0.00)]). fof(t16_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k2_arytm_0(A,k1_arytm_0(B,C)) = k1_arytm_0(k2_arytm_0(A,B),k2_arytm_0(A,C)) ) ) ) ), file(arytm_0,t16_arytm_0), [interesting(0.00)]). fof(t27_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k3_arytm_0(k1_arytm_0(A,B)) = k1_arytm_0(k3_arytm_0(A),k3_arytm_0(B)) ) ) ), file(arytm_0,t27_arytm_0), [interesting(0.00)]). fof(d2_numbers,definition,( k2_numbers = k2_xboole_0(k4_xboole_0(k1_funct_2(k2_tarski(0,k13_arytm_3),k1_numbers),a_0_0_numbers),k1_numbers) ), file(numbers,d2_numbers), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(d4_ordinal2,definition,( k4_ordinal2 = k1_ordinal1(k1_xboole_0) ), file(ordinal2,d4_ordinal2), [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(t1_arytm_0,theorem,( r1_tarski(k2_arytm_2,k1_numbers) ), file(arytm_0,t1_arytm_0), [interesting(0.00)]). fof(t21_arytm_2,theorem, ( r2_hidden(k12_arytm_3,k2_arytm_2) & r2_hidden(k13_arytm_3,k2_arytm_2) ), file(arytm_2,t21_arytm_2), [interesting(0.00)]). fof(d2_arytm_0,definition,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) => ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = D & B = E & C = k7_arytm_2(D,E) ) ) ) ) & ( ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = D & B = k4_tarski(0,E) & C = k2_arytm_1(D,E) ) ) ) ) & ( ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) => ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = k4_tarski(0,D) & B = E & C = k2_arytm_1(E,D) ) ) ) ) & ~ ( ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_arytm_2) ) & ~ ( r2_hidden(A,k2_arytm_2) & r2_hidden(B,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) & ~ ( r2_hidden(B,k2_arytm_2) & r2_hidden(A,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)) ) & ~ ( C = k1_arytm_0(A,B) <=> ? [D] : ( m1_subset_1(D,k2_arytm_2) & ? [E] : ( m1_subset_1(E,k2_arytm_2) & A = k4_tarski(0,D) & B = k4_tarski(0,E) & C = k4_tarski(0,k7_arytm_2(D,E)) ) ) ) ) ) ) ) ) ), file(arytm_0,d2_arytm_0), [interesting(0.00)]). fof(t12_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ! [C] : ( m1_subset_1(C,k2_arytm_2) => ( k7_arytm_2(A,B) = k7_arytm_2(A,C) => B = C ) ) ) ) ), file(arytm_2,t12_arytm_2), [interesting(0.00)]). fof(t6_arytm_2,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( k7_arytm_2(A,B) = k12_arytm_3 => A = k12_arytm_3 ) ) ) ), file(arytm_2,t6_arytm_2), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(d1_numbers,definition,( k1_numbers = k4_xboole_0(k2_xboole_0(k2_arytm_2,k2_zfmisc_1(k1_tarski(0),k2_arytm_2)),k1_tarski(k4_tarski(0,0))) ), file(numbers,d1_numbers), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(t19_arytm_1,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( A = k1_xboole_0 => ( B = k1_xboole_0 | k2_arytm_1(A,B) = k4_tarski(k1_xboole_0,B) ) ) ) ) ), file(arytm_1,t19_arytm_1), [interesting(0.00)]). fof(t6_arytm_0,theorem,( ! [A] : ( m1_subset_1(A,k2_arytm_2) => ! [B] : ( m1_subset_1(B,k2_arytm_2) => ( k2_arytm_1(A,B) = k12_arytm_3 => A = B ) ) ) ), file(arytm_0,t6_arytm_0), [interesting(0.00)]). fof(t33_zfmisc_1,theorem,( ! [A,B,C,D] : ( k4_tarski(A,B) = k4_tarski(C,D) => ( A = C & B = D ) ) ), file(zfmisc_1,t33_zfmisc_1), [interesting(0.00)]). fof(l9_xcmplx_0,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ( ( k1_arytm_0(A,B) = 0 & k1_arytm_0(A,C) = 0 ) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_arytm_0,t12_arytm_2,d2_arytm_0,d2_arytm_0,t6_arytm_2,d1_tarski,d1_numbers,d4_xboole_0,t19_arytm_1,d2_arytm_0,d2_arytm_0,t6_arytm_2,d1_tarski,d1_numbers,d4_xboole_0,t19_arytm_1,d2_arytm_0,d2_arytm_0,t6_arytm_0,t6_arytm_0,d2_arytm_0,d2_arytm_0,t33_zfmisc_1,t6_arytm_0,t6_arytm_0,d2_arytm_0,d2_arytm_0]), [file(xcmplx_0,l9_xcmplx_0),interesting(0.00)]).