fof(t31_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k3_enumset1(A,B,C,D,E),k2_enumset1(F,G,H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t47_enumset1,t4_xboole_1,t50_enumset1]), [file(bvfunc24,t31_bvfunc24),interesting(1.00)]). fof(t28_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k2_tarski(A,B),k5_enumset1(C,D,E,F,G,H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t45_enumset1,t4_xboole_1,t57_enumset1]), [file(bvfunc24,t28_bvfunc24),interesting(0.97)]). fof(l28_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k2_enumset1(A,B,C,D),k3_enumset1(E,F,G,H,I)) ), inference(mizar_proof,[status(thm)],[d2_enumset1,d3_enumset1,d1_bvfunc24,d2_xboole_0,t2_tarski]), [file(bvfunc24,l28_bvfunc24),interesting(0.95)]). fof(t33_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k5_enumset1(A,B,C,D,E,F,G),k2_tarski(H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t49_enumset1,t4_xboole_1,t59_enumset1]), [file(bvfunc24,t33_bvfunc24),interesting(0.94)]). fof(t32_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k4_enumset1(A,B,C,D,E,F),k1_enumset1(G,H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t48_enumset1,t4_xboole_1,t54_enumset1]), [file(bvfunc24,t32_bvfunc24),interesting(0.94)]). fof(t29_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k1_enumset1(A,B,C),k4_enumset1(D,E,F,G,H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t46_enumset1,t4_xboole_1,t51_enumset1]), [file(bvfunc24,t29_bvfunc24),interesting(0.94)]). fof(t27_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k1_tarski(A),k6_enumset1(B,C,D,E,F,G,H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t44_enumset1,t4_xboole_1,t64_enumset1]), [file(bvfunc24,t27_bvfunc24),interesting(0.94)]). fof(t34_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k6_enumset1(A,B,C,D,E,F,G,H),k1_tarski(I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t50_enumset1,t4_xboole_1,t65_enumset1]), [file(bvfunc24,t34_bvfunc24),interesting(0.91)]). fof(t30_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : k1_bvfunc24(A,B,C,D,E,F,G,H,I) = k2_xboole_0(k2_enumset1(A,B,C,D),k3_enumset1(E,F,G,H,I)) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24]), [file(bvfunc24,t30_bvfunc24),interesting(0.90)]). fof(l26_bvfunc24,theorem,( ! [A,B,C] : ( r2_hidden(A,k3_tarski(k2_tarski(B,k1_tarski(C)))) <=> ( r2_hidden(A,B) | A = C ) ) ), inference(mizar_proof,[status(thm)],[d4_tarski,d2_tarski,d2_tarski,d1_tarski,d4_tarski]), [file(bvfunc24,l26_bvfunc24),interesting(0.72)]). fof(t45_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I,J] : ( ( v1_relat_1(J) & v1_funct_1(J) ) => ! [K,L,M,N,O,P,Q,R,S] : ( J = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,L),k3_cqc_lang(C,M)),k3_cqc_lang(D,N)),k3_cqc_lang(E,O)),k3_cqc_lang(F,P)),k3_cqc_lang(G,Q)),k3_cqc_lang(H,R)),k3_cqc_lang(I,S)),k3_cqc_lang(A,K)) => k1_relat_1(J) = k1_bvfunc24(A,B,C,D,E,F,G,H,I) ) ) ), inference(mizar_proof,[status(thm)],[t22_bvfunc24,t62_enumset1,t68_enumset1,t5_cqc_lang,d1_funct_4,t27_bvfunc24]), [file(bvfunc24,t45_bvfunc24),interesting(0.66)]). fof(t9_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H] : ( ( v1_relat_1(H) & v1_funct_1(H) ) => ! [I,J,K,L,M,N,O] : ( H = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,J),k3_cqc_lang(C,K)),k3_cqc_lang(D,L)),k3_cqc_lang(E,M)),k3_cqc_lang(F,N)),k3_cqc_lang(G,O)),k3_cqc_lang(A,I)) => k1_relat_1(H) = k5_enumset1(A,B,C,D,E,F,G) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_funct_4,t8_bvfunc23,t51_enumset1,t55_enumset1,t56_enumset1]), [file(bvfunc24,t9_bvfunc24),interesting(0.65)]). fof(t22_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : ( ( v1_relat_1(I) & v1_funct_1(I) ) => ! [J,K,L,M,N,O,P,Q] : ( I = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,K),k3_cqc_lang(C,L)),k3_cqc_lang(D,M)),k3_cqc_lang(E,N)),k3_cqc_lang(F,O)),k3_cqc_lang(G,P)),k3_cqc_lang(H,Q)),k3_cqc_lang(A,J)) => k1_relat_1(I) = k6_enumset1(A,B,C,D,E,F,G,H) ) ) ), inference(mizar_proof,[status(thm)],[t9_bvfunc24,t56_enumset1,t61_enumset1,t5_cqc_lang,d1_funct_4,t62_enumset1]), [file(bvfunc24,t22_bvfunc24),interesting(0.65)]). fof(t10_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H] : ( ( v1_relat_1(H) & v1_funct_1(H) ) => ! [I,J,K,L,M,N,O] : ( H = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,J),k3_cqc_lang(C,K)),k3_cqc_lang(D,L)),k3_cqc_lang(E,M)),k3_cqc_lang(F,N)),k3_cqc_lang(G,O)),k3_cqc_lang(A,I)) => k2_relat_1(H) = k5_enumset1(k1_funct_1(H,A),k1_funct_1(H,B),k1_funct_1(H,C),k1_funct_1(H,D),k1_funct_1(H,E),k1_funct_1(H,F),k1_funct_1(H,G)) ) ) ), inference(mizar_proof,[status(thm)],[t9_bvfunc24,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d3_tarski,d5_funct_1,d5_enumset1,d5_enumset1,d3_tarski,d5_enumset1,d10_xboole_0]), [file(bvfunc24,t10_bvfunc24),interesting(0.58)]). fof(t23_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : ( ( v1_relat_1(I) & v1_funct_1(I) ) => ! [J,K,L,M,N,O,P,Q] : ( I = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,K),k3_cqc_lang(C,L)),k3_cqc_lang(D,M)),k3_cqc_lang(E,N)),k3_cqc_lang(F,O)),k3_cqc_lang(G,P)),k3_cqc_lang(H,Q)),k3_cqc_lang(A,J)) => k2_relat_1(I) = k6_enumset1(k1_funct_1(I,A),k1_funct_1(I,B),k1_funct_1(I,C),k1_funct_1(I,D),k1_funct_1(I,E),k1_funct_1(I,F),k1_funct_1(I,G),k1_funct_1(I,H)) ) ) ), inference(mizar_proof,[status(thm)],[t22_bvfunc24,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d3_tarski,d5_funct_1,d6_enumset1,d6_enumset1,d3_tarski,d6_enumset1,d10_xboole_0]), [file(bvfunc24,t23_bvfunc24),interesting(0.57)]). fof(t46_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I,J] : ( ( v1_relat_1(J) & v1_funct_1(J) ) => ! [K,L,M,N,O,P,Q,R,S] : ( J = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,L),k3_cqc_lang(C,M)),k3_cqc_lang(D,N)),k3_cqc_lang(E,O)),k3_cqc_lang(F,P)),k3_cqc_lang(G,Q)),k3_cqc_lang(H,R)),k3_cqc_lang(I,S)),k3_cqc_lang(A,K)) => k2_relat_1(J) = k1_bvfunc24(k1_funct_1(J,A),k1_funct_1(J,B),k1_funct_1(J,C),k1_funct_1(J,D),k1_funct_1(J,E),k1_funct_1(J,F),k1_funct_1(J,G),k1_funct_1(J,H),k1_funct_1(J,I)) ) ) ), inference(mizar_proof,[status(thm)],[t45_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d3_tarski,d5_funct_1,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d1_bvfunc24,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d1_bvfunc24,d10_xboole_0]), [file(bvfunc24,t46_bvfunc24),interesting(0.56)]). fof(t6_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,H,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),I) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t59_enumset1,t99_enumset1,t59_enumset1,t5_bvfunc24]), [file(bvfunc24,t6_bvfunc24),interesting(0.46)]). fof(t1_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,C,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H),I) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_bvfunc_2,t56_enumset1,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,t72_zfmisc_1,t51_enumset1,t42_xboole_1,t67_zfmisc_1,t47_enumset1,t42_xboole_1,t45_enumset1,t42_xboole_1,t72_zfmisc_1,t67_zfmisc_1,t45_enumset1,t47_enumset1,t51_enumset1,t42_xboole_1,t37_xboole_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,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,t8_bvfunc23,t51_enumset1,t55_enumset1,t8_bvfunc23,t51_enumset1,t55_enumset1,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,d4_enumset1,t7_bvfunc23,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d3_tarski,d5_funct_1,d4_enumset1,d4_enumset1,d3_tarski,d4_enumset1,d10_xboole_0,d3_tarski,d4_enumset1,d10_setfam_1,d3_tarski,d4_enumset1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,d3_xboole_0,d3_xboole_0,d4_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d4_enumset1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d4_enumset1,d5_funct_1,d10_setfam_1,d1_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_tarski,d5_funct_1,d4_enumset1,d4_enumset1,d4_enumset1,d1_setfam_1,d3_tarski,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,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,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0]), [file(bvfunc24,t1_bvfunc24),interesting(0.45)]). fof(t2_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,D,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,E),F),G),H),I) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t57_enumset1,t57_enumset1,t1_bvfunc24]), [file(bvfunc24,t2_bvfunc24),interesting(0.45)]). fof(t3_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,E,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),F),G),H),I) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_enumset1,t42_enumset1,t42_enumset1,t43_enumset1,t43_enumset1,t58_enumset1,t1_bvfunc24]), [file(bvfunc24,t3_bvfunc24),interesting(0.45)]). fof(t4_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,F,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),G),H),I) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t57_enumset1,t48_enumset1,t48_enumset1,t57_enumset1,t3_bvfunc24]), [file(bvfunc24,t4_bvfunc24),interesting(0.45)]). fof(t5_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,G,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),H),I) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t58_enumset1,t45_enumset1,t45_enumset1,t58_enumset1,t4_bvfunc24]), [file(bvfunc24,t5_bvfunc24),interesting(0.45)]). fof(t14_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,D,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,E),F),G),H),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_enumset1,t63_enumset1,t13_bvfunc24]), [file(bvfunc24,t14_bvfunc24),interesting(0.43)]). fof(t15_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,E,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),F),G),H),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t64_enumset1,t42_enumset1,t42_enumset1,t64_enumset1,t14_bvfunc24]), [file(bvfunc24,t15_bvfunc24),interesting(0.43)]). fof(t16_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,F,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),G),H),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t63_enumset1,t52_enumset1,t52_enumset1,t63_enumset1,t15_bvfunc24]), [file(bvfunc24,t16_bvfunc24),interesting(0.43)]). fof(t17_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,G,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),H),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t64_enumset1,t48_enumset1,t48_enumset1,t64_enumset1,t16_bvfunc24]), [file(bvfunc24,t17_bvfunc24),interesting(0.43)]). fof(t18_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,H,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t65_enumset1,t45_enumset1,t45_enumset1,t65_enumset1,t17_bvfunc24]), [file(bvfunc24,t18_bvfunc24),interesting(0.43)]). fof(t19_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,I,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),H),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t66_enumset1,t43_enumset1,t43_enumset1,t66_enumset1,t18_bvfunc24]), [file(bvfunc24,t19_bvfunc24),interesting(0.43)]). fof(t42_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,J,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),H),I),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_bvfunc24,t43_enumset1,t43_enumset1,t32_bvfunc24,t41_bvfunc24]), [file(bvfunc24,t42_bvfunc24),interesting(0.43)]). fof(t13_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,C,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_bvfunc_2,t62_enumset1,t42_xboole_1,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,t56_enumset1,t42_xboole_1,t67_zfmisc_1,t51_enumset1,t42_xboole_1,t48_enumset1,t42_xboole_1,t72_zfmisc_1,t43_enumset1,t42_xboole_1,t72_zfmisc_1,t67_zfmisc_1,t67_zfmisc_1,t43_enumset1,t48_enumset1,t51_enumset1,t56_enumset1,t37_xboole_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,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,t9_bvfunc24,t56_enumset1,t61_enumset1,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,d5_enumset1,t8_bvfunc24,d5_enumset1,d5_funct_1,d5_enumset1,d5_enumset1,d5_enumset1,d5_enumset1,d5_enumset1,d5_enumset1,d3_tarski,d5_funct_1,d5_enumset1,d5_enumset1,d3_tarski,d5_enumset1,d5_funct_1,d10_xboole_0,d3_tarski,d5_enumset1,d10_setfam_1,d3_tarski,d5_enumset1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,d3_xboole_0,d3_xboole_0,d5_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d5_enumset1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d5_enumset1,d5_funct_1,d10_setfam_1,d1_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_tarski,d5_funct_1,d5_enumset1,d5_enumset1,d5_enumset1,d1_setfam_1,d3_tarski,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,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,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]), [file(bvfunc24,t13_bvfunc24),interesting(0.42)]). fof(t38_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,F,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),G),H),I),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_bvfunc24,t57_enumset1,t57_enumset1,t28_bvfunc24,t37_bvfunc24]), [file(bvfunc24,t38_bvfunc24),interesting(0.42)]). fof(t39_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,G,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),H),I),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_bvfunc24,t52_enumset1,t52_enumset1,t29_bvfunc24,t38_bvfunc24]), [file(bvfunc24,t39_bvfunc24),interesting(0.42)]). fof(t40_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,H,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),I),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l28_bvfunc24,t48_enumset1,t48_enumset1,l28_bvfunc24,t39_bvfunc24]), [file(bvfunc24,t40_bvfunc24),interesting(0.42)]). fof(t41_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,I,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),H),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_bvfunc24,t45_enumset1,t45_enumset1,t31_bvfunc24,t40_bvfunc24]), [file(bvfunc24,t41_bvfunc24),interesting(0.42)]). fof(t35_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,C,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H),I),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_bvfunc_2,t27_bvfunc24,t42_xboole_1,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,t72_zfmisc_1,t62_enumset1,t42_xboole_1,t67_zfmisc_1,t56_enumset1,t42_xboole_1,t52_enumset1,t42_xboole_1,t45_enumset1,t42_xboole_1,t72_zfmisc_1,t67_zfmisc_1,t72_zfmisc_1,t45_enumset1,t52_enumset1,t56_enumset1,t62_enumset1,t37_xboole_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,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,t22_bvfunc24,t62_enumset1,t68_enumset1,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t15_bvfunc14,t3_yellow14,d6_enumset1,t21_bvfunc24,t15_bvfunc14,t3_yellow14,d6_enumset1,d5_funct_1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d3_tarski,d5_funct_1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d6_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d6_enumset1,d10_xboole_0,d3_tarski,d6_enumset1,d10_setfam_1,d3_tarski,d6_enumset1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,t16_xboole_1,d3_xboole_0,t16_xboole_1,d3_xboole_0,d3_xboole_0,d6_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d6_enumset1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d6_enumset1,d5_funct_1,d10_setfam_1,d1_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_tarski,d5_funct_1,d6_enumset1,d6_enumset1,d6_enumset1,d1_setfam_1,d3_tarski,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,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,d5_setfam_1,d4_xboole_0,d4_partit1,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]), [file(bvfunc24,t35_bvfunc24),interesting(0.41)]). fof(t36_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,D,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,E),F),G),H),I),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t28_bvfunc24,t28_bvfunc24,t35_bvfunc24]), [file(bvfunc24,t36_bvfunc24),interesting(0.41)]). fof(t37_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,E,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),F),G),H),I),J),K) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_bvfunc24,t42_enumset1,t42_enumset1,t29_bvfunc24,t36_bvfunc24]), [file(bvfunc24,t37_bvfunc24),interesting(0.41)]). fof(t7_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ( B = k5_enumset1(C,D,E,F,G,H,I) => ( C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | k5_bvfunc_2(A,I,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),H) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t60_enumset1,t60_enumset1,t6_bvfunc24]), [file(bvfunc24,t7_bvfunc24),interesting(0.30)]). fof(t20_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ( B = k6_enumset1(C,D,E,F,G,H,I,J) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | D = E | D = F | D = G | D = H | D = I | D = J | E = F | E = G | E = H | E = I | E = J | F = G | F = H | F = I | F = J | G = H | G = I | G = J | H = I | H = J | I = J | k5_bvfunc_2(A,J,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),H),I) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t67_enumset1,t67_enumset1,t19_bvfunc24]), [file(bvfunc24,t20_bvfunc24),interesting(0.27)]). fof(t43_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ( B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) => ( C = D | C = E | C = F | C = G | C = H | C = I | C = J | C = K | D = E | D = F | D = G | D = H | D = I | D = J | D = K | E = F | E = G | E = H | E = I | E = J | E = K | F = G | F = H | F = I | F = J | F = K | G = H | G = I | G = J | G = K | H = I | H = J | H = K | I = J | I = K | J = K | k5_bvfunc_2(A,K,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G),H),I),J) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_bvfunc24,t33_bvfunc24,t42_bvfunc24]), [file(bvfunc24,t43_bvfunc24),interesting(0.27)]). fof(t48_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ! [L] : ( m1_subset_1(L,A) => ! [M] : ( m1_subset_1(M,A) => ~ ( v2_bvfunc_2(B,A) & B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) & C != D & C != E & C != F & C != G & C != H & C != I & C != J & C != K & D != E & D != F & D != G & D != H & D != I & D != J & D != K & E != F & E != G & E != H & E != I & E != J & E != K & F != G & F != H & F != I & F != J & F != K & G != H & G != I & G != J & G != K & H != I & H != J & H != K & I != J & I != K & J != K & k22_bvfunc_1(A,L,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H),I),J),K)) = k22_bvfunc_1(A,M,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H),I),J),K)) & r1_xboole_0(k22_bvfunc_1(A,M,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,L,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_bvfunc24,t36_bvfunc24,t45_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,d1_bvfunc24,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,t46_bvfunc24,d3_tarski,d1_bvfunc24,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d1_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,d4_partit1,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,t16_partit1,t16_partit1,t16_partit1,t16_partit1,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,t3_xboole_0,t16_partit1,t16_partit1,t16_partit1,t16_partit1,t16_partit1,t16_partit1,d4_partit1,d6_eqrel_1,t3_xboole_0]), [file(bvfunc24,t48_bvfunc24),interesting(0.18)]). fof(t47_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_eqrel_1(K,A) => ! [L] : ( m1_subset_1(L,A) => ! [M] : ( m1_subset_1(M,A) => ~ ( v2_bvfunc_2(B,A) & B = k1_bvfunc24(C,D,E,F,G,H,I,J,K) & C != D & C != E & C != F & C != G & C != H & C != I & C != J & C != K & D != E & D != F & D != G & D != H & D != I & D != J & D != K & E != F & E != G & E != H & E != I & E != J & E != K & F != G & F != H & F != I & F != J & F != K & G != H & G != I & G != J & G != K & H != I & H != J & H != K & I != J & I != K & J != K & k5_subset_1(A,k22_bvfunc_1(A,M,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H),I),J),K)),k22_bvfunc_1(A,L,C)) = k1_xboole_0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t45_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,t44_bvfunc24,d1_bvfunc24,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,d1_bvfunc24,d5_funct_1,t46_bvfunc24,d3_tarski,d1_bvfunc24,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0]), [file(bvfunc24,t47_bvfunc24),interesting(0.15)]). fof(t11_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_subset_1(J,A) => ! [K] : ( m1_subset_1(K,A) => ~ ( v2_bvfunc_2(B,A) & B = k5_enumset1(C,D,E,F,G,H,I) & C != D & C != E & C != F & C != G & C != H & C != I & D != E & D != F & D != G & D != H & D != I & E != F & E != G & E != H & E != I & F != G & F != H & F != I & G != H & G != I & H != I & r1_xboole_0(k22_bvfunc_1(A,K,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H),I)),k22_bvfunc_1(A,J,C)) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,d5_enumset1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,t10_bvfunc24,d3_tarski,d5_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d7_xboole_0]), [file(bvfunc24,t11_bvfunc24),interesting(0.13)]). fof(t12_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_subset_1(J,A) => ! [K] : ( m1_subset_1(K,A) => ~ ( v2_bvfunc_2(B,A) & B = k5_enumset1(C,D,E,F,G,H,I) & C != D & C != E & C != F & C != G & C != H & C != I & D != E & D != F & D != G & D != H & D != I & E != F & E != G & E != H & E != I & F != G & F != H & F != I & G != H & G != I & H != I & k22_bvfunc_1(A,J,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H),I)) = k22_bvfunc_1(A,K,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H),I)) & r1_xboole_0(k22_bvfunc_1(A,K,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,J,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_bvfunc24,t2_bvfunc24,t9_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,t8_bvfunc24,d5_enumset1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,d5_enumset1,d5_funct_1,t10_bvfunc24,d3_tarski,d5_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d1_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,d4_partit1,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,d4_partit1,t16_partit1,t16_partit1,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,t3_xboole_0,t16_partit1,t16_partit1,t16_partit1,t16_partit1,d6_eqrel_1,t3_xboole_0]), [file(bvfunc24,t12_bvfunc24),interesting(0.02)]). fof(t24_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_subset_1(K,A) => ! [L] : ( m1_subset_1(L,A) => ~ ( v2_bvfunc_2(B,A) & B = k6_enumset1(C,D,E,F,G,H,I,J) & C != D & C != E & C != F & C != G & C != H & C != I & C != J & D != E & D != F & D != G & D != H & D != I & D != J & E != F & E != G & E != H & E != I & E != J & F != G & F != H & F != I & F != J & G != H & G != I & G != J & H != I & H != J & I != J & k5_subset_1(A,k22_bvfunc_1(A,L,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H),I),J)),k22_bvfunc_1(A,K,C)) = k1_xboole_0 ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_bvfunc24,t3_yellow14,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t15_bvfunc14,d6_enumset1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,t23_bvfunc24,d3_tarski,d6_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0]), [file(bvfunc24,t24_bvfunc24),interesting(0.01)]). fof(d4_tarski,definition,( ! [A,B] : ( B = k3_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(C,D) & r2_hidden(D,A) ) ) ) ), file(tarski,d4_tarski), [interesting(0.00)]). fof(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(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [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(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(t8_bvfunc23,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K,L,M] : ( G = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,I),k3_cqc_lang(C,J)),k3_cqc_lang(D,K)),k3_cqc_lang(E,L)),k3_cqc_lang(F,M)),k3_cqc_lang(A,H)) => k1_relat_1(G) = k4_enumset1(A,B,C,D,E,F) ) ) ), file(bvfunc23,t8_bvfunc23), [interesting(0.00)]). fof(t51_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k1_tarski(A),k3_enumset1(B,C,D,E,F)) ), file(enumset1,t51_enumset1), [interesting(0.00)]). fof(t55_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k3_enumset1(A,B,C,D,E),k1_tarski(F)) ), file(enumset1,t55_enumset1), [interesting(0.00)]). fof(t56_enumset1,theorem,( ! [A,B,C,D,E,F,G] : k5_enumset1(A,B,C,D,E,F,G) = k2_xboole_0(k1_tarski(A),k4_enumset1(B,C,D,E,F,G)) ), file(enumset1,t56_enumset1), [interesting(0.00)]). fof(t14_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ), file(funct_4,t14_funct_4), [interesting(0.00)]). fof(t6_cqc_lang,theorem,( ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ), file(cqc_lang,t6_cqc_lang), [interesting(0.00)]). fof(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(t7_bvfunc23,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K,L,M] : ( G = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,I),k3_cqc_lang(C,J)),k3_cqc_lang(D,K)),k3_cqc_lang(E,L)),k3_cqc_lang(F,M)),k3_cqc_lang(A,H)) => ( A = B | A = C | A = D | A = E | A = F | B = C | B = D | B = E | B = F | C = D | C = E | C = F | D = E | D = F | E = F | ( k1_funct_1(G,A) = H & k1_funct_1(G,B) = I & k1_funct_1(G,C) = J & k1_funct_1(G,D) = K & k1_funct_1(G,E) = L & k1_funct_1(G,F) = M ) ) ) ) ), file(bvfunc23,t7_bvfunc23), [interesting(0.00)]). fof(t8_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H] : ( ( v1_relat_1(H) & v1_funct_1(H) ) => ! [I,J,K,L,M,N,O] : ( H = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,J),k3_cqc_lang(C,K)),k3_cqc_lang(D,L)),k3_cqc_lang(E,M)),k3_cqc_lang(F,N)),k3_cqc_lang(G,O)),k3_cqc_lang(A,I)) => ( A = B | A = C | A = D | A = E | A = F | A = G | B = C | B = D | B = E | B = F | B = G | C = D | C = E | C = F | C = G | D = E | D = F | D = G | E = F | E = G | F = G | ( k1_funct_1(H,A) = I & k1_funct_1(H,B) = J & k1_funct_1(H,C) = K & k1_funct_1(H,D) = L & k1_funct_1(H,E) = M & k1_funct_1(H,F) = N & k1_funct_1(H,G) = O ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,t7_bvfunc23,d1_tarski,t12_funct_4,t7_bvfunc23,d1_tarski,t12_funct_4,t7_bvfunc23,d1_tarski,t12_funct_4,t7_bvfunc23,d1_tarski,t12_funct_4,t7_bvfunc23,d1_tarski,t12_funct_4,t7_bvfunc23]), [file(bvfunc24,t8_bvfunc24),interesting(0.00)]). fof(d5_enumset1,definition,( ! [A,B,C,D,E,F,G,H] : ( H = k5_enumset1(A,B,C,D,E,F,G) <=> ! [I] : ( r2_hidden(I,H) <=> ~ ( I != A & I != B & I != C & I != D & I != E & I != F & I != G ) ) ) ), file(enumset1,d5_enumset1), [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(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(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(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(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(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)) ) ) ) ) ), file(bvfunc14,t1_bvfunc14), [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(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(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(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(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(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(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(t45_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_xboole_0(k2_tarski(A,B),k2_tarski(C,D)) ), file(enumset1,t45_enumset1), [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(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(d4_enumset1,definition,( ! [A,B,C,D,E,F,G] : ( G = k4_enumset1(A,B,C,D,E,F) <=> ! [H] : ( r2_hidden(H,G) <=> ~ ( H != A & H != B & H != C & H != D & H != E & H != F ) ) ) ), file(enumset1,d4_enumset1), [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(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(t57_enumset1,theorem,( ! [A,B,C,D,E,F,G] : k5_enumset1(A,B,C,D,E,F,G) = k2_xboole_0(k2_tarski(A,B),k3_enumset1(C,D,E,F,G)) ), file(enumset1,t57_enumset1), [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(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(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(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(t67_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k4_enumset1(A,B,C,D,E,F),k2_tarski(G,H)) ), file(enumset1,t67_enumset1), [interesting(0.00)]). fof(t66_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k3_enumset1(A,B,C,D,E),k1_enumset1(F,G,H)) ), file(enumset1,t66_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(t65_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k2_enumset1(A,B,C,D),k2_enumset1(E,F,G,H)) ), file(enumset1,t65_enumset1), [interesting(0.00)]). fof(t64_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k1_enumset1(A,B,C),k3_enumset1(D,E,F,G,H)) ), file(enumset1,t64_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(t63_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k2_tarski(A,B),k4_enumset1(C,D,E,F,G,H)) ), file(enumset1,t63_enumset1), [interesting(0.00)]). fof(t52_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k2_tarski(A,B),k2_enumset1(C,D,E,F)) ), file(enumset1,t52_enumset1), [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(t62_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k1_tarski(A),k5_enumset1(B,C,D,E,F,G,H)) ), file(enumset1,t62_enumset1), [interesting(0.00)]). fof(t61_enumset1,theorem,( ! [A,B,C,D,E,F,G] : k5_enumset1(A,B,C,D,E,F,G) = k2_xboole_0(k4_enumset1(A,B,C,D,E,F),k1_tarski(G)) ), file(enumset1,t61_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(t21_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I] : ( ( v1_relat_1(I) & v1_funct_1(I) ) => ! [J,K,L,M,N,O,P,Q] : ( I = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,K),k3_cqc_lang(C,L)),k3_cqc_lang(D,M)),k3_cqc_lang(E,N)),k3_cqc_lang(F,O)),k3_cqc_lang(G,P)),k3_cqc_lang(H,Q)),k3_cqc_lang(A,J)) => ( A = B | A = C | A = D | A = E | A = F | A = G | A = H | B = C | B = D | B = E | B = F | B = G | B = H | C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | ( k1_funct_1(I,B) = K & k1_funct_1(I,C) = L & k1_funct_1(I,D) = M & k1_funct_1(I,E) = N & k1_funct_1(I,F) = O & k1_funct_1(I,G) = P ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t12_funct_4,t8_bvfunc24,d1_tarski,t12_funct_4,t8_bvfunc24,d1_tarski,t12_funct_4,t8_bvfunc24,d1_tarski,t12_funct_4,t8_bvfunc24,d1_tarski,t12_funct_4,t8_bvfunc24,d1_tarski,t12_funct_4,t8_bvfunc24]), [file(bvfunc24,t21_bvfunc24),interesting(0.00)]). 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 ) ) ), file(bvfunc14,t15_bvfunc14), [interesting(0.00)]). fof(d6_enumset1,definition,( ! [A,B,C,D,E,F,G,H,I] : ( I = k6_enumset1(A,B,C,D,E,F,G,H) <=> ! [J] : ( r2_hidden(J,I) <=> ~ ( J != A & J != B & J != C & J != D & J != E & J != F & J != G & J != H ) ) ) ), file(enumset1,d6_enumset1), [interesting(0.00)]). fof(t25_bvfunc24,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_eqrel_1(H,A) => ! [I] : ( m1_eqrel_1(I,A) => ! [J] : ( m1_eqrel_1(J,A) => ! [K] : ( m1_subset_1(K,A) => ! [L] : ( m1_subset_1(L,A) => ~ ( v2_bvfunc_2(B,A) & B = k6_enumset1(C,D,E,F,G,H,I,J) & C != D & C != E & C != F & C != G & C != H & C != I & C != J & D != E & D != F & D != G & D != H & D != I & D != J & E != F & E != G & E != H & E != I & E != J & F != G & F != H & F != I & F != J & G != H & G != I & G != J & H != I & H != J & I != J & k22_bvfunc_1(A,K,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H),I),J)) = k22_bvfunc_1(A,L,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H),I),J)) & r1_xboole_0(k22_bvfunc_1(A,L,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,K,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_bvfunc24,t13_bvfunc24,t22_bvfunc24,t3_yellow14,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t21_bvfunc24,t15_bvfunc14,d6_enumset1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,d6_enumset1,d5_funct_1,t23_bvfunc24,d3_tarski,d6_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d1_xboole_0,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,d4_partit1,t16_partit1,t16_partit1,t16_partit1,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,t3_xboole_0,t16_partit1,t16_partit1,t16_partit1,t16_partit1,t16_partit1,d6_eqrel_1,t3_xboole_0]), [file(bvfunc24,t25_bvfunc24),interesting(0.00)]). fof(t26_bvfunc24,theorem,( $true ), file(bvfunc24,t26_bvfunc24), [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(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(d1_bvfunc24,definition,( ! [A,B,C,D,E,F,G,H,I,J] : ( J = k1_bvfunc24(A,B,C,D,E,F,G,H,I) <=> ! [K] : ( r2_hidden(K,J) <=> ~ ( K != A & K != B & K != C & K != D & K != E & K != F & K != G & K != H & K != I ) ) ) ), file(bvfunc24,d1_bvfunc24), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(t2_tarski,theorem,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), [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(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(t59_enumset1,theorem,( ! [A,B,C,D,E,F,G] : k5_enumset1(A,B,C,D,E,F,G) = k2_xboole_0(k2_enumset1(A,B,C,D),k1_enumset1(E,F,G)) ), file(enumset1,t59_enumset1), [interesting(0.00)]). fof(t54_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k2_enumset1(A,B,C,D),k2_tarski(E,F)) ), file(enumset1,t54_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(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(t68_enumset1,theorem,( ! [A,B,C,D,E,F,G,H] : k6_enumset1(A,B,C,D,E,F,G,H) = k2_xboole_0(k5_enumset1(A,B,C,D,E,F,G),k1_tarski(H)) ), file(enumset1,t68_enumset1), [interesting(0.00)]). fof(t44_bvfunc24,theorem,( ! [A,B,C,D,E,F,G,H,I,J] : ( ( v1_relat_1(J) & v1_funct_1(J) ) => ! [K,L,M,N,O,P,Q,R,S] : ( J = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,L),k3_cqc_lang(C,M)),k3_cqc_lang(D,N)),k3_cqc_lang(E,O)),k3_cqc_lang(F,P)),k3_cqc_lang(G,Q)),k3_cqc_lang(H,R)),k3_cqc_lang(I,S)),k3_cqc_lang(A,K)) => ( A = B | A = C | A = D | A = E | A = F | A = G | A = H | A = I | B = C | B = D | B = E | B = F | B = G | B = H | B = I | C = D | C = E | C = F | C = G | C = H | C = I | D = E | D = F | D = G | D = H | D = I | E = F | E = G | E = H | E = I | F = G | F = H | F = I | G = H | G = I | H = I | ( k1_funct_1(J,A) = K & k1_funct_1(J,B) = L & k1_funct_1(J,C) = M & k1_funct_1(J,D) = N & k1_funct_1(J,E) = O & k1_funct_1(J,F) = P & k1_funct_1(J,G) = Q & k1_funct_1(J,H) = R & k1_funct_1(J,I) = S ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,t21_bvfunc24,d1_tarski,t12_funct_4,t21_bvfunc24,d1_tarski,t12_funct_4,t21_bvfunc24,d1_tarski,t12_funct_4,t21_bvfunc24,d1_tarski,t12_funct_4,t21_bvfunc24,d1_tarski,t12_funct_4,t21_bvfunc24,d1_tarski,t12_funct_4,t15_bvfunc14,d1_tarski,t12_funct_4,t3_yellow14]), [file(bvfunc24,t44_bvfunc24),interesting(0.00)]). fof(t60_enumset1,theorem,( ! [A,B,C,D,E,F,G] : k5_enumset1(A,B,C,D,E,F,G) = k2_xboole_0(k3_enumset1(A,B,C,D,E),k2_tarski(F,G)) ), file(enumset1,t60_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(t58_enumset1,theorem,( ! [A,B,C,D,E,F,G] : k5_enumset1(A,B,C,D,E,F,G) = k2_xboole_0(k1_enumset1(A,B,C),k2_enumset1(D,E,F,G)) ), file(enumset1,t58_enumset1), [interesting(0.00)]).