fof(t8_bvfunc_5,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k14_bvfunc_1(A,B,B) = k19_bvfunc_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d11_bvfunc_1,t41_margrel1,d14_bvfunc_1,t19_binarith,t19_binarith,t39_margrel1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t8_bvfunc_5),interesting(1.00)]). fof(t18_bvfunc_5,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)) => k14_bvfunc_1(A,C,k14_bvfunc_1(A,k14_bvfunc_1(A,C,B),B)) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t18_bvfunc_5),interesting(0.79)]). fof(t16_bvfunc_5,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)) => k14_bvfunc_1(A,C,k14_bvfunc_1(A,B,C)) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t16_bvfunc_5),interesting(0.78)]). fof(t23_bvfunc_5,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)) => ( B = k19_bvfunc_1(A) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),C) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t50_margrel1,t19_binarith,d14_bvfunc_1]), [file(bvfunc_5,t23_bvfunc_5),interesting(0.77)]). fof(t7_bvfunc_5,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k5_valuat_1(A,k6_valuat_1(A,B,k5_valuat_1(A,B))) = k19_bvfunc_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d6_valuat_1,d5_valuat_1,t41_margrel1,d13_bvfunc_1,t45_margrel1,t45_margrel1,t39_margrel1,d2_funct_2,d2_funct_2,t9_funct_1,t5_bvfunc_1]), [file(bvfunc_5,t7_bvfunc_5),interesting(0.77)]). fof(t1_bvfunc_5,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)) => ( ( B = k19_bvfunc_1(A) & C = k19_bvfunc_1(A) ) <=> k6_valuat_1(A,B,C) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_bvfunc_1,t9_bvfunc_1,d14_bvfunc_1,d6_valuat_1,t45_margrel1,d14_bvfunc_1,t9_bvfunc_1]), [file(bvfunc_5,t1_bvfunc_5),interesting(0.76)]). fof(t3_bvfunc_5,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)) => ( B = k19_bvfunc_1(A) => k8_bvfunc_1(A,B,C) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d7_bvfunc_1,t19_binarith,d14_bvfunc_1]), [file(bvfunc_5,t3_bvfunc_5),interesting(0.71)]). fof(t27_bvfunc_5,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)) => ( k14_bvfunc_1(A,B,k14_bvfunc_1(A,B,C)) = k19_bvfunc_1(A) => k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t20_binarith,t21_binarith,t39_margrel1,d11_bvfunc_1,t19_binarith,t19_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t27_bvfunc_5),interesting(0.66)]). fof(t2_bvfunc_5,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)) => ( ( B = k19_bvfunc_1(A) & k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) ) => C = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d14_bvfunc_1,d11_bvfunc_1,t41_margrel1,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t2_bvfunc_5),interesting(0.66)]). fof(t5_bvfunc_5,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)) => ( C = k19_bvfunc_1(A) => k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,t19_binarith,d14_bvfunc_1]), [file(bvfunc_5,t5_bvfunc_5),interesting(0.66)]). fof(t12_bvfunc_5,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k14_bvfunc_1(A,k14_bvfunc_1(A,k5_valuat_1(A,B),B),B) = k19_bvfunc_1(A) ) ) ), inference(mizar_proof,[status(thm)],[d5_valuat_1,t40_margrel1,t21_binarith,d11_bvfunc_1,d11_bvfunc_1,d14_bvfunc_1,t19_binarith,t41_margrel1,t19_binarith,d14_bvfunc_1,t39_margrel1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t12_bvfunc_5),interesting(0.64)]). fof(t17_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),D),k14_bvfunc_1(A,C,D)) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,d11_bvfunc_1,t22_binarith,t20_binarith,t20_binarith,t23_binarith,t50_margrel1,t20_binarith,t19_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t17_bvfunc_5),interesting(0.64)]). fof(t21_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,C,k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,C,D)) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t10_binarith,t40_margrel1,t40_margrel1,t52_margrel1,t16_binarith,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t21_bvfunc_5),interesting(0.64)]). fof(t19_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,D,k14_bvfunc_1(A,C,B)),k14_bvfunc_1(A,C,k14_bvfunc_1(A,D,B))) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t10_binarith,t40_margrel1,t52_margrel1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t20_binarith,t23_binarith,t50_margrel1,t20_binarith,t20_binarith,t19_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t19_bvfunc_5),interesting(0.61)]). fof(t14_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k14_bvfunc_1(A,C,D),k14_bvfunc_1(A,B,D))) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,d11_bvfunc_1,t10_binarith,t40_margrel1,d11_bvfunc_1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t23_binarith,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t20_binarith,t20_binarith,t19_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t14_bvfunc_5),interesting(0.60)]). fof(t20_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,C,D),k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D))) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t10_binarith,t40_margrel1,t40_margrel1,t23_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t50_margrel1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t20_bvfunc_5),interesting(0.60)]). fof(t15_bvfunc_5,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)) => ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) => k14_bvfunc_1(A,k14_bvfunc_1(A,C,D),k14_bvfunc_1(A,B,D)) = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t15_bvfunc_5),interesting(0.59)]). fof(t36_bvfunc_5,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,k5_valuat_1(A,B)),k5_valuat_1(A,B)) = k19_bvfunc_1(A) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,d5_valuat_1,t40_margrel1,t16_binarith,d5_valuat_1,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t36_bvfunc_5),interesting(0.59)]). fof(t22_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)),k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D))) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t10_binarith,t10_binarith,t40_margrel1,t40_margrel1,t40_margrel1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t23_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t50_margrel1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t22_bvfunc_5),interesting(0.57)]). fof(t28_bvfunc_5,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)) => ( k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)) = k19_bvfunc_1(A) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,B,D)) = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t20_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1]), [file(bvfunc_5,t28_bvfunc_5),interesting(0.57)]). fof(t10_bvfunc_5,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)) => ( ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) & k14_bvfunc_1(A,C,D) = k19_bvfunc_1(A) ) => k14_bvfunc_1(A,B,D) = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,t39_margrel1,d14_bvfunc_1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t19_binarith,t19_binarith,t41_margrel1,t43_margrel1,t19_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t10_bvfunc_5),interesting(0.53)]). fof(t25_bvfunc_5,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)) => ( ( k14_bvfunc_1(A,D,k14_bvfunc_1(A,C,B)) = k19_bvfunc_1(A) & C = k19_bvfunc_1(A) ) => k14_bvfunc_1(A,D,B) = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d14_bvfunc_1,t41_margrel1,t7_binarith,d11_bvfunc_1,d14_bvfunc_1]), [file(bvfunc_5,t25_bvfunc_5),interesting(0.50)]). fof(t24_bvfunc_5,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)) => ( k14_bvfunc_1(A,D,k14_bvfunc_1(A,C,B)) = k19_bvfunc_1(A) => k14_bvfunc_1(A,C,k14_bvfunc_1(A,D,B)) = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t20_binarith,d14_bvfunc_1]), [file(bvfunc_5,t24_bvfunc_5),interesting(0.49)]). fof(t29_bvfunc_5,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)) => ( ( k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)) = k19_bvfunc_1(A) & k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) ) => k14_bvfunc_1(A,B,D) = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d14_bvfunc_1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,t19_binarith,t19_binarith,t19_binarith,t41_margrel1,t7_binarith,t19_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t29_bvfunc_5),interesting(0.49)]). fof(t26_bvfunc_5,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)) => ( ( k14_bvfunc_1(A,D,k14_bvfunc_1(A,C,B)) = k19_bvfunc_1(A) & C = k19_bvfunc_1(A) & D = k19_bvfunc_1(A) ) => B = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d14_bvfunc_1,t41_margrel1,t41_margrel1,t7_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t26_bvfunc_5),interesting(0.47)]). fof(t37_bvfunc_5,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)) => k14_bvfunc_1(A,k5_valuat_1(A,B),k14_bvfunc_1(A,B,C)) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d5_valuat_1,t40_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t37_bvfunc_5),interesting(0.46)]). fof(t30_bvfunc_5,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)) => ( ( k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)) = k19_bvfunc_1(A) & k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) & B = k19_bvfunc_1(A) ) => D = k19_bvfunc_1(A) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d14_bvfunc_1,d14_bvfunc_1,d11_bvfunc_1,t41_margrel1,t7_binarith,t41_margrel1,t41_margrel1,t7_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t30_bvfunc_5),interesting(0.45)]). fof(t40_bvfunc_5,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)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k8_bvfunc_1(A,B,k6_valuat_1(A,k6_valuat_1(A,C,D),E)) = k6_valuat_1(A,k6_valuat_1(A,k8_bvfunc_1(A,B,C),k8_bvfunc_1(A,B,D)),k8_bvfunc_1(A,B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t14_bvfunc_1,t14_bvfunc_1]), [file(bvfunc_5,t40_bvfunc_5),interesting(0.45)]). fof(t41_bvfunc_5,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)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k6_valuat_1(A,B,k8_bvfunc_1(A,k8_bvfunc_1(A,C,D),E)) = k8_bvfunc_1(A,k8_bvfunc_1(A,k6_valuat_1(A,B,C),k6_valuat_1(A,B,D)),k6_valuat_1(A,B,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_bvfunc_1,t15_bvfunc_1]), [file(bvfunc_5,t41_bvfunc_5),interesting(0.45)]). fof(t32_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)),k14_bvfunc_1(A,C,B)) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t20_binarith,d5_valuat_1,t19_binarith,t50_margrel1,t20_binarith,d5_valuat_1,t40_margrel1,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t32_bvfunc_5),interesting(0.42)]). fof(t33_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k5_valuat_1(A,C),k5_valuat_1(A,B))) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,d5_valuat_1,t40_margrel1,d5_valuat_1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t33_bvfunc_5),interesting(0.42)]). fof(t34_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,k5_valuat_1(A,C)),k14_bvfunc_1(A,C,k5_valuat_1(A,B))) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,d5_valuat_1,t40_margrel1,d5_valuat_1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t34_bvfunc_5),interesting(0.42)]). fof(t35_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,k5_valuat_1(A,B),C),k14_bvfunc_1(A,k5_valuat_1(A,C),B)) = k19_bvfunc_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t10_binarith,t40_margrel1,d5_valuat_1,d5_valuat_1,t40_margrel1,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t35_bvfunc_5),interesting(0.42)]). fof(t31_bvfunc_5,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)) => ! [E] : ( m2_fraenkel(E,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( ( k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,D)) = k19_bvfunc_1(A) & k14_bvfunc_1(A,B,k14_bvfunc_1(A,D,E)) = k19_bvfunc_1(A) ) => k14_bvfunc_1(A,B,k14_bvfunc_1(A,C,E)) = k19_bvfunc_1(A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t39_margrel1,d14_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,d11_bvfunc_1,t19_binarith,t19_binarith,t19_binarith,t39_margrel1,t39_margrel1,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t41_margrel1,t43_margrel1,t19_binarith,t19_binarith,t7_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t31_bvfunc_5),interesting(0.36)]). fof(t6_bvfunc_5,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,B) = k19_bvfunc_1(A) => k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d5_valuat_1,d11_bvfunc_1,t19_binarith,d14_bvfunc_1]), [file(bvfunc_5,t6_bvfunc_5),interesting(0.34)]). fof(t9_bvfunc_5,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)) => ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) <=> k14_bvfunc_1(A,k5_valuat_1(A,C),k5_valuat_1(A,B)) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,t39_margrel1,d11_bvfunc_1,d5_valuat_1,t19_binarith,d5_valuat_1,d11_bvfunc_1,t40_margrel1,t19_binarith,t7_binarith,d14_bvfunc_1,d14_bvfunc_1,d11_bvfunc_1,d5_valuat_1,d5_valuat_1,t40_margrel1,t39_margrel1,d11_bvfunc_1,t19_binarith,d11_bvfunc_1,t19_binarith,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t9_bvfunc_5),interesting(0.31)]). fof(t11_bvfunc_5,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)) => ( ( k14_bvfunc_1(A,B,C) = k19_bvfunc_1(A) & k14_bvfunc_1(A,B,k5_valuat_1(A,C)) = k19_bvfunc_1(A) ) => k5_valuat_1(A,B) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d14_bvfunc_1,d11_bvfunc_1,t39_margrel1,d14_bvfunc_1,d11_bvfunc_1,d5_valuat_1,d5_valuat_1,d5_valuat_1,d5_valuat_1,t41_margrel1,t43_margrel1,t7_binarith,d14_bvfunc_1]), [file(bvfunc_5,t11_bvfunc_5),interesting(0.29)]). fof(t38_bvfunc_5,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)) => k5_valuat_1(A,k6_valuat_1(A,k6_valuat_1(A,B,C),D)) = k8_bvfunc_1(A,k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)),k5_valuat_1(A,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t17_bvfunc_1,t17_bvfunc_1]), [file(bvfunc_5,t38_bvfunc_5),interesting(0.18)]). fof(t39_bvfunc_5,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)) => k5_valuat_1(A,k8_bvfunc_1(A,k8_bvfunc_1(A,B,C),D)) = k6_valuat_1(A,k6_valuat_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)),k5_valuat_1(A,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_bvfunc_1,t16_bvfunc_1]), [file(bvfunc_5,t39_bvfunc_5),interesting(0.18)]). fof(d14_bvfunc_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( B = k19_bvfunc_1(A) <=> ! [C] : ( m1_subset_1(C,A) => k1_funct_1(B,C) = k8_margrel1 ) ) ) ) ), file(bvfunc_1,d14_bvfunc_1), [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(t39_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ( A = k7_margrel1 | A = k8_margrel1 ) ) ), file(margrel1,t39_margrel1), [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(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(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(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(t40_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k9_margrel1(k9_margrel1(A)) = A ) ), file(margrel1,t40_margrel1), [interesting(0.00)]). fof(t21_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,A) = A ) ), file(binarith,t21_binarith), [interesting(0.00)]). fof(d2_funct_2,definition,( ! [A,B,C] : ( C = k1_funct_2(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E] : ( v1_relat_1(E) & v1_funct_1(E) & D = E & k1_relat_1(E) = A & r1_tarski(k2_relat_1(E),B) ) ) ) ), file(funct_2,d2_funct_2), [interesting(0.00)]). fof(t9_funct_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), [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(t17_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,k6_valuat_1(A,B,C)) = k8_bvfunc_1(A,k5_valuat_1(A,B),k5_valuat_1(A,C)) ) ) ) ), file(bvfunc_1,t17_bvfunc_1), [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(t10_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k1_binarith(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ), file(binarith,t10_binarith), [interesting(0.00)]). fof(t23_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(A,k10_margrel1(B,C)) = k10_margrel1(k1_binarith(A,B),k1_binarith(A,C)) ) ) ) ), file(binarith,t23_binarith), [interesting(0.00)]). fof(t20_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(k1_binarith(A,B),C) = k1_binarith(A,k1_binarith(B,C)) ) ) ) ), file(binarith,t20_binarith), [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(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(t13_bvfunc_5,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)) => k14_bvfunc_1(A,k14_bvfunc_1(A,B,C),k14_bvfunc_1(A,k5_valuat_1(A,k6_valuat_1(A,C,D)),k5_valuat_1(A,k6_valuat_1(A,B,D)))) = k19_bvfunc_1(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_bvfunc_1,d11_bvfunc_1,d5_valuat_1,t40_margrel1,d6_valuat_1,t17_bvfunc_1,d7_bvfunc_1,d5_valuat_1,d5_valuat_1,d11_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t20_binarith,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t50_margrel1,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t19_binarith,t19_binarith,t45_margrel1,d14_bvfunc_1,d2_funct_2,d2_funct_2,t9_funct_1]), [file(bvfunc_5,t13_bvfunc_5),interesting(0.00)]). fof(t22_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k1_binarith(B,C)) = k1_binarith(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ), file(binarith,t22_binarith), [interesting(0.00)]). fof(t52_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k10_margrel1(B,C)) = k10_margrel1(k10_margrel1(A,B),C) ) ) ) ), file(margrel1,t52_margrel1), [interesting(0.00)]). fof(t9_bvfunc_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => k6_valuat_1(A,B,k19_bvfunc_1(A)) = B ) ) ), file(bvfunc_1,t9_bvfunc_1), [interesting(0.00)]). fof(t16_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,A) = A ) ), file(binarith,t16_binarith), [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(t14_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)) => k8_bvfunc_1(A,k6_valuat_1(A,B,C),D) = k6_valuat_1(A,k8_bvfunc_1(A,B,D),k8_bvfunc_1(A,C,D)) ) ) ) ) ), file(bvfunc_1,t14_bvfunc_1), [interesting(0.00)]). fof(t15_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)) => k6_valuat_1(A,k8_bvfunc_1(A,B,C),D) = k8_bvfunc_1(A,k6_valuat_1(A,B,D),k6_valuat_1(A,C,D)) ) ) ) ) ), file(bvfunc_1,t15_bvfunc_1), [interesting(0.00)]). fof(t4_bvfunc_5,theorem,( $true ), file(bvfunc_5,t4_bvfunc_5), [interesting(0.00)]). fof(d13_bvfunc_1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( B = k18_bvfunc_1(A) <=> ! [C] : ( m1_subset_1(C,A) => k1_funct_1(B,C) = k7_margrel1 ) ) ) ) ), file(bvfunc_1,d13_bvfunc_1), [interesting(0.00)]). fof(t5_bvfunc_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_fraenkel(B,A,k6_margrel1,k1_fraenkel(A,k6_margrel1)) => ( k5_valuat_1(A,k19_bvfunc_1(A)) = k18_bvfunc_1(A) & k5_valuat_1(A,k18_bvfunc_1(A)) = k19_bvfunc_1(A) ) ) ) ), file(bvfunc_1,t5_bvfunc_1), [interesting(0.00)]).