fof(t29_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_bvfunc_1(A,B) = k2_bvfunc_1(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t28_binari_5,t28_binari_5,t23_binari_5]), [file(binari_5,t29_binari_5),interesting(1.00)]). fof(t27_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( ( k2_bvfunc_1(A,B) = k8_margrel1 & k2_bvfunc_1(B,C) = k8_margrel1 ) => k2_bvfunc_1(A,C) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_5,t24_binari_5,t26_binari_5,t26_binari_5,t24_binari_5]), [file(binari_5,t27_binari_5),interesting(0.95)]). fof(t28_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,B) = k1_bvfunc_1(k9_margrel1(B),k9_margrel1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,t40_margrel1,d1_bvfunc_1,t18_binarith,d1_bvfunc_1,d1_bvfunc_1,t40_margrel1,d1_bvfunc_1,t18_binarith,t25_binari_5]), [file(binari_5,t28_binari_5),interesting(0.85)]). fof(t45_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k1_bvfunc_1(k1_bvfunc_1(A,B),B)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t50_margrel1,t20_binarith,t19_binarith]), [file(binari_5,t45_binari_5),interesting(0.79)]). fof(t43_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k1_bvfunc_1(B,A)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,t20_binarith,t19_binarith]), [file(binari_5,t43_binari_5),interesting(0.78)]). fof(t48_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(k1_bvfunc_1(A,k1_bvfunc_1(A,B)),k1_bvfunc_1(A,B)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_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]), [file(binari_5,t48_binari_5),interesting(0.77)]). fof(t25_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( ( k1_bvfunc_1(A,B) = k8_margrel1 & k1_bvfunc_1(B,A) = k8_margrel1 ) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t41_margrel1,t7_binarith,t38_margrel1,d1_bvfunc_1,t41_margrel1,t7_binarith,t38_margrel1,t39_margrel1]), [file(binari_5,t25_binari_5),interesting(0.72)]). fof(t37_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k1_bvfunc_1(A,A) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t18_binarith]), [file(binari_5,t37_binari_5),interesting(0.71)]). fof(t50_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( A = k8_margrel1 => k1_bvfunc_1(k1_bvfunc_1(A,B),B) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t50_margrel1,t19_binarith]), [file(binari_5,t50_binari_5),interesting(0.71)]). fof(t17_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k5_binari_5(k8_margrel1,A) = A ) ), inference(mizar_proof,[status(thm)],[t13_binarith,t40_margrel1]), [file(binari_5,t17_binari_5),interesting(0.70)]). fof(t44_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(k1_bvfunc_1(k1_bvfunc_1(A,B),C),k1_bvfunc_1(B,C)) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t40_margrel1,d1_bvfunc_1,t22_binarith,t20_binarith,t20_binarith,t23_binarith,t50_margrel1,t20_binarith,t19_binarith,t19_binarith]), [file(binari_5,t44_binari_5),interesting(0.70)]). fof(t46_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(k1_bvfunc_1(A,k1_bvfunc_1(B,C)),k1_bvfunc_1(B,k1_bvfunc_1(A,C))) = k8_margrel1 ) ) ) ), 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,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_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]), [file(binari_5,t46_binari_5),interesting(0.65)]). fof(t26_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( ( k1_bvfunc_1(A,B) = k8_margrel1 & k1_bvfunc_1(B,C) = k8_margrel1 ) => k1_bvfunc_1(A,C) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t41_margrel1,t7_binarith,d1_bvfunc_1,t41_margrel1,t7_binarith,d1_bvfunc_1,t19_binarith,d1_bvfunc_1,t39_margrel1,t41_margrel1,t19_binarith]), [file(binari_5,t26_binari_5),interesting(0.63)]). fof(t41_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(k1_bvfunc_1(A,B),k1_bvfunc_1(k1_bvfunc_1(B,C),k1_bvfunc_1(A,C))) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t40_margrel1,d1_bvfunc_1,t10_binarith,t40_margrel1,d1_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]), [file(binari_5,t41_binari_5),interesting(0.63)]). fof(t47_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(k1_bvfunc_1(A,B),k1_bvfunc_1(k1_bvfunc_1(C,A),k1_bvfunc_1(C,B))) = k8_margrel1 ) ) ) ), 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,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_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]), [file(binari_5,t47_binari_5),interesting(0.63)]). fof(t23_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_bvfunc_1(A,B) = k10_margrel1(k1_bvfunc_1(A,B),k1_bvfunc_1(B,A)) ) ) ), inference(mizar_proof,[status(thm)],[d2_bvfunc_1,d2_binarith,t10_binarith,t9_binarith,t9_binarith,t40_margrel1,t40_margrel1,t22_binarith,t22_binarith,t22_binarith,t46_margrel1,t46_margrel1,t7_binarith,t7_binarith,t23_binarith,t23_binarith,t23_binarith,t18_binarith,t18_binarith,t50_margrel1,t50_margrel1,d1_bvfunc_1,d1_bvfunc_1]), [file(binari_5,t23_binari_5),interesting(0.62)]). fof(t12_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ( k3_binari_5(A,A) = k9_margrel1(A) & k9_margrel1(k3_binari_5(A,A)) = A ) ) ), inference(mizar_proof,[status(thm)],[t21_binarith,t40_margrel1]), [file(binari_5,t12_binari_5),interesting(0.61)]). fof(t3_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ( k1_binari_5(A,A) = k9_margrel1(A) & k9_margrel1(k1_binari_5(A,A)) = A ) ) ), inference(mizar_proof,[status(thm)],[t16_binarith,t40_margrel1]), [file(binari_5,t3_binari_5),interesting(0.61)]). fof(t22_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( r1_xreal_0(A,k1_bvfunc_1(B,C)) <=> r1_xreal_0(k10_margrel1(A,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t20_binarith,t9_binarith,d1_bvfunc_1,d3_bvfunc_1,d3_bvfunc_1,d1_bvfunc_1,t9_binarith,t20_binarith,d1_bvfunc_1,d1_bvfunc_1,d3_bvfunc_1]), [file(binari_5,t22_binari_5),interesting(0.60)]). fof(t35_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( A = k8_margrel1 => k1_bvfunc_1(B,A) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t19_binarith]), [file(binari_5,t35_binari_5),interesting(0.59)]). fof(t49_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(k1_bvfunc_1(A,k1_bvfunc_1(B,C)),k1_bvfunc_1(k1_bvfunc_1(A,B),k1_bvfunc_1(A,C))) = k8_margrel1 ) ) ) ), 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,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_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]), [file(binari_5,t49_binari_5),interesting(0.59)]). fof(t24_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( k2_bvfunc_1(A,B) = k8_margrel1 <=> ( k1_bvfunc_1(A,B) = k8_margrel1 & k1_bvfunc_1(B,A) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t45_margrel1,d17_margrel1,t23_binari_5]), [file(binari_5,t24_binari_5),interesting(0.58)]). fof(t2_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k1_binari_5(k7_margrel1,A) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[t49_margrel1,t41_margrel1]), [file(binari_5,t2_binari_5),interesting(0.58)]). fof(t34_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( ( A = k8_margrel1 & k1_bvfunc_1(A,B) = k8_margrel1 ) => B = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t41_margrel1,t7_binarith]), [file(binari_5,t34_binari_5),interesting(0.58)]). fof(t42_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_bvfunc_1(A,B) = k8_margrel1 => k1_bvfunc_1(k1_bvfunc_1(B,C),k1_bvfunc_1(A,C)) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,d1_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]), [file(binari_5,t42_binari_5),interesting(0.58)]). fof(t54_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( k1_bvfunc_1(A,k1_bvfunc_1(A,B)) = k8_margrel1 => k1_bvfunc_1(A,B) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,t20_binarith,t21_binarith,t39_margrel1,d1_bvfunc_1,t19_binarith,t19_binarith,t7_binarith]), [file(binari_5,t54_binari_5),interesting(0.58)]). fof(t39_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k1_bvfunc_1(k1_bvfunc_1(k9_margrel1(A),A),A) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t21_binarith,d1_bvfunc_1,d1_bvfunc_1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1]), [file(binari_5,t39_binari_5),interesting(0.57)]). fof(t7_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k10_margrel1(B,C)) = k1_binari_5(k10_margrel1(A,B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_margrel1]), [file(binari_5,t7_binari_5),interesting(0.57)]). fof(t55_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_bvfunc_1(A,k1_bvfunc_1(B,C)) = k8_margrel1 => k1_bvfunc_1(k1_bvfunc_1(A,B),k1_bvfunc_1(A,C)) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,t19_binarith,t41_margrel1,t19_binarith,t39_margrel1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t40_margrel1,t23_binarith,t20_binarith,t50_margrel1,t20_binarith,t19_binarith]), [file(binari_5,t55_binari_5),interesting(0.55)]). fof(t10_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k3_binari_5(k8_margrel1,A) = k7_margrel1 ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t41_margrel1]), [file(binari_5,t10_binari_5),interesting(0.54)]). fof(t51_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_bvfunc_1(A,k1_bvfunc_1(B,C)) = k8_margrel1 => k1_bvfunc_1(B,k1_bvfunc_1(A,C)) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t20_binarith]), [file(binari_5,t51_binari_5),interesting(0.48)]). fof(t52_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( ( k1_bvfunc_1(A,k1_bvfunc_1(B,C)) = k8_margrel1 & B = k8_margrel1 ) => k1_bvfunc_1(A,C) = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,t41_margrel1,t7_binarith,d1_bvfunc_1]), [file(binari_5,t52_binari_5),interesting(0.48)]). fof(t30_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ! [D] : ( v2_margrel1(D) => ( ( k2_bvfunc_1(A,B) = k8_margrel1 & k2_bvfunc_1(C,D) = k8_margrel1 ) => k2_bvfunc_1(k10_margrel1(A,C),k10_margrel1(B,D)) = k8_margrel1 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_5,t24_binari_5,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t23_binari_5,d1_bvfunc_1,d1_bvfunc_1,t9_binarith,t9_binarith,t23_binarith,t23_binarith,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith,t50_margrel1,t20_binarith,t19_binarith]), [file(binari_5,t30_binari_5),interesting(0.47)]). fof(t32_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ! [D] : ( v2_margrel1(D) => ( ( k2_bvfunc_1(A,B) = k8_margrel1 & k2_bvfunc_1(C,D) = k8_margrel1 ) => k2_bvfunc_1(k1_binarith(A,C),k1_binarith(B,D)) = k8_margrel1 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_5,t24_binari_5,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t23_binari_5,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t10_binarith,t23_binarith,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t50_margrel1]), [file(binari_5,t32_binari_5),interesting(0.46)]). fof(t31_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ! [D] : ( v2_margrel1(D) => ( ( k2_bvfunc_1(A,B) = k8_margrel1 & k2_bvfunc_1(C,D) = k8_margrel1 ) => k2_bvfunc_1(k1_bvfunc_1(A,C),k1_bvfunc_1(B,D)) = k8_margrel1 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_5,t24_binari_5,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t23_binari_5,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t10_binarith,t10_binarith,t40_margrel1,t40_margrel1,t23_binarith,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t50_margrel1]), [file(binari_5,t31_binari_5),interesting(0.44)]). fof(t53_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( ( k1_bvfunc_1(A,k1_bvfunc_1(B,C)) = k8_margrel1 & B = k8_margrel1 & A = k8_margrel1 ) => C = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,t41_margrel1,t41_margrel1,t7_binarith,t7_binarith]), [file(binari_5,t53_binari_5),interesting(0.44)]). fof(t1_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k1_binari_5(k8_margrel1,A) = k9_margrel1(A) ) ), inference(mizar_proof,[status(thm)],[t50_margrel1]), [file(binari_5,t1_binari_5),interesting(0.40)]). fof(t11_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k3_binari_5(k7_margrel1,A) = k9_margrel1(A) ) ), inference(mizar_proof,[status(thm)],[t7_binarith]), [file(binari_5,t11_binari_5),interesting(0.39)]). fof(t18_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => k5_binari_5(k7_margrel1,A) = k9_margrel1(A) ) ), inference(mizar_proof,[status(thm)],[t14_binarith]), [file(binari_5,t18_binari_5),interesting(0.39)]). fof(t4_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k1_binari_5(A,B)) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1]), [file(binari_5,t4_binari_5),interesting(0.39)]). fof(t13_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k3_binari_5(A,B)) = k1_binarith(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1]), [file(binari_5,t13_binari_5),interesting(0.38)]). fof(t20_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k5_binari_5(A,B)) = k2_binarith(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1]), [file(binari_5,t20_binari_5),interesting(0.37)]). fof(t6_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k10_margrel1(B,C)) = k9_margrel1(k10_margrel1(k10_margrel1(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_margrel1]), [file(binari_5,t6_binari_5),interesting(0.33)]). fof(t16_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k1_binarith(B,C)) = k9_margrel1(k1_binarith(k1_binarith(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith]), [file(binari_5,t16_binari_5),interesting(0.32)]). fof(t36_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( k9_margrel1(A) = k8_margrel1 => k1_bvfunc_1(A,B) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t19_binarith]), [file(binari_5,t36_binari_5),interesting(0.30)]). fof(t38_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( ( k1_bvfunc_1(A,B) = k8_margrel1 & k1_bvfunc_1(A,k9_margrel1(B)) = k8_margrel1 ) => k9_margrel1(A) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,t39_margrel1,d1_bvfunc_1,t41_margrel1,t43_margrel1,t7_binarith]), [file(binari_5,t38_binari_5),interesting(0.26)]). fof(t40_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(k1_bvfunc_1(A,B),k1_bvfunc_1(k9_margrel1(k10_margrel1(B,C)),k9_margrel1(k10_margrel1(A,C)))) = k8_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_bvfunc_1,d1_bvfunc_1,t40_margrel1,t9_binarith,d1_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]), [file(binari_5,t40_binari_5),interesting(0.19)]). fof(t19_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ( k5_binari_5(A,A) = k8_margrel1 & k9_margrel1(k5_binari_5(A,A)) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t46_margrel1,t46_margrel1,t7_binarith,t41_margrel1,t41_margrel1]), [file(binari_5,t19_binari_5),interesting(0.16)]). fof(t5_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ( k1_binari_5(A,k9_margrel1(A)) = k8_margrel1 & k9_margrel1(k1_binari_5(A,k9_margrel1(A))) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t46_margrel1,t41_margrel1,t41_margrel1]), [file(binari_5,t5_binari_5),interesting(0.09)]). fof(t14_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ( k3_binari_5(A,k9_margrel1(A)) = k7_margrel1 & k9_margrel1(k3_binari_5(A,k9_margrel1(A))) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t18_binarith,t41_margrel1,t41_margrel1]), [file(binari_5,t14_binari_5),interesting(0.05)]). fof(t21_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ( k5_binari_5(A,k9_margrel1(A)) = k7_margrel1 & k9_margrel1(k5_binari_5(A,k9_margrel1(A))) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t17_binarith,t41_margrel1,t41_margrel1]), [file(binari_5,t21_binari_5),interesting(0.05)]). fof(t9_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k2_binarith(B,C)) = k2_bvfunc_1(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_binarith,d2_bvfunc_1]), [file(binari_5,t9_binari_5),interesting(0.02)]). 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(t7_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k7_margrel1) = A ) ), file(binarith,t7_binarith), [interesting(0.00)]). fof(t21_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,A) = A ) ), file(binarith,t21_binarith), [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(t18_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ), file(binarith,t18_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(t9_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k10_margrel1(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ), file(binarith,t9_binarith), [interesting(0.00)]). fof(t15_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k10_margrel1(B,C)) = k1_binarith(k9_margrel1(k1_binarith(A,B)),k9_margrel1(k1_binarith(A,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binarith,t9_binarith]), [file(binari_5,t15_binari_5),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(t13_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k8_margrel1,A) = k9_margrel1(A) ) ), file(binarith,t13_binarith), [interesting(0.00)]). fof(t14_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k7_margrel1,A) = A ) ), file(binarith,t14_binarith), [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(t46_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,k9_margrel1(A)) = k7_margrel1 ) ), file(margrel1,t46_margrel1), [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(t17_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ), file(binarith,t17_binarith), [interesting(0.00)]). fof(d3_bvfunc_1,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( r1_xreal_0(A,B) <=> k1_bvfunc_1(A,B) = k8_margrel1 ) ) ) ), file(bvfunc_1,d3_bvfunc_1), [interesting(0.00)]). fof(d1_bvfunc_1,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,B) = k1_binarith(k9_margrel1(A),B) ) ) ), file(bvfunc_1,d1_bvfunc_1), [interesting(0.00)]). fof(d2_bvfunc_1,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_bvfunc_1(A,B) = k9_margrel1(k2_binarith(A,B)) ) ) ), file(bvfunc_1,d2_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(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(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(d17_margrel1,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( ( ( A = k8_margrel1 & B = k8_margrel1 ) => k10_margrel1(A,B) = k8_margrel1 ) & ( ~ ( A = k8_margrel1 & B = k8_margrel1 ) => k10_margrel1(A,B) = k7_margrel1 ) ) ) ) ), file(margrel1,d17_margrel1), [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(t38_margrel1,theorem,( k7_margrel1 != k8_margrel1 ), file(margrel1,t38_margrel1), [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)]). fof(t33_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ! [D] : ( v2_margrel1(D) => ( ( k2_bvfunc_1(A,B) = k8_margrel1 & k2_bvfunc_1(C,D) = k8_margrel1 ) => k2_bvfunc_1(k2_bvfunc_1(A,C),k2_bvfunc_1(B,D)) = k8_margrel1 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_5,t24_binari_5,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t23_binari_5,d1_bvfunc_1,d1_bvfunc_1,t23_binari_5,t23_binari_5,t23_binari_5,t23_binari_5,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,d1_bvfunc_1,t9_binarith,t9_binarith,t10_binarith,t10_binarith,t10_binarith,t10_binarith,t40_margrel1,t40_margrel1,t40_margrel1,t40_margrel1,t23_binarith,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t23_binarith,t23_binarith,t23_binarith,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t23_binarith,t23_binarith,t23_binarith,t23_binarith,t23_binarith,t23_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t50_margrel1,t50_margrel1,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t20_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t19_binarith,t50_margrel1,t50_margrel1,t50_margrel1]), [file(binari_5,t33_binari_5),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(t16_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,A) = A ) ), file(binarith,t16_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(t8_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k1_binarith(B,C)) = k10_margrel1(k9_margrel1(k10_margrel1(A,B)),k9_margrel1(k10_margrel1(A,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_binarith,t10_binarith]), [file(binari_5,t8_binari_5),interesting(0.00)]). fof(t38_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k2_binarith(B,C)) = k2_binarith(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ), file(binarith,t38_binarith), [interesting(0.00)]).