fof(t37_amistd_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => k5_amistd_1(B,k4_amistd_1(B),A) = A ) ) ), inference(mizar_proof,[status(thm)],[d21_ordinal2,d12_amistd_1,d11_amistd_1,t35_funct_1,t24_amistd_1,d2_tarski,t35_funct_1,d2_tarski,t29_nat_1,t18_amistd_1,t17_amistd_1,t35_funct_1]), [file(amistd_1,t37_amistd_1),interesting(1.00)]). fof(t40_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m1_struct_0(B,k4_amistd_1(A),u2_ami_1(A,k4_amistd_1(A))) => k3_amistd_1(A,k4_amistd_1(A),B) = k2_struct_0(k4_amistd_1(A),B,k9_amistd_1(A,k4_amistd_1(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[t26_amistd_1,t37_amistd_1,d13_amistd_1,t24_amistd_1,t37_amistd_1,t37_amistd_1]), [file(amistd_1,t40_amistd_1),interesting(0.97)]). fof(t8_amistd_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_graph_2(B,k9_finseq_1(A)) = B ) ), inference(mizar_proof,[status(thm)],[t56_finseq_1,d1_graph_2,t25_finseq_1,d2_graph_2,t47_finseq_1]), [file(amistd_1,t8_amistd_1),interesting(0.74)]). fof(t7_amistd_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => k3_graph_2(A,k1_xboole_0) = A ) ), inference(mizar_proof,[status(thm)],[t25_finseq_1,d2_graph_2,d1_graph_2,t47_finseq_1]), [file(amistd_1,t7_amistd_1),interesting(0.74)]). fof(t24_amistd_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( m1_struct_0(C,k4_amistd_1(B),u2_ami_1(B,k4_amistd_1(B))) => ( C = A => k3_amistd_1(B,k4_amistd_1(B),C) = k2_tarski(A,k2_xcmplx_0(A,1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l40_amistd_1,l39_amistd_1,d2_tarski,t20_amistd_1,l40_amistd_1,t15_amistd_1,d2_tarski,t22_amistd_1,d2_tarski,d11_amistd_1,l40_amistd_1,d1_ami_5,d1_mcart_1,t20_amistd_1,t15_amistd_1,d2_tarski,d11_amistd_1,l40_amistd_1,d1_ami_5,d1_mcart_1,l39_amistd_1,d2_tarski,t2_tarski,t32_zfmisc_1]), [file(amistd_1,t24_amistd_1),interesting(0.68)]). fof(t1_amistd_1,theorem,( ! [A] : ( v1_xreal_0(A) => k1_pre_circ(k1_tarski(A)) = A ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_pre_circ]), [file(amistd_1,t1_amistd_1),interesting(0.66)]). fof(t3_amistd_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_realset1(B) & m2_finseq_1(B,A) ) => ~ ( ~ v1_xboole_0(B) & ! [C] : ( m1_subset_1(C,A) => B != k13_binarith(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_realset1,d1_tarski,d1_relat_1,d5_relat_1,d4_finseq_1,t6_finseq_5,t23_relat_1,d1_tarski,d5_finseq_1]), [file(amistd_1,t3_amistd_1),interesting(0.65)]). fof(t9_amistd_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m2_finseq_1(D,A) => ( ( r1_xreal_0(1,B) & r1_xreal_0(B,k3_finseq_1(C)) ) => k4_finseq_4(k5_numbers,A,k4_graph_2(A,C,D),B) = k4_finseq_4(k5_numbers,A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_amistd_1,t13_graph_2,t25_finseq_1,t19_nat_1,t8_xreal_1,t2_xreal_1,t38_nat_1,t24_finseq_4,t14_graph_2,t24_finseq_4]), [file(amistd_1,t9_amistd_1),interesting(0.60)]). fof(l40_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => v1_xboole_0(k2_amistd_1(A,k4_amistd_1(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[d1_xboole_0,d11_amistd_1,l39_amistd_1,d1_setfam_1,d1_tarski,t20_amistd_1,t15_amistd_1,t14_amistd_1,t22_amistd_1]), [file(amistd_1,l40_amistd_1),interesting(0.58)]). fof(t30_amistd_1,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) ) => ( v4_amistd_1(B,A) => v3_amistd_1(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_amistd_1,t29_amistd_1,t1_xreal_1,t27_amistd_1]), [file(amistd_1,t30_amistd_1),interesting(0.57)]). fof(t5_amistd_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m2_finseq_1(B,A) ) => ! [C] : ( m2_finseq_1(C,A) => k4_finseq_4(k5_numbers,A,k4_graph_2(A,B,C),1) = k4_finseq_4(k5_numbers,A,B,1) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_finseq_5,t6_finseq_5,d2_graph_2,d4_finseq_4,d7_finseq_1,d4_finseq_4]), [file(amistd_1,t5_amistd_1),interesting(0.56)]). fof(t13_amistd_1,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) ) => v13_ami_1(B,A) ) ) ), inference(mizar_proof,[status(thm)],[d27_ami_1,l12_amistd_1]), [file(amistd_1,t13_amistd_1),interesting(0.55)]). fof(t16_amistd_1,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)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ! [E] : ( m1_struct_0(E,B,u2_ami_1(A,B)) => ( ( r1_amistd_1(A,B,C,D) & r1_amistd_1(A,B,D,E) ) => r1_amistd_1(A,B,C,E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_amistd_1,d8_amistd_1,d8_amistd_1,t5_amistd_1,t3_amistd_1,t8_amistd_1,t56_finseq_1,t6_amistd_1,t29_nat_1,t13_graph_2,t38_nat_1,t9_amistd_1,t9_amistd_1,t9_amistd_1,t8_xreal_1,t8_xreal_1,t10_amistd_1,t28_nat_1,t39_nat_1,t29_nat_1,t8_xreal_1,t8_xreal_1,t29_nat_1,t2_xreal_1,t10_amistd_1,t10_amistd_1,t1_xreal_1]), [file(amistd_1,t16_amistd_1),interesting(0.55)]). fof(t6_amistd_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( ( ~ v1_realset1(C) & m2_finseq_1(C,A) ) => k4_finseq_4(k5_numbers,A,k4_graph_2(A,B,C),k3_finseq_1(k4_graph_2(A,B,C))) = k4_finseq_4(k5_numbers,A,C,k3_finseq_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_realset1,t2_xreal_1,t18_nat_1,t10_xreal_1,t13_graph_2,t38_nat_1,t24_finseq_4,t16_graph_2,t24_finseq_4]), [file(amistd_1,t6_amistd_1),interesting(0.54)]). fof(t55_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => k10_amistd_1(A,B,C) = k5_amistd_1(A,B,k5_binarith(k4_card_1(C),1)) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_amistd_1,t26_amistd_1,d21_ordinal2,t50_amistd_1,t12_jordan3,t8_xreal_1,t59_card_2,t39_nat_1,t53_binarith,t50_amistd_1,t53_amistd_1,t28_amistd_1,t29_nat_1,t1_xreal_1,d5_real_1]), [file(amistd_1,t55_amistd_1),interesting(0.53)]). fof(t26_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ? [D] : ( v4_ordinal2(D) & C = k5_amistd_1(A,B,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_amistd_1,d4_funct_2,d3_funct_2,d5_funct_1,d1_funct_2,d12_amistd_1]), [file(amistd_1,t26_amistd_1),interesting(0.51)]). fof(t50_amistd_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v4_amistd_1(C,B) & l1_ami_1(C,B) ) => ! [D] : ( ( v1_ami_3(D,B,C) & v9_amistd_1(D,B,C) & m1_ami_1(D,B,C) ) => ( ~ r1_xreal_0(k4_card_1(D),A) <=> r2_hidden(k5_amistd_1(B,C,A),k1_relat_1(D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_ami_3,t26_amistd_1,d21_ordinal2,t25_amistd_1,s3_funct_7,s7_domain_1,t28_amistd_1,d20_amistd_1,t22_funct_7,d21_ordinal2,t78_finseq_1,d5_card_1,t73_card_1,t21_pre_circ,t21_card_1,t21_card_1,t21_pre_circ,t73_card_1]), [file(amistd_1,t50_amistd_1),interesting(0.50)]). fof(t25_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( v4_ordinal2(C) => ! [D] : ( v4_ordinal2(D) => ( k5_amistd_1(A,B,C) = k5_amistd_1(A,B,D) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_ordinal2,d12_amistd_1,d12_amistd_1,t17_amistd_1,d1_funct_2,d4_funct_2,d8_funct_1]), [file(amistd_1,t25_amistd_1),interesting(0.49)]). fof(t28_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( v4_ordinal2(C) => ! [D] : ( v4_ordinal2(D) => ( r1_amistd_1(A,B,k5_amistd_1(A,B,C),k5_amistd_1(A,B,D)) <=> r1_xreal_0(C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_ordinal2,d12_amistd_1,d12_amistd_1,t17_amistd_1]), [file(amistd_1,t28_amistd_1),interesting(0.48)]). fof(t45_amistd_1,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_ami_1(C,A,B) => ( v6_amistd_1(C,A,B) => v7_amistd_1(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d18_amistd_1,d19_ami_1,d17_amistd_1,d5_ami_5,t8_grfunc_1,t54_ami_1,d19_ami_1,s1_nat_1]), [file(amistd_1,t45_amistd_1),interesting(0.48)]). fof(t39_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m1_struct_0(B,k4_amistd_1(A),u2_ami_1(A,k4_amistd_1(A))) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => ( k1_ami_5(A,k4_amistd_1(A),C) = 1 => k1_amistd_1(A,k4_amistd_1(A),B,C) = k1_struct_0(k4_amistd_1(A),k9_amistd_1(A,k4_amistd_1(A),B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t26_amistd_1,t37_amistd_1,d13_amistd_1,t37_amistd_1,l39_amistd_1]), [file(amistd_1,t39_amistd_1),interesting(0.47)]). fof(t2_amistd_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_pre_circ(k6_domain_1(k5_numbers,A)) = A ) ), inference(mizar_proof,[status(thm)],[t1_amistd_1]), [file(amistd_1,t2_amistd_1),interesting(0.46)]). fof(t23_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => v2_amistd_1(B,A,k4_amistd_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d11_amistd_1,d3_amistd_1,d4_amistd_1,d2_xboole_0,d1_tarski,d13_ami_1]), [file(amistd_1,t23_amistd_1),interesting(0.40)]). fof(t35_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => C != k9_amistd_1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_amistd_1]), [file(amistd_1,t35_amistd_1),interesting(0.39)]). fof(l32_amistd_1,theorem,( ! [A,B] : k1_relat_1(k1_funct_4(k2_pre_circ(k5_numbers,A),k3_cqc_lang(k5_numbers,B))) = k2_xboole_0(k5_numbers,k6_domain_1(k1_zfmisc_1(k1_numbers),k5_numbers)) ), inference(mizar_proof,[status(thm)],[d1_funct_4,t19_funcop_1,t19_funcop_1]), [file(amistd_1,l32_amistd_1),interesting(0.38)]). fof(t51_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => r2_hidden(k10_amistd_1(A,B,C),k1_relat_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_amistd_1,d1_pre_circ,d13_amistd_1]), [file(amistd_1,t51_amistd_1),interesting(0.38)]). fof(t47_amistd_1,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] : ( ( v1_xboole_0(C) & m1_ami_1(C,A,B) ) => v9_amistd_1(C,A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_amistd_1]), [file(amistd_1,t47_amistd_1),interesting(0.38)]). fof(t46_amistd_1,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) & v8_ami_1(B,A) & v10_ami_1(B,A) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => v6_amistd_1(k14_ami_3(A,B,k5_amistd_1(A,B,0),k5_ami_1(A,B)),A,B) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d17_amistd_1,d1_tarski,d5_ami_5,t6_cqc_lang,t15_amistd_1]), [file(amistd_1,t46_amistd_1),interesting(0.37)]). fof(l12_amistd_1,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_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ! [E] : ( m1_ami_1(E,A,B) => ( E = k14_ami_3(A,B,C,D) => v11_ami_1(E,A,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d25_ami_1,t5_cqc_lang,d1_tarski,t8_grfunc_1,t6_cqc_lang,t36_ami_3,t91_relat_1,t36_ami_3,t91_relat_1,d1_tarski,t38_ami_3,t38_ami_3,t72_funct_1,t72_funct_1,t9_funct_1]), [file(amistd_1,l12_amistd_1),interesting(0.36)]). fof(t32_amistd_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v4_amistd_1(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m1_struct_0(D,C,u2_ami_1(B,C)) => ! [E] : ( m1_struct_0(E,C,u2_ami_1(B,C)) => ( k8_amistd_1(B,C,D,A) = k8_amistd_1(B,C,E,A) => D = E ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_amistd_1,t27_amistd_1]), [file(amistd_1,t32_amistd_1),interesting(0.35)]). fof(l39_amistd_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( m1_struct_0(C,k4_amistd_1(B),u2_ami_1(B,k4_amistd_1(B))) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,k4_amistd_1(B)),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(k4_amistd_1(B))))),u4_ami_1(B,k4_amistd_1(B))) => ( ( C = A & k1_ami_5(B,k4_amistd_1(B),D) = 1 ) => k1_amistd_1(B,k4_amistd_1(B),C,D) = k1_tarski(k2_xcmplx_0(A,1)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_ordinal2,l34_amistd_1,t52_card_1,d1_tarski,d1_tarski,t52_card_1,t19_funcop_1,t11_amistd_1,d11_ami_1,t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,t48_ami_1,d1_tarski,t12_funct_4,t14_funct_4,t13_funcop_1,l34_amistd_1,t2_tarski]), [file(amistd_1,l39_amistd_1),interesting(0.31)]). fof(t38_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,k4_amistd_1(A)))) => ( k1_ami_5(A,k4_amistd_1(A),B) = 1 => k1_funct_1(k4_ami_1(A,k4_amistd_1(A),B,C),k2_ami_1(A,k4_amistd_1(A))) = k9_amistd_1(A,k4_amistd_1(A),k6_ami_1(A,k4_amistd_1(A),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t37_amistd_1,d11_amistd_1,l34_amistd_1,t52_card_1,d13_amistd_1]), [file(amistd_1,t38_amistd_1),interesting(0.30)]). fof(t14_amistd_1,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] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => k1_amistd_1(A,B,D,C) = k1_struct_0(B,D) ) => ( v1_realset1(u2_ami_1(A,B)) | v1_xboole_0(k2_amistd_1(A,B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_yellow_8,d1_xboole_0,d1_setfam_1,d1_tarski]), [file(amistd_1,t14_amistd_1),interesting(0.29)]). fof(t31_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => k8_amistd_1(A,B,C,0) = C ) ) ) ), inference(mizar_proof,[status(thm)],[d13_amistd_1]), [file(amistd_1,t31_amistd_1),interesting(0.28)]). fof(t15_amistd_1,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) & v10_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( v3_ami_1(D,A,B) => k1_amistd_1(A,B,C,D) = k1_struct_0(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_ami_1,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d11_ami_1,d14_ami_1,t58_ami_1,t65_funct_4,d2_tarski,d2_tarski,t48_ami_1,t14_funct_4,t66_funct_4,t14_funct_4,t66_funct_4,d1_tarski,l20_amistd_1]), [file(amistd_1,t15_amistd_1),interesting(0.27)]). fof(t12_amistd_1,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_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => v11_ami_1(k14_ami_3(A,B,C,D),A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l12_amistd_1]), [file(amistd_1,t12_amistd_1),interesting(0.23)]). fof(t33_amistd_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v4_amistd_1(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m1_struct_0(D,C,u2_ami_1(B,C)) => k2_xcmplx_0(k7_amistd_1(B,C,D),A) = k7_amistd_1(B,C,k8_amistd_1(B,C,D,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_amistd_1]), [file(amistd_1,t33_amistd_1),interesting(0.21)]). fof(l34_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,k4_amistd_1(A)))) => ( k1_ami_5(A,k4_amistd_1(A),B) = 1 => k1_funct_1(k4_ami_1(A,k4_amistd_1(A),B,C),k2_ami_1(A,k4_amistd_1(A))) = k1_ordinal1(k6_ami_1(A,k4_amistd_1(A),C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_ami_5,d11_amistd_1,d11_amistd_1,d2_tarski,t7_mcart_1,d1_tarski,d1_tarski,t7_mcart_1,t19_funcop_1,t12_funct_4,t13_funcop_1,d1_tarski,t19_funcop_1,t14_funct_4,t13_funcop_1]), [file(amistd_1,l34_amistd_1),interesting(0.19)]). fof(t43_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ~ ( ~ v1_xboole_0(k2_amistd_1(A,B,C)) & v5_amistd_1(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xboole_0,d1_setfam_1,d16_amistd_1,t35_amistd_1]), [file(amistd_1,t43_amistd_1),interesting(0.14)]). fof(t48_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => v9_amistd_1(k14_ami_3(A,B,k5_amistd_1(A,B,0),C),A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d20_amistd_1,d1_tarski,t26_amistd_1,t28_amistd_1,t18_nat_1,t1_xreal_1]), [file(amistd_1,t48_amistd_1),interesting(0.09)]). fof(t17_amistd_1,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] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u2_ami_1(A,B)) & m2_relset_1(C,k5_numbers,u2_ami_1(A,B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u2_ami_1(A,B)) & m2_relset_1(D,k5_numbers,u2_ami_1(A,B)) ) => ( ( v3_funct_2(C,k5_numbers,u2_ami_1(A,B)) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( r1_xreal_0(E,F) <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E),k8_funct_2(k5_numbers,u2_ami_1(A,B),C,F)) ) ) ) & v3_funct_2(D,k5_numbers,u2_ami_1(A,B)) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( r1_xreal_0(E,F) <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),D,E),k8_funct_2(k5_numbers,u2_ami_1(A,B),D,F)) ) ) ) ) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_funct_2,s5_nat_1,d4_funct_2,d3_funct_2,d5_funct_1,d1_funct_2,d5_funct_1,d1_funct_2,d4_funct_2,d1_funct_2,t1_xreal_1,t1_xreal_1,d8_funct_1,t1_xreal_1,d8_funct_1,t1_xreal_1]), [file(amistd_1,t17_amistd_1),interesting(0.07)]). fof(l83_amistd_1,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) & v8_ami_1(B,A) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ( k1_funct_1(k14_ami_3(A,B,k5_amistd_1(A,B,0),k5_ami_1(A,B)),k10_amistd_1(A,B,k14_ami_3(A,B,k5_amistd_1(A,B,0),k5_ami_1(A,B)))) = k5_ami_1(A,B) & ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ( ( k1_funct_1(k14_ami_3(A,B,k5_amistd_1(A,B,0),k5_ami_1(A,B)),C) = k5_ami_1(A,B) & r2_hidden(C,k1_relat_1(k14_ami_3(A,B,k5_amistd_1(A,B,0),k5_ami_1(A,B)))) ) => C = k10_amistd_1(A,B,k14_ami_3(A,B,k5_amistd_1(A,B,0),k5_ami_1(A,B))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t79_card_1,t48_amistd_1,t55_amistd_1,t21_pre_circ,t51_binarith,t6_cqc_lang,d1_tarski]), [file(amistd_1,l83_amistd_1),interesting(0.02)]). 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(t19_funcop_1,theorem,( ! [A,B] : ( k1_relat_1(k2_funcop_1(A,B)) = A & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ), file(funcop_1,t19_funcop_1), [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(t79_card_1,theorem,( ! [A] : k4_card_1(k1_tarski(A)) = 1 ), file(card_1,t79_card_1), [interesting(0.00)]). fof(d20_amistd_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) => ( v9_amistd_1(C,A,B) <=> ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r2_hidden(D,k1_relat_1(C)) => ! [E] : ( m1_struct_0(E,B,u2_ami_1(A,B)) => ( r1_amistd_1(A,B,E,D) => r2_hidden(E,k1_relat_1(C)) ) ) ) ) ) ) ) ) ), file(amistd_1,d20_amistd_1), [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(d12_amistd_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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( v4_ordinal2(C) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( D = k5_amistd_1(A,B,C) <=> ? [E] : ( v1_funct_1(E) & v1_funct_2(E,k5_numbers,u2_ami_1(A,B)) & m2_relset_1(E,k5_numbers,u2_ami_1(A,B)) & v3_funct_2(E,k5_numbers,u2_ami_1(A,B)) & ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ! [G] : ( m2_subset_1(G,k1_numbers,k5_numbers) => ( r1_xreal_0(F,G) <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),E,F),k8_funct_2(k5_numbers,u2_ami_1(A,B),E,G)) ) ) ) & D = k1_funct_1(E,C) ) ) ) ) ) ) ), file(amistd_1,d12_amistd_1), [interesting(0.00)]). fof(d4_funct_2,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( v3_funct_2(C,A,B) <=> ( v2_funct_1(C) & v2_funct_2(C,A,B) ) ) ) ), file(funct_2,d4_funct_2), [interesting(0.00)]). fof(d3_funct_2,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( v2_funct_2(C,A,B) <=> k2_relat_1(C) = B ) ) ), file(funct_2,d3_funct_2), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(d21_ordinal2,definition,( ! [A] : ( v4_ordinal2(A) <=> r2_hidden(A,k5_ordinal2) ) ), file(ordinal2,d21_ordinal2), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(s5_nat_1,theorem, ( ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s5_nat_1(A) ) => ? [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) & p1_s5_nat_1(A) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( p1_s5_nat_1(B) => r1_xreal_0(A,B) ) ) ) ), file(nat_1,s5_nat_1), [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(d8_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) & k1_funct_1(A,B) = k1_funct_1(A,C) ) => B = C ) ) ) ), file(funct_1,d8_funct_1), [interesting(0.00)]). fof(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_nat_1), [interesting(0.00)]). fof(d21_amistd_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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( D = k10_amistd_1(A,B,C) <=> ? [E] : ( ~ v1_xboole_0(E) & v1_finset_1(E) & v5_membered(E) & E = a_3_2_amistd_1(A,B,C) & D = k5_amistd_1(A,B,k1_pre_circ(E)) ) ) ) ) ) ) ), file(amistd_1,d21_amistd_1), [interesting(0.00)]). fof(d1_pre_circ,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_finset_1(A) & v2_membered(A) ) => ! [B] : ( v1_xreal_0(B) => ( B = k1_pre_circ(A) <=> ( r2_hidden(B,A) & ! [C] : ( v1_xreal_0(C) => ( r2_hidden(C,A) => r1_xreal_0(C,B) ) ) ) ) ) ) ), file(pre_circ,d1_pre_circ), [interesting(0.00)]). fof(d13_amistd_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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( v4_ordinal2(D) => ( D = k6_amistd_1(A,B,C) <=> k5_amistd_1(A,B,D) = C ) ) ) ) ) ), file(amistd_1,d13_amistd_1), [interesting(0.00)]). fof(d13_ami_3,definition,( ! [A,B] : ( l1_ami_1(B,A) => ! [C] : ( m1_ami_1(C,A,B) => ( v1_ami_3(C,A,B) <=> r1_tarski(k1_relat_1(C),u2_ami_1(A,B)) ) ) ) ), file(ami_3,d13_ami_3), [interesting(0.00)]). fof(s3_funct_7,theorem, ( ( ! [A] : ~ ( r2_hidden(A,f1_s3_funct_7) & ! [B] : ( m1_subset_1(B,f2_s3_funct_7) => A != f3_s3_funct_7(B) ) ) & ! [A] : ( m1_subset_1(A,f2_s3_funct_7) => ! [B] : ( m1_subset_1(B,f2_s3_funct_7) => ( f3_s3_funct_7(A) = f3_s3_funct_7(B) => A = B ) ) ) ) => r2_tarski(f1_s3_funct_7,a_0_1_funct_7) ), file(funct_7,s3_funct_7), [interesting(0.00)]). fof(s7_domain_1,theorem,( m1_subset_1(a_0_0_domain_1,k1_zfmisc_1(f1_s7_domain_1)) ), file(domain_1,s7_domain_1), [interesting(0.00)]). fof(t22_funct_7,theorem,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(k5_numbers)) => ( ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(B,A) => ( r1_xreal_0(B,C) | r2_hidden(C,A) ) ) ) ) => v1_card_1(A) ) ) ), file(funct_7,t22_funct_7), [interesting(0.00)]). fof(t78_finseq_1,theorem, ( ! [A] : ( v4_ordinal2(A) => k4_card_1(k2_finseq_1(A)) = A ) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( k4_card_1(A) = A & k4_card_1(k1_card_1(A)) = A ) ) ), file(finseq_1,t78_finseq_1), [interesting(0.00)]). fof(d5_card_1,definition,( ! [A,B] : ( v1_card_1(B) => ( B = k1_card_1(A) <=> r2_wellord2(A,B) ) ) ), file(card_1,d5_card_1), [interesting(0.00)]). fof(t73_card_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(k1_card_1(A),k1_card_1(B)) <=> ~ r1_xreal_0(B,A) ) ) ) ), file(card_1,t73_card_1), [interesting(0.00)]). fof(t21_pre_circ,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => k1_card_1(A) = k1_card_1(k1_relat_1(A)) ) ), file(pre_circ,t21_pre_circ), [interesting(0.00)]). fof(t21_card_1,theorem,( ! [A,B] : ( r2_wellord2(A,B) <=> k1_card_1(A) = k1_card_1(B) ) ), file(card_1,t21_card_1), [interesting(0.00)]). fof(t12_jordan3,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ ( r1_xreal_0(B,A) & ~ r1_xreal_0(k2_xcmplx_0(A,1),B) ) => r1_xreal_0(A,k5_binarith(B,1)) ) ) ) ), file(jordan3,t12_jordan3), [interesting(0.00)]). fof(t8_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(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(t59_card_2,theorem,( ! [A] : ( k1_card_1(A) = 0 => A = k1_xboole_0 ) ), file(card_2,t59_card_2), [interesting(0.00)]). fof(t39_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(1,A) => A = 0 ) ) ), file(nat_1,t39_nat_1), [interesting(0.00)]). fof(t53_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(B,A) => k2_xcmplx_0(k5_binarith(A,B),B) = A ) ) ) ), file(binarith,t53_binarith), [interesting(0.00)]). fof(t29_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r1_xreal_0(k7_amistd_1(A,B,C),k7_amistd_1(A,B,D)) <=> r1_amistd_1(A,B,C,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_amistd_1,t28_amistd_1]), [file(amistd_1,t29_amistd_1),interesting(0.00)]). fof(t53_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r2_hidden(D,k1_relat_1(C)) => r1_amistd_1(A,B,D,k10_amistd_1(A,B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_amistd_1,d13_amistd_1,d1_pre_circ,t29_amistd_1]), [file(amistd_1,t53_amistd_1),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(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t51_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => k5_binarith(A,A) = 0 ) ), file(binarith,t51_binarith), [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(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(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(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(t91_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), [interesting(0.00)]). fof(t38_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] : ( ( v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => ( r1_tarski(C,D) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => r1_tarski(C,k11_ami_1(A,B,k10_ami_1(A,B,D),E)) ) ) ) ) ) ) ), file(ami_3,t38_ami_3), [interesting(0.00)]). fof(t72_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,A) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t72_funct_1), [interesting(0.00)]). fof(t9_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( 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) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), [interesting(0.00)]). fof(d27_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) ) => ( v13_ami_1(B,A) <=> ? [C] : ( m1_ami_1(C,A,B) & ~ v1_xboole_0(C) & v11_ami_1(C,A,B) ) ) ) ) ), file(ami_1,d27_ami_1), [interesting(0.00)]). fof(d8_amistd_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_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r1_amistd_1(A,B,C,D) <=> ? [E] : ( ~ v1_xboole_0(E) & m2_finseq_1(E,u2_ami_1(A,B)) & k4_finseq_4(k5_numbers,u2_ami_1(A,B),E,1) = C & k4_finseq_4(k5_numbers,u2_ami_1(A,B),E,k3_finseq_1(E)) = D & ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( r1_xreal_0(1,F) => ( r1_xreal_0(k3_finseq_1(E),F) | r2_hidden(k4_finseq_4(k5_numbers,u2_ami_1(A,B),E,k1_nat_1(F,1)),k3_amistd_1(A,B,k4_finseq_4(k5_numbers,u2_ami_1(A,B),E,F))) ) ) ) ) ) ) ) ) ) ), file(amistd_1,d8_amistd_1), [interesting(0.00)]). fof(t6_finseq_5,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( r2_hidden(1,k4_finseq_1(A)) & r2_hidden(k3_finseq_1(A),k4_finseq_1(A)) ) ) ), file(finseq_5,t6_finseq_5), [interesting(0.00)]). fof(d2_graph_2,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_graph_2(A,B) = k7_finseq_1(A,k1_graph_2(B,2,k3_finseq_1(B))) ) ) ), file(graph_2,d2_graph_2), [interesting(0.00)]). fof(d4_finseq_4,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,B) ) => ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ), file(finseq_4,d4_finseq_4), [interesting(0.00)]). fof(d7_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k7_finseq_1(A,B) <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ), file(finseq_1,d7_finseq_1), [interesting(0.00)]). fof(d4_realset1,definition,( ! [A] : ( v1_realset1(A) <=> ~ ( ~ v1_xboole_0(A) & ! [B] : A != k1_tarski(B) ) ) ), file(realset1,d4_realset1), [interesting(0.00)]). fof(d1_relat_1,definition,( ! [A] : ( v1_relat_1(A) <=> ! [B] : ~ ( r2_hidden(B,A) & ! [C,D] : B != k4_tarski(C,D) ) ) ), file(relat_1,d1_relat_1), [interesting(0.00)]). fof(d5_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : r2_hidden(k4_tarski(D,C),A) ) ) ) ), file(relat_1,d5_relat_1), [interesting(0.00)]). fof(d4_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( m1_finseq_1(B,A) <=> r1_tarski(k2_relat_1(B),A) ) ) ), file(finseq_1,d4_finseq_1), [interesting(0.00)]). fof(t23_relat_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( C = k1_tarski(k4_tarski(A,B)) => ( k1_relat_1(C) = k1_tarski(A) & k2_relat_1(C) = k1_tarski(B) ) ) ) ), file(relat_1,t23_relat_1), [interesting(0.00)]). fof(d5_finseq_1,definition,( ! [A] : k5_finseq_1(A) = k1_tarski(k4_tarski(1,A)) ), file(finseq_1,d5_finseq_1), [interesting(0.00)]). fof(t56_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t56_finseq_1), [interesting(0.00)]). fof(d1_graph_2,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ( ( ( r1_xreal_0(1,B) & r1_xreal_0(B,k1_nat_1(C,1)) & r1_xreal_0(C,k3_finseq_1(A)) ) => ( D = k1_graph_2(A,B,C) <=> ( k1_nat_1(k3_finseq_1(D),B) = k1_nat_1(C,1) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(k3_finseq_1(D),E) => k1_funct_1(D,k1_nat_1(E,1)) = k1_funct_1(A,k1_nat_1(B,E)) ) ) ) ) ) & ( ~ ( r1_xreal_0(1,B) & r1_xreal_0(B,k1_nat_1(C,1)) & r1_xreal_0(C,k3_finseq_1(A)) ) => ( D = k1_graph_2(A,B,C) <=> D = k1_xboole_0 ) ) ) ) ) ) ) ), file(graph_2,d1_graph_2), [interesting(0.00)]). fof(t25_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k3_finseq_1(A) = 0 <=> A = k1_xboole_0 ) ) ), file(finseq_1,t25_finseq_1), [interesting(0.00)]). fof(t47_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k7_finseq_1(A,k1_xboole_0) = A & k7_finseq_1(k1_xboole_0,A) = A ) ) ), file(finseq_1,t47_finseq_1), [interesting(0.00)]). fof(t13_realset1,theorem,( ! [A] : ( v1_finset_1(A) => ( v1_realset1(A) <=> ~ r1_xreal_0(2,k4_card_1(A)) ) ) ), file(realset1,t13_realset1), [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(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t13_graph_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( A != k1_xboole_0 => k1_nat_1(k3_finseq_1(k3_graph_2(B,A)),1) = k1_nat_1(k3_finseq_1(B),k3_finseq_1(A)) ) ) ) ), file(graph_2,t13_graph_2), [interesting(0.00)]). fof(t38_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), file(nat_1,t38_nat_1), [interesting(0.00)]). fof(t24_finseq_4,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(B)) ) => k4_finseq_4(k5_numbers,A,B,C) = k1_funct_1(B,C) ) ) ) ), file(finseq_4,t24_finseq_4), [interesting(0.00)]). fof(t16_graph_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( ~ r1_xreal_0(k3_finseq_1(A),1) => k1_funct_1(k3_graph_2(B,A),k3_finseq_1(k3_graph_2(B,A))) = k1_funct_1(A,k3_finseq_1(A)) ) ) ) ), file(graph_2,t16_graph_2), [interesting(0.00)]). fof(t19_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( 0 != A & r1_xreal_0(A,0) ) ) ), file(nat_1,t19_nat_1), [interesting(0.00)]). fof(t14_graph_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(A)) ) => k1_funct_1(k3_graph_2(A,B),C) = k1_funct_1(A,C) ) ) ) ) ), file(graph_2,t14_graph_2), [interesting(0.00)]). fof(t9_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t15_graph_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(1,C) => ( r1_xreal_0(k3_finseq_1(A),C) | k1_funct_1(k3_graph_2(B,A),k1_nat_1(k3_finseq_1(B),C)) = k1_funct_1(A,k1_nat_1(C,1)) ) ) ) ) ) ), file(graph_2,t15_graph_2), [interesting(0.00)]). fof(t10_amistd_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( m2_finseq_1(D,A) => ( r1_xreal_0(1,B) => ( r1_xreal_0(k3_finseq_1(D),B) | k4_finseq_4(k5_numbers,A,k4_graph_2(A,C,D),k1_nat_1(k3_finseq_1(C),B)) = k4_finseq_4(k5_numbers,A,D,k1_nat_1(B,1)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_nat_1,t9_xreal_1,t13_graph_2,t8_xreal_1,t38_nat_1,t25_finseq_1,t18_nat_1,t18_nat_1,t8_xreal_1,t38_nat_1,t24_finseq_4,t15_graph_2,t24_finseq_4]), [file(amistd_1,t10_amistd_1),interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(d10_amistd_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) ) => ( v4_amistd_1(B,A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u2_ami_1(A,B)) & m2_relset_1(C,k5_numbers,u2_ami_1(A,B)) & v3_funct_2(C,k5_numbers,u2_ami_1(A,B)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_xreal_0(D,E) <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D),k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E)) ) ) ) ) ) ) ) ), file(amistd_1,d10_amistd_1), [interesting(0.00)]). fof(t3_revrot_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( ~ v1_xboole_0(B) & m2_finseq_1(B,A) ) => r2_hidden(k4_finseq_4(k5_numbers,A,B,k3_finseq_1(B)),k2_relat_1(B)) ) ) ), file(revrot_1,t3_revrot_1), [interesting(0.00)]). fof(t29_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => k1_funct_1(A,k5_finseq_4(A,B)) = B ) ) ), file(finseq_4,t29_finseq_4), [interesting(0.00)]). fof(t30_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r2_hidden(k5_finseq_4(A,B),k4_finseq_1(A)) ) ) ), file(finseq_4,t30_finseq_4), [interesting(0.00)]). fof(t27_finseq_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(B,k4_finseq_1(A)) <=> ( r1_xreal_0(1,B) & r1_xreal_0(B,k3_finseq_1(A)) ) ) ) ) ), file(finseq_3,t27_finseq_3), [interesting(0.00)]). fof(t46_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => k3_finseq_1(k6_finseq_4(A,B)) = k6_xcmplx_0(k5_finseq_4(A,B),1) ) ) ), file(finseq_4,t46_finseq_4), [interesting(0.00)]). fof(t53_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( ~ v1_xboole_0(C) => ( ( r2_hidden(B,k2_relat_1(A)) & m2_finseq_1(A,C) ) => m2_finseq_1(k6_finseq_4(A,B),C) ) ) ) ), file(finseq_4,t53_finseq_4), [interesting(0.00)]). fof(t48_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B,C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r2_hidden(B,k2_relat_1(A)) & r2_hidden(C,k4_finseq_1(k6_finseq_4(A,B))) ) => k1_funct_1(A,C) = k1_funct_1(k6_finseq_4(A,B),C) ) ) ) ), file(finseq_4,t48_finseq_4), [interesting(0.00)]). fof(t61_finseq_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k10_finseq_1(A,B) <=> ( k3_finseq_1(C) = 2 & k1_funct_1(C,1) = A & k1_funct_1(C,2) = B ) ) ) ), file(finseq_1,t61_finseq_1), [interesting(0.00)]). fof(t3_cqc_the1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( r1_xreal_0(A,2) & A != 0 & A != 1 & A != 2 ) ) ), file(cqc_the1,t3_cqc_the1), [interesting(0.00)]). fof(t27_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & r1_xreal_0(B,k2_xcmplx_0(A,1)) & A != B & B != k2_xcmplx_0(A,1) ) ) ) ), file(nat_1,t27_nat_1), [interesting(0.00)]). fof(t50_finseq_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( r2_hidden(B,k2_relat_1(A)) => r1_xboole_0(k2_relat_1(k6_finseq_4(A,B)),k1_tarski(B)) ) ) ), file(finseq_4,t50_finseq_4), [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(s1_finseq_2,theorem,( ? [A] : ( m2_finseq_1(A,f2_s1_finseq_2) & k3_finseq_1(A) = f1_s1_finseq_2 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k2_finseq_1(f1_s1_finseq_2)) => k1_funct_1(A,B) = f3_s1_finseq_2(B) ) ) ) ), file(finseq_2,s1_finseq_2), [interesting(0.00)]). fof(t20_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ~ r1_xreal_0(B,A) => r1_xreal_0(k2_xcmplx_0(A,1),B) ) ) ) ), file(int_1,t20_int_1), [interesting(0.00)]). fof(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [interesting(0.00)]). fof(d3_binarith,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ( r1_xreal_0(0,k6_xcmplx_0(A,B)) => k5_binarith(A,B) = k6_xcmplx_0(A,B) ) & ( ~ r1_xreal_0(0,k6_xcmplx_0(A,B)) => k5_binarith(A,B) = 0 ) ) ) ) ), file(binarith,d3_binarith), [interesting(0.00)]). fof(d3_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k3_finseq_1(A) <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ), file(finseq_1,d3_finseq_1), [interesting(0.00)]). fof(t39_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => k5_binarith(k2_xcmplx_0(A,B),B) = A ) ) ), file(binarith,t39_binarith), [interesting(0.00)]). fof(t3_jordan4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(A,B) => k5_binarith(k1_nat_1(B,C),A) = k1_nat_1(k5_binarith(B,A),C) ) ) ) ) ), file(jordan4,t3_jordan4), [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(t18_amistd_1,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] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u2_ami_1(A,B)) & m2_relset_1(C,k5_numbers,u2_ami_1(A,B)) ) => ( v3_funct_2(C,k5_numbers,u2_ami_1(A,B)) => ( ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_xreal_0(D,E) <=> r1_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D),k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E)) ) ) ) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(A,B),C,k1_nat_1(D,1)),k3_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D))) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E),k3_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D))) => r1_xreal_0(D,E) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,d8_amistd_1,t25_finseq_1,t39_nat_1,d4_funct_2,d1_funct_2,d8_funct_1,t3_revrot_1,t29_finseq_4,t30_finseq_4,t27_finseq_3,t27_finseq_3,d4_finseq_4,d5_real_1,t46_finseq_4,t38_nat_1,d4_finseq_4,t29_finseq_4,d4_finseq_4,t25_finseq_1,t53_finseq_4,d3_funct_2,d5_funct_1,d1_funct_2,t27_finseq_3,d4_finseq_4,t48_finseq_4,d4_finseq_4,t27_finseq_3,t27_finseq_3,d4_finseq_4,t48_finseq_4,d4_finseq_4,t27_finseq_3,t38_nat_1,t27_finseq_3,t2_xreal_1,t27_finseq_3,t2_xreal_1,t27_finseq_3,d4_finseq_4,t48_finseq_4,d4_finseq_4,d4_finseq_4,t48_finseq_4,d4_finseq_4,t2_xreal_1,d8_amistd_1,t61_finseq_1,t27_finseq_3,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,t3_cqc_the1,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,d8_amistd_1,t27_nat_1,t50_finseq_4,d7_xboole_0,d3_xboole_0,t27_finseq_3,d4_finseq_4,d5_funct_1,d1_tarski,t61_finseq_1,t27_finseq_3,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,t61_finseq_1,t3_cqc_the1,d4_finseq_4,t61_finseq_1,d4_finseq_4,t61_finseq_1,d8_amistd_1,s1_finseq_2,t25_finseq_1,d8_amistd_1,t20_int_1,t21_xreal_1,t2_xreal_1,d3_binarith,t29_nat_1,t27_finseq_3,d3_finseq_1,d4_finseq_4,t39_binarith,d4_finseq_4,t39_binarith,t38_nat_1,t27_finseq_3,d3_finseq_1,t29_nat_1,t2_xreal_1,d4_finseq_4,t3_jordan4,d4_finseq_4,t1_xreal_1,d4_funct_2,d1_funct_2,d8_amistd_1,t39_nat_1,t38_nat_1,t38_nat_1,t39_nat_1,d3_funct_2,d5_funct_1,d1_funct_2,t2_xreal_1,t19_nat_1,s1_nat_1,t25_finseq_1,t39_nat_1,d8_funct_1]), [file(amistd_1,t18_amistd_1),interesting(0.00)]). fof(t19_amistd_1,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) ) => ( v4_amistd_1(B,A) <=> ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u2_ami_1(A,B)) & m2_relset_1(C,k5_numbers,u2_ami_1(A,B)) & v3_funct_2(C,k5_numbers,u2_ami_1(A,B)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(A,B),C,k1_nat_1(D,1)),k3_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D))) & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(k8_funct_2(k5_numbers,u2_ami_1(A,B),C,E),k3_amistd_1(A,B,k8_funct_2(k5_numbers,u2_ami_1(A,B),C,D))) => r1_xreal_0(D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_amistd_1,t18_amistd_1,d10_amistd_1,t18_amistd_1]), [file(amistd_1,t19_amistd_1),interesting(0.00)]). fof(d8_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( v3_ami_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => k4_ami_1(A,B,C,D) = D ) ) ) ) ) ), file(ami_1,d8_ami_1), [interesting(0.00)]). fof(d1_ami_5,definition,( ! [A,B] : ( l1_ami_1(B,A) => ! [C] : ( m1_subset_1(C,u4_ami_1(A,B)) => k1_ami_5(A,B,C) = k1_mcart_1(C) ) ) ), file(ami_5,d1_ami_5), [interesting(0.00)]). fof(d11_amistd_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( v1_ami_1(B,A) & l1_ami_1(B,A) ) => ( B = k4_amistd_1(A) <=> ( u1_struct_0(B) = k2_xboole_0(k5_numbers,k6_domain_1(k1_zfmisc_1(k1_numbers),k5_numbers)) & u1_ami_1(A,B) = k5_numbers & u2_ami_1(A,B) = k5_numbers & u3_ami_1(A,B) = k7_domain_1(k5_numbers,0,1) & u4_ami_1(A,B) = k7_domain_1(k2_zfmisc_1(k5_numbers,k5_numbers),k1_domain_1(k5_numbers,k5_numbers,0,0),k1_domain_1(k5_numbers,k5_numbers,1,0)) & u5_ami_1(A,B) = k1_funct_4(k2_pre_circ(k5_numbers,k7_domain_1(k2_zfmisc_1(k5_numbers,k5_numbers),k1_domain_1(k5_numbers,k5_numbers,1,0),k1_domain_1(k5_numbers,k5_numbers,0,0))),k3_cqc_lang(k5_numbers,k5_numbers)) & ? [C] : ( v1_funct_1(C) & v1_funct_2(C,k4_card_3(u5_ami_1(A,B)),k4_card_3(u5_ami_1(A,B))) & m2_relset_1(C,k4_card_3(u5_ami_1(A,B)),k4_card_3(u5_ami_1(A,B))) & ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => k1_funct_1(C,D) = k1_funct_4(D,k3_cqc_lang(k5_numbers,k1_ordinal1(k1_funct_1(D,k5_numbers)))) ) & u6_ami_1(A,B) = k1_funct_4(k3_cqc_lang(k1_domain_1(k5_numbers,k5_numbers,1,0),C),k3_cqc_lang(k1_domain_1(k5_numbers,k5_numbers,0,0),k6_partfun1(k4_card_3(u5_ami_1(A,B))))) ) ) ) ) ) ), file(amistd_1,d11_amistd_1), [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(t7_mcart_1,theorem,( ! [A,B] : ( k1_mcart_1(k4_tarski(A,B)) = A & k2_mcart_1(k4_tarski(A,B)) = B ) ), file(mcart_1,t7_mcart_1), [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(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [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(t14_ordinal1,theorem,( ! [A] : A != k1_ordinal1(A) ), file(ordinal1,t14_ordinal1), [interesting(0.00)]). fof(t21_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => ~ ( k1_ami_5(A,k4_amistd_1(A),B) = 1 & v3_ami_1(B,A,k4_amistd_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_ami_1,l34_amistd_1,t14_ordinal1]), [file(amistd_1,t21_amistd_1),interesting(0.00)]). fof(d3_amistd_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_subset_1(C,u3_ami_1(A,B)) => ( v1_amistd_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m2_subset_1(F,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( k1_ami_5(A,B,F) = C => ( E = k2_ami_1(A,B) | k1_funct_1(k4_ami_1(A,B,F,D),E) = k1_funct_1(D,E) ) ) ) ) ) ) ) ) ) ), file(amistd_1,d3_amistd_1), [interesting(0.00)]). fof(d4_amistd_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( v2_amistd_1(C,A,B) <=> v1_amistd_1(k1_ami_5(A,B,C),A,B) ) ) ) ) ), file(amistd_1,d4_amistd_1), [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(d13_ami_1,definition,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ( v7_ami_1(B,A) <=> ! [C] : ( m1_subset_1(C,k4_card_3(u5_ami_1(A,B))) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ! [E] : ( m1_struct_0(E,B,u2_ami_1(A,B)) => k1_funct_1(k4_ami_1(A,B,D,C),E) = k1_funct_1(C,E) ) ) ) ) ) ) ), file(ami_1,d13_ami_1), [interesting(0.00)]). fof(d9_amistd_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) ) => ( v3_amistd_1(B,A) <=> ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( ( r1_amistd_1(A,B,C,D) & r1_amistd_1(A,B,D,C) ) => C = D ) ) ) ) ) ) ), file(amistd_1,d9_amistd_1), [interesting(0.00)]). fof(t27_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( k7_amistd_1(A,B,C) = k7_amistd_1(A,B,D) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_amistd_1]), [file(amistd_1,t27_amistd_1),interesting(0.00)]). fof(t34_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => k9_amistd_1(A,B,C) = k5_amistd_1(A,B,k1_nat_1(k7_amistd_1(A,B,C),1)) ) ) ) ), file(amistd_1,t34_amistd_1), [interesting(0.00)]). fof(t36_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( k9_amistd_1(A,B,C) = k9_amistd_1(A,B,D) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_amistd_1,t27_amistd_1]), [file(amistd_1,t36_amistd_1),interesting(0.00)]). fof(t35_funct_1,theorem,( ! [A,B] : ( r2_hidden(B,A) => k1_funct_1(k6_relat_1(A),B) = B ) ), file(funct_1,t35_funct_1), [interesting(0.00)]). fof(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [interesting(0.00)]). fof(t52_card_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_ordinal1(A) = k1_nat_1(A,1) ) ), file(card_1,t52_card_1), [interesting(0.00)]). fof(d14_ami_1,definition,( ! [A,B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & l1_ami_1(B,A) ) => ( v8_ami_1(B,A) <=> ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => k3_ami_1(A,B,C) = u4_ami_1(A,B) ) ) ) ), file(ami_1,d14_ami_1), [interesting(0.00)]). fof(d16_ami_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k7_ami_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( v1_relat_1(D) & v1_funct_1(D) & C = D & r1_tarski(k1_relat_1(D),k1_relat_1(A)) & ! [E] : ( r2_hidden(E,k1_relat_1(D)) => r2_hidden(k1_funct_1(D,E),k1_funct_1(A,E)) ) ) ) ) ) ), file(ami_1,d16_ami_1), [interesting(0.00)]). fof(t29_ami_1,theorem,( ! [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) ) => ( ( r2_hidden(A,k4_card_3(B)) & r2_hidden(C,k7_ami_1(B)) ) => r2_hidden(k1_funct_4(A,C),k4_card_3(B)) ) ) ) ) ), file(ami_1,t29_ami_1), [interesting(0.00)]). fof(t11_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v8_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => m1_subset_1(k1_funct_4(D,k2_pre_circ(u2_ami_1(A,B),C)),k4_card_3(u5_ami_1(A,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_funcop_1,t36_ami_3,d1_funct_2,t13_funcop_1,t19_funcop_1,d14_ami_1,d16_ami_1,t29_ami_1]), [file(amistd_1,t11_amistd_1),interesting(0.00)]). fof(d11_ami_1,definition,( ! [A,B] : ( ( ~ v3_struct_0(B) & l1_ami_1(B,A) ) => ( v5_ami_1(B,A) <=> k3_ami_1(A,B,k2_ami_1(A,B)) = u2_ami_1(A,B) ) ) ), file(ami_1,d11_ami_1), [interesting(0.00)]). fof(t48_ami_1,theorem,( ! [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) ) => ( v10_ami_1(B,A) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => k2_ami_1(A,B) != C ) ) ) ), file(ami_1,t48_ami_1), [interesting(0.00)]). fof(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [interesting(0.00)]). fof(d1_setfam_1,definition,( ! [A,B] : ( ( A != k1_xboole_0 => ( B = k1_setfam_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ! [D] : ( r2_hidden(D,A) => r2_hidden(C,D) ) ) ) ) & ( A = k1_xboole_0 => ( B = k1_setfam_1(A) <=> B = k1_xboole_0 ) ) ) ), file(setfam_1,d1_setfam_1), [interesting(0.00)]). fof(t20_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => ( k1_ami_5(A,k4_amistd_1(A),B) = 0 => v3_ami_1(B,A,k4_amistd_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_ami_5,d11_amistd_1,d8_ami_1,d11_amistd_1,d2_tarski,t7_mcart_1,d1_tarski,t19_funcop_1,t14_funct_4,t13_funcop_1,t35_funct_1]), [file(amistd_1,t20_amistd_1),interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(t58_ami_1,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,D,E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ( ( k3_ami_1(A,B,E) = C & k3_ami_1(A,B,F) = D ) => ! [G] : ( m1_subset_1(G,C) => ! [H] : ( m1_subset_1(H,D) => m1_ami_1(k4_funct_4(E,F,G,H),A,B) ) ) ) ) ) ) ) ), file(ami_1,t58_ami_1), [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(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(l20_amistd_1,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) & v10_ami_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ! [E] : ( m1_subset_1(E,k4_card_3(u5_ami_1(A,B))) => ! [F] : ( m1_ami_1(F,A,B) => ( F = k4_funct_4(k2_ami_1(A,B),D,D,C) => r2_hidden(k6_ami_1(A,B,k9_ami_1(A,B,k8_ami_5(A,B,E,F))),k1_amistd_1(A,B,D,C)) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t48_ami_1,t65_funct_4,d2_tarski,t14_funct_4,t66_funct_4,d2_tarski,t14_funct_4,t66_funct_4]), [file(amistd_1,l20_amistd_1),interesting(0.00)]). fof(d1_yellow_8,definition,( ! [A] : ( ~ v1_xboole_0(A) => ( v1_realset1(A) <=> ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => B = C ) ) ) ) ), file(yellow_8,d1_yellow_8), [interesting(0.00)]). fof(d1_mcart_1,definition,( ! [A] : ( ? [B,C] : A = k4_tarski(B,C) => ! [B] : ( B = k1_mcart_1(A) <=> ! [C,D] : ( A = k4_tarski(C,D) => B = C ) ) ) ), file(mcart_1,d1_mcart_1), [interesting(0.00)]). fof(t22_amistd_1,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m2_subset_1(B,k2_zfmisc_1(u3_ami_1(A,k4_amistd_1(A)),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(k4_amistd_1(A))))),u4_ami_1(A,k4_amistd_1(A))) => ( k1_ami_5(A,k4_amistd_1(A),B) = 1 | k1_ami_5(A,k4_amistd_1(A),B) = 0 ) ) ) ), inference(mizar_proof,[status(thm)],[d11_amistd_1,d2_tarski,d1_mcart_1,d1_ami_5]), [file(amistd_1,t22_amistd_1),interesting(0.00)]). fof(t32_zfmisc_1,theorem,( ! [A,B] : k3_tarski(k2_tarski(k1_tarski(A),k1_tarski(B))) = k2_tarski(A,B) ), file(zfmisc_1,t32_zfmisc_1), [interesting(0.00)]). fof(d16_amistd_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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( v5_amistd_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => k1_funct_1(k4_ami_1(A,B,C,D),k2_ami_1(A,B)) = k9_amistd_1(A,B,k6_ami_1(A,B,D)) ) ) ) ) ) ), file(amistd_1,d16_amistd_1), [interesting(0.00)]). fof(t41_amistd_1,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) & v10_ami_1(B,A) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_struct_0(C,B,u2_ami_1(A,B)) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ( v5_amistd_1(D,A,B) => k1_amistd_1(A,B,C,D) = k1_struct_0(B,k9_amistd_1(A,B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_amistd_1,d11_ami_1,d14_ami_1,t65_funct_4,d2_tarski,t48_ami_1,t14_funct_4,t66_funct_4,d2_tarski,t14_funct_4,t66_funct_4,d1_tarski,t2_tarski]), [file(amistd_1,t41_amistd_1),interesting(0.00)]). fof(t6_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),k1_tarski(B)) => A = B ) ), file(zfmisc_1,t6_zfmisc_1), [interesting(0.00)]). fof(t42_amistd_1,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) & v10_ami_1(B,A) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m2_subset_1(C,k2_zfmisc_1(u3_ami_1(A,B),k13_finseq_1(k2_xboole_0(k3_tarski(A),u1_struct_0(B)))),u4_ami_1(A,B)) => ~ ( v5_amistd_1(C,A,B) & v3_ami_1(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_amistd_1,t35_amistd_1,t6_zfmisc_1,t15_amistd_1]), [file(amistd_1,t42_amistd_1),interesting(0.00)]). fof(d18_amistd_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) => ( v7_amistd_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => ( ( r1_tarski(C,D) & r2_hidden(k6_ami_1(A,B,D),k1_relat_1(C)) ) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => r2_hidden(k6_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,D),E)),k1_relat_1(C)) ) ) ) ) ) ) ) ), file(amistd_1,d18_amistd_1), [interesting(0.00)]). fof(d19_amistd_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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ( v8_amistd_1(C,A,B) <=> ! [D] : ( m1_subset_1(D,k4_card_3(u5_ami_1(A,B))) => ( ( r1_tarski(C,D) & k6_ami_1(A,B,D) = k5_amistd_1(A,B,0) ) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => r2_hidden(k6_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,D),E)),k1_relat_1(C)) ) ) ) ) ) ) ) ), file(amistd_1,d19_amistd_1), [interesting(0.00)]). fof(t44_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( m1_ami_1(C,A,B) => ( ( v7_amistd_1(C,A,B) & r2_hidden(k5_amistd_1(A,B,0),k1_relat_1(C)) ) => v8_amistd_1(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d18_amistd_1,d19_amistd_1]), [file(amistd_1,t44_amistd_1),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(d17_amistd_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) => ( v6_amistd_1(C,A,B) <=> ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( r2_hidden(D,k1_relat_1(C)) => r1_tarski(k1_amistd_1(A,B,D,k5_ami_5(A,B,C,D)),k1_relat_1(C)) ) ) ) ) ) ) ), file(amistd_1,d17_amistd_1), [interesting(0.00)]). fof(d5_ami_5,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)) => ( r2_hidden(D,k1_relat_1(C)) => k5_ami_5(A,B,C,D) = k1_funct_1(C,D) ) ) ) ) ) ), file(ami_5,d5_ami_5), [interesting(0.00)]). fof(t54_ami_1,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] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k13_ami_1(A,B,C,D) = k13_ami_1(A,B,k11_ami_1(A,B,k10_ami_1(A,B,C),E),D) ) ) ) ) ) ), file(ami_1,t54_ami_1), [interesting(0.00)]). fof(t49_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => r2_hidden(k5_amistd_1(A,B,0),k1_relat_1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xboole_0,d13_ami_3,d12_amistd_1,d4_funct_2,d3_funct_2,d5_funct_1,d1_funct_2,t18_nat_1,d20_amistd_1]), [file(amistd_1,t49_amistd_1),interesting(0.00)]). fof(t4_amistd_1,theorem,( $true ), file(amistd_1,t4_amistd_1), [interesting(0.00)]). fof(t2_membered,theorem,( ! [A] : ( v2_membered(A) => r1_tarski(A,k1_numbers) ) ), file(membered,t2_membered), [interesting(0.00)]). fof(t38_integra2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_finset_1(A) & m1_subset_1(A,k1_zfmisc_1(k1_numbers)) ) => ! [B] : ( ( ~ v1_xboole_0(B) & v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(k1_numbers)) ) => ( r1_tarski(A,B) => r1_xreal_0(k1_pre_circ(A),k1_pre_circ(B)) ) ) ) ), file(integra2,t38_integra2), [interesting(0.00)]). fof(t52_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( ( ~ v1_xboole_0(D) & v1_ami_3(D,A,B) & m1_ami_1(D,A,B) ) => ( r1_tarski(C,D) => r1_amistd_1(A,B,k10_amistd_1(A,B,C),k10_amistd_1(A,B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d21_amistd_1,d21_amistd_1,t2_membered,d3_tarski,t8_grfunc_1,t38_integra2,t28_amistd_1]), [file(amistd_1,t52_amistd_1),interesting(0.00)]). fof(t9_grfunc_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & r1_tarski(A,B) ) => A = B ) ) ) ), file(grfunc_1,t9_grfunc_1), [interesting(0.00)]). fof(t54_amistd_1,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) & v4_amistd_1(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( ( ~ v1_xboole_0(D) & v1_ami_3(D,A,B) & m1_ami_1(D,A,B) ) => ( ( r1_tarski(C,D) & k10_amistd_1(A,B,C) = k10_amistd_1(A,B,D) ) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_grfunc_1,d10_xboole_0,d3_tarski,d13_ami_3,t53_amistd_1,t51_amistd_1,d20_amistd_1,t9_grfunc_1]), [file(amistd_1,t54_amistd_1),interesting(0.00)]).