% Mizar ND problem: t2_binop_1,binop_1,44,13 fof(dh_c1_3__binop_1,definition, ( ( ~ v1_xboole_0(c1_3__binop_1) => ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(c1_3__binop_1,A),B) & m2_relset_1(C,k2_zfmisc_1(c1_3__binop_1,A),B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(c1_3__binop_1,A),B) & m2_relset_1(D,k2_zfmisc_1(c1_3__binop_1,A),B) ) => ( ! [E] : ( m1_subset_1(E,c1_3__binop_1) => ! [F] : ( m1_subset_1(F,A) => k2_binop_1(c1_3__binop_1,A,B,C,E,F) = k2_binop_1(c1_3__binop_1,A,B,D,E,F) ) ) => C = D ) ) ) ) ) ) => ! [G] : ( ~ v1_xboole_0(G) => ! [H] : ( ~ v1_xboole_0(H) => ! [I] : ( ~ v1_xboole_0(I) => ! [J] : ( ( v1_funct_1(J) & v1_funct_2(J,k2_zfmisc_1(G,H),I) & m2_relset_1(J,k2_zfmisc_1(G,H),I) ) => ! [K] : ( ( v1_funct_1(K) & v1_funct_2(K,k2_zfmisc_1(G,H),I) & m2_relset_1(K,k2_zfmisc_1(G,H),I) ) => ( ! [L] : ( m1_subset_1(L,G) => ! [M] : ( m1_subset_1(M,H) => k2_binop_1(G,H,I,J,L,M) = k2_binop_1(G,H,I,K,L,M) ) ) => J = K ) ) ) ) ) ) ), introduced(definition,[new_symbol(c1_3__binop_1),file(binop_1,c1_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c1_3__binop_1)]). fof(dh_c2_3__binop_1,definition, ( ( ~ v1_xboole_0(c2_3__binop_1) => ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),A) & m2_relset_1(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),A) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),A) & m2_relset_1(C,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),A) ) => ( ! [D] : ( m1_subset_1(D,c1_3__binop_1) => ! [E] : ( m1_subset_1(E,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,A,B,D,E) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,A,C,D,E) ) ) => B = C ) ) ) ) ) => ! [F] : ( ~ v1_xboole_0(F) => ! [G] : ( ~ v1_xboole_0(G) => ! [H] : ( ( v1_funct_1(H) & v1_funct_2(H,k2_zfmisc_1(c1_3__binop_1,F),G) & m2_relset_1(H,k2_zfmisc_1(c1_3__binop_1,F),G) ) => ! [I] : ( ( v1_funct_1(I) & v1_funct_2(I,k2_zfmisc_1(c1_3__binop_1,F),G) & m2_relset_1(I,k2_zfmisc_1(c1_3__binop_1,F),G) ) => ( ! [J] : ( m1_subset_1(J,c1_3__binop_1) => ! [K] : ( m1_subset_1(K,F) => k2_binop_1(c1_3__binop_1,F,G,H,J,K) = k2_binop_1(c1_3__binop_1,F,G,I,J,K) ) ) => H = I ) ) ) ) ) ), introduced(definition,[new_symbol(c2_3__binop_1),file(binop_1,c2_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c2_3__binop_1)]). fof(dh_c3_3__binop_1,definition, ( ( ~ v1_xboole_0(c3_3__binop_1) => ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [C] : ( m1_subset_1(C,c1_3__binop_1) => ! [D] : ( m1_subset_1(D,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,A,C,D) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,B,C,D) ) ) => A = B ) ) ) ) => ! [E] : ( ~ v1_xboole_0(E) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),E) & m2_relset_1(F,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),E) ) => ! [G] : ( ( v1_funct_1(G) & v1_funct_2(G,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),E) & m2_relset_1(G,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),E) ) => ( ! [H] : ( m1_subset_1(H,c1_3__binop_1) => ! [I] : ( m1_subset_1(I,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,E,F,H,I) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,E,G,H,I) ) ) => F = G ) ) ) ) ), introduced(definition,[new_symbol(c3_3__binop_1),file(binop_1,c3_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c3_3__binop_1)]). fof(dh_c4_3__binop_1,definition, ( ( ( v1_funct_1(c4_3__binop_1) & v1_funct_2(c4_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(c4_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [B] : ( m1_subset_1(B,c1_3__binop_1) => ! [C] : ( m1_subset_1(C,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,B,C) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,A,B,C) ) ) => c4_3__binop_1 = A ) ) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(D,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(E,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [F] : ( m1_subset_1(F,c1_3__binop_1) => ! [G] : ( m1_subset_1(G,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,D,F,G) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,E,F,G) ) ) => D = E ) ) ) ), introduced(definition,[new_symbol(c4_3__binop_1),file(binop_1,c4_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c4_3__binop_1)]). fof(dh_c5_3__binop_1,definition, ( ( ( v1_funct_1(c5_3__binop_1) & v1_funct_2(c5_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(c5_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [A] : ( m1_subset_1(A,c1_3__binop_1) => ! [B] : ( m1_subset_1(B,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,A,B) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c5_3__binop_1,A,B) ) ) => c4_3__binop_1 = c5_3__binop_1 ) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(C,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [D] : ( m1_subset_1(D,c1_3__binop_1) => ! [E] : ( m1_subset_1(E,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,D,E) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,C,D,E) ) ) => c4_3__binop_1 = C ) ) ), introduced(definition,[new_symbol(c5_3__binop_1),file(binop_1,c5_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c5_3__binop_1)]). fof(e1_3__binop_1,assumption,( ! [A] : ( m1_subset_1(A,c1_3__binop_1) => ! [B] : ( m1_subset_1(B,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,A,B) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c5_3__binop_1,A,B) ) ) ), introduced(assumption,[file(binop_1,e1_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,e1_3__binop_1)]). fof(reflexivity_r1_tarski,theorem,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), [interesting(0.9),axiom,file(tarski,r1_tarski)]). fof(antisymmetry_r2_hidden,theorem,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), [interesting(0.9),axiom,file(hidden,r2_hidden)]). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), [interesting(0.9),axiom,file(xboole_0,k1_xboole_0)]). fof(fc1_xboole_0,theorem,( v1_xboole_0(k1_xboole_0) ), file(xboole_0,fc1_xboole_0), [interesting(0.9),axiom,file(xboole_0,fc1_xboole_0)]). fof(t1_subset,theorem,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), [interesting(0.9),axiom,file(subset,t1_subset)]). fof(t4_subset,theorem,( ! [A,B,C] : ( ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) ) => m1_subset_1(A,C) ) ), file(subset,t4_subset), [interesting(0.9),axiom,file(subset,t4_subset)]). fof(t5_subset,theorem,( ! [A,B,C] : ~ ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) & v1_xboole_0(C) ) ), file(subset,t5_subset), [interesting(0.9),axiom,file(subset,t5_subset)]). fof(existence_m1_relset_1,axiom,( ! [A,B] : ? [C] : m1_relset_1(C,A,B) ), file(relset_1,m1_relset_1), [interesting(0.9),axiom,file(relset_1,m1_relset_1)]). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), [interesting(0.9),axiom,file(zfmisc_1,k1_zfmisc_1)]). fof(dt_m1_relset_1,axiom,( $true ), file(relset_1,m1_relset_1), [interesting(0.9),axiom,file(relset_1,m1_relset_1)]). fof(dt_c3_3__binop_1,assumption,( ~ v1_xboole_0(c3_3__binop_1) ), introduced(assumption,[file(binop_1,c3_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c3_3__binop_1)]). fof(cc1_relset_1,theorem,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) => v1_relat_1(C) ) ), file(relset_1,cc1_relset_1), [interesting(0.9),axiom,file(relset_1,cc1_relset_1)]). fof(fc1_subset_1,theorem,( ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ), file(subset_1,fc1_subset_1), [interesting(0.9),axiom,file(subset_1,fc1_subset_1)]). fof(fc4_subset_1,theorem,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) ) => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ), file(subset_1,fc4_subset_1), [interesting(0.9),axiom,file(subset_1,fc4_subset_1)]). fof(rc1_subset_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) ) ) ), file(subset_1,rc1_subset_1), [interesting(0.9),axiom,file(subset_1,rc1_subset_1)]). fof(rc1_xboole_0,theorem,( ? [A] : v1_xboole_0(A) ), file(xboole_0,rc1_xboole_0), [interesting(0.9),axiom,file(xboole_0,rc1_xboole_0)]). fof(rc2_subset_1,theorem,( ! [A] : ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & v1_xboole_0(B) ) ), file(subset_1,rc2_subset_1), [interesting(0.9),axiom,file(subset_1,rc2_subset_1)]). fof(rc2_xboole_0,theorem,( ? [A] : ~ v1_xboole_0(A) ), file(xboole_0,rc2_xboole_0), [interesting(0.9),axiom,file(xboole_0,rc2_xboole_0)]). fof(t2_subset,theorem,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), [interesting(0.9),axiom,file(subset,t2_subset)]). fof(t3_subset,theorem,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), [interesting(0.9),axiom,file(subset,t3_subset)]). fof(t6_boole,theorem,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), [interesting(0.9),axiom,file(boole,t6_boole)]). fof(t7_boole,theorem,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), [interesting(0.9),axiom,file(boole,t7_boole)]). fof(t8_boole,theorem,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), [interesting(0.9),axiom,file(boole,t8_boole)]). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(existence_m2_relset_1,axiom,( ! [A,B] : ? [C] : m2_relset_1(C,A,B) ), file(relset_1,m2_relset_1), [interesting(0.9),axiom,file(relset_1,m2_relset_1)]). fof(redefinition_m2_relset_1,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) <=> m1_relset_1(C,A,B) ) ), file(relset_1,m2_relset_1), [interesting(0.9),axiom,file(relset_1,m2_relset_1)]). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), [interesting(0.9),axiom,file(funct_1,k1_funct_1)]). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), [interesting(0.9),axiom,file(zfmisc_1,k2_zfmisc_1)]). fof(dt_k4_tarski,axiom,( $true ), file(tarski,k4_tarski), [interesting(0.9),axiom,file(tarski,k4_tarski)]). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(dt_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ), file(relset_1,m2_relset_1), [interesting(0.9),axiom,file(relset_1,m2_relset_1)]). fof(dt_c1_3__binop_1,assumption,( ~ v1_xboole_0(c1_3__binop_1) ), introduced(assumption,[file(binop_1,c1_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c1_3__binop_1)]). fof(dt_c2_3__binop_1,assumption,( ~ v1_xboole_0(c2_3__binop_1) ), introduced(assumption,[file(binop_1,c2_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c2_3__binop_1)]). fof(dt_c4_3__binop_1,assumption, ( v1_funct_1(c4_3__binop_1) & v1_funct_2(c4_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(c4_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ), introduced(assumption,[file(binop_1,c4_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c4_3__binop_1)]). fof(dt_c5_3__binop_1,assumption, ( v1_funct_1(c5_3__binop_1) & v1_funct_2(c5_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(c5_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ), introduced(assumption,[file(binop_1,c5_3__binop_1)]), [interesting(0.8),axiom,file(binop_1,c5_3__binop_1)]). fof(fc1_zfmisc_1,theorem,( ! [A,B] : ~ v1_xboole_0(k4_tarski(A,B)) ), file(zfmisc_1,fc1_zfmisc_1), [interesting(0.9),axiom,file(zfmisc_1,fc1_zfmisc_1)]). fof(dh_c1_3_1__binop_1,definition, ( ( m1_subset_1(c1_3_1__binop_1,c1_3__binop_1) => ! [A] : ( m1_subset_1(A,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) ) ) => ! [B] : ( m1_subset_1(B,c1_3__binop_1) => ! [C] : ( m1_subset_1(C,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(B,C)) = k1_funct_1(c5_3__binop_1,k4_tarski(B,C)) ) ) ), introduced(definition,[new_symbol(c1_3_1__binop_1),file(binop_1,c1_3_1__binop_1)]), [interesting(0.65),axiom,file(binop_1,c1_3_1__binop_1)]). fof(dh_c2_3_1__binop_1,definition, ( ( m1_subset_1(c2_3_1__binop_1,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) ) => ! [A] : ( m1_subset_1(A,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) ) ), introduced(definition,[new_symbol(c2_3_1__binop_1),file(binop_1,c2_3_1__binop_1)]), [interesting(0.65),axiom,file(binop_1,c2_3_1__binop_1)]). fof(dt_k1_binop_1,axiom,( $true ), file(binop_1,k1_binop_1), [interesting(0.9),axiom,file(binop_1,k1_binop_1)]). fof(d1_binop_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B,C] : k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C)) ) ), file(binop_1,d1_binop_1), [interesting(0.9),axiom,file(binop_1,d1_binop_1)]). fof(redefinition_k2_binop_1,definition,( ! [A,B,C,D,E,F] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,B),C) & m1_relset_1(D,k2_zfmisc_1(A,B),C) & m1_subset_1(E,A) & m1_subset_1(F,B) ) => k2_binop_1(A,B,C,D,E,F) = k1_binop_1(D,E,F) ) ), file(binop_1,k2_binop_1), [interesting(0.9),axiom,file(binop_1,k2_binop_1)]). fof(dt_k2_binop_1,axiom,( ! [A,B,C,D,E,F] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) & v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,B),C) & m1_relset_1(D,k2_zfmisc_1(A,B),C) & m1_subset_1(E,A) & m1_subset_1(F,B) ) => m1_subset_1(k2_binop_1(A,B,C,D,E,F),C) ) ), file(binop_1,k2_binop_1), [interesting(0.9),axiom,file(binop_1,k2_binop_1)]). fof(dt_c1_3_1__binop_1,assumption,( m1_subset_1(c1_3_1__binop_1,c1_3__binop_1) ), introduced(assumption,[file(binop_1,c1_3_1__binop_1)]), [interesting(0.65),axiom,file(binop_1,c1_3_1__binop_1)]). fof(dt_c2_3_1__binop_1,assumption,( m1_subset_1(c2_3_1__binop_1,c2_3__binop_1) ), introduced(assumption,[file(binop_1,c2_3_1__binop_1)]), [interesting(0.65),axiom,file(binop_1,c2_3_1__binop_1)]). fof(e1_3_1__binop_1,plain, ( k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,c1_3_1__binop_1,c2_3_1__binop_1) = k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) & k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c5_3__binop_1,c1_3_1__binop_1,c2_3_1__binop_1) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c2_3_1__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1])],[reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,dt_k1_zfmisc_1,cc1_relset_1,fc1_subset_1,fc1_xboole_0,rc1_subset_1,rc2_subset_1,t1_subset,t3_subset,t4_subset,t5_subset,existence_m1_relset_1,existence_m1_subset_1,existence_m2_relset_1,redefinition_m2_relset_1,dt_k1_binop_1,dt_k2_zfmisc_1,dt_m1_relset_1,dt_m1_subset_1,dt_m2_relset_1,fc4_subset_1,rc1_xboole_0,rc2_xboole_0,t2_subset,t6_boole,t7_boole,t8_boole,d1_binop_1,redefinition_k2_binop_1,dt_k1_funct_1,dt_k2_binop_1,dt_k4_tarski,dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c2_3_1__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,fc1_zfmisc_1]), [interesting(0.65),file(binop_1,e1_3_1__binop_1),[file(binop_1,e1_3_1__binop_1)]]). fof(e2_3_1__binop_1,plain,( k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) ), inference(mizar_by,[status(thm),assumptions([dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c2_3_1__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1])],[reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,dt_k1_zfmisc_1,cc1_relset_1,fc1_subset_1,fc1_xboole_0,rc1_subset_1,rc2_subset_1,t1_subset,t3_subset,t4_subset,t5_subset,existence_m1_relset_1,existence_m2_relset_1,redefinition_m2_relset_1,dt_k1_binop_1,dt_k2_zfmisc_1,dt_m1_relset_1,dt_m2_relset_1,fc4_subset_1,rc1_xboole_0,rc2_xboole_0,t2_subset,t6_boole,t7_boole,t8_boole,d1_binop_1,existence_m1_subset_1,redefinition_k2_binop_1,dt_k1_funct_1,dt_k2_binop_1,dt_k4_tarski,dt_m1_subset_1,dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c2_3_1__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,fc1_zfmisc_1,e1_3_1__binop_1,e1_3__binop_1]), [interesting(0.65),file(binop_1,e2_3_1__binop_1),[file(binop_1,e2_3_1__binop_1)]]). fof(i3_3_1__binop_1,theorem,( $true ), introduced(tautology,[file(binop_1,i3_3_1__binop_1)]), [interesting(0.65),trivial,file(binop_1,i3_3_1__binop_1)]). fof(i2_3_1__binop_1,plain,( k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) ), inference(conclusion,[status(thm),assumptions([dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c2_3_1__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1])],[e2_3_1__binop_1,i3_3_1__binop_1]), [interesting(0.65),file(binop_1,i2_3_1__binop_1),[file(binop_1,i2_3_1__binop_1)]]). fof(i2_3_1_tmp__binop_1,plain, ( m1_subset_1(c2_3_1__binop_1,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,c2_3_1__binop_1)) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1]),discharge_asm(discharge,[dt_c2_3_1__binop_1])],[dt_c2_3_1__binop_1,i2_3_1__binop_1]), [interesting(0.65),i1_3_1__binop_1]). fof(i1_3_1__binop_1,plain,( ! [A] : ( m1_subset_1(A,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) ) ), inference(let,[status(thm),assumptions([dt_c1_3__binop_1,dt_c1_3_1__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1])],[i2_3_1_tmp__binop_1,dh_c2_3_1__binop_1]), [interesting(0.65),file(binop_1,i1_3_1__binop_1),[file(binop_1,i1_3_1__binop_1)]]). fof(i1_3_1_tmp__binop_1,plain, ( m1_subset_1(c1_3_1__binop_1,c1_3__binop_1) => ! [A] : ( m1_subset_1(A,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) = k1_funct_1(c5_3__binop_1,k4_tarski(c1_3_1__binop_1,A)) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1]),discharge_asm(discharge,[dt_c1_3_1__binop_1])],[dt_c1_3_1__binop_1,i1_3_1__binop_1]), [interesting(0.8),e2_3__binop_1]). fof(e2_3__binop_1,plain,( ! [A] : ( m1_subset_1(A,c1_3__binop_1) => ! [B] : ( m1_subset_1(B,c2_3__binop_1) => k1_funct_1(c4_3__binop_1,k4_tarski(A,B)) = k1_funct_1(c5_3__binop_1,k4_tarski(A,B)) ) ) ), inference(let,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1])],[i1_3_1_tmp__binop_1,dh_c1_3_1__binop_1]), [interesting(0.8),file(binop_1,e2_3__binop_1),[file(binop_1,e2_3__binop_1)]]). fof(t120_funct_2,theorem,( ! [A,B,C,D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,B),C) & m2_relset_1(D,k2_zfmisc_1(A,B),C) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => ( ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,B) => k1_funct_1(D,k4_tarski(F,G)) = k1_funct_1(E,k4_tarski(F,G)) ) ) => D = E ) ) ) ), file(funct_2,t120_funct_2), [interesting(0.9),axiom,file(funct_2,t120_funct_2)]). fof(e3_3__binop_1,plain,( c4_3__binop_1 = c5_3__binop_1 ), inference(mizar_by,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1])],[reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,fc1_xboole_0,t1_subset,t4_subset,t5_subset,existence_m1_relset_1,dt_k1_zfmisc_1,dt_m1_relset_1,dt_c3_3__binop_1,cc1_relset_1,fc1_subset_1,fc4_subset_1,rc1_subset_1,rc1_xboole_0,rc2_subset_1,rc2_xboole_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_m1_subset_1,existence_m2_relset_1,redefinition_m2_relset_1,dt_k1_funct_1,dt_k2_zfmisc_1,dt_k4_tarski,dt_m1_subset_1,dt_m2_relset_1,dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,fc1_zfmisc_1,e2_3__binop_1,t120_funct_2]), [interesting(0.8),file(binop_1,e3_3__binop_1),[file(binop_1,e3_3__binop_1)]]). fof(i4_3__binop_1,theorem,( $true ), introduced(tautology,[file(binop_1,i4_3__binop_1)]), [interesting(0.8),trivial,file(binop_1,i4_3__binop_1)]). fof(i3_3__binop_1,plain,( c4_3__binop_1 = c5_3__binop_1 ), inference(conclusion,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1,e1_3__binop_1])],[e3_3__binop_1,i4_3__binop_1]), [interesting(0.8),file(binop_1,i3_3__binop_1),[file(binop_1,i3_3__binop_1)]]). fof(i2_3__binop_1,plain, ( ! [A] : ( m1_subset_1(A,c1_3__binop_1) => ! [B] : ( m1_subset_1(B,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,A,B) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c5_3__binop_1,A,B) ) ) => c4_3__binop_1 = c5_3__binop_1 ), inference(discharge_asm,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,dt_c4_3__binop_1,dt_c5_3__binop_1]),discharge_asm(discharge,[e1_3__binop_1])],[e1_3__binop_1,i3_3__binop_1]), [interesting(0.8),file(binop_1,i2_3__binop_1),[file(binop_1,i2_3__binop_1)]]). fof(i2_3_tmp__binop_1,plain, ( ( v1_funct_1(c4_3__binop_1) & v1_funct_2(c4_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(c4_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & v1_funct_1(c5_3__binop_1) & v1_funct_2(c5_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(c5_3__binop_1,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [A] : ( m1_subset_1(A,c1_3__binop_1) => ! [B] : ( m1_subset_1(B,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c4_3__binop_1,A,B) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,c5_3__binop_1,A,B) ) ) => c4_3__binop_1 = c5_3__binop_1 ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1]),discharge_asm(discharge,[dt_c4_3__binop_1,dt_c5_3__binop_1])],[dt_c4_3__binop_1,dt_c5_3__binop_1,i2_3__binop_1]), [interesting(0.8),i1_3__binop_1]). fof(i1_3__binop_1,plain,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [C] : ( m1_subset_1(C,c1_3__binop_1) => ! [D] : ( m1_subset_1(D,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,A,C,D) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,B,C,D) ) ) => A = B ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1])],[i2_3_tmp__binop_1,dh_c4_3__binop_1,dh_c5_3__binop_1]), [interesting(0.8),file(binop_1,i1_3__binop_1),[file(binop_1,i1_3__binop_1)]]). fof(i1_3_tmp__binop_1,plain, ( ( ~ v1_xboole_0(c1_3__binop_1) & ~ v1_xboole_0(c2_3__binop_1) & ~ v1_xboole_0(c3_3__binop_1) ) => ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(A,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) & m2_relset_1(B,k2_zfmisc_1(c1_3__binop_1,c2_3__binop_1),c3_3__binop_1) ) => ( ! [C] : ( m1_subset_1(C,c1_3__binop_1) => ! [D] : ( m1_subset_1(D,c2_3__binop_1) => k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,A,C,D) = k2_binop_1(c1_3__binop_1,c2_3__binop_1,c3_3__binop_1,B,C,D) ) ) => A = B ) ) ) ), inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1])],[dt_c1_3__binop_1,dt_c2_3__binop_1,dt_c3_3__binop_1,i1_3__binop_1]), [interesting(1),t2_binop_1]). fof(t2_binop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,B),C) & m2_relset_1(D,k2_zfmisc_1(A,B),C) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,k2_zfmisc_1(A,B),C) & m2_relset_1(E,k2_zfmisc_1(A,B),C) ) => ( ! [F] : ( m1_subset_1(F,A) => ! [G] : ( m1_subset_1(G,B) => k2_binop_1(A,B,C,D,F,G) = k2_binop_1(A,B,C,E,F,G) ) ) => D = E ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([])],[i1_3_tmp__binop_1,dh_c1_3__binop_1,dh_c2_3__binop_1,dh_c3_3__binop_1]), [interesting(1),file(binop_1,t2_binop_1),[file(binop_1,t2_binop_1)]]).