fof(t56_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k5_altcat_4(k1_altcat_4(A)) = k5_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d5_altcat_4,d1_altcat_4,t42_altcat_4,t43_altcat_4,t36_altcat_4,t103_zfmisc_1,d1_altcat_4,d3_tarski,d5_altcat_4,t32_altcat_2,d1_altcat_4,t32_altcat_2,t1_xboole_1,t52_altcat_4,t3_xboole_1,t3_xboole_1,d5_altcat_4,t40_altcat_4,d5_altcat_4,d10_xboole_0,d3_tarski,d5_altcat_4,d11_altcat_2,d2_altcat_2,t52_altcat_4,t32_altcat_2,t52_altcat_4,t40_altcat_4,d5_altcat_4,t3_pboole,t22_altcat_2,t25_altcat_2,t26_altcat_2]), [file(altcat_4,t56_altcat_4),interesting(1.00)]). fof(t57_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k5_altcat_4(k2_altcat_4(A)) = k5_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d5_altcat_4,d2_altcat_4,t41_altcat_4,t44_altcat_4,t36_altcat_4,t103_zfmisc_1,d2_altcat_4,d3_tarski,d5_altcat_4,t32_altcat_2,d2_altcat_4,t32_altcat_2,t1_xboole_1,t52_altcat_4,t3_xboole_1,t3_xboole_1,d5_altcat_4,t40_altcat_4,d5_altcat_4,d10_xboole_0,d3_tarski,d5_altcat_4,d11_altcat_2,d2_altcat_2,t52_altcat_4,t32_altcat_2,t52_altcat_4,t40_altcat_4,d5_altcat_4,t3_pboole,t22_altcat_2,t25_altcat_2,t26_altcat_2]), [file(altcat_4,t57_altcat_4),interesting(1.00)]). fof(t58_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k5_altcat_4(k3_altcat_4(A)) = k5_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d5_altcat_4,d3_altcat_4,t41_altcat_4,t103_zfmisc_1,d3_altcat_4,d3_tarski,d5_altcat_4,t32_altcat_2,d3_altcat_4,t32_altcat_2,t1_xboole_1,t52_altcat_4,t3_xboole_1,t3_xboole_1,d5_altcat_4,t40_altcat_4,d5_altcat_4,d10_xboole_0,d3_tarski,d5_altcat_4,d11_altcat_2,d2_altcat_2,t52_altcat_4,t32_altcat_2,t52_altcat_4,t40_altcat_4,d5_altcat_4,t3_pboole,t22_altcat_2,t25_altcat_2,t26_altcat_2]), [file(altcat_4,t58_altcat_4),interesting(0.95)]). fof(t59_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k5_altcat_4(k4_altcat_4(A)) = k5_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d5_altcat_4,d4_altcat_4,t42_altcat_4,t103_zfmisc_1,d4_altcat_4,d3_tarski,d5_altcat_4,t32_altcat_2,d4_altcat_4,t32_altcat_2,t1_xboole_1,t52_altcat_4,t3_xboole_1,t3_xboole_1,d5_altcat_4,t40_altcat_4,d5_altcat_4,d10_xboole_0,d3_tarski,d5_altcat_4,d11_altcat_2,d2_altcat_2,t52_altcat_4,t32_altcat_2,t52_altcat_4,t40_altcat_4,d5_altcat_4,t3_pboole,t22_altcat_2,t25_altcat_2,t26_altcat_2]), [file(altcat_4,t59_altcat_4),interesting(0.95)]). fof(t55_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k5_altcat_4(k5_altcat_4(A)) = k5_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d5_altcat_4,d5_altcat_4,t103_zfmisc_1,d5_altcat_4,d2_altcat_2,d10_xboole_0,d3_tarski,t52_altcat_4,t52_altcat_4,d5_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t55_altcat_4),interesting(0.75)]). fof(t53_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k1_altcat_4(k1_altcat_4(A)) = k1_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d1_altcat_4,d1_altcat_4,d1_altcat_4,t103_zfmisc_1,d1_altcat_4,d2_altcat_2,d10_xboole_0,d3_tarski,t50_altcat_4,d1_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t53_altcat_4),interesting(0.70)]). fof(t54_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => k2_altcat_4(k2_altcat_4(A)) = k2_altcat_4(A) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_4,d2_altcat_4,d2_altcat_4,t103_zfmisc_1,d2_altcat_4,d2_altcat_2,d10_xboole_0,d3_tarski,t51_altcat_4,d2_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t54_altcat_4),interesting(0.70)]). fof(t34_altcat_4,theorem,( ! [A] : ( l2_altcat_1(A) => ! [B] : ( m1_altcat_2(B,A) => ( ( u1_struct_0(A) = u1_struct_0(B) & u1_altcat_1(A) = u1_altcat_1(B) ) => v2_altcat_2(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_pboole,t97_relat_1,d13_altcat_2]), [file(altcat_4,t34_altcat_4),interesting(0.66)]). fof(t4_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( v5_altcat_3(k8_altcat_1(A,B),A,B,B) & v4_altcat_3(k8_altcat_1(A,B),A,B,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_altcat_3,d19_altcat_1,d19_altcat_1,d7_altcat_3,t24_altcat_1,t24_altcat_1]), [file(altcat_4,t4_altcat_4),interesting(0.61)]). fof(t43_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ~ v3_struct_0(k4_altcat_4(A)) & v2_altcat_1(k4_altcat_4(A)) & v3_altcat_2(k4_altcat_4(A),k1_altcat_4(A)) & m1_altcat_2(k4_altcat_4(A),k1_altcat_4(A)) ) ) ), inference(mizar_proof,[status(thm)],[d4_altcat_4,d1_altcat_4,t119_zfmisc_1,d2_altcat_2,t103_zfmisc_1,d4_altcat_4,d3_tarski,d4_altcat_4,d2_altcat_2,d4_altcat_4,d4_altcat_4,t16_altcat_3,d1_altcat_4,t25_altcat_2,d4_altcat_4,t35_altcat_2,t35_altcat_2,d14_altcat_2]), [file(altcat_4,t43_altcat_4),interesting(0.57)]). fof(t44_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ~ v3_struct_0(k3_altcat_4(A)) & v2_altcat_1(k3_altcat_4(A)) & v3_altcat_2(k3_altcat_4(A),k2_altcat_4(A)) & m1_altcat_2(k3_altcat_4(A),k2_altcat_4(A)) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_4,d2_altcat_4,t119_zfmisc_1,d2_altcat_2,t103_zfmisc_1,d3_altcat_4,d3_tarski,d3_altcat_4,d2_altcat_2,d3_altcat_4,d3_altcat_4,t15_altcat_3,d2_altcat_4,t25_altcat_2,d3_altcat_4,t35_altcat_2,t35_altcat_2,d14_altcat_2]), [file(altcat_4,t44_altcat_4),interesting(0.57)]). fof(t8_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v7_altcat_3(B,A) => v4_altcat_3(D,A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_altcat_3,t27_altcat_3]), [file(altcat_4,t8_altcat_4),interesting(0.57)]). fof(t9_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,C,B)) => ( v6_altcat_3(B,A) => v5_altcat_3(D,A,C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_altcat_3,t25_altcat_3]), [file(altcat_4,t9_altcat_4),interesting(0.57)]). fof(t11_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( v6_altcat_3(B,A) & r2_altcat_3(A,B,C) ) => v6_altcat_3(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_altcat_3,d6_altcat_3,d5_altcat_3,d6_altcat_3,d4_altcat_1,t2_altcat_4,t25_altcat_3]), [file(altcat_4,t11_altcat_4),interesting(0.56)]). fof(t10_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( v7_altcat_3(B,A) & r2_altcat_3(A,C,B) ) => v7_altcat_3(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_altcat_3,d6_altcat_3,d5_altcat_3,d6_altcat_3,d4_altcat_1,t1_altcat_4,t27_altcat_3]), [file(altcat_4,t10_altcat_4),interesting(0.55)]). fof(t15_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l2_altcat_1(B) ) => ! [C] : ( ( v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v17_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => v2_funct_1(k7_functor0(A,B,C,E,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d31_functor0,t106_zfmisc_1,d3_pboole,d2_msualg_3,d31_functor0,d2_msualg_3,d3_pboole,t103_zfmisc_1]), [file(altcat_4,t15_altcat_4),interesting(0.55)]). fof(t35_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_altcat_2(B,A) => ( ( u1_struct_0(A) = u1_struct_0(B) & u1_altcat_1(A) = u1_altcat_1(B) ) => ( v2_altcat_2(B,A) & v3_altcat_2(B,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_altcat_4,d1_struct_0,t34_altcat_4,t29_altcat_2,d14_altcat_2]), [file(altcat_4,t35_altcat_4),interesting(0.50)]). fof(t50_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k1_altcat_4(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k1_altcat_4(A))) => ! [D] : ( m1_subset_1(D,k1_altcat_1(k1_altcat_4(A),B,C)) => ( k1_altcat_1(k1_altcat_4(A),B,C) != k1_xboole_0 => v4_altcat_3(D,k1_altcat_4(A),B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_altcat_4,t34_altcat_2,d1_altcat_4,t37_altcat_4]), [file(altcat_4,t50_altcat_4),interesting(0.48)]). fof(t51_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k2_altcat_4(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k2_altcat_4(A))) => ! [D] : ( m1_subset_1(D,k1_altcat_1(k2_altcat_4(A),B,C)) => ( k1_altcat_1(k2_altcat_4(A),B,C) != k1_xboole_0 => v5_altcat_3(D,k2_altcat_4(A),B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_4,t34_altcat_2,d2_altcat_4,t37_altcat_4]), [file(altcat_4,t51_altcat_4),interesting(0.48)]). fof(t37_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,D)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(B,E,F)) => ( ( E = C & F = D & G = H ) => ( k1_altcat_1(B,E,F) = k1_xboole_0 | ( ( v4_altcat_3(G,A,C,D) => v4_altcat_3(H,B,E,F) ) & ( v5_altcat_3(G,A,C,D) => v5_altcat_3(H,B,E,F) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_altcat_3,t30_altcat_2,t32_altcat_2,t3_xboole_1,t34_altcat_2,t33_altcat_2,t33_altcat_2,d7_altcat_3,d8_altcat_3,t30_altcat_2,t32_altcat_2,t3_xboole_1,t34_altcat_2,t33_altcat_2,t33_altcat_2,d8_altcat_3]), [file(altcat_4,t37_altcat_4),interesting(0.43)]). fof(t12_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( v6_altcat_3(B,A) & v7_altcat_3(C,A) ) => ( k1_altcat_1(A,C,B) = k1_xboole_0 | ( v6_altcat_3(C,A) & v7_altcat_3(B,A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xboole_0,t25_altcat_3,t25_altcat_3,d4_altcat_1,t27_altcat_3,t25_altcat_1,d19_altcat_1,t25_altcat_3,t27_altcat_3,d4_altcat_1,t25_altcat_3,t25_altcat_1,t24_altcat_1,t27_altcat_3]), [file(altcat_4,t12_altcat_4),interesting(0.40)]). fof(t52_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(k5_altcat_4(A))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k5_altcat_4(A))) => ! [D] : ( m1_subset_1(D,k1_altcat_1(k5_altcat_4(A),B,C)) => ( k1_altcat_1(k5_altcat_4(A),B,C) != k1_xboole_0 => ( v3_altcat_3(D,k5_altcat_4(A),B,C) & r2_hidden(k1_altcat_3(k5_altcat_4(A),B,C,D),k1_altcat_1(k5_altcat_4(A),C,B)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,t34_altcat_2,d5_altcat_4,t3_altcat_4,d5_altcat_4,d2_altcat_3,t33_altcat_2,d5_altcat_3,t35_altcat_2,d1_altcat_3,d3_altcat_3,t33_altcat_2,d5_altcat_3,t35_altcat_2,d1_altcat_3,t6_altcat_3]), [file(altcat_4,t52_altcat_4),interesting(0.38)]). fof(t17_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l2_altcat_1(B) ) => ! [C] : ( ( v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D))) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & v18_functor0(C,A,B) & v8_functor0(C,A,B) & ! [G] : ( m1_subset_1(G,k1_altcat_1(A,D,E)) => F != k8_functor0(A,B,C,D,E,G) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_altcat_4,d3_funct_2,d20_functor0,d5_funct_1,d1_funct_2,d17_functor0]), [file(altcat_4,t17_altcat_4),interesting(0.37)]). fof(t6_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => v2_altcat_3(D,A,B,C) ) ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ~ v3_altcat_3(D,A,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_3,d2_altcat_3,t16_altcat_3,t25_altcat_1,d1_altcat_3,t24_altcat_1,d19_altcat_1,d7_altcat_3,d1_altcat_3,t6_altcat_3]), [file(altcat_4,t6_altcat_4),interesting(0.31)]). fof(t18_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( v1_altcat_3(F,A,D,E) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v1_altcat_3(k6_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_3,d2_altcat_3,d1_altcat_3,d24_functor0,t2_functor2,d1_altcat_3]), [file(altcat_4,t18_altcat_4),interesting(0.28)]). fof(t19_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( v2_altcat_3(F,A,D,E) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v2_altcat_3(k6_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_3,d3_altcat_3,d1_altcat_3,d24_functor0,t2_functor2,d1_altcat_3]), [file(altcat_4,t19_altcat_4),interesting(0.28)]). fof(t22_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( v1_altcat_3(F,A,D,E) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v2_altcat_3(k8_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_3,d3_altcat_3,d1_altcat_3,d25_functor0,t13_altcat_4,d1_altcat_3]), [file(altcat_4,t22_altcat_4),interesting(0.27)]). fof(t23_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( v2_altcat_3(F,A,D,E) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v1_altcat_3(k8_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_3,d2_altcat_3,d1_altcat_3,d25_functor0,t13_altcat_4,d1_altcat_3]), [file(altcat_4,t23_altcat_4),interesting(0.27)]). fof(t32_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & v3_altcat_3(k8_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v3_altcat_3(F,A,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_functor0,t6_altcat_3,t30_altcat_4,t31_altcat_4,t6_altcat_3]), [file(altcat_4,t32_altcat_4),interesting(0.25)]). fof(t40_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v3_altcat_2(B,A) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,D)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(B,E,F)) => ( ( E = C & F = D & G = H ) => ( k1_altcat_1(B,E,F) = k1_xboole_0 | k1_altcat_1(B,F,E) = k1_xboole_0 | ( ( v1_altcat_3(H,B,E,F) => v1_altcat_3(G,A,C,D) ) & ( v2_altcat_3(H,B,E,F) => v2_altcat_3(G,A,C,D) ) & ( v3_altcat_3(H,B,E,F) => v3_altcat_3(G,A,C,D) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_3,t34_altcat_2,d2_altcat_3,t38_altcat_4,d3_altcat_3,t34_altcat_2,d3_altcat_3,t38_altcat_4,t32_altcat_2,t3_xboole_1,t5_altcat_3,t6_altcat_3]), [file(altcat_4,t40_altcat_4),interesting(0.24)]). fof(t33_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & r2_altcat_3(B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | r2_altcat_3(A,D,E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_altcat_3,d6_altcat_3,t17_altcat_4,t32_altcat_4]), [file(altcat_4,t33_altcat_4),interesting(0.23)]). fof(t45_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => v4_altcat_3(D,A,B,C) ) ) ) => g2_altcat_1(u1_struct_0(A),u1_altcat_1(A),u2_altcat_1(A)) = k1_altcat_4(A) ) ) ), inference(mizar_proof,[status(thm)],[d1_altcat_4,d1_altcat_4,t103_zfmisc_1,d2_altcat_2,d10_xboole_0,d3_tarski,d1_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t45_altcat_4),interesting(0.21)]). fof(t46_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => v5_altcat_3(D,A,B,C) ) ) ) => g2_altcat_1(u1_struct_0(A),u1_altcat_1(A),u2_altcat_1(A)) = k2_altcat_4(A) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_4,d2_altcat_4,t103_zfmisc_1,d2_altcat_2,d10_xboole_0,d3_tarski,d2_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t46_altcat_4),interesting(0.21)]). fof(t24_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( v3_altcat_3(F,A,D,E) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v3_altcat_3(k8_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d20_functor0,t6_altcat_3,t22_altcat_4,t23_altcat_4,t6_altcat_3]), [file(altcat_4,t24_altcat_4),interesting(0.20)]). fof(t30_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & v1_altcat_3(k8_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v2_altcat_3(F,A,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_3,d1_altcat_3,t14_altcat_4,d3_funct_2,d20_functor0,d5_funct_1,d1_funct_2,d1_funct_2,d3_altcat_3,t15_altcat_4,d17_functor0,t13_altcat_4,d17_functor0,d25_functor0,d17_functor0,d8_funct_1,d1_altcat_3]), [file(altcat_4,t30_altcat_4),interesting(0.20)]). fof(t31_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & v2_altcat_3(k8_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v1_altcat_3(F,A,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_3,d1_altcat_3,t14_altcat_4,d3_funct_2,d20_functor0,d5_funct_1,d1_funct_2,d1_funct_2,d2_altcat_3,t15_altcat_4,d17_functor0,t13_altcat_4,d17_functor0,d25_functor0,d17_functor0,d8_funct_1,d1_altcat_3]), [file(altcat_4,t31_altcat_4),interesting(0.20)]). fof(t26_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & v1_altcat_3(k6_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v1_altcat_3(F,A,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_3,d1_altcat_3,t18_functor1,d3_funct_2,d19_functor0,d5_funct_1,d1_funct_2,d1_funct_2,d2_altcat_3,t19_functor1,d16_functor0,t2_functor2,d16_functor0,d24_functor0,d16_functor0,d8_funct_1,d1_altcat_3]), [file(altcat_4,t26_altcat_4),interesting(0.18)]). fof(t27_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & v2_altcat_3(k6_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v2_altcat_3(F,A,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_3,d1_altcat_3,t18_functor1,d3_funct_2,d19_functor0,d5_funct_1,d1_funct_2,d1_funct_2,d3_altcat_3,t19_functor1,d16_functor0,t2_functor2,d16_functor0,d24_functor0,d16_functor0,d8_funct_1,d1_altcat_3]), [file(altcat_4,t27_altcat_4),interesting(0.18)]). fof(t20_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( v3_altcat_3(F,A,D,E) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v3_altcat_3(k6_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_functor0,t6_altcat_3,t18_altcat_4,t19_altcat_4,t6_altcat_3]), [file(altcat_4,t20_altcat_4),interesting(0.16)]). fof(t28_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & v3_altcat_3(k6_functor0(A,B,C,D,E,F),B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | v3_altcat_3(F,A,D,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_functor0,t6_altcat_3,t26_altcat_4,t27_altcat_4,t6_altcat_3]), [file(altcat_4,t28_altcat_4),interesting(0.16)]). fof(t29_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( v18_functor0(C,A,B) & v17_functor0(C,A,B) & r2_altcat_3(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) => ( k1_altcat_1(A,D,E) = k1_xboole_0 | k1_altcat_1(A,E,D) = k1_xboole_0 | r2_altcat_3(A,D,E) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_altcat_3,d6_altcat_3,t16_altcat_4,t28_altcat_4]), [file(altcat_4,t29_altcat_4),interesting(0.10)]). 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(d2_zfmisc_1,definition,( ! [A,B,C] : ( C = k2_zfmisc_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k4_tarski(E,F) ) ) ) ), file(zfmisc_1,d2_zfmisc_1), [interesting(0.00)]). fof(d4_altcat_1,definition,( ! [A] : ( l1_altcat_1(A) => ( v2_altcat_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,D) != k1_xboole_0 & k1_altcat_1(A,B,D) = k1_xboole_0 ) ) ) ) ) ) ), file(altcat_1,d4_altcat_1), [interesting(0.00)]). fof(l34_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( k1_binop_1(u1_altcat_1(A),B,D) = k1_xboole_0 => k2_zfmisc_1(k1_binop_1(u1_altcat_1(A),C,D),k1_binop_1(u1_altcat_1(A),B,C)) = k1_xboole_0 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_xboole_0,d2_zfmisc_1,d4_altcat_1]), [file(altcat_4,l34_altcat_4),interesting(0.00)]). fof(t27_altcat_3,theorem,( ! [A] : ( l1_altcat_1(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( v7_altcat_3(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ? [D] : ( m1_subset_1(D,k1_altcat_1(A,C,B)) & r2_hidden(D,k1_altcat_1(A,C,B)) & ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,B)) => ( r2_hidden(E,k1_altcat_1(A,C,B)) => D = E ) ) ) ) ) ) ) ), file(altcat_3,t27_altcat_3), [interesting(0.00)]). fof(d6_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_altcat_3(A,B,C) <=> ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ? [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) & v3_altcat_3(D,A,B,C) ) ) ) ) ) ) ), file(altcat_3,d6_altcat_3), [interesting(0.00)]). fof(d5_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v3_altcat_3(D,A,B,C) <=> ( k5_altcat_1(A,C,B,C,k1_altcat_3(A,B,C,D),D) = k8_altcat_1(A,C) & k5_altcat_1(A,B,C,B,D,k1_altcat_3(A,B,C,D)) = k8_altcat_1(A,B) ) ) ) ) ) ) ), file(altcat_3,d5_altcat_3), [interesting(0.00)]). fof(t25_altcat_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,D) != k1_xboole_0 & k1_altcat_1(A,D,E) != k1_xboole_0 & ~ ! [F] : ( m1_subset_1(F,k1_altcat_1(A,B,C)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,D)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(A,D,E)) => k5_altcat_1(A,B,D,E,k5_altcat_1(A,B,C,D,F,G),H) = k5_altcat_1(A,B,C,E,F,k5_altcat_1(A,C,D,E,G,H)) ) ) ) ) ) ) ) ) ) ), file(altcat_1,t25_altcat_1), [interesting(0.00)]). fof(t24_altcat_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k1_altcat_1(A,B,C) != k1_xboole_0 => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => k5_altcat_1(A,B,C,C,D,k8_altcat_1(A,C)) = D ) ) ) ) ) ), file(altcat_1,t24_altcat_1), [interesting(0.00)]). fof(t1_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,B,C)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,B,D)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,D)) => ( ( F = k5_altcat_1(A,B,C,D,E,G) & k5_altcat_1(A,C,D,C,G,k1_altcat_3(A,C,D,G)) = k8_altcat_1(A,C) ) => ( k1_altcat_1(A,B,C) = k1_xboole_0 | k1_altcat_1(A,C,D) = k1_xboole_0 | k1_altcat_1(A,D,C) = k1_xboole_0 | E = k5_altcat_1(A,B,D,C,F,k1_altcat_3(A,C,D,G)) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_altcat_1,t24_altcat_1]), [file(altcat_4,t1_altcat_4),interesting(0.00)]). fof(t25_altcat_3,theorem,( ! [A] : ( l1_altcat_1(A) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( v6_altcat_3(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ? [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) & r2_hidden(D,k1_altcat_1(A,B,C)) & ! [E] : ( m1_subset_1(E,k1_altcat_1(A,B,C)) => ( r2_hidden(E,k1_altcat_1(A,B,C)) => D = E ) ) ) ) ) ) ) ), file(altcat_3,t25_altcat_3), [interesting(0.00)]). fof(d19_altcat_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_altcat_1(A,B,B)) => ( C = k8_altcat_1(A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( k1_altcat_1(A,B,D) != k1_xboole_0 => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,B,D)) => k5_altcat_1(A,B,B,D,C,E) = E ) ) ) ) ) ) ) ), file(altcat_1,d19_altcat_1), [interesting(0.00)]). fof(t2_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,B,C)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,C)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,D,B)) => ( ( F = k5_altcat_1(A,D,B,C,G,E) & k5_altcat_1(A,B,D,B,k1_altcat_3(A,D,B,G),G) = k8_altcat_1(A,B) ) => ( k1_altcat_1(A,D,B) = k1_xboole_0 | k1_altcat_1(A,B,D) = k1_xboole_0 | k1_altcat_1(A,B,C) = k1_xboole_0 | E = k5_altcat_1(A,B,D,C,k1_altcat_3(A,D,B,G),F) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t25_altcat_1,d19_altcat_1]), [file(altcat_4,t2_altcat_4),interesting(0.00)]). fof(d19_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l1_altcat_1(B) ) => ! [C] : ( ( v10_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v8_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & k1_altcat_1(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) = k1_xboole_0 ) ) ) ) ) ) ) ), file(functor0,d19_functor0), [interesting(0.00)]). fof(t6_altcat_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ~ ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v3_altcat_3(D,A,B,C) <=> ( v1_altcat_3(D,A,B,C) & v2_altcat_3(D,A,B,C) ) ) ) ) ) ) ) ), file(altcat_3,t6_altcat_3), [interesting(0.00)]). fof(d2_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v1_altcat_3(D,A,B,C) <=> ? [E] : ( m1_subset_1(E,k1_altcat_1(A,C,B)) & r1_altcat_3(A,B,C,D,E) ) ) ) ) ) ) ), file(altcat_3,d2_altcat_3), [interesting(0.00)]). fof(d1_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,B)) => ( r1_altcat_3(A,B,C,D,E) <=> k5_altcat_1(A,C,B,C,E,D) = k8_altcat_1(A,C) ) ) ) ) ) ) ), file(altcat_3,d1_altcat_3), [interesting(0.00)]). fof(d24_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v1_altcat_2(B) & l2_altcat_1(B) ) => ! [C] : ( ( v8_functor0(C,A,B) & v10_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v13_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & k1_altcat_1(A,E,F) != k1_xboole_0 & ~ ! [G] : ( m1_subset_1(G,k1_altcat_1(A,D,E)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(A,E,F)) => k6_functor0(A,B,C,D,F,k5_altcat_1(A,D,E,F,G,H)) = k5_altcat_1(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E),k3_functor0(A,B,C,F),k6_functor0(A,B,C,D,E,G),k6_functor0(A,B,C,E,F,H)) ) ) ) ) ) ) ) ) ) ) ), file(functor0,d24_functor0), [interesting(0.00)]). fof(t2_functor2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_functor0(A,B,C,D,D,k8_altcat_1(A,D)) = k8_altcat_1(B,k3_functor0(A,B,C,D)) ) ) ) ) ), file(functor2,t2_functor2), [interesting(0.00)]). fof(d3_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v2_altcat_3(D,A,B,C) <=> ? [E] : ( m1_subset_1(E,k1_altcat_1(A,C,B)) & r1_altcat_3(A,C,B,E,D) ) ) ) ) ) ) ), file(altcat_3,d3_altcat_3), [interesting(0.00)]). fof(t21_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v15_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_altcat_3(A,D,E) => r2_altcat_3(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_altcat_3,d19_functor0,d6_altcat_3,d6_altcat_3,t20_altcat_4]), [file(altcat_4,t21_altcat_4),interesting(0.00)]). fof(d20_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l1_altcat_1(B) ) => ! [C] : ( ( v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v8_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & k1_altcat_1(B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) = k1_xboole_0 ) ) ) ) ) ) ) ), file(functor0,d20_functor0), [interesting(0.00)]). fof(d25_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v1_altcat_2(B) & l2_altcat_1(B) ) => ! [C] : ( ( v8_functor0(C,A,B) & v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v14_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & k1_altcat_1(A,E,F) != k1_xboole_0 & ~ ! [G] : ( m1_subset_1(G,k1_altcat_1(A,D,E)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(A,E,F)) => k8_functor0(A,B,C,D,F,k5_altcat_1(A,D,E,F,G,H)) = k5_altcat_1(B,k3_functor0(A,B,C,F),k3_functor0(A,B,C,E),k3_functor0(A,B,C,D),k8_functor0(A,B,C,E,F,H),k8_functor0(A,B,C,D,E,G)) ) ) ) ) ) ) ) ) ) ) ), file(functor0,d25_functor0), [interesting(0.00)]). fof(d17_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l1_altcat_1(B) ) => ! [C] : ( ( v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & k1_altcat_1(B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) != k1_xboole_0 & ~ ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => k8_functor0(A,B,C,D,E,F) = k1_funct_1(k7_functor0(A,B,C,D,E),F) ) ) ) ) ) ) ) ), file(functor0,d17_functor0), [interesting(0.00)]). fof(d21_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( l2_functor0(C,A,B) => ( v12_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k1_funct_1(k4_functor0(A,B,C,D,D),k8_altcat_1(A,D)) = k8_altcat_1(B,k3_functor0(A,B,C,D)) ) ) ) ) ) ), file(functor0,d21_functor0), [interesting(0.00)]). fof(t13_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k8_functor0(A,B,C,D,D,k8_altcat_1(A,D)) = k8_altcat_1(B,k3_functor0(A,B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d17_functor0,d21_functor0]), [file(altcat_4,t13_altcat_4),interesting(0.00)]). fof(t25_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v11_altcat_1(B) & v12_altcat_1(B) & l2_altcat_1(B) ) => ! [C] : ( ( v16_functor0(C,A,B) & m2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_altcat_3(A,D,E) => r2_altcat_3(B,k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_altcat_3,d20_functor0,d6_altcat_3,d6_altcat_3,t24_altcat_4]), [file(altcat_4,t25_altcat_4),interesting(0.00)]). fof(t18_functor1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l2_altcat_1(B) ) => ! [C] : ( ( v10_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v18_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => v2_funct_2(k5_functor0(A,B,C,D,E),k1_altcat_1(A,D,E),k1_altcat_1(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E))) ) ) ) ) ) ) ), file(functor1,t18_functor1), [interesting(0.00)]). fof(d3_funct_2,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ( v2_funct_2(C,A,B) <=> k2_relat_1(C) = B ) ) ), file(funct_2,d3_funct_2), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(d16_functor0,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l1_altcat_1(B) ) => ! [C] : ( ( v10_functor0(C,A,B) & l2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & k1_altcat_1(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E)) != k1_xboole_0 & ~ ! [F] : ( m1_subset_1(F,k1_altcat_1(A,D,E)) => k6_functor0(A,B,C,D,E,F) = k1_funct_1(k5_functor0(A,B,C,D,E),F) ) ) ) ) ) ) ) ), file(functor0,d16_functor0), [interesting(0.00)]). fof(t16_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l2_altcat_1(B) ) => ! [C] : ( ( v10_functor0(C,A,B) & l2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E))) => ~ ( k1_altcat_1(A,D,E) != k1_xboole_0 & v18_functor0(C,A,B) & v8_functor0(C,A,B) & ! [G] : ( m1_subset_1(G,k1_altcat_1(A,D,E)) => F != k6_functor0(A,B,C,D,E,G) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_functor1,d3_funct_2,d19_functor0,d5_funct_1,d1_funct_2,d16_functor0]), [file(altcat_4,t16_altcat_4),interesting(0.00)]). fof(t19_functor1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l2_altcat_1(B) ) => ! [C] : ( ( v10_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v17_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => v2_funct_1(k5_functor0(A,B,C,D,E)) ) ) ) ) ) ) ), file(functor1,t19_functor1), [interesting(0.00)]). fof(d8_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v2_funct_1(A) <=> ! [B,C] : ( ( r2_hidden(B,k1_relat_1(A)) & r2_hidden(C,k1_relat_1(A)) & k1_funct_1(A,B) = k1_funct_1(A,C) ) => B = C ) ) ) ), file(funct_1,d8_funct_1), [interesting(0.00)]). fof(d33_functor0,definition,( ! [A] : ( l1_altcat_1(A) => ! [B] : ( ( ~ v3_struct_0(B) & l1_altcat_1(B) ) => ! [C] : ( l2_functor0(C,A,B) => ( v18_functor0(C,A,B) <=> ? [D] : ( m3_pboole(D,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(A),k7_pboole(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_functor0(A,B,C),u1_altcat_1(B))) & r6_pboole(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),D,u2_functor0(A,B,C)) & v2_msualg_3(D,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(A),k7_pboole(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_functor0(A,B,C),u1_altcat_1(B))) ) ) ) ) ) ), file(functor0,d33_functor0), [interesting(0.00)]). fof(t106_zfmisc_1,theorem,( ! [A,B,C,D] : ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D)) <=> ( r2_hidden(A,C) & r2_hidden(B,D) ) ) ), file(zfmisc_1,t106_zfmisc_1), [interesting(0.00)]). fof(d3_msualg_3,definition,( ! [A,B] : ( m1_pboole(B,A) => ! [C] : ( m1_pboole(C,A) => ! [D] : ( m3_pboole(D,A,B,C) => ( v2_msualg_3(D,A,B,C) <=> ! [E] : ( r2_hidden(E,A) => k2_relat_1(k1_funct_1(D,E)) = k1_funct_1(C,E) ) ) ) ) ) ), file(msualg_3,d3_msualg_3), [interesting(0.00)]). fof(t23_funct_1,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(k5_relat_1(B,C),A) = k1_funct_1(C,k1_funct_1(B,A)) ) ) ) ), file(funct_1,t23_funct_1), [interesting(0.00)]). fof(t24_functor0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l1_altcat_1(B) ) => ! [C] : ( ( v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k2_binop_1(u1_struct_0(A),u1_struct_0(A),k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),u1_functor0(A,B,C),D,E) = k4_tarski(k3_functor0(A,B,C,E),k3_functor0(A,B,C,D)) ) ) ) ) ) ), file(functor0,t24_functor0), [interesting(0.00)]). fof(d4_functor0,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( m1_pboole(D,A) => ! [E] : ( m1_pboole(E,B) => ! [F] : ( m1_pboole(F,A) => ( ( B != k1_xboole_0 => ( m1_functor0(F,A,B,C,D,E) <=> ? [G] : ( ~ v1_xboole_0(G) & ? [H] : ( m1_pboole(H,G) & ? [I] : ( v1_funct_1(I) & v1_funct_2(I,A,G) & m2_relset_1(I,A,G) & C = I & E = H & m3_pboole(F,A,D,k7_pboole(A,G,I,H)) ) ) ) ) ) & ( B = k1_xboole_0 => ( m1_functor0(F,A,B,C,D,E) <=> r6_pboole(A,F,k1_pboole(A)) ) ) ) ) ) ) ) ), file(functor0,d4_functor0), [interesting(0.00)]). fof(t103_zfmisc_1,theorem,( ! [A,B,C,D] : ~ ( r1_tarski(A,k2_zfmisc_1(B,C)) & r2_hidden(D,A) & ! [E,F] : ~ ( r2_hidden(E,B) & r2_hidden(F,C) & D = k4_tarski(E,F) ) ) ), file(zfmisc_1,t103_zfmisc_1), [interesting(0.00)]). fof(t14_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & l2_altcat_1(B) ) => ! [C] : ( ( v11_functor0(C,A,B) & l2_functor0(C,A,B) ) => ( v18_functor0(C,A,B) <=> ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => v2_funct_2(k7_functor0(A,B,C,E,D),k1_altcat_1(A,E,D),k1_altcat_1(B,k3_functor0(A,B,C,D),k3_functor0(A,B,C,E))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d33_functor0,t106_zfmisc_1,d1_funct_2,d3_msualg_3,t23_funct_1,t24_functor0,d3_funct_2,d4_functor0,d33_functor0,d3_msualg_3,t103_zfmisc_1,t106_zfmisc_1,d1_funct_2,d3_funct_2,t24_functor0,t23_funct_1]), [file(altcat_4,t14_altcat_4),interesting(0.00)]). fof(d31_functor0,definition,( ! [A] : ( l1_altcat_1(A) => ! [B] : ( l1_altcat_1(B) => ! [C] : ( l2_functor0(C,A,B) => ( v17_functor0(C,A,B) <=> v1_msualg_3(u2_functor0(A,B,C)) ) ) ) ) ), file(functor0,d31_functor0), [interesting(0.00)]). fof(d3_pboole,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( m1_pboole(B,A) <=> k1_relat_1(B) = A ) ) ), file(pboole,d3_pboole), [interesting(0.00)]). fof(d2_msualg_3,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ( v1_msualg_3(A) <=> ! [B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ( r2_hidden(B,k1_relat_1(A)) & k1_funct_1(A,B) = C ) => v2_funct_1(C) ) ) ) ) ), file(msualg_3,d2_msualg_3), [interesting(0.00)]). fof(t97_relat_1,theorem,( ! [A,B] : ( v1_relat_1(B) => ( r1_tarski(k1_relat_1(B),A) => k7_relat_1(B,A) = B ) ) ), file(relat_1,t97_relat_1), [interesting(0.00)]). fof(d13_altcat_2,definition,( ! [A] : ( l2_altcat_1(A) => ! [B] : ( m1_altcat_2(B,A) => ( v2_altcat_2(B,A) <=> u1_altcat_1(B) = k1_realset1(u1_altcat_1(A),u1_struct_0(B)) ) ) ) ), file(altcat_2,d13_altcat_2), [interesting(0.00)]). fof(d1_struct_0,definition,( ! [A] : ( l1_struct_0(A) => ( v3_struct_0(A) <=> v1_xboole_0(u1_struct_0(A)) ) ) ), file(struct_0,d1_struct_0), [interesting(0.00)]). fof(t29_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_2(B,A) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ( ( C = E & D = F ) => k1_altcat_1(A,C,D) = k1_altcat_1(B,E,F) ) ) ) ) ) ) ) ), file(altcat_2,t29_altcat_2), [interesting(0.00)]). fof(d14_altcat_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_altcat_2(B,A) => ( ( ~ v3_struct_0(B) => ( v3_altcat_2(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( C = D => r2_hidden(k8_altcat_1(A,D),k1_altcat_1(B,C,C)) ) ) ) ) ) & ( v3_struct_0(B) => v3_altcat_2(B,A) ) ) ) ) ), file(altcat_2,d14_altcat_2), [interesting(0.00)]). fof(t33_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ~ ( k1_altcat_1(B,C,D) != k1_xboole_0 & k1_altcat_1(B,D,E) != k1_xboole_0 & ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & ? [H] : ( m1_subset_1(H,u1_struct_0(A)) & F = C & G = D & H = E & ? [I] : ( m1_subset_1(I,k1_altcat_1(A,F,G)) & ? [J] : ( m1_subset_1(J,k1_altcat_1(A,G,H)) & ? [K] : ( m1_subset_1(K,k1_altcat_1(B,C,D)) & ? [L] : ( m1_subset_1(L,k1_altcat_1(B,D,E)) & I = K & J = L & k5_altcat_1(A,F,G,H,I,J) != k5_altcat_1(B,C,D,E,K,L) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(altcat_2,t33_altcat_2), [interesting(0.00)]). fof(t35_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v3_altcat_2(B,A) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( C = D => k8_altcat_1(B,C) = k8_altcat_1(A,D) ) ) ) ) ) ), file(altcat_2,t35_altcat_2), [interesting(0.00)]). fof(t38_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v3_altcat_2(B,A) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,D)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(A,D,C)) => ! [I] : ( m1_subset_1(I,k1_altcat_1(B,E,F)) => ! [J] : ( m1_subset_1(J,k1_altcat_1(B,F,E)) => ( ( E = C & F = D & G = I & H = J ) => ( k1_altcat_1(B,E,F) = k1_xboole_0 | k1_altcat_1(B,F,E) = k1_xboole_0 | ( ( r1_altcat_3(A,C,D,G,H) => r1_altcat_3(B,E,F,I,J) ) & ( r1_altcat_3(B,E,F,I,J) => r1_altcat_3(A,C,D,G,H) ) & ( r1_altcat_3(A,D,C,H,G) => r1_altcat_3(B,F,E,J,I) ) & ( r1_altcat_3(B,F,E,J,I) => r1_altcat_3(A,D,C,H,G) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_altcat_2,d1_altcat_3,t35_altcat_2,d1_altcat_3,t33_altcat_2,d1_altcat_3,t35_altcat_2,d1_altcat_3,t33_altcat_2,d1_altcat_3,t35_altcat_2,d1_altcat_3,t33_altcat_2,d1_altcat_3,t35_altcat_2,d1_altcat_3]), [file(altcat_4,t38_altcat_4),interesting(0.00)]). fof(t5_altcat_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v3_altcat_3(D,A,B,C) => ( v1_altcat_3(D,A,B,C) & v2_altcat_3(D,A,B,C) ) ) ) ) ) ) ), file(altcat_3,t5_altcat_3), [interesting(0.00)]). fof(t39_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v2_altcat_2(B,A) & v3_altcat_2(B,A) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,D)) => ! [H] : ( m1_subset_1(H,k1_altcat_1(B,E,F)) => ( ( E = C & F = D & G = H ) => ( k1_altcat_1(B,E,F) = k1_xboole_0 | k1_altcat_1(B,F,E) = k1_xboole_0 | ( ( v1_altcat_3(G,A,C,D) => v1_altcat_3(H,B,E,F) ) & ( v2_altcat_3(G,A,C,D) => v2_altcat_3(H,B,E,F) ) & ( v3_altcat_3(G,A,C,D) => v3_altcat_3(H,B,E,F) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_altcat_3,t29_altcat_2,d2_altcat_3,t38_altcat_4,d3_altcat_3,t29_altcat_2,d3_altcat_3,t38_altcat_4,t5_altcat_3,t6_altcat_3]), [file(altcat_4,t39_altcat_4),interesting(0.00)]). fof(d1_altcat_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v6_altcat_1(B) & m1_altcat_2(B,A) ) => ( B = k1_altcat_4(A) <=> ( u1_struct_0(B) = u1_struct_0(A) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(B),u1_altcat_1(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,D)) => ( r2_hidden(E,k1_binop_1(u1_altcat_1(B),C,D)) <=> ( k1_altcat_1(A,C,D) != k1_xboole_0 & v4_altcat_3(E,A,C,D) ) ) ) ) ) ) ) ) ) ), file(altcat_4,d1_altcat_4), [interesting(0.00)]). fof(d2_altcat_2,definition,( ! [A,B,C] : ( m1_pboole(C,A) => ! [D] : ( m1_pboole(D,B) => ( r2_altcat_2(A,B,C,D) <=> ( r1_tarski(A,B) & ! [E] : ( r2_hidden(E,A) => r1_tarski(k1_funct_1(C,E),k1_funct_1(D,E)) ) ) ) ) ) ), file(altcat_2,d2_altcat_2), [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(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(t3_pboole,theorem,( ! [A,B] : ( m1_pboole(B,A) => ! [C] : ( m1_pboole(C,A) => ( ! [D] : ( r2_hidden(D,A) => k1_funct_1(B,D) = k1_funct_1(C,D) ) => B = C ) ) ) ), file(pboole,t3_pboole), [interesting(0.00)]). fof(t26_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_altcat_2(B,A) => ( ( u1_struct_0(B) = u1_struct_0(A) & u1_altcat_1(B) = u1_altcat_1(A) ) => g2_altcat_1(u1_struct_0(B),u1_altcat_1(B),u2_altcat_1(B)) = g2_altcat_1(u1_struct_0(A),u1_altcat_1(A),u2_altcat_1(A)) ) ) ) ), file(altcat_2,t26_altcat_2), [interesting(0.00)]). fof(d2_altcat_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v6_altcat_1(B) & m1_altcat_2(B,A) ) => ( B = k2_altcat_4(A) <=> ( u1_struct_0(B) = u1_struct_0(A) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(B),u1_altcat_1(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,D)) => ( r2_hidden(E,k1_binop_1(u1_altcat_1(B),C,D)) <=> ( k1_altcat_1(A,C,D) != k1_xboole_0 & v5_altcat_3(E,A,C,D) ) ) ) ) ) ) ) ) ) ), file(altcat_4,d2_altcat_4), [interesting(0.00)]). fof(d3_altcat_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v6_altcat_1(B) & m1_altcat_2(B,A) ) => ( B = k3_altcat_4(A) <=> ( u1_struct_0(B) = u1_struct_0(A) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(B),u1_altcat_1(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,D)) => ( r2_hidden(E,k1_binop_1(u1_altcat_1(B),C,D)) <=> ( k1_altcat_1(A,C,D) != k1_xboole_0 & k1_altcat_1(A,D,C) != k1_xboole_0 & v1_altcat_3(E,A,C,D) ) ) ) ) ) ) ) ) ) ), file(altcat_4,d3_altcat_4), [interesting(0.00)]). fof(t47_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v1_altcat_3(D,A,B,C) & k1_altcat_1(A,C,B) != k1_xboole_0 ) ) ) ) => g2_altcat_1(u1_struct_0(A),u1_altcat_1(A),u2_altcat_1(A)) = k3_altcat_4(A) ) ) ), inference(mizar_proof,[status(thm)],[d3_altcat_4,d3_altcat_4,t103_zfmisc_1,d2_altcat_2,d10_xboole_0,d3_tarski,d3_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t47_altcat_4),interesting(0.00)]). fof(d4_altcat_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v6_altcat_1(B) & m1_altcat_2(B,A) ) => ( B = k4_altcat_4(A) <=> ( u1_struct_0(B) = u1_struct_0(A) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(B),u1_altcat_1(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,D)) => ( r2_hidden(E,k1_binop_1(u1_altcat_1(B),C,D)) <=> ( k1_altcat_1(A,C,D) != k1_xboole_0 & k1_altcat_1(A,D,C) != k1_xboole_0 & v2_altcat_3(E,A,C,D) ) ) ) ) ) ) ) ) ) ), file(altcat_4,d4_altcat_4), [interesting(0.00)]). fof(t48_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v2_altcat_3(D,A,B,C) & k1_altcat_1(A,C,B) != k1_xboole_0 ) ) ) ) => g2_altcat_1(u1_struct_0(A),u1_altcat_1(A),u2_altcat_1(A)) = k4_altcat_4(A) ) ) ), inference(mizar_proof,[status(thm)],[d4_altcat_4,d4_altcat_4,t103_zfmisc_1,d2_altcat_2,d10_xboole_0,d3_tarski,d4_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t48_altcat_4),interesting(0.00)]). fof(d5_altcat_4,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v6_altcat_1(B) & m1_altcat_2(B,A) ) => ( B = k5_altcat_4(A) <=> ( u1_struct_0(B) = u1_struct_0(A) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(B),u1_altcat_1(A)) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,D)) => ( r2_hidden(E,k1_binop_1(u1_altcat_1(B),C,D)) <=> ( k1_altcat_1(A,C,D) != k1_xboole_0 & k1_altcat_1(A,D,C) != k1_xboole_0 & v3_altcat_3(E,A,C,D) ) ) ) ) ) ) ) ) ) ), file(altcat_4,d5_altcat_4), [interesting(0.00)]). fof(t49_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v3_altcat_3(D,A,B,C) & k1_altcat_1(A,C,B) != k1_xboole_0 ) ) ) ) => g2_altcat_1(u1_struct_0(A),u1_altcat_1(A),u2_altcat_1(A)) = k5_altcat_4(A) ) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d5_altcat_4,t103_zfmisc_1,d2_altcat_2,d10_xboole_0,d3_tarski,d5_altcat_4,t3_pboole,t26_altcat_2]), [file(altcat_4,t49_altcat_4),interesting(0.00)]). fof(d8_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v5_altcat_3(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k1_altcat_1(A,C,E) != k1_xboole_0 => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,C,E)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,C,E)) => ( k5_altcat_1(A,B,C,E,D,F) = k5_altcat_1(A,B,C,E,D,G) => F = G ) ) ) ) ) ) ) ) ) ) ), file(altcat_3,d8_altcat_3), [interesting(0.00)]). fof(d7_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v4_altcat_3(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( k1_altcat_1(A,E,B) != k1_xboole_0 => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,E,B)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,E,B)) => ( k5_altcat_1(A,E,B,C,F,D) = k5_altcat_1(A,E,B,C,G,D) => F = G ) ) ) ) ) ) ) ) ) ) ), file(altcat_3,d7_altcat_3), [interesting(0.00)]). fof(t34_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ( ( C = E & D = F ) => ( k1_altcat_1(B,E,F) = k1_xboole_0 | ! [G] : ( m1_subset_1(G,k1_altcat_1(B,E,F)) => m1_subset_1(G,k1_altcat_1(A,C,D)) ) ) ) ) ) ) ) ) ) ), file(altcat_2,t34_altcat_2), [interesting(0.00)]). fof(t30_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => m1_subset_1(C,u1_struct_0(A)) ) ) ) ), file(altcat_2,t30_altcat_2), [interesting(0.00)]). fof(t32_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & m1_altcat_2(B,A) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(B)) => ! [F] : ( m1_subset_1(F,u1_struct_0(B)) => ( ( C = E & D = F ) => r1_tarski(k1_altcat_1(B,E,F),k1_altcat_1(A,C,D)) ) ) ) ) ) ) ) ), file(altcat_2,t32_altcat_2), [interesting(0.00)]). fof(t3_xboole_1,theorem,( ! [A] : ( r1_tarski(A,k1_xboole_0) => A = k1_xboole_0 ) ), file(xboole_1,t3_xboole_1), [interesting(0.00)]). fof(t3_altcat_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ? [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) & v1_altcat_3(D,A,B,C) & v2_altcat_3(D,A,B,C) & k1_altcat_3(A,C,B,k1_altcat_3(A,B,C,D)) != D ) ) ) ) ) ), file(altcat_3,t3_altcat_3), [interesting(0.00)]). fof(t2_altcat_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ? [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) & v1_altcat_3(D,A,B,C) & v2_altcat_3(D,A,B,C) & ~ ( k5_altcat_1(A,B,C,B,D,k1_altcat_3(A,B,C,D)) = k8_altcat_1(A,B) & k5_altcat_1(A,C,B,C,k1_altcat_3(A,B,C,D),D) = k8_altcat_1(A,C) ) ) ) ) ) ) ), file(altcat_3,t2_altcat_3), [interesting(0.00)]). fof(t3_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v3_altcat_3(D,A,B,C) => ( k1_altcat_1(A,B,C) = k1_xboole_0 | k1_altcat_1(A,C,B) = k1_xboole_0 | v3_altcat_3(k1_altcat_3(A,B,C,D),A,C,B) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_altcat_3,t3_altcat_3,t2_altcat_3,d5_altcat_3,t3_altcat_3,t2_altcat_3]), [file(altcat_4,t3_altcat_4),interesting(0.00)]). fof(t119_zfmisc_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ), file(zfmisc_1,t119_zfmisc_1), [interesting(0.00)]). fof(t25_altcat_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & m1_altcat_2(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v2_altcat_1(C) & m1_altcat_2(C,A) ) => ( ( r1_tarski(u1_struct_0(B),u1_struct_0(C)) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(C),u1_struct_0(C)),u1_altcat_1(B),u1_altcat_1(C)) ) => m1_altcat_2(B,C) ) ) ) ) ), file(altcat_2,t25_altcat_2), [interesting(0.00)]). fof(t42_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ~ v3_struct_0(k5_altcat_4(A)) & v2_altcat_1(k5_altcat_4(A)) & v3_altcat_2(k5_altcat_4(A),k4_altcat_4(A)) & m1_altcat_2(k5_altcat_4(A),k4_altcat_4(A)) ) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d4_altcat_4,t119_zfmisc_1,d2_altcat_2,t103_zfmisc_1,d5_altcat_4,d3_tarski,d5_altcat_4,d2_altcat_2,d5_altcat_4,d5_altcat_4,t5_altcat_3,d4_altcat_4,t25_altcat_2,d5_altcat_4,t35_altcat_2,t35_altcat_2,d14_altcat_2]), [file(altcat_4,t42_altcat_4),interesting(0.00)]). fof(t16_altcat_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ? [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) & v2_altcat_3(D,A,B,C) & ~ v4_altcat_3(D,A,B,C) ) ) ) ) ) ), file(altcat_3,t16_altcat_3), [interesting(0.00)]). fof(t22_altcat_2,theorem,( ! [A] : ( l2_altcat_1(A) => ! [B] : ( l2_altcat_1(B) => ! [C] : ( l2_altcat_1(C) => ( ( m1_altcat_2(A,B) & m1_altcat_2(B,C) ) => m1_altcat_2(A,C) ) ) ) ) ), file(altcat_2,t22_altcat_2), [interesting(0.00)]). fof(d11_altcat_2,definition,( ! [A] : ( l2_altcat_1(A) => ! [B] : ( l2_altcat_1(B) => ( m1_altcat_2(B,A) <=> ( r1_tarski(u1_struct_0(B),u1_struct_0(A)) & r2_altcat_2(k2_zfmisc_1(u1_struct_0(B),u1_struct_0(B)),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_altcat_1(B),u1_altcat_1(A)) & r2_altcat_2(k3_zfmisc_1(u1_struct_0(B),u1_struct_0(B),u1_struct_0(B)),k3_zfmisc_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A)),u2_altcat_1(B),u2_altcat_1(A)) ) ) ) ) ), file(altcat_2,d11_altcat_2), [interesting(0.00)]). fof(t36_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( ( ~ v3_struct_0(B) & v2_altcat_1(B) & v3_altcat_2(B,A) & m1_altcat_2(B,A) ) => ! [C] : ( ( ~ v3_struct_0(C) & v2_altcat_1(C) & v3_altcat_2(C,B) & m1_altcat_2(C,B) ) => ( ~ v3_struct_0(C) & v2_altcat_1(C) & v3_altcat_2(C,A) & m1_altcat_2(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_altcat_2,d11_altcat_2,t35_altcat_2,t35_altcat_2,d14_altcat_2]), [file(altcat_4,t36_altcat_4),interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t41_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ( ~ v3_struct_0(k5_altcat_4(A)) & v2_altcat_1(k5_altcat_4(A)) & v3_altcat_2(k5_altcat_4(A),k3_altcat_4(A)) & m1_altcat_2(k5_altcat_4(A),k3_altcat_4(A)) ) ) ), inference(mizar_proof,[status(thm)],[d5_altcat_4,d3_altcat_4,t119_zfmisc_1,d2_altcat_2,t103_zfmisc_1,d5_altcat_4,d3_tarski,d5_altcat_4,d2_altcat_2,d5_altcat_4,d5_altcat_4,t5_altcat_3,d3_altcat_4,t25_altcat_2,d5_altcat_4,t35_altcat_2,t35_altcat_2,d14_altcat_2]), [file(altcat_4,t41_altcat_4),interesting(0.00)]). fof(t15_altcat_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( k1_altcat_1(A,B,C) != k1_xboole_0 & k1_altcat_1(A,C,B) != k1_xboole_0 & ? [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) & v1_altcat_3(D,A,B,C) & ~ v5_altcat_3(D,A,B,C) ) ) ) ) ) ), file(altcat_3,t15_altcat_3), [interesting(0.00)]). fof(t5_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,C,B)) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,C,B)) => ( ( k5_altcat_1(A,B,C,B,D,F) = k8_altcat_1(A,B) & k5_altcat_1(A,C,B,C,E,D) = k8_altcat_1(A,C) ) => ( k1_altcat_1(A,B,C) = k1_xboole_0 | k1_altcat_1(A,C,B) = k1_xboole_0 | E = F ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_altcat_1,t25_altcat_1,d19_altcat_1]), [file(altcat_4,t5_altcat_4),interesting(0.00)]). fof(d12_altcat_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ( v9_altcat_3(D,A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( v8_altcat_3(E,A) => ! [F] : ( m1_subset_1(F,k1_altcat_1(A,B,E)) => ! [G] : ( m1_subset_1(G,k1_altcat_1(A,E,C)) => D = k5_altcat_1(A,B,E,C,F,G) ) ) ) ) ) ) ) ) ) ), file(altcat_3,d12_altcat_3), [interesting(0.00)]). fof(t7_altcat_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v2_altcat_1(A) & v11_altcat_1(A) & v12_altcat_1(A) & l2_altcat_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_altcat_1(A,B,C)) => ! [E] : ( m1_subset_1(E,k1_altcat_1(A,B,C)) => ( ( v9_altcat_3(D,A,B,C) & v9_altcat_3(E,A,B,C) ) => ( ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ v8_altcat_3(F,A) ) | D = E ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d12_altcat_3,d12_altcat_3]), [file(altcat_4,t7_altcat_4),interesting(0.00)]).