fof(t17_binari_4,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(k8_margrel1,A) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[d1_binarith,t41_margrel1,t49_margrel1,t41_margrel1]), [file(binari_4,t17_binari_4),interesting(1.00)]). fof(t33_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ? [C] : ( m1_subset_1(C,k6_margrel1) & k2_binari_4(k1_nat_1(A,1),B) = k8_finseq_1(k6_margrel1,k2_binari_4(A,B),k13_binarith(k6_margrel1,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t137_finseq_2,t109_finseq_2,t3_finseq_1,t29_nat_1,t2_xreal_1,t24_finseq_4,t32_binari_4,t24_finseq_4,d3_finseq_1,d7_finseq_1,t139_finseq_2,t113_finseq_2,t14_finseq_1,t117_finseq_2,t47_finseq_1]), [file(binari_4,t33_binari_4),interesting(0.90)]). fof(t2_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => r1_xreal_0(A,k3_series_1(2,A)) ) ), inference(mizar_proof,[status(thm)],[t30_power,t20_nat_1,t30_power,t32_power,t1_binari_4,t2_xreal_1,s1_nat_1]), [file(binari_4,t2_binari_4),interesting(0.82)]). fof(t9_binari_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( r1_xreal_0(A,k2_xcmplx_0(B,C)) => ( r1_xreal_0(0,B) | r1_xreal_0(0,C) | ( ~ r1_xreal_0(B,A) & ~ r1_xreal_0(C,A) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_xreal_1,t10_xreal_1,t11_xreal_1,t10_xreal_1]), [file(binari_4,t9_binari_4),interesting(0.80)]). fof(l35_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( k6_int_1(B,k3_series_1(2,A)) = k6_int_1(C,k3_series_1(2,A)) => ( r1_xreal_0(0,B) | r1_xreal_0(0,C) | k2_binari_4(A,B) = k2_binari_4(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_binari_4,d2_binari_4,d1_absvalue,d1_binari_4,t8_xreal_1,t16_int_1,d1_absvalue,d1_binari_4,t8_xreal_1,t16_int_1,t101_newton,l33_binari_4,t3_finseq_1,t109_finseq_2,t11_xreal_1,d3_binarith,t148_xreal_1,t2_xreal_1,d1_absvalue,t24_finseq_4,d1_binari_3,l32_binari_4,d1_binari_3,t24_finseq_4,d1_absvalue,t139_finseq_2]), [file(binari_4,l35_binari_4),interesting(0.77)]). fof(t31_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_int_1(B,C,k3_series_1(2,A)) => k1_binari_3(A,B) = k1_binari_3(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t12_int_3,t101_newton,t101_newton,t30_binari_4]), [file(binari_4,t31_binari_4),interesting(0.75)]). fof(t22_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,A) => r1_xreal_0(k1_binari_4(B,C),k1_binari_4(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_4,t2_xreal_1,d1_binari_4]), [file(binari_4,t22_binari_4),interesting(0.75)]). fof(t34_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ? [C] : ( m1_subset_1(C,k6_margrel1) & k1_binari_3(k1_nat_1(A,1),B) = k8_finseq_1(k6_margrel1,k1_binari_3(A,B),k13_binarith(k6_margrel1,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t33_binari_4,d1_absvalue,d2_binari_4,d2_binari_4]), [file(binari_4,t34_binari_4),interesting(0.74)]). fof(t24_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(A,k3_series_1(2,B)) => k1_binari_4(B,A) = B ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_4]), [file(binari_4,t24_binari_4),interesting(0.73)]). fof(t29_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( r1_int_1(B,C,k3_series_1(2,A)) => ( ( ~ ( r1_xreal_0(0,B) & r1_xreal_0(0,C) ) & ~ ( ~ r1_xreal_0(0,B) & ~ r1_xreal_0(0,C) ) ) | k2_binari_4(A,B) = k2_binari_4(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t12_int_3,l34_binari_4,l35_binari_4]), [file(binari_4,t29_binari_4),interesting(0.72)]). fof(t32_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,A) ) => k4_finseq_4(k5_numbers,k6_margrel1,k2_binari_4(k1_nat_1(A,1),B),C) = k4_finseq_4(k5_numbers,k6_margrel1,k2_binari_4(A,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_finseq_1,t29_nat_1,t2_xreal_1,t3_finseq_1,t29_nat_1,t22_binari_4,t28_nat_1,d1_binari_4,d1_absvalue,t8_xreal_1,d1_absvalue,t32_power,t101_newton,t63_nat_1,t101_newton,t14_int_3,t101_newton,t77_nat_1,d1_binari_4,d1_absvalue,t8_xreal_1,d1_absvalue,t101_newton,t14_int_3,d1_binari_4,t8_xreal_1,d3_binarith,t148_xreal_1,t2_xreal_1,t2_xreal_1,l32_binari_4,t16_int_1,d2_binari_4,d1_absvalue,d1_binari_3,d2_binari_4,d1_absvalue,d1_binari_3,d2_binari_4,d1_binari_3,d2_binari_4,d1_binari_3]), [file(binari_4,t32_binari_4),interesting(0.72)]). fof(t1_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(A,0) => r1_xreal_0(k1_nat_1(A,1),k2_nat_1(A,2)) ) ) ), inference(mizar_proof,[status(thm)],[t20_int_1,t8_xreal_1]), [file(binari_4,t1_binari_4),interesting(0.71)]). fof(t3_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k7_euclid(A,k5_euclid(A),k5_euclid(A)) = k5_euclid(A) ) ), inference(mizar_proof,[status(thm)],[d1_funct_2,d4_finseq_1,t119_zfmisc_1,d4_rvsum_1,t84_funcop_1,d4_euclid,t68_finseq_2,d4_euclid,t68_finseq_2,d4_euclid,t70_finseq_2,t26_rvsum_1,t17_finseq_1]), [file(binari_4,t3_binari_4),interesting(0.70)]). fof(l34_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( r1_xreal_0(0,B) & r1_xreal_0(0,C) & k6_int_1(B,k3_series_1(2,A)) = k6_int_1(C,k3_series_1(2,A)) ) => k2_binari_4(A,B) = k2_binari_4(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_binari_4,d2_binari_4,t3_finseq_1,t11_xreal_1,d3_binarith,t148_xreal_1,t2_xreal_1,d1_absvalue,t39_power,t9_int_3,t101_newton,t109_finseq_2,t24_finseq_4,d1_binari_3,l32_binari_4,t24_finseq_4,d1_binari_3,t139_finseq_2]), [file(binari_4,l34_binari_4),interesting(0.67)]). fof(t23_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( r1_xreal_0(1,A) => k1_binari_4(A,1) = A ) ) ), inference(mizar_proof,[status(thm)],[t40_power,d1_binari_4]), [file(binari_4,t23_binari_4),interesting(0.65)]). fof(t15_binari_4,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(1,k6_margrel1)) => ( A = k13_binarith(k6_margrel1,k8_margrel1) => k4_binari_2(1,A) = k1_real_1(1) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t24_finseq_4,t57_finseq_1,d3_binari_2,t38_margrel1,t42_binarith,t30_power]), [file(binari_4,t15_binari_4),interesting(0.64)]). fof(t26_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k2_binari_4(A,0) = k5_euclid(A) ) ), inference(mizar_proof,[status(thm)],[d2_binari_4,t7_absvalue,t26_binari_3]), [file(binari_4,t26_binari_4),interesting(0.63)]). fof(t14_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ( ~ v1_xboole_0(C) & m2_subset_1(C,k1_numbers,k5_numbers) ) => ( r1_xreal_0(k1_nat_1(A,B),k5_real_1(k3_series_1(2,k5_binarith(C,1)),1)) => k4_binari_2(C,k10_binarith(C,k1_binari_3(C,A),k1_binari_3(C,B))) = k1_nat_1(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_binari_4,t39_nat_1,t3_finseq_1,d1_binari_3,t5_jordan4,t78_nat_1,d1_cqc_lang,d1_binari_3,t5_jordan4,t78_nat_1,d1_cqc_lang,d8_binarith,t14_binarith,t14_binarith,t13_binari_4,d3_binari_2,t39_nat_1,t11_xreal_1,d3_binarith,t148_xreal_1,t44_power,t92_real_1,t2_xreal_1,t11_binari_4]), [file(binari_4,t14_binari_4),interesting(0.63)]). fof(t25_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(A,k3_series_1(2,B)) & r1_xreal_0(k1_binari_4(B,A),B) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_4,t2_xreal_1,t10_pre_ff]), [file(binari_4,t25_binari_4),interesting(0.62)]). fof(t28_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( k6_int_1(B,k3_series_1(2,A)) = k6_int_1(C,k3_series_1(2,A)) => ( ( ~ ( r1_xreal_0(0,B) & r1_xreal_0(0,C) ) & ~ ( ~ r1_xreal_0(0,B) & ~ r1_xreal_0(0,C) ) ) | k2_binari_4(A,B) = k2_binari_4(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l34_binari_4,l35_binari_4]), [file(binari_4,t28_binari_4),interesting(0.62)]). fof(t21_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(B,A) => r1_xreal_0(k1_binari_4(C,B),k1_binari_4(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_4,t2_xreal_1,d1_binari_4]), [file(binari_4,t21_binari_4),interesting(0.60)]). fof(t20_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => k6_int_1(k3_xcmplx_0(B,A),A) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t15_int_3,t101_newton,t77_nat_1,t101_newton,t78_nat_1]), [file(binari_4,t20_binari_4),interesting(0.59)]). fof(t7_binari_4,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)) => ( B = k5_euclid(A) => k4_binari_2(A,B) = 0 ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t39_nat_1,t3_finseq_1,t24_finseq_4,t2_jordan2b,d13_margrel1,d3_binari_2,t7_binari_3]), [file(binari_4,t7_binari_4),interesting(0.50)]). fof(t16_binari_4,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(1,k6_margrel1)) => ( A = k13_binarith(k6_margrel1,k7_margrel1) => k4_binari_2(1,A) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t24_finseq_4,t57_finseq_1,d3_binari_2,t41_binarith]), [file(binari_4,t16_binari_4),interesting(0.49)]). fof(t11_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(k1_nat_1(B,C),k5_real_1(k3_series_1(2,A),1)) => k9_binarith(A,k10_binarith(A,k1_binari_3(A,B),k1_binari_3(A,C))) = k1_nat_1(B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_binari_4,t10_binari_4,d10_binarith,t48_binarith,t36_binari_3,t36_binari_3]), [file(binari_4,t11_binari_4),interesting(0.47)]). fof(t13_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(k1_nat_1(B,C),k5_real_1(k3_series_1(2,k5_binarith(A,1)),1)) => k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,k1_binari_3(A,B),k1_binari_3(A,C)),A) = k7_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_margrel1,t8_binari_4,t39_nat_1,t3_finseq_1,d1_binari_3,t5_jordan4,t78_nat_1,d1_cqc_lang,d1_binari_3,t5_jordan4,t78_nat_1,d1_cqc_lang,t39_nat_1,t11_xreal_1,d3_binarith,t148_xreal_1,t44_power,t92_real_1,t2_xreal_1,d8_binarith,t14_binarith,t14_binarith,t12_binari_4,t148_xreal_1,t2_xreal_1,t11_binari_4]), [file(binari_4,t13_binari_4),interesting(0.47)]). fof(l33_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( k6_int_1(B,k3_series_1(2,A)) = k6_int_1(C,k3_series_1(2,A)) => k6_int_1(k2_xcmplx_0(k3_series_1(2,k1_binari_4(A,k1_prepower(B))),B),k3_series_1(2,A)) = k6_int_1(k2_xcmplx_0(k3_series_1(2,k1_binari_4(A,k1_prepower(C))),C),k3_series_1(2,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_4,t28_nat_1,t32_power,t101_newton,t10_euler_2,t77_nat_1,t78_nat_1,d1_binari_4,t28_nat_1,t32_power,t101_newton,t10_euler_2,t77_nat_1,t78_nat_1,t14_int_3,t14_int_3]), [file(binari_4,l33_binari_4),interesting(0.43)]). fof(t12_binari_4,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)) => ( k4_finseq_4(k5_numbers,k6_margrel1,B,A) = k8_margrel1 => r1_xreal_0(k3_series_1(2,k5_binarith(A,1)),k9_binarith(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t24_finseq_4,t57_finseq_1,t42_binarith,d3_binarith,t29_power,t137_finseq_2,t29_nat_1,t11_xreal_1,d3_binarith,t109_finseq_2,t24_finseq_4,t136_finseq_2,t46_binarith,d1_cqc_lang,t38_margrel1,t29_nat_1,s1_binarith]), [file(binari_4,t12_binari_4),interesting(0.43)]). fof(t10_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(k1_nat_1(B,C),k5_real_1(k3_series_1(2,A),1)) => k11_binarith(A,k1_binari_3(A,B),k1_binari_3(A,C)) = k7_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_binari_4,d1_cqc_lang,t47_binarith,t36_binari_3,t36_binari_3,t148_xreal_1,t29_nat_1,t2_xreal_1]), [file(binari_4,t10_binari_4),interesting(0.41)]). fof(t27_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( v1_int_1(B) => ( ( r1_xreal_0(B,k5_real_1(k3_series_1(2,k5_binarith(A,1)),1)) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(A,1))),B) ) => k4_binari_2(A,k2_binari_4(A,B)) = B ) ) ) ), inference(mizar_proof,[status(thm)],[t39_nat_1,t16_int_1,d2_binari_4,d1_absvalue,t8_xreal_1,t38_nat_1,t39_nat_1,t11_xreal_1,d3_binarith,t148_xreal_1,t44_power,t2_xreal_1,t36_binari_3,t39_nat_1,t3_finseq_1,d1_binari_3,t5_jordan4,t78_nat_1,d1_cqc_lang,d3_binari_2,d1_absvalue,t26_xreal_1,t11_nat_2,t44_power,t26_xreal_1,t2_xreal_1,t11_xreal_1,t26_xreal_1,t16_int_1,t2_xreal_1,t24_binari_4,d2_binari_4,d1_absvalue,t8_xreal_1,t12_nat_2,t30_power,t8_xreal_1,t10_xreal_1,t12_nat_2,t30_power,t3_finseq_1,d1_binari_3,t22_nat_2,t64_nat_1,d1_cqc_lang,d3_binari_2,t38_margrel1,t36_binari_3]), [file(binari_4,t27_binari_4),interesting(0.37)]). fof(t18_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ( r1_xreal_0(0,k5_real_1(k3_series_1(2,k5_binarith(A,1)),1)) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(A,1))),0) ) ) ), inference(mizar_proof,[status(thm)],[d3_binarith,t29_power,t39_binarith,t11_nat_2,t44_power,t11_xreal_1,s1_binarith]), [file(binari_4,t18_binari_4),interesting(0.35)]). fof(t35_binari_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( ( ~ v1_xboole_0(C) & m2_subset_1(C,k1_numbers,k5_numbers) ) => ( ( r1_xreal_0(k1_real_1(k3_series_1(2,C)),k2_xcmplx_0(A,B)) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),A) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),B) ) => ( r1_xreal_0(0,A) | r1_xreal_0(0,B) | k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(k1_nat_1(C,1),k2_binari_4(k1_nat_1(C,1),A),k2_binari_4(k1_nat_1(C,1),B)),k1_nat_1(C,1)) = k8_margrel1 ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binari_4,t30_power,t20_int_1,t21_int_1,t1_xreal_1,d1_absvalue,t29_power,t44_power,t24_binari_4,t46_power,t30_pepin,t46_power,t46_power,t30_power,t30_power,d1_absvalue,d3_binarith,t29_power,t6_nat_2,t74_nat_1,t77_nat_1,t101_newton,t5_pepin,t3_finseq_1,d2_binari_4,d1_binari_3,d1_cqc_lang,d5_binarith,t45_margrel1,t50_margrel1,t50_margrel1,t17_binari_4,t17_binari_4,d3_binarith,d3_binarith,t148_xreal_1,t44_power,t30_power,t32_power,t1_xcmplx_1,d1_absvalue,t26_xreal_1,t2_xreal_1,t24_binari_4,t8_xreal_1,t16_int_1,t109_finseq_2,t29_nat_1,t10_xreal_1,d2_binari_4,d1_absvalue,t24_finseq_4,t30_binari_3,d2_binari_4,d1_absvalue,t24_finseq_4,t30_binari_3,t32_binari_4,t38_nat_1,d5_binarith,t45_margrel1,t50_margrel1,t50_margrel1,t17_binari_4,t17_binari_4,s1_binarith]), [file(binari_4,t35_binari_4),interesting(0.29)]). fof(t37_binari_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( ( ~ v1_xboole_0(C) & m2_subset_1(C,k1_numbers,k5_numbers) ) => ( ( r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(k1_nat_1(C,1),1))),k2_xcmplx_0(A,B)) & r1_xreal_0(k2_xcmplx_0(A,B),k5_real_1(k3_series_1(2,k5_binarith(k1_nat_1(C,1),1)),1)) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),A) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),B) ) => ( r1_xreal_0(0,A) | r1_xreal_0(0,B) | k4_binari_2(k1_nat_1(C,1),k10_binarith(k1_nat_1(C,1),k2_binari_4(k1_nat_1(C,1),A),k2_binari_4(k1_nat_1(C,1),B))) = k2_xcmplx_0(A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_binarith,t9_binari_4,t26_xreal_1,d1_absvalue,t31_xreal_1,t44_power,t2_xreal_1,t24_binari_4,t10_xreal_1,t32_power,t30_power,t8_xreal_1,t16_int_1,t33_binari_4,t33_binari_4,t109_finseq_2,t29_nat_1,t24_finseq_4,d2_binari_4,d1_absvalue,t30_binari_3,t24_finseq_4,d2_binari_4,d1_absvalue,t30_binari_3,d2_binari_4,d1_absvalue,d2_binari_4,d1_absvalue,d3_binari_2,t38_margrel1,t36_binari_3,d3_binari_2,t38_margrel1,t36_binari_3,t35_binari_4,d4_binari_2,t41_margrel1,t45_margrel1,t45_margrel1,d5_binari_2,t45_margrel1,t46_margrel1,t14_binari_2]), [file(binari_4,t37_binari_4),interesting(0.19)]). fof(t36_binari_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( ( ~ v1_xboole_0(C) & m2_subset_1(C,k1_numbers,k5_numbers) ) => ( ( r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),k2_xcmplx_0(A,B)) & r1_xreal_0(k2_xcmplx_0(A,B),k5_real_1(k3_series_1(2,k5_binarith(C,1)),1)) & r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => k4_binari_2(C,k10_binarith(C,k2_binari_4(C,A),k2_binari_4(C,B))) = k2_xcmplx_0(A,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_int_1,d2_binari_4,d1_absvalue,d2_binari_4,d1_absvalue,t14_binari_4]), [file(binari_4,t36_binari_4),interesting(0.18)]). 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(t24_finseq_4,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(B)) ) => k4_finseq_4(k5_numbers,A,B,C) = k1_funct_1(B,C) ) ) ) ), file(finseq_4,t24_finseq_4), [interesting(0.00)]). fof(t57_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 & k1_funct_1(B,1) = A ) ) ) ), file(finseq_1,t57_finseq_1), [interesting(0.00)]). fof(d3_binari_2,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( ( k4_finseq_4(k5_numbers,k6_margrel1,B,A) = k7_margrel1 => k4_binari_2(A,B) = k9_binarith(A,B) ) & ( k4_finseq_4(k5_numbers,k6_margrel1,B,A) != k7_margrel1 => k4_binari_2(A,B) = k10_binop_2(k9_binarith(A,B),k3_series_1(2,A)) ) ) ) ) ), file(binari_2,d3_binari_2), [interesting(0.00)]). 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 ) ) ), file(binarith,t41_binarith), [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(t39_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => k5_binarith(k2_xcmplx_0(A,B),B) = A ) ) ), file(binarith,t39_binarith), [interesting(0.00)]). fof(t11_nat_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v4_ordinal2(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & v4_ordinal2(B) ) => ~ r1_xreal_0(A,k5_binarith(A,B)) ) ) ), file(nat_2,t11_nat_2), [interesting(0.00)]). fof(t44_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(B,A) & ~ r1_xreal_0(C,1) & r1_xreal_0(k3_power(C,B),k3_power(C,A)) ) ) ) ) ), file(power,t44_power), [interesting(0.00)]). fof(t11_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(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t11_xreal_1), [interesting(0.00)]). 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) ) ), file(binarith,s1_binarith), [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(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(d4_euclid,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k4_euclid(A) = k4_finseqop(k1_numbers,A,0) ) ), file(euclid,d4_euclid), [interesting(0.00)]). fof(t70_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B,C] : ( r2_hidden(B,k2_finseq_1(A)) => k1_funct_1(k2_finseq_2(A,C),B) = C ) ) ), file(finseq_2,t70_finseq_2), [interesting(0.00)]). fof(t36_margrel1,theorem, ( k7_margrel1 = 0 & k8_margrel1 = 1 ), file(margrel1,t36_margrel1), [interesting(0.00)]). fof(d9_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)) => k11_binarith(A,B,C) = k3_binarith(k3_binarith(k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,A),k4_finseq_4(k5_numbers,k6_margrel1,C,A)),k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,A),k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,C),A))),k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,C,A),k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,C),A))) ) ) ) ), file(binarith,d9_binarith), [interesting(0.00)]). fof(t49_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k7_margrel1,A) = k7_margrel1 ) ), file(margrel1,t49_margrel1), [interesting(0.00)]). fof(t7_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k7_margrel1) = A ) ), file(binarith,t7_binarith), [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(t19_binari_4,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)) => ( ( B = k5_euclid(A) & C = k5_euclid(A) ) => r1_binarith(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t39_nat_1,t3_finseq_1,t24_finseq_4,d4_euclid,t70_finseq_2,t36_margrel1,d9_binarith,t49_margrel1,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,d10_binarith]), [file(binari_4,t19_binari_4),interesting(0.00)]). fof(d1_binari_4,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( C = k1_binari_4(A,B) <=> ( r1_xreal_0(B,k3_series_1(2,C)) & r1_xreal_0(A,C) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( ( r1_xreal_0(B,k3_series_1(2,D)) & r1_xreal_0(A,D) ) => r1_xreal_0(C,D) ) ) ) ) ) ) ) ), file(binari_4,d1_binari_4), [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(t40_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,1) & ~ r1_xreal_0(B,0) & r1_xreal_0(k3_power(A,B),1) ) ) ) ), file(power,t40_power), [interesting(0.00)]). fof(t10_pre_ff,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,B) => ( r1_xreal_0(C,1) | r1_xreal_0(k3_power(C,A),k3_power(C,B)) ) ) ) ) ) ), file(pre_ff,t10_pre_ff), [interesting(0.00)]). fof(d2_binari_4,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( v1_int_1(B) => ( ( ~ r1_xreal_0(0,B) => k2_binari_4(A,B) = k1_binari_3(A,k1_prepower(k2_xcmplx_0(k3_series_1(2,k1_binari_4(A,k1_prepower(B))),B))) ) & ( r1_xreal_0(0,B) => k2_binari_4(A,B) = k1_binari_3(A,k1_prepower(B)) ) ) ) ) ), file(binari_4,d2_binari_4), [interesting(0.00)]). fof(t7_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ( A = 0 <=> k18_complex1(A) = 0 ) ) ), file(absvalue,t7_absvalue), [interesting(0.00)]). fof(t26_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_binari_3(A,0) = k5_euclid(A) ) ), file(binari_3,t26_binari_3), [interesting(0.00)]). fof(t16_int_1,theorem,( ! [A] : ( v1_int_1(A) => ( r1_xreal_0(0,A) => r2_hidden(A,k5_numbers) ) ) ), file(int_1,t16_int_1), [interesting(0.00)]). fof(d1_absvalue,definition,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) => k16_complex1(A) = A ) & ( ~ r1_xreal_0(0,A) => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ), file(absvalue,d1_absvalue), [interesting(0.00)]). fof(t8_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(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t8_xreal_1), [interesting(0.00)]). fof(t38_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A) <=> r1_xreal_0(A,B) ) ) ) ), file(nat_1,t38_nat_1), [interesting(0.00)]). fof(t148_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ r1_xreal_0(A,k6_xcmplx_0(A,1)) ) ), file(xreal_1,t148_xreal_1), [interesting(0.00)]). fof(t36_binari_3,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(k3_series_1(2,A),B) => k9_binarith(A,k1_binari_3(A,B)) = B ) ) ) ), file(binari_3,t36_binari_3), [interesting(0.00)]). fof(d1_binari_3,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( C = k1_binari_3(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k4_finseq_4(k5_numbers,k6_margrel1,C,D) = k2_cqc_lang(k6_margrel1,k4_nat_1(k3_nat_1(B,k3_series_1(2,k5_binarith(D,1))),2),0,k7_margrel1,k8_margrel1) ) ) ) ) ) ) ), file(binari_3,d1_binari_3), [interesting(0.00)]). fof(t5_jordan4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(B,A) => k3_nat_1(A,B) = 0 ) ) ) ), file(jordan4,t5_jordan4), [interesting(0.00)]). fof(t78_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => 0 = k4_nat_1(0,A) ) ), file(nat_1,t78_nat_1), [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(t26_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ), file(xreal_1,t26_xreal_1), [interesting(0.00)]). fof(t12_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(B,A) => k3_power(2,A) = k3_xcmplx_0(k3_power(2,B),k3_series_1(2,k5_binarith(A,B))) ) ) ) ), file(nat_2,t12_nat_2), [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(t10_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ), file(xreal_1,t10_xreal_1), [interesting(0.00)]). fof(t22_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) => ( r1_xreal_0(k2_xcmplx_0(A,A),B) | k3_nat_1(B,A) = 1 ) ) ) ) ), file(nat_2,t22_nat_2), [interesting(0.00)]). fof(t64_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,1) => k4_nat_1(1,A) = 1 ) ) ) ), file(nat_1,t64_nat_1), [interesting(0.00)]). fof(t38_margrel1,theorem,( k7_margrel1 != k8_margrel1 ), file(margrel1,t38_margrel1), [interesting(0.00)]). fof(t39_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k3_power(A,B),0) ) ) ) ), file(power,t39_power), [interesting(0.00)]). fof(t9_int_3,theorem,( ! [A] : ( v4_ordinal2(A) => ( ~ r1_xreal_0(A,0) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(0,k6_int_1(B,A)) & ~ r1_xreal_0(A,k6_int_1(B,A)) ) ) ) ) ), file(int_3,t9_int_3), [interesting(0.00)]). fof(t101_newton,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( k5_int_1(A,B) = k3_nat_1(A,B) & k6_int_1(A,B) = k4_nat_1(A,B) ) ) ) ), file(newton,t101_newton), [interesting(0.00)]). fof(t46_power,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( A != 0 => k3_power(A,B) = k2_newton(A,B) ) ) ) ), file(power,t46_power), [interesting(0.00)]). fof(t12_prepower,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v4_ordinal2(B) => ~ ( 0 != A & 0 = k2_newton(A,B) ) ) ) ), file(prepower,t12_prepower), [interesting(0.00)]). fof(t47_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,0) => B = k2_xcmplx_0(k3_xcmplx_0(A,k3_nat_1(B,A)),k4_nat_1(B,A)) ) ) ) ), file(nat_1,t47_nat_1), [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(t15_int_3,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => k6_int_1(k3_xcmplx_0(B,C),A) = k6_int_1(k3_xcmplx_0(k6_int_1(B,A),k6_int_1(C,A)),A) ) ) ) ), file(int_3,t15_int_3), [interesting(0.00)]). fof(t77_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => k4_nat_1(A,A) = 0 ) ), file(nat_1,t77_nat_1), [interesting(0.00)]). fof(t69_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( k4_nat_1(A,B) = 0 => k3_nat_1(k2_xcmplx_0(A,C),B) = k1_nat_1(k3_nat_1(A,B),k3_nat_1(C,B)) ) ) ) ) ), file(nat_1,t69_nat_1), [interesting(0.00)]). fof(l30_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( k4_nat_1(B,A) = k4_nat_1(C,A) & ~ r1_xreal_0(B,C) & ! [D] : ( v1_int_1(D) => B != k2_xcmplx_0(C,k3_xcmplx_0(D,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_nat_1,t47_nat_1,t28_nat_1,t101_newton,t20_binari_4,t69_nat_1,t47_nat_1,t47_nat_1]), [file(binari_4,l30_binari_4),interesting(0.00)]). fof(t1_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,A) ) => A = B ) ) ) ), file(xreal_1,t1_xreal_1), [interesting(0.00)]). fof(l31_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( k4_nat_1(B,A) = k4_nat_1(C,A) & ! [D] : ( v1_int_1(D) => B != k2_xcmplx_0(C,k3_xcmplx_0(D,A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l30_binari_4,l30_binari_4,t1_xreal_1]), [file(binari_4,l31_binari_4),interesting(0.00)]). fof(t13_nat_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(B,A) => r1_nat_1(k3_series_1(2,B),k3_series_1(2,A)) ) ) ) ), file(nat_2,t13_nat_2), [interesting(0.00)]). fof(t6_pepin,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B != 0 => ( r1_nat_1(B,A) <=> k4_nat_1(A,B) = 0 ) ) ) ) ), file(pepin,t6_pepin), [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(t8_int_3,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( A != 0 => k5_int_1(k2_xcmplx_0(B,k3_xcmplx_0(A,C)),A) = k2_xcmplx_0(k5_int_1(B,A),C) ) & k6_int_1(k2_xcmplx_0(B,k3_xcmplx_0(A,C)),A) = k6_int_1(B,A) ) ) ) ) ), file(int_3,t8_int_3), [interesting(0.00)]). fof(t14_int_3,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => k6_int_1(k2_xcmplx_0(B,C),A) = k6_int_1(k2_xcmplx_0(k6_int_1(B,A),k6_int_1(C,A)),A) ) ) ) ), file(int_3,t14_int_3), [interesting(0.00)]). fof(t13_int_3,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v1_int_1(B) => k6_int_1(k6_int_1(B,A),A) = k6_int_1(B,A) ) ) ), file(int_3,t13_int_3), [interesting(0.00)]). fof(l32_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( k4_nat_1(B,k3_series_1(2,A)) = k4_nat_1(C,k3_series_1(2,A)) => ( r1_xreal_0(A,D) | k4_nat_1(k3_nat_1(B,k3_series_1(2,D)),2) = k4_nat_1(k3_nat_1(C,k3_series_1(2,D)),2) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t46_power,t12_prepower,l31_binari_4,t28_nat_1,t39_power,t101_newton,t10_xreal_1,t10_xreal_1,t38_nat_1,t13_nat_2,t30_power,t6_pepin,t15_int_3,t101_newton,t101_newton,t78_nat_1,t101_newton,t32_power,t8_int_3,t101_newton,t101_newton,t101_newton,t14_int_3,t13_int_3,t101_newton]), [file(binari_4,l32_binari_4),interesting(0.00)]). fof(t139_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)) => ! [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) => ( ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => ( r2_hidden(E,k2_finseq_1(A)) => k1_funct_1(C,E) = k1_funct_1(D,E) ) ) => C = D ) ) ) ) ) ), file(finseq_2,t139_finseq_2), [interesting(0.00)]). fof(t10_euler_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k4_nat_1(k2_nat_1(A,B),C) = k4_nat_1(k2_nat_1(k4_nat_1(A,C),B),C) ) ) ) ), file(euler_2,t10_euler_2), [interesting(0.00)]). fof(t12_int_3,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( v1_int_1(C) => ( ( k6_int_1(B,A) = k6_int_1(C,A) => ( A = 0 | r1_int_1(B,C,A) ) ) & ( r1_int_1(B,C,A) => k6_int_1(B,A) = k6_int_1(C,A) ) ) ) ) ) ), file(int_3,t12_int_3), [interesting(0.00)]). fof(t20_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(A,B) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ), file(nat_1,t20_nat_1), [interesting(0.00)]). fof(t20_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( ~ r1_xreal_0(B,A) => r1_xreal_0(k2_xcmplx_0(A,1),B) ) ) ) ), file(int_1,t20_int_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(t30_binari_4,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( k4_nat_1(B,k3_series_1(2,A)) = k4_nat_1(C,k3_series_1(2,A)) => k1_binari_3(A,B) = k1_binari_3(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t101_newton,t101_newton,d1_absvalue,d2_binari_4,l34_binari_4]), [file(binari_4,t30_binari_4),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(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(t63_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => k4_nat_1(k3_xcmplx_0(A,B),A) = 0 ) ) ), file(nat_1,t63_nat_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(d7_finseq_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ( C = k7_finseq_1(A,B) <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B))) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(A)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k4_finseq_1(B)) => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ), file(finseq_1,d7_finseq_1), [interesting(0.00)]). fof(t113_finseq_2,theorem,( ! [A,B] : ( m1_subset_1(B,k4_finseq_2(0,A)) => B = k6_finseq_1(A) ) ), file(finseq_2,t113_finseq_2), [interesting(0.00)]). fof(t14_finseq_1,theorem, ( v1_relat_1(k1_xboole_0) & v1_funct_1(k1_xboole_0) & v1_finseq_1(k1_xboole_0) ), file(finseq_1,t14_finseq_1), [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(t47_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ( k7_finseq_1(A,k1_xboole_0) = A & k7_finseq_1(k1_xboole_0,A) = A ) ) ), file(finseq_1,t47_finseq_1), [interesting(0.00)]). fof(t8_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r1_xreal_0(k1_nat_1(A,B),k5_real_1(C,1)) => ( ~ r1_xreal_0(C,A) & ~ r1_xreal_0(C,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_nat_1,t11_xreal_1,t11_xreal_1,t148_xreal_1,t2_xreal_1,t2_xreal_1,t29_nat_1,t11_xreal_1,t11_xreal_1,t148_xreal_1,t2_xreal_1,t2_xreal_1]), [file(binari_4,t8_binari_4),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(t14_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k7_margrel1,A) = A ) ), file(binarith,t14_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(t92_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( ( r1_xreal_0(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k6_xcmplx_0(A,D),k6_xcmplx_0(B,C)) ) & ~ ( ( ( ~ r1_xreal_0(B,A) & r1_xreal_0(C,D) ) | ( r1_xreal_0(A,B) & ~ r1_xreal_0(D,C) ) ) & r1_xreal_0(k6_xcmplx_0(B,C),k6_xcmplx_0(A,D)) ) ) ) ) ) ) ), file(real_1,t92_real_1), [interesting(0.00)]). 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 ) ) ), file(binarith,t42_binarith), [interesting(0.00)]). fof(t136_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)) => ! [D] : ( m1_subset_1(D,B) => k1_funct_1(k8_finseq_1(B,C,k12_finseq_1(B,D)),k1_nat_1(A,1)) = D ) ) ) ) ), file(finseq_2,t136_finseq_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))) ) ) ) ), file(binarith,t46_binarith), [interesting(0.00)]). 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)) ) ) ) ), file(binarith,t47_binarith), [interesting(0.00)]). 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)) ) ) ) ) ), file(binarith,t48_binarith), [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(t30_binari_3,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r1_xreal_0(k3_series_1(2,A),B) => ( r1_xreal_0(k3_series_1(2,k1_nat_1(A,1)),B) | k1_funct_1(k1_binari_3(k1_nat_1(A,1),B),k1_nat_1(A,1)) = k8_margrel1 ) ) ) ) ), file(binari_3,t30_binari_3), [interesting(0.00)]). fof(t21_int_1,theorem,( ! [A] : ( v1_int_1(A) => ( ~ r1_xreal_0(0,A) => r1_xreal_0(A,k1_real_1(1)) ) ) ), file(int_1,t21_int_1), [interesting(0.00)]). fof(t30_pepin,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k3_euler_2(2,k1_nat_1(A,1)) = k1_nat_1(k3_euler_2(2,A),k3_euler_2(2,A)) ) ), file(pepin,t30_pepin), [interesting(0.00)]). fof(t6_nat_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k3_nat_1(A,1) = A ) ), file(nat_2,t6_nat_2), [interesting(0.00)]). fof(t74_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => k4_nat_1(k2_xcmplx_0(A,B),C) = k4_nat_1(k2_xcmplx_0(k4_nat_1(A,C),B),C) ) ) ) ), file(nat_1,t74_nat_1), [interesting(0.00)]). fof(t5_pepin,theorem,( ! [A] : ( v1_int_1(A) => ( ~ r1_xreal_0(A,1) => k6_int_1(1,A) = 1 ) ) ), file(pepin,t5_pepin), [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(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(t50_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k8_margrel1,A) = A ) ), file(margrel1,t50_margrel1), [interesting(0.00)]). fof(d1_binarith,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,B) = k9_margrel1(k10_margrel1(k9_margrel1(A),k9_margrel1(B))) ) ) ), file(binarith,d1_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(t1_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k2_xcmplx_0(A,k2_xcmplx_0(B,C)) = k2_xcmplx_0(k2_xcmplx_0(A,B),C) ) ) ) ), file(xcmplx_1,t1_xcmplx_1), [interesting(0.00)]). fof(d4_binari_2,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)) => k5_binari_2(A,B,C) = k12_margrel1(k12_margrel1(k11_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,A)),k11_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,C,A))),k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,C),A)) ) ) ) ), file(binari_2,d4_binari_2), [interesting(0.00)]). fof(d5_binari_2,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)) => k6_binari_2(A,B,C) = k12_margrel1(k12_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,A),k4_finseq_4(k5_numbers,k6_margrel1,C,A)),k11_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,C),A))) ) ) ) ), file(binari_2,d5_binari_2), [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(t14_binari_2,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) => k4_binari_2(k23_binop_2(A,1),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)))) = k2_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(k4_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,D))),k4_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,C,k13_binarith(k6_margrel1,E)))),k2_cqc_lang(k5_numbers,k5_binari_2(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))),k7_margrel1,0,k3_series_1(2,k23_binop_2(A,1)))),k2_cqc_lang(k5_numbers,k6_binari_2(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))),k7_margrel1,0,k3_series_1(2,k23_binop_2(A,1)))) ) ) ) ) ) ), file(binari_2,t14_binari_2), [interesting(0.00)]). fof(t73_finseq_2,theorem,( ! [A] : k2_finseq_2(1,A) = k9_finseq_1(A) ), file(finseq_2,t73_finseq_2), [interesting(0.00)]). fof(t72_finseq_2,theorem,( ! [A] : k2_finseq_2(0,A) = k1_xboole_0 ), file(finseq_2,t72_finseq_2), [interesting(0.00)]). fof(t29_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_binari_3(k1_nat_1(A,1),k3_series_1(2,A)) = k8_finseq_1(k1_numbers,k5_euclid(A),k13_binarith(k1_numbers,1)) ) ), file(binari_3,t29_binari_3), [interesting(0.00)]). fof(t18_binari_3,theorem, ( k10_binarith(1,k13_binarith(k6_margrel1,k7_margrel1),k13_binarith(k6_margrel1,k8_margrel1)) = k13_binarith(k6_margrel1,k8_margrel1) & k10_binarith(1,k13_binarith(k6_margrel1,k8_margrel1),k13_binarith(k6_margrel1,k7_margrel1)) = k13_binarith(k6_margrel1,k8_margrel1) ), file(binari_3,t18_binari_3), [interesting(0.00)]). fof(t27_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(k3_series_1(2,A),B) => k1_funct_1(k1_binari_3(k1_nat_1(A,1),B),k1_nat_1(A,1)) = k7_margrel1 ) ) ) ), file(binari_3,t27_binari_3), [interesting(0.00)]). fof(t38_binari_4,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ! [C] : ( ( ~ v1_xboole_0(C) & m2_subset_1(C,k1_numbers,k5_numbers) ) => ( ( r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),A) & r1_xreal_0(A,k5_real_1(k3_series_1(2,k5_binarith(C,1)),1)) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),B) & r1_xreal_0(B,k5_real_1(k3_series_1(2,k5_binarith(C,1)),1)) & r1_xreal_0(k1_real_1(k3_series_1(2,k5_binarith(C,1))),k2_xcmplx_0(A,B)) & r1_xreal_0(k2_xcmplx_0(A,B),k5_real_1(k3_series_1(2,k5_binarith(C,1)),1)) ) => ( ( ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) & ~ ( ~ r1_xreal_0(0,A) & r1_xreal_0(0,B) ) ) | k4_binari_2(C,k10_binarith(C,k2_binari_4(C,A),k2_binari_4(C,B))) = k2_xcmplx_0(A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_binarith,t29_power,d2_binari_4,d1_absvalue,t26_binari_3,d4_euclid,t73_finseq_2,t36_margrel1,t30_power,d1_absvalue,d1_binari_4,d4_euclid,t72_finseq_2,d2_binari_4,t30_power,d1_absvalue,t29_power,t29_binari_3,t47_finseq_1,t36_margrel1,t21_int_1,t1_xreal_1,t15_binari_4,t18_binari_3,t21_int_1,t1_xreal_1,t15_binari_4,t18_binari_3,d3_binarith,t33_binari_4,t33_binari_4,t16_int_1,d2_binari_4,d1_absvalue,t109_finseq_2,t29_nat_1,t148_xreal_1,t2_xreal_1,t27_binari_3,d1_absvalue,t26_xreal_1,t31_xreal_1,t44_power,t2_xreal_1,t24_binari_4,t10_xreal_1,t32_power,t30_power,t8_xreal_1,t39_power,t16_int_1,d2_binari_4,d1_absvalue,t30_binari_3,t10_xreal_1,t44_power,t2_xreal_1,t24_finseq_4,d3_binari_2,t36_binari_3,d2_binari_4,d1_absvalue,t24_finseq_4,d3_binari_2,t38_margrel1,t36_binari_3,d4_binari_2,t41_margrel1,t46_margrel1,t45_margrel1,d5_binari_2,t45_margrel1,t45_margrel1,t14_binari_2,t16_int_1,d2_binari_4,d1_absvalue,t109_finseq_2,t29_nat_1,t148_xreal_1,t2_xreal_1,t27_binari_3,d1_absvalue,t26_xreal_1,t31_xreal_1,t44_power,t2_xreal_1,t24_binari_4,t10_xreal_1,t32_power,t30_power,t8_xreal_1,t39_power,t16_int_1,d2_binari_4,d1_absvalue,t30_binari_3,t10_xreal_1,t44_power,t2_xreal_1,t24_finseq_4,d3_binari_2,t36_binari_3,d2_binari_4,d1_absvalue,t24_finseq_4,d3_binari_2,t38_margrel1,t36_binari_3,d4_binari_2,t41_margrel1,t46_margrel1,t45_margrel1,d5_binari_2,t45_margrel1,t45_margrel1,t14_binari_2,s1_binarith]), [file(binari_4,t38_binari_4),interesting(0.00)]). fof(d1_funct_2,definition,( ! [A,B,C] : ( m2_relset_1(C,A,B) => ( ( ( B = k1_xboole_0 => A = k1_xboole_0 ) => ( v1_funct_2(C,A,B) <=> A = k4_relset_1(A,B,C) ) ) & ( B = k1_xboole_0 => ( A = k1_xboole_0 | ( v1_funct_2(C,A,B) <=> C = k1_xboole_0 ) ) ) ) ) ), file(funct_2,d1_funct_2), [interesting(0.00)]). fof(d4_finseq_1,definition,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( m1_finseq_1(B,A) <=> r1_tarski(k2_relat_1(B),A) ) ) ), file(finseq_1,d4_finseq_1), [interesting(0.00)]). fof(t119_zfmisc_1,theorem,( ! [A,B,C,D] : ( ( r1_tarski(A,B) & r1_tarski(C,D) ) => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ), file(zfmisc_1,t119_zfmisc_1), [interesting(0.00)]). fof(d4_rvsum_1,definition,( ! [A] : ( m2_finseq_1(A,k1_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => k3_rvsum_1(A,B) = k1_finseqop(k1_numbers,k1_numbers,k1_numbers,k33_binop_2,A,B) ) ) ), file(rvsum_1,d4_rvsum_1), [interesting(0.00)]). fof(t84_funcop_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r1_tarski(k2_zfmisc_1(k2_relat_1(B),k2_relat_1(C)),k1_relat_1(A)) => k1_relat_1(k3_funcop_1(A,B,C)) = k3_xboole_0(k1_relat_1(B),k1_relat_1(C)) ) ) ) ) ), file(funcop_1,t84_funcop_1), [interesting(0.00)]). fof(t68_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : k4_finseq_1(k2_finseq_2(A,B)) = k2_finseq_1(A) ) ), file(finseq_2,t68_finseq_2), [interesting(0.00)]). fof(t26_rvsum_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_1(B,k1_numbers) => ! [C] : ( m2_finseq_1(C,k1_numbers) => ( r2_hidden(A,k4_finseq_1(k3_rvsum_1(B,C))) => k2_seq_1(k5_numbers,k1_numbers,k3_rvsum_1(B,C),A) = k9_binop_2(k2_seq_1(k5_numbers,k1_numbers,B,A),k2_seq_1(k5_numbers,k1_numbers,C,A)) ) ) ) ) ), file(rvsum_1,t26_rvsum_1), [interesting(0.00)]). fof(t17_finseq_1,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( ( k4_finseq_1(A) = k4_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t17_finseq_1), [interesting(0.00)]). fof(t18_int_1,theorem,( ! [A] : ( v1_int_1(A) => ! [B] : ( v1_int_1(B) => ( r1_xreal_0(A,B) => r2_hidden(k6_xcmplx_0(B,A),k5_numbers) ) ) ) ), file(int_1,t18_int_1), [interesting(0.00)]). fof(t69_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : k3_finseq_1(k2_finseq_2(A,B)) = A ) ), file(finseq_2,t69_finseq_2), [interesting(0.00)]). fof(t4_binari_4,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( r1_xreal_0(C,A) & r1_xreal_0(A,B) & C != A & ~ ( r1_xreal_0(k1_nat_1(C,1),A) & r1_xreal_0(A,B) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_nat_1,t1_xreal_1,t38_nat_1,s1_nat_1]), [file(binari_4,t4_binari_4),interesting(0.00)]). fof(t5_binari_4,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)) => ( ( B = k5_euclid(A) & C = k5_euclid(A) ) => k7_binarith(A,B,C) = k5_euclid(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t39_nat_1,t24_finseq_4,d5_binarith,t36_margrel1,t18_int_1,t38_nat_1,t3_finseq_1,t109_finseq_2,d4_euclid,t69_finseq_2,t24_finseq_4,d4_euclid,t70_finseq_2,t36_margrel1,t109_finseq_2,t24_finseq_4,d5_binarith,t49_margrel1,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,t36_margrel1,t3_finseq_1,d4_euclid,t70_finseq_2,t38_nat_1,t4_binari_4,t139_finseq_2]), [file(binari_4,t5_binari_4),interesting(0.00)]). fof(t6_binari_4,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)) => ( ( B = k5_euclid(A) & C = k5_euclid(A) ) => k10_binarith(A,B,C) = k5_euclid(A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_euclid,t70_finseq_2,t36_margrel1,t109_finseq_2,t3_finseq_1,t24_finseq_4,t24_finseq_4,t5_binari_4,t24_finseq_4,d8_binarith,t14_binarith,t14_binarith,t139_finseq_2]), [file(binari_4,t6_binari_4),interesting(0.00)]). fof(t2_jordan2b,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( r2_hidden(B,k2_finseq_1(A)) => k1_funct_1(k5_euclid(A),B) = 0 ) ) ) ), file(jordan2b,t2_jordan2b), [interesting(0.00)]). fof(d13_margrel1,definition,( k7_margrel1 = 0 ), file(margrel1,d13_margrel1), [interesting(0.00)]). fof(t7_binari_3,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)) => ( B = k5_euclid(A) => k9_binarith(A,B) = 0 ) ) ) ), file(binari_3,t7_binari_3), [interesting(0.00)]).