fof(t21_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,A) = A ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t7_binarith,t39_margrel1]), [file(binarith,t21_binarith),interesting(1.00)]). fof(t33_binarith,theorem,( k4_binarith(k8_margrel1,k7_margrel1) = k8_margrel1 ), inference(mizar_proof,[status(thm)],[t41_margrel1,t17_binarith]), [file(binarith,t33_binarith),interesting(0.98)]). fof(t16_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,A) = A ) ), inference(mizar_proof,[status(thm)],[t45_margrel1,t45_margrel1,t39_margrel1]), [file(binarith,t16_binarith),interesting(0.96)]). fof(t36_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k2_binarith(A,B)) = k1_binarith(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t26_binarith,t23_binarith,t20_binarith,t21_binarith,t20_binarith,t18_binarith,t19_binarith,t50_margrel1]), [file(binarith,t36_binarith),interesting(0.96)]). fof(t35_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k10_margrel1(k9_margrel1(A),B)) = k1_binarith(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t52_margrel1,t16_binarith,t9_binarith,t40_margrel1,t25_binarith,t26_binarith]), [file(binarith,t35_binarith),interesting(0.95)]). fof(t17_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t16_binarith,t16_binarith,t47_margrel1]), [file(binarith,t17_binarith),interesting(0.92)]). fof(t37_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k2_binarith(k9_margrel1(A),B)) = k1_binarith(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t20_binarith,t26_binarith,t23_binarith,t20_binarith,t21_binarith,t20_binarith,t18_binarith,t19_binarith,t50_margrel1]), [file(binarith,t37_binarith),interesting(0.90)]). fof(t15_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(A,A) = k7_margrel1 ) ), inference(mizar_proof,[status(thm)],[t46_margrel1,t46_margrel1,t7_binarith]), [file(binarith,t15_binarith),interesting(0.90)]). fof(t7_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k7_margrel1) = A ) ), inference(mizar_proof,[status(thm)],[t41_margrel1,t50_margrel1,t40_margrel1]), [file(binarith,t7_binarith),interesting(0.87)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t16_binarith,t19_binarith,t19_binarith,t7_binarith,t7_binarith,t7_binarith,t39_margrel1]), [file(binarith,t23_binarith),interesting(0.87)]). fof(t34_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k2_binarith(k2_binarith(A,B),C) = k2_binarith(A,k2_binarith(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t9_binarith,t40_margrel1,t9_binarith,t40_margrel1,t52_margrel1,t22_binarith,t22_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t22_binarith,t52_margrel1,t52_margrel1,t20_binarith,t20_binarith,t52_margrel1,t52_margrel1,t52_margrel1,t52_margrel1,t10_binarith,t52_margrel1,t22_binarith,t52_margrel1,t52_margrel1,t9_binarith,t40_margrel1,t9_binarith,t40_margrel1,t22_binarith,t22_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t20_binarith,t52_margrel1]), [file(binarith,t34_binarith),interesting(0.87)]). fof(t26_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k10_margrel1(k9_margrel1(A),B)) = k1_binarith(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t49_margrel1,t7_binarith,t19_binarith,d16_margrel1,t50_margrel1,t39_margrel1]), [file(binarith,t26_binarith),interesting(0.86)]). fof(t14_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k7_margrel1,A) = A ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t50_margrel1,t49_margrel1,t7_binarith]), [file(binarith,t14_binarith),interesting(0.85)]). fof(t25_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binarith(A,B)) = A ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t50_margrel1,t49_margrel1,t39_margrel1]), [file(binarith,t25_binarith),interesting(0.82)]). fof(t13_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k8_margrel1,A) = k9_margrel1(A) ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t49_margrel1,t50_margrel1,t7_binarith]), [file(binarith,t13_binarith),interesting(0.81)]). fof(t24_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k10_margrel1(A,B)) = A ) ) ), inference(mizar_proof,[status(thm)],[t19_binarith,t7_binarith,t49_margrel1,t39_margrel1]), [file(binarith,t24_binarith),interesting(0.81)]). fof(t48_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( r1_binarith(A,B,C) => k9_binarith(A,k10_binarith(A,B,C)) = k23_binop_2(k9_binarith(A,B),k9_binarith(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d10_binarith,d1_cqc_lang,t47_binarith]), [file(binarith,t48_binarith),interesting(0.81)]). fof(t39_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => k5_binarith(k2_xcmplx_0(A,B),B) = A ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t21_xreal_1,d3_binarith]), [file(binarith,t39_binarith),interesting(0.80)]). fof(t19_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k8_margrel1) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t49_margrel1,d16_margrel1]), [file(binarith,t19_binarith),interesting(0.79)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_margrel1,t50_margrel1,t50_margrel1,t49_margrel1,t7_binarith,t49_margrel1,t49_margrel1,t39_margrel1]), [file(binarith,t22_binarith),interesting(0.78)]). fof(t47_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => k23_binop_2(k9_binarith(A,k10_binarith(A,B,C)),k2_cqc_lang(k5_numbers,k11_binarith(A,B,C),k7_margrel1,0,k3_series_1(2,A))) = k23_binop_2(k9_binarith(A,B),k9_binarith(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_binarith,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,t41_binarith,t42_binarith,t25_finseq_4,t25_finseq_4,t16_binarith,d1_cqc_lang,t4_finseq_1,d1_tarski,t25_finseq_4,t15_binarith,t15_binarith,t25_finseq_4,t25_finseq_4,d5_binarith,d8_binarith,t25_finseq_4,t25_finseq_4,t49_margrel1,d1_cqc_lang,t4_finseq_1,d1_tarski,t25_finseq_4,t17_binarith,t41_margrel1,t17_binarith,t41_margrel1,t25_finseq_4,t25_finseq_4,d5_binarith,d8_binarith,t25_finseq_4,t49_margrel1,d1_cqc_lang,t4_finseq_1,d1_tarski,t25_finseq_4,t17_binarith,t41_margrel1,t17_binarith,t41_margrel1,t25_finseq_4,t25_finseq_4,d5_binarith,d8_binarith,t25_finseq_4,t25_finseq_4,t16_binarith,d1_cqc_lang,t38_margrel1,t30_power,t4_finseq_1,d1_tarski,t25_finseq_4,t15_binarith,t17_binarith,t34_binarith,t41_margrel1,t25_finseq_4,t25_finseq_4,d5_binarith,d8_binarith,t40_binarith,t137_finseq_2,t137_finseq_2,t3_binarith,t3_binarith,t3_binarith,t3_binarith,t44_binarith,t44_binarith,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,t45_margrel1,t45_margrel1,t45_margrel1,t7_binarith,t7_binarith,t15_binarith,t15_binarith,d1_cqc_lang,d1_cqc_lang,t45_margrel1,t45_margrel1,t45_margrel1,t7_binarith,t7_binarith,t15_binarith,t33_binarith,t39_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,t45_margrel1,t45_margrel1,t45_margrel1,t7_binarith,t7_binarith,t33_binarith,t39_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,d1_cqc_lang,t45_margrel1,t45_margrel1,t39_margrel1,t39_margrel1,t45_margrel1,t7_binarith,t7_binarith,t33_binarith,t39_margrel1,t39_margrel1,t15_binarith,d1_cqc_lang,t38_margrel1,t32_power,t30_power,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,t45_margrel1,t45_margrel1,t45_margrel1,t7_binarith,t7_binarith,t33_binarith,t39_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,d1_cqc_lang,t45_margrel1,t39_margrel1,t39_margrel1,t45_margrel1,t45_margrel1,t7_binarith,t7_binarith,t33_binarith,t39_margrel1,t39_margrel1,t15_binarith,d1_cqc_lang,t38_margrel1,t32_power,t30_power,d1_cqc_lang,d1_cqc_lang,t39_margrel1,t39_margrel1,t16_binarith,t45_margrel1,t45_margrel1,t7_binarith,t7_binarith,t39_margrel1,t39_margrel1,t15_binarith,t15_binarith,d1_cqc_lang,t38_margrel1,t32_power,t30_power,t39_margrel1,t39_margrel1,t16_binarith,t39_margrel1,t39_margrel1,t16_binarith,t39_margrel1,t39_margrel1,t16_binarith,t21_binarith,t21_binarith,t39_margrel1,t39_margrel1,t15_binarith,t33_binarith,t39_margrel1,d1_cqc_lang,t38_margrel1,t32_power,t30_power,d1_cqc_lang,t45_binarith,t46_binarith,t46_binarith,t46_binarith,s1_binarith]), [file(binarith,t47_binarith),interesting(0.76)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t52_margrel1,t40_margrel1]), [file(binarith,t20_binarith),interesting(0.75)]). fof(t27_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binarith(k9_margrel1(A),B)) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t7_binarith,t49_margrel1,t49_margrel1,t39_margrel1]), [file(binarith,t27_binarith),interesting(0.74)]). fof(t18_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[t47_margrel1]), [file(binarith,t18_binarith),interesting(0.74)]). fof(t52_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(k5_binarith(A,B),A) ) ) ), inference(mizar_proof,[status(thm)],[t18_nat_1,t106_real_2,d3_binarith,d3_binarith,t18_nat_1]), [file(binarith,t52_binarith),interesting(0.74)]). 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)) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1]), [file(binarith,t10_binarith),interesting(0.71)]). 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)) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t40_margrel1]), [file(binarith,t9_binarith),interesting(0.71)]). 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)) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_binarith,t52_margrel1,t52_margrel1,t9_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t9_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t52_margrel1]), [file(binarith,t38_binarith),interesting(0.69)]). fof(t51_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => k5_binarith(A,A) = 0 ) ), inference(mizar_proof,[status(thm)],[d3_binarith]), [file(binarith,t51_binarith),interesting(0.67)]). fof(t53_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(B,A) => k2_xcmplx_0(k5_binarith(A,B),B) = A ) ) ) ), inference(mizar_proof,[status(thm)],[t28_nat_1,t39_binarith]), [file(binarith,t53_binarith),interesting(0.64)]). fof(l1_binarith,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k2_binop_1(k5_numbers,k5_numbers,k5_numbers,k47_binop_2,A,B) = k23_binop_2(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d23_binop_2]), [file(binarith,l1_binarith),interesting(0.63)]). fof(t50_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) => k5_binarith(B,A) = k6_xcmplx_0(B,A) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_xreal_1,d3_binarith]), [file(binarith,t50_binarith),interesting(0.63)]). fof(t42_binarith,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(1,k6_margrel1)) => ( A = k12_finseq_1(k6_margrel1,k8_margrel1) => k9_binarith(1,A) = 1 ) ) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t25_finseq_4,t38_margrel1,d6_binarith,d1_cqc_lang,t25_finseq_4,t12_finsop_1,d3_binarith,t29_power]), [file(binarith,t42_binarith),interesting(0.62)]). fof(t40_binarith,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(1,k6_margrel1)) => ( A = k12_finseq_1(k6_margrel1,k7_margrel1) | A = k12_finseq_1(k6_margrel1,k8_margrel1) ) ) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t25_finseq_4,t25_finseq_4,t39_margrel1]), [file(binarith,t40_binarith),interesting(0.61)]). fof(s1_binarith,theorem, ( ( p1_s1_binarith(1) & ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ( p1_s1_binarith(A) => p1_s1_binarith(k23_binop_2(A,1)) ) ) ) => ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => p1_s1_binarith(A) ) ), inference(mizar_proof,[status(thm)],[t51_card_1,s1_nat_1]), [file(binarith,s1_binarith),interesting(0.61)]). fof(t41_binarith,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(1,k6_margrel1)) => ( A = k12_finseq_1(k6_margrel1,k7_margrel1) => k9_binarith(1,A) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t25_finseq_4,d6_binarith,d1_cqc_lang,t25_finseq_4,t12_finsop_1]), [file(binarith,t41_binarith),interesting(0.60)]). fof(t49_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(A,C) & k5_binarith(B,A) = k5_binarith(C,A) ) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_xreal_1,d3_binarith,t50_xreal_1,d3_binarith]), [file(binarith,t49_binarith),interesting(0.59)]). fof(t12_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,B) = k9_margrel1(k1_binarith(k9_margrel1(A),k9_margrel1(B))) ) ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t40_margrel1,t10_binarith]), [file(binarith,t12_binarith),interesting(0.56)]). fof(t3_binarith,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,D,k12_finseq_1(B,C)),k23_binop_2(A,1)) = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t56_finseq_1,d3_finseq_1,t109_finseq_2,t84_finseq_4,t25_finseq_4]), [file(binarith,t3_binarith),interesting(0.52)]). fof(t5_binarith,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( r2_hidden(A,k2_finseq_1(B)) & v1_xboole_0(A) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_card_1,t3_finseq_1]), [file(binarith,t5_binarith),interesting(0.52)]). fof(t2_binarith,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( m2_finseq_2(E,C,k4_finseq_2(B,C)) => ( r2_hidden(A,k2_finseq_1(B)) => k4_finseq_4(k5_numbers,C,k8_finseq_1(C,E,k12_finseq_1(C,D)),A) = k4_finseq_4(k5_numbers,C,E,A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,d3_finseq_1,t83_finseq_4]), [file(binarith,t2_binarith),interesting(0.46)]). fof(t44_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k6_margrel1) => ! [E] : ( m1_subset_1(E,k6_margrel1) => k11_binarith(A,B,C) = k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,D)),k12_binarith(A,1,k6_margrel1,C,k13_binarith(k6_margrel1,E))),k23_binop_2(A,1)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_finseq_1,t43_binarith,t2_binarith,t2_binarith,t39_nat_1,t31_xreal_1,d5_binarith]), [file(binarith,t44_binarith),interesting(0.29)]). fof(t45_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k6_margrel1) => ! [E] : ( m1_subset_1(E,k6_margrel1) => k10_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,D)),k12_binarith(A,1,k6_margrel1,C,k13_binarith(k6_margrel1,E))) = k12_binarith(A,1,k6_margrel1,k10_binarith(A,B,C),k13_binarith(k6_margrel1,k4_binarith(k4_binarith(D,E),k11_binarith(A,B,C)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_finseq_1,t2_binarith,d8_binarith,t2_binarith,t2_binarith,t43_binarith,d1_tarski,t3_binarith,t44_binarith,t3_binarith,t3_binarith,d2_xboole_0,d8_binarith]), [file(binarith,t45_binarith),interesting(0.29)]). fof(t43_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k6_margrel1) => ! [E] : ( m1_subset_1(E,k6_margrel1) => ! [F] : ( m2_subset_1(F,k1_numbers,k5_numbers) => ( r2_hidden(F,k2_finseq_1(A)) => k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,D)),k12_binarith(A,1,k6_margrel1,C,k13_binarith(k6_margrel1,E))),F) = k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,C),F) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_binarith,d5_binarith,t31_xreal_1,t3_finseq_1,t2_xreal_1,t39_nat_1,t2_binarith,t2_binarith,t29_nat_1,t2_xreal_1,d5_binarith,d5_binarith,t51_card_1,t3_finseq_1,s1_binarith]), [file(binarith,t43_binarith),interesting(0.20)]). fof(t11_binarith,theorem,( $true ), file(binarith,t11_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(d16_margrel1,definition,( ! [A] : ( v2_margrel1(A) => ( ( A = k7_margrel1 => k9_margrel1(A) = k8_margrel1 ) & ( A != k7_margrel1 => k9_margrel1(A) = k7_margrel1 ) ) ) ), file(margrel1,d16_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(t50_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k8_margrel1,A) = A ) ), file(margrel1,t50_margrel1), [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(t1_binarith,theorem,( $true ), file(binarith,t1_binarith), [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(t28_binarith,theorem,( $true ), file(binarith,t28_binarith), [interesting(0.00)]). fof(t29_binarith,theorem,( $true ), file(binarith,t29_binarith), [interesting(0.00)]). fof(t30_binarith,theorem,( $true ), file(binarith,t30_binarith), [interesting(0.00)]). fof(t31_binarith,theorem,( $true ), file(binarith,t31_binarith), [interesting(0.00)]). fof(t32_binarith,theorem,( $true ), file(binarith,t32_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(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(t47_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k9_margrel1(k10_margrel1(A,k9_margrel1(A))) = k8_margrel1 ) ), file(margrel1,t47_margrel1), [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(d10_binarith,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( r1_binarith(A,B,C) <=> k11_binarith(A,B,C) = k7_margrel1 ) ) ) ) ), file(binarith,d10_binarith), [interesting(0.00)]). fof(d1_cqc_lang,definition,( ! [A,B,C,D] : ( ( A = B => k1_cqc_lang(A,B,C,D) = C ) & ( A != B => k1_cqc_lang(A,B,C,D) = D ) ) ), file(cqc_lang,d1_cqc_lang), [interesting(0.00)]). fof(d5_binarith,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [D] : ( m2_finseq_2(D,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( D = k7_binarith(A,B,C) <=> ( k4_finseq_4(k5_numbers,k6_margrel1,D,1) = k7_margrel1 & ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r1_xreal_0(1,E) => ( r1_xreal_0(A,E) | k4_finseq_4(k5_numbers,k6_margrel1,D,k23_binop_2(E,1)) = k3_binarith(k3_binarith(k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,E),k4_finseq_4(k5_numbers,k6_margrel1,C,E)),k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,E),k4_finseq_4(k5_numbers,k6_margrel1,D,E))),k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,C,E),k4_finseq_4(k5_numbers,k6_margrel1,D,E))) ) ) ) ) ) ) ) ) ) ), file(binarith,d5_binarith), [interesting(0.00)]). fof(t117_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_2(B,A,k4_finseq_2(1,A)) => ? [C] : ( m1_subset_1(C,A) & B = k12_finseq_1(A,C) ) ) ) ), file(finseq_2,t117_finseq_2), [interesting(0.00)]). fof(t25_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => k4_finseq_4(k5_numbers,A,k12_finseq_1(A,B),1) = B ) ) ), file(finseq_4,t25_finseq_4), [interesting(0.00)]). fof(d6_binarith,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k5_numbers,k4_finseq_2(A,k5_numbers)) => ( C = k8_binarith(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k4_finseq_4(k5_numbers,k5_numbers,C,D) = k2_cqc_lang(k5_numbers,k4_finseq_4(k5_numbers,k6_margrel1,B,D),k7_margrel1,0,k3_series_1(2,k5_binarith(D,1))) ) ) ) ) ) ) ), file(binarith,d6_binarith), [interesting(0.00)]). fof(t12_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ), file(finsop_1,t12_finsop_1), [interesting(0.00)]). fof(t38_margrel1,theorem,( k7_margrel1 != k8_margrel1 ), file(margrel1,t38_margrel1), [interesting(0.00)]). fof(d3_binarith,definition,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ( r1_xreal_0(0,k6_xcmplx_0(A,B)) => k5_binarith(A,B) = k6_xcmplx_0(A,B) ) & ( ~ r1_xreal_0(0,k6_xcmplx_0(A,B)) => k5_binarith(A,B) = 0 ) ) ) ) ), file(binarith,d3_binarith), [interesting(0.00)]). fof(t29_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(A,0) = 1 ) ), file(power,t29_power), [interesting(0.00)]). fof(t4_finseq_1,theorem, ( k2_finseq_1(0) = k1_xboole_0 & k2_finseq_1(1) = k1_tarski(1) & k2_finseq_1(2) = k2_tarski(1,2) ), file(finseq_1,t4_finseq_1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(d8_binarith,definition,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [D] : ( m2_finseq_2(D,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( D = k10_binarith(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k2_finseq_1(A)) => k4_finseq_4(k5_numbers,k6_margrel1,D,E) = k4_binarith(k4_binarith(k4_finseq_4(k5_numbers,k6_margrel1,B,E),k4_finseq_4(k5_numbers,k6_margrel1,C,E)),k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,C),E)) ) ) ) ) ) ) ) ), file(binarith,d8_binarith), [interesting(0.00)]). fof(t30_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(A,1) = A ) ), file(power,t30_power), [interesting(0.00)]). fof(t137_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_2(C,B,k4_finseq_2(k1_nat_1(A,1),B)) => ? [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) & ? [E] : ( m1_subset_1(E,B) & C = k8_finseq_1(B,D,k12_finseq_1(B,E)) ) ) ) ) ) ), file(finseq_2,t137_finseq_2), [interesting(0.00)]). fof(t56_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( B = k9_finseq_1(A) <=> ( k3_finseq_1(B) = 1 & k2_relat_1(B) = k1_tarski(A) ) ) ) ), file(finseq_1,t56_finseq_1), [interesting(0.00)]). fof(d3_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B = k3_finseq_1(A) <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ), file(finseq_1,d3_finseq_1), [interesting(0.00)]). fof(t109_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_2(C,B,k4_finseq_2(A,B)) => k3_finseq_1(C) = A ) ) ) ), file(finseq_2,t109_finseq_2), [interesting(0.00)]). fof(t84_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r2_hidden(A,k4_finseq_1(D)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),k1_nat_1(k3_finseq_1(C),A)) = k4_finseq_4(k5_numbers,B,D,A) ) ) ) ) ) ), file(finseq_4,t84_finseq_4), [interesting(0.00)]). fof(t5_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( A = 0 | r2_hidden(A,k2_finseq_1(A)) ) ) ), file(finseq_1,t5_finseq_1), [interesting(0.00)]). fof(t31_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ), file(xreal_1,t31_xreal_1), [interesting(0.00)]). fof(t3_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r2_hidden(A,k2_finseq_1(B)) <=> ( r1_xreal_0(1,A) & r1_xreal_0(A,B) ) ) ) ) ), file(finseq_1,t3_finseq_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(t39_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(1,A) => A = 0 ) ) ), file(nat_1,t39_nat_1), [interesting(0.00)]). fof(t83_finseq_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m2_finseq_1(C,B) => ! [D] : ( m2_finseq_1(D,B) => ( r2_hidden(A,k4_finseq_1(C)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),A) = k4_finseq_4(k5_numbers,B,C,A) ) ) ) ) ) ), file(finseq_4,t83_finseq_4), [interesting(0.00)]). fof(t29_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => r1_xreal_0(A,k2_xcmplx_0(A,B)) ) ) ), file(nat_1,t29_nat_1), [interesting(0.00)]). fof(t51_card_1,theorem,( 0 = k1_xboole_0 ), file(card_1,t51_card_1), [interesting(0.00)]). fof(s1_nat_1,theorem, ( ( p1_s1_nat_1(0) & ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( p1_s1_nat_1(A) => p1_s1_nat_1(k1_nat_1(A,1)) ) ) ) => ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => p1_s1_nat_1(A) ) ), file(nat_1,s1_nat_1), [interesting(0.00)]). fof(t32_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => k3_power(A,k2_xcmplx_0(B,C)) = k3_xcmplx_0(k3_power(A,B),k3_power(A,C)) ) ) ) ) ), file(power,t32_power), [interesting(0.00)]). fof(t11_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => k2_xboole_0(k2_finseq_1(A),k1_tarski(k2_xcmplx_0(A,1))) = k2_finseq_1(k2_xcmplx_0(A,1)) ) ), file(finseq_1,t11_finseq_1), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(t21_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(k2_xcmplx_0(A,B),C) <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ), file(xreal_1,t21_xreal_1), [interesting(0.00)]). fof(t5_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( ( v1_setwiseo(D,A) | r1_xreal_0(1,k3_finseq_1(C)) ) => k2_finsop_1(A,k8_finseq_1(A,C,k12_finseq_1(A,B)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,C,D),B) ) ) ) ) ) ), file(finsop_1,t5_finsop_1), [interesting(0.00)]). fof(d23_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) & m2_relset_1(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) ) => ( A = k47_binop_2 <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_binop_1(k5_numbers,k5_numbers,k5_numbers,A,B,C) = k23_binop_2(B,C) ) ) ) ) ), file(binop_2,d23_binop_2), [interesting(0.00)]). fof(t46_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m1_subset_1(C,k6_margrel1) => k9_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C))) = k23_binop_2(k9_binarith(A,B),k2_cqc_lang(k5_numbers,C,k7_margrel1,0,k3_series_1(2,A))) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_finseq_1,t2_binarith,d6_binarith,t2_binarith,d1_tarski,t3_binarith,t3_binarith,t39_binarith,d2_xboole_0,d6_binarith,t5_finsop_1,l1_binarith]), [file(binarith,t46_binarith),interesting(0.00)]). fof(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_xreal_1), [interesting(0.00)]). fof(t4_binarith,theorem,( $true ), file(binarith,t4_binarith), [interesting(0.00)]). fof(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_nat_1), [interesting(0.00)]). fof(t106_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ ( r1_xreal_0(0,k2_xcmplx_0(A,k4_xcmplx_0(B))) & r1_xreal_0(k6_xcmplx_0(B,A),0) & r1_xreal_0(k2_xcmplx_0(k4_xcmplx_0(A),B),0) & r1_xreal_0(k2_xcmplx_0(B,k4_xcmplx_0(C)),k6_xcmplx_0(A,C)) & r1_xreal_0(k6_xcmplx_0(B,C),k2_xcmplx_0(A,k4_xcmplx_0(C))) & r1_xreal_0(k6_xcmplx_0(C,A),k6_xcmplx_0(C,B)) ) & r1_xreal_0(B,A) ) ) ) ) ), file(real_2,t106_real_2), [interesting(0.00)]). fof(t28_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ~ ( r1_xreal_0(A,B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => B != k2_xcmplx_0(A,C) ) ) ) ) ), file(nat_1,t28_nat_1), [interesting(0.00)]). fof(t6_binarith,theorem,( $true ), file(binarith,t6_binarith), [interesting(0.00)]). fof(t8_binarith,theorem,( $true ), file(binarith,t8_binarith), [interesting(0.00)]).