fof(t25_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_bvfunc13,t20_bvfunc_2]), [file(bvfunc13,t25_bvfunc13),interesting(1.00)]). fof(t22_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_bvfunc13,t21_bvfunc_2,t21_bvfunc11]), [file(bvfunc13,t22_bvfunc13),interesting(0.96)]). fof(t28_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t28_bvfunc13),interesting(0.87)]). fof(t46_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t28_bvfunc13]), [file(bvfunc13,t46_bvfunc13),interesting(0.87)]). fof(t43_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t25_bvfunc13]), [file(bvfunc13,t43_bvfunc13),interesting(0.86)]). fof(t2_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bvfunc_2,d15_bvfunc_1,d1_t_1topsp,d1_t_1topsp,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d19_bvfunc_1,t43_margrel1,d5_valuat_1,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,t41_margrel1,d5_valuat_1]), [file(bvfunc13,t2_bvfunc13),interesting(0.83)]). fof(t40_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t22_bvfunc13]), [file(bvfunc13,t40_bvfunc13),interesting(0.82)]). fof(t58_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t21_bvfunc_2,t22_bvfunc13]), [file(bvfunc13,t58_bvfunc13),interesting(0.82)]). fof(t19_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_bvfunc13,t21_bvfunc_2,t20_bvfunc_2]), [file(bvfunc13,t19_bvfunc13),interesting(0.81)]). fof(t37_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t19_bvfunc13]), [file(bvfunc13,t37_bvfunc13),interesting(0.81)]). fof(t55_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t21_bvfunc_2,t19_bvfunc13]), [file(bvfunc13,t55_bvfunc13),interesting(0.81)]). fof(t3_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t2_bvfunc13]), [file(bvfunc13,t3_bvfunc13),interesting(0.75)]). fof(t11_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d15_bvfunc_1,d5_valuat_1,t41_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d20_bvfunc_1,d1_t_1topsp,d1_t_1topsp,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,t41_margrel1,d5_valuat_1]), [file(bvfunc13,t11_bvfunc13),interesting(0.74)]). fof(t16_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t16_bvfunc13),interesting(0.73)]). fof(t32_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t11_bvfunc13]), [file(bvfunc13,t32_bvfunc13),interesting(0.73)]). fof(t50_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t21_bvfunc_2,t11_bvfunc13]), [file(bvfunc13,t50_bvfunc13),interesting(0.73)]). fof(t31_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d9_bvfunc_2,d9_bvfunc_2,d10_bvfunc_2,d15_bvfunc_1,d1_t_1topsp,d19_bvfunc_1,t43_margrel1,d5_valuat_1,t41_margrel1,d20_bvfunc_1,t43_margrel1,d1_t_1topsp,d19_bvfunc_1,t43_margrel1,d20_bvfunc_1,t41_margrel1,d5_valuat_1]), [file(bvfunc13,t31_bvfunc13),interesting(0.66)]). fof(t42_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t21_bvfunc_2,t24_bvfunc13]), [file(bvfunc13,t42_bvfunc13),interesting(0.57)]). fof(t61_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_bvfunc11,t15_bvfunc11]), [file(bvfunc13,t61_bvfunc13),interesting(0.51)]). fof(t24_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_bvfunc13,t20_bvfunc_2]), [file(bvfunc13,t24_bvfunc13),interesting(0.47)]). fof(t18_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_bvfunc13,t21_bvfunc11,t21_bvfunc_2,t20_bvfunc_2]), [file(bvfunc13,t18_bvfunc13),interesting(0.43)]). fof(t27_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc13,t20_bvfunc_2]), [file(bvfunc13,t27_bvfunc13),interesting(0.43)]). fof(t57_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t21_bvfunc_2,t21_bvfunc13]), [file(bvfunc13,t57_bvfunc13),interesting(0.43)]). fof(t1_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,D)),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_partit_2,t21_bvfunc_2,t8_bvfunc11,t11_partit_2]), [file(bvfunc13,t1_bvfunc13),interesting(0.41)]). fof(t62_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t24_bvfunc13]), [file(bvfunc13,t62_bvfunc13),interesting(0.40)]). fof(t21_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t21_bvfunc13),interesting(0.35)]). fof(t26_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_bvfunc13,t20_bvfunc_2]), [file(bvfunc13,t26_bvfunc13),interesting(0.35)]). fof(t45_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t27_bvfunc13]), [file(bvfunc13,t45_bvfunc13),interesting(0.35)]). fof(t17_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_bvfunc13,t21_bvfunc_2,t20_bvfunc_2]), [file(bvfunc13,t17_bvfunc13),interesting(0.34)]). fof(t36_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t21_bvfunc_2,t18_bvfunc13]), [file(bvfunc13,t36_bvfunc13),interesting(0.34)]). fof(t54_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t18_bvfunc13]), [file(bvfunc13,t54_bvfunc13),interesting(0.34)]). fof(t7_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_bvfunc_2,t17_partit_2,t8_bvfunc11,t13_partit_2,t11_partit_2]), [file(bvfunc13,t7_bvfunc13),interesting(0.30)]). fof(t44_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t21_bvfunc_2,t26_bvfunc13]), [file(bvfunc13,t44_bvfunc13),interesting(0.29)]). fof(t53_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_bvfunc11,t17_bvfunc13]), [file(bvfunc13,t53_bvfunc13),interesting(0.29)]). fof(t15_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_bvfunc13,t21_bvfunc_2,t21_bvfunc11]), [file(bvfunc13,t15_bvfunc13),interesting(0.28)]). fof(t10_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_partit_2,t8_bvfunc11,t15_partit_2,t11_partit_2]), [file(bvfunc13,t10_bvfunc13),interesting(0.28)]). fof(t6_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_partit_2,t4_bvfunc13,t18_bvfunc_1,t17_partit_2]), [file(bvfunc13,t6_bvfunc13),interesting(0.28)]). fof(t20_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t20_bvfunc13),interesting(0.26)]). fof(t29_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)) = k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t29_bvfunc13),interesting(0.26)]). fof(t39_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t39_bvfunc13),interesting(0.25)]). fof(t4_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_bvfunc_2,t21_bvfunc_2,t11_bvfunc11,t11_partit_2]), [file(bvfunc13,t4_bvfunc13),interesting(0.25)]). fof(t35_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,D)),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t17_bvfunc13]), [file(bvfunc13,t35_bvfunc13),interesting(0.24)]). fof(t23_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)) = k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,E)),C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t18_partit_2,t21_bvfunc_2]), [file(bvfunc13,t23_bvfunc13),interesting(0.21)]). fof(t38_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t21_bvfunc_2,t20_bvfunc13]), [file(bvfunc13,t38_bvfunc13),interesting(0.20)]). fof(t56_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k6_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t20_bvfunc13]), [file(bvfunc13,t56_bvfunc13),interesting(0.20)]). fof(t9_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)),k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_partit_2,t11_partit_2]), [file(bvfunc13,t9_bvfunc13),interesting(0.19)]). fof(t49_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t21_bvfunc_2,t10_bvfunc13]), [file(bvfunc13,t49_bvfunc13),interesting(0.19)]). fof(t14_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E)),k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_bvfunc13,t21_bvfunc_2]), [file(bvfunc13,t14_bvfunc13),interesting(0.14)]). fof(t30_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E),k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bvfunc13,t21_bvfunc11,t21_bvfunc_2]), [file(bvfunc13,t30_bvfunc13),interesting(0.14)]). fof(t47_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E) = k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t29_bvfunc13]), [file(bvfunc13,t47_bvfunc13),interesting(0.14)]). fof(t48_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc11,t9_bvfunc13]), [file(bvfunc13,t48_bvfunc13),interesting(0.11)]). fof(t41_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E) = k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,E)),C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t23_bvfunc13]), [file(bvfunc13,t41_bvfunc13),interesting(0.09)]). fof(t34_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,D)),C,E) = k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_bvfunc_2,t17_bvfunc11]), [file(bvfunc13,t34_bvfunc13),interesting(0.04)]). fof(t33_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,D)),C,E) = k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t18_partit_2]), [file(bvfunc13,t33_bvfunc13),interesting(0.03)]). fof(t59_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E) = k6_bvfunc_2(A,k5_valuat_1(A,k7_bvfunc_2(A,B,C,E)),C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_partit_2,t21_bvfunc_2]), [file(bvfunc13,t59_bvfunc13),interesting(0.03)]). fof(t52_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_bvfunc11,t17_bvfunc11]), [file(bvfunc13,t52_bvfunc13),interesting(0.02)]). fof(t12_bvfunc13,theorem,( $true ), file(bvfunc13,t12_bvfunc13), [interesting(0.00)]). fof(t13_bvfunc13,theorem,( $true ), file(bvfunc13,t13_bvfunc13), [interesting(0.00)]). fof(t17_partit_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E) = k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D) ) ) ) ) ) ) ), file(partit_2,t17_partit_2), [interesting(0.00)]). fof(t21_bvfunc_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_partit1(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m1_eqrel_1(D,A) => k5_valuat_1(A,k7_bvfunc_2(A,C,B,D)) = k6_bvfunc_2(A,k5_valuat_1(A,C),B,D) ) ) ) ) ), file(bvfunc_2,t21_bvfunc_2), [interesting(0.00)]). fof(t8_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [E] : ( m1_eqrel_1(E,A) => ( r1_bvfunc_1(A,B,C) => r1_bvfunc_1(A,k6_bvfunc_2(A,B,D,E),k7_bvfunc_2(A,C,D,E)) ) ) ) ) ) ) ), file(bvfunc11,t8_bvfunc11), [interesting(0.00)]). fof(t11_partit_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( r1_bvfunc_1(A,B,C) => r1_bvfunc_1(A,k5_valuat_1(A,C),k5_valuat_1(A,B)) ) ) ) ) ), file(partit_2,t11_partit_2), [interesting(0.00)]). fof(t20_bvfunc_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_partit1(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m1_eqrel_1(D,A) => k5_valuat_1(A,k6_bvfunc_2(A,C,B,D)) = k7_bvfunc_2(A,k5_valuat_1(A,C),B,D) ) ) ) ) ), file(bvfunc_2,t20_bvfunc_2), [interesting(0.00)]). fof(t13_partit_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [E] : ( m1_eqrel_1(E,A) => ( r1_bvfunc_1(A,B,C) => r1_bvfunc_1(A,k6_bvfunc_2(A,B,D,E),k6_bvfunc_2(A,C,D,E)) ) ) ) ) ) ) ), file(partit_2,t13_partit_2), [interesting(0.00)]). fof(t21_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => k5_valuat_1(A,k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E)) = k7_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E) ) ) ) ) ) ), file(bvfunc11,t21_bvfunc11), [interesting(0.00)]). fof(d9_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => k6_bvfunc_2(A,B,C,D) = k23_bvfunc_1(A,B,k5_bvfunc_2(A,D,C)) ) ) ) ) ), file(bvfunc_2,d9_bvfunc_2), [interesting(0.00)]). fof(d15_bvfunc_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( r1_bvfunc_1(A,B,C) <=> ! [D] : ( m1_subset_1(D,A) => ( k1_funct_1(B,D) = k8_margrel1 => k1_funct_1(C,D) = k8_margrel1 ) ) ) ) ) ) ), file(bvfunc_1,d15_bvfunc_1), [interesting(0.00)]). fof(d1_t_1topsp,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( D = k1_t_1topsp(A,B,C) <=> ( r2_hidden(B,D) & r2_hidden(D,C) ) ) ) ) ) ) ), file(t_1topsp,d1_t_1topsp), [interesting(0.00)]). fof(d19_bvfunc_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( D = k23_bvfunc_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => ( ( ! [F] : ( m1_subset_1(F,A) => ( r2_hidden(F,k22_bvfunc_1(A,E,C)) => k1_funct_1(B,F) = k8_margrel1 ) ) => k1_funct_1(D,E) = k8_margrel1 ) & ( ? [F] : ( m1_subset_1(F,A) & r2_hidden(F,k22_bvfunc_1(A,E,C)) & k1_funct_1(B,F) != k8_margrel1 ) => k1_funct_1(D,E) = k7_margrel1 ) ) ) ) ) ) ) ) ), file(bvfunc_1,d19_bvfunc_1), [interesting(0.00)]). fof(t43_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ( A != k8_margrel1 <=> A = k7_margrel1 ) ) ), file(margrel1,t43_margrel1), [interesting(0.00)]). fof(d5_valuat_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( C = k5_valuat_1(A,B) <=> ! [D] : ( m1_subset_1(D,A) => k8_funct_2(A,k6_margrel1,C,D) = k11_margrel1(k8_funct_2(A,k6_margrel1,B,D)) ) ) ) ) ) ), file(valuat_1,d5_valuat_1), [interesting(0.00)]). fof(t41_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ( ( A = k7_margrel1 => k9_margrel1(A) = k8_margrel1 ) & ( k9_margrel1(A) = k8_margrel1 => A = k7_margrel1 ) & ( A = k8_margrel1 => k9_margrel1(A) = k7_margrel1 ) & ( k9_margrel1(A) = k7_margrel1 => A = k8_margrel1 ) ) ) ), file(margrel1,t41_margrel1), [interesting(0.00)]). fof(t19_partit_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E),k6_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D)) ) ) ) ) ) ) ), file(partit_2,t19_partit_2), [interesting(0.00)]). fof(d10_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => k7_bvfunc_2(A,B,C,D) = k24_bvfunc_1(A,B,k5_bvfunc_2(A,D,C)) ) ) ) ) ), file(bvfunc_2,d10_bvfunc_2), [interesting(0.00)]). fof(d20_bvfunc_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( D = k24_bvfunc_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => ( ( ? [F] : ( m1_subset_1(F,A) & r2_hidden(F,k22_bvfunc_1(A,E,C)) & k1_funct_1(B,F) = k8_margrel1 ) => k1_funct_1(D,E) = k8_margrel1 ) & ( ! [F] : ( m1_subset_1(F,A) => ~ ( r2_hidden(F,k22_bvfunc_1(A,E,C)) & k1_funct_1(B,F) = k8_margrel1 ) ) => k1_funct_1(D,E) = k7_margrel1 ) ) ) ) ) ) ) ) ), file(bvfunc_1,d20_bvfunc_1), [interesting(0.00)]). fof(t18_partit_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,D),C,E) = k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D) ) ) ) ) ) ) ), file(partit_2,t18_partit_2), [interesting(0.00)]). fof(t17_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E)) = k7_bvfunc_2(A,k5_valuat_1(A,k6_bvfunc_2(A,B,C,E)),C,D) ) ) ) ) ) ) ), file(bvfunc11,t17_bvfunc11), [interesting(0.00)]). fof(t15_partit_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [E] : ( m1_eqrel_1(E,A) => ( r1_bvfunc_1(A,B,C) => r1_bvfunc_1(A,k7_bvfunc_2(A,B,D,E),k7_bvfunc_2(A,C,D,E)) ) ) ) ) ) ) ), file(partit_2,t15_partit_2), [interesting(0.00)]). fof(t51_bvfunc13,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E),k5_valuat_1(A,k7_bvfunc_2(A,k7_bvfunc_2(A,B,C,E),C,D))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_bvfunc_2,t21_bvfunc_2,t18_partit_2]), [file(bvfunc13,t51_bvfunc13),interesting(0.00)]). fof(t23_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => k5_valuat_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E)) = k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E) ) ) ) ) ) ), file(bvfunc11,t23_bvfunc11), [interesting(0.00)]). fof(t22_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E)) = k6_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,D),C,E) ) ) ) ) ) ), file(bvfunc11,t22_bvfunc11), [interesting(0.00)]). fof(t5_bvfunc13,theorem,( $true ), file(bvfunc13,t5_bvfunc13), [interesting(0.00)]). fof(t60_bvfunc13,theorem,( $true ), file(bvfunc13,t60_bvfunc13), [interesting(0.00)]). fof(t15_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E)),k7_bvfunc_2(A,k7_bvfunc_2(A,k5_valuat_1(A,B),C,E),C,D)) ) ) ) ) ) ), file(bvfunc11,t15_bvfunc11), [interesting(0.00)]). fof(t11_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ( v2_bvfunc_2(C,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k6_bvfunc_2(A,B,C,D),C,E),k7_bvfunc_2(A,k6_bvfunc_2(A,B,C,E),C,D)) ) ) ) ) ) ) ), file(bvfunc11,t11_bvfunc11), [interesting(0.00)]). fof(t18_bvfunc_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( ( ( r1_bvfunc_1(A,B,C) & r1_bvfunc_1(A,C,B) ) => B = C ) & ( ( r1_bvfunc_1(A,B,C) & r1_bvfunc_1(A,C,D) ) => r1_bvfunc_1(A,B,D) ) ) ) ) ) ) ), file(bvfunc_1,t18_bvfunc_1), [interesting(0.00)]). fof(t8_bvfunc13,theorem,( $true ), file(bvfunc13,t8_bvfunc13), [interesting(0.00)]).