fof(t13_ami_4,theorem,( r1_ami_1(k1_tarski(k4_numbers),k1_ami_3,k17_ami_1(k1_tarski(k4_numbers),k1_ami_3,k12_ami_3(k1_tarski(k4_numbers),k1_ami_3,k16_ami_3(0)),k1_ami_4),k2_ami_4) ), inference(mizar_proof,[status(thm)],[d29_ami_1,t11_ami_4,t65_funct_4,d2_tarski,t34_ami_3,t4_ami_4,d1_funct_4,t3_xboole_0,d2_xboole_0,d3_enumset1,d1_tarski,d2_tarski,t57_ami_3,t33_funct_4,t26_funct_4,t1_xboole_1,t25_relat_1,d1_tarski,d2_xboole_0,d7_xboole_0,d3_xboole_0,d17_ami_3,t57_ami_3,t4_ami_4,d3_enumset1,d16_ami_3,t12_funct_4,t12_funct_4,t50_ami_3,t26_funct_4,t1_xboole_1,t8_grfunc_1,t66_funct_4,t8_grfunc_1,t66_funct_4,d25_ami_1,t49_ami_3,t1_xboole_1,t49_ami_3,t1_xboole_1,d1_funct_4,t4_xboole_1,t42_enumset1,t43_ami_3,t43_ami_3,t4_ami_4,t64_grfunc_1,t4_ami_4,t64_grfunc_1,t36_ami_3,t36_ami_3,d19_ami_1,d14_ami_3,d14_ami_3,t5_cqc_the1,t5_ami_4,t5_ami_4,t5_ami_4,t5_ami_4,t5_ami_4,t5_ami_4,t5_ami_4,t6_ami_4,t6_ami_4,t6_ami_4,t6_ami_4,t6_ami_4,t6_ami_4,t6_ami_4,t7_ami_4,t7_ami_4,t7_ami_4,t7_ami_4,t7_ami_4,t8_ami_4,t8_ami_4,t8_ami_4,t8_ami_4,t8_ami_4,t29_nat_1,l6_ami_4,t46_ami_3,l12_ami_4,s1_ami_3,t26_ami_3,t185_relat_1,d26_ami_1,t1_xboole_1,t49_ami_3,t16_int_1,l14_ami_4,t40_ami_3,d1_absvalue,t2_ami_4,t77_nat_1,d19_ami_1,l13_ami_4,l12_ami_4,l6_ami_4,t40_ami_3,d1_absvalue,t2_ami_4,t76_nat_1,d19_ami_1,l13_ami_4,l12_ami_4,d14_ami_3,t43_ami_3,l14_ami_4,t51_ami_1,t48_ami_3,t40_ami_3,t1_xreal_1,t12_ami_4,t39_ami_3,t65_funct_4,d2_tarski,t26_funct_4,t1_xboole_1,t26_funct_4,t1_xboole_1,t1_xboole_1,t49_ami_3,t36_ami_3,t66_funct_4,t8_grfunc_1,t10_ami_4,t27_ami_3,t25_relat_1,t5_cqc_lang,t12_zfmisc_1,t1_xboole_1,d28_ami_1,t186_relat_1]), [file(ami_4,t13_ami_4),interesting(1.00)]). fof(t10_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( ( r1_ami_3(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(0)) & r1_tarski(k1_ami_4,A) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( k2_ami_3(A,k15_ami_3(0)) = B & k2_ami_3(A,k15_ami_3(1)) = C ) => ( r1_xreal_0(B,0) | r1_xreal_0(C,0) | k2_ami_3(k12_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k15_ami_3(0)) = k3_int_2(B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l14_ami_4,t16_int_1,d1_absvalue,t2_ami_4,t77_nat_1,d19_ami_1,l13_ami_4,l12_ami_4,l6_ami_4,t44_ami_3,l13_ami_4,d1_absvalue,d3_int_2,t16_int_1,d1_absvalue,t2_ami_4,t76_nat_1,d19_ami_1,l13_ami_4,l12_ami_4,d14_ami_3,t43_ami_3,l14_ami_4,t51_ami_1,t48_ami_3,l14_ami_4,t47_ami_3,t1_xreal_1]), [file(ami_4,t10_ami_4),interesting(0.69)]). fof(t1_ami_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => r1_xreal_0(0,k5_int_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_int_1,d4_int_1,t125_real_2,t11_xreal_1,t2_xreal_1,t21_int_1]), [file(ami_4,t1_ami_4),interesting(0.66)]). fof(t2_ami_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => ( k4_nat_1(k1_int_2(A),k1_int_2(B)) = k6_int_1(A,B) & k3_nat_1(k1_int_2(A),k1_int_2(B)) = k5_int_1(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_absvalue,t1_ami_4,t78_newton,t16_int_1,t79_newton,d8_int_1,d1_nat_1,d2_nat_1,d1_absvalue,d1_nat_1,d2_nat_1,t75_int_1,d8_int_1]), [file(ami_4,t2_ami_4),interesting(0.65)]). fof(t4_ami_4,theorem,( k1_relat_1(k1_ami_4) = k3_enumset1(k16_ami_3(0),k16_ami_3(1),k16_ami_3(2),k16_ami_3(3),k16_ami_3(4)) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,d1_funct_4,t41_enumset1,d1_funct_4,t42_enumset1,d1_funct_4,t44_enumset1,d1_funct_4,t47_enumset1]), [file(ami_4,t4_ami_4),interesting(0.62)]). fof(t11_ami_4,theorem,( ! [A] : ( r2_hidden(A,k1_relat_1(k2_ami_4)) <=> ? [B] : ( v1_int_1(B) & ? [C] : ( v1_int_1(C) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(C,0) & A = k18_ami_3(k15_ami_3(0),k15_ami_3(1),B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_funct_1,t12_relset_1,t27_partfun1,t32_ami_3,d2_ami_4,d2_ami_4,t8_funct_1]), [file(ami_4,t11_ami_4),interesting(0.57)]). fof(t12_ami_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & k1_funct_1(k2_ami_4,k18_ami_3(k15_ami_3(0),k15_ami_3(1),A,B)) != k17_ami_3(k15_ami_3(0),k3_int_2(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_ami_4,t8_funct_1]), [file(ami_4,t12_ami_4),interesting(0.55)]). fof(s1_ami_4,theorem, ( ( ~ r1_xreal_0(f4_s1_ami_4,0) & ~ r1_xreal_0(f3_s1_ami_4,f4_s1_ami_4) & f1_s1_ami_4(0) = f3_s1_ami_4 & f2_s1_ami_4(0) = f4_s1_ami_4 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(f2_s1_ami_4(A),0) => ( f1_s1_ami_4(k1_nat_1(A,1)) = f2_s1_ami_4(A) & f2_s1_ami_4(k1_nat_1(A,1)) = k4_nat_1(f1_s1_ami_4(A),f2_s1_ami_4(A)) ) ) ) ) => ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & f1_s1_ami_4(A) = k6_nat_1(f3_s1_ami_4,f4_s1_ami_4) & f2_s1_ami_4(A) = 0 ) ), inference(mizar_proof,[status(thm)],[s4_recdef_1,d1_cqc_lang,t22_nat_1,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,d2_nat_1,s8_nat_1,t71_newton,d1_cqc_lang]), [file(ami_4,s1_ami_4),interesting(0.48)]). fof(l14_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( ( r1_ami_3(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(0)) & r1_tarski(k1_ami_4,A) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( k2_ami_3(A,k15_ami_3(0)) = B & k2_ami_3(A,k15_ami_3(1)) = C ) => ( r1_xreal_0(B,C) | r1_xreal_0(C,0) | ( k2_ami_3(k12_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k15_ami_3(0)) = k3_int_2(B,C) & ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r2_ami_3(k1_tarski(k4_numbers),k1_ami_3,A,k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),D))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_int_1,d19_ami_1,d1_absvalue,d19_ami_1,d1_absvalue,l12_ami_4,l13_ami_4,t7_absvalue,l12_ami_4,l12_ami_4,d1_absvalue,l13_ami_4,t7_absvalue,t2_ami_4,s1_ami_4,d1_absvalue,l12_ami_4,t7_absvalue,l12_ami_4,l6_ami_4,t44_ami_3,d1_absvalue,d3_int_2]), [file(ami_4,l14_ami_4),interesting(0.45)]). fof(t9_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( r1_tarski(k1_ami_4,A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B)) = k16_ami_3(4) => k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,C)) = k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,l6_ami_4,t46_ami_3]), [file(ami_4,t9_ami_4),interesting(0.44)]). fof(l6_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( r1_tarski(k1_ami_4,A) => ( k13_ami_1(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(0)) = k3_ami_3(k15_ami_3(2),k15_ami_3(1)) & k13_ami_1(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(1)) = k7_ami_3(k15_ami_3(0),k15_ami_3(1)) & k13_ami_1(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(2)) = k3_ami_3(k15_ami_3(0),k15_ami_3(2)) & k13_ami_1(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(3)) = k10_ami_3(k16_ami_3(0),k15_ami_3(1)) & r2_ami_3(k1_tarski(k4_numbers),k1_ami_3,A,k16_ami_3(4)) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,d1_funct_4,t41_enumset1,d1_funct_4,t42_enumset1,d1_funct_4,t44_enumset1,d2_enumset1,t4_ami_4,d3_enumset1,t8_grfunc_1,t12_funct_4,t6_cqc_lang,t26_funct_4,t1_xboole_1,d1_enumset1,d2_enumset1,t8_grfunc_1,t12_funct_4,t6_cqc_lang,t26_funct_4,t1_xboole_1,d2_tarski,d1_enumset1,t8_grfunc_1,t12_funct_4,t6_cqc_lang,t26_funct_4,t1_xboole_1,d1_tarski,d2_tarski,t8_grfunc_1,t12_funct_4,t6_cqc_lang,d2_tarski,d1_tarski,t8_grfunc_1,t14_funct_4,t6_cqc_lang,d15_ami_3]), [file(ami_4,l6_ami_4),interesting(0.38)]). fof(l12_ami_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( ( r1_ami_3(k1_tarski(k4_numbers),k1_ami_3,B,k16_ami_3(0)) & r1_tarski(k1_ami_4,B) ) => ( r1_xreal_0(k2_ami_3(B,k15_ami_3(0)),0) | r1_xreal_0(k2_ami_3(B,k15_ami_3(1)),0) | ( ~ r1_xreal_0(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(0)),0) & ( ( ~ r1_xreal_0(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(1)),0) & k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A))) = k16_ami_3(0) ) | ( k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(1)) = 0 & k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A))) = k16_ami_3(4) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_ami_3,d19_ami_1,t5_ami_4,t6_ami_4,t7_ami_4,t8_ami_4,t78_newton,t9_ami_4,s1_nat_1]), [file(ami_4,l12_ami_4),interesting(0.26)]). fof(t5_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( r1_tarski(k1_ami_4,A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B)) = k16_ami_3(0) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1))) = k16_ami_3(1) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(0)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(0)) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(1)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1)) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(2)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_ami_1,l6_ami_4,t8_ami_3,t54_ami_3,t8_ami_3,t8_ami_3]), [file(ami_4,t5_ami_4),interesting(0.23)]). fof(t7_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( r1_tarski(k1_ami_4,A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B)) = k16_ami_3(2) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1))) = k16_ami_3(3) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(0)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(2)) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(1)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1)) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(2)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(2)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_ami_1,l6_ami_4,t8_ami_3,t54_ami_3,t8_ami_3,t8_ami_3]), [file(ami_4,t7_ami_4),interesting(0.22)]). fof(t8_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( r1_tarski(k1_ami_4,A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B)) = k16_ami_3(3) => ( ( ~ r1_xreal_0(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1)),0) => k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1))) = k16_ami_3(0) ) & ( r1_xreal_0(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1)),0) => k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1))) = k16_ami_3(4) ) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(0)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(0)) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(1)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_ami_1,l6_ami_4,t15_ami_3,t15_ami_3,t54_ami_3,t15_ami_3]), [file(ami_4,t8_ami_4),interesting(0.17)]). fof(t6_ami_4,theorem,( ! [A] : ( m1_subset_1(A,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( r1_tarski(k1_ami_4,A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B)) = k16_ami_3(1) => ( k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1))) = k16_ami_3(2) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(0)) = k5_int_1(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(0)),k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1))) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(1)) = k6_int_1(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(0)),k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(1))) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),k1_nat_1(B,1)),k15_ami_3(2)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,A),B),k15_ami_3(2)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_ami_1,l6_ami_4,t12_ami_3,t54_ami_3,t12_ami_3]), [file(ami_4,t6_ami_4),interesting(0.16)]). fof(d29_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & v10_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ( r1_ami_1(A,B,C,D) <=> ! [E] : ~ ( r2_hidden(E,k1_relat_1(D)) & ! [F] : ( m1_ami_1(F,A,B) => ~ ( E = F & v11_ami_1(k17_ami_1(A,B,C,F),A,B) & v12_ami_1(k17_ami_1(A,B,C,F),A,B) & m1_ami_1(k17_ami_1(A,B,C,F),A,B) & r1_tarski(k1_funct_1(D,F),k18_ami_1(A,B,k17_ami_1(A,B,C,F))) ) ) ) ) ) ) ) ) ), file(ami_1,d29_ami_1), [interesting(0.00)]). fof(t8_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(k4_tarski(A,B),C) <=> ( r2_hidden(A,k1_relat_1(C)) & B = k1_funct_1(C,A) ) ) ) ), file(funct_1,t8_funct_1), [interesting(0.00)]). fof(t12_relset_1,theorem,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) ) ), file(relset_1,t12_relset_1), [interesting(0.00)]). fof(t27_partfun1,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & m2_relset_1(D,A,B) ) => ( r2_hidden(C,k4_relset_1(A,B,D)) => r2_hidden(k1_funct_1(D,C),B) ) ) ), file(partfun1,t27_partfun1), [interesting(0.00)]). fof(t32_ami_3,theorem,( ! [A,B] : ( l1_ami_1(B,A) => ! [C] : ( m2_subset_1(C,k7_ami_1(u5_ami_1(A,B)),k14_ami_1(A,B)) => m1_ami_1(C,A,B) ) ) ), file(ami_3,t32_ami_3), [interesting(0.00)]). fof(d2_ami_4,definition,( ! [A] : ( ( v1_funct_1(A) & m2_relset_1(A,k14_ami_1(k1_tarski(k4_numbers),k1_ami_3),k14_ami_1(k1_tarski(k4_numbers),k1_ami_3)) ) => ( A = k2_ami_4 <=> ! [B] : ( m1_ami_1(B,k1_tarski(k4_numbers),k1_ami_3) => ! [C] : ( m1_ami_1(C,k1_tarski(k4_numbers),k1_ami_3) => ( r2_hidden(k4_tarski(B,C),A) <=> ? [D] : ( v1_int_1(D) & ? [E] : ( v1_int_1(E) & ~ r1_xreal_0(D,0) & ~ r1_xreal_0(E,0) & B = k18_ami_3(k15_ami_3(0),k15_ami_3(1),D,E) & C = k17_ami_3(k15_ami_3(0),k3_int_2(D,E)) ) ) ) ) ) ) ) ), file(ami_4,d2_ami_4), [interesting(0.00)]). fof(t65_funct_4,theorem,( ! [A,B,C,D] : ( k1_relat_1(k4_funct_4(A,B,C,D)) = k2_tarski(A,B) & r1_tarski(k2_relat_1(k4_funct_4(A,B,C,D)),k2_tarski(C,D)) ) ), file(funct_4,t65_funct_4), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t34_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => k1_relat_1(k12_ami_3(A,B,C)) = k1_struct_0(B,k2_ami_1(A,B)) ) ) ) ), file(ami_3,t34_ami_3), [interesting(0.00)]). fof(t5_cqc_lang,theorem,( ! [A,B] : ( k1_relat_1(k3_cqc_lang(A,B)) = k1_tarski(A) & k2_relat_1(k3_cqc_lang(A,B)) = k1_tarski(B) ) ), file(cqc_lang,t5_cqc_lang), [interesting(0.00)]). fof(d1_funct_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k1_funct_4(A,B) <=> ( k1_relat_1(C) = k2_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k2_xboole_0(k1_relat_1(A),k1_relat_1(B))) => ( ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(B,D) ) & ( ~ r2_hidden(D,k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) ) ) ) ) ) ) ), file(funct_4,d1_funct_4), [interesting(0.00)]). fof(t41_enumset1,theorem,( ! [A,B] : k2_tarski(A,B) = k2_xboole_0(k1_tarski(A),k1_tarski(B)) ), file(enumset1,t41_enumset1), [interesting(0.00)]). fof(t42_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k1_tarski(A),k2_tarski(B,C)) ), file(enumset1,t42_enumset1), [interesting(0.00)]). fof(t44_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_xboole_0(k1_tarski(A),k1_enumset1(B,C,D)) ), file(enumset1,t44_enumset1), [interesting(0.00)]). fof(t47_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k1_tarski(A),k2_enumset1(B,C,D,E)) ), file(enumset1,t47_enumset1), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(d3_enumset1,definition,( ! [A,B,C,D,E,F] : ( F = k3_enumset1(A,B,C,D,E) <=> ! [G] : ( r2_hidden(G,F) <=> ~ ( G != A & G != B & G != C & G != D & G != E ) ) ) ), file(enumset1,d3_enumset1), [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(t57_ami_3,theorem,( ! [A] : ( v4_ordinal2(A) => ( k2_ami_1(k1_tarski(k4_numbers),k1_ami_3) != k15_ami_3(A) & k2_ami_1(k1_tarski(k4_numbers),k1_ami_3) != k16_ami_3(A) ) ) ), file(ami_3,t57_ami_3), [interesting(0.00)]). fof(t33_funct_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_xboole_0(k1_relat_1(A),k1_relat_1(B)) => r1_tarski(A,k1_funct_4(A,B)) ) ) ) ), file(funct_4,t33_funct_4), [interesting(0.00)]). fof(t26_funct_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => r1_tarski(A,k1_funct_4(B,A)) ) ) ), file(funct_4,t26_funct_4), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t25_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(A,B) => ( r1_tarski(k1_relat_1(A),k1_relat_1(B)) & r1_tarski(k2_relat_1(A),k2_relat_1(B)) ) ) ) ) ), file(relat_1,t25_relat_1), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d17_ami_3,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r3_ami_3(A,B,C,D) <=> ( r2_hidden(k2_ami_1(A,B),k1_relat_1(C)) & k13_ami_3(A,B,C) = D ) ) ) ) ) ) ), file(ami_3,d17_ami_3), [interesting(0.00)]). fof(d16_ami_3,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ( r2_hidden(k2_ami_1(A,B),k1_relat_1(C)) => k13_ami_3(A,B,C) = k1_funct_1(C,k2_ami_1(A,B)) ) ) ) ) ), file(ami_3,d16_ami_3), [interesting(0.00)]). fof(t12_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ~ r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(C,A) ) ) ) ), file(funct_4,t12_funct_4), [interesting(0.00)]). fof(t50_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => k1_funct_1(k12_ami_3(A,B,C),k2_ami_1(A,B)) = C ) ) ) ), file(ami_3,t50_ami_3), [interesting(0.00)]). fof(t8_grfunc_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(A,B) <=> ( r1_tarski(k1_relat_1(A),k1_relat_1(B)) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) ) ) ), file(grfunc_1,t8_grfunc_1), [interesting(0.00)]). fof(t66_funct_4,theorem,( ! [A,B,C,D] : ( A != B => ( k1_funct_1(k4_funct_4(A,B,C,D),A) = C & k1_funct_1(k4_funct_4(A,B,C,D),B) = D ) ) ), file(funct_4,t66_funct_4), [interesting(0.00)]). fof(d25_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ( v11_ami_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => ! [E] : ( m1_subset_1(E,k4_card_3(u5_ami_1(A,B))) => ( ( r1_tarski(C,D) & r1_tarski(C,E) ) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => k7_relat_1(k11_ami_1(A,B,k10_ami_1(A,B,D),F),k1_relat_1(C)) = k7_relat_1(k11_ami_1(A,B,k10_ami_1(A,B,E),F),k1_relat_1(C)) ) ) ) ) ) ) ) ) ), file(ami_1,d25_ami_1), [interesting(0.00)]). fof(t49_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r3_ami_3(A,B,C,D) => ! [E] : ( m1_subset_1(E,k4_card_3(u5_ami_1(A,B))) => ( r1_tarski(C,E) => r1_ami_3(A,B,E,D) ) ) ) ) ) ) ) ), file(ami_3,t49_ami_3), [interesting(0.00)]). fof(t4_xboole_1,theorem,( ! [A,B,C] : k2_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(A,k2_xboole_0(B,C)) ), file(xboole_1,t4_xboole_1), [interesting(0.00)]). fof(t43_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v7_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( ( v1_ami_3(D,A,B) & m1_ami_1(D,A,B) ) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_tarski(D,C) <=> r1_tarski(D,k11_ami_1(A,B,k10_ami_1(A,B,C),E)) ) ) ) ) ) ) ), file(ami_3,t43_ami_3), [interesting(0.00)]). fof(t64_grfunc_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(A,B) => k7_relat_1(B,k1_relat_1(A)) = A ) ) ) ), file(grfunc_1,t64_grfunc_1), [interesting(0.00)]). fof(t36_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => k1_relat_1(C) = u1_struct_0(B) ) ) ) ), file(ami_3,t36_ami_3), [interesting(0.00)]). fof(d19_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,k4_card_3(u5_ami_1(A,B))) & m2_relset_1(D,k5_numbers,k4_card_3(u5_ami_1(A,B))) ) => ( D = k10_ami_1(A,B,C) <=> ( k8_funct_2(k5_numbers,k4_card_3(u5_ami_1(A,B)),D,0) = C & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,k4_card_3(u5_ami_1(A,B)),D,k1_nat_1(E,1)) = k9_ami_1(A,B,k8_funct_2(k5_numbers,k4_card_3(u5_ami_1(A,B)),D,E)) ) ) ) ) ) ) ) ), file(ami_1,d19_ami_1), [interesting(0.00)]). fof(d14_ami_3,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v5_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r1_ami_3(A,B,C,D) <=> k6_ami_1(A,B,C) = D ) ) ) ) ) ), file(ami_3,d14_ami_3), [interesting(0.00)]). fof(t5_cqc_the1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( r1_xreal_0(A,4) & A != 0 & A != 1 & A != 2 & A != 3 & A != 4 ) ) ), file(cqc_the1,t5_cqc_the1), [interesting(0.00)]). fof(t55_ami_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,A) & v5_ami_1(C,A) & v7_ami_1(C,A) & v8_ami_1(C,A) & l1_ami_1(C,A) ) => ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,C))) => k11_ami_1(A,C,k10_ami_1(A,C,D),k1_nat_1(B,1)) = k4_ami_1(A,C,k13_ami_1(A,C,D,k6_ami_1(A,C,k11_ami_1(A,C,k10_ami_1(A,C,D),B))),k11_ami_1(A,C,k10_ami_1(A,C,D),B)) ) ) ) ) ), file(ami_1,t55_ami_1), [interesting(0.00)]). fof(d2_enumset1,definition,( ! [A,B,C,D,E] : ( E = k2_enumset1(A,B,C,D) <=> ! [F] : ( r2_hidden(F,E) <=> ~ ( F != A & F != B & F != C & F != D ) ) ) ), file(enumset1,d2_enumset1), [interesting(0.00)]). fof(t6_cqc_lang,theorem,( ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ), file(cqc_lang,t6_cqc_lang), [interesting(0.00)]). fof(d1_enumset1,definition,( ! [A,B,C,D] : ( D = k1_enumset1(A,B,C) <=> ! [E] : ( r2_hidden(E,D) <=> ~ ( E != A & E != B & E != C ) ) ) ), file(enumset1,d1_enumset1), [interesting(0.00)]). fof(t14_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ), file(funct_4,t14_funct_4), [interesting(0.00)]). fof(d15_ami_3,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r2_ami_3(A,B,C,D) <=> k1_funct_1(C,D) = k5_ami_1(A,B) ) ) ) ) ) ), file(ami_3,d15_ami_3), [interesting(0.00)]). fof(t8_ami_3,theorem,( ! [A] : ( m1_ami_3(A) => ! [B] : ( m1_ami_3(B) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C)) & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B),C),A) = k2_ami_3(C,B) & ! [D] : ( m1_ami_3(D) => ( D != A => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k3_ami_3(A,B),C),D) = k2_ami_3(C,D) ) ) ) ) ) ) ), file(ami_3,t8_ami_3), [interesting(0.00)]). fof(t54_ami_3,theorem,( ! [A] : ( v4_ordinal2(A) => k11_ami_3(k16_ami_3(A)) = k16_ami_3(k2_xcmplx_0(A,1)) ) ), file(ami_3,t54_ami_3), [interesting(0.00)]). fof(t12_ami_3,theorem,( ! [A] : ( m1_ami_3(A) => ! [B] : ( m1_ami_3(B) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,C)) & ( A != B => k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),A) = k5_int_1(k2_ami_3(C,A),k2_ami_3(C,B)) ) & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),B) = k6_int_1(k2_ami_3(C,A),k2_ami_3(C,B)) & ! [D] : ( m1_ami_3(D) => ~ ( D != A & D != B & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k7_ami_3(A,B),C),D) != k2_ami_3(C,D) ) ) ) ) ) ) ), file(ami_3,t12_ami_3), [interesting(0.00)]). fof(t15_ami_3,theorem,( ! [A] : ( m1_ami_3(A) => ! [B] : ( m1_ami_3(B) => ! [C] : ( m1_struct_0(C,k1_ami_3,u2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) => ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( ( ~ r1_xreal_0(k2_ami_3(D,A),0) => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(C,A),D),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = C ) & ( r1_xreal_0(k2_ami_3(D,A),0) => k1_funct_1(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(C,A),D),k2_ami_1(k1_tarski(k4_numbers),k1_ami_3)) = k11_ami_3(k6_ami_1(k1_tarski(k4_numbers),k1_ami_3,D)) ) & k2_ami_3(k4_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_3(C,A),D),B) = k2_ami_3(D,B) ) ) ) ) ) ), file(ami_3,t15_ami_3), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_1), [interesting(0.00)]). fof(t46_ami_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( v1_setfam_1(C) => ( r1_xreal_0(A,B) => ! [D] : ( ( ~ v3_struct_0(D) & ~ v2_ami_1(D,C) & v4_ami_1(D,C) & v5_ami_1(D,C) & v7_ami_1(D,C) & v8_ami_1(D,C) & l1_ami_1(D,C) ) => ! [E] : ( m1_subset_1(E,k4_card_3(u5_ami_1(C,D))) => ( r2_ami_3(C,D,E,k6_ami_1(C,D,k11_ami_1(C,D,k10_ami_1(C,D,E),A))) => k11_ami_1(C,D,k10_ami_1(C,D,E),B) = k11_ami_1(C,D,k10_ami_1(C,D,E),A) ) ) ) ) ) ) ) ), file(ami_3,t46_ami_3), [interesting(0.00)]). fof(t78_newton,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(0,A) => r1_xreal_0(0,k6_int_1(B,A)) ) ) ) ), file(newton,t78_newton), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(s1_ami_3,theorem, ( ( p1_s1_ami_3(0) & ~ r1_xreal_0(f1_s1_ami_3,0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ( p1_s1_ami_3(k2_nat_1(f1_s1_ami_3,A)) & r1_xreal_0(B,f1_s1_ami_3) ) => ( B = 0 | p1_s1_ami_3(k1_nat_1(k2_nat_1(f1_s1_ami_3,A),B)) ) ) ) ) ) => p1_s1_ami_3(f2_s1_ami_3) ), file(ami_3,s1_ami_3), [interesting(0.00)]). fof(t26_ami_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C,D,E] : ( ( k1_relat_1(A) = k1_relat_1(B) & k1_funct_1(A,C) = k1_funct_1(B,C) & k1_funct_1(A,D) = k1_funct_1(B,D) & k1_funct_1(A,E) = k1_funct_1(B,E) ) => k7_relat_1(A,k1_enumset1(C,D,E)) = k7_relat_1(B,k1_enumset1(C,D,E)) ) ) ) ), file(ami_3,t26_ami_3), [interesting(0.00)]). fof(t185_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ! [C,D] : ( ( k7_relat_1(A,C) = k7_relat_1(B,C) & k7_relat_1(A,D) = k7_relat_1(B,D) ) => k7_relat_1(A,k2_xboole_0(C,D)) = k7_relat_1(B,k2_xboole_0(C,D)) ) ) ) ), file(relat_1,t185_relat_1), [interesting(0.00)]). fof(d26_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ( v12_ami_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => ( r1_tarski(C,D) => v9_ami_1(D,A,B) ) ) ) ) ) ) ), file(ami_1,d26_ami_1), [interesting(0.00)]). fof(t16_int_1,theorem,( ! [A] : ( v1_int_1(A) => ( r1_xreal_0(0,A) => r2_hidden(A,k5_numbers) ) ) ), file(int_1,t16_int_1), [interesting(0.00)]). fof(d1_absvalue,definition,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) => k16_complex1(A) = A ) & ( ~ r1_xreal_0(0,A) => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ), file(absvalue,d1_absvalue), [interesting(0.00)]). fof(l13_ami_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m1_subset_1(B,k4_card_3(u5_ami_1(k1_tarski(k4_numbers),k1_ami_3))) => ( ( r1_ami_3(k1_tarski(k4_numbers),k1_ami_3,B,k16_ami_3(0)) & r1_tarski(k1_ami_4,B) ) => ( r1_xreal_0(k2_ami_3(B,k15_ami_3(0)),0) | r1_xreal_0(k2_ami_3(B,k15_ami_3(1)),0) | r1_xreal_0(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(1)),0) | ( k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,k1_nat_1(A,1))),k15_ami_3(0)) = k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(1)) & k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,k1_nat_1(A,1))),k15_ami_3(1)) = k6_int_1(k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(0)),k2_ami_3(k11_ami_1(k1_tarski(k4_numbers),k1_ami_3,k10_ami_1(k1_tarski(k4_numbers),k1_ami_3,B),k2_nat_1(4,A)),k15_ami_3(1))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_ami_4,t5_ami_4,t6_ami_4,t7_ami_4,t8_ami_4,t8_ami_4]), [file(ami_4,l13_ami_4),interesting(0.00)]). fof(t7_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ( A = 0 <=> k18_complex1(A) = 0 ) ) ), file(absvalue,t7_absvalue), [interesting(0.00)]). fof(d7_int_1,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => k5_int_1(A,B) = k1_int_1(k7_xcmplx_0(A,B)) ) ) ), file(int_1,d7_int_1), [interesting(0.00)]). fof(d4_int_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_int_1(B) => ( B = k1_int_1(A) <=> ( r1_xreal_0(B,A) & ~ r1_xreal_0(B,k6_xcmplx_0(A,1)) ) ) ) ) ), file(int_1,d4_int_1), [interesting(0.00)]). fof(t125_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(A,0) & r1_xreal_0(B,0) ) | ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) ) => r1_xreal_0(0,k7_xcmplx_0(A,B)) ) ) ) ), file(real_2,t125_real_2), [interesting(0.00)]). fof(t11_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(t21_int_1,theorem,( ! [A] : ( v1_int_1(A) => ( ~ r1_xreal_0(0,A) => r1_xreal_0(A,k1_real_1(1)) ) ) ), file(int_1,t21_int_1), [interesting(0.00)]). fof(t79_newton,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k6_int_1(B,A)) ) ) ) ), file(newton,t79_newton), [interesting(0.00)]). fof(d8_int_1,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ( B != 0 => k6_int_1(A,B) = k6_xcmplx_0(A,k3_xcmplx_0(k5_int_1(A,B),B)) ) & ( B = 0 => k6_int_1(A,B) = 0 ) ) ) ) ), file(int_1,d8_int_1), [interesting(0.00)]). fof(d1_nat_1,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k3_nat_1(A,B) <=> ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( A = k2_xcmplx_0(k3_xcmplx_0(B,C),D) & ~ r1_xreal_0(B,D) ) ) & ~ ( C = 0 & B = 0 ) ) ) ) ) ) ), file(nat_1,d1_nat_1), [interesting(0.00)]). fof(d2_nat_1,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k4_nat_1(A,B) <=> ~ ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( A = k2_xcmplx_0(k3_xcmplx_0(B,D),C) & ~ r1_xreal_0(B,C) ) ) & ~ ( C = 0 & B = 0 ) ) ) ) ) ) ), file(nat_1,d2_nat_1), [interesting(0.00)]). fof(t75_int_1,theorem,( ! [A] : ( v1_int_1(A) => k5_int_1(A,0) = 0 ) ), file(int_1,t75_int_1), [interesting(0.00)]). fof(s4_recdef_1,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,f1_s4_recdef_1) & m2_relset_1(A,k5_numbers,f1_s4_recdef_1) & k8_funct_2(k5_numbers,f1_s4_recdef_1,A,0) = f2_s4_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,f1_s4_recdef_1,A,k1_nat_1(B,1)) = f3_s4_recdef_1(B,k8_funct_2(k5_numbers,f1_s4_recdef_1,A,B)) ) ) ), file(recdef_1,s4_recdef_1), [interesting(0.00)]). fof(d1_cqc_lang,definition,( ! [A,B,C,D] : ( ( A = B => k1_cqc_lang(A,B,C,D) = C ) & ( A != B => k1_cqc_lang(A,B,C,D) = D ) ) ), file(cqc_lang,d1_cqc_lang), [interesting(0.00)]). fof(t22_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(B,1) ) ) ) ), file(nat_1,t22_nat_1), [interesting(0.00)]). fof(s8_nat_1,theorem, ( ( ~ r1_xreal_0(f3_s8_nat_1,0) & ~ r1_xreal_0(f2_s8_nat_1,f3_s8_nat_1) & f1_s8_nat_1(0) = f2_s8_nat_1 & f1_s8_nat_1(1) = f3_s8_nat_1 & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => f1_s8_nat_1(k1_nat_1(A,2)) = k4_nat_1(f1_s8_nat_1(A),f1_s8_nat_1(k1_nat_1(A,1))) ) ) => ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & f1_s8_nat_1(A) = k6_nat_1(f2_s8_nat_1,f3_s8_nat_1) & f1_s8_nat_1(k1_nat_1(A,1)) = 0 ) ), file(nat_1,s8_nat_1), [interesting(0.00)]). fof(t71_newton,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k6_nat_1(A,B),0) ) ) ) ), file(newton,t71_newton), [interesting(0.00)]). fof(t44_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v7_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_ami_3(A,B,C,k6_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,C),D))) => k12_ami_1(A,B,C) = k11_ami_1(A,B,k10_ami_1(A,B,C),D) ) ) ) ) ) ), file(ami_3,t44_ami_3), [interesting(0.00)]). fof(d3_int_2,definition,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => k3_int_2(A,B) = k6_nat_1(k1_int_2(A),k1_int_2(B)) ) ) ), file(int_2,d3_int_2), [interesting(0.00)]). fof(t40_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v7_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ( v9_ami_1(C,A,B) <=> ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r2_ami_3(A,B,C,k6_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,C),D))) ) ) ) ) ) ), file(ami_3,t40_ami_3), [interesting(0.00)]). fof(t77_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => k4_nat_1(A,A) = 0 ) ), file(nat_1,t77_nat_1), [interesting(0.00)]). fof(t76_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,B) => k4_nat_1(B,A) = B ) ) ) ), file(nat_1,t76_nat_1), [interesting(0.00)]). fof(t51_ami_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,A) & v5_ami_1(C,A) & v8_ami_1(C,A) & l1_ami_1(C,A) ) => ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,C))) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k11_ami_1(A,C,k10_ami_1(A,C,D),k1_nat_1(B,E)) = k11_ami_1(A,C,k10_ami_1(A,C,k11_ami_1(A,C,k10_ami_1(A,C,D),B)),E) ) ) ) ) ) ), file(ami_1,t51_ami_1), [interesting(0.00)]). fof(t48_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v7_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_ami_3(A,B,C,D) <=> r2_ami_3(A,B,k11_ami_1(A,B,k10_ami_1(A,B,C),E),D) ) ) ) ) ) ) ), file(ami_3,t48_ami_3), [interesting(0.00)]). fof(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [interesting(0.00)]). fof(t39_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ? [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) & r1_tarski(C,D) ) ) ) ) ), file(ami_3,t39_ami_3), [interesting(0.00)]). fof(t47_ami_3,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v7_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ( ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r2_ami_3(A,B,C,k6_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,C),D))) ) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k12_ami_1(A,B,C) = k12_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,C),D)) ) ) ) ) ) ), file(ami_3,t47_ami_3), [interesting(0.00)]). fof(t27_ami_3,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( r2_hidden(A,k1_relat_1(C)) & k1_funct_1(C,A) = B ) => r1_tarski(k3_cqc_lang(A,B),C) ) ) ), file(ami_3,t27_ami_3), [interesting(0.00)]). fof(t12_zfmisc_1,theorem,( ! [A,B] : r1_tarski(k1_tarski(A),k2_tarski(A,B)) ), file(zfmisc_1,t12_zfmisc_1), [interesting(0.00)]). fof(d28_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v4_ami_1(B,A) & v5_ami_1(B,A) & v8_ami_1(B,A) & v10_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ( ( v11_ami_1(C,A,B) & v12_ami_1(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( m1_ami_1(D,A,B) => ( D = k18_ami_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,k4_card_3(u5_ami_1(A,B))) => ( r1_tarski(C,E) => D = k7_relat_1(k12_ami_1(A,B,E),k1_relat_1(C)) ) ) ) ) ) ) ) ) ), file(ami_1,d28_ami_1), [interesting(0.00)]). fof(t186_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ! [C] : ( v1_relat_1(C) => ( ( r1_tarski(k1_relat_1(C),A) & r1_tarski(C,B) ) => r1_tarski(C,k7_relat_1(B,A)) ) ) ) ), file(relat_1,t186_relat_1), [interesting(0.00)]). fof(t3_ami_4,theorem,( $true ), file(ami_4,t3_ami_4), [interesting(0.00)]).