fof(t157_group_3,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_card_1(k7_group_3(A,B)) = k16_group_2(A,k10_group_3(A,k6_domain_1(u1_struct_0(A),B))) ) ) ), inference(mizar_proof,[status(thm)],[s3_funct_1,d3_tarski,d5_funct_1,t118_group_3,d10_xboole_0,d3_tarski,t118_group_3,d5_funct_1,d8_funct_1,t6_zfmisc_1,d4_wellord2,t21_card_1,t155_group_3]), [file(group_3,t157_group_3),interesting(1.00)]). fof(t118_group_3,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)) => k8_group_3(A,k6_domain_1(u1_struct_0(A),B)) = a_2_2_group_3(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t104_group_3,t44_group_3,t88_group_3,t96_group_3,d10_xboole_0,d3_tarski,t96_group_3,t108_group_3]), [file(group_3,t118_group_3),interesting(0.94)]). fof(t137_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( v1_group_3(k5_group_2(A),A) & v1_group_3(k6_group_2(A),A) ) ) ), inference(mizar_proof,[status(thm)],[t80_group_3,d13_group_3,t82_group_3,d13_group_3]), [file(group_3,t137_group_3),interesting(0.89)]). fof(t19_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( v6_group_1(A) => v1_finset_1(k1_group_3(A)) ) ) ), inference(mizar_proof,[status(thm)],[d1_group_3,s2_funct_1,d3_tarski,d5_funct_1,d5_group_2,d8_funct_1,t68_group_2,t26_card_1,d14_group_1,t24_finset_1,t68_card_2]), [file(group_3,t19_group_3),interesting(0.84)]). fof(t164_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k11_group_3(A,k5_group_2(A)) = A ) ), inference(mizar_proof,[status(thm)],[t137_group_3,t163_group_3]), [file(group_3,t164_group_3),interesting(0.83)]). fof(t165_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k11_group_3(A,k6_group_2(A)) = A ) ), inference(mizar_proof,[status(thm)],[t137_group_3,t163_group_3]), [file(group_3,t165_group_3),interesting(0.83)]). fof(t92_group_3,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)) => ( ( r2_group_3(A,B,k2_group_1(A)) | r2_group_3(A,k2_group_1(A),B) ) => B = k2_group_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_group_3,t23_group_3,d7_group_3,t23_group_3]), [file(group_3,t92_group_3),interesting(0.82)]). fof(t150_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_3(B,A) & m1_group_2(B,A) ) => k14_group_2(A,B) = k15_group_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d15_group_2,t140_group_3,d16_group_2,d10_xboole_0,d3_tarski,d16_group_2,t140_group_3,d15_group_2]), [file(group_3,t150_group_3),interesting(0.82)]). fof(t84_group_3,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) => k16_group_2(A,C) = k16_group_2(A,k6_group_3(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t71_group_3,t39_group_2,t38_group_2,t38_group_2,d6_group_1,t43_group_2,t38_group_2,t38_group_2,t43_group_2,d6_group_1,t38_group_2,t38_group_2,t39_group_2,t71_group_3,d15_group_2,s2_funct_1,d3_tarski,d5_funct_1,d15_group_2,d10_xboole_0,d3_tarski,d15_group_2,t30_group_3,d15_group_2,d5_funct_1,d8_funct_1,t137_group_2,t32_group_3,t28_group_3,t70_group_3,t21_group_3,t137_group_2,d4_wellord2,t21_card_1]), [file(group_3,t84_group_3),interesting(0.82)]). fof(t108_group_3,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)) => ( r4_group_3(A,k6_domain_1(u1_struct_0(A),B),k6_domain_1(u1_struct_0(A),C)) <=> r2_group_3(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t104_group_3,t44_group_3,t6_zfmisc_1,t88_group_3,t88_group_3,t44_group_3,t104_group_3]), [file(group_3,t108_group_3),interesting(0.79)]). fof(t129_group_3,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] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => r2_hidden(k6_group_3(A,C,B),k9_group_3(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t121_group_3,d12_group_3]), [file(group_3,t129_group_3),interesting(0.78)]). fof(t122_group_3,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) ) => r5_group_3(A,B,B) ) ) ), inference(mizar_proof,[status(thm)],[d11_group_3,t73_group_3]), [file(group_3,t122_group_3),interesting(0.76)]). fof(t142_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_tarski(k13_group_2(A,B,C),k12_group_2(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t140_group_3,t5_group_3,t127_group_2,d6_group_1,t132_group_2,t128_group_2,t5_group_3,t40_group_2,d6_group_1,t43_group_2,d10_xboole_0,t140_group_3]), [file(group_3,t142_group_3),interesting(0.76)]). fof(t141_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_tarski(k12_group_2(A,B,C),k13_group_2(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t140_group_3,t5_group_3,t127_group_2,d6_group_1,t132_group_2,t128_group_2,t5_group_3,t40_group_2,d6_group_1,t43_group_2,d10_xboole_0,t140_group_3]), [file(group_3,t141_group_3),interesting(0.76)]). fof(t155_group_3,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))) => k1_card_1(k8_group_3(A,B)) = k16_group_2(A,k10_group_3(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t63_group_3,t56_group_3,t154_group_3,t143_group_2,t104_group_3,s2_funct_1,d3_tarski,d5_funct_1,d16_group_2,d10_xboole_0,d3_tarski,d16_group_2,t104_group_3,d5_funct_1,d8_funct_1,t143_group_2,t154_group_3,t56_group_3,t63_group_3,d4_wellord2,t21_card_1,t175_group_2]), [file(group_3,t155_group_3),interesting(0.76)]). fof(t82_group_3,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)) => r1_group_2(A,k6_group_3(A,k6_group_2(A),B),k6_group_2(A)) ) ) ), inference(mizar_proof,[status(thm)],[d6_group_2,t29_group_3,d6_group_1,t24_group_3,d1_rlvect_1,t70_group_3,d1_rlvect_1]), [file(group_3,t82_group_3),interesting(0.76)]). fof(t97_group_3,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)) => r2_hidden(k2_group_3(A,B,C),k7_group_3(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t88_group_3,t95_group_3]), [file(group_3,t97_group_3),interesting(0.75)]). fof(t25_group_3,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)) => k2_group_3(A,B,B) = B ) ) ), inference(mizar_proof,[status(thm)],[d6_group_1,d5_group_1]), [file(group_3,t25_group_3),interesting(0.73)]). fof(t123_group_3,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) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r5_group_3(A,B,C) => r5_group_3(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_group_3,t74_group_3,d11_group_3]), [file(group_3,t123_group_3),interesting(0.73)]). fof(t146_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> k9_group_3(A,B) = k1_tarski(B) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d12_group_3,t121_group_3,d13_group_3,d1_tarski,d10_xboole_0,t130_group_3,t37_zfmisc_1,d13_group_3,t129_group_3,d1_tarski]), [file(group_3,t146_group_3),interesting(0.72)]). fof(t80_group_3,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)) => r1_group_2(A,k6_group_3(A,k5_group_2(A),B),k5_group_2(A)) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_2,d6_group_3,t44_group_3,t22_group_3,d7_group_2]), [file(group_3,t80_group_3),interesting(0.72)]). fof(t89_group_3,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)) => r1_group_3(A,B,B) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_3,t24_group_3]), [file(group_3,t89_group_3),interesting(0.71)]). fof(t88_group_3,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)) => ( r1_group_3(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & C = k2_group_3(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_3,t30_group_3,t30_group_3,d7_group_3]), [file(group_3,t88_group_3),interesting(0.70)]). fof(t124_group_3,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) ) => ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => ( ( r6_group_3(A,C,D) & r5_group_3(A,D,B) ) => r5_group_3(A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_group_3,d11_group_3,t72_group_3,d11_group_3]), [file(group_3,t124_group_3),interesting(0.70)]). fof(t140_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k12_group_2(A,B,C) = k13_group_2(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_group_3,t71_group_3,t39_group_2,t127_group_2,d6_group_1,t128_group_2,t43_group_2,d13_group_3,t71_group_3,t129_group_2,d6_group_1,t132_group_2,t68_group_2]), [file(group_3,t140_group_3),interesting(0.70)]). fof(t121_group_3,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) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r5_group_3(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & r1_group_2(A,C,k6_group_3(A,B,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_group_3,t74_group_3,t74_group_3,d11_group_3]), [file(group_3,t121_group_3),interesting(0.70)]). fof(t78_group_3,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) <=> v6_group_1(k6_group_3(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t77_group_3,t21_card_1,t68_card_1,d14_group_1]), [file(group_3,t78_group_3),interesting(0.70)]). fof(t90_group_3,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)) => ( r1_group_3(A,B,C) => r1_group_3(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_3,t30_group_3,d7_group_3]), [file(group_3,t90_group_3),interesting(0.70)]). fof(t91_group_3,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)) => ( ( r2_group_3(A,B,C) & r2_group_3(A,C,D) ) => r2_group_3(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_group_3,d7_group_3,t29_group_3,d7_group_3]), [file(group_3,t91_group_3),interesting(0.68)]). fof(t105_group_3,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))) => r3_group_3(A,B,B) ) ) ), inference(mizar_proof,[status(thm)],[d9_group_3,t61_group_3]), [file(group_3,t105_group_3),interesting(0.68)]). fof(t144_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => m1_group_2(B,k6_group_3(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_group_3,t63_group_2,t71_group_3,t40_group_2,d6_group_1,t43_group_2,t19_group_1,t6_group_3,t142_group_3]), [file(group_3,t144_group_3),interesting(0.68)]). fof(t145_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => m1_group_2(k6_group_3(A,B,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_group_3,t63_group_2,t71_group_3,t40_group_2,d6_group_1,t43_group_2,t19_group_1,t6_group_3,t141_group_3]), [file(group_3,t145_group_3),interesting(0.68)]). fof(t151_group_3,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)) & k17_group_2(A,B) = 2 ) => ( v1_group_3(B,A) & m1_group_2(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t176_group_2,t176_group_2,t79_card_2,t79_card_2,t165_group_2,d2_tarski,d2_tarski,t167_group_2,t93_zfmisc_1,d2_tarski,d15_group_2,t132_group_2,t138_group_2,t69_enumset1,t8_zfmisc_1,t88_xboole_1,t93_zfmisc_1,d2_tarski,d16_group_2,t132_group_2,t144_group_2,t69_enumset1,t8_zfmisc_1,t136_group_2,t142_group_2,t136_group_2,t142_group_2,d15_group_2,d16_group_2,d2_tarski,t88_xboole_1,t140_group_3]), [file(group_3,t151_group_3),interesting(0.68)]). fof(t133_group_3,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(k9_group_3(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_group_3,t13_finset_1]), [file(group_3,t133_group_3),interesting(0.67)]). fof(t163_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> k11_group_3(A,B) = A ) ) ) ), inference(mizar_proof,[status(thm)],[d13_group_3,t160_group_3,t71_group_2,d13_group_3,d1_rlvect_1,t160_group_3]), [file(group_3,t163_group_3),interesting(0.67)]). fof(t3_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => v7_group_1(k5_group_2(A)) ) ), inference(mizar_proof,[status(thm)],[d16_group_1,d7_group_2,d1_tarski]), [file(group_3,t3_group_3),interesting(0.67)]). fof(t73_group_3,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,k6_group_3(A,B,k2_group_1(A)),B) ) ) ), inference(mizar_proof,[status(thm)],[d6_group_3,t61_group_3,t68_group_2]), [file(group_3,t73_group_3),interesting(0.66)]). fof(t130_group_3,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) ) => r2_hidden(B,k9_group_3(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d12_group_3]), [file(group_3,t130_group_3),interesting(0.66)]). fof(t134_group_3,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) ) => ( r5_group_3(A,C,B) <=> r4_group_3(A,k7_group_2(A,C),k7_group_2(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_group_3,d6_group_3,d9_group_3,d9_group_3,d6_group_3,t68_group_2,d11_group_3]), [file(group_3,t134_group_3),interesting(0.66)]). fof(t77_group_3,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) = k8_group_1(k6_group_3(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[s4_funct_2,d1_funct_2,d5_group_2,t91_relat_1,d3_tarski,d5_funct_1,t91_relat_1,t51_group_2,t70_funct_1,t50_group_3,d6_group_3,d10_xboole_0,d3_tarski,d6_group_3,t50_group_3,t70_funct_1,d5_funct_1,d8_funct_1,t91_relat_1,t51_group_2,t70_funct_1,t21_group_3,d4_wellord2,t21_card_1]), [file(group_3,t77_group_3),interesting(0.66)]). fof(t26_group_3,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)) => ( k2_group_3(A,B,k3_group_1(A,B)) = B & k2_group_3(A,k3_group_1(A,B),B) = k3_group_1(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_group_1,t1_group_3,t1_group_3]), [file(group_3,t26_group_3),interesting(0.65)]). fof(t106_group_3,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))) => ( r3_group_3(A,B,C) => r3_group_3(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_group_3,t63_group_3,d9_group_3]), [file(group_3,t106_group_3),interesting(0.65)]). fof(t24_group_3,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)) => k2_group_3(A,B,k2_group_1(A)) = B ) ) ), inference(mizar_proof,[status(thm)],[t20_group_3,d5_group_1,t16_group_1,d5_group_1]), [file(group_3,t24_group_3),interesting(0.64)]). fof(t101_group_3,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)) => ( k7_group_3(A,B) = k6_domain_1(u1_struct_0(A),k2_group_1(A)) <=> B = k2_group_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t96_group_3,d1_tarski,d3_tarski,t95_group_3,t92_group_3,d1_tarski,d10_xboole_0,t96_group_3,t37_zfmisc_1]), [file(group_3,t101_group_3),interesting(0.64)]). fof(t127_group_3,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,k9_group_3(B,C)) => ( v1_group_1(A) & m1_group_2(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_group_3]), [file(group_3,t127_group_3),interesting(0.64)]). fof(t114_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => r2_hidden(k4_group_3(A,C,B),k8_group_3(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t104_group_3]), [file(group_3,t114_group_3),interesting(0.63)]). fof(t61_group_3,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))) => k4_group_3(A,B,k2_group_1(A)) = B ) ) ), inference(mizar_proof,[status(thm)],[t59_group_3,t43_group_2,t16_group_1,t43_group_2]), [file(group_3,t61_group_3),interesting(0.62)]). fof(t96_group_3,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)) => ( r2_hidden(B,k7_group_3(A,C)) <=> r2_group_3(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t95_group_3,t95_group_3]), [file(group_3,t96_group_3),interesting(0.61)]). fof(t143_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => k10_group_2(A,B,C) = k11_group_2(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t114_group_2,t125_group_2,t140_group_3,t126_group_2,t115_group_2,d10_xboole_0,d3_tarski,t115_group_2,t126_group_2,t140_group_3,t125_group_2,t114_group_2,t140_group_3]), [file(group_3,t143_group_3),interesting(0.61)]). fof(t23_group_3,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)) => ( k2_group_3(A,B,C) = k2_group_1(A) => B = k2_group_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_group_1,t15_group_1]), [file(group_3,t23_group_3),interesting(0.60)]). fof(t27_group_3,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)) => ( k2_group_3(A,B,C) = B <=> k1_group_1(A,B,C) = k1_group_1(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_group_3,t21_group_1,t21_group_1,t20_group_3]), [file(group_3,t27_group_3),interesting(0.60)]). fof(t79_group_3,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) => k9_group_1(C) = k9_group_1(k6_group_3(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t78_group_3,d15_group_1,d15_group_1,t77_group_3]), [file(group_3,t79_group_3),interesting(0.60)]). fof(t21_group_3,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)) => ( k2_group_3(A,B,C) = k2_group_3(A,D,C) => B = D ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_group_1,t14_group_1]), [file(group_3,t21_group_3),interesting(0.59)]). fof(t22_group_3,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)) => k2_group_3(A,k2_group_1(A),B) = k2_group_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_1,d6_group_1]), [file(group_3,t22_group_3),interesting(0.59)]). fof(t18_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v1_group_1(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => r2_hidden(A,k1_group_3(A)) ) ), inference(mizar_proof,[status(thm)],[t63_group_2,d1_group_3]), [file(group_3,t18_group_3),interesting(0.59)]). fof(t76_group_3,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) => r1_group_2(A,k6_group_3(A,k9_group_2(A,C,D),B),k9_group_2(A,k6_group_3(A,C,B),k6_group_3(A,D,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_group_2,t70_group_3,t99_group_2,t70_group_3,t99_group_2,t99_group_2,t70_group_3,t99_group_2,t70_group_3,t21_group_3,t99_group_2,t70_group_3]), [file(group_3,t76_group_3),interesting(0.58)]). fof(t139_group_3,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) ) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => v1_group_3(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t86_group_3,d13_group_3]), [file(group_3,t139_group_3),interesting(0.58)]). fof(t32_group_3,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)) => k2_group_3(A,k3_group_1(A,B),C) = k3_group_1(A,k2_group_3(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_group_1,t19_group_1,t25_group_1,t20_group_3]), [file(group_3,t32_group_3),interesting(0.58)]). fof(t102_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => k2_group_2(A,k7_group_3(A,B),C) = k2_group_2(A,C,k7_group_3(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t96_group_3,d7_group_3,t19_group_1,d4_group_1,t1_group_3,t30_group_3,t28_group_3,t25_group_3,t29_group_3,t97_group_3,d10_xboole_0,d3_tarski,t96_group_3,d7_group_3,t1_group_3,t30_group_3,t28_group_3,t29_group_3,t26_group_3,t97_group_3]), [file(group_3,t102_group_3),interesting(0.57)]). fof(t128_group_3,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) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r2_hidden(B,k9_group_3(A,C)) <=> r6_group_3(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_group_3,d12_group_3]), [file(group_3,t128_group_3),interesting(0.57)]). fof(t158_group_3,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)) => ~ ( ( v1_finset_1(k7_group_3(A,B)) | v1_finset_1(k14_group_2(A,k10_group_3(A,k6_domain_1(u1_struct_0(A),B)))) ) & ! [C] : ( v1_finset_1(C) => ~ ( C = k7_group_3(A,B) & k4_card_1(C) = k17_group_2(A,k10_group_3(A,k6_domain_1(u1_struct_0(A),B))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t157_group_3,t21_card_1,t68_card_1,d18_group_2,t68_card_1]), [file(group_3,t158_group_3),interesting(0.56)]). fof(t36_group_3,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)) => k2_group_3(A,B,C) = B ) ) => v7_group_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d16_group_1,t27_group_3]), [file(group_3,t36_group_3),interesting(0.56)]). fof(t98_group_3,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)) => r2_hidden(B,k7_group_3(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t96_group_3]), [file(group_3,t98_group_3),interesting(0.56)]). fof(t95_group_3,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)) => ( r2_hidden(A,k7_group_3(B,C)) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(B)) & D = A & r2_group_3(B,C,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t93_group_3,t93_group_3]), [file(group_3,t95_group_3),interesting(0.55)]). fof(t85_group_3,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) => ( v1_finset_1(k14_group_2(A,C)) => k17_group_2(A,C) = k17_group_2(A,k6_group_3(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d18_group_2,t84_group_3,t21_card_1,t68_card_1,d18_group_2]), [file(group_3,t85_group_3),interesting(0.55)]). fof(t138_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & v1_group_3(B,A) & m1_group_2(B,A) ) => ! [C] : ( ( v1_group_1(C) & v1_group_3(C,A) & m1_group_2(C,A) ) => v1_group_3(k9_group_2(A,B,C),A) ) ) ) ), inference(mizar_proof,[status(thm)],[d13_group_3,t76_group_3,d13_group_3,d13_group_3]), [file(group_3,t138_group_3),interesting(0.54)]). fof(t93_group_3,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)) => k5_group_3(A,k7_group_2(A,k6_group_2(A)),B) = a_2_0_group_3(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t51_group_3,d7_group_3,d10_xboole_0,d3_tarski,d7_group_3,t51_group_3]), [file(group_3,t93_group_3),interesting(0.53)]). fof(t161_group_3,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) ) => k1_card_1(k9_group_3(A,B)) = k16_group_2(A,k11_group_3(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d1_group_3,s2_funct_1,d3_tarski,d5_funct_1,t128_group_3,t134_group_3,d10_xboole_0,d3_tarski,t109_group_3,t134_group_3,t128_group_3,d5_funct_1,d8_funct_1,t68_group_2,d4_wellord2,t21_card_1,t155_group_3]), [file(group_3,t161_group_3),interesting(0.51)]). fof(t100_group_3,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)) => ( k7_group_3(A,B) = k7_group_3(A,C) <=> ~ r1_xboole_0(k7_group_3(A,B),k7_group_3(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t96_group_3,t3_xboole_0,t3_xboole_0,d3_tarski,t95_group_3,t96_group_3,t91_group_3,t91_group_3,t95_group_3,d10_xboole_0,d3_tarski,t95_group_3,t96_group_3,t91_group_3,t91_group_3,t95_group_3]), [file(group_3,t100_group_3),interesting(0.50)]). fof(t72_group_3,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_group_2(A,k6_group_3(A,k6_group_3(A,D,B),C),k6_group_3(A,D,k1_group_1(A,B,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_group_3,d6_group_3,t56_group_3,d6_group_3,t68_group_2]), [file(group_3,t72_group_3),interesting(0.50)]). fof(l38_group_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [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_subset_1(D,u1_struct_0(B)) => k2_group_3(B,k6_group_1(B,A,C),D) = k6_group_1(B,A,k2_group_3(B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l36_group_3,l37_group_3,s1_nat_1]), [file(group_3,l38_group_3),interesting(0.50)]). fof(t132_group_3,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) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( k9_group_3(A,B) = k9_group_3(A,C) <=> ~ r1_xboole_0(k9_group_3(A,B),k9_group_3(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t130_group_3,t3_xboole_0,t3_xboole_0,t127_group_3,d3_tarski,d12_group_3,t128_group_3,t124_group_3,t124_group_3,d12_group_3,d10_xboole_0,d3_tarski,d12_group_3,t128_group_3,t124_group_3,t124_group_3,d12_group_3]), [file(group_3,t132_group_3),interesting(0.49)]). fof(t59_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => k4_group_3(A,C,B) = k4_group_2(A,B,k3_group_2(A,k3_group_1(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t40_group_3,t6_group_2,d10_xboole_0,d3_tarski,t34_group_2,t33_group_2,t50_group_3]), [file(group_3,t59_group_3),interesting(0.48)]). fof(t71_group_3,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) => u1_struct_0(k6_group_3(A,C,B)) = k4_group_2(A,B,k12_group_2(A,C,k3_group_1(A,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_group_3,t59_group_3]), [file(group_3,t71_group_3),interesting(0.47)]). fof(t2_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) <=> v1_binop_1(u1_group_1(A),u1_struct_0(A)) ) ) ), inference(mizar_proof,[status(thm)],[d13_binop_1,l2_group_3,d16_group_1,d2_binop_1]), [file(group_3,t2_group_3),interesting(0.47)]). fof(t34_group_3,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] : ( v1_int_1(D) => k2_group_3(A,k6_group_1(A,D,B),C) = k6_group_1(A,D,k2_group_3(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_absvalue,l38_group_3,t56_group_1,t32_group_3,l38_group_3,t56_group_1]), [file(group_3,t34_group_3),interesting(0.47)]). fof(t83_group_3,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] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( k6_group_3(A,C,B) = A => C = A ) ) ) ) ), inference(mizar_proof,[status(thm)],[t70_group_3,t21_group_3,d1_rlvect_1,t71_group_2]), [file(group_3,t83_group_3),interesting(0.47)]). fof(t99_group_3,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)) => ( r2_hidden(B,k7_group_3(A,C)) => r2_hidden(C,k7_group_3(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t96_group_3,t96_group_3]), [file(group_3,t99_group_3),interesting(0.47)]). fof(t70_group_3,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) => ( r1_rlvect_1(k6_group_3(B,D,C),A) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k2_group_3(B,E,C) & r1_rlvect_1(D,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,d6_group_3,t50_group_3,t88_group_2,t88_group_2,t50_group_3,d6_group_3,d1_rlvect_1]), [file(group_3,t70_group_3),interesting(0.45)]). fof(t154_group_3,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))) => ( r1_rlvect_1(k10_group_3(B,C),A) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(B)) & A = D & k4_group_3(B,C,D) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_rlvect_1,d14_group_3,d14_group_3,d1_rlvect_1]), [file(group_3,t154_group_3),interesting(0.45)]). fof(t109_group_3,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) => ~ ( r4_group_3(A,B,k7_group_2(A,C)) & ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => u1_struct_0(D) != B ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_group_3,d6_group_3]), [file(group_3,t109_group_3),interesting(0.45)]). fof(t160_group_3,theorem,( ! [A,B] : ( ( ~ v3_struct_0(B) & v3_group_1(B) & v4_group_1(B) & l1_group_1(B) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,B) ) => ( r1_rlvect_1(k11_group_3(B,C),A) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(B)) & A = D & r1_group_2(B,k6_group_3(B,C,D),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t154_group_3,d6_group_3,t68_group_2,d6_group_3,t154_group_3]), [file(group_3,t160_group_3),interesting(0.45)]). fof(t131_group_3,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) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r2_hidden(B,k9_group_3(A,C)) => r2_hidden(C,k9_group_3(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t128_group_3,t128_group_3]), [file(group_3,t131_group_3),interesting(0.43)]). fof(t147_group_3,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_group_3(B,A) & m1_group_2(B,A) ) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_rlvect_1(B,C) => r1_tarski(k7_group_3(A,C),k7_group_2(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t95_group_3,t88_group_3,t70_group_3,d13_group_3,t88_group_2,d13_group_3,d6_group_2,t70_group_3,t97_group_3,t88_group_2,t97_group_3,t88_group_2,t70_group_3,t30_group_3]), [file(group_3,t147_group_3),interesting(0.43)]). fof(t81_group_3,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] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r1_group_2(A,k6_group_3(A,C,B),k5_group_2(A)) => r1_group_2(A,C,k5_group_2(A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t80_group_2,t81_group_2,t78_group_3,t79_group_3,t82_group_2]), [file(group_3,t81_group_3),interesting(0.42)]). fof(t119_group_3,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))) => ( v6_group_1(A) => v1_finset_1(k8_group_3(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_group_1,t24_finset_1,t13_finset_1]), [file(group_3,t119_group_3),interesting(0.40)]). fof(t10_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k10_group_2(A,D,k4_group_2(A,B,C)) = k2_group_2(A,C,k12_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t116_group_2]), [file(group_3,t10_group_3),interesting(0.37)]). fof(t116_group_3,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))) => ( r2_hidden(B,k8_group_3(A,C)) => r2_hidden(C,k8_group_3(A,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_group_3]), [file(group_3,t116_group_3),interesting(0.35)]). fof(t156_group_3,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))) => ~ ( ( v1_finset_1(k8_group_3(A,B)) | v1_finset_1(k14_group_2(A,k10_group_3(A,B))) ) & ! [C] : ( v1_finset_1(C) => ~ ( C = k8_group_3(A,B) & k4_card_1(C) = k17_group_2(A,k10_group_3(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t155_group_3,t21_card_1,t68_card_1,d18_group_2,t68_card_1]), [file(group_3,t156_group_3),interesting(0.32)]). fof(t33_group_3,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] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_group_3(A,k6_group_1(A,D,B),C) = k6_group_1(A,D,k2_group_3(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l38_group_3]), [file(group_3,t33_group_3),interesting(0.32)]). fof(t67_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(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,u1_struct_0(A)) => ( B != k1_xboole_0 => k5_group_3(A,B,C) = k6_domain_1(u1_struct_0(A),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t65_group_3,t44_group_3,t6_zfmisc_1,t36_group_3]), [file(group_3,t67_group_3),interesting(0.29)]). fof(t62_group_3,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 => k5_group_3(A,B,k2_group_1(A)) = k6_domain_1(u1_struct_0(A),k2_group_1(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t51_group_3,t22_group_3,d1_tarski,d10_xboole_0,d3_tarski,d1_tarski,d3_tarski,t22_group_3,t51_group_3]), [file(group_3,t62_group_3),interesting(0.26)]). fof(t15_group_3,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) => k10_group_2(A,D,k13_group_2(A,C,B)) = k11_group_2(A,C,k12_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_group_3]), [file(group_3,t15_group_3),interesting(0.24)]). fof(t52_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k5_group_3(A,C,B),k2_group_2(A,k4_group_2(A,B,k1_group_2(A,C)),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t51_group_3,t34_group_2]), [file(group_3,t52_group_3),interesting(0.24)]). fof(t13_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k2_group_2(A,k13_group_2(A,D,B),C) = k11_group_2(A,D,k3_group_2(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t118_group_2]), [file(group_3,t13_group_3),interesting(0.16)]). fof(t11_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k2_group_2(A,k12_group_2(A,D,B),C) = k3_group_2(A,B,k11_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t117_group_2]), [file(group_3,t11_group_3),interesting(0.15)]). fof(t12_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k4_group_2(A,B,k10_group_2(A,D,C)) = k2_group_2(A,C,k13_group_2(A,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t117_group_2]), [file(group_3,t12_group_3),interesting(0.15)]). fof(l37_group_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ! [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_subset_1(D,u1_struct_0(B)) => k2_group_3(B,k6_group_1(B,A,C),D) = k6_group_1(B,A,k2_group_3(B,C,D)) ) ) ) => ! [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_subset_1(D,u1_struct_0(B)) => k2_group_3(B,k6_group_1(B,k1_nat_1(A,1),C),D) = k6_group_1(B,k1_nat_1(A,1),k2_group_3(B,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t49_group_1,t28_group_3,t49_group_1]), [file(group_3,l37_group_3),interesting(0.12)]). 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(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t51_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,k5_group_3(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k2_group_3(B,C,E) & r2_hidden(E,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]), [file(group_3,t51_group_3),interesting(0.00)]). fof(d7_group_3,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)) => ( r1_group_3(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & B = k2_group_3(A,C,D) ) ) ) ) ) ), file(group_3,d7_group_3), [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(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(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(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(t29_group_3,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)) => k2_group_3(A,k2_group_3(A,B,C),D) = k2_group_3(A,B,k1_group_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_group_1,d4_group_1,t25_group_1,d4_group_1]), [file(group_3,t29_group_3),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(t20_group_3,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)) => ( k2_group_3(A,B,C) = k1_group_1(A,k1_group_1(A,k3_group_1(A,C),B),C) & k2_group_3(A,B,C) = k1_group_1(A,k3_group_1(A,C),k1_group_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_group_1]), [file(group_3,t20_group_3),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(t16_group_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => k3_group_1(A,k2_group_1(A)) = k2_group_1(A) ) ), file(group_1,t16_group_1), [interesting(0.00)]). fof(t30_group_3,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)) => ( k2_group_3(A,k2_group_3(A,B,C),k3_group_1(A,C)) = B & k2_group_3(A,k2_group_3(A,B,k3_group_1(A,C)),C) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_group_3,d6_group_1,t24_group_3,t29_group_3,d6_group_1,t24_group_3]), [file(group_3,t30_group_3),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(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(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(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(t1_group_3,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,k1_group_1(A,B,C),k3_group_1(A,C)) = B & k1_group_1(A,k1_group_1(A,B,k3_group_1(A,C)),C) = B & k1_group_1(A,k1_group_1(A,k3_group_1(A,C),C),B) = B & k1_group_1(A,k1_group_1(A,C,k3_group_1(A,C)),B) = B & k1_group_1(A,B,k1_group_1(A,C,k3_group_1(A,C))) = B & k1_group_1(A,B,k1_group_1(A,k3_group_1(A,C),C)) = B & k1_group_1(A,k3_group_1(A,C),k1_group_1(A,C,B)) = B & k1_group_1(A,C,k1_group_1(A,k3_group_1(A,C),B)) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_group_1,d6_group_1,d5_group_1,d4_group_1,d6_group_1,d5_group_1,d6_group_1,d5_group_1,d6_group_1,d5_group_1,d4_group_1]), [file(group_3,t1_group_3),interesting(0.00)]). fof(t28_group_3,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)) => k2_group_3(A,k1_group_1(A,B,C),D) = k1_group_1(A,k2_group_3(A,B,D),k2_group_3(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_1,d6_group_1,d4_group_1,d4_group_1,d4_group_1,d4_group_1,d4_group_1]), [file(group_3,t28_group_3),interesting(0.00)]). fof(t103_group_3,theorem,( $true ), file(group_3,t103_group_3), [interesting(0.00)]). fof(d9_group_3,definition,( ! [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))) => ( r3_group_3(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & B = k4_group_3(A,C,D) ) ) ) ) ) ), file(group_3,d9_group_3), [interesting(0.00)]). fof(t40_group_3,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))) => r1_tarski(k3_group_3(A,B,C),k2_group_2(A,k2_group_2(A,k1_group_2(A,C),B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski]), [file(group_3,t40_group_3),interesting(0.00)]). 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)) ) ) ), file(group_2,t6_group_2), [interesting(0.00)]). 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) ) ) ) ) ) ), file(group_2,t34_group_2), [interesting(0.00)]). 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) ) ) ) ) ) ), file(group_2,t33_group_2), [interesting(0.00)]). fof(t50_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,k4_group_3(B,D,C)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & A = k2_group_3(B,E,C) & r2_hidden(E,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]), [file(group_3,t50_group_3),interesting(0.00)]). 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 ) ) ) ), file(group_2,t43_group_2), [interesting(0.00)]). fof(t42_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => k3_group_3(A,k3_group_3(A,B,C),D) = k3_group_3(A,B,k2_group_2(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t29_group_3,d10_xboole_0,d3_tarski,t29_group_3]), [file(group_3,t42_group_3),interesting(0.00)]). fof(t54_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => k3_group_3(A,k4_group_3(A,C,B),D) = k3_group_3(A,C,k3_group_2(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t42_group_3]), [file(group_3,t54_group_3),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)) ) ) ) ), file(group_2,t22_group_2), [interesting(0.00)]). fof(t56_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => k4_group_3(A,k4_group_3(A,D,B),C) = k4_group_3(A,D,k1_group_1(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t54_group_3,t22_group_2]), [file(group_3,t56_group_3),interesting(0.00)]). fof(t63_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ( k4_group_3(A,k4_group_3(A,C,B),k3_group_1(A,B)) = C & k4_group_3(A,k4_group_3(A,C,k3_group_1(A,B)),B) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t56_group_3,d6_group_1,t61_group_3,t56_group_3,d6_group_1,t61_group_3]), [file(group_3,t63_group_3),interesting(0.00)]). fof(t110_group_3,theorem,( $true ), file(group_3,t110_group_3), [interesting(0.00)]). fof(t111_group_3,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,k8_group_3(B,C)) <=> ? [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) & A = D & r4_group_3(B,C,D) ) ) ) ) ), file(group_3,t111_group_3), [interesting(0.00)]). fof(t112_group_3,theorem,( $true ), file(group_3,t112_group_3), [interesting(0.00)]). fof(t104_group_3,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))) => ( r3_group_3(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & C = k4_group_3(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_group_3,t63_group_3,t63_group_3,d9_group_3]), [file(group_3,t104_group_3),interesting(0.00)]). fof(t115_group_3,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))) => r2_hidden(B,k8_group_3(A,B)) ) ) ), file(group_3,t115_group_3), [interesting(0.00)]). fof(t113_group_3,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))) => ( r2_hidden(B,k8_group_3(A,C)) <=> r4_group_3(A,B,C) ) ) ) ) ), file(group_3,t113_group_3), [interesting(0.00)]). fof(t107_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( r4_group_3(A,B,C) & r4_group_3(A,C,D) ) => r4_group_3(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_group_3,d9_group_3,t56_group_3,d9_group_3]), [file(group_3,t107_group_3),interesting(0.00)]). fof(t117_group_3,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))) => ( k8_group_3(A,B) = k8_group_3(A,C) <=> ~ r1_xboole_0(k8_group_3(A,B),k8_group_3(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_xboole_0,t3_xboole_0,d3_tarski,t113_group_3,t107_group_3,t107_group_3,d10_xboole_0,d3_tarski,t113_group_3,t107_group_3,t107_group_3]), [file(group_3,t117_group_3),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(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(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(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)) ) ) ) ) ), file(group_2,t117_group_2), [interesting(0.00)]). fof(t120_group_3,theorem,( $true ), file(group_3,t120_group_3), [interesting(0.00)]). fof(d11_group_3,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) => ( r5_group_3(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & g1_group_1(u1_struct_0(B),u1_group_1(B)) = k6_group_3(A,C,D) ) ) ) ) ) ), file(group_3,d11_group_3), [interesting(0.00)]). fof(d6_group_3,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,u1_struct_0(A)) => ! [D] : ( ( v1_group_1(D) & m1_group_2(D,A) ) => ( D = k6_group_3(A,B,C) <=> u1_struct_0(D) = k4_group_3(A,k7_group_2(A,B),C) ) ) ) ) ) ), file(group_3,d6_group_3), [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)) ) ) ) ) ), file(group_2,t68_group_2), [interesting(0.00)]). fof(t74_group_3,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] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r1_group_2(A,k6_group_3(A,k6_group_3(A,C,B),k3_group_1(A,B)),C) & r1_group_2(A,k6_group_3(A,k6_group_3(A,C,k3_group_1(A,B)),B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t72_group_3,d6_group_1,t73_group_3,t72_group_3,d6_group_1,t73_group_3]), [file(group_3,t74_group_3),interesting(0.00)]). fof(t125_group_3,theorem,( $true ), file(group_3,t125_group_3), [interesting(0.00)]). fof(t126_group_3,theorem,( $true ), file(group_3,t126_group_3), [interesting(0.00)]). fof(d12_group_3,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_group_3(A))) => ( C = k9_group_3(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E] : ( v1_group_1(E) & m1_group_2(E,A) & D = E & r5_group_3(A,B,E) ) ) ) ) ) ) ), file(group_3,d12_group_3), [interesting(0.00)]). fof(d1_group_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( B = k1_group_3(A) <=> ! [C] : ( r2_hidden(C,B) <=> ( v1_group_1(C) & m1_group_2(C,A) ) ) ) ) ), file(group_3,d1_group_3), [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(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(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(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(t26_card_1,theorem,( ! [A,B] : ( r1_tarski(k1_card_1(A),k1_card_1(B)) <=> ? [C] : ( v1_relat_1(C) & v1_funct_1(C) & v2_funct_1(C) & k1_relat_1(C) = A & r1_tarski(k2_relat_1(C),B) ) ) ), file(card_1,t26_card_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(t135_group_3,theorem,( $true ), file(group_3,t135_group_3), [interesting(0.00)]). fof(t136_group_3,theorem,( $true ), file(group_3,t136_group_3), [interesting(0.00)]). fof(d13_group_3,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_group_3(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k6_group_3(A,B,C) = g1_group_1(u1_struct_0(B),u1_group_1(B)) ) ) ) ) ), file(group_3,d13_group_3), [interesting(0.00)]). fof(d6_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) ) => ! [C] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( r1_group_2(A,B,C) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_rlvect_1(B,D) <=> r1_rlvect_1(C,D) ) ) ) ) ) ) ), file(group_2,d6_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(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) ) ) ) ), file(group_2,t88_group_2), [interesting(0.00)]). 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) ) ) ) ) ) ), file(group_2,t99_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(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) ) ) ) ) ), file(group_2,t135_group_2), [interesting(0.00)]). 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)) ) ) ) ) ), file(group_2,t129_group_2), [interesting(0.00)]). 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) ) ) ) ), file(group_2,t132_group_2), [interesting(0.00)]). fof(t86_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & m1_group_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_group_2(A,k6_group_3(A,B,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t71_group_3,t135_group_2,t129_group_2,d6_group_1,t132_group_2,t68_group_2]), [file(group_3,t86_group_3),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)) ) ) ) ) ), file(group_2,t118_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) ) ) ) ) ) ) ), file(group_2,t114_group_2), [interesting(0.00)]). 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) ) ) ) ) ) ), file(group_2,t125_group_2), [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)) ) ) ) ) ) ), file(group_2,t39_group_2), [interesting(0.00)]). 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)) ) ) ) ) ), file(group_2,t127_group_2), [interesting(0.00)]). 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)) ) ) ) ) ), file(group_2,t128_group_2), [interesting(0.00)]). 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) ) ) ) ) ) ), file(group_2,t126_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) ) ) ) ) ) ) ), file(group_2,t115_group_2), [interesting(0.00)]). 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) ) ), file(group_2,t63_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) ) ) ) ) ) ), file(group_2,t40_group_2), [interesting(0.00)]). fof(t4_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( r1_tarski(B,C) & r1_tarski(D,E) ) => r1_tarski(k2_group_2(A,B,D),k2_group_2(A,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski]), [file(group_3,t4_group_3),interesting(0.00)]). fof(t5_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( r1_tarski(C,D) => ( r1_tarski(k3_group_2(A,B,C),k3_group_2(A,B,D)) & r1_tarski(k4_group_2(A,B,C),k4_group_2(A,B,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t4_group_3]), [file(group_3,t5_group_3),interesting(0.00)]). fof(t6_group_3,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) => ( m1_group_2(C,D) => ( r1_tarski(k12_group_2(A,C,B),k12_group_2(A,D,B)) & r1_tarski(k13_group_2(A,C,B),k13_group_2(A,D,B)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_group_2,t5_group_3]), [file(group_3,t6_group_3),interesting(0.00)]). fof(l165_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_3(B,A) & m1_group_2(B,A) ) => ! [C] : ( ( v1_group_1(C) & v1_group_3(C,A) & m1_group_2(C,A) ) => r1_tarski(k2_group_2(A,k7_group_2(A,C),k7_group_2(A,B)),k2_group_2(A,k7_group_2(A,B),k7_group_2(A,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t88_group_2,t70_group_3,d13_group_3,t88_group_2,t20_group_3,t1_group_3]), [file(group_3,l165_group_3),interesting(0.00)]). fof(t148_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & v1_group_3(B,A) & m1_group_2(B,A) ) => ! [C] : ( ( v1_group_1(C) & v1_group_3(C,A) & 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[l165_group_3,d10_xboole_0]), [file(group_3,t148_group_3),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)) ) ) ) ) ) ), file(group_2,t93_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)) ) ) ) ) ) ), 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)) ) ) ) ) ) ), 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)) ) ) ) ) ) ), file(group_2,t37_group_2), [interesting(0.00)]). fof(t149_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(A) ) => ! [B] : ( ( v1_group_1(B) & v1_group_3(B,A) & m1_group_2(B,A) ) => ! [C] : ( ( v1_group_1(C) & v1_group_3(C,A) & m1_group_2(C,A) ) => ? [D] : ( v1_group_1(D) & v1_group_3(D,A) & 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)],[t148_group_3,t93_group_2,t35_group_2,t140_group_3,t36_group_2,t140_group_3,t37_group_2,t140_group_3]), [file(group_3,t149_group_3),interesting(0.00)]). fof(t14_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k4_group_2(A,B,k11_group_2(A,D,C)) = k11_group_2(A,D,k4_group_2(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t118_group_2]), [file(group_3,t14_group_3),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(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) ) ) ) ) ) ), file(group_2,t176_group_2), [interesting(0.00)]). fof(t79_card_2,theorem,( ! [A] : ( v1_finset_1(A) => ~ ( k4_card_1(A) = 2 & ! [B,C] : ~ ( B != C & A = k2_tarski(B,C) ) ) ) ), file(card_2,t79_card_2), [interesting(0.00)]). 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)) ) ) ) ), file(group_2,t165_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(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) ) ) ) ), file(group_2,t167_group_2), [interesting(0.00)]). fof(t93_zfmisc_1,theorem,( ! [A,B] : k3_tarski(k2_tarski(A,B)) = k2_xboole_0(A,B) ), file(zfmisc_1,t93_zfmisc_1), [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)) ) ) ) ) ) ), file(group_2,t138_group_2), [interesting(0.00)]). fof(t69_enumset1,theorem,( ! [A] : k2_tarski(A,A) = k1_tarski(A) ), file(enumset1,t69_enumset1), [interesting(0.00)]). fof(t8_zfmisc_1,theorem,( ! [A,B,C] : ( k1_tarski(A) = k2_tarski(B,C) => A = B ) ), file(zfmisc_1,t8_zfmisc_1), [interesting(0.00)]). fof(t88_xboole_1,theorem,( ! [A,B] : ( r1_xboole_0(A,B) => k4_xboole_0(k2_xboole_0(A,B),B) = A ) ), file(xboole_1,t88_xboole_1), [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)) ) ) ) ) ) ), file(group_2,t144_group_2), [interesting(0.00)]). 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) ) ) ) ) ), file(group_2,t136_group_2), [interesting(0.00)]). 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) ) ) ) ) ), file(group_2,t142_group_2), [interesting(0.00)]). fof(t152_group_3,theorem,( $true ), file(group_3,t152_group_3), [interesting(0.00)]). fof(t153_group_3,theorem,( $true ), file(group_3,t153_group_3), [interesting(0.00)]). fof(d14_group_3,definition,( ! [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] : ( ( v1_group_1(C) & m1_group_2(C,A) ) => ( C = k10_group_3(A,B) <=> u1_struct_0(C) = a_2_3_group_3(A,B) ) ) ) ) ), file(group_3,d14_group_3), [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))) ) ) ) ) ) ), file(group_2,t143_group_2), [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(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(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)) ) ) ) ), file(group_2,t175_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(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(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(t38_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(B))) => ( r2_hidden(A,k3_group_3(B,C,D)) <=> ? [E] : ( m1_subset_1(E,u1_struct_0(B)) & ? [F] : ( m1_subset_1(F,u1_struct_0(B)) & A = k2_group_3(B,E,F) & r2_hidden(E,C) & r2_hidden(F,D) ) ) ) ) ) ) ), file(group_3,t38_group_3), [interesting(0.00)]). fof(t39_group_3,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))) => ( k3_group_3(A,B,C) != k1_xboole_0 <=> ( B != k1_xboole_0 & C != k1_xboole_0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_group_3,d3_tarski]), [file(group_3,t39_group_3),interesting(0.00)]). fof(t39_zfmisc_1,theorem,( ! [A,B] : ( r1_tarski(A,k1_tarski(B)) <=> ( A = k1_xboole_0 | A = k1_tarski(B) ) ) ), file(zfmisc_1,t39_zfmisc_1), [interesting(0.00)]). fof(t44_group_3,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_3(A,k6_domain_1(u1_struct_0(A),B),k6_domain_1(u1_struct_0(A),C)) = k6_domain_1(u1_struct_0(A),k2_group_3(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t40_group_3,t6_group_2,t22_group_2,t22_group_2,t39_group_3,t39_zfmisc_1]), [file(group_3,t44_group_3),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(t159_group_3,theorem,( $true ), file(group_3,t159_group_3), [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)) ) ) ) ) ), file(group_2,t116_group_2), [interesting(0.00)]). fof(t162_group_3,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(k9_group_3(A,B)) | v1_finset_1(k14_group_2(A,k11_group_3(A,B))) ) & ! [C] : ( v1_finset_1(C) => ~ ( C = k9_group_3(A,B) & k4_card_1(C) = k17_group_2(A,k11_group_3(A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t161_group_3,t21_card_1,t68_card_1,d18_group_2,t68_card_1]), [file(group_3,t162_group_3),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(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)) ) ) ) ), file(group_2,t71_group_2), [interesting(0.00)]). fof(t16_group_3,theorem,( $true ), file(group_3,t16_group_3), [interesting(0.00)]). fof(t17_group_3,theorem,( $true ), file(group_3,t17_group_3), [interesting(0.00)]). fof(d13_binop_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_binop_1(B,A) <=> ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => k2_binop_1(A,A,A,B,C,D) = k2_binop_1(A,A,A,B,D,C) ) ) ) ) ) ), file(binop_1,d13_binop_1), [interesting(0.00)]). fof(l2_group_3,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_3,l2_group_3), [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(d2_binop_1,definition,( ! [A,B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(A,A),A) & m2_relset_1(B,k2_zfmisc_1(A,A),A) ) => ( v1_binop_1(B,A) <=> ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => k1_binop_1(B,C,D) = k1_binop_1(B,D,C) ) ) ) ) ), file(binop_1,d2_binop_1), [interesting(0.00)]). fof(t31_group_3,theorem,( $true ), file(group_3,t31_group_3), [interesting(0.00)]). fof(t43_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,0,B) = k2_group_1(A) ) ) ), file(group_1,t43_group_1), [interesting(0.00)]). fof(l36_group_3,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)) => k2_group_3(A,k6_group_1(A,0,B),C) = k6_group_1(A,0,k2_group_3(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_group_1,t22_group_3,t43_group_1]), [file(group_3,l36_group_3),interesting(0.00)]). fof(t49_group_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [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)) => ( k6_group_1(B,k1_nat_1(A,1),C) = k1_group_1(B,k6_group_1(B,A,C),C) & k6_group_1(B,k1_nat_1(A,1),C) = k1_group_1(B,C,k6_group_1(B,A,C)) ) ) ) ) ), file(group_1,t49_group_1), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(d1_absvalue,definition,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) => k16_complex1(A) = A ) & ( ~ r1_xreal_0(0,A) => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ), file(absvalue,d1_absvalue), [interesting(0.00)]). fof(t56_group_1,theorem,( ! [A] : ( v1_int_1(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)) => ( ~ r1_xreal_0(0,A) => k6_group_1(B,A,C) = k3_group_1(B,k6_group_1(B,k1_int_2(A),C)) ) ) ) ) ), file(group_1,t56_group_1), [interesting(0.00)]). fof(t37_group_3,theorem,( $true ), file(group_3,t37_group_3), [interesting(0.00)]). fof(t43_group_3,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))) => k3_group_3(A,k1_group_2(A,B),C) = k1_group_2(A,k3_group_3(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t32_group_3,d10_xboole_0,d3_tarski,t32_group_3]), [file(group_3,t43_group_3),interesting(0.00)]). fof(t45_group_3,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)) => k3_group_3(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),k2_group_3(A,B,C),k2_group_3(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_3,t45_group_3),interesting(0.00)]). fof(t46_group_3,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)) => k3_group_3(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),k2_group_3(A,B,D),k2_group_3(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_3,t46_group_3),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(t47_group_3,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)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k3_group_3(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),k2_group_3(A,B,D),k2_group_3(A,B,E),k2_group_3(A,C,D),k2_group_3(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_3,t47_group_3),interesting(0.00)]). fof(t48_group_3,theorem,( $true ), file(group_3,t48_group_3), [interesting(0.00)]). fof(t49_group_3,theorem,( $true ), file(group_3,t49_group_3), [interesting(0.00)]). fof(t55_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => k3_group_3(A,k5_group_3(A,C,B),D) = k5_group_3(A,k2_group_2(A,C,D),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t42_group_3]), [file(group_3,t55_group_3),interesting(0.00)]). fof(t53_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => k4_group_3(A,k3_group_3(A,C,D),B) = k3_group_3(A,C,k4_group_2(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t42_group_3]), [file(group_3,t53_group_3),interesting(0.00)]). fof(t57_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => k4_group_3(A,k5_group_3(A,D,B),C) = k5_group_3(A,k4_group_2(A,C,D),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_group_3]), [file(group_3,t57_group_3),interesting(0.00)]). fof(t58_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => k5_group_3(A,D,k2_group_3(A,B,C)) = k5_group_3(A,k3_group_2(A,C,D),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t44_group_3,t42_group_3]), [file(group_3,t58_group_3),interesting(0.00)]). fof(t41_group_3,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_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k3_group_3(A,k2_group_2(A,B,C),D),k2_group_2(A,k3_group_3(A,B,D),k3_group_3(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t28_group_3]), [file(group_3,t41_group_3),interesting(0.00)]). fof(t60_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => r1_tarski(k4_group_3(A,k2_group_2(A,C,D),B),k2_group_2(A,k4_group_3(A,C,B),k4_group_3(A,D,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_group_3]), [file(group_3,t60_group_3),interesting(0.00)]). fof(t64_group_3,theorem,( $true ), file(group_3,t64_group_3), [interesting(0.00)]). fof(t35_group_3,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)) => ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & v7_group_1(A) & l1_group_1(A) ) => k2_group_3(A,B,C) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[l2_group_3,t1_group_3]), [file(group_3,t35_group_3),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(t65_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(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))) => ( C != k1_xboole_0 => k3_group_3(A,B,C) = B ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t35_group_3,d10_xboole_0,d3_tarski,d3_tarski,t35_group_3,t44_group_3,t6_zfmisc_1,t36_group_3]), [file(group_3,t65_group_3),interesting(0.00)]). fof(t66_group_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_group_1(A) & v4_group_1(A) & l1_group_1(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,u1_struct_0(A)) => k4_group_3(A,B,C) = B ) ) ) ) ), inference(mizar_proof,[status(thm)],[t65_group_3,t44_group_3,t6_zfmisc_1,t36_group_3]), [file(group_3,t66_group_3),interesting(0.00)]). fof(t68_group_3,theorem,( $true ), file(group_3,t68_group_3), [interesting(0.00)]). fof(t69_group_3,theorem,( $true ), file(group_3,t69_group_3), [interesting(0.00)]). fof(t75_group_3,theorem,( $true ), file(group_3,t75_group_3), [interesting(0.00)]). fof(t7_group_3,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) => k12_group_2(A,C,B) = k10_group_2(A,C,k6_domain_1(u1_struct_0(A),B)) ) ) ) ), file(group_3,t7_group_3), [interesting(0.00)]). 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)) ) ), file(group_2,t80_group_2), [interesting(0.00)]). 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 ) ), file(group_2,t81_group_2), [interesting(0.00)]). fof(s4_funct_2,theorem,( ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s4_funct_2,f2_s4_funct_2) & m2_relset_1(A,f1_s4_funct_2,f2_s4_funct_2) & ! [B] : ( m1_subset_1(B,f1_s4_funct_2) => k8_funct_2(f1_s4_funct_2,f2_s4_funct_2,A,B) = f3_s4_funct_2(B) ) ) ), file(funct_2,s4_funct_2), [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(t91_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(A,k1_relat_1(B)) => k1_relat_1(k7_relat_1(B,A)) = A ) ) ), file(relat_1,t91_relat_1), [interesting(0.00)]). fof(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)) ) ) ) ), file(group_2,t51_group_2), [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(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(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)) ) ) ) ), file(group_2,t82_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)) ) ) ) ) ) ), 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)) ) ) ) ) ) ), file(group_2,t137_group_2), [interesting(0.00)]). fof(t87_group_3,theorem,( $true ), file(group_3,t87_group_3), [interesting(0.00)]). fof(t8_group_3,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) => k13_group_2(A,C,B) = k11_group_2(A,C,k6_domain_1(u1_struct_0(A),B)) ) ) ) ), file(group_3,t8_group_3), [interesting(0.00)]). fof(t94_group_3,theorem,( $true ), file(group_3,t94_group_3), [interesting(0.00)]). fof(t9_group_3,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,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_group_2(D,A) => k10_group_2(A,D,k3_group_2(A,B,C)) = k3_group_2(A,B,k10_group_2(A,D,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t116_group_2]), [file(group_3,t9_group_3),interesting(0.00)]).