fof(t14_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E),k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bvfunc_2,d15_bvfunc_1,d1_t_1topsp,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t43_margrel1,t41_margrel1,t7_binarith,l15_bvfunc_3,t43_margrel1,d11_bvfunc_1,d19_bvfunc_1,t41_margrel1,t19_binarith]), [file(bvfunc_3,t14_bvfunc_3),interesting(1.00)]). fof(t15_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E),k14_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t43_margrel1,t41_margrel1,t7_binarith,l15_bvfunc_3,t43_margrel1,d11_bvfunc_1,d20_bvfunc_1,t41_margrel1,t19_binarith]), [file(bvfunc_3,t15_bvfunc_3),interesting(1.00)]). fof(t11_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k8_bvfunc_1(A,C,D),B,E),k8_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d1_t_1topsp,l10_bvfunc_3,d7_bvfunc_1,t39_margrel1,d20_bvfunc_1,d10_bvfunc_2,d7_bvfunc_1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d7_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t11_bvfunc_3),interesting(0.97)]). fof(t10_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k8_bvfunc_1(A,C,D),B,E),k8_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,d7_bvfunc_1,t19_binarith,d19_bvfunc_1,d9_bvfunc_2,d7_bvfunc_1,t19_binarith,t43_margrel1,d7_bvfunc_1,t43_margrel1,t7_binarith,l10_bvfunc_3,t43_margrel1]), [file(bvfunc_3,t10_bvfunc_3),interesting(0.96)]). fof(t23_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E)) = k7_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bvfunc_2,d15_bvfunc_1,d11_bvfunc_1,t39_margrel1,t41_margrel1,t43_margrel1,d19_bvfunc_1,d11_bvfunc_1,t43_margrel1,t41_margrel1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d11_bvfunc_1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,t7_binarith,d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d11_bvfunc_1,t39_margrel1,t41_margrel1,t43_margrel1,d19_bvfunc_1,d11_bvfunc_1,t41_margrel1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t7_binarith,t18_bvfunc_1]), [file(bvfunc_3,t23_bvfunc_3),interesting(0.78)]). fof(t1_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k14_bvfunc_1(A,C,D),k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,d11_bvfunc_1,t41_margrel1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t1_bvfunc_3),interesting(0.77)]). fof(t19_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E),k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d11_bvfunc_1,t39_margrel1,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,d11_bvfunc_1,t41_margrel1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t19_bvfunc_3),interesting(0.73)]). fof(t12_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E)),k7_bvfunc_2(A,k6_valuat_1(A,C,D),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2]), [file(bvfunc_3,t12_bvfunc_3),interesting(0.72)]). fof(t13_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E)),k7_bvfunc_2(A,k6_valuat_1(A,C,D),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2]), [file(bvfunc_3,t13_bvfunc_3),interesting(0.72)]). fof(t16_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k14_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E)),k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t19_binarith,d19_bvfunc_1,d9_bvfunc_2,d20_bvfunc_1,d10_bvfunc_2,t41_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t7_binarith,d11_bvfunc_1,t43_margrel1,t41_margrel1,t19_binarith,d19_bvfunc_1,d9_bvfunc_2]), [file(bvfunc_3,t16_bvfunc_3),interesting(0.72)]). fof(t27_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E) = k5_valuat_1(A,k7_bvfunc_2(A,k6_valuat_1(A,C,k5_valuat_1(A,D)),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_bvfunc_2,t4_bvfunc_1,t16_bvfunc_1,t4_bvfunc_1,t26_bvfunc_3]), [file(bvfunc_3,t27_bvfunc_3),interesting(0.71)]). fof(t21_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => ( r3_bvfunc_2(A,C,B,E) => r1_bvfunc_1(A,k7_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E),k14_bvfunc_1(A,C,k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bvfunc_2,d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,d18_bvfunc_1,t41_margrel1,d11_bvfunc_1,t41_margrel1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t21_bvfunc_3),interesting(0.69)]). fof(t25_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k14_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E)),k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d15_bvfunc_1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,t41_margrel1,t43_margrel1,d20_bvfunc_1,d19_bvfunc_1,d9_bvfunc_2,d11_bvfunc_1,t41_margrel1,t19_binarith,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t25_bvfunc_3),interesting(0.69)]). fof(t26_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E) = k6_bvfunc_2(A,k8_bvfunc_1(A,k5_valuat_1(A,C),D),B,E) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d11_bvfunc_1,t39_margrel1,d5_valuat_1,d7_bvfunc_1,t19_binarith,d7_bvfunc_1,t19_binarith,t7_binarith,d19_bvfunc_1,d9_bvfunc_2,d15_bvfunc_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d7_bvfunc_1,t39_margrel1,d5_valuat_1,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t19_binarith,t7_binarith,d19_bvfunc_1,d9_bvfunc_2,t18_bvfunc_1]), [file(bvfunc_3,t26_bvfunc_3),interesting(0.68)]). fof(t9_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,k8_bvfunc_1(A,C,D),B,E),k8_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d20_bvfunc_1,d10_bvfunc_2,d7_bvfunc_1,t19_binarith,d19_bvfunc_1,d9_bvfunc_2,d7_bvfunc_1,t19_binarith,t43_margrel1,d7_bvfunc_1,t43_margrel1,t7_binarith,t43_margrel1]), [file(bvfunc_3,t9_bvfunc_3),interesting(0.68)]). fof(t20_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k14_bvfunc_1(A,k7_bvfunc_2(A,D,B,E),k7_bvfunc_2(A,k6_valuat_1(A,C,D),B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t43_margrel1,d11_bvfunc_1,t41_margrel1,t19_binarith]), [file(bvfunc_3,t20_bvfunc_3),interesting(0.66)]). fof(t24_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E)),k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,d11_bvfunc_1,t19_binarith,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t24_bvfunc_3),interesting(0.65)]). fof(t22_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => ( r3_bvfunc_2(A,C,B,E) => r1_bvfunc_1(A,k7_bvfunc_2(A,k14_bvfunc_1(A,D,C),B,E),k14_bvfunc_1(A,k6_bvfunc_2(A,D,B,E),C)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bvfunc_2,d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,d11_bvfunc_1,t41_margrel1,t19_binarith,d18_bvfunc_1,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t22_bvfunc_3),interesting(0.64)]). fof(t30_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E)),k7_bvfunc_2(A,k6_valuat_1(A,C,D),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t41_margrel1,d6_valuat_1,t7_binarith,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2]), [file(bvfunc_3,t30_bvfunc_3),interesting(0.61)]). fof(t29_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k5_valuat_1(A,k6_valuat_1(A,k5_valuat_1(A,k7_bvfunc_2(A,k6_valuat_1(A,C,D),B,E)),k5_valuat_1(A,k7_bvfunc_2(A,k6_valuat_1(A,C,k5_valuat_1(A,D)),B,E))))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d6_valuat_1,t50_margrel1,d6_valuat_1,t50_margrel1,d5_valuat_1,d5_valuat_1,d6_valuat_1,d5_valuat_1,d20_bvfunc_1,d10_bvfunc_2,t41_margrel1,t45_margrel1,t41_margrel1,d5_valuat_1,t41_margrel1,d20_bvfunc_1,d10_bvfunc_2,t41_margrel1,t45_margrel1,t41_margrel1,t39_margrel1]), [file(bvfunc_3,t29_bvfunc_3),interesting(0.52)]). fof(t32_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,D,E),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,C,E),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t19_binarith,t41_margrel1,t43_margrel1,d11_bvfunc_1,t19_binarith,t7_binarith,d19_bvfunc_1,d9_bvfunc_2]), [file(bvfunc_3,t32_bvfunc_3),interesting(0.49)]). fof(t4_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => k5_valuat_1(A,k6_valuat_1(A,k6_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E))) = k8_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,C),B,E),k7_bvfunc_2(A,k5_valuat_1(A,D),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bvfunc_2,d9_bvfunc_2,d15_bvfunc_1,d5_valuat_1,d6_valuat_1,t41_margrel1,t43_margrel1,d19_bvfunc_1,t43_margrel1,t41_margrel1,d5_valuat_1,d20_bvfunc_1,d10_bvfunc_2,d7_bvfunc_1,t19_binarith,t43_margrel1,d19_bvfunc_1,t43_margrel1,t41_margrel1,d5_valuat_1,d20_bvfunc_1,d10_bvfunc_2,d7_bvfunc_1,t19_binarith,t45_margrel1,d15_bvfunc_1,d7_bvfunc_1,t39_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d5_valuat_1,t41_margrel1,t43_margrel1,d5_valuat_1,d6_valuat_1,d19_bvfunc_1,t45_margrel1,t41_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d5_valuat_1,t41_margrel1,t43_margrel1,d5_valuat_1,d6_valuat_1,d19_bvfunc_1,t45_margrel1,t41_margrel1,t7_binarith,t18_bvfunc_1]), [file(bvfunc_3,t4_bvfunc_3),interesting(0.43)]). fof(t5_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => k5_valuat_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) = k8_bvfunc_1(A,k6_bvfunc_2(A,k5_valuat_1(A,C),B,E),k6_bvfunc_2(A,k5_valuat_1(A,D),B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bvfunc_2,d9_bvfunc_2,d10_bvfunc_2,d10_bvfunc_2,d15_bvfunc_1,d5_valuat_1,t41_margrel1,d6_valuat_1,t43_margrel1,d20_bvfunc_1,t43_margrel1,t41_margrel1,d5_valuat_1,d7_bvfunc_1,d19_bvfunc_1,t19_binarith,t43_margrel1,d20_bvfunc_1,t43_margrel1,t41_margrel1,d5_valuat_1,d7_bvfunc_1,d19_bvfunc_1,t19_binarith,t45_margrel1,d15_bvfunc_1,d7_bvfunc_1,t39_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d5_valuat_1,t41_margrel1,t43_margrel1,d5_valuat_1,d6_valuat_1,d20_bvfunc_1,t45_margrel1,t41_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d5_valuat_1,t41_margrel1,t43_margrel1,d5_valuat_1,d6_valuat_1,d20_bvfunc_1,t45_margrel1,t41_margrel1,t7_binarith,t18_bvfunc_1]), [file(bvfunc_3,t5_bvfunc_3),interesting(0.43)]). fof(t28_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k5_valuat_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E),k6_bvfunc_2(A,k14_bvfunc_1(A,C,k5_valuat_1(A,D)),B,E)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,d5_valuat_1,d6_valuat_1,d11_bvfunc_1,t41_margrel1,t7_binarith,d11_bvfunc_1,t41_margrel1,t7_binarith,d5_valuat_1,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,t45_margrel1,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,t45_margrel1,t41_margrel1,t39_margrel1]), [file(bvfunc_3,t28_bvfunc_3),interesting(0.42)]). fof(t31_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,E),k5_valuat_1(A,k7_bvfunc_2(A,k6_valuat_1(A,C,D),B,E))),k5_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d15_bvfunc_1,d6_valuat_1,t45_margrel1,d5_valuat_1,t41_margrel1,t43_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d20_bvfunc_1,t43_margrel1,d6_valuat_1,t43_margrel1,d11_bvfunc_1,t41_margrel1,t7_binarith,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,d5_valuat_1,t41_margrel1,t45_margrel1]), [file(bvfunc_3,t31_bvfunc_3),interesting(0.42)]). fof(t33_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F),k7_bvfunc_2(A,k6_valuat_1(A,E,C),B,F)),k7_bvfunc_2(A,k6_valuat_1(A,E,D),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d6_valuat_1,t41_margrel1,t43_margrel1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t7_binarith,t45_margrel1]), [file(bvfunc_3,t33_bvfunc_3),interesting(0.41)]). fof(t38_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,C,E),B,F)),k7_bvfunc_2(A,k6_valuat_1(A,E,D),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t41_margrel1,t43_margrel1,t41_margrel1,t43_margrel1,t41_margrel1,t43_margrel1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t7_binarith]), [file(bvfunc_3,t38_bvfunc_3),interesting(0.34)]). fof(t40_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,D,E),B,F)),k7_bvfunc_2(A,k6_valuat_1(A,E,C),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,t41_margrel1,t43_margrel1,t41_margrel1,t43_margrel1,t41_margrel1,t43_margrel1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t7_binarith]), [file(bvfunc_3,t40_bvfunc_3),interesting(0.34)]). fof(t8_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k9_bvfunc_1(A,C,D),k8_bvfunc_1(A,k5_valuat_1(A,k9_bvfunc_1(A,k7_bvfunc_2(A,k5_valuat_1(A,C),B,E),k7_bvfunc_2(A,D,B,E))),k5_valuat_1(A,k9_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,k5_valuat_1(A,D),B,E))))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d10_bvfunc_2,d15_bvfunc_1,d8_bvfunc_1,d2_binarith,t39_margrel1,d1_t_1topsp,t41_margrel1,t49_margrel1,t45_margrel1,d5_valuat_1,d20_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,d8_bvfunc_1,d2_binarith,t7_binarith,d5_valuat_1,d7_bvfunc_1,d5_valuat_1,t41_margrel1,t19_binarith,t45_margrel1,d5_valuat_1,d20_bvfunc_1,d20_bvfunc_1,d10_bvfunc_2,d8_bvfunc_1,d2_binarith,t7_binarith,d5_valuat_1,d7_bvfunc_1,d5_valuat_1,t41_margrel1,t19_binarith,t7_binarith]), [file(bvfunc_3,t8_bvfunc_3),interesting(0.34)]). fof(t34_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,k5_valuat_1(A,D)),B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,E,D),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,E,k5_valuat_1(A,C)),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t39_margrel1,d5_valuat_1,d11_bvfunc_1,t19_binarith,d5_valuat_1,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t19_binarith,d5_valuat_1,t41_margrel1,t43_margrel1,t7_binarith,d19_bvfunc_1,d9_bvfunc_2]), [file(bvfunc_3,t34_bvfunc_3),interesting(0.31)]). fof(t35_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,E,k5_valuat_1(A,D)),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,E,k5_valuat_1(A,C)),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t39_margrel1,d5_valuat_1,d11_bvfunc_1,t19_binarith,d5_valuat_1,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t19_binarith,d5_valuat_1,t41_margrel1,t43_margrel1,t7_binarith,d19_bvfunc_1,d9_bvfunc_2]), [file(bvfunc_3,t35_bvfunc_3),interesting(0.31)]). fof(t39_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,D,k5_valuat_1(A,E)),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,E,k5_valuat_1(A,C)),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t39_margrel1,d5_valuat_1,d11_bvfunc_1,t19_binarith,t41_margrel1,t43_margrel1,d5_valuat_1,d11_bvfunc_1,t19_binarith,d5_valuat_1,d11_bvfunc_1,t19_binarith,t7_binarith,d19_bvfunc_1,d9_bvfunc_2]), [file(bvfunc_3,t39_bvfunc_3),interesting(0.31)]). fof(t36_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,k5_valuat_1(A,D)),B,F),k7_bvfunc_2(A,k6_valuat_1(A,E,D),B,F)),k7_bvfunc_2(A,k6_valuat_1(A,E,k5_valuat_1(A,C)),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d6_valuat_1,d6_valuat_1,d5_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,d5_valuat_1,t41_margrel1,t43_margrel1,t7_binarith,t45_margrel1]), [file(bvfunc_3,t36_bvfunc_3),interesting(0.23)]). fof(t37_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,k14_bvfunc_1(A,C,D),B,F),k7_bvfunc_2(A,k6_valuat_1(A,E,k5_valuat_1(A,D)),B,F)),k7_bvfunc_2(A,k6_valuat_1(A,E,k5_valuat_1(A,C)),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d6_valuat_1,d6_valuat_1,d5_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,d5_valuat_1,t41_margrel1,t43_margrel1,t7_binarith,t45_margrel1]), [file(bvfunc_3,t37_bvfunc_3),interesting(0.23)]). fof(t41_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [F] : ( m1_eqrel_1(F,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_valuat_1(A,k7_bvfunc_2(A,C,B,F),k6_bvfunc_2(A,k14_bvfunc_1(A,D,k5_valuat_1(A,C)),B,F)),k6_bvfunc_2(A,k14_bvfunc_1(A,C,E),B,F)),k7_bvfunc_2(A,k6_valuat_1(A,E,k5_valuat_1(A,D)),B,F)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d6_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d11_bvfunc_1,t39_margrel1,t41_margrel1,t43_margrel1,t41_margrel1,t43_margrel1,d6_valuat_1,d5_valuat_1,t45_margrel1,d20_bvfunc_1,d10_bvfunc_2,d5_valuat_1,t41_margrel1,t43_margrel1,t7_binarith]), [file(bvfunc_3,t41_bvfunc_3),interesting(0.15)]). 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(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(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(d7_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)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( D = k8_bvfunc_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,k6_margrel1,D,E) = k3_binarith(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ), file(bvfunc_1,d7_bvfunc_1), [interesting(0.00)]). fof(t19_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k8_margrel1) = k8_margrel1 ) ), file(binarith,t19_binarith), [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(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(t43_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ( A != k8_margrel1 <=> A = k7_margrel1 ) ) ), file(margrel1,t43_margrel1), [interesting(0.00)]). fof(t7_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k7_margrel1) = A ) ), file(binarith,t7_binarith), [interesting(0.00)]). fof(l10_bvfunc_3,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) => ! [F] : ( m1_subset_1(F,A) => ( k1_funct_1(k6_bvfunc_2(A,k8_bvfunc_1(A,B,C),D,E),F) = k8_margrel1 => ! [G] : ( m1_subset_1(G,A) => ( r2_hidden(G,k22_bvfunc_1(A,F,k5_bvfunc_2(A,E,D))) => k1_funct_1(k8_bvfunc_1(A,B,C),G) = k8_margrel1 ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_bvfunc_1,d9_bvfunc_2,t43_margrel1]), [file(bvfunc_3,l10_bvfunc_3),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(t39_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ( A = k7_margrel1 | A = k8_margrel1 ) ) ), file(margrel1,t39_margrel1), [interesting(0.00)]). fof(d6_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)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( D = k6_valuat_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,k6_margrel1,D,E) = k12_margrel1(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ), file(valuat_1,d6_valuat_1), [interesting(0.00)]). fof(t45_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( ( k10_margrel1(A,B) = k8_margrel1 => ( A = k8_margrel1 & B = k8_margrel1 ) ) & ( ( A = k8_margrel1 & B = k8_margrel1 ) => k10_margrel1(A,B) = k8_margrel1 ) & ~ ( k10_margrel1(A,B) = k7_margrel1 & A != k7_margrel1 & B != k7_margrel1 ) & ( ( A = k7_margrel1 | B = k7_margrel1 ) => k10_margrel1(A,B) = k7_margrel1 ) ) ) ) ), file(margrel1,t45_margrel1), [interesting(0.00)]). fof(d11_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)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( D = k14_bvfunc_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,k6_margrel1,D,E) = k1_binarith(k9_margrel1(k1_funct_1(B,E)),k1_funct_1(C,E)) ) ) ) ) ) ) ), file(bvfunc_1,d11_bvfunc_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(l15_bvfunc_3,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) => ! [F] : ( m1_subset_1(F,A) => ( k1_funct_1(k6_bvfunc_2(A,k14_bvfunc_1(A,B,C),D,E),F) = k8_margrel1 => ! [G] : ( m1_subset_1(G,A) => ( r2_hidden(G,k22_bvfunc_1(A,F,k5_bvfunc_2(A,E,D))) => k1_funct_1(k14_bvfunc_1(A,B,C),G) = k8_margrel1 ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d19_bvfunc_1,d9_bvfunc_2,t43_margrel1]), [file(bvfunc_3,l15_bvfunc_3),interesting(0.00)]). fof(t17_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k14_bvfunc_1(A,C,D),k14_bvfunc_1(A,C,k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,d11_bvfunc_1,t19_binarith,d20_bvfunc_1,d10_bvfunc_2,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t17_bvfunc_3),interesting(0.00)]). fof(t18_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k14_bvfunc_1(A,C,D),k14_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d11_bvfunc_1,t39_margrel1,d1_t_1topsp,t41_margrel1,t43_margrel1,d19_bvfunc_1,d9_bvfunc_2,d11_bvfunc_1,t41_margrel1,t19_binarith,d11_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t18_bvfunc_3),interesting(0.00)]). fof(d8_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) => ( r3_bvfunc_2(A,B,C,D) <=> r2_bvfunc_1(A,B,k5_bvfunc_2(A,D,C)) ) ) ) ) ) ), file(bvfunc_2,d8_bvfunc_2), [interesting(0.00)]). fof(d18_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) => ( r2_bvfunc_1(A,B,C) <=> ! [D] : ( r2_hidden(D,C) => ! [E,F] : ( ( r2_hidden(E,D) & r2_hidden(F,D) ) => k1_funct_1(B,E) = k1_funct_1(B,F) ) ) ) ) ) ) ), file(bvfunc_1,d18_bvfunc_1), [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(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(t4_bvfunc_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_valuat_1(A) ) => k3_valuat_1(k3_valuat_1(A)) = A ) ), file(bvfunc_1,t4_bvfunc_1), [interesting(0.00)]). fof(t16_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)) => k5_valuat_1(A,k8_bvfunc_1(A,B,C)) = k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ), file(bvfunc_1,t16_bvfunc_1), [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(t50_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k8_margrel1,A) = A ) ), file(margrel1,t50_margrel1), [interesting(0.00)]). fof(t2_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_valuat_1(A,k6_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E)),k6_valuat_1(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d6_valuat_1,d1_t_1topsp,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,t45_margrel1,d6_valuat_1,t45_margrel1]), [file(bvfunc_3,t2_bvfunc_3),interesting(0.00)]). fof(t3_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k6_valuat_1(A,C,D),k6_valuat_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d15_bvfunc_1,d6_valuat_1,t45_margrel1,d1_t_1topsp,d20_bvfunc_1,d10_bvfunc_2,d6_valuat_1,d20_bvfunc_1,t45_margrel1]), [file(bvfunc_3,t3_bvfunc_3),interesting(0.00)]). fof(t6_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k8_bvfunc_1(A,k6_bvfunc_2(A,C,B,E),k6_bvfunc_2(A,D,B,E)),k8_bvfunc_1(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d15_bvfunc_1,d7_bvfunc_1,t39_margrel1,d1_t_1topsp,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d7_bvfunc_1,t19_binarith,d19_bvfunc_1,d9_bvfunc_2,t43_margrel1,d7_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t6_bvfunc_3),interesting(0.00)]). fof(t7_bvfunc_3,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m2_fraenkel(C,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ! [E] : ( m1_eqrel_1(E,A) => r1_bvfunc_1(A,k8_bvfunc_1(A,C,D),k8_bvfunc_1(A,k7_bvfunc_2(A,C,B,E),k7_bvfunc_2(A,D,B,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_bvfunc_2,d10_bvfunc_2,d15_bvfunc_1,d7_bvfunc_1,t39_margrel1,d1_t_1topsp,d7_bvfunc_1,d20_bvfunc_1,t19_binarith,d7_bvfunc_1,d20_bvfunc_1,t19_binarith,t7_binarith]), [file(bvfunc_3,t7_bvfunc_3),interesting(0.00)]). fof(d8_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)) => ! [D] : ( m2_fraenkel(D,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( D = k9_bvfunc_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,A) => k8_funct_2(A,k6_margrel1,D,E) = k4_binarith(k8_funct_2(A,k6_margrel1,B,E),k8_funct_2(A,k6_margrel1,C,E)) ) ) ) ) ) ) ), file(bvfunc_1,d8_bvfunc_1), [interesting(0.00)]). fof(d2_binarith,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,B) = k1_binarith(k10_margrel1(k9_margrel1(A),B),k10_margrel1(A,k9_margrel1(B))) ) ) ), file(binarith,d2_binarith), [interesting(0.00)]). fof(t49_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k7_margrel1,A) = k7_margrel1 ) ), file(margrel1,t49_margrel1), [interesting(0.00)]).