% Mizar ND problem: t1_autalg_1,autalg_1,39,14 fof(dh_c1_1__autalg_1,definition, ( ( ( ~ v3_struct_0(c1_1__autalg_1) & v6_unialg_1(c1_1__autalg_1) & v7_unialg_1(c1_1__autalg_1) & v8_unialg_1(c1_1__autalg_1) & l1_unialg_1(c1_1__autalg_1) ) => r4_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ) => ! [A] : ( ( ~ v3_struct_0(A) & v6_unialg_1(A) & v7_unialg_1(A) & v8_unialg_1(A) & l1_unialg_1(A) ) => r4_alg_1(A,A,k6_partfun1(u1_struct_0(A))) ) ), introduced(definition,[new_symbol(c1_1__autalg_1),file(autalg_1,c1_1__autalg_1)]), [interesting(0.8),axiom,file(autalg_1,c1_1__autalg_1)]). fof(cc2_funct_2,theorem,( ! [A,B,C] : ( m1_relset_1(C,A,B) => ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & v3_funct_2(C,A,B) ) => ( v1_funct_1(C) & v2_funct_1(C) & v1_funct_2(C,A,B) & v2_funct_2(C,A,B) ) ) ) ), file(funct_2,cc2_funct_2), [interesting(0.9),axiom,file(funct_2,cc2_funct_2)]). fof(cc3_funct_2,theorem,( ! [A,B,C] : ( m1_relset_1(C,A,B) => ( ( v1_funct_1(C) & v2_funct_1(C) & v1_funct_2(C,A,B) & v2_funct_2(C,A,B) ) => ( v1_funct_1(C) & v1_funct_2(C,A,B) & v3_funct_2(C,A,B) ) ) ) ), file(funct_2,cc3_funct_2), [interesting(0.9),axiom,file(funct_2,cc3_funct_2)]). fof(rc1_partfun1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) & v1_xboole_0(A) ) ), file(partfun1,rc1_partfun1), [interesting(0.9),axiom,file(partfun1,rc1_partfun1)]). fof(rc2_funct_2,theorem,( ! [A] : ? [B] : ( m1_relset_1(B,A,A) & v1_relat_1(B) & v1_funct_1(B) & v2_funct_1(B) & v1_funct_2(B,A,A) & v2_funct_2(B,A,A) & v3_funct_2(B,A,A) ) ), file(funct_2,rc2_funct_2), [interesting(0.9),axiom,file(funct_2,rc2_funct_2)]). fof(rc3_funct_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ), file(funct_1,rc3_funct_1), [interesting(0.9),axiom,file(funct_1,rc3_funct_1)]). fof(cc1_funct_1,theorem,( ! [A] : ( v1_xboole_0(A) => v1_funct_1(A) ) ), file(funct_1,cc1_funct_1), [interesting(0.9),axiom,file(funct_1,cc1_funct_1)]). fof(cc1_partfun1,theorem,( ! [A] : ( ( v1_relat_1(A) & v3_relat_2(A) & v8_relat_2(A) ) => ( v1_relat_1(A) & v1_relat_2(A) ) ) ), file(partfun1,cc1_partfun1), [interesting(0.9),axiom,file(partfun1,cc1_partfun1)]). fof(cc2_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) => ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ) ), file(funct_1,cc2_funct_1), [interesting(0.9),axiom,file(funct_1,cc2_funct_1)]). fof(cc4_funct_2,theorem,( ! [A,B] : ( m1_relset_1(B,A,A) => ( ( v1_funct_1(B) & v1_partfun1(B,A,A) & v1_relat_2(B) & v1_funct_2(B,A,A) ) => ( v1_funct_1(B) & v2_funct_1(B) & v1_funct_2(B,A,A) & v2_funct_2(B,A,A) & v3_funct_2(B,A,A) ) ) ) ), file(funct_2,cc4_funct_2), [interesting(0.9),axiom,file(funct_2,cc4_funct_2)]). fof(cc5_funct_2,theorem,( ! [A,B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_relset_1(C,A,B) => ( ( v1_funct_1(C) & v1_funct_2(C,A,B) ) => ( v1_funct_1(C) & v1_partfun1(C,A,B) & v1_funct_2(C,A,B) ) ) ) ) ), file(funct_2,cc5_funct_2), [interesting(0.9),axiom,file(funct_2,cc5_funct_2)]). fof(cc6_funct_2,theorem,( ! [A,B] : ( ( ~ v1_xboole_0(A) & ~ v1_xboole_0(B) ) => ! [C] : ( m1_relset_1(C,A,B) => ( ( v1_funct_1(C) & v1_funct_2(C,A,B) ) => ( v1_funct_1(C) & ~ v1_xboole_0(C) & v1_partfun1(C,A,B) & v1_funct_2(C,A,B) ) ) ) ) ), file(funct_2,cc6_funct_2), [interesting(0.9),axiom,file(funct_2,cc6_funct_2)]). 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_funct_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) ) ), file(funct_1,rc1_funct_1), [interesting(0.9),axiom,file(funct_1,rc1_funct_1)]). fof(rc1_funct_2,theorem,( ! [A,B] : ? [C] : ( m1_relset_1(C,A,B) & v1_relat_1(C) & v1_funct_1(C) & v1_funct_2(C,A,B) ) ), file(funct_2,rc1_funct_2), [interesting(0.9),axiom,file(funct_2,rc1_funct_2)]). 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_funct_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) ), file(funct_1,rc2_funct_1), [interesting(0.9),axiom,file(funct_1,rc2_funct_1)]). fof(rc2_partfun1,theorem,( ! [A,B] : ? [C] : ( m1_relset_1(C,A,B) & v1_relat_1(C) & v1_funct_1(C) ) ), file(partfun1,rc2_partfun1), [interesting(0.9),axiom,file(partfun1,rc2_partfun1)]). 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(rc3_partfun1,theorem,( ! [A] : ? [B] : ( m1_relset_1(B,A,A) & v1_relat_1(B) & v1_relat_2(B) & v3_relat_2(B) & v4_relat_2(B) & v8_relat_2(B) & v1_partfun1(B,A,A) ) ), file(partfun1,rc3_partfun1), [interesting(0.9),axiom,file(partfun1,rc3_partfun1)]). fof(rc5_struct_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & ~ v1_xboole_0(B) ) ) ), file(struct_0,rc5_struct_0), [interesting(0.9),axiom,file(struct_0,rc5_struct_0)]). 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_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), [interesting(0.9),axiom,file(zfmisc_1,k2_zfmisc_1)]). fof(dt_k6_relat_1,axiom,( ! [A] : v1_relat_1(k6_relat_1(A)) ), file(relat_1,k6_relat_1), [interesting(0.9),axiom,file(relat_1,k6_relat_1)]). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), [interesting(0.9),axiom,file(struct_0,l1_struct_0)]). 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_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(cc1_funct_2,theorem,( ! [A,B,C] : ( m1_relset_1(C,A,B) => ( ( v1_funct_1(C) & v1_partfun1(C,A,B) ) => ( v1_funct_1(C) & v1_funct_2(C,A,B) ) ) ) ), file(funct_2,cc1_funct_2), [interesting(0.9),axiom,file(funct_2,cc1_funct_2)]). 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_struct_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ~ v1_xboole_0(u1_struct_0(A)) ) ), file(struct_0,fc1_struct_0), [interesting(0.9),axiom,file(struct_0,fc1_struct_0)]). 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(fc2_funct_1,theorem,( ! [A] : ( v1_relat_1(k6_relat_1(A)) & v1_funct_1(k6_relat_1(A)) ) ), file(funct_1,fc2_funct_1), [interesting(0.9),axiom,file(funct_1,fc2_funct_1)]). fof(fc2_partfun1,theorem,( ! [A] : ( v1_relat_1(k6_relat_1(A)) & v1_funct_1(k6_relat_1(A)) & v1_relat_2(k6_relat_1(A)) & v3_relat_2(k6_relat_1(A)) & v4_relat_2(k6_relat_1(A)) & v8_relat_2(k6_relat_1(A)) ) ), file(partfun1,fc2_partfun1), [interesting(0.9),axiom,file(partfun1,fc2_partfun1)]). fof(rc3_struct_0,theorem,( ? [A] : ( l1_struct_0(A) & ~ v3_struct_0(A) ) ), file(struct_0,rc3_struct_0), [interesting(0.9),axiom,file(struct_0,rc3_struct_0)]). fof(redefinition_k6_partfun1,definition,( ! [A] : k6_partfun1(A) = k6_relat_1(A) ), file(partfun1,k6_partfun1), [interesting(0.9),axiom,file(partfun1,k6_partfun1)]). 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_k6_partfun1,axiom,( ! [A] : ( v1_partfun1(k6_partfun1(A),A,A) & m2_relset_1(k6_partfun1(A),A,A) ) ), file(partfun1,k6_partfun1), [interesting(0.9),axiom,file(partfun1,k6_partfun1)]). fof(dt_l1_unialg_1,axiom,( ! [A] : ( l1_unialg_1(A) => l1_struct_0(A) ) ), file(unialg_1,l1_unialg_1), [interesting(0.9),axiom,file(unialg_1,l1_unialg_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_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), [interesting(0.9),axiom,file(struct_0,u1_struct_0)]). fof(dt_c1_1__autalg_1,assumption, ( ~ v3_struct_0(c1_1__autalg_1) & v6_unialg_1(c1_1__autalg_1) & v7_unialg_1(c1_1__autalg_1) & v8_unialg_1(c1_1__autalg_1) & l1_unialg_1(c1_1__autalg_1) ), introduced(assumption,[file(autalg_1,c1_1__autalg_1)]), [interesting(0.8),axiom,file(autalg_1,c1_1__autalg_1)]). fof(d4_alg_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v6_unialg_1(A) & v7_unialg_1(A) & v8_unialg_1(A) & l1_unialg_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v6_unialg_1(B) & v7_unialg_1(B) & v8_unialg_1(B) & l1_unialg_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( r4_alg_1(A,B,C) <=> ( r2_alg_1(A,B,C) & r3_alg_1(A,B,C) ) ) ) ) ) ), file(alg_1,d4_alg_1), [interesting(0.9),axiom,file(alg_1,d4_alg_1)]). fof(d2_alg_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v6_unialg_1(A) & v7_unialg_1(A) & v8_unialg_1(A) & l1_unialg_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v6_unialg_1(B) & v7_unialg_1(B) & v8_unialg_1(B) & l1_unialg_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( r2_alg_1(A,B,C) <=> ( r1_alg_1(A,B,C) & v2_funct_1(C) ) ) ) ) ) ), file(alg_1,d2_alg_1), [interesting(0.9),axiom,file(alg_1,d2_alg_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(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(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_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), [interesting(0.9),axiom,file(struct_0,l1_struct_0)]). 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(existence_l1_unialg_1,axiom,( ? [A] : l1_unialg_1(A) ), file(unialg_1,l1_unialg_1), [interesting(0.9),axiom,file(unialg_1,l1_unialg_1)]). fof(t6_alg_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v6_unialg_1(A) & v7_unialg_1(A) & v8_unialg_1(A) & l1_unialg_1(A) ) => r1_alg_1(A,A,k6_partfun1(u1_struct_0(A))) ) ), file(alg_1,t6_alg_1), [interesting(0.9),axiom,file(alg_1,t6_alg_1)]). fof(e1_1_1__autalg_1,plain,( r1_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(mizar_by,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc2_funct_2,reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc1_xboole_0,rc1_funct_2,rc1_partfun1,rc3_funct_1,t1_subset,t4_subset,t5_subset,existence_m1_relset_1,existence_m1_subset_1,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_1,cc1_funct_2,cc1_partfun1,cc1_relset_1,cc2_funct_1,fc1_subset_1,fc4_subset_1,rc1_funct_1,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_partfun1,rc2_subset_1,rc2_xboole_0,rc3_partfun1,rc5_struct_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_l1_struct_0,existence_m2_relset_1,redefinition_m2_relset_1,dt_k6_relat_1,dt_l1_struct_0,dt_m2_relset_1,fc1_struct_0,fc2_funct_1,fc2_partfun1,rc3_struct_0,existence_l1_unialg_1,redefinition_k6_partfun1,dt_k6_partfun1,dt_l1_unialg_1,dt_u1_struct_0,dt_c1_1__autalg_1,t6_alg_1]), [interesting(0.65),file(autalg_1,e1_1_1__autalg_1),[file(autalg_1,e1_1_1__autalg_1)]]). fof(e2_1_1__autalg_1,plain,( v2_funct_1(k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(mizar_by,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc2_funct_2,reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc1_xboole_0,rc1_funct_2,t1_subset,t4_subset,t5_subset,existence_m1_relset_1,existence_m1_subset_1,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_1,cc1_funct_2,cc1_partfun1,cc1_relset_1,cc2_funct_1,fc1_subset_1,fc4_subset_1,rc1_funct_1,rc1_partfun1,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_partfun1,rc2_subset_1,rc2_xboole_0,rc3_funct_1,rc3_partfun1,rc5_struct_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_l1_struct_0,existence_l1_unialg_1,existence_m2_relset_1,redefinition_m2_relset_1,dt_k6_relat_1,dt_l1_struct_0,dt_l1_unialg_1,dt_m2_relset_1,fc1_struct_0,fc2_funct_1,fc2_partfun1,rc3_struct_0,redefinition_k6_partfun1,dt_k6_partfun1,dt_u1_struct_0,dt_c1_1__autalg_1]), [interesting(0.65),file(autalg_1,e2_1_1__autalg_1),[file(autalg_1,e2_1_1__autalg_1)]]). fof(i2_1_1__autalg_1,theorem,( $true ), introduced(tautology,[file(autalg_1,i2_1_1__autalg_1)]), [interesting(0.65),trivial,file(autalg_1,i2_1_1__autalg_1)]). fof(i1_1_1__autalg_1,plain,( v2_funct_1(k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(conclusion,[status(thm),assumptions([dt_c1_1__autalg_1])],[e2_1_1__autalg_1,i2_1_1__autalg_1]), [interesting(0.65),file(autalg_1,i1_1_1__autalg_1),[file(autalg_1,i1_1_1__autalg_1)]]). fof(e1_1__autalg_1,plain,( r2_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(conclusion,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc2_funct_2,cc1_funct_1,cc1_partfun1,cc2_funct_1,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc4_subset_1,rc1_funct_1,rc1_funct_2,rc1_partfun1,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_partfun1,rc2_subset_1,rc2_xboole_0,rc3_funct_1,rc3_partfun1,rc5_struct_0,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_k6_relat_1,dt_l1_struct_0,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_2,cc1_relset_1,fc1_struct_0,fc1_subset_1,fc2_funct_1,fc2_partfun1,rc3_struct_0,redefinition_k6_partfun1,redefinition_m2_relset_1,dt_k6_partfun1,dt_l1_unialg_1,dt_m2_relset_1,dt_u1_struct_0,dt_c1_1__autalg_1,d2_alg_1,e1_1_1__autalg_1,i1_1_1__autalg_1]), [interesting(0.8),file(autalg_1,e1_1__autalg_1),[file(autalg_1,e1_1__autalg_1)]]). fof(dt_k2_relat_1,axiom,( $true ), file(relat_1,k2_relat_1), [interesting(0.9),axiom,file(relat_1,k2_relat_1)]). fof(d3_alg_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v6_unialg_1(A) & v7_unialg_1(A) & v8_unialg_1(A) & l1_unialg_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v6_unialg_1(B) & v7_unialg_1(B) & v8_unialg_1(B) & l1_unialg_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) => ( r3_alg_1(A,B,C) <=> ( r1_alg_1(A,B,C) & k2_relat_1(C) = u1_struct_0(B) ) ) ) ) ) ), file(alg_1,d3_alg_1), [interesting(0.9),axiom,file(alg_1,d3_alg_1)]). fof(e1_1_2__autalg_1,plain,( r1_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(mizar_by,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc2_funct_2,reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc1_xboole_0,rc1_funct_2,rc1_partfun1,rc3_funct_1,t1_subset,t4_subset,t5_subset,existence_m1_relset_1,existence_m1_subset_1,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_1,cc1_funct_2,cc1_partfun1,cc1_relset_1,cc2_funct_1,fc1_subset_1,fc4_subset_1,rc1_funct_1,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_partfun1,rc2_subset_1,rc2_xboole_0,rc3_partfun1,rc5_struct_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_l1_struct_0,existence_m2_relset_1,redefinition_m2_relset_1,dt_k6_relat_1,dt_l1_struct_0,dt_m2_relset_1,fc1_struct_0,fc2_funct_1,fc2_partfun1,rc3_struct_0,existence_l1_unialg_1,redefinition_k6_partfun1,dt_k6_partfun1,dt_l1_unialg_1,dt_u1_struct_0,dt_c1_1__autalg_1,t6_alg_1]), [interesting(0.65),file(autalg_1,e1_1_2__autalg_1),[file(autalg_1,e1_1_2__autalg_1)]]). fof(dt_k1_relat_1,axiom,( $true ), file(relat_1,k1_relat_1), [interesting(0.9),axiom,file(relat_1,k1_relat_1)]). fof(t71_relat_1,theorem,( ! [A] : ( k1_relat_1(k6_relat_1(A)) = A & k2_relat_1(k6_relat_1(A)) = A ) ), file(relat_1,t71_relat_1), [interesting(0.9),axiom,file(relat_1,t71_relat_1)]). fof(e2_1_2__autalg_1,plain,( k2_relat_1(k6_partfun1(u1_struct_0(c1_1__autalg_1))) = u1_struct_0(c1_1__autalg_1) ), inference(mizar_by,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc2_funct_2,reflexivity_r1_tarski,antisymmetry_r2_hidden,dt_k1_xboole_0,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc1_xboole_0,rc1_funct_2,rc1_partfun1,rc3_funct_1,t1_subset,t4_subset,t5_subset,existence_m1_relset_1,existence_m1_subset_1,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_1,cc1_funct_2,cc1_relset_1,cc2_funct_1,fc1_subset_1,fc4_subset_1,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_partfun1,rc2_subset_1,rc2_xboole_0,rc3_partfun1,rc5_struct_0,t2_subset,t3_subset,t6_boole,t7_boole,t8_boole,existence_l1_struct_0,existence_l1_unialg_1,existence_m2_relset_1,redefinition_m2_relset_1,dt_l1_struct_0,dt_l1_unialg_1,dt_m2_relset_1,cc1_partfun1,fc1_struct_0,rc1_funct_1,rc3_struct_0,redefinition_k6_partfun1,dt_k1_relat_1,dt_k2_relat_1,dt_k6_partfun1,dt_k6_relat_1,dt_u1_struct_0,dt_c1_1__autalg_1,fc2_funct_1,fc2_partfun1,t71_relat_1]), [interesting(0.65),file(autalg_1,e2_1_2__autalg_1),[file(autalg_1,e2_1_2__autalg_1)]]). fof(i2_1_2__autalg_1,theorem,( $true ), introduced(tautology,[file(autalg_1,i2_1_2__autalg_1)]), [interesting(0.65),trivial,file(autalg_1,i2_1_2__autalg_1)]). fof(i1_1_2__autalg_1,plain,( k2_relat_1(k6_partfun1(u1_struct_0(c1_1__autalg_1))) = u1_struct_0(c1_1__autalg_1) ), inference(conclusion,[status(thm),assumptions([dt_c1_1__autalg_1])],[e2_1_2__autalg_1,i2_1_2__autalg_1]), [interesting(0.65),file(autalg_1,i1_1_2__autalg_1),[file(autalg_1,i1_1_2__autalg_1)]]). fof(e2_1__autalg_1,plain,( r3_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(conclusion,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc1_partfun1,rc2_funct_2,rc3_funct_1,cc1_funct_1,cc1_partfun1,cc2_funct_1,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc4_subset_1,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_subset_1,rc2_xboole_0,rc3_partfun1,rc5_struct_0,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_k6_relat_1,dt_l1_struct_0,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_2,cc1_relset_1,fc1_struct_0,fc1_subset_1,fc2_funct_1,fc2_partfun1,rc1_funct_1,rc1_funct_2,rc2_partfun1,rc3_struct_0,redefinition_k6_partfun1,redefinition_m2_relset_1,dt_k2_relat_1,dt_k6_partfun1,dt_l1_unialg_1,dt_m2_relset_1,dt_u1_struct_0,dt_c1_1__autalg_1,d3_alg_1,e1_1_2__autalg_1,i1_1_2__autalg_1]), [interesting(0.8),file(autalg_1,e2_1__autalg_1),[file(autalg_1,e2_1__autalg_1)]]). fof(i3_1__autalg_1,theorem,( $true ), introduced(tautology,[file(autalg_1,i3_1__autalg_1)]), [interesting(0.8),trivial,file(autalg_1,i3_1__autalg_1)]). fof(i2_1__autalg_1,plain,( r3_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(conclusion,[status(thm),assumptions([dt_c1_1__autalg_1])],[e2_1__autalg_1,i3_1__autalg_1]), [interesting(0.8),file(autalg_1,i2_1__autalg_1),[file(autalg_1,i2_1__autalg_1)]]). fof(i1_1__autalg_1,plain,( r4_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(conclusion,[status(thm),assumptions([dt_c1_1__autalg_1])],[cc2_funct_2,cc3_funct_2,rc1_partfun1,rc2_funct_2,rc3_funct_1,cc1_funct_1,cc1_partfun1,cc2_funct_1,cc4_funct_2,cc5_funct_2,cc6_funct_2,fc4_subset_1,rc1_funct_1,rc1_funct_2,rc1_subset_1,rc1_xboole_0,rc2_funct_1,rc2_partfun1,rc2_subset_1,rc2_xboole_0,rc3_partfun1,rc5_struct_0,dt_k1_zfmisc_1,dt_k2_zfmisc_1,dt_k6_relat_1,dt_l1_struct_0,dt_m1_relset_1,dt_m1_subset_1,cc1_funct_2,cc1_relset_1,fc1_struct_0,fc1_subset_1,fc2_funct_1,fc2_partfun1,rc3_struct_0,redefinition_k6_partfun1,redefinition_m2_relset_1,dt_k6_partfun1,dt_l1_unialg_1,dt_m2_relset_1,dt_u1_struct_0,dt_c1_1__autalg_1,d4_alg_1,e1_1__autalg_1,i2_1__autalg_1]), [interesting(0.8),file(autalg_1,i1_1__autalg_1),[file(autalg_1,i1_1__autalg_1)]]). fof(i1_1_tmp__autalg_1,plain, ( ( ~ v3_struct_0(c1_1__autalg_1) & v6_unialg_1(c1_1__autalg_1) & v7_unialg_1(c1_1__autalg_1) & v8_unialg_1(c1_1__autalg_1) & l1_unialg_1(c1_1__autalg_1) ) => r4_alg_1(c1_1__autalg_1,c1_1__autalg_1,k6_partfun1(u1_struct_0(c1_1__autalg_1))) ), inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_1__autalg_1])],[dt_c1_1__autalg_1,i1_1__autalg_1]), [interesting(1),t1_autalg_1]). fof(t1_autalg_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v6_unialg_1(A) & v7_unialg_1(A) & v8_unialg_1(A) & l1_unialg_1(A) ) => r4_alg_1(A,A,k6_partfun1(u1_struct_0(A))) ) ), inference(let,[status(thm),assumptions([])],[i1_1_tmp__autalg_1,dh_c1_1__autalg_1]), [interesting(1),file(autalg_1,t1_autalg_1),[file(autalg_1,t1_autalg_1)]]).