fof(l3_bvfunc14,theorem,( ! [A,B,C,D,E,F] : k1_relat_1(k1_funct_4(k1_funct_4(k3_cqc_lang(A,D),k3_cqc_lang(B,E)),k3_cqc_lang(C,F))) = k1_enumset1(A,B,C) ), inference(mizar_proof,[status(thm)],[d1_funct_4,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,d1_funct_4,t41_enumset1,t43_enumset1]), [file(bvfunc14,l3_bvfunc14),interesting(1.00)]). fof(t1_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => k22_bvfunc_1(A,B,k2_partit1(A,C,D)) = k5_subset_1(A,k22_bvfunc_1(A,B,C),k22_bvfunc_1(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,t3_bvfunc11,t3_bvfunc11,d3_xboole_0,d3_tarski,d3_xboole_0,d1_t_1topsp,d1_t_1topsp,t3_xboole_0,t3_xboole_0,d1_t_1topsp,d1_t_1topsp,d4_partit1,d4_xboole_0,d5_setfam_1,d1_t_1topsp,d3_xboole_0,t3_xboole_0,d6_eqrel_1,t3_xboole_0,d6_eqrel_1,t9_t_1topsp,d3_xboole_0,t9_t_1topsp,d10_xboole_0]), [file(bvfunc14,t1_bvfunc14),interesting(0.99)]). fof(t24_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ( B = k3_enumset1(C,D,E,F,G) => ( C = D | C = E | C = F | C = G | k5_bvfunc_2(A,C,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_enumset1,t110_enumset1,t50_enumset1,t72_enumset1,t108_enumset1,t7_bvfunc14,t15_partit1,t50_enumset1,t112_enumset1,t50_enumset1,t72_enumset1,t108_enumset1,t7_bvfunc14,t15_partit1,t16_partit1,t47_enumset1,t105_enumset1,t71_enumset1,t44_enumset1,t7_bvfunc14,t15_partit1,t16_partit1,t16_partit1,t16_partit1,t50_enumset1,t118_enumset1,t71_enumset1,t46_enumset1,t110_enumset1,t7_bvfunc14,t15_partit1,t16_partit1,t47_enumset1,t117_enumset1,t71_enumset1,t44_enumset1,t104_enumset1,t7_bvfunc14,t15_partit1,t16_partit1,t16_partit1,t16_partit1,t16_partit1,t47_enumset1,t118_enumset1,t71_enumset1,t44_enumset1,t105_enumset1,t7_bvfunc14,t15_partit1,t16_partit1,t16_partit1,t16_partit1,t16_partit1,t47_enumset1,t42_xboole_1,d1_tarski,d1_tarski,d1_tarski,d1_tarski,t44_enumset1,t42_xboole_1,t67_zfmisc_1,t42_enumset1,t42_xboole_1,t72_zfmisc_1,t67_zfmisc_1,t42_enumset1,t44_enumset1,d1_tarski,t68_zfmisc_1,d3_tarski,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d1_funct_4,d1_funct_4,d1_funct_4,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t41_enumset1,t43_enumset1,t46_enumset1,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,d1_tarski,t12_funct_4,t12_funct_4,d1_tarski,t12_funct_4,t6_cqc_lang,d1_tarski,d1_tarski,t12_funct_4,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d3_tarski,d5_funct_1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d2_enumset1,d10_xboole_0,d3_tarski,d2_enumset1,t12_funct_1,d3_tarski,d2_enumset1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,d3_xboole_0,d3_xboole_0,d2_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d2_enumset1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d2_enumset1,d2_enumset1,d5_funct_1,d1_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d3_tarski,d5_funct_1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d2_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0,d7_bvfunc_2]), [file(bvfunc14,t24_bvfunc14),interesting(0.97)]). fof(l5_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ~ ( A != B & C != A & k1_funct_1(k1_funct_4(k1_funct_4(k3_cqc_lang(A,D),k3_cqc_lang(B,E)),k3_cqc_lang(C,F)),A) != D ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t5_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,t6_cqc_lang]), [file(bvfunc14,l5_bvfunc14),interesting(0.96)]). fof(l4_bvfunc14,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C,D,E] : ( B != C => k1_funct_1(k1_funct_4(k1_funct_4(A,k3_cqc_lang(B,D)),k3_cqc_lang(C,E)),B) = D ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t5_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang]), [file(bvfunc14,l4_bvfunc14),interesting(0.96)]). fof(t8_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ( B = k2_enumset1(C,D,E,F) => ( C = D | D = E | D = F | k5_bvfunc_2(A,D,B) = k2_partit1(A,k2_partit1(A,C,E),F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t108_enumset1,t7_bvfunc14]), [file(bvfunc14,t8_bvfunc14),interesting(0.92)]). fof(t7_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ( B = k2_enumset1(C,D,E,F) => ( C = D | C = E | C = F | k5_bvfunc_2(A,C,B) = k2_partit1(A,k2_partit1(A,D,E),F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t116_enumset1,t71_enumset1,t99_enumset1,t4_bvfunc14,t15_partit1,t112_enumset1,t71_enumset1,t99_enumset1,t4_bvfunc14,t15_partit1,t16_partit1,t118_enumset1,t71_enumset1,t100_enumset1,t4_bvfunc14,t15_partit1,t16_partit1,t44_enumset1,t42_xboole_1,d1_tarski,d1_tarski,d1_tarski,t42_enumset1,t42_xboole_1,t72_zfmisc_1,t67_zfmisc_1,t42_enumset1,t37_xboole_1,d3_tarski,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,l3_bvfunc14,t3_yellow14,l5_bvfunc14,l4_bvfunc14,t3_yellow14,l5_bvfunc14,l4_bvfunc14,d1_enumset1,d1_enumset1,l6_bvfunc14,t100_enumset1,d3_tarski,d1_enumset1,t12_funct_1,d3_tarski,d1_enumset1,d3_xboole_0,t16_xboole_1,d3_xboole_0,t16_xboole_1,d3_xboole_0,d1_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_enumset1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d1_enumset1,d1_enumset1,d5_funct_1,d1_tarski,d3_tarski,d3_xboole_0,d3_tarski,d5_funct_1,d1_enumset1,d1_enumset1,d1_enumset1,d1_enumset1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d1_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0,d7_bvfunc_2]), [file(bvfunc14,t7_bvfunc14),interesting(0.91)]). fof(t14_bvfunc14,theorem,( ! [A,B,C,D,E,F] : k1_relat_1(k1_funct_4(k1_funct_4(k3_cqc_lang(A,D),k3_cqc_lang(B,E)),k3_cqc_lang(C,F))) = k1_enumset1(A,B,C) ), inference(mizar_proof,[status(thm)],[l3_bvfunc14]), [file(bvfunc14,t14_bvfunc14),interesting(0.88)]). fof(t4_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( B = k1_enumset1(C,D,E) => ( C = D | E = C | k5_bvfunc_2(A,C,B) = k2_partit1(A,D,E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_enumset1,t70_enumset1,t7_bvfunc11,t15_partit1,d7_bvfunc_2,t42_enumset1,t42_xboole_1,d1_tarski,d1_tarski,t72_zfmisc_1,t37_xboole_1,d3_tarski,d4_partit1,d4_xboole_0,d5_setfam_1,t65_funct_4,t67_funct_4,d3_tarski,d2_tarski,t66_funct_4,t66_funct_4,d2_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d2_tarski,d1_setfam_1,d10_setfam_1,d3_tarski,d2_tarski,d10_setfam_1,d1_setfam_1,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d2_tarski,d2_tarski,d5_funct_1,d1_tarski,d3_tarski,d3_tarski,d5_funct_1,d2_tarski,d2_tarski,d2_tarski,d3_xboole_0,d3_xboole_0,d2_tarski,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_setfam_1,d3_xboole_0,d10_xboole_0,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0]), [file(bvfunc14,t4_bvfunc14),interesting(0.85)]). fof(t5_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( B = k1_enumset1(C,D,E) => ( C = D | D = E | k5_bvfunc_2(A,D,B) = k2_partit1(A,E,C) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_enumset1,t4_bvfunc14]), [file(bvfunc14,t5_bvfunc14),interesting(0.85)]). fof(t15_bvfunc14,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C,D,E] : ( B != C => k1_funct_1(k1_funct_4(k1_funct_4(A,k3_cqc_lang(B,D)),k3_cqc_lang(C,E)),B) = D ) ) ), inference(mizar_proof,[status(thm)],[l4_bvfunc14]), [file(bvfunc14,t15_bvfunc14),interesting(0.84)]). fof(t16_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ~ ( A != B & C != A & k1_funct_1(k1_funct_4(k1_funct_4(k3_cqc_lang(A,D),k3_cqc_lang(B,E)),k3_cqc_lang(C,F)),A) != D ) ), inference(mizar_proof,[status(thm)],[l5_bvfunc14]), [file(bvfunc14,t16_bvfunc14),interesting(0.83)]). fof(t19_bvfunc14,theorem,( ! [A,B,C,D,E] : ( ( v1_relat_1(E) & v1_funct_1(E) ) => ! [F,G,H,I] : ( E = k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,G),k3_cqc_lang(C,H)),k3_cqc_lang(D,I)),k3_cqc_lang(A,F)) => k1_relat_1(E) = k2_enumset1(A,B,C,D) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_4,d1_funct_4,t5_cqc_lang,d1_funct_4,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t41_enumset1,t43_enumset1,t44_enumset1]), [file(bvfunc14,t19_bvfunc14),interesting(0.82)]). fof(l6_bvfunc14,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ( G = k1_funct_4(k1_funct_4(k3_cqc_lang(A,D),k3_cqc_lang(B,E)),k3_cqc_lang(C,F)) => k2_relat_1(G) = k1_enumset1(k1_funct_1(G,A),k1_funct_1(G,B),k1_funct_1(G,C)) ) ) ), inference(mizar_proof,[status(thm)],[l3_bvfunc14,d1_enumset1,d1_enumset1,d1_enumset1,d3_tarski,d5_funct_1,d1_enumset1,d1_enumset1,d1_enumset1,d1_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d1_enumset1,d10_xboole_0]), [file(bvfunc14,l6_bvfunc14),interesting(0.81)]). fof(t10_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ( B = k2_enumset1(C,D,E,F) => ( C = F | D = F | E = F | k5_bvfunc_2(A,F,B) = k2_partit1(A,k2_partit1(A,C,E),D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t113_enumset1,t7_bvfunc14]), [file(bvfunc14,t10_bvfunc14),interesting(0.78)]). fof(t9_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ( B = k2_enumset1(C,D,E,F) => ( C = E | D = E | E = F | k5_bvfunc_2(A,E,B) = k2_partit1(A,k2_partit1(A,C,D),F) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t110_enumset1,t7_bvfunc14]), [file(bvfunc14,t9_bvfunc14),interesting(0.78)]). fof(t27_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ( ( v2_bvfunc_2(B,A) & B = k3_enumset1(C,D,E,F,G) ) => ( C = D | C = E | C = F | C = G | D = E | D = F | D = G | E = F | E = G | F = G | k5_bvfunc_2(A,F,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t48_enumset1,t43_enumset1,t43_enumset1,t48_enumset1,t26_bvfunc14]), [file(bvfunc14,t27_bvfunc14),interesting(0.76)]). fof(t26_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ( ( v2_bvfunc_2(B,A) & B = k3_enumset1(C,D,E,F,G) ) => ( C = D | C = E | C = F | C = G | D = E | D = F | D = G | E = F | E = G | F = G | k5_bvfunc_2(A,E,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),F),G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t49_enumset1,t42_enumset1,t42_enumset1,t43_enumset1,t43_enumset1,t49_enumset1,t24_bvfunc14]), [file(bvfunc14,t26_bvfunc14),interesting(0.75)]). fof(t25_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ( ( v2_bvfunc_2(B,A) & B = k3_enumset1(C,D,E,F,G) ) => ( C = D | C = E | C = F | C = G | D = E | D = F | D = G | E = F | E = G | F = G | k5_bvfunc_2(A,D,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,C,E),F),G) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t48_enumset1,t48_enumset1,t24_bvfunc14]), [file(bvfunc14,t25_bvfunc14),interesting(0.75)]). fof(t2_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ( B = k2_tarski(C,D) => ( C = D | k2_bvfunc_2(A,B) = k2_partit1(A,C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_partit1,d4_xboole_0,d5_setfam_1,t65_funct_4,t67_funct_4,t67_funct_4,d3_tarski,d2_tarski,t66_funct_4,t66_funct_4,d2_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d2_tarski,d1_setfam_1,d10_setfam_1,d3_tarski,d2_tarski,t67_funct_4,d10_setfam_1,d1_setfam_1,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d2_tarski,d2_tarski,d5_funct_1,d1_tarski,d3_tarski,d3_tarski,d5_funct_1,d2_tarski,d2_tarski,d2_tarski,d3_xboole_0,d3_xboole_0,d2_tarski,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_setfam_1,d3_xboole_0,d10_xboole_0,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0]), [file(bvfunc14,t2_bvfunc14),interesting(0.73)]). fof(t3_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( B = k1_enumset1(C,D,E) => ( C = D | D = E | E = C | k2_bvfunc_2(A,B) = k2_partit1(A,k2_partit1(A,C,D),E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_tarski,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,l3_bvfunc14,t3_yellow14,l5_bvfunc14,l4_bvfunc14,t3_yellow14,l5_bvfunc14,l4_bvfunc14,d1_enumset1,d1_enumset1,l6_bvfunc14,t100_enumset1,d3_tarski,l5_bvfunc14,l4_bvfunc14,d1_enumset1,t12_funct_1,d3_tarski,d1_enumset1,d3_xboole_0,t16_xboole_1,d3_xboole_0,t16_xboole_1,d3_xboole_0,d1_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_enumset1,d1_setfam_1,l4_bvfunc14,l5_bvfunc14,t3_yellow14,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d1_enumset1,d1_enumset1,d5_funct_1,d1_tarski,d3_tarski,d3_xboole_0,d3_tarski,d5_funct_1,d1_enumset1,d1_enumset1,d1_enumset1,d1_enumset1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d1_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d10_setfam_1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0]), [file(bvfunc14,t3_bvfunc14),interesting(0.70)]). fof(t6_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( B = k1_enumset1(C,D,E) => ( D = E | E = C | k5_bvfunc_2(A,E,B) = k2_partit1(A,C,D) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t100_enumset1,t4_bvfunc14]), [file(bvfunc14,t6_bvfunc14),interesting(0.70)]). fof(t31_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ( ( v1_relat_1(F) & v1_funct_1(F) ) => ! [G,H,I,J,K] : ( F = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,H),k3_cqc_lang(C,I)),k3_cqc_lang(D,J)),k3_cqc_lang(E,K)),k3_cqc_lang(A,G)) => k2_relat_1(F) = k3_enumset1(k1_funct_1(F,A),k1_funct_1(F,B),k1_funct_1(F,C),k1_funct_1(F,D),k1_funct_1(F,E)) ) ) ), inference(mizar_proof,[status(thm)],[t30_bvfunc14,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_tarski,d5_funct_1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d3_enumset1,d10_xboole_0]), [file(bvfunc14,t31_bvfunc14),interesting(0.69)]). fof(t17_bvfunc14,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ( G = k1_funct_4(k1_funct_4(k3_cqc_lang(A,D),k3_cqc_lang(B,E)),k3_cqc_lang(C,F)) => k2_relat_1(G) = k1_enumset1(k1_funct_1(G,A),k1_funct_1(G,B),k1_funct_1(G,C)) ) ) ), inference(mizar_proof,[status(thm)],[l6_bvfunc14]), [file(bvfunc14,t17_bvfunc14),interesting(0.66)]). fof(t28_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ( ( v2_bvfunc_2(B,A) & B = k3_enumset1(C,D,E,F,G) ) => ( C = D | C = E | C = F | C = G | D = E | D = F | D = G | E = F | E = G | F = G | k5_bvfunc_2(A,G,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t49_enumset1,t49_enumset1,t27_bvfunc14]), [file(bvfunc14,t28_bvfunc14),interesting(0.60)]). fof(t33_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_subset_1(H,A) => ! [I] : ( m1_subset_1(I,A) => ~ ( v2_bvfunc_2(B,A) & B = k3_enumset1(C,D,E,F,G) & C != D & C != E & C != F & C != G & D != E & D != F & D != G & E != F & E != G & F != G & k22_bvfunc_1(A,H,k2_partit1(A,k2_partit1(A,E,F),G)) = k22_bvfunc_1(A,I,k2_partit1(A,k2_partit1(A,E,F),G)) & r1_xboole_0(k22_bvfunc_1(A,I,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,H,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_bvfunc14,t30_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,d3_enumset1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,t31_bvfunc14,d3_tarski,t29_bvfunc14,d3_enumset1,d5_bvfunc_2,d1_xboole_0,d10_setfam_1,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,t1_bvfunc14,d1_xboole_0,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,t16_partit1,t16_partit1,t3_bvfunc11,d3_xboole_0,d1_t_1topsp,t3_xboole_0,t9_t_1topsp,d1_t_1topsp,d1_t_1topsp,d3_xboole_0,d1_t_1topsp,t16_partit1,t16_partit1,d4_partit1,d6_eqrel_1,t3_xboole_0,d3_xboole_0,d3_xboole_0,t4_xboole_0,t24_bvfunc14]), [file(bvfunc14,t33_bvfunc14),interesting(0.47)]). fof(t23_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ~ ( v2_bvfunc_2(B,A) & B = k1_enumset1(C,D,E) & C != D & D != E & E != C & k22_bvfunc_1(A,F,E) = k22_bvfunc_1(A,G,E) & r1_xboole_0(k22_bvfunc_1(A,G,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,F,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_bvfunc14,t4_bvfunc14,d1_funct_4,d1_funct_4,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t4_xboole_1,t41_enumset1,t43_enumset1,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang,d1_enumset1,d1_enumset1,d5_funct_1,d1_enumset1,d5_funct_1,d1_enumset1,d5_funct_1,d3_tarski,d5_funct_1,d1_enumset1,d1_enumset1,d1_enumset1,d1_enumset1,d3_tarski,d1_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d1_xboole_0,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d1_tarski,d5_setfam_1,d4_xboole_0,d4_partit1,t3_bvfunc11,d3_xboole_0,d1_t_1topsp,t3_xboole_0,t9_t_1topsp,d1_t_1topsp,d1_t_1topsp,d3_xboole_0,d1_t_1topsp,d6_eqrel_1,t3_xboole_0]), [file(bvfunc14,t23_bvfunc14),interesting(0.43)]). fof(t22_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ! [H] : ( m1_subset_1(H,A) => ~ ( v2_bvfunc_2(B,A) & B = k2_enumset1(C,D,E,F) & C != D & C != E & C != F & D != E & D != F & E != F & k22_bvfunc_1(A,G,k2_partit1(A,E,F)) = k22_bvfunc_1(A,H,k2_partit1(A,E,F)) & r1_xboole_0(k22_bvfunc_1(A,H,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,G,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_bvfunc14,t19_bvfunc14,t3_yellow14,t18_bvfunc14,t18_bvfunc14,t18_bvfunc14,t3_yellow14,t18_bvfunc14,t18_bvfunc14,t18_bvfunc14,d2_enumset1,d2_enumset1,d5_funct_1,d2_enumset1,d5_funct_1,d2_enumset1,d5_funct_1,d2_enumset1,d5_funct_1,t20_bvfunc14,d3_tarski,t3_yellow14,t18_bvfunc14,t18_bvfunc14,t18_bvfunc14,d2_enumset1,t19_bvfunc14,d5_bvfunc_2,d1_xboole_0,d10_setfam_1,d1_setfam_1,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,t1_bvfunc14,d1_xboole_0,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,t16_partit1,t3_bvfunc11,d3_xboole_0,d1_t_1topsp,t3_xboole_0,t9_t_1topsp,d1_t_1topsp,d1_t_1topsp,d3_xboole_0,d1_t_1topsp,t16_partit1,d4_partit1,d6_eqrel_1,t3_xboole_0,d3_xboole_0,d3_xboole_0,t4_xboole_0,t7_bvfunc14]), [file(bvfunc14,t22_bvfunc14),interesting(0.33)]). fof(t20_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K] : ( ( B = k2_enumset1(C,D,E,F) & G = k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(D,I),k3_cqc_lang(E,J)),k3_cqc_lang(F,K)),k3_cqc_lang(C,H)) ) => k2_relat_1(G) = k2_enumset1(k1_funct_1(G,C),k1_funct_1(G,D),k1_funct_1(G,E),k1_funct_1(G,F)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_bvfunc14,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d3_tarski,d5_funct_1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d2_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d2_enumset1,d10_xboole_0]), [file(bvfunc14,t20_bvfunc14),interesting(0.26)]). fof(t18_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K] : ( ( B = k2_enumset1(C,D,E,F) & G = k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(D,I),k3_cqc_lang(E,J)),k3_cqc_lang(F,K)),k3_cqc_lang(C,H)) ) => ( C = D | C = E | C = F | D = E | D = F | E = F | ( k1_funct_1(G,D) = I & k1_funct_1(G,E) = J & k1_funct_1(G,F) = K ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang]), [file(bvfunc14,t18_bvfunc14),interesting(0.20)]). fof(t21_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_subset_1(G,A) => ! [H] : ( m1_subset_1(H,A) => ! [I] : ( ( v1_relat_1(I) & v1_funct_1(I) ) => ~ ( v2_bvfunc_2(B,A) & B = k2_enumset1(C,D,E,F) & C != D & C != E & C != F & D != E & D != F & E != F & r1_xboole_0(k22_bvfunc_1(A,H,k2_partit1(A,k2_partit1(A,D,E),F)),k22_bvfunc_1(A,G,C)) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_bvfunc14,t3_yellow14,t18_bvfunc14,t18_bvfunc14,t18_bvfunc14,t3_yellow14,t18_bvfunc14,t18_bvfunc14,t18_bvfunc14,d2_enumset1,d2_enumset1,d5_funct_1,d2_enumset1,d5_funct_1,d2_enumset1,d5_funct_1,d2_enumset1,d5_funct_1,t20_bvfunc14,d3_tarski,t3_yellow14,d2_enumset1,d5_bvfunc_2,d1_xboole_0,d10_setfam_1,d1_setfam_1,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,t4_xboole_0,t1_bvfunc14]), [file(bvfunc14,t21_bvfunc14),interesting(0.14)]). fof(t113_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(B,D,C,A) ), file(enumset1,t113_enumset1), [interesting(0.00)]). fof(t116_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(C,B,A,D) ), file(enumset1,t116_enumset1), [interesting(0.00)]). fof(t71_enumset1,theorem,( ! [A,B,C] : k2_enumset1(A,A,B,C) = k1_enumset1(A,B,C) ), file(enumset1,t71_enumset1), [interesting(0.00)]). fof(t99_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k1_enumset1(B,A,C) ), file(enumset1,t99_enumset1), [interesting(0.00)]). fof(t100_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k1_enumset1(B,C,A) ), file(enumset1,t100_enumset1), [interesting(0.00)]). fof(t70_enumset1,theorem,( ! [A,B] : k1_enumset1(A,A,B) = k2_tarski(A,B) ), file(enumset1,t70_enumset1), [interesting(0.00)]). fof(t7_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ( B = k2_tarski(C,D) => ( C = D | k5_bvfunc_2(A,C,B) = D ) ) ) ) ) ) ), file(bvfunc11,t7_bvfunc11), [interesting(0.00)]). fof(t15_partit1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => k2_partit1(A,B,B) = B ) ) ), file(partit1,t15_partit1), [interesting(0.00)]). fof(d7_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => k5_bvfunc_2(A,B,C) = k2_bvfunc_2(A,k6_subset_1(k1_bvfunc_2(A),C,k4_bvfunc_2(A,B))) ) ) ) ), file(bvfunc_2,d7_bvfunc_2), [interesting(0.00)]). fof(t42_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k1_tarski(A),k2_tarski(B,C)) ), file(enumset1,t42_enumset1), [interesting(0.00)]). fof(t42_xboole_1,theorem,( ! [A,B,C] : k4_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(k4_xboole_0(A,C),k4_xboole_0(B,C)) ), file(xboole_1,t42_xboole_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t72_zfmisc_1,theorem,( ! [A,B,C] : ( k4_xboole_0(k2_tarski(A,B),C) = k2_tarski(A,B) <=> ( ~ r2_hidden(A,C) & ~ r2_hidden(B,C) ) ) ), file(zfmisc_1,t72_zfmisc_1), [interesting(0.00)]). fof(t37_xboole_1,theorem,( ! [A,B] : ( k4_xboole_0(A,B) = k1_xboole_0 <=> r1_tarski(A,B) ) ), file(xboole_1,t37_xboole_1), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d4_partit1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => k2_partit1(A,B,C) = k4_xboole_0(k3_setfam_1(B,C),k1_tarski(k1_xboole_0)) ) ) ) ), file(partit1,d4_partit1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(d5_setfam_1,definition,( ! [A,B,C] : ( C = k3_setfam_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k3_xboole_0(E,F) ) ) ) ), file(setfam_1,d5_setfam_1), [interesting(0.00)]). fof(t65_funct_4,theorem,( ! [A,B,C,D] : ( k1_relat_1(k4_funct_4(A,B,C,D)) = k2_tarski(A,B) & r1_tarski(k2_relat_1(k4_funct_4(A,B,C,D)),k2_tarski(C,D)) ) ), file(funct_4,t65_funct_4), [interesting(0.00)]). fof(t67_funct_4,theorem,( ! [A,B,C,D] : ( A != B => k2_relat_1(k4_funct_4(A,B,C,D)) = k2_tarski(C,D) ) ), file(funct_4,t67_funct_4), [interesting(0.00)]). fof(d2_tarski,definition,( ! [A,B,C] : ( C = k2_tarski(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( D = A | D = B ) ) ) ), file(tarski,d2_tarski), [interesting(0.00)]). fof(t66_funct_4,theorem,( ! [A,B,C,D] : ( A != B => ( k1_funct_1(k4_funct_4(A,B,C,D),A) = C & k1_funct_1(k4_funct_4(A,B,C,D),B) = D ) ) ), file(funct_4,t66_funct_4), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d1_setfam_1,definition,( ! [A,B] : ( ( A != k1_xboole_0 => ( B = k1_setfam_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ! [D] : ( r2_hidden(D,A) => r2_hidden(C,D) ) ) ) ) & ( A = k1_xboole_0 => ( B = k1_setfam_1(A) <=> B = k1_xboole_0 ) ) ) ), file(setfam_1,d1_setfam_1), [interesting(0.00)]). fof(d10_setfam_1,definition,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ( ( B != k1_xboole_0 => k8_setfam_1(A,B) = k6_setfam_1(A,B) ) & ( B = k1_xboole_0 => k8_setfam_1(A,B) = A ) ) ) ), file(setfam_1,d10_setfam_1), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(d6_eqrel_1,definition,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ( ( A != k1_xboole_0 => ( m1_eqrel_1(B,A) <=> ( k5_setfam_1(A,B) = A & ! [C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ( r2_hidden(C,B) => ( C != k1_xboole_0 & ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ~ ( r2_hidden(D,B) & C != D & ~ r1_xboole_0(C,D) ) ) ) ) ) ) ) ) & ( A = k1_xboole_0 => ( m1_eqrel_1(B,A) <=> B = k1_xboole_0 ) ) ) ) ), file(eqrel_1,d6_eqrel_1), [interesting(0.00)]). fof(d1_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ( C = k2_bvfunc_2(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E] : ( v1_relat_1(E) & v1_funct_1(E) & ? [F] : ( m1_subset_1(F,k1_zfmisc_1(k1_zfmisc_1(A))) & k1_relat_1(E) = B & k2_relat_1(E) = F & ! [G] : ( r2_hidden(G,B) => r2_hidden(k1_funct_1(E,G),G) ) & D = k8_setfam_1(A,F) & D != k1_xboole_0 ) ) ) ) ) ) ) ), file(bvfunc_2,d1_bvfunc_2), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(t112_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(B,D,A,C) ), file(enumset1,t112_enumset1), [interesting(0.00)]). fof(t16_partit1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => k2_partit1(A,k2_partit1(A,B,C),D) = k2_partit1(A,B,k2_partit1(A,C,D)) ) ) ) ) ), file(partit1,t16_partit1), [interesting(0.00)]). fof(t118_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(C,D,A,B) ), file(enumset1,t118_enumset1), [interesting(0.00)]). fof(t44_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_xboole_0(k1_tarski(A),k1_enumset1(B,C,D)) ), file(enumset1,t44_enumset1), [interesting(0.00)]). fof(t67_zfmisc_1,theorem,( ! [A,B] : ( k4_xboole_0(k1_tarski(A),B) = k1_tarski(A) <=> ~ r2_hidden(A,B) ) ), file(zfmisc_1,t67_zfmisc_1), [interesting(0.00)]). fof(d1_funct_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k1_funct_4(A,B) <=> ( k1_relat_1(C) = k2_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k2_xboole_0(k1_relat_1(A),k1_relat_1(B))) => ( ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(B,D) ) & ( ~ r2_hidden(D,k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) ) ) ) ) ) ) ), file(funct_4,d1_funct_4), [interesting(0.00)]). fof(t5_cqc_lang,theorem,( ! [A,B] : ( k1_relat_1(k3_cqc_lang(A,B)) = k1_tarski(A) & k2_relat_1(k3_cqc_lang(A,B)) = k1_tarski(B) ) ), file(cqc_lang,t5_cqc_lang), [interesting(0.00)]). fof(t41_enumset1,theorem,( ! [A,B] : k2_tarski(A,B) = k2_xboole_0(k1_tarski(A),k1_tarski(B)) ), file(enumset1,t41_enumset1), [interesting(0.00)]). fof(t43_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k2_tarski(A,B),k1_tarski(C)) ), file(enumset1,t43_enumset1), [interesting(0.00)]). fof(t3_yellow14,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : k1_funct_1(k1_funct_4(A,k3_cqc_lang(B,C)),B) = C ) ), file(yellow14,t3_yellow14), [interesting(0.00)]). fof(t12_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ~ r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(C,A) ) ) ) ), file(funct_4,t12_funct_4), [interesting(0.00)]). fof(t6_cqc_lang,theorem,( ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ), file(cqc_lang,t6_cqc_lang), [interesting(0.00)]). fof(t14_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ), file(funct_4,t14_funct_4), [interesting(0.00)]). fof(d1_enumset1,definition,( ! [A,B,C,D] : ( D = k1_enumset1(A,B,C) <=> ! [E] : ( r2_hidden(E,D) <=> ~ ( E != A & E != B & E != C ) ) ) ), file(enumset1,d1_enumset1), [interesting(0.00)]). fof(t12_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => r2_hidden(k1_funct_1(B,A),k2_relat_1(B)) ) ) ), file(funct_1,t12_funct_1), [interesting(0.00)]). fof(t16_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(k3_xboole_0(A,B),C) = k3_xboole_0(A,k3_xboole_0(B,C)) ), file(xboole_1,t16_xboole_1), [interesting(0.00)]). fof(t11_bvfunc14,theorem,( $true ), file(bvfunc14,t11_bvfunc14), [interesting(0.00)]). fof(t12_bvfunc14,theorem,( $true ), file(bvfunc14,t12_bvfunc14), [interesting(0.00)]). fof(t13_bvfunc14,theorem,( $true ), file(bvfunc14,t13_bvfunc14), [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(d5_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ( v2_bvfunc_2(B,A) <=> ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(A))) => ~ ( k1_relat_1(C) = B & k2_relat_1(C) = D & ! [E] : ( r2_hidden(E,B) => r2_hidden(k1_funct_1(C,E),E) ) & k8_setfam_1(A,D) = k1_xboole_0 ) ) ) ) ) ) ), file(bvfunc_2,d5_bvfunc_2), [interesting(0.00)]). fof(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [interesting(0.00)]). fof(t3_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => r1_tarski(k22_bvfunc_1(A,B,k2_partit1(A,C,D)),k22_bvfunc_1(A,B,C)) ) ) ) ) ), file(bvfunc11,t3_bvfunc11), [interesting(0.00)]). fof(d1_t_1topsp,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( D = k1_t_1topsp(A,B,C) <=> ( r2_hidden(B,D) & r2_hidden(D,C) ) ) ) ) ) ) ), file(t_1topsp,d1_t_1topsp), [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(t9_t_1topsp,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ( ~ r1_xboole_0(k1_t_1topsp(A,C,B),k1_t_1topsp(A,D,B)) => k1_t_1topsp(A,C,B) = k1_t_1topsp(A,D,B) ) ) ) ) ) ), file(t_1topsp,t9_t_1topsp), [interesting(0.00)]). fof(t4_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ r2_hidden(C,k3_xboole_0(A,B)) ) & ~ ( ? [C] : r2_hidden(C,k3_xboole_0(A,B)) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t4_xboole_0), [interesting(0.00)]). fof(t108_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(B,A,C,D) ), file(enumset1,t108_enumset1), [interesting(0.00)]). fof(t4_xboole_1,theorem,( ! [A,B,C] : k2_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(A,k2_xboole_0(B,C)) ), file(xboole_1,t4_xboole_1), [interesting(0.00)]). fof(t49_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k1_enumset1(A,B,C),k2_tarski(D,E)) ), file(enumset1,t49_enumset1), [interesting(0.00)]). fof(t48_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k2_tarski(A,B),k1_enumset1(C,D,E)) ), file(enumset1,t48_enumset1), [interesting(0.00)]). fof(t50_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k2_enumset1(A,B,C,D),k1_tarski(E)) ), file(enumset1,t50_enumset1), [interesting(0.00)]). fof(t110_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(B,C,A,D) ), file(enumset1,t110_enumset1), [interesting(0.00)]). fof(t72_enumset1,theorem,( ! [A,B,C,D] : k3_enumset1(A,A,B,C,D) = k2_enumset1(A,B,C,D) ), file(enumset1,t72_enumset1), [interesting(0.00)]). fof(t47_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k1_tarski(A),k2_enumset1(B,C,D,E)) ), file(enumset1,t47_enumset1), [interesting(0.00)]). fof(t105_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(A,C,D,B) ), file(enumset1,t105_enumset1), [interesting(0.00)]). fof(t46_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_xboole_0(k1_enumset1(A,B,C),k1_tarski(D)) ), file(enumset1,t46_enumset1), [interesting(0.00)]). fof(t117_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(C,B,D,A) ), file(enumset1,t117_enumset1), [interesting(0.00)]). fof(t104_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_enumset1(A,C,B,D) ), file(enumset1,t104_enumset1), [interesting(0.00)]). fof(t68_zfmisc_1,theorem,( ! [A,B] : ( k4_xboole_0(k1_tarski(A),B) = k1_xboole_0 <=> r2_hidden(A,B) ) ), file(zfmisc_1,t68_zfmisc_1), [interesting(0.00)]). fof(t30_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ( ( v1_relat_1(F) & v1_funct_1(F) ) => ! [G,H,I,J,K] : ( F = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,H),k3_cqc_lang(C,I)),k3_cqc_lang(D,J)),k3_cqc_lang(E,K)),k3_cqc_lang(A,G)) => k1_relat_1(F) = k3_enumset1(A,B,C,D,E) ) ) ), inference(mizar_proof,[status(thm)],[d1_funct_4,d1_funct_4,d1_funct_4,d1_funct_4,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t41_enumset1,t43_enumset1,t46_enumset1,t47_enumset1]), [file(bvfunc14,t30_bvfunc14),interesting(0.00)]). fof(t29_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ( ( v1_relat_1(F) & v1_funct_1(F) ) => ! [G,H,I,J,K] : ( F = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,H),k3_cqc_lang(C,I)),k3_cqc_lang(D,J)),k3_cqc_lang(E,K)),k3_cqc_lang(A,G)) => ( A = B | A = C | A = D | A = E | B = C | B = D | B = E | C = D | C = E | D = E | ( k1_funct_1(F,A) = G & k1_funct_1(F,B) = H & k1_funct_1(F,C) = I & k1_funct_1(F,D) = J & k1_funct_1(F,E) = K ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,d1_tarski,t12_funct_4,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang]), [file(bvfunc14,t29_bvfunc14),interesting(0.00)]). fof(d3_enumset1,definition,( ! [A,B,C,D,E,F] : ( F = k3_enumset1(A,B,C,D,E) <=> ! [G] : ( r2_hidden(G,F) <=> ~ ( G != A & G != B & G != C & G != D & G != E ) ) ) ), file(enumset1,d3_enumset1), [interesting(0.00)]). fof(t32_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_subset_1(H,A) => ! [I] : ( m1_subset_1(I,A) => ! [J] : ( ( v1_relat_1(J) & v1_funct_1(J) ) => ~ ( v2_bvfunc_2(B,A) & B = k3_enumset1(C,D,E,F,G) & C != D & C != E & C != F & C != G & D != E & D != F & D != G & E != F & E != G & F != G & r1_xboole_0(k22_bvfunc_1(A,I,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G)),k22_bvfunc_1(A,H,C)) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,d3_enumset1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,d3_enumset1,d5_funct_1,t31_bvfunc14,d3_tarski,t29_bvfunc14,d3_enumset1,d5_bvfunc_2,d1_xboole_0,d10_setfam_1,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,t4_xboole_0,t1_bvfunc14]), [file(bvfunc14,t32_bvfunc14),interesting(0.00)]).