fof(t9_amistd_2,theorem,( ! [A] : ( ( v1_fraenkel(A) & v1_pralg_2(A) ) => r1_tarski(A,k4_card_3(k1_amistd_2(A))) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d2_pralg_2,t7_amistd_2,d1_amistd_2,d6_card_3,t18_card_3]), [file(amistd_2,t9_amistd_2),interesting(1.00)]). fof(t10_amistd_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_amistd_2(A) ) => A = k4_card_3(k1_amistd_2(A)) ) ), inference(mizar_proof,[status(thm)],[t9_amistd_2,d10_xboole_0,d3_tarski,d5_card_3,d2_amistd_2,t7_amistd_2,d2_pralg_2,t18_card_3,d1_amistd_2,d6_card_3,t18_card_3,t18_card_3]), [file(amistd_2,t10_amistd_2),interesting(0.97)]). fof(t7_amistd_2,theorem,( ! [A] : ( ( v1_fraenkel(A) & v1_pralg_2(A) ) => k1_relat_1(k1_amistd_2(A)) = k1_pralg_2(A) ) ), inference(mizar_proof,[status(thm)],[d1_amistd_2,t60_relat_1,d2_pralg_2,d1_amistd_2,d2_pralg_2,d3_tarski,d10_xboole_0,d3_tarski,d2_pralg_2,d1_amistd_2]), [file(amistd_2,t7_amistd_2),interesting(0.92)]). fof(t11_amistd_2,theorem,( ! [A,B,C] : ( l1_ami_1(C,B) => ! [D] : ( m1_ami_1(D,B,C) => m1_ami_1(k4_xboole_0(D,A),B,C) ) ) ), inference(mizar_proof,[status(thm)],[t36_xboole_1,t40_ami_1,d24_ami_1]), [file(amistd_2,t11_amistd_2),interesting(0.89)]). fof(l1_amistd_2,theorem,( ! [A] : ( v1_relat_1(A) => ~ ( k1_relat_1(A) != k1_xboole_0 & A = k1_xboole_0 ) ) ), inference(mizar_proof,[status(thm)],[t60_relat_1]), [file(amistd_2,l1_amistd_2),interesting(0.86)]). fof(t1_amistd_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_tarski(k1_relat_1(A),k1_relat_1(B)) <=> r2_tarski(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_pre_circ,t21_card_1,t21_card_1,t21_card_1,t21_card_1]), [file(amistd_2,t1_amistd_2),interesting(0.83)]). fof(t4_amistd_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_finset_1(A) ) => k6_xcmplx_0(k4_card_1(A),1) = k5_binarith(k4_card_1(A),1) ) ), inference(mizar_proof,[status(thm)],[t59_card_2,t39_nat_1,t50_xreal_1,d3_binarith]), [file(amistd_2,t4_amistd_2),interesting(0.80)]). fof(t3_amistd_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k4_xboole_0(k1_relat_1(B),k1_relat_1(C))) => k1_funct_1(k4_xboole_0(B,C),A) = k1_funct_1(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_relat_1,t36_xboole_1,t8_grfunc_1]), [file(amistd_2,t3_amistd_2),interesting(0.78)]). fof(t5_amistd_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_fraenkel(A) ) => k1_relat_1(k1_amistd_2(A)) = k1_setfam_1(a_1_0_amistd_2(A)) ) ), inference(mizar_proof,[status(thm)],[d1_amistd_2,d1_setfam_1,d3_tarski,d10_xboole_0,d3_tarski,d1_setfam_1,d1_amistd_2]), [file(amistd_2,t5_amistd_2),interesting(0.78)]). fof(t43_amistd_2,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) & m1_ami_1(D,B,C) ) => r2_tarski(k1_relat_1(D),k1_relat_1(k10_amistd_2(B,C,D,A))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_ami_3,s1_zfrefle1,d4_wellord2,t25_amistd_1,t27_amistd_1,d8_funct_1,d16_amistd_2,d5_funct_1,t26_amistd_1,d21_ordinal2,d13_amistd_1,d3_tarski,d10_xboole_0,d3_tarski,d13_amistd_1,d5_funct_1]), [file(amistd_2,t43_amistd_2),interesting(0.74)]). fof(t54_amistd_2,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) & v8_amistd_2(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) & v9_amistd_1(D,A,B) & m1_ami_1(D,A,B) ) => r1_tarski(k11_amistd_2(A,B,C),k11_amistd_2(A,B,k12_amistd_2(A,B,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_4,t15_amistd_2,t49_amistd_2,t52_amistd_2,t49_amistd_2,t59_card_2,t39_nat_1,t11_xreal_1,t8_xreal_1,t2_xreal_1,d3_tarski,t50_amistd_1,d16_amistd_2,t49_amistd_2,t4_amistd_2,t25_amistd_1,t29_nat_1,d2_xboole_0,t55_amistd_1,t25_amistd_1,t4_amistd_2,t49_amistd_2,d1_tarski,t5_cqc_lang,d4_xboole_0,t3_amistd_2,t12_funct_4,t8_grfunc_1]), [file(amistd_2,t54_amistd_2),interesting(0.74)]). fof(t38_amistd_2,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) & v8_amistd_2(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => k9_amistd_2(A,B,C,0) = C ) ) ) ), inference(mizar_proof,[status(thm)],[d5_ami_5,t28_amistd_2,d15_amistd_2]), [file(amistd_2,t38_amistd_2),interesting(0.73)]). fof(t6_amistd_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v1_fraenkel(A) ) => ! [B] : ( r2_hidden(B,k1_relat_1(k1_amistd_2(A))) => k1_funct_1(k1_amistd_2(A),B) = a_2_0_amistd_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d1_amistd_2,d6_card_3,d3_tarski,d10_xboole_0,d3_tarski,d6_card_3,d1_amistd_2]), [file(amistd_2,t6_amistd_2),interesting(0.71)]). fof(t40_amistd_2,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_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => k10_amistd_2(A,B,C,0) = C ) ) ) ), inference(mizar_proof,[status(thm)],[d13_ami_3,t26_amistd_1,d21_ordinal2,d3_tarski,d10_xboole_0,d3_tarski,d16_amistd_2]), [file(amistd_2,t40_amistd_2),interesting(0.70)]). fof(t19_amistd_2,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( m1_subset_1(B,u3_ami_1(A,k4_amistd_1(A))) => k5_amistd_2(A,k4_amistd_1(A),B) = k6_domain_1(k5_numbers,0) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d11_amistd_1,d11_amistd_1,d2_tarski,t17_amistd_2,d1_ami_5,d1_mcart_1,d2_tarski,t17_amistd_2,d1_ami_5,d1_mcart_1,d2_tarski,d3_tarski,d10_xboole_0,d3_tarski,t17_amistd_2,d1_tarski]), [file(amistd_2,t19_amistd_2),interesting(0.69)]). fof(t8_amistd_2,theorem,( ! [A] : ( v1_fraenkel(A) => ! [B] : ( r2_hidden(B,k1_relat_1(k1_amistd_2(A))) => k1_funct_1(k1_amistd_2(A),B) = k5_card_3(B,A) ) ) ), inference(mizar_proof,[status(thm)],[d1_amistd_2,d1_amistd_2]), [file(amistd_2,t8_amistd_2),interesting(0.69)]). fof(t15_amistd_2,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_ami_3(C,A,B) & v9_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => k1_relat_1(C) = a_3_0_amistd_2(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_ami_3,t14_amistd_2,d13_amistd_1,d3_tarski,d10_xboole_0,d3_tarski,t50_amistd_1]), [file(amistd_2,t15_amistd_2),interesting(0.67)]). fof(t25_amistd_2,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) ) => k4_card_1(k6_amistd_2(A,B)) = 1 ) ) ), inference(mizar_proof,[status(thm)],[t19_ami_1,t79_card_1]), [file(amistd_2,t25_amistd_2),interesting(0.66)]). fof(l45_amistd_2,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) ) => k5_binarith(k4_card_1(k6_amistd_2(A,B)),1) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t4_amistd_2,t25_amistd_2]), [file(amistd_2,l45_amistd_2),interesting(0.66)]). fof(l74_amistd_2,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) ) => r1_tarski(k11_amistd_2(A,B,C),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t36_xboole_1]), [file(amistd_2,l74_amistd_2),interesting(0.65)]). fof(t59_amistd_2,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) & v6_amistd_2(B,A) & v8_amistd_2(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & v10_amistd_1(C,A,B) & v11_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => k12_amistd_2(A,B,C,k7_amistd_2(A,B)) = C ) ) ) ), inference(mizar_proof,[status(thm)],[t57_amistd_2,t48_amistd_2,t58_amistd_2,t5_cqc_lang,t55_amistd_1,d1_funct_4,t50_amistd_2,d7_xboole_0,l74_amistd_2,d3_xboole_0,t12_funct_4,t8_grfunc_1,d1_tarski,t55_amistd_1,l41_amistd_2,d16_amistd_2,t14_funct_4,d16_amistd_2,l42_amistd_2,d22_amistd_1,d2_xboole_0,t9_funct_1]), [file(amistd_2,t59_amistd_2),interesting(0.65)]). fof(t12_amistd_2,theorem,( ! [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) & l1_ami_1(C,B) ) => ! [D] : ( ( v1_ami_3(D,B,C) & m1_ami_1(D,B,C) ) => ( v1_ami_3(k4_xboole_0(D,A),B,C) & m1_ami_1(k4_xboole_0(D,A),B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_amistd_2,t36_xboole_1,t8_grfunc_1,d13_ami_3,t1_xboole_1,d13_ami_3]), [file(amistd_2,t12_amistd_2),interesting(0.63)]). fof(t53_amistd_2,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) & v8_amistd_2(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) & v9_amistd_1(D,A,B) & m1_ami_1(D,A,B) ) => r1_tarski(k1_relat_1(C),k1_relat_1(k12_amistd_2(A,B,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l81_amistd_2,t48_amistd_2,d3_tarski,d2_xboole_0,d1_tarski,d1_tarski,t55_amistd_1,d13_amistd_1,t4_amistd_2,t52_amistd_2,t59_card_2,t8_xreal_1,t50_amistd_1,d13_amistd_1,d2_xboole_0]), [file(amistd_2,t53_amistd_2),interesting(0.59)]). fof(t60_amistd_2,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) & v8_amistd_2(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & v10_amistd_1(C,A,B) & v11_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => k12_amistd_2(A,B,k7_amistd_2(A,B),C) = C ) ) ) ), inference(mizar_proof,[status(thm)],[l45_amistd_2,t38_amistd_2,t40_amistd_2,t21_funct_4]), [file(amistd_2,t60_amistd_2),interesting(0.59)]). fof(t47_amistd_2,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) ) => k1_relat_1(k11_amistd_2(A,B,C)) = k4_xboole_0(k1_relat_1(C),k1_struct_0(B,k10_amistd_1(A,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t4_relat_1,t19_ami_1,t5_cqc_lang,d3_tarski,d4_relat_1,d4_xboole_0,d4_relat_1,d1_tarski,d4_xboole_0,d1_tarski,t8_funct_1,d4_xboole_0,d1_tarski,d10_xboole_0,t15_relat_1]), [file(amistd_2,t47_amistd_2),interesting(0.58)]). fof(t61_amistd_2,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) & v10_ami_1(B,A) & v4_amistd_1(B,A) & v6_amistd_2(B,A) & v8_amistd_2(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & v10_amistd_1(C,A,B) & v11_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( ( ~ v1_xboole_0(D) & v1_ami_3(D,A,B) & v9_amistd_1(D,A,B) & v10_amistd_1(D,A,B) & v11_amistd_1(D,A,B) & m1_ami_1(D,A,B) ) => ! [E] : ( ( ~ v1_xboole_0(E) & v1_ami_3(E,A,B) & v9_amistd_1(E,A,B) & v10_amistd_1(E,A,B) & v11_amistd_1(E,A,B) & m1_ami_1(E,A,B) ) => k13_amistd_2(A,B,k13_amistd_2(A,B,C,D),E) = k13_amistd_2(A,B,C,k13_amistd_2(A,B,D,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_amistd_2,t60_amistd_2,t59_amistd_2,t60_amistd_2,t52_amistd_2,t52_amistd_2,t52_amistd_2,t52_amistd_2,t15_amistd_2,t15_amistd_2,d16_amistd_2,d16_amistd_2,d16_amistd_2,t4_amistd_2,t52_amistd_2,t4_amistd_2,t4_amistd_2,d16_amistd_2,l74_amistd_2,t4_amistd_2,t4_amistd_2,t26_amistd_2,t59_card_2,t38_nat_1,t2_cqc_the1,t2_xreal_1,t54_amistd_2,t25_amistd_1,t4_amistd_2,t4_amistd_2,t4_amistd_2,t29_nat_1,t25_amistd_1,t4_amistd_2,t29_nat_1,t49_amistd_2,t50_amistd_1,t12_funct_4,t8_grfunc_1,t12_funct_4,t25_amistd_1,t4_amistd_2,t23_nat_1,t4_amistd_2,t26_amistd_2,t49_amistd_1,t49_amistd_1,t49_amistd_1,t49_amistd_1,t4_amistd_2,t4_amistd_2,t49_amistd_1,d2_xboole_0,l81_amistd_2,t5_cqc_lang,t55_amistd_1,d1_tarski,t25_amistd_1,t4_amistd_2,t26_amistd_2,d4_xboole_0,t59_card_2,t26_amistd_2,t39_nat_1,d5_real_1,t11_xreal_1,t4_amistd_2,t41_amistd_2,t49_amistd_2,t51_card_1,t49_amistd_1,t78_card_1,d5_ami_5,t8_grfunc_1,t12_funct_4,d5_ami_5,t12_funct_4,t3_amistd_2,t14_funct_4,d16_amistd_2,d15_amistd_2,d15_amistd_2,d16_amistd_2,t14_funct_4,t25_amistd_1,t8_xreal_1,l14_amistd_2,t52_binarith,t2_xreal_1,t53_binarith,t11_xreal_1,t92_real_1,t92_real_1,t4_amistd_2,t31_xreal_1,t2_xreal_1,t2_xreal_1,t9_xreal_1,t4_amistd_2,d3_binarith,t49_amistd_2,t50_amistd_1,d2_xboole_0,l81_amistd_2,d15_amistd_2,t92_real_1,t2_xreal_1,t52_amistd_2,t50_amistd_1,t5_cqc_lang,d1_tarski,t55_amistd_1,t25_amistd_1,t4_amistd_2,d4_xboole_0,t8_grfunc_1,d15_amistd_2,t25_amistd_1,d3_binarith,t4_amistd_2,t4_amistd_2,t11_xreal_1,l14_amistd_2,d5_ami_5,t12_funct_4,t8_grfunc_1,t12_funct_4,t3_amistd_2,t14_funct_4,d16_amistd_2,d15_amistd_2,d5_ami_5,d15_amistd_2,d16_amistd_2,t14_funct_4,t53_binarith,d3_binarith,t49_amistd_1,t59_card_2,t8_xreal_1,t4_amistd_2,t52_amistd_2,t50_amistd_1,d15_amistd_2,t49_amistd_1,d5_ami_5,t49_amistd_1,d5_ami_5,d15_amistd_2,t55_amistd_1,t55_amistd_2,d5_ami_5,t37_amistd_2,t14_funct_4,d16_amistd_2,d15_amistd_2,d15_amistd_2,d16_amistd_2,t14_funct_4,t53_binarith,t50_xreal_1,t23_xreal_1,d3_binarith,t50_amistd_1,d15_amistd_2,t29_nat_1,t2_xreal_1,t53_binarith,t50_xreal_1,t11_xreal_1,d3_binarith,d3_binarith,t52_amistd_2,t50_amistd_1,d15_amistd_2,d15_amistd_2,t11_xreal_1,t50_binarith,t50_binarith,t53_binarith,t11_xreal_1,t50_binarith,t50_amistd_1,d15_amistd_2,t50_binarith,t50_binarith,t50_binarith,d5_ami_5,t14_funct_4,d16_amistd_2,d15_amistd_2,t14_funct_4,d16_amistd_2,d15_amistd_2,t37_amistd_2,d15_amistd_2,d16_amistd_2,t14_funct_4,l15_amistd_2,t9_funct_1]), [file(amistd_2,t61_amistd_2),interesting(0.58)]). fof(t46_amistd_2,theorem,( ! [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) => v12_amistd_2(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_ami_1,d19_amistd_2]), [file(amistd_2,t46_amistd_2),interesting(0.53)]). fof(t27_amistd_2,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) ) => k10_amistd_1(A,B,k6_amistd_2(A,B)) = k5_amistd_1(A,B,0) ) ) ), inference(mizar_proof,[status(thm)],[l45_amistd_2,t55_amistd_1]), [file(amistd_2,t27_amistd_2),interesting(0.52)]). fof(l42_amistd_2,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(k6_amistd_2(A,B),k5_amistd_1(A,B,0)) = k5_ami_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t6_cqc_lang]), [file(amistd_2,l42_amistd_2),interesting(0.52)]). fof(t44_amistd_2,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) & v6_amistd_2(B,A) & v8_amistd_2(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) => v10_amistd_2(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d17_amistd_2,t24_amistd_2,t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,d16_amistd_1,d13_amistd_1,d16_amistd_1,d13_amistd_1,t29_amistd_2]), [file(amistd_2,t44_amistd_2),interesting(0.45)]). fof(t29_amistd_2,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) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ( v9_amistd_2(D,B,C) => k8_amistd_2(B,C,D,A) = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,t9_funct_1,t16_amistd_2]), [file(amistd_2,t29_amistd_2),interesting(0.44)]). fof(t52_amistd_2,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) & v8_amistd_2(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) ) => ( k4_card_1(k12_amistd_2(A,B,C,D)) = k6_xcmplx_0(k1_nat_1(k4_card_1(C),k4_card_1(D)),1) & k4_card_1(k12_amistd_2(A,B,C,D)) = k5_binarith(k1_nat_1(k4_card_1(C),k4_card_1(D)),1) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_amistd_2,t1_amistd_2,t50_amistd_2,t2_amistd_2,t21_card_1,t21_pre_circ,d15_amistd_2,t21_pre_circ,t49_amistd_2,d3_binarith]), [file(amistd_2,t52_amistd_2),interesting(0.44)]). fof(t45_amistd_2,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) & v6_amistd_2(B,A) & v8_amistd_2(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) => v10_amistd_2(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d17_amistd_2,t23_amistd_2,t5_cqc_lang,d1_tarski,d8_ami_1,t6_cqc_lang,t14_funct_4,d8_ami_1,t29_amistd_2]), [file(amistd_2,t45_amistd_2),interesting(0.40)]). fof(t50_amistd_2,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) & v8_amistd_2(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_xboole_0(k1_relat_1(k11_amistd_2(A,B,C)),k1_relat_1(k10_amistd_2(A,B,k9_amistd_2(A,B,D,k5_binarith(k4_card_1(C),1)),k5_binarith(k4_card_1(C),1)))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_xboole_0,d3_xboole_0,d3_xboole_0,d16_amistd_2,l1_amistd_2,t53_amistd_1,t55_amistd_1,t28_amistd_1,t49_amistd_2,t4_amistd_2,d3_binarith,t11_xreal_1,l14_amistd_2,d3_binarith,t23_nat_1,t59_card_2]), [file(amistd_2,t50_amistd_2),interesting(0.40)]). fof(t31_amistd_2,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) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => k5_amistd_2(B,C,k1_ami_5(B,C,D)) = k5_amistd_2(B,C,k1_ami_5(B,C,k8_amistd_2(B,C,D,A))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_amistd_2,d3_tarski,d10_xboole_0,d3_tarski,d14_amistd_2]), [file(amistd_2,t31_amistd_2),interesting(0.39)]). fof(t37_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v1_setfam_1(C) => ! [D] : ( ( ~ v3_struct_0(D) & ~ v2_ami_1(D,C) & v5_ami_1(D,C) & v8_ami_1(D,C) & v4_amistd_1(D,C) & v8_amistd_2(D,C) & l1_ami_1(D,C) ) => ! [E] : ( m2_subset_1(E,k2_zfmisc_1(u3_ami_1(C,D),k13_finseq_1(k2_xboole_0(k3_tarski(C),u1_struct_0(D)))),u4_ami_1(C,D)) => k8_amistd_2(C,D,k8_amistd_2(C,D,E,A),B) = k8_amistd_2(C,D,E,k2_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,t31_amistd_2,d14_amistd_2,d14_amistd_2,d13_amistd_1,d14_amistd_2,d14_amistd_2,d14_amistd_2,d14_amistd_2,t9_funct_1,t16_amistd_2]), [file(amistd_2,t37_amistd_2),interesting(0.38)]). fof(t36_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v4_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v10_ami_1(C,B) & v4_amistd_1(C,B) & v6_amistd_2(C,B) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ( v5_amistd_1(D,B,C) => v5_amistd_1(k8_amistd_2(B,C,D,A),B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_amistd_2,t29_amistd_2]), [file(amistd_2,t36_amistd_2),interesting(0.23)]). fof(t51_amistd_2,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) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & v11_amistd_1(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(k11_amistd_2(A,B,C))) & k1_funct_1(k11_amistd_2(A,B,C),D) = k5_ami_1(A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l74_amistd_2,t8_grfunc_1,t8_grfunc_1,d23_amistd_1,t47_amistd_2,d4_xboole_0,d1_tarski]), [file(amistd_2,t51_amistd_2),interesting(0.22)]). fof(t22_amistd_2,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) & v5_amistd_2(B,A) & v7_amistd_2(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_2(C,A,B) => v1_xboole_0(k2_amistd_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_amistd_2,d1_xboole_0,d6_amistd_2]), [file(amistd_2,t22_amistd_2),interesting(0.20)]). fof(t35_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v4_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v10_ami_1(C,B) & v4_amistd_1(C,B) & v6_amistd_2(C,B) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ( k8_amistd_2(B,C,D,A) = k5_ami_1(B,C) => D = k5_ami_1(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_amistd_2,t34_amistd_2]), [file(amistd_2,t35_amistd_2),interesting(0.20)]). fof(t56_amistd_2,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) & v8_amistd_2(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) & v9_amistd_1(D,A,B) & m1_ami_1(D,A,B) ) => ! [E] : ( m1_struct_0(E,B,u2_ami_1(A,B)) => ( ~ r1_xreal_0(k6_xcmplx_0(k4_card_1(C),1),k7_amistd_1(A,B,E)) => k1_funct_1(k9_amistd_2(A,B,C,k5_binarith(k4_card_1(C),1)),E) = k1_funct_1(k9_amistd_2(A,B,k12_amistd_2(A,B,C,D),k5_binarith(k4_card_1(C),1)),E) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t49_amistd_2,t50_amistd_1,d13_amistd_1,l74_amistd_2,t8_grfunc_1,l74_amistd_2,t54_amistd_2,t1_xboole_1,t8_grfunc_1,d5_ami_5,t50_amistd_2,d7_xboole_0,d3_xboole_0,t12_funct_4,t8_grfunc_1,d15_amistd_2,d5_ami_5,d15_amistd_2]), [file(amistd_2,t56_amistd_2),interesting(0.12)]). fof(t18_amistd_2,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)) => ( ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => k1_amistd_1(A,B,D,C) = k1_struct_0(B,k9_amistd_1(A,B,D)) ) => 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,t36_amistd_1]), [file(amistd_2,t18_amistd_2),interesting(0.11)]). fof(t20_amistd_2,theorem,( ! [A] : ( v1_setfam_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & ~ v2_ami_1(B,A) & v2_amistd_2(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] : ( ( r2_hidden(D,k4_finseq_1(k4_amistd_2(A,B,C))) & k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),D) = u2_ami_1(A,B) ) => m1_struct_0(k1_funct_1(k4_amistd_2(A,B,C),D),B,u2_ami_1(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_amistd_2,d1_amistd_2,d1_amistd_2,d6_card_3]), [file(amistd_2,t20_amistd_2),interesting(0.08)]). 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(d2_pralg_2,definition,( ! [A] : ( ( v1_fraenkel(A) & v1_pralg_2(A) ) => ! [B] : ( ( A != k1_xboole_0 => ( B = k1_pralg_2(A) <=> ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(C,A) => B = k1_relat_1(C) ) ) ) ) & ( A = k1_xboole_0 => ( B = k1_pralg_2(A) <=> B = k1_xboole_0 ) ) ) ) ), file(pralg_2,d2_pralg_2), [interesting(0.00)]). fof(d1_amistd_2,definition,( ! [A] : ( v1_fraenkel(A) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( ~ v1_xboole_0(A) => ( B = k1_amistd_2(A) <=> ( ! [C] : ( r2_hidden(C,k1_relat_1(B)) <=> ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) ) => ( r2_hidden(D,A) => r2_hidden(C,k1_relat_1(D)) ) ) ) & ! [C] : ( r2_hidden(C,k1_relat_1(B)) => k1_funct_1(B,C) = k5_card_3(C,A) ) ) ) ) & ( v1_xboole_0(A) => ( B = k1_amistd_2(A) <=> B = k1_xboole_0 ) ) ) ) ) ), file(amistd_2,d1_amistd_2), [interesting(0.00)]). fof(t60_relat_1,theorem, ( k1_relat_1(k1_xboole_0) = k1_xboole_0 & k2_relat_1(k1_xboole_0) = k1_xboole_0 ), file(relat_1,t60_relat_1), [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(d6_card_3,definition,( ! [A,B,C] : ( C = k5_card_3(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E] : ( v1_relat_1(E) & v1_funct_1(E) & r2_hidden(E,B) & D = k1_funct_1(E,A) ) ) ) ), file(card_3,d6_card_3), [interesting(0.00)]). fof(t18_card_3,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k4_card_3(B)) <=> ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(B)) => r2_hidden(k1_funct_1(A,C),k1_funct_1(B,C)) ) ) ) ) ) ), file(card_3,t18_card_3), [interesting(0.00)]). fof(d5_card_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k4_card_3(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( v1_relat_1(D) & v1_funct_1(D) & C = D & k1_relat_1(D) = k1_relat_1(A) & ! [E] : ( r2_hidden(E,k1_relat_1(A)) => r2_hidden(k1_funct_1(D,E),k1_funct_1(A,E)) ) ) ) ) ) ), file(card_3,d5_card_3), [interesting(0.00)]). fof(d2_amistd_2,definition,( ! [A] : ( v1_amistd_2(A) <=> ? [B] : ( v1_relat_1(B) & v1_funct_1(B) & A = k4_card_3(B) ) ) ), file(amistd_2,d2_amistd_2), [interesting(0.00)]). fof(t36_xboole_1,theorem,( ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ), file(xboole_1,t36_xboole_1), [interesting(0.00)]). fof(t40_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) ) => ( ( r1_tarski(A,B) & r2_hidden(B,k7_ami_1(C)) ) => r2_hidden(A,k7_ami_1(C)) ) ) ) ) ), file(ami_1,t40_ami_1), [interesting(0.00)]). fof(d24_ami_1,definition,( ! [A,B] : ( l1_ami_1(B,A) => ! [C] : ( m1_subset_1(C,k7_ami_1(u5_ami_1(A,B))) => ( m1_ami_1(C,A,B) <=> v1_finset_1(C) ) ) ) ), file(ami_1,d24_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(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(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(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(t13_amistd_2,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_ami_3(C,A,B) & v9_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( ( v1_ami_3(D,A,B) & m1_ami_1(D,A,B) ) => ( k1_relat_1(C) = k1_relat_1(D) => v9_amistd_1(D,A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_amistd_1,d20_amistd_1]), [file(amistd_2,t13_amistd_2),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_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [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(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [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 ) ) ) ) ) ), file(amistd_1,t36_amistd_1), [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(d2_mcart_1,definition,( ! [A] : ( ? [B,C] : A = k4_tarski(B,C) => ! [B] : ( B = k2_mcart_1(A) <=> ! [C,D] : ( A = k4_tarski(C,D) => B = D ) ) ) ), file(mcart_1,d2_mcart_1), [interesting(0.00)]). fof(t17_amistd_2,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))) => k4_amistd_2(A,k4_amistd_1(A),B) = 0 ) ) ), inference(mizar_proof,[status(thm)],[d11_amistd_1,d2_tarski,d2_mcart_1]), [file(amistd_2,t17_amistd_2),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(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(d4_amistd_2,definition,( ! [A,B] : ( l1_ami_1(B,A) => ( v2_amistd_2(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] : ( 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)) => ( k1_ami_5(A,B,C) = k1_ami_5(A,B,D) => k4_finseq_1(k4_amistd_2(A,B,C)) = k4_finseq_1(k4_amistd_2(A,B,D)) ) ) ) ) ) ), file(amistd_2,d4_amistd_2), [interesting(0.00)]). fof(d12_amistd_2,definition,( ! [A,B] : ( 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_2(C,A,B) <=> ! [D] : ~ ( r2_hidden(D,k4_finseq_1(k4_amistd_2(A,B,C))) & k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),D) = u2_ami_1(A,B) ) ) ) ) ), file(amistd_2,d12_amistd_2), [interesting(0.00)]). fof(d6_amistd_2,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] : ( 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_amistd_2(C,A,B) <=> ! [D] : ~ ( r2_hidden(D,k2_amistd_1(A,B,C)) & ! [E] : ~ ( r2_hidden(E,k4_finseq_1(k4_amistd_2(A,B,C))) & D = k1_funct_1(k4_amistd_2(A,B,C),E) & k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),E) = u2_ami_1(A,B) ) ) ) ) ) ) ), file(amistd_2,d6_amistd_2), [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(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_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(t19_ami_1,theorem,( ! [A,B] : k3_cqc_lang(A,B) = k1_tarski(k4_tarski(A,B)) ), file(ami_1,t19_ami_1), [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(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)) ) ) ) ), file(amistd_1,t55_amistd_1), [interesting(0.00)]). fof(d14_amistd_2,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) & v8_amistd_2(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] : ( v4_ordinal2(D) => ! [E] : ( m2_subset_1(E,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 = k8_amistd_2(A,B,C,D) <=> ( k1_ami_5(A,B,E) = k1_ami_5(A,B,C) & k4_finseq_1(k4_amistd_2(A,B,E)) = k4_finseq_1(k4_amistd_2(A,B,C)) & ! [F] : ( r2_hidden(F,k4_finseq_1(k4_amistd_2(A,B,C))) => ( ~ ( k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),F) = u2_ami_1(A,B) & ! [G] : ( m1_struct_0(G,B,u2_ami_1(A,B)) => ~ ( G = k1_funct_1(k4_amistd_2(A,B,C),F) & k1_funct_1(k4_amistd_2(A,B,E),F) = k5_amistd_1(A,B,k2_xcmplx_0(D,k7_amistd_1(A,B,G))) ) ) ) & ( k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),F) != u2_ami_1(A,B) => k1_funct_1(k4_amistd_2(A,B,E),F) = k1_funct_1(k4_amistd_2(A,B,C),F) ) ) ) ) ) ) ) ) ) ) ), file(amistd_2,d14_amistd_2), [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(d2_zfmisc_1,definition,( ! [A,B,C] : ( C = k2_zfmisc_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k4_tarski(E,F) ) ) ) ), file(zfmisc_1,d2_zfmisc_1), [interesting(0.00)]). fof(t8_mcart_1,theorem,( ! [A] : ( ? [B,C] : A = k4_tarski(B,C) => k4_tarski(k1_mcart_1(A),k2_mcart_1(A)) = A ) ), file(mcart_1,t8_mcart_1), [interesting(0.00)]). fof(t16_amistd_2,theorem,( ! [A,B] : ( 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] : ( 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)) => ( ( k1_ami_5(A,B,C) = k1_ami_5(A,B,D) & k4_amistd_2(A,B,C) = k4_amistd_2(A,B,D) ) => C = D ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_zfmisc_1,t8_mcart_1,d1_ami_5]), [file(amistd_2,t16_amistd_2),interesting(0.00)]). fof(t30_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v4_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v10_ami_1(C,B) & v4_amistd_1(C,B) & v6_amistd_2(C,B) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => k8_amistd_2(B,C,k5_ami_1(B,C),A) = k5_ami_1(B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_amistd_2]), [file(amistd_2,t30_amistd_2),interesting(0.00)]). fof(t32_amistd_2,theorem,( ! [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) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ! [E] : ( m2_subset_1(E,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ( k1_funct_1(k1_amistd_2(k5_amistd_2(B,C,k1_ami_5(B,C,D))),A) = u2_ami_1(B,C) => ( ! [F] : ( v4_ordinal2(F) => k8_amistd_2(B,C,D,F) != k8_amistd_2(B,C,E,F) ) | k1_funct_1(k1_amistd_2(k5_amistd_2(B,C,k1_ami_5(B,C,E))),A) = u2_ami_1(B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_amistd_2,d14_amistd_2]), [file(amistd_2,t32_amistd_2),interesting(0.00)]). 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 ) ) ) ) ) ), file(amistd_1,t25_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 ) ) ) ) ) ), file(amistd_1,t27_amistd_1), [interesting(0.00)]). fof(t33_amistd_2,theorem,( ! [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) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => ! [D] : ( m2_subset_1(D,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ! [E] : ( m2_subset_1(E,k2_zfmisc_1(u3_ami_1(B,C),k13_finseq_1(k2_xboole_0(k3_tarski(B),u1_struct_0(C)))),u4_ami_1(B,C)) => ~ ( ? [F] : ( v4_ordinal2(F) & k8_amistd_2(B,C,D,F) = k8_amistd_2(B,C,E,F) ) & k1_funct_1(k1_amistd_2(k5_amistd_2(B,C,k1_ami_5(B,C,D))),A) != u2_ami_1(B,C) & k1_funct_1(k1_amistd_2(k5_amistd_2(B,C,k1_ami_5(B,C,E))),A) = u2_ami_1(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_amistd_2,t31_amistd_2]), [file(amistd_2,t33_amistd_2),interesting(0.00)]). fof(t34_amistd_2,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) & v8_amistd_2(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] : ( 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] : ( v4_ordinal2(E) & k8_amistd_2(A,B,C,E) = k8_amistd_2(A,B,D,E) ) => C = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_amistd_2,d14_amistd_2,d4_amistd_2,d14_amistd_2,t32_amistd_2,d14_amistd_2,t25_amistd_1,t27_amistd_1,t33_amistd_2,d14_amistd_2,d14_amistd_2,t9_funct_1,t16_amistd_2]), [file(amistd_2,t34_amistd_2),interesting(0.00)]). fof(d7_amistd_2,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] : ( 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)) => ( v4_amistd_2(C,A,B) <=> ! [D] : ( ? [E] : ( r2_hidden(E,k4_finseq_1(k4_amistd_2(A,B,C))) & D = k1_funct_1(k4_amistd_2(A,B,C),E) & k1_funct_1(k1_amistd_2(k5_amistd_2(A,B,k1_ami_5(A,B,C))),E) = u2_ami_1(A,B) ) => r2_hidden(D,k2_amistd_1(A,B,C)) ) ) ) ) ) ), file(amistd_2,d7_amistd_2), [interesting(0.00)]). 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) ) ) ) ) ), file(amistd_1,t43_amistd_1), [interesting(0.00)]). fof(t24_amistd_2,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) & v6_amistd_2(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) => v9_amistd_2(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_amistd_2,d7_amistd_2,t43_amistd_1]), [file(amistd_2,t24_amistd_2),interesting(0.00)]). fof(d15_amistd_2,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) & v8_amistd_2(B,A) & l1_ami_1(B,A) ) => ! [C] : ( ( v1_ami_3(C,A,B) & m1_ami_1(C,A,B) ) => ! [D] : ( v4_ordinal2(D) => ! [E] : ( m1_ami_1(E,A,B) => ( E = k9_amistd_2(A,B,C,D) <=> ( k1_relat_1(E) = k1_relat_1(C) & ! [F] : ( v4_ordinal2(F) => ( r2_hidden(k5_amistd_1(A,B,F),k1_relat_1(C)) => k1_funct_1(E,k5_amistd_1(A,B,F)) = k8_amistd_2(A,B,k5_ami_5(A,B,C,k5_amistd_1(A,B,F)),D) ) ) ) ) ) ) ) ) ) ), file(amistd_2,d15_amistd_2), [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(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(t39_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v1_setfam_1(C) => ! [D] : ( ( ~ v3_struct_0(D) & ~ v2_ami_1(D,C) & v5_ami_1(D,C) & v8_ami_1(D,C) & v4_amistd_1(D,C) & v8_amistd_2(D,C) & l1_ami_1(D,C) ) => ! [E] : ( ( v1_ami_3(E,C,D) & v9_amistd_1(E,C,D) & m1_ami_1(E,C,D) ) => k9_amistd_2(C,D,k9_amistd_2(C,D,E,A),B) = k9_amistd_2(C,D,E,k2_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_amistd_2,d15_amistd_2,d15_amistd_2,d13_ami_3,d13_amistd_1,d15_amistd_2,d15_amistd_2,d5_ami_5,d15_amistd_2,t37_amistd_2,d15_amistd_2,t9_funct_1]), [file(amistd_2,t39_amistd_2),interesting(0.00)]). fof(d16_amistd_2,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) => ! [D] : ( v4_ordinal2(D) => ! [E] : ( m1_ami_1(E,A,B) => ( E = k10_amistd_2(A,B,C,D) <=> ( k1_relat_1(E) = a_4_0_amistd_2(A,B,C,D) & ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( r2_hidden(k5_amistd_1(A,B,F),k1_relat_1(C)) => k1_funct_1(E,k5_amistd_1(A,B,k2_xcmplx_0(F,D))) = k1_funct_1(C,k5_amistd_1(A,B,F)) ) ) ) ) ) ) ) ) ) ), file(amistd_2,d16_amistd_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(t42_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v1_setfam_1(C) => ! [D] : ( ( ~ v3_struct_0(D) & ~ v2_ami_1(D,C) & v5_ami_1(D,C) & v8_ami_1(D,C) & v4_amistd_1(D,C) & l1_ami_1(D,C) ) => ! [E] : ( m1_ami_1(E,C,D) => k10_amistd_2(C,D,k10_amistd_2(C,D,E,A),B) = k10_amistd_2(C,D,E,k2_xcmplx_0(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_amistd_2,t25_amistd_1,d3_tarski,d10_xboole_0,d3_tarski,d21_ordinal2,d16_amistd_2,d21_ordinal2,d16_amistd_2,d16_amistd_2,d16_amistd_2]), [file(amistd_2,t42_amistd_2),interesting(0.00)]). fof(d17_amistd_2,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) & v8_amistd_2(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)) => ( v10_amistd_2(C,A,B) <=> ! [D] : ( v4_ordinal2(D) => ! [E] : ( m1_subset_1(E,k4_card_3(u5_ami_1(A,B))) => ! [F] : ( m1_subset_1(F,k4_card_3(u5_ami_1(A,B))) => ( F = k1_funct_4(E,k3_cqc_lang(k2_ami_1(A,B),k8_amistd_1(A,B,k6_ami_1(A,B,E),D))) => k8_amistd_1(A,B,k6_ami_1(A,B,k4_ami_1(A,B,C,E)),D) = k6_ami_1(A,B,k4_ami_1(A,B,k8_amistd_2(A,B,C,D),F)) ) ) ) ) ) ) ) ) ), file(amistd_2,d17_amistd_2), [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(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(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(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(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) ) ) ) ) ) ), file(amistd_1,t15_amistd_1), [interesting(0.00)]). 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)) ) ) ) ) ) ), file(amistd_1,t14_amistd_1), [interesting(0.00)]). fof(t21_amistd_2,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) & v7_amistd_2(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) => v1_xboole_0(k2_amistd_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_amistd_1,t14_amistd_1]), [file(amistd_2,t21_amistd_2),interesting(0.00)]). fof(t23_amistd_2,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) & v6_amistd_2(B,A) & v7_amistd_2(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) => v9_amistd_2(C,A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_amistd_2,d7_amistd_2,t21_amistd_2]), [file(amistd_2,t23_amistd_2),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(d19_amistd_2,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)) => ( v12_amistd_2(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_funct_7(D,E,u2_ami_1(A,B)) => r1_funct_7(k4_ami_1(A,B,C,D),k4_ami_1(A,B,C,E),u2_ami_1(A,B)) ) ) ) ) ) ) ) ), file(amistd_2,d19_amistd_2), [interesting(0.00)]). fof(d23_amistd_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) & 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) ) => ( v11_amistd_1(C,A,B) <=> ! [D] : ( m1_struct_0(D,B,u2_ami_1(A,B)) => ( ( k1_funct_1(C,D) = k5_ami_1(A,B) & r2_hidden(D,k1_relat_1(C)) ) => D = k10_amistd_1(A,B,C) ) ) ) ) ) ) ), file(amistd_1,d23_amistd_1), [interesting(0.00)]). fof(t4_relat_1,theorem,( ! [A,B] : v1_relat_1(k1_tarski(k4_tarski(A,B))) ), file(relat_1,t4_relat_1), [interesting(0.00)]). fof(d4_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( B = k1_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : r2_hidden(k4_tarski(C,D),A) ) ) ) ), file(relat_1,d4_relat_1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(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(t15_relat_1,theorem,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => r1_tarski(k4_xboole_0(k1_relat_1(A),k1_relat_1(B)),k1_relat_1(k4_xboole_0(A,B))) ) ) ), file(relat_1,t15_relat_1), [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(l81_amistd_2,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) & v8_amistd_2(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) ) => k1_relat_1(k12_amistd_2(A,B,C,D)) = k2_xboole_0(k1_relat_1(k11_amistd_2(A,B,C)),k1_relat_1(k10_amistd_2(A,B,k9_amistd_2(A,B,D,k5_binarith(k4_card_1(C),1)),k5_binarith(k4_card_1(C),1)))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_4]), [file(amistd_2,l81_amistd_2),interesting(0.00)]). 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)) ) ) ) ), file(amistd_1,t51_amistd_1), [interesting(0.00)]). fof(t37_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(k1_tarski(A),B) <=> r2_hidden(A,B) ) ), file(zfmisc_1,t37_zfmisc_1), [interesting(0.00)]). fof(t45_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => B = k2_xboole_0(A,k4_xboole_0(B,A)) ) ), file(xboole_1,t45_xboole_1), [interesting(0.00)]). fof(t48_amistd_2,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) ) => k1_relat_1(C) = k2_xboole_0(k1_relat_1(k11_amistd_2(A,B,C)),k1_struct_0(B,k10_amistd_1(A,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_amistd_1,t37_zfmisc_1,t47_amistd_2,t45_xboole_1]), [file(amistd_2,t48_amistd_2),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(s1_zfrefle1,theorem, ( ! [A] : ~ ( r2_hidden(A,f1_s1_zfrefle1) & ! [B] : ~ p1_s1_zfrefle1(A,B) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s1_zfrefle1 & ! [B] : ( r2_hidden(B,f1_s1_zfrefle1) => p1_s1_zfrefle1(B,k1_funct_1(A,B)) ) ) ), file(zfrefle1,s1_zfrefle1), [interesting(0.00)]). fof(d4_wellord2,definition,( ! [A,B] : ( r2_wellord2(A,B) <=> ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v2_funct_1(C) & k1_relat_1(C) = A & k2_relat_1(C) = B ) ) ), file(wellord2,d4_wellord2), [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(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(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) ) ) ) ) ), file(amistd_1,t26_amistd_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(t4_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ r2_hidden(C,k3_xboole_0(A,B)) ) & ~ ( ? [C] : r2_hidden(C,k3_xboole_0(A,B)) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t4_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(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)) ) ) ) ) ) ), file(amistd_1,t53_amistd_1), [interesting(0.00)]). 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) ) ) ) ) ) ), file(amistd_1,t28_amistd_1), [interesting(0.00)]). fof(d3_relat_1,definition,( ! [A] : ( v1_relat_1(A) => ! [B] : ( v1_relat_1(B) => ( r1_tarski(A,B) <=> ! [C,D] : ( r2_hidden(k4_tarski(C,D),A) => r2_hidden(k4_tarski(C,D),B) ) ) ) ) ), file(relat_1,d3_relat_1), [interesting(0.00)]). fof(d4_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> r2_hidden(k4_tarski(B,C),A) ) ) & ( ~ r2_hidden(B,k1_relat_1(A)) => ( C = k1_funct_1(A,B) <=> C = k1_xboole_0 ) ) ) ) ), file(funct_1,d4_funct_1), [interesting(0.00)]). fof(t63_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_tarski(B,A) => k4_card_1(k4_xboole_0(A,B)) = k5_real_1(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_2,t63_card_2), [interesting(0.00)]). fof(t49_amistd_2,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) ) => k4_card_1(k11_amistd_2(A,B,C)) = k6_xcmplx_0(k4_card_1(C),1) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_relat_1,t19_ami_1,d1_tarski,t51_amistd_1,d4_funct_1,t63_card_2,t19_ami_1,t79_card_1]), [file(amistd_2,t49_amistd_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(l14_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ~ r1_xreal_0(A,k4_xcmplx_0(1)) ) ), file(amistd_2,l14_amistd_2), [interesting(0.00)]). fof(t23_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( k2_xcmplx_0(A,B) = 0 => ( A = 0 & B = 0 ) ) ) ) ), file(nat_1,t23_nat_1), [interesting(0.00)]). fof(t53_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_xboole_0(A,B) => k4_card_1(k2_xboole_0(A,B)) = k1_nat_1(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_2,t53_card_2), [interesting(0.00)]). fof(t2_amistd_2,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finset_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finset_1(B) ) => ( r1_xboole_0(k1_relat_1(A),k1_relat_1(B)) => k4_card_1(k1_funct_4(A,B)) = k1_nat_1(k4_card_1(A),k4_card_1(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_pre_circ,d1_funct_4,t53_card_2,t21_pre_circ,t21_pre_circ]), [file(amistd_2,t2_amistd_2),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(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)) ) ) ) ) ) ), file(amistd_1,t50_amistd_1), [interesting(0.00)]). fof(t14_amistd_2,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_ami_3(C,A,B) & v9_amistd_1(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_xreal_0(k4_card_1(C),k7_amistd_1(A,B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_amistd_1,t50_amistd_1]), [file(amistd_2,t14_amistd_2),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(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(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(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(t17_finseq_1,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) ) => ( ( k4_finseq_1(A) = k4_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t17_finseq_1), [interesting(0.00)]). fof(t28_amistd_2,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) & v8_amistd_2(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)) => k8_amistd_2(A,B,C,0) = C ) ) ) ), inference(mizar_proof,[status(thm)],[d14_amistd_2,d14_amistd_2,d14_amistd_2,d13_amistd_1,d14_amistd_2,t17_finseq_1,t16_amistd_2]), [file(amistd_2,t28_amistd_2),interesting(0.00)]). fof(t21_funct_4,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => k1_funct_4(k1_xboole_0,A) = A ) ), file(funct_4,t21_funct_4), [interesting(0.00)]). fof(l41_amistd_2,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_relat_1(k6_amistd_2(A,B)) = k1_struct_0(B,k5_amistd_1(A,B,0)) & r2_hidden(k5_amistd_1(A,B,0),k1_relat_1(k6_amistd_2(A,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski]), [file(amistd_2,l41_amistd_2),interesting(0.00)]). fof(t57_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v4_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v10_ami_1(C,B) & v4_amistd_1(C,B) & v6_amistd_2(C,B) & v8_amistd_2(C,B) & l1_ami_1(C,B) ) => k9_amistd_2(B,C,k7_amistd_2(B,C),A) = k7_amistd_2(B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_amistd_2,l41_amistd_2,l41_amistd_2,d1_tarski,d5_ami_5,t6_cqc_lang,d15_amistd_2,t29_amistd_2,t6_cqc_lang,t9_funct_1]), [file(amistd_2,t57_amistd_2),interesting(0.00)]). fof(t58_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_setfam_1(B) => ! [C] : ( ( ~ v3_struct_0(C) & ~ v2_ami_1(C,B) & v4_ami_1(C,B) & v5_ami_1(C,B) & v8_ami_1(C,B) & v4_amistd_1(C,B) & l1_ami_1(C,B) ) => k10_amistd_2(B,C,k7_amistd_2(B,C),A) = k14_ami_3(B,C,k5_amistd_1(B,C,A),k5_ami_1(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_amistd_2,l41_amistd_2,l41_amistd_2,d1_tarski,t25_amistd_1,d1_tarski,d3_tarski,d10_xboole_0,d3_tarski,d1_tarski,t5_cqc_lang,d1_tarski,l41_amistd_2,d16_amistd_2,l42_amistd_2,t6_cqc_lang,t9_funct_1]), [file(amistd_2,t58_amistd_2),interesting(0.00)]). fof(d22_amistd_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) & 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) ) => ( v10_amistd_1(C,A,B) <=> k1_funct_1(C,k10_amistd_1(A,B,C)) = k5_ami_1(A,B) ) ) ) ) ), file(amistd_1,d22_amistd_1), [interesting(0.00)]). fof(t60_card_2,theorem,( ! [A] : ( k1_card_1(A) = 1 <=> ? [B] : A = k1_tarski(B) ) ), file(card_2,t60_card_2), [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(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(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)) ) ) ) ), file(amistd_1,t49_amistd_1), [interesting(0.00)]). fof(t26_amistd_2,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) ) => ! [C] : ( ( ~ v1_xboole_0(C) & v1_ami_3(C,A,B) & v9_amistd_1(C,A,B) & v10_amistd_1(C,A,B) & v11_amistd_1(C,A,B) & m1_ami_1(C,A,B) ) => ( k4_card_1(C) = 1 => C = k6_amistd_2(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_card_2,d1_tarski,d1_relat_1,t23_relat_1,t49_amistd_1,d1_tarski,t4_amistd_2,t55_amistd_1,d22_amistd_1,d5_funct_1,t23_relat_1,d1_tarski,t19_ami_1]), [file(amistd_2,t26_amistd_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(t2_cqc_the1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( r1_xreal_0(A,1) & A != 0 & A != 1 ) ) ), file(cqc_the1,t2_cqc_the1), [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(t41_amistd_2,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_ami_1(C,A,B) => ! [D] : ( v4_ordinal2(D) => ~ ( ~ r1_xreal_0(D,0) & r2_hidden(k5_amistd_1(A,B,0),k1_relat_1(k10_amistd_2(A,B,C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d16_amistd_2,t25_amistd_1,t23_nat_1]), [file(amistd_2,t41_amistd_2),interesting(0.00)]). fof(t51_card_1,theorem,( 0 = k1_xboole_0 ), file(card_1,t51_card_1), [interesting(0.00)]). fof(t78_card_1,theorem,( k4_card_1(k1_xboole_0) = 0 ), file(card_1,t78_card_1), [interesting(0.00)]). fof(t52_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(k5_binarith(A,B),A) ) ) ), file(binarith,t52_binarith), [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(t92_real_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(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) ) & ~ ( ( ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) ) | ( r1_xreal_0(A,B) & ~ r1_xreal_0(D,C) ) ) & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ) ), file(real_1,t92_real_1), [interesting(0.00)]). fof(t31_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ), file(xreal_1,t31_xreal_1), [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(t55_amistd_2,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) & v8_amistd_2(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) & v9_amistd_1(D,A,B) & m1_ami_1(D,A,B) ) => k1_funct_1(k12_amistd_2(A,B,C,D),k10_amistd_1(A,B,C)) = k1_funct_1(k9_amistd_2(A,B,D,k5_binarith(k4_card_1(C),1)),k5_amistd_1(A,B,0)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_amistd_1,t49_amistd_1,d16_amistd_2,t14_funct_4,d16_amistd_2]), [file(amistd_2,t55_amistd_2),interesting(0.00)]). fof(t23_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(k2_xcmplx_0(A,B),k2_xcmplx_0(C,D)) <=> r1_xreal_0(k6_xcmplx_0(A,C),k6_xcmplx_0(D,B)) ) ) ) ) ) ), file(xreal_1,t23_xreal_1), [interesting(0.00)]). fof(t50_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) => k5_binarith(B,A) = k6_xcmplx_0(B,A) ) ) ) ), file(binarith,t50_binarith), [interesting(0.00)]). fof(t18_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(A,B) => r2_hidden(k6_xcmplx_0(B,A),k5_numbers) ) ) ) ), file(int_1,t18_int_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(l15_amistd_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ~ ( r1_xreal_0(1,B) & r1_xreal_0(2,C) & r1_xreal_0(k6_xcmplx_0(B,1),A) & ~ ( r1_xreal_0(B,A) & r1_xreal_0(A,k6_xcmplx_0(k1_nat_1(B,C),3)) ) & A != k6_xcmplx_0(k1_nat_1(B,C),2) & r1_xreal_0(A,k6_xcmplx_0(k1_nat_1(B,C),2)) & A != k6_xcmplx_0(B,1) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_int_1,t38_nat_1,t9_xreal_1,t18_int_1,d5_real_1,t38_nat_1,t1_xreal_1]), [file(amistd_2,l15_amistd_2),interesting(0.00)]).