% Mizar problem: t15_robbins1,robbins1,525,12 fof(t15_robbins1,conjecture,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) & l2_robbins1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_robbins1(A,B,k6_lattices(A)) = B ) ) ), inference(mizar_bg_added,[status(thm)],[cc1_relset_1,cc1_robbins1,cc1_tex_2,cc2_robbins1,cc2_tex_2,commutativity_k5_robbins1,commutativity_k6_robbins1,d1_lattices,d3_robbins1,d4_robbins1,dt_k1_binop_1,dt_k1_funct_1,dt_k1_lattices,dt_k1_zfmisc_1,dt_k2_binop_1,dt_k2_zfmisc_1,dt_k3_robbins1,dt_k4_robbins1,dt_k5_robbins1,dt_k6_lattices,dt_k6_robbins1,dt_k7_robbins1,dt_k8_funct_2,dt_l1_robbins1,dt_l1_struct_0,dt_l2_lattices,dt_l2_robbins1,dt_m1_relset_1,dt_m1_subset_1,dt_m2_relset_1,dt_u1_robbins1,dt_u1_struct_0,dt_u2_lattices,existence_l1_robbins1,existence_l1_struct_0,existence_l2_lattices,existence_l2_robbins1,existence_m1_relset_1,existence_m1_subset_1,existence_m2_relset_1,fc1_struct_0,fc2_lattice2,fc3_lattice2,rc2_tex_2,rc3_struct_0,rc3_tex_2,rc4_tex_2,rc5_struct_0,redefinition_k2_binop_1,redefinition_k5_robbins1,redefinition_k6_robbins1,redefinition_k8_funct_2,redefinition_m2_relset_1,t10_robbins1,t14_robbins1,t3_robbins1]), [file(robbins1,t15_robbins1)]). fof(cc1_relset_1,axiom,( ! [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), []). fof(cc1_robbins1,axiom,( ! [A] : ( l2_robbins1(A) => ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) & v6_robbins1(A) ) => ( ~ v3_struct_0(A) & v14_lattices(A) ) ) ) ), file(robbins1,cc1_robbins1), []). fof(cc1_tex_2,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( ~ v1_tex_2(B,k1_zfmisc_1(A)) => ~ v1_xboole_0(B) ) ) ) ), file(tex_2,cc1_tex_2), []). fof(cc2_robbins1,axiom,( ! [A] : ( l2_robbins1(A) => ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) ) => ( ~ v3_struct_0(A) & v6_robbins1(A) ) ) ) ), file(robbins1,cc2_robbins1), []). fof(cc2_tex_2,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) => ( v1_xboole_0(B) => v1_tex_2(B,k1_zfmisc_1(A)) ) ) ) ), file(tex_2,cc2_tex_2), []). fof(commutativity_k5_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => k5_robbins1(A,B,C) = k5_robbins1(A,C,B) ) ), file(robbins1,k5_robbins1), []). fof(commutativity_k6_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => k6_robbins1(A,B,C) = k6_robbins1(A,C,B) ) ), file(robbins1,k6_robbins1), []). fof(d1_lattices,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l2_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_lattices(A,B,C) = k2_binop_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),u2_lattices(A),B,C) ) ) ) ), file(lattices,d1_lattices), []). fof(d3_robbins1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_robbins1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_robbins1(A,B) = k8_funct_2(u1_struct_0(A),u1_struct_0(A),u1_robbins1(A),B) ) ) ), file(robbins1,d3_robbins1), []). fof(d4_robbins1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l2_robbins1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k4_robbins1(A,B,C) = k3_robbins1(A,k1_lattices(A,k3_robbins1(A,B),k3_robbins1(A,C))) ) ) ) ), file(robbins1,d4_robbins1), []). fof(dt_k1_binop_1,axiom,( $true ), file(binop_1,k1_binop_1), []). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), []). fof(dt_k1_lattices,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & l2_lattices(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k1_lattices(A,B,C),u1_struct_0(A)) ) ), file(lattices,k1_lattices), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_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), []). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), []). fof(dt_k3_robbins1,axiom,( ! [A,B] : ( ( ~ v3_struct_0(A) & l1_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) ) => m1_subset_1(k3_robbins1(A,B),u1_struct_0(A)) ) ), file(robbins1,k3_robbins1), []). fof(dt_k4_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k4_robbins1(A,B,C),u1_struct_0(A)) ) ), file(robbins1,k4_robbins1), []). fof(dt_k5_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k5_robbins1(A,B,C),u1_struct_0(A)) ) ), file(robbins1,k5_robbins1), []). fof(dt_k6_lattices,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l2_lattices(A) ) => m1_subset_1(k6_lattices(A),u1_struct_0(A)) ) ), file(lattices,k6_lattices), []). fof(dt_k6_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => m1_subset_1(k6_robbins1(A,B,C),u1_struct_0(A)) ) ), file(robbins1,k6_robbins1), []). fof(dt_k7_robbins1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) & v6_robbins1(A) & l2_robbins1(A) ) => m1_subset_1(k7_robbins1(A),u1_struct_0(A)) ) ), file(robbins1,k7_robbins1), []). fof(dt_k8_funct_2,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & v1_funct_1(C) & v1_funct_2(C,A,B) & m1_relset_1(C,A,B) & m1_subset_1(D,A) ) => m1_subset_1(k8_funct_2(A,B,C,D),B) ) ), file(funct_2,k8_funct_2), []). fof(dt_l1_robbins1,axiom,( ! [A] : ( l1_robbins1(A) => l1_struct_0(A) ) ), file(robbins1,l1_robbins1), []). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), []). fof(dt_l2_lattices,axiom,( ! [A] : ( l2_lattices(A) => l1_struct_0(A) ) ), file(lattices,l2_lattices), []). fof(dt_l2_robbins1,axiom,( ! [A] : ( l2_robbins1(A) => ( l2_lattices(A) & l1_robbins1(A) ) ) ), file(robbins1,l2_robbins1), []). fof(dt_m1_relset_1,axiom,( $true ), file(relset_1,m1_relset_1), []). fof(dt_m1_subset_1,axiom,( $true ), 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), []). fof(dt_u1_robbins1,axiom,( ! [A] : ( l1_robbins1(A) => ( v1_funct_1(u1_robbins1(A)) & v1_funct_2(u1_robbins1(A),u1_struct_0(A),u1_struct_0(A)) & m2_relset_1(u1_robbins1(A),u1_struct_0(A),u1_struct_0(A)) ) ) ), file(robbins1,u1_robbins1), []). fof(dt_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), []). fof(dt_u2_lattices,axiom,( ! [A] : ( l2_lattices(A) => ( v1_funct_1(u2_lattices(A)) & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) & m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ), file(lattices,u2_lattices), []). fof(existence_l1_robbins1,axiom,( ? [A] : l1_robbins1(A) ), file(robbins1,l1_robbins1), []). fof(existence_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), []). fof(existence_l2_lattices,axiom,( ? [A] : l2_lattices(A) ), file(lattices,l2_lattices), []). fof(existence_l2_robbins1,axiom,( ? [A] : l2_robbins1(A) ), file(robbins1,l2_robbins1), []). fof(existence_m1_relset_1,axiom,( ! [A,B] : ? [C] : m1_relset_1(C,A,B) ), 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), []). fof(existence_m2_relset_1,axiom,( ! [A,B] : ? [C] : m2_relset_1(C,A,B) ), file(relset_1,m2_relset_1), []). fof(fc1_struct_0,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ~ v1_xboole_0(u1_struct_0(A)) ) ), file(struct_0,fc1_struct_0), []). fof(fc2_lattice2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & l2_lattices(A) ) => ( v1_relat_1(u2_lattices(A)) & v1_funct_1(u2_lattices(A)) & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) & v1_binop_1(u2_lattices(A),u1_struct_0(A)) & v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ), file(lattice2,fc2_lattice2), []). fof(fc3_lattice2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v5_lattices(A) & l2_lattices(A) ) => ( v1_relat_1(u2_lattices(A)) & v1_funct_1(u2_lattices(A)) & v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) & v2_binop_1(u2_lattices(A),u1_struct_0(A)) & v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ), file(lattice2,fc3_lattice2), []). fof(rc2_tex_2,axiom,( ! [A] : ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_tex_2(B,k1_zfmisc_1(A)) ) ), file(tex_2,rc2_tex_2), []). fof(rc3_struct_0,axiom,( ? [A] : ( l1_struct_0(A) & ~ v3_struct_0(A) ) ), file(struct_0,rc3_struct_0), []). fof(rc3_tex_2,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & v1_tex_2(B,k1_zfmisc_1(A)) ) ) ), file(tex_2,rc3_tex_2), []). fof(rc4_tex_2,axiom,( ! [A] : ( ~ v1_xboole_0(A) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(A)) & ~ v1_xboole_0(B) & ~ v1_tex_2(B,k1_zfmisc_1(A)) ) ) ), file(tex_2,rc4_tex_2), []). fof(rc5_struct_0,axiom,( ! [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), []). fof(redefinition_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) ) => k2_binop_1(A,B,C,D,E,F) = k1_binop_1(D,E,F) ) ), file(binop_1,k2_binop_1), []). fof(redefinition_k5_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => k5_robbins1(A,B,C) = k1_lattices(A,B,C) ) ), file(robbins1,k5_robbins1), []). fof(redefinition_k6_robbins1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & l2_robbins1(A) & m1_subset_1(B,u1_struct_0(A)) & m1_subset_1(C,u1_struct_0(A)) ) => k6_robbins1(A,B,C) = k4_robbins1(A,B,C) ) ), file(robbins1,k6_robbins1), []). fof(redefinition_k8_funct_2,axiom,( ! [A,B,C,D] : ( ( ~ v1_xboole_0(A) & v1_funct_1(C) & v1_funct_2(C,A,B) & m1_relset_1(C,A,B) & m1_subset_1(D,A) ) => k8_funct_2(A,B,C,D) = k1_funct_1(C,D) ) ), file(funct_2,k8_funct_2), []). fof(redefinition_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) <=> m1_relset_1(C,A,B) ) ), file(relset_1,m2_relset_1), []). fof(t10_robbins1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) & v6_robbins1(A) & l2_robbins1(A) ) => ( k3_robbins1(A,k6_lattices(A)) = k7_robbins1(A) & k6_lattices(A) = k3_robbins1(A,k7_robbins1(A)) ) ) ), file(robbins1,t10_robbins1), []). fof(t14_robbins1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) & l2_robbins1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_robbins1(A,B,k7_robbins1(A)) = B ) ) ), file(robbins1,t14_robbins1), []). fof(t3_robbins1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & v5_lattices(A) & v5_robbins1(A) & l2_robbins1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_robbins1(A,k3_robbins1(A,B)) = B ) ) ), file(robbins1,t3_robbins1), []).