fof(t166_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => r2_wellord2(k14_group_2(A,B),k15_group_2(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t137_group_2,t19_group_1,t143_group_2,d15_group_2,s2_funct_1,d3_tarski,d5_funct_1,d16_group_2,d10_xboole_0,d3_tarski,d16_group_2,d15_group_2,d5_funct_1,t137_group_2,t143_group_2,d8_funct_1,t143_group_2,t19_group_1,t137_group_2,d4_wellord2]), [file(group_2,t166_group_2),interesting(1.00)]). fof(t77_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => m1_group_2(k5_group_2(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t75_group_2]), [file(group_2,t77_group_2),interesting(0.82)]). fof(t178_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v6_group_1(A) => r1_nat_1(k9_group_1(B),k9_group_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t177_group_2,d3_nat_1]), [file(group_2,t178_group_2),interesting(0.82)]). fof(t183_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( v6_group_1(A) => k17_group_2(A,k5_group_2(A)) = k9_group_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t177_group_2,t81_group_2]), [file(group_2,t183_group_2),interesting(0.80)]). fof(t48_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v6_group_1(A) => v6_group_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,d14_group_1,t13_finset_1,d14_group_1]), [file(group_2,t48_group_2),interesting(0.79)]). fof(t49_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_group_2(C,B) => ( r1_rlvect_1(C,A) => r1_rlvect_1(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,d1_rlvect_1,d1_rlvect_1]), [file(group_2,t49_group_2),interesting(0.78)]). fof(t63_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => m1_group_2(A,A) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t97_relat_1,d5_group_2]), [file(group_2,t63_group_2),interesting(0.78)]). fof(t177_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v6_group_1(A) => k9_group_1(A) = k2_nat_1(k9_group_1(B),k17_group_2(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t164_group_2,d15_group_1,t167_group_2,d15_group_2,t3_group_2,t48_group_2,t156_group_2,d15_group_2,t151_group_2,t138_group_2,l199_group_2,d18_group_2]), [file(group_2,t177_group_2),interesting(0.78)]). fof(t75_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => k5_group_2(B) = k5_group_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_2,t53_group_2,t65_group_2,t68_group_2]), [file(group_2,t75_group_2),interesting(0.76)]). fof(l119_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => m1_group_2(k9_group_2(A,B,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t97_group_2,t17_xboole_1,t66_group_2]), [file(group_2,l119_group_2),interesting(0.75)]). fof(t175_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( k16_group_2(A,B) = k1_card_1(k14_group_2(A,B)) & k16_group_2(A,B) = k1_card_1(k15_group_2(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t166_group_2,t21_card_1]), [file(group_2,t175_group_2),interesting(0.75)]). fof(t80_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => v6_group_1(k5_group_2(A)) ) ), inference(mizar_proof,[status(thm)],[d7_group_2,d14_group_1]), [file(group_2,t80_group_2),interesting(0.74)]). fof(t179_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,C) => ( ( v6_group_1(A) & B = D ) => k17_group_2(A,B) = k2_nat_1(k17_group_2(C,D),k17_group_2(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t177_group_2,t48_group_2,t177_group_2,t90_group_1,t5_xcmplx_1]), [file(group_2,t179_group_2),interesting(0.73)]). fof(t53_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => k2_group_1(B) = k2_group_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t51_group_2,d5_group_1,t52_group_2,t15_group_1]), [file(group_2,t53_group_2),interesting(0.72)]). fof(t51_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => m1_subset_1(C,u1_struct_0(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_group_2,d1_rlvect_1]), [file(group_2,t51_group_2),interesting(0.71)]). fof(t55_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => r1_rlvect_1(B,k2_group_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,t53_group_2]), [file(group_2,t55_group_2),interesting(0.71)]). fof(t50_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => r1_rlvect_1(A,C) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,t49_group_2]), [file(group_2,t50_group_2),interesting(0.70)]). fof(t168_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k14_group_2(A,k5_group_2(A)) = a_1_0_group_2(A) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d15_group_2,t133_group_2,d10_xboole_0,d3_tarski,t133_group_2,d15_group_2]), [file(group_2,t168_group_2),interesting(0.69)]). fof(t3_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v6_group_1(A) => v1_finset_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_group_1,t13_finset_1]), [file(group_2,t3_group_2),interesting(0.68)]). fof(t184_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( ( v6_group_1(A) & k17_group_2(A,B) = k9_group_1(A) ) => r1_group_2(A,B,k5_group_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t177_group_2,t90_group_1,t48_group_2,t5_xcmplx_1,t82_group_2]), [file(group_2,t184_group_2),interesting(0.68)]). fof(l115_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( m1_group_2(C,B) <=> r1_group_2(A,k9_group_2(A,C,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,d10_group_2,t28_xboole_1,t68_group_2,d10_group_2,t17_xboole_1,t66_group_2]), [file(group_2,l115_group_2),interesting(0.66)]). fof(t66_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( r1_tarski(u1_struct_0(B),u1_struct_0(C)) => m1_group_2(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,d5_group_2,t119_zfmisc_1,t82_funct_1]), [file(group_2,t66_group_2),interesting(0.65)]). fof(t70_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( u1_struct_0(B) = u1_struct_0(A) => B = A ) ) ) ), inference(mizar_proof,[status(thm)],[t63_group_2,t68_group_2]), [file(group_2,t70_group_2),interesting(0.65)]). fof(t99_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_group_2(C,B) => ! [D] : ( m1_group_2(D,B) => ( r1_rlvect_1(k8_group_2(B,C,D),A) <=> ( r1_rlvect_1(C,A) & r1_rlvect_1(D,A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,d10_group_2,d3_xboole_0,t88_group_2,t88_group_2,d3_xboole_0,t98_group_2,t88_group_2]), [file(group_2,t99_group_2),interesting(0.64)]). fof(t151_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => r2_wellord2(k12_group_2(A,D,B),k12_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s2_funct_1,d3_tarski,d5_funct_1,t125_group_2,d4_group_1,d4_group_1,d6_group_1,d5_group_1,t125_group_2,d10_xboole_0,d3_tarski,t125_group_2,t125_group_2,d4_group_1,d4_group_1,d6_group_1,d5_group_1,d5_funct_1,d8_funct_1,t14_group_1,d4_wellord2]), [file(group_2,t151_group_2),interesting(0.64)]). fof(t153_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => r2_wellord2(k13_group_2(A,D,B),k13_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t152_group_2,t22_wellord2]), [file(group_2,t153_group_2),interesting(0.64)]). fof(t180_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k17_group_2(A,k6_group_2(A)) = 1 ) ), inference(mizar_proof,[status(thm)],[t172_group_2,d18_group_2,t79_card_1]), [file(group_2,t180_group_2),interesting(0.64)]). fof(t81_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k9_group_1(k5_group_2(A)) = 1 ) ), inference(mizar_proof,[status(thm)],[d7_group_2,t80_group_2,t79_card_1,d15_group_1]), [file(group_2,t81_group_2),interesting(0.64)]). fof(t76_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => k5_group_2(B) = k5_group_2(C) ) ) ) ), inference(mizar_proof,[status(thm)],[t75_group_2,t75_group_2]), [file(group_2,t76_group_2),interesting(0.63)]). fof(t92_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => k1_group_2(A,k7_group_2(A,B)) = k7_group_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t90_group_2,t27_group_2]), [file(group_2,t92_group_2),interesting(0.63)]). fof(t60_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r1_rlvect_1(C,B) => r1_rlvect_1(C,k3_group_1(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,d1_rlvect_1,t57_group_2]), [file(group_2,t60_group_2),interesting(0.62)]). fof(t182_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k16_group_2(A,k5_group_2(A)) = k8_group_1(A) ) ), inference(mizar_proof,[status(thm)],[s3_funct_1,d3_tarski,d5_funct_1,t168_group_2,d10_xboole_0,d3_tarski,t168_group_2,d5_funct_1,d8_funct_1,t6_zfmisc_1,d4_wellord2,t21_card_1]), [file(group_2,t182_group_2),interesting(0.61)]). fof(t101_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => r1_group_2(A,k8_group_2(A,B,C),k8_group_2(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_group_2,d10_group_2,t68_group_2]), [file(group_2,t101_group_2),interesting(0.60)]). fof(t108_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => ( m1_group_2(B,C) => m1_group_2(k9_group_2(A,B,D),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l119_group_2,t65_group_2]), [file(group_2,t108_group_2),interesting(0.60)]). fof(t88_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_group_2(C,B) => ( r2_hidden(A,k7_group_2(B,C)) <=> r1_rlvect_1(C,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1]), [file(group_2,t88_group_2),interesting(0.60)]). fof(t57_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ( D = B => k3_group_1(C,D) = k3_group_1(A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_group_2,d6_group_1,t52_group_2,t53_group_2,t20_group_1]), [file(group_2,t57_group_2),interesting(0.60)]). fof(t152_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => r2_wellord2(k12_group_2(A,D,B),k13_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[s2_funct_1,d3_tarski,d5_funct_1,t125_group_2,d4_group_1,d6_group_1,d5_group_1,t126_group_2,d10_xboole_0,d3_tarski,t126_group_2,t125_group_2,d4_group_1,d6_group_1,d5_group_1,d5_funct_1,d8_funct_1,t14_group_1,t14_group_1,d4_wellord2]), [file(group_2,t152_group_2),interesting(0.60)]). fof(t56_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => r1_rlvect_1(C,k2_group_1(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_group_2,t55_group_2]), [file(group_2,t56_group_2),interesting(0.60)]). fof(t100_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => r1_group_2(A,k8_group_2(A,B,B),B) ) ) ), inference(mizar_proof,[status(thm)],[d10_group_2,t68_group_2]), [file(group_2,t100_group_2),interesting(0.59)]). fof(t106_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( m1_group_2(k9_group_2(A,B,C),B) & m1_group_2(k9_group_2(A,B,C),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l119_group_2]), [file(group_2,t106_group_2),interesting(0.59)]). fof(t109_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => ( ( m1_group_2(B,C) & m1_group_2(B,D) ) => m1_group_2(B,k9_group_2(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t49_group_2,t99_group_2,t67_group_2]), [file(group_2,t109_group_2),interesting(0.58)]). fof(t110_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => ( m1_group_2(B,C) => m1_group_2(k9_group_2(A,B,D),k9_group_2(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,t26_xboole_1,t97_group_2,t97_group_2,t66_group_2]), [file(group_2,t110_group_2),interesting(0.58)]). fof(t54_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => k2_group_1(B) = k2_group_1(C) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_group_2,t53_group_2]), [file(group_2,t54_group_2),interesting(0.58)]). fof(t91_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => k2_group_2(A,k7_group_2(A,B),k7_group_2(A,B)) = k7_group_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t89_group_2,t90_group_2,t26_group_2]), [file(group_2,t91_group_2),interesting(0.58)]). fof(t169_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k15_group_2(A,k5_group_2(A)) = a_1_0_group_2(A) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d16_group_2,t133_group_2,d10_xboole_0,d3_tarski,t133_group_2,d16_group_2]), [file(group_2,t169_group_2),interesting(0.57)]). fof(t62_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => v7_group_1(B) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_group_2,t52_group_2,l32_group_2,t52_group_2,d16_group_1]), [file(group_2,t62_group_2),interesting(0.57)]). fof(t83_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => r1_tarski(k8_group_1(B),k8_group_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,t27_card_1]), [file(group_2,t83_group_2),interesting(0.57)]). fof(t104_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( r1_group_2(A,k9_group_2(A,B,k6_group_2(A)),B) & r1_group_2(A,k9_group_2(A,k6_group_2(A),B),B) ) ) ) ), inference(mizar_proof,[status(thm)],[l115_group_2]), [file(group_2,t104_group_2),interesting(0.56)]). fof(t67_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_rlvect_1(B,D) => r1_rlvect_1(C,D) ) ) => m1_group_2(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t51_group_2,d1_rlvect_1,d1_rlvect_1,t66_group_2]), [file(group_2,t67_group_2),interesting(0.56)]). fof(t173_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( k14_group_2(A,B) = k1_tarski(u1_struct_0(A)) => B = A ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d15_group_2,t125_group_2,t14_group_1,t71_group_2]), [file(group_2,t173_group_2),interesting(0.56)]). fof(t105_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k9_group_2(A,k6_group_2(A),k6_group_2(A)) = A ) ), inference(mizar_proof,[status(thm)],[t104_group_2]), [file(group_2,t105_group_2),interesting(0.55)]). fof(t111_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( ( v6_group_1(B) | v6_group_1(C) ) => v6_group_1(k9_group_2(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l119_group_2,t48_group_2]), [file(group_2,t111_group_2),interesting(0.55)]). fof(t164_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v6_group_1(A) => ( v1_finset_1(k15_group_2(A,B)) & v1_finset_1(k14_group_2(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_group_1,t24_finset_1,t13_finset_1]), [file(group_2,t164_group_2),interesting(0.55)]). fof(t154_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r2_wellord2(k7_group_2(A,C),k12_group_2(A,C,B)) & r2_wellord2(k7_group_2(A,C),k13_group_2(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t132_group_2,t151_group_2,t153_group_2]), [file(group_2,t154_group_2),interesting(0.54)]). fof(t172_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( k14_group_2(A,k6_group_2(A)) = k1_tarski(u1_struct_0(A)) & k15_group_2(A,k6_group_2(A)) = k1_tarski(u1_struct_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[t134_group_2,d15_group_2,d16_group_2,t37_zfmisc_1,d3_tarski,d15_group_2,t134_group_2,d1_tarski,d3_tarski,d16_group_2,t134_group_2,d1_tarski,d10_xboole_0]), [file(group_2,t172_group_2),interesting(0.54)]). fof(t90_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r2_hidden(B,k7_group_2(A,C)) => r2_hidden(k3_group_1(A,B),k7_group_2(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_group_2,t60_group_2,t88_group_2]), [file(group_2,t90_group_2),interesting(0.54)]). fof(t102_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => r1_group_2(A,k9_group_2(A,k9_group_2(A,B,C),D),k9_group_2(A,B,k9_group_2(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_group_2,d10_group_2,t16_xboole_1,d10_group_2,d10_group_2,t68_group_2]), [file(group_2,t102_group_2),interesting(0.53)]). fof(t107_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( m1_group_2(C,B) <=> r1_group_2(A,k9_group_2(A,C,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l115_group_2]), [file(group_2,t107_group_2),interesting(0.53)]). fof(t84_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v6_group_1(A) => r1_xreal_0(k9_group_1(B),k9_group_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t48_group_2,d15_group_1,d15_group_1,d5_group_2,t80_card_1]), [file(group_2,t84_group_2),interesting(0.52)]). fof(t134_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k12_group_2(A,k6_group_2(A),B) = u1_struct_0(A) & k13_group_2(A,k6_group_2(A),B) = u1_struct_0(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t42_group_2,d4_subset_1]), [file(group_2,t134_group_2),interesting(0.51)]). fof(t58_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => k4_group_1(B) = k8_relset_1(u1_struct_0(A),u1_struct_0(A),k4_group_1(A),u1_struct_0(B)) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,d1_funct_2,t28_xboole_1,t51_group_2,d7_group_1,t57_group_2,d7_group_1,t68_funct_1]), [file(group_2,t58_group_2),interesting(0.50)]). fof(t103_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( r1_group_2(A,k9_group_2(A,k5_group_2(A),B),k5_group_2(A)) & r1_group_2(A,k9_group_2(A,B,k5_group_2(A)),k5_group_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t77_group_2,l115_group_2,l115_group_2]), [file(group_2,t103_group_2),interesting(0.49)]). fof(t33_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( r2_hidden(A,k3_group_2(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k1_group_1(B,D,E) & r2_hidden(E,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]), [file(group_2,t33_group_2),interesting(0.49)]). fof(t34_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ( r2_hidden(A,k4_group_2(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k1_group_1(B,E,D) & r2_hidden(E,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]), [file(group_2,t34_group_2),interesting(0.49)]). fof(t9_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k1_group_2(A,k2_subset_1(u1_struct_0(A))) = u1_struct_0(A) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,d3_tarski,d4_subset_1,t19_group_1]), [file(group_2,t9_group_2),interesting(0.49)]). fof(t59_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ( ( r1_rlvect_1(D,B) & r1_rlvect_1(D,C) ) => r1_rlvect_1(D,k1_group_1(A,B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,d1_rlvect_1,t52_group_2]), [file(group_2,t59_group_2),interesting(0.47)]). fof(t142_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r1_rlvect_1(C,B) <=> k13_group_2(A,C,B) = k7_group_2(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t126_group_2,t59_group_2,t88_group_2,d10_xboole_0,d3_tarski,t88_group_2,t49_group_2,d1_rlvect_1,t60_group_2,t59_group_2,d4_group_1,d6_group_1,d5_group_1,t126_group_2,t55_group_2,d5_group_1,t126_group_2,t88_group_2]), [file(group_2,t142_group_2),interesting(0.47)]). fof(t136_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r1_rlvect_1(C,B) <=> k12_group_2(A,C,B) = k7_group_2(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t125_group_2,t59_group_2,t88_group_2,d10_xboole_0,d3_tarski,t88_group_2,t49_group_2,d1_rlvect_1,t60_group_2,t59_group_2,d4_group_1,d6_group_1,d5_group_1,t125_group_2,t55_group_2,d5_group_1,t125_group_2,t88_group_2]), [file(group_2,t136_group_2),interesting(0.47)]). fof(t130_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r2_hidden(B,k12_group_2(A,C,B)) & r2_hidden(B,k13_group_2(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t55_group_2,d5_group_1,t125_group_2,t126_group_2]), [file(group_2,t130_group_2),interesting(0.46)]). fof(t8_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k1_group_2(A,k1_subset_1(u1_struct_0(A))) = k1_xboole_0 ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,t2_xboole_1]), [file(group_2,t8_group_2),interesting(0.46)]). fof(t132_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( k12_group_2(A,B,k2_group_1(A)) = k7_group_2(A,B) & k13_group_2(A,B,k2_group_1(A)) = k7_group_2(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_group_2]), [file(group_2,t132_group_2),interesting(0.45)]). fof(t165_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( r2_hidden(k7_group_2(A,B),k14_group_2(A,B)) & r2_hidden(k7_group_2(A,B),k15_group_2(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t132_group_2,d15_group_2,d16_group_2]), [file(group_2,t165_group_2),interesting(0.45)]). fof(t85_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( ( v6_group_1(A) & k9_group_1(A) = k9_group_1(B) ) => B = A ) ) ) ), inference(mizar_proof,[status(thm)],[t48_group_2,d15_group_1,d15_group_1,d5_group_2,d8_xboole_0,t67_card_2,t70_group_2]), [file(group_2,t85_group_2),interesting(0.43)]). fof(t43_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( k3_group_2(A,k2_group_1(A),B) = B & k4_group_2(A,k2_group_1(A),B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t33_group_2,d5_group_1,d10_xboole_0,d3_tarski,d5_group_1,t33_group_2,d3_tarski,t34_group_2,d5_group_1,d10_xboole_0,d3_tarski,d5_group_1,t34_group_2]), [file(group_2,t43_group_2),interesting(0.42)]). fof(t170_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( k14_group_2(A,B) = a_1_0_group_2(A) => r1_group_2(A,B,k5_group_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_rlvect_1,t51_group_2,t55_group_2,d15_group_2,t125_group_2,d1_tarski,t14_group_1,d1_tarski,t55_group_2,d1_rlvect_1,t37_zfmisc_1,d10_xboole_0,d7_group_2]), [file(group_2,t170_group_2),interesting(0.42)]). fof(t171_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( k15_group_2(A,B) = a_1_0_group_2(A) => r1_group_2(A,B,k5_group_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_rlvect_1,t51_group_2,t55_group_2,d16_group_2,t126_group_2,d1_tarski,t14_group_1,d1_tarski,t55_group_2,d1_rlvect_1,t37_zfmisc_1,d10_xboole_0,d7_group_2]), [file(group_2,t171_group_2),interesting(0.42)]). fof(t174_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( k15_group_2(A,B) = k1_tarski(u1_struct_0(A)) => B = A ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d16_group_2,t126_group_2,t14_group_1,t71_group_2]), [file(group_2,t174_group_2),interesting(0.42)]). fof(t82_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( ( v6_group_1(B) & k9_group_1(B) = 1 ) => r1_group_2(A,B,k5_group_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_group_1,t60_card_2,t55_group_2,d1_rlvect_1,d1_tarski,d7_group_2]), [file(group_2,t82_group_2),interesting(0.42)]). fof(t150_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ? [D] : ( v1_group_1(D) & m1_group_2(D,A) & u1_struct_0(D) = k4_group_2(A,k3_group_1(A,B),k12_group_2(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t130_group_2,l1_group_2,t34_group_2,t34_group_2,t128_group_2,t33_group_2,t125_group_2,t126_group_2,d4_group_1,d4_group_1,d6_group_1,d5_group_1,d4_group_1,d4_group_1,t59_group_2,t125_group_2,t34_group_2,t34_group_2,t125_group_2,t25_group_1,t19_group_1,t25_group_1,t60_group_2,t126_group_2,t33_group_2,t128_group_2,t61_group_2]), [file(group_2,t150_group_2),interesting(0.41)]). fof(t27_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_hidden(C,B) => r2_hidden(k3_group_1(A,C),B) ) ) => k1_group_2(A,B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,d3_tarski,t19_group_1]), [file(group_2,t27_group_2),interesting(0.40)]). fof(t98_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => k7_group_2(A,k8_group_2(A,B,C)) = k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k7_group_2(A,B),k7_group_2(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_group_2]), [file(group_2,t98_group_2),interesting(0.39)]). fof(t129_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => k4_group_2(A,C,k13_group_2(A,D,B)) = k13_group_2(A,D,k1_group_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t40_group_2]), [file(group_2,t129_group_2),interesting(0.38)]). fof(t185_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( ( v1_finset_1(k14_group_2(A,B)) & k16_group_2(A,B) = k8_group_1(A) ) => ( v6_group_1(A) & r1_group_2(A,B,k5_group_2(A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_card_2,d14_group_1,d15_group_1,d18_group_2,t184_group_2]), [file(group_2,t185_group_2),interesting(0.38)]). fof(t128_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => k4_group_2(A,C,k12_group_2(A,D,B)) = k3_group_2(A,B,k13_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_group_2]), [file(group_2,t128_group_2),interesting(0.37)]). fof(t181_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( ( v1_finset_1(k14_group_2(A,B)) & k17_group_2(A,B) = 1 ) => B = A ) ) ) ), inference(mizar_proof,[status(thm)],[d18_group_2,t60_card_2,t167_group_2,t31_zfmisc_1,t173_group_2]), [file(group_2,t181_group_2),interesting(0.37)]). fof(t41_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k4_group_2(A,B,k1_subset_1(u1_struct_0(A))) = k1_xboole_0 & k3_group_2(A,B,k1_subset_1(u1_struct_0(A))) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[t20_group_2]), [file(group_2,t41_group_2),interesting(0.36)]). fof(t6_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_group_2(A,k6_domain_1(u1_struct_0(A),B)) = k6_domain_1(u1_struct_0(A),k3_group_1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_tarski,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski]), [file(group_2,t6_group_2),interesting(0.35)]). fof(t94_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ~ ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) & ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => u1_struct_0(D) != k2_group_2(A,k7_group_2(A,B),k7_group_2(A,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_group_2,t93_group_2]), [file(group_2,t94_group_2),interesting(0.34)]). fof(t125_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_group_2(D,B) => ( r2_hidden(A,k12_group_2(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k1_group_1(B,C,E) & r1_rlvect_1(D,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_group_2,t88_group_2,t88_group_2,t33_group_2]), [file(group_2,t125_group_2),interesting(0.31)]). fof(t155_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( k8_group_1(C) = k1_card_1(k12_group_2(A,C,B)) & k8_group_1(C) = k1_card_1(k13_group_2(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t154_group_2,t21_card_1,t154_group_2,t21_card_1]), [file(group_2,t155_group_2),interesting(0.31)]). fof(t127_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => k12_group_2(A,D,k1_group_1(A,B,C)) = k3_group_2(A,B,k12_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_group_2]), [file(group_2,t127_group_2),interesting(0.31)]). fof(t126_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_group_2(D,B) => ( r2_hidden(A,k13_group_2(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k1_group_1(B,E,C) & r1_rlvect_1(D,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_group_2,t88_group_2,t88_group_2,t34_group_2]), [file(group_2,t126_group_2),interesting(0.30)]). fof(t120_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => k10_group_2(A,D,k11_group_2(A,C,B)) = k11_group_2(A,C,k10_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t116_group_2]), [file(group_2,t120_group_2),interesting(0.26)]). fof(t147_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => r1_tarski(k13_group_2(A,C,k6_group_1(A,2,B)),k2_group_2(A,k13_group_2(A,C,B),k13_group_2(A,C,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t129_group_2,t45_group_1,t145_group_2]), [file(group_2,t147_group_2),interesting(0.24)]). fof(t141_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => r1_tarski(k12_group_2(A,C,k6_group_1(A,2,B)),k2_group_2(A,k12_group_2(A,C,B),k12_group_2(A,C,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t45_group_1,t139_group_2]), [file(group_2,t141_group_2),interesting(0.23)]). fof(t156_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ~ ( v6_group_1(C) & ! [D] : ( v1_finset_1(D) => ! [E] : ( v1_finset_1(E) => ~ ( D = k12_group_2(A,C,B) & E = k13_group_2(A,C,B) & k9_group_1(C) = k4_card_1(D) & k9_group_1(C) = k4_card_1(E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_group_1,t154_group_2,t68_card_1,t81_card_1]), [file(group_2,t156_group_2),interesting(0.23)]). fof(t148_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => k12_group_2(A,k9_group_2(A,C,D),B) = k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k12_group_2(A,C,B),k12_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t125_group_2,t99_group_2,t125_group_2,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,t125_group_2,t125_group_2,t14_group_1,t99_group_2,t125_group_2]), [file(group_2,t148_group_2),interesting(0.17)]). fof(t149_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => k13_group_2(A,k9_group_2(A,C,D),B) = k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k13_group_2(A,C,B),k13_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t126_group_2,t99_group_2,t126_group_2,d3_xboole_0,d10_xboole_0,d3_tarski,d3_xboole_0,t126_group_2,t126_group_2,t14_group_1,t99_group_2,t126_group_2]), [file(group_2,t149_group_2),interesting(0.17)]). fof(t146_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r1_tarski(k7_group_2(A,C),k2_group_2(A,k13_group_2(A,C,B),k13_group_2(A,C,k3_group_1(A,B)))) & r1_tarski(k7_group_2(A,C),k2_group_2(A,k13_group_2(A,C,k3_group_1(A,B)),k13_group_2(A,C,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t129_group_2,d6_group_1,t132_group_2,t129_group_2,d6_group_1,t132_group_2,t145_group_2]), [file(group_2,t146_group_2),interesting(0.16)]). fof(t140_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( r1_tarski(k7_group_2(A,C),k2_group_2(A,k12_group_2(A,C,B),k12_group_2(A,C,k3_group_1(A,B)))) & r1_tarski(k7_group_2(A,C),k2_group_2(A,k12_group_2(A,C,k3_group_1(A,B)),k12_group_2(A,C,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_group_1,t132_group_2,d6_group_1,t132_group_2,t139_group_2]), [file(group_2,t140_group_2),interesting(0.15)]). fof(t122_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_group_2(C,A) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => k10_group_2(A,C,B) = k11_group_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_group_2]), [file(group_2,t122_group_2),interesting(0.13)]). fof(t119_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => k10_group_2(A,D,k10_group_2(A,C,B)) = k2_group_2(A,B,k11_group_2(A,C,k7_group_2(A,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t119_group_2),interesting(0.12)]). fof(t61_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ~ ( B != k1_xboole_0 & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( r2_hidden(C,B) & r2_hidden(D,B) ) => r2_hidden(k1_group_1(A,C,D),B) ) ) ) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_hidden(C,B) => r2_hidden(k3_group_1(A,C),B) ) ) & ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => u1_struct_0(C) != B ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,t90_relat_1,t28_xboole_1,d3_tarski,d5_funct_1,t102_zfmisc_1,t106_zfmisc_1,t106_zfmisc_1,t70_funct_1,d1_funct_2,t11_relset_1,t72_funct_1,l1_group_2,d6_group_1,d3_group_1,l1_group_2,d5_group_1,d5_group_1,d6_group_1,d6_group_1,d5_group_2]), [file(group_2,t61_group_2),interesting(0.06)]). fof(d10_group_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => ( D = k8_group_2(A,B,C) <=> u1_struct_0(D) = k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k7_group_2(A,B),k7_group_2(A,C)) ) ) ) ) ) ), file(group_2,d10_group_2), [interesting(0.00)]). fof(d5_group_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & l1_group_1(B) ) => ( m1_group_2(B,A) <=> ( r1_tarski(u1_struct_0(B),u1_struct_0(A)) & u1_group_1(B) = k1_realset1(u1_group_1(A),u1_struct_0(B)) ) ) ) ) ), file(group_2,d5_group_2), [interesting(0.00)]). fof(t119_zfmisc_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ), file(zfmisc_1,t119_zfmisc_1), [interesting(0.00)]). fof(t82_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r1_tarski(A,B) => ( k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,A) & k7_relat_1(k7_relat_1(C,B),A) = k7_relat_1(C,A) ) ) ) ), file(funct_1,t82_funct_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(t101_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k7_relat_1(k7_relat_1(B,A),A) = k7_relat_1(B,A) ) ), file(relat_1,t101_relat_1), [interesting(0.00)]). fof(t64_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ( ( m1_group_2(A,B) & m1_group_2(B,A) ) => g1_group_1(u1_struct_0(A),u1_group_1(A)) = g1_group_1(u1_struct_0(B),u1_group_1(B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,d10_xboole_0,d5_group_2,d5_group_2,t101_relat_1,d5_group_2,d10_xboole_0]), [file(group_2,t64_group_2),interesting(0.00)]). fof(t68_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( u1_struct_0(B) = u1_struct_0(C) => g1_group_1(u1_struct_0(B),u1_group_1(B)) = g1_group_1(u1_struct_0(C),u1_group_1(C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_group_2,t64_group_2]), [file(group_2,t68_group_2),interesting(0.00)]). fof(t16_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(k3_xboole_0(A,B),C) = k3_xboole_0(A,k3_xboole_0(B,C)) ), file(xboole_1,t16_xboole_1), [interesting(0.00)]). fof(d7_group_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ( B = k5_group_2(A) <=> u1_struct_0(B) = k6_domain_1(u1_struct_0(A),k2_group_1(A)) ) ) ) ), file(group_2,d7_group_2), [interesting(0.00)]). fof(d1_rlvect_1,definition,( ! [A] : ( l1_struct_0(A) => ! [B] : ( r1_rlvect_1(A,B) <=> r2_hidden(B,u1_struct_0(A)) ) ) ), file(rlvect_1,d1_rlvect_1), [interesting(0.00)]). fof(d5_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v2_group_1(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( B = k2_group_1(A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k1_group_1(A,C,B) = C & k1_group_1(A,B,C) = C ) ) ) ) ) ) ), file(group_1,d5_group_1), [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(t52_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ! [E] : ( m1_subset_1(E,u1_struct_0(D)) => ! [F] : ( m1_subset_1(F,u1_struct_0(D)) => ( ( E = B & F = C ) => k1_group_1(D,E,F) = k1_group_1(A,B,C) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,t72_funct_1]), [file(group_2,t52_group_2),interesting(0.00)]). fof(t15_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( k1_group_1(A,B,C) = B | k1_group_1(A,C,B) = B ) => C = k2_group_1(A) ) ) ) ) ), file(group_1,t15_group_1), [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(t65_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( ( ~ v3_struct_0(C) & v3_group_1(C) & v4_group_1(C) & l1_group_1(C) ) => ( ( m1_group_2(A,B) & m1_group_2(B,C) ) => m1_group_2(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,t1_xboole_1,t119_zfmisc_1,d5_group_2,d5_group_2,t82_funct_1,d5_group_2]), [file(group_2,t65_group_2),interesting(0.00)]). fof(t28_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k3_xboole_0(A,B) = A ) ), file(xboole_1,t28_xboole_1), [interesting(0.00)]). fof(t17_xboole_1,theorem,( ! [A,B] : r1_tarski(k3_xboole_0(A,B),A) ), file(xboole_1,t17_xboole_1), [interesting(0.00)]). fof(t97_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( ! [D] : ( m1_group_2(D,A) => ( D = k8_group_2(A,B,C) => u1_struct_0(D) = k3_xboole_0(u1_struct_0(B),u1_struct_0(C)) ) ) & ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => ( u1_struct_0(D) = k3_xboole_0(u1_struct_0(B),u1_struct_0(C)) => r1_group_2(A,D,k8_group_2(A,B,C)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_group_2,d10_group_2]), [file(group_2,t97_group_2),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(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(l1_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & l1_struct_0(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,C) => m1_subset_1(A,u1_struct_0(B)) ) ) ) ), file(group_2,l1_group_2), [interesting(0.00)]). fof(t5_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,k1_group_2(B,C)) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(B)) & A = k3_group_1(B,D) & r2_hidden(D,C) ) ) ) ) ), file(group_2,t5_group_2), [interesting(0.00)]). fof(t10_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( ~ ( B != k1_xboole_0 & k1_group_2(A,B) = k1_xboole_0 ) & ~ ( k1_group_2(A,B) != k1_xboole_0 & B = k1_xboole_0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[l1_group_2,t5_group_2]), [file(group_2,t10_group_2),interesting(0.00)]). fof(t26_xboole_1,theorem,( ! [A,B,C] : ( r1_tarski(A,B) => r1_tarski(k3_xboole_0(A,C),k3_xboole_0(B,C)) ) ), file(xboole_1,t26_xboole_1), [interesting(0.00)]). fof(d14_group_1,definition,( ! [A] : ( l1_struct_0(A) => ( v6_group_1(A) <=> v1_finset_1(u1_struct_0(A)) ) ) ), file(group_1,d14_group_1), [interesting(0.00)]). fof(t13_finset_1,theorem,( ! [A,B] : ( ( r1_tarski(A,B) & v1_finset_1(B) ) => v1_finset_1(A) ) ), file(finset_1,t13_finset_1), [interesting(0.00)]). fof(t112_group_2,theorem,( $true ), file(group_2,t112_group_2), [interesting(0.00)]). fof(t113_group_2,theorem,( $true ), file(group_2,t113_group_2), [interesting(0.00)]). fof(t114_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ! [D] : ( m1_group_2(D,B) => ( r2_hidden(A,k10_group_2(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & ? [F] : ( m1_subset_1(F,u1_struct_0(B)) & A = k1_group_1(B,E,F) & r2_hidden(E,C) & r1_rlvect_1(D,F) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_group_2,t88_group_2]), [file(group_2,t114_group_2),interesting(0.00)]). fof(t115_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ! [D] : ( m1_group_2(D,B) => ( r2_hidden(A,k11_group_2(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & ? [F] : ( m1_subset_1(F,u1_struct_0(B)) & A = k1_group_1(B,E,F) & r1_rlvect_1(D,E) & r2_hidden(F,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_group_2,t88_group_2]), [file(group_2,t115_group_2),interesting(0.00)]). fof(d4_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v4_group_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k1_group_1(A,k1_group_1(A,B,C),D) = k1_group_1(A,B,k1_group_1(A,C,D)) ) ) ) ) ) ), file(group_1,d4_group_1), [interesting(0.00)]). fof(t14_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( v4_group_1(A) => k2_group_2(A,k2_group_2(A,B,C),D) = k2_group_2(A,B,k2_group_2(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_group_1,d10_xboole_0,d3_tarski,d4_group_1]), [file(group_2,t14_group_2),interesting(0.00)]). fof(t117_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k2_group_2(A,k10_group_2(A,D,B),C) = k2_group_2(A,B,k11_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t117_group_2),interesting(0.00)]). fof(t11_group_2,theorem,( $true ), file(group_2,t11_group_2), [interesting(0.00)]). fof(t116_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k10_group_2(A,D,k2_group_2(A,B,C)) = k2_group_2(A,B,k10_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t116_group_2),interesting(0.00)]). fof(t118_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k2_group_2(A,k11_group_2(A,D,B),C) = k11_group_2(A,D,k2_group_2(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t118_group_2),interesting(0.00)]). fof(t121_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_group_2(C,A) => ! [D] : ( m1_group_2(D,A) => k2_group_2(A,k11_group_2(A,C,k7_group_2(A,D)),B) = k11_group_2(A,C,k11_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t118_group_2]), [file(group_2,t121_group_2),interesting(0.00)]). fof(l32_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k10_group_1(A,B,C) = k10_group_1(A,C,B) ) ) ) ), file(group_2,l32_group_2), [interesting(0.00)]). fof(t29_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => k2_group_2(A,B,C) = k2_group_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,l32_group_2,d10_xboole_0,d3_tarski,l32_group_2]), [file(group_2,t29_group_2),interesting(0.00)]). fof(t123_group_2,theorem,( $true ), file(group_2,t123_group_2), [interesting(0.00)]). fof(t124_group_2,theorem,( $true ), file(group_2,t124_group_2), [interesting(0.00)]). fof(t131_group_2,theorem,( $true ), file(group_2,t131_group_2), [interesting(0.00)]). fof(t44_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => k3_group_2(A,B,C) = k4_group_2(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_group_2]), [file(group_2,t44_group_2),interesting(0.00)]). fof(t135_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_group_2(C,A) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => k12_group_2(A,C,B) = k13_group_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t44_group_2]), [file(group_2,t135_group_2),interesting(0.00)]). fof(d6_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k3_group_1(A,B) <=> ( k1_group_1(A,B,C) = k2_group_1(A) & k1_group_1(A,C,B) = k2_group_1(A) ) ) ) ) ) ), file(group_1,d6_group_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(t139_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => r1_tarski(k12_group_2(A,D,k1_group_1(A,B,C)),k2_group_2(A,k12_group_2(A,D,B),k12_group_2(A,D,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t125_group_2,d5_group_1,d4_group_1,t55_group_2,t125_group_2]), [file(group_2,t139_group_2),interesting(0.00)]). fof(t45_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_group_1(A,2,B) = k1_group_1(A,B,B) ) ) ), file(group_1,t45_group_1), [interesting(0.00)]). fof(t66_xboole_1,theorem,( ! [A] : ( ~ ( ~ r1_xboole_0(A,A) & A = k1_xboole_0 ) & ~ ( A != k1_xboole_0 & r1_xboole_0(A,A) ) ) ), file(xboole_1,t66_xboole_1), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t21_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( k1_group_1(A,B,C) = D <=> C = k1_group_1(A,k3_group_1(A,B),D) ) ) ) ) ) ), file(group_1,t21_group_1), [interesting(0.00)]). fof(t22_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( k1_group_1(A,B,C) = D <=> B = k1_group_1(A,D,k3_group_1(A,C)) ) ) ) ) ) ), file(group_1,t22_group_1), [interesting(0.00)]). fof(t20_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( k1_group_1(A,B,C) = k2_group_1(A) | k1_group_1(A,C,B) = k2_group_1(A) ) => ( B = k3_group_1(A,C) & C = k3_group_1(A,B) ) ) ) ) ) ), file(group_1,t20_group_1), [interesting(0.00)]). fof(t22_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_group_2(A,k6_domain_1(u1_struct_0(A),B),k6_domain_1(u1_struct_0(A),C)) = k6_domain_1(u1_struct_0(A),k1_group_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_tarski,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski]), [file(group_2,t22_group_2),interesting(0.00)]). fof(t40_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( v4_group_1(A) => k4_group_2(A,D,k4_group_2(A,C,B)) = k4_group_2(A,k1_group_1(A,C,D),B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2,t22_group_2]), [file(group_2,t40_group_2),interesting(0.00)]). fof(t143_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ( k13_group_2(A,D,B) = k13_group_2(A,D,C) <=> r1_rlvect_1(D,k1_group_1(A,C,k3_group_1(A,B))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_group_2,d6_group_1,t129_group_2,t129_group_2,t142_group_2,t142_group_2,t129_group_2,d4_group_1,d6_group_1,d5_group_1]), [file(group_2,t143_group_2),interesting(0.00)]). fof(t144_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ( k13_group_2(A,D,B) = k13_group_2(A,D,C) <=> ~ r1_xboole_0(k13_group_2(A,D,B),k13_group_2(A,D,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t130_group_2,t66_xboole_1,t3_xboole_0,t126_group_2,t126_group_2,t21_group_1,d4_group_1,t22_group_1,t60_group_2,t59_group_2,t143_group_2]), [file(group_2,t144_group_2),interesting(0.00)]). fof(t145_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => r1_tarski(k4_group_2(A,C,k13_group_2(A,D,B)),k2_group_2(A,k13_group_2(A,D,B),k13_group_2(A,D,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t129_group_2,t126_group_2,t55_group_2,t126_group_2,d4_group_1,d5_group_1]), [file(group_2,t145_group_2),interesting(0.00)]). fof(t14_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( k1_group_1(A,B,C) = k1_group_1(A,B,D) | k1_group_1(A,C,B) = k1_group_1(A,D,B) ) => C = D ) ) ) ) ) ), file(group_1,t14_group_1), [interesting(0.00)]). fof(t39_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( v4_group_1(A) => k4_group_2(A,D,k3_group_2(A,C,B)) = k3_group_2(A,C,k4_group_2(A,D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t39_group_2),interesting(0.00)]). fof(t25_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k3_group_1(A,k1_group_1(A,B,C)) = k1_group_1(A,k3_group_1(A,C),k3_group_1(A,B)) ) ) ) ), file(group_1,t25_group_1), [interesting(0.00)]). fof(t19_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_group_1(A,k3_group_1(A,B)) = B ) ) ), file(group_1,t19_group_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(t90_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => k1_relat_1(k7_relat_1(B,A)) = k3_xboole_0(k1_relat_1(B),A) ) ), file(relat_1,t90_relat_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(t102_zfmisc_1,theorem,( ! [A,B,C] : ~ ( r2_hidden(A,k2_zfmisc_1(B,C)) & ! [D,E] : k4_tarski(D,E) != A ) ), file(zfmisc_1,t102_zfmisc_1), [interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(t70_funct_1,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A))) => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ), file(funct_1,t70_funct_1), [interesting(0.00)]). fof(t11_relset_1,theorem,( ! [A,B,C] : ( v1_relat_1(C) => ( ( r1_tarski(k1_relat_1(C),A) & r1_tarski(k2_relat_1(C),B) ) => m2_relset_1(C,A,B) ) ) ), file(relset_1,t11_relset_1), [interesting(0.00)]). fof(d3_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v3_group_1(A) <=> ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k1_group_1(A,C,B) = C & k1_group_1(A,B,C) = C & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & k1_group_1(A,C,D) = B & k1_group_1(A,D,C) = B ) ) ) ) ) ) ), file(group_1,d3_group_1), [interesting(0.00)]). fof(s2_funct_1,theorem, ( ( ! [A,B,C] : ( ( r2_hidden(A,f1_s2_funct_1) & p1_s2_funct_1(A,B) & p1_s2_funct_1(A,C) ) => B = C ) & ! [A] : ~ ( r2_hidden(A,f1_s2_funct_1) & ! [B] : ~ p1_s2_funct_1(A,B) ) ) => ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s2_funct_1 & ! [B] : ( r2_hidden(B,f1_s2_funct_1) => p1_s2_funct_1(B,k1_funct_1(A,B)) ) ) ), file(funct_1,s2_funct_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(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(t22_wellord2,theorem,( ! [A,B,C] : ( ( r2_wellord2(A,B) & r2_wellord2(B,C) ) => r2_wellord2(A,C) ) ), file(wellord2,t22_wellord2), [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(t157_group_2,theorem,( $true ), file(group_2,t157_group_2), [interesting(0.00)]). fof(t158_group_2,theorem,( $true ), file(group_2,t158_group_2), [interesting(0.00)]). fof(t159_group_2,theorem,( $true ), file(group_2,t159_group_2), [interesting(0.00)]). fof(t15_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => k1_group_2(A,k2_group_2(A,B,C)) = k2_group_2(A,k1_group_2(A,C),k1_group_2(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t25_group_1,d10_xboole_0,d3_tarski,t25_group_1]), [file(group_2,t15_group_2),interesting(0.00)]). fof(t160_group_2,theorem,( $true ), file(group_2,t160_group_2), [interesting(0.00)]). fof(t161_group_2,theorem,( $true ), file(group_2,t161_group_2), [interesting(0.00)]). fof(t162_group_2,theorem,( $true ), file(group_2,t162_group_2), [interesting(0.00)]). fof(t163_group_2,theorem,( $true ), file(group_2,t163_group_2), [interesting(0.00)]). fof(d15_group_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ( C = k14_group_2(A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(D,C) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & D = k12_group_2(A,B,E) ) ) ) ) ) ) ) ), file(group_2,d15_group_2), [interesting(0.00)]). fof(d16_group_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) => ( C = k15_group_2(A,B) <=> ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(D,C) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & D = k13_group_2(A,B,E) ) ) ) ) ) ) ) ), file(group_2,d16_group_2), [interesting(0.00)]). fof(t133_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k13_group_2(A,k5_group_2(A),B) = k6_domain_1(u1_struct_0(A),B) & k12_group_2(A,k5_group_2(A),B) = k6_domain_1(u1_struct_0(A),B) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_2,t22_group_2,d5_group_1,t22_group_2,d5_group_1]), [file(group_2,t133_group_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(t16_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => k2_group_2(A,B,k1_finsub_1(k1_zfmisc_1(u1_struct_0(A)),C,D)) = k1_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k2_group_2(A,B,C),k2_group_2(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d2_xboole_0,d2_xboole_0,d10_xboole_0,d3_tarski,d2_xboole_0,d2_xboole_0,d2_xboole_0]), [file(group_2,t16_group_2),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(t97_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k1_relat_1(B),A) => k7_relat_1(B,A) = B ) ) ), file(relat_1,t97_relat_1), [interesting(0.00)]). fof(t69_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_rlvect_1(B,D) <=> r1_rlvect_1(C,D) ) ) => g1_group_1(u1_struct_0(B),u1_group_1(B)) = g1_group_1(u1_struct_0(C),u1_group_1(C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t67_group_2,t64_group_2]), [file(group_2,t69_group_2),interesting(0.00)]). fof(t71_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_rlvect_1(B,C) ) => g1_group_1(u1_struct_0(B),u1_group_1(B)) = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,t63_group_2,t69_group_2]), [file(group_2,t71_group_2),interesting(0.00)]). fof(t38_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( v4_group_1(A) => k3_group_2(A,k1_group_1(A,C,D),B) = k3_group_2(A,C,k3_group_2(A,D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_group_2,t14_group_2]), [file(group_2,t38_group_2),interesting(0.00)]). fof(t137_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ( k12_group_2(A,D,B) = k12_group_2(A,D,C) <=> r1_rlvect_1(D,k1_group_1(A,k3_group_1(A,C),B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t127_group_2,t127_group_2,d6_group_1,t132_group_2,t136_group_2,t43_group_2,t127_group_2,d6_group_1,d4_group_1,t127_group_2,t136_group_2]), [file(group_2,t137_group_2),interesting(0.00)]). fof(d18_group_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v1_finset_1(k14_group_2(A,B)) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k17_group_2(A,B) <=> ? [D] : ( v1_finset_1(D) & D = k14_group_2(A,B) & C = k4_card_1(D) ) ) ) ) ) ) ), file(group_2,d18_group_2), [interesting(0.00)]). fof(t68_card_1,theorem,( ! [A,B] : ( ( r2_wellord2(A,B) & v1_finset_1(A) ) => v1_finset_1(B) ) ), file(card_1,t68_card_1), [interesting(0.00)]). fof(t81_card_1,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r2_wellord2(A,B) => k4_card_1(A) = k4_card_1(B) ) ) ) ), file(card_1,t81_card_1), [interesting(0.00)]). fof(t176_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( v1_finset_1(k14_group_2(A,B)) => ( ? [C] : ( v1_finset_1(C) & C = k14_group_2(A,B) & k17_group_2(A,B) = k4_card_1(C) ) & ? [C] : ( v1_finset_1(C) & C = k15_group_2(A,B) & k17_group_2(A,B) = k4_card_1(C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d18_group_2,d18_group_2,t166_group_2,t68_card_1,t81_card_1]), [file(group_2,t176_group_2),interesting(0.00)]). fof(t24_finset_1,theorem,( ! [A] : ( v1_finset_1(A) <=> v1_finset_1(k1_zfmisc_1(A)) ) ), file(finset_1,t24_finset_1), [interesting(0.00)]). fof(d15_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( v6_group_1(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k9_group_1(A) <=> ? [C] : ( v1_finset_1(C) & C = u1_struct_0(A) & B = k4_card_1(C) ) ) ) ) ) ), file(group_1,d15_group_1), [interesting(0.00)]). fof(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [interesting(0.00)]). fof(t167_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ( k5_setfam_1(u1_struct_0(A),k14_group_2(A,B)) = u1_struct_0(A) & k5_setfam_1(u1_struct_0(A),k15_group_2(A,B)) = u1_struct_0(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,d3_tarski,t51_group_2,d1_rlvect_1,d5_group_1,d6_group_1,d4_group_1,d15_group_2,t125_group_2,d4_tarski,d10_xboole_0,d3_tarski,t51_group_2,d1_rlvect_1,d5_group_1,d6_group_1,d4_group_1,d16_group_2,t126_group_2,d4_tarski]), [file(group_2,t167_group_2),interesting(0.00)]). fof(t138_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ( k12_group_2(A,D,B) = k12_group_2(A,D,C) <=> ~ r1_xboole_0(k12_group_2(A,D,B),k12_group_2(A,D,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t130_group_2,t66_xboole_1,t3_xboole_0,t125_group_2,t125_group_2,t22_group_1,d4_group_1,t21_group_1,t60_group_2,t59_group_2,t137_group_2]), [file(group_2,t138_group_2),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(t2_zfmisc_1,theorem,( k3_tarski(k1_xboole_0) = k1_xboole_0 ), file(zfmisc_1,t2_zfmisc_1), [interesting(0.00)]). fof(t25_finset_1,theorem,( ! [A] : ( ( v1_finset_1(A) & ! [B] : ( r2_hidden(B,A) => v1_finset_1(B) ) ) <=> v1_finset_1(k3_tarski(A)) ) ), file(finset_1,t25_finset_1), [interesting(0.00)]). fof(t31_zfmisc_1,theorem,( ! [A] : k3_tarski(k1_tarski(A)) = A ), file(zfmisc_1,t31_zfmisc_1), [interesting(0.00)]). fof(t96_zfmisc_1,theorem,( ! [A,B] : k3_tarski(k2_xboole_0(A,B)) = k2_xboole_0(k3_tarski(A),k3_tarski(B)) ), file(zfmisc_1,t96_zfmisc_1), [interesting(0.00)]). fof(t54_card_2,theorem,( ! [A,B] : ( v1_finset_1(B) => ( ~ r2_hidden(A,B) => k4_card_1(k2_xboole_0(B,k1_tarski(A))) = k1_nat_1(k4_card_1(B),1) ) ) ), file(card_2,t54_card_2), [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(s2_setwiseo,theorem, ( ( p1_s2_setwiseo(k1_setwiseo(f1_s2_setwiseo)) & ! [A] : ( m1_subset_1(A,k5_finsub_1(f1_s2_setwiseo)) => ! [B] : ( m1_subset_1(B,f1_s2_setwiseo) => ( p1_s2_setwiseo(A) => ( r2_hidden(B,A) | p1_s2_setwiseo(k5_setwiseo(f1_s2_setwiseo,A,k2_setwiseo(f1_s2_setwiseo,B))) ) ) ) ) ) => ! [A] : ( m1_subset_1(A,k5_finsub_1(f1_s2_setwiseo)) => p1_s2_setwiseo(A) ) ), file(setwiseo,s2_setwiseo), [interesting(0.00)]). fof(d5_finsub_1,definition,( ! [A,B] : ( v4_finsub_1(B) => ( B = k5_finsub_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ( r1_tarski(C,A) & v1_finset_1(C) ) ) ) ) ), file(finsub_1,d5_finsub_1), [interesting(0.00)]). fof(l199_group_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_finset_1(B) => ~ ( ! [C] : ~ ( r2_hidden(C,B) & ! [D] : ( v1_finset_1(D) => ~ ( D = C & k4_card_1(D) = A & ! [E] : ( r2_hidden(E,B) => ( C = E | ( r2_wellord2(C,E) & r1_xboole_0(C,E) ) ) ) ) ) ) & ! [C] : ( v1_finset_1(C) => ~ ( C = k3_tarski(B) & k4_card_1(C) = k2_nat_1(A,k4_card_1(B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t78_card_1,t2_zfmisc_1,t78_card_1,t2_zfmisc_1,d1_tarski,d2_xboole_0,t25_finset_1,t31_zfmisc_1,d1_tarski,d2_xboole_0,t3_xboole_0,d4_tarski,d4_tarski,d1_tarski,d2_xboole_0,t3_xboole_0,t96_zfmisc_1,d2_xboole_0,d2_xboole_0,t54_card_2,t53_card_2,s2_setwiseo,d5_finsub_1]), [file(group_2,l199_group_2),interesting(0.00)]). fof(d3_nat_1,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_nat_1(A,B) <=> ? [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) & B = k3_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,d3_nat_1), [interesting(0.00)]). fof(t90_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( v6_group_1(A) => r1_xreal_0(1,k9_group_1(A)) ) ) ), file(group_1,t90_group_1), [interesting(0.00)]). fof(t5_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => ( k3_xcmplx_0(B,A) = k3_xcmplx_0(C,A) => ( A = 0 | B = C ) ) ) ) ) ), file(xcmplx_1,t5_xcmplx_1), [interesting(0.00)]). fof(t17_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => k2_group_2(A,k1_finsub_1(k1_zfmisc_1(u1_struct_0(A)),B,C),D) = k1_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k2_group_2(A,B,D),k2_group_2(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d2_xboole_0,d2_xboole_0,d10_xboole_0,d3_tarski,d2_xboole_0,d2_xboole_0,d2_xboole_0]), [file(group_2,t17_group_2),interesting(0.00)]). fof(d4_subset_1,definition,( ! [A] : k2_subset_1(A) = A ), file(subset_1,d4_subset_1), [interesting(0.00)]). fof(t21_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( B != k1_xboole_0 => ( k2_group_2(A,k2_subset_1(u1_struct_0(A)),B) = u1_struct_0(A) & k2_group_2(A,B,k2_subset_1(u1_struct_0(A))) = u1_struct_0(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_xboole_0,d3_tarski,l1_group_2,d4_group_1,d6_group_1,d5_group_1,d4_subset_1,d10_xboole_0,d3_tarski,l1_group_2,d4_group_1,d6_group_1,d5_group_1,d4_subset_1]), [file(group_2,t21_group_2),interesting(0.00)]). fof(t42_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k4_group_2(A,B,k2_subset_1(u1_struct_0(A))) = u1_struct_0(A) & k3_group_2(A,B,k2_subset_1(u1_struct_0(A))) = u1_struct_0(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_group_2]), [file(group_2,t42_group_2),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(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(s3_funct_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = f1_s3_funct_1 & ! [B] : ( r2_hidden(B,f1_s3_funct_1) => k1_funct_1(A,B) = f2_s3_funct_1(B) ) ) ), file(funct_1,s3_funct_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(t68_card_2,theorem,( ! [A,B] : ( v1_finset_1(B) => ( ( ~ r1_tarski(k1_card_1(A),k1_card_1(B)) & ~ r2_hidden(k1_card_1(A),k1_card_1(B)) ) | v1_finset_1(A) ) ) ), file(card_2,t68_card_2), [interesting(0.00)]). fof(t186_group_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_finset_1(B) => ~ ( ! [C] : ~ ( r2_hidden(C,B) & ! [D] : ( v1_finset_1(D) => ~ ( D = C & k4_card_1(D) = A & ! [E] : ( r2_hidden(E,B) => ( C = E | ( r2_wellord2(C,E) & r1_xboole_0(C,E) ) ) ) ) ) ) & ! [C] : ( v1_finset_1(C) => ~ ( C = k3_tarski(B) & k4_card_1(C) = k2_nat_1(A,k4_card_1(B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l199_group_2]), [file(group_2,t186_group_2),interesting(0.00)]). fof(t18_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k2_group_2(A,B,k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),C,D)),k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k2_group_2(A,B,C),k2_group_2(A,B,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d3_xboole_0]), [file(group_2,t18_group_2),interesting(0.00)]). fof(t19_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k2_group_2(A,k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),B,C),D),k3_finsub_1(k1_zfmisc_1(u1_struct_0(A)),k2_group_2(A,B,D),k2_group_2(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_xboole_0,d3_xboole_0]), [file(group_2,t19_group_2),interesting(0.00)]). fof(t1_group_2,theorem,( $true ), file(group_2,t1_group_2), [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(t23_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_group_2(A,k6_domain_1(u1_struct_0(A),B),k7_domain_1(u1_struct_0(A),C,D)) = k7_domain_1(u1_struct_0(A),k1_group_1(A,B,C),k1_group_1(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_tarski,d2_tarski,d2_tarski,d10_xboole_0,d3_tarski,d1_tarski,d2_tarski]), [file(group_2,t23_group_2),interesting(0.00)]). fof(t24_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_group_2(A,k7_domain_1(u1_struct_0(A),B,C),k6_domain_1(u1_struct_0(A),D)) = k7_domain_1(u1_struct_0(A),k1_group_1(A,B,D),k1_group_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d1_tarski,d2_tarski,d2_tarski,d10_xboole_0,d3_tarski,d1_tarski,d2_tarski]), [file(group_2,t24_group_2),interesting(0.00)]). fof(d2_enumset1,definition,( ! [A,B,C,D,E] : ( E = k2_enumset1(A,B,C,D) <=> ! [F] : ( r2_hidden(F,E) <=> ~ ( F != A & F != B & F != C & F != D ) ) ) ), file(enumset1,d2_enumset1), [interesting(0.00)]). fof(t25_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k2_group_2(A,k7_domain_1(u1_struct_0(A),B,C),k7_domain_1(u1_struct_0(A),D,E)) = k9_domain_1(u1_struct_0(A),k1_group_1(A,B,D),k1_group_1(A,B,E),k1_group_1(A,C,D),k1_group_1(A,C,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d2_tarski,d2_enumset1,d10_xboole_0,d3_tarski,d2_enumset1,d2_tarski]), [file(group_2,t25_group_2),interesting(0.00)]). fof(t28_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r2_hidden(D,B) & r2_hidden(E,C) ) => k1_group_1(A,D,E) = k1_group_1(A,E,D) ) ) ) => k2_group_2(A,B,C) = k2_group_2(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,d3_tarski]), [file(group_2,t28_group_2),interesting(0.00)]). fof(t2_group_2,theorem,( $true ), file(group_2,t2_group_2), [interesting(0.00)]). fof(t94_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k3_group_1(A,k10_group_1(A,B,C)) = k10_group_1(A,k3_group_1(A,B),k3_group_1(A,C)) ) ) ) ), file(group_1,t94_group_1), [interesting(0.00)]). fof(t30_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => k1_group_2(A,k2_group_2(A,B,C)) = k2_group_2(A,k1_group_2(A,B),k1_group_2(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t94_group_1,d10_xboole_0,d3_tarski,t94_group_1]), [file(group_2,t30_group_2),interesting(0.00)]). fof(t31_group_2,theorem,( $true ), file(group_2,t31_group_2), [interesting(0.00)]). fof(t32_group_2,theorem,( $true ), file(group_2,t32_group_2), [interesting(0.00)]). fof(t35_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( v4_group_1(A) => k2_group_2(A,k3_group_2(A,D,B),C) = k3_group_2(A,D,k2_group_2(A,B,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t35_group_2),interesting(0.00)]). fof(t36_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( v4_group_1(A) => k2_group_2(A,k4_group_2(A,D,B),C) = k2_group_2(A,B,k3_group_2(A,D,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t36_group_2),interesting(0.00)]). fof(t37_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( v4_group_1(A) => k4_group_2(A,D,k2_group_2(A,B,C)) = k2_group_2(A,B,k4_group_2(A,D,C)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_2]), [file(group_2,t37_group_2),interesting(0.00)]). fof(t12_group_2,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & l1_group_1(B) ) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,k2_group_2(B,C,D)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & ? [F] : ( m1_subset_1(F,u1_struct_0(B)) & A = k1_group_1(B,E,F) & r2_hidden(E,C) & r2_hidden(F,D) ) ) ) ) ) ) ), file(group_2,t12_group_2), [interesting(0.00)]). fof(t20_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( k2_group_2(A,k1_subset_1(u1_struct_0(A)),B) = k1_xboole_0 & k2_group_2(A,B,k1_subset_1(u1_struct_0(A))) = k1_xboole_0 ) ) ) ), inference(mizar_proof,[status(thm)],[t12_group_2,t12_group_2]), [file(group_2,t20_group_2),interesting(0.00)]). fof(t45_group_2,theorem,( $true ), file(group_2,t45_group_2), [interesting(0.00)]). fof(t46_group_2,theorem,( $true ), file(group_2,t46_group_2), [interesting(0.00)]). fof(t47_group_2,theorem,( $true ), file(group_2,t47_group_2), [interesting(0.00)]). fof(t4_group_2,theorem,( $true ), file(group_2,t4_group_2), [interesting(0.00)]). fof(d7_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A)) & m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) ) => ( B = k4_group_1(A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k8_funct_2(u1_struct_0(A),u1_struct_0(A),B,C) = k3_group_1(A,C) ) ) ) ) ), file(group_1,d7_group_1), [interesting(0.00)]). fof(t68_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( B = k7_relat_1(C,A) <=> ( k1_relat_1(B) = k3_xboole_0(k1_relat_1(C),A) & ! [D] : ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) ) ) ), file(funct_1,t68_funct_1), [interesting(0.00)]). fof(d16_group_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ( v7_group_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_group_1(A,B,C) = k1_group_1(A,C,B) ) ) ) ) ), file(group_1,d16_group_1), [interesting(0.00)]). fof(t72_group_2,theorem,( $true ), file(group_2,t72_group_2), [interesting(0.00)]). fof(t73_group_2,theorem,( $true ), file(group_2,t73_group_2), [interesting(0.00)]). fof(t74_group_2,theorem,( $true ), file(group_2,t74_group_2), [interesting(0.00)]). fof(t78_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => m1_group_2(B,k6_group_2(A)) ) ) ), file(group_2,t78_group_2), [interesting(0.00)]). fof(t79_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => m1_group_2(A,k6_group_2(A)) ) ), file(group_2,t79_group_2), [interesting(0.00)]). fof(t7_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_group_2(A,k7_domain_1(u1_struct_0(A),B,C)) = k7_domain_1(u1_struct_0(A),k3_group_1(A,B),k3_group_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d2_tarski,d2_tarski,d10_xboole_0,d3_tarski,d2_tarski]), [file(group_2,t7_group_2),interesting(0.00)]). fof(t27_card_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => r1_tarski(k1_card_1(A),k1_card_1(B)) ) ), file(card_1,t27_card_1), [interesting(0.00)]). fof(t80_card_1,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r1_tarski(A,B) => r1_xreal_0(k4_card_1(A),k4_card_1(B)) ) ) ) ), file(card_1,t80_card_1), [interesting(0.00)]). fof(d8_xboole_0,definition,( ! [A,B] : ( r2_xboole_0(A,B) <=> ( r1_tarski(A,B) & A != B ) ) ), file(xboole_0,d8_xboole_0), [interesting(0.00)]). fof(t67_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ! [B] : ( v1_finset_1(B) => ( r2_xboole_0(A,B) => ( ~ r1_xreal_0(k4_card_1(B),k4_card_1(A)) & r2_hidden(k1_card_1(A),k1_card_1(B)) ) ) ) ) ), file(card_2,t67_card_2), [interesting(0.00)]). fof(t86_group_2,theorem,( $true ), file(group_2,t86_group_2), [interesting(0.00)]). fof(t87_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => k7_group_2(A,B) != k1_xboole_0 ) ) ), file(group_2,t87_group_2), [interesting(0.00)]). fof(t2_xboole_1,theorem,( ! [A] : r1_tarski(k1_xboole_0,A) ), file(xboole_1,t2_xboole_1), [interesting(0.00)]). fof(t89_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_group_2(D,A) => ( ( r2_hidden(B,k7_group_2(A,D)) & r2_hidden(C,k7_group_2(A,D)) ) => r2_hidden(k1_group_1(A,B,C),k7_group_2(A,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_group_2,t59_group_2,t88_group_2]), [file(group_2,t89_group_2),interesting(0.00)]). fof(t26_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( ( ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( r2_hidden(C,B) & r2_hidden(D,B) ) => r2_hidden(k1_group_1(A,C,D),B) ) ) ) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_hidden(C,B) => r2_hidden(k3_group_1(A,C),B) ) ) ) => k2_group_2(A,B,B) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d10_xboole_0,d3_tarski,d5_group_1,d6_group_1]), [file(group_2,t26_group_2),interesting(0.00)]). fof(t13_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_group_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( ( B != k1_xboole_0 & C != k1_xboole_0 ) <=> k2_group_2(A,B,C) != k1_xboole_0 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d3_tarski,t12_group_2]), [file(group_2,t13_group_2),interesting(0.00)]). fof(t93_group_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( m1_group_2(B,A) => ! [C] : ( m1_group_2(C,A) => ( ~ ( k2_group_2(A,k7_group_2(A,B),k7_group_2(A,C)) = k2_group_2(A,k7_group_2(A,C),k7_group_2(A,B)) & ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => u1_struct_0(D) != k2_group_2(A,k7_group_2(A,B),k7_group_2(A,C)) ) ) & ( ? [D] : ( m1_group_2(D,A) & u1_struct_0(D) = k2_group_2(A,k7_group_2(A,B),k7_group_2(A,C)) ) => k2_group_2(A,k7_group_2(A,B),k7_group_2(A,C)) = k2_group_2(A,k7_group_2(A,C),k7_group_2(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_group_2,d4_group_1,d4_group_1,d4_group_1,d4_group_1,t89_group_2,t25_group_1,t90_group_2,t61_group_2,d3_tarski,t90_group_2,t19_group_1,t25_group_1,t90_group_2,d10_xboole_0,d3_tarski,t90_group_2,t25_group_1,t90_group_2,t19_group_1]), [file(group_2,t93_group_2),interesting(0.00)]). fof(t95_group_2,theorem,( $true ), file(group_2,t95_group_2), [interesting(0.00)]). fof(t96_group_2,theorem,( $true ), file(group_2,t96_group_2), [interesting(0.00)]).