fof(t37_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)) => k1_binari_3(A,k9_binarith(A,B)) = B ) ) ), inference(mizar_proof,[status(thm)],[t1_binari_3,t36_binari_3,t2_binari_3]), [file(binari_3,t37_binari_3),interesting(1.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 ) ) ) ), inference(mizar_proof,[status(thm)],[t26_binari_3,t7_binari_3,t38_nat_1,t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t11_xreal_1,t32_binari_3,t24_binari_3,t39_margrel1,d10_binarith,t34_binari_3,t48_binarith,t12_binari_3,t38_nat_1,s1_nat_1]), [file(binari_3,t36_binari_3),interesting(0.97)]). fof(t26_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k1_binari_3(A,0) = k5_euclid(A) ) ), inference(mizar_proof,[status(thm)],[t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t109_finseq_2,d3_finseq_1,d4_finseq_4,d1_binari_3,t4_nat_2,t78_nat_1,d1_cqc_lang,t36_margrel1,t70_finseq_2,d4_euclid,t139_finseq_2]), [file(binari_3,t26_binari_3),interesting(0.71)]). fof(t11_binari_3,theorem,( k2_binari_2(1) = k13_binarith(k6_margrel1,k8_margrel1) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t5_finseq_1,t7_binari_2,t25_finseq_4]), [file(binari_3,t11_binari_3),interesting(0.71)]). fof(t34_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),k1_nat_1(B,1)) => k1_binari_3(A,k1_nat_1(B,1)) = k10_binarith(A,k1_binari_3(A,B),k2_binari_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_power,t8_xreal_1,t39_nat_1,t30_power,t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,d4_euclid,t73_finseq_2,t36_margrel1,t32_binari_3,t11_binari_3,t15_binari_3,t18_binari_3,t26_binari_3,t38_nat_1,t38_nat_1,t33_binari_3,t28_binari_3,t14_binarith,t14_binarith,t45_binarith,t9_binari_2,t28_binari_3,t38_nat_1,t32_power,t30_power,t21_xreal_1,t50_binarith,t33_binari_3,t31_binari_3,t3_jordan4,t14_binarith,t14_binarith,t45_binarith,t9_binari_2,t31_binari_3,t38_nat_1,t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t32_binari_3,t24_binari_3,t29_binari_3,d14_margrel1,t25_binari_3,t32_binari_3,t14_binarith,t14_binarith,t45_binarith,t9_binari_2,t28_binari_3,d5_real_1,s1_binarith]), [file(binari_3,t34_binari_3),interesting(0.69)]). fof(t15_binari_3,theorem,( k6_binarith(1,k13_binarith(k6_margrel1,k7_margrel1)) = k13_binarith(k6_margrel1,k8_margrel1) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,d1_tarski,t109_finseq_2,t24_finseq_4,t109_finseq_2,t24_finseq_4,d4_binarith,t57_finseq_1,t41_margrel1,t57_finseq_1,t139_finseq_2]), [file(binari_3,t15_binari_3),interesting(0.67)]). fof(t12_binari_3,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => k9_binarith(A,k2_binari_2(A)) = 1 ) ), inference(mizar_proof,[status(thm)],[t11_binari_3,t42_binarith,t9_binari_2,t46_binarith,d1_cqc_lang,s1_binarith]), [file(binari_3,t12_binari_3),interesting(0.67)]). fof(t5_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => r2_hidden(k5_euclid(A),k13_finseq_1(k6_margrel1)) ) ), inference(mizar_proof,[status(thm)],[t77_finseq_2,d13_margrel1,d4_euclid,d11_finseq_1]), [file(binari_3,t5_binari_3),interesting(0.65)]). fof(t9_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k4_finseq_5(k1_numbers,k5_euclid(A)) = k5_euclid(A) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d3_finseq_5,d3_finseq_1,d3_finseq_1,t2_euclid,t2_finseq_5,t2_euclid,t61_finseq_5,d4_euclid,t70_finseq_2,t70_finseq_2,d4_euclid,t17_finseq_1]), [file(binari_3,t9_binari_3),interesting(0.62)]). fof(t17_binari_3,theorem,( k10_binarith(1,k13_binarith(k6_margrel1,k7_margrel1),k13_binarith(k6_margrel1,k7_margrel1)) = k13_binarith(k6_margrel1,k7_margrel1) ), inference(mizar_proof,[status(thm)],[t14_binari_3,t38_margrel1,t39_margrel1,d10_binarith,t48_binarith,t41_binarith,t2_binari_3]), [file(binari_3,t17_binari_3),interesting(0.61)]). fof(t19_binari_3,theorem,( k10_binarith(1,k13_binarith(k6_margrel1,k8_margrel1),k13_binarith(k6_margrel1,k8_margrel1)) = k13_binarith(k6_margrel1,k7_margrel1) ), inference(mizar_proof,[status(thm)],[t14_binari_3,t30_power,d1_cqc_lang,t38_margrel1,t47_binarith,t42_binarith,t42_binarith,t41_binarith,t2_binari_3]), [file(binari_3,t19_binari_3),interesting(0.58)]). fof(t3_binari_3,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) ) => ( k3_finseq_5(A) = k3_finseq_5(B) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[t29_finseq_6,t29_finseq_6]), [file(binari_3,t3_binari_3),interesting(0.58)]). fof(t25_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) => k10_binarith(A,k6_binarith(A,B),k2_binari_2(A)) = B ) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_3,d1_cqc_lang,t38_margrel1,t47_binarith,t15_binari_2,t12_binari_3,t7_binari_3,t7_binari_3,t2_binari_3]), [file(binari_3,t25_binari_3),interesting(0.57)]). fof(t16_binari_3,theorem,( k6_binarith(1,k13_binarith(k6_margrel1,k8_margrel1)) = k13_binarith(k6_margrel1,k7_margrel1) ), inference(mizar_proof,[status(thm)],[t4_finseq_1,d1_tarski,t109_finseq_2,t24_finseq_4,t109_finseq_2,t24_finseq_4,d4_binarith,t57_finseq_1,t41_margrel1,t57_finseq_1,t139_finseq_2]), [file(binari_3,t16_binari_3),interesting(0.54)]). 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)) ) ), inference(mizar_proof,[status(thm)],[t30_power,d4_euclid,t73_finseq_2,d13_margrel1,d4_euclid,t72_finseq_2,l33_binari_3,t15_binari_3,t29_power,t47_finseq_1,d14_margrel1,l30_binari_3,d14_margrel1,t19_nat_1]), [file(binari_3,t29_binari_3),interesting(0.51)]). fof(t4_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k5_euclid(k1_nat_1(A,1)) = k8_finseq_1(k1_numbers,k5_euclid(A),k13_binarith(k1_numbers,0)) ) ), inference(mizar_proof,[status(thm)],[d4_euclid,t74_finseq_2,d4_euclid]), [file(binari_3,t4_binari_3),interesting(0.47)]). 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 ) ) ) ), inference(mizar_proof,[status(thm)],[d4_euclid,t73_finseq_2,t36_margrel1,t41_binarith,t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t4_binari_3,t36_margrel1,t46_binarith,d1_cqc_lang,s1_binarith]), [file(binari_3,t7_binari_3),interesting(0.47)]). fof(t23_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) => k7_binarith(A,k6_binarith(A,B),k2_binari_2(A)) = k6_binarith(A,k2_binari_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_finseq_1,t39_nat_1,d4_euclid,t70_finseq_2,t109_finseq_2,d4_binarith,t24_finseq_4,t36_margrel1,t41_margrel1,t4_finseq_1,d1_tarski,t109_finseq_2,t109_finseq_2,t24_finseq_4,d5_binarith,t41_margrel1,t7_binari_2,d4_binarith,t24_finseq_4,t139_finseq_2,d1_nat_2,t38_nat_1,t3_finseq_1,t7_binari_2,d4_euclid,t70_finseq_2,t36_margrel1,d4_binarith,t24_finseq_4,t41_margrel1,t45_margrel1,t19_binarith,d5_binarith,t19_binarith,t39_nat_1,t38_nat_1,t3_finseq_1,d4_euclid,t70_finseq_2,t36_margrel1,d4_binarith,t24_finseq_4,t41_margrel1,d1_nat_2,t8_binari_2,t45_margrel1,d5_binarith,t7_binarith,t7_binarith,t45_margrel1,t38_nat_1,s2_nat_2,t21_binari_3]), [file(binari_3,t23_binari_3),interesting(0.47)]). fof(t6_binari_3,theorem,( ! [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) => k6_binarith(A,B) = k4_finseqop(k1_numbers,A,1) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t69_finseq_2,t109_finseq_2,t3_finseq_1,d4_euclid,t70_finseq_2,t36_margrel1,t24_finseq_4,d4_binarith,t24_finseq_4,t36_margrel1,t41_margrel1,t70_finseq_2,t18_finseq_1]), [file(binari_3,t6_binari_3),interesting(0.46)]). fof(t33_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),k1_nat_1(B,1)) => k11_binarith(A,k1_binari_3(A,B),k2_binari_2(A)) = k7_margrel1 ) ) ) ), inference(mizar_proof,[status(thm)],[t22_xreal_1,t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t38_nat_1,t32_binari_3,t24_binari_3,t39_margrel1]), [file(binari_3,t33_binari_3),interesting(0.45)]). fof(t1_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)) => ~ r1_xreal_0(k3_series_1(2,A),k9_binarith(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t39_margrel1,t41_binarith,t42_binarith,t30_power,t137_finseq_2,t46_binarith,t38_nat_1,t44_power,d1_cqc_lang,t10_xreal_1,t8_xreal_1,d1_cqc_lang,t38_margrel1,t8_xreal_1,t30_power,t32_power,t39_margrel1,s1_binarith]), [file(binari_3,t1_binari_3),interesting(0.44)]). fof(t10_binari_3,theorem,( ! [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_finseq_5(k6_margrel1,k6_binarith(A,B)) = k6_binarith(A,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d3_finseq_5,d3_finseq_1,d3_finseq_1,t109_finseq_2,t2_finseq_5,t109_finseq_2,t61_finseq_5,t6_binari_3,t70_finseq_2,t70_finseq_2,t6_binari_3,t17_finseq_1]), [file(binari_3,t10_binari_3),interesting(0.39)]). fof(t24_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)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( C = k5_euclid(A) => ( k11_binarith(A,B,k2_binari_2(A)) = k8_margrel1 <=> B = k6_binarith(A,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_finseq_1,t5_finseq_1,d9_binarith,t45_margrel1,t8_binari_2,t38_margrel1,t45_margrel1,t22_binari_3,t13_binari_3,t45_margrel1,t8_binari_2,t38_margrel1,t13_binari_3,t117_finseq_2,t11_binari_3,t14_binari_3,t109_finseq_2,d3_finseq_1,d4_finseq_4,d4_euclid,t70_finseq_2,t4_finseq_1,d1_tarski,t25_finseq_4,t36_margrel1,t41_margrel1,d4_binarith,t109_finseq_2,d3_finseq_1,d4_finseq_4,d4_euclid,t70_finseq_2,d4_binarith,t36_margrel1,t41_margrel1,t23_binari_3,d4_binarith,t8_binari_2,t41_margrel1,t45_margrel1,t19_binarith,d9_binarith,t19_binarith,t117_finseq_2,t109_finseq_2,d3_finseq_1,d4_finseq_4,d4_euclid,t70_finseq_2,t25_finseq_4,d4_binarith,t36_margrel1,t41_margrel1,t11_binari_3,t14_binari_3]), [file(binari_3,t24_binari_3),interesting(0.39)]). 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 ) ) ) ), inference(mizar_proof,[status(thm)],[t2_jordan4,t5_jordan4,t78_nat_1,t6_finseq_1,t109_finseq_2,d3_finseq_1,d4_finseq_4,d1_binari_3,d1_cqc_lang]), [file(binari_3,t27_binari_3),interesting(0.36)]). fof(t21_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)) => ( ( k4_finseq_4(k5_numbers,k6_margrel1,B,A) = k8_margrel1 & k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,k2_binari_2(A)),A) = k8_margrel1 ) => k7_binarith(A,B,k2_binari_2(A)) = k6_binarith(A,k2_binari_2(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_finseq_1,t109_finseq_2,t109_finseq_2,t24_finseq_4,d5_binarith,t41_margrel1,t7_binari_2,d4_binarith,t24_finseq_4,t5_binarith,t24_finseq_4,t20_binari_3,t41_margrel1,t8_binari_2,d4_binarith,t24_finseq_4,t139_finseq_2]), [file(binari_3,t21_binari_3),interesting(0.31)]). fof(l30_binari_3,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => k1_binari_3(k1_nat_1(A,1),k3_series_1(2,A)) = k7_finseq_1(k5_euclid(A),k13_binarith(k6_margrel1,k8_margrel1)) ) ), inference(mizar_proof,[status(thm)],[t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t109_finseq_2,d3_finseq_1,t3_finseq_1,t3_finseq_1,t11_xreal_1,t50_binarith,t3_finseq_1,t38_nat_1,t21_xreal_1,t52_xreal_1,t50_binarith,t50_binarith,t22_nat_1,t32_power,t30_power,t39_power,t50_binarith,t32_power,t72_nat_1,t63_nat_1,t109_finseq_2,d3_finseq_1,d4_finseq_4,d1_binari_3,d1_cqc_lang,t36_margrel1,t70_finseq_2,d4_euclid,d7_finseq_1,t6_finseq_1,t109_finseq_2,d3_finseq_1,t39_power,t2_jordan4,t5_nat_2,t64_nat_1,d4_finseq_4,d1_binari_3,d1_cqc_lang,t136_finseq_2,t8_finseq_2,t139_finseq_2]), [file(binari_3,l30_binari_3),interesting(0.28)]). fof(l31_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 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_power,t30_power,t2_jordan4,t22_nat_2,t76_nat_1,t6_finseq_1,t109_finseq_2,d3_finseq_1,d4_finseq_4,d1_binari_3,d1_cqc_lang]), [file(binari_3,l31_binari_3),interesting(0.25)]). fof(t22_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)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( ( C = k5_euclid(A) & k4_finseq_4(k5_numbers,k6_margrel1,B,A) = k8_margrel1 & k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,k2_binari_2(A)),A) = k8_margrel1 ) => B = k6_binarith(A,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t109_finseq_2,t109_finseq_2,t109_finseq_2,t3_finseq_1,d4_euclid,t70_finseq_2,t36_margrel1,t39_nat_1,d5_binarith,t38_margrel1,t38_nat_1,t3_finseq_1,t109_finseq_2,d5_binarith,t45_margrel1,t21_binari_3,t24_finseq_4,d4_binarith,t8_binari_2,t41_margrel1,t24_finseq_4,d5_binarith,t7_binarith,t7_binarith,t24_finseq_4,t45_margrel1,t41_margrel1,t24_finseq_4,d4_binarith,t24_finseq_4,d5_real_1,t5_binarith,t24_finseq_4,t20_binari_3,t41_margrel1,t24_finseq_4,d4_binarith,t24_finseq_4,t139_finseq_2]), [file(binari_3,t22_binari_3),interesting(0.22)]). fof(t35_binari_3,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k1_binari_3(k1_nat_1(A,1),B) = k7_finseq_1(k13_binarith(k1_numbers,k4_nat_1(B,2)),k1_binari_3(A,k3_nat_1(B,2))) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t8_finseq_5,t109_finseq_2,t3_finseq_1,t56_finseq_1,t11_xreal_1,t50_binarith,t38_nat_1,t22_xreal_1,t50_binarith,t109_finseq_2,t3_finseq_1,t32_power,t30_power,t53_binarith,t29_nat_2,t109_finseq_2,t24_finseq_4,d1_binari_3,d1_binari_3,t24_finseq_4,t50_binarith,t37_finseq_1,t29_power,d1_cqc_lang,t36_margrel1,d1_cqc_lang,t36_margrel1,t62_nat_1,t24_finseq_4,d1_binari_3,t51_binarith,t6_nat_2,t58_finseq_1,d5_real_1,t10_finseq_2]), [file(binari_3,t35_binari_3),interesting(0.20)]). fof(t28_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) => k1_binari_3(k1_nat_1(A,1),B) = k12_binarith(A,1,k6_margrel1,k1_binari_3(A,B),k13_binarith(k6_margrel1,k7_margrel1)) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,d3_finseq_1,t109_finseq_2,d3_finseq_1,d4_finseq_4,d1_binari_3,d1_binari_3,d4_finseq_4,d7_finseq_1,t27_binari_3,t136_finseq_2,t8_finseq_2,t139_finseq_2]), [file(binari_3,t28_binari_3),interesting(0.18)]). fof(l33_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) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( C = k5_euclid(A) => ( k1_binari_3(A,B) = k6_binarith(A,C) <=> B = k5_real_1(k3_series_1(2,A),1) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_euclid,t73_finseq_2,t36_margrel1,t109_finseq_2,t5_finseq_1,t30_power,t57_finseq_1,t15_binari_3,t24_finseq_4,t36_margrel1,d1_binari_3,t71_nat_1,t39_power,t5_jordan4,t78_nat_1,d1_cqc_lang,t36_margrel1,t30_power,t109_finseq_2,t109_finseq_2,t6_finseq_1,t18_nat_1,t8_xreal_1,d4_euclid,t70_finseq_2,t36_margrel1,t24_finseq_4,d4_binarith,t24_finseq_4,t41_margrel1,t27_binari_3,t38_margrel1,l32_binari_3,t32_power,t30_power,t21_xreal_1,t50_binarith,t5_binari_3,d11_finseq_1,t8_jordan2b,t110_finseq_2,t4_binari_3,t11_binari_2,t36_margrel1,t20_finseq_2,t50_binarith,t30_power,t32_power,s1_binarith,t109_finseq_2,d3_finseq_1,t109_finseq_2,t109_finseq_2,t3_finseq_1,d4_euclid,t70_finseq_2,t36_margrel1,t39_power,t38_nat_1,t3_finseq_1,t38_nat_1,t11_xreal_1,t50_binarith,t13_nat_2,t22_xreal_1,t50_binarith,t19_nat_2,t39_power,t38_nat_1,t39_power,t38_nat_1,t50_binarith,t17_nat_2,t18_nat_2,t50_binarith,t20_nat_2,d4_finseq_4,d1_binari_3,d1_cqc_lang,t41_margrel1,t24_finseq_4,d4_binarith,t24_finseq_4,t139_finseq_2]), [file(binari_3,l33_binari_3),interesting(0.16)]). fof(t32_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) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( C = k5_euclid(A) => ( k1_binari_3(A,B) = k6_binarith(A,C) <=> B = k5_real_1(k3_series_1(2,A),1) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l33_binari_3]), [file(binari_3,t32_binari_3),interesting(0.16)]). fof(t20_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)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( ( k4_finseq_4(k5_numbers,k6_margrel1,B,A) = k8_margrel1 & k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,k2_binari_2(A)),A) = k8_margrel1 ) => ! [D] : ( ( ~ v1_xboole_0(D) & m2_subset_1(D,k1_numbers,k5_numbers) ) => ( r1_xreal_0(D,A) => ( D = 1 | ( k4_finseq_4(k5_numbers,k6_margrel1,B,D) = k8_margrel1 & k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,k2_binari_2(A)),D) = k8_margrel1 ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t39_nat_1,t53_binarith,t3_finseq_1,t39_nat_1,t38_nat_1,t50_binarith,t22_xreal_1,t38_nat_1,t11_nat_2,t50_binarith,t21_xreal_1,t21_xreal_1,t50_binarith,t38_nat_1,t3_finseq_1,t8_binari_2,t45_margrel1,d5_binarith,t3_finseq_1,t7_binarith,t7_binarith,t45_margrel1,t9_nat_2,t9_nat_2,s1_binarith,t29_nat_1,t50_binarith,t21_nat_2,t38_nat_1,t21_xreal_1,t92_real_1,t50_binarith,t21_xreal_1,t38_nat_1,t7_nat_2,t3_finseq_1]), [file(binari_3,t20_binari_3),interesting(0.06)]). fof(l32_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_binari_3(k1_nat_1(A,1),B) = k12_binarith(A,1,k6_margrel1,k1_binari_3(A,k5_binarith(B,k3_series_1(2,A))),k13_binarith(k6_margrel1,k8_margrel1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,d3_finseq_1,t109_finseq_2,d3_finseq_1,t39_power,t38_nat_1,t3_finseq_1,t30_power,t32_power,t50_binarith,t13_nat_2,t23_nat_2,t25_nat_2,t23_nat_2,t24_nat_2,t25_nat_2,t24_nat_2,d4_finseq_4,d1_binari_3,d1_binari_3,d4_finseq_4,d7_finseq_1,l31_binari_3,t136_finseq_2,t8_finseq_2,t139_finseq_2]), [file(binari_3,l32_binari_3),interesting(0.05)]). fof(t31_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_binari_3(k1_nat_1(A,1),B) = k12_binarith(A,1,k6_margrel1,k1_binari_3(A,k5_binarith(B,k3_series_1(2,A))),k13_binarith(k6_margrel1,k8_margrel1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l32_binari_3]), [file(binari_3,t31_binari_3),interesting(0.05)]). 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 ) ) ) ) ), inference(mizar_proof,[status(thm)],[l31_binari_3]), [file(binari_3,t30_binari_3),interesting(0.04)]). 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(d3_finseq_5,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) ) => ( B = k3_finseq_5(A) <=> ( k3_finseq_1(B) = k3_finseq_1(A) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k4_finseq_1(B)) => k1_funct_1(B,C) = k1_funct_1(A,k2_xcmplx_0(k6_xcmplx_0(k3_finseq_1(A),C),1)) ) ) ) ) ) ) ), file(finseq_5,d3_finseq_5), [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(t2_finseq_5,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)) => r2_hidden(k2_xcmplx_0(k6_xcmplx_0(B,A),1),k2_finseq_1(B)) ) ) ) ), file(finseq_5,t2_finseq_5), [interesting(0.00)]). fof(t61_finseq_5,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => ( r2_hidden(A,k4_finseq_1(B)) => k1_funct_1(k3_finseq_5(B),A) = k1_funct_1(B,k2_xcmplx_0(k6_xcmplx_0(k3_finseq_1(B),A),1)) ) ) ) ), file(finseq_5,t61_finseq_5), [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(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(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(d4_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,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( C = k6_binarith(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) = k11_margrel1(k4_finseq_4(k5_numbers,k6_margrel1,B,D)) ) ) ) ) ) ) ), file(binarith,d4_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(t18_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) ) => ( ( k3_finseq_1(A) = k3_finseq_1(B) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( ( r1_xreal_0(1,C) & r1_xreal_0(C,k3_finseq_1(A)) ) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) ) => A = B ) ) ) ), file(finseq_1,t18_finseq_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(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(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(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(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(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(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(t19_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k8_margrel1) = k8_margrel1 ) ), file(binarith,t19_binarith), [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(t13_binari_3,theorem,( ! [A] : ( m1_subset_1(A,k6_margrel1) => ! [B] : ( m1_subset_1(B,k6_margrel1) => ( ~ ( k3_binarith(A,B) = k8_margrel1 & A != k8_margrel1 & B != k8_margrel1 ) & ( ( A = k8_margrel1 | B = k8_margrel1 ) => k3_binarith(A,B) = k8_margrel1 ) & ( k3_binarith(A,B) = k7_margrel1 => ( A = k7_margrel1 & B = k7_margrel1 ) ) & ( ( A = k7_margrel1 & B = k7_margrel1 ) => k3_binarith(A,B) = k7_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t41_margrel1,t45_margrel1,t41_margrel1,t19_binarith,t10_binarith,t41_margrel1,t45_margrel1,t41_margrel1,t7_binarith]), [file(binari_3,t13_binari_3),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(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(t38_margrel1,theorem,( k7_margrel1 != k8_margrel1 ), file(margrel1,t38_margrel1), [interesting(0.00)]). fof(t14_binari_3,theorem,( ! [A] : ( m1_subset_1(A,k6_margrel1) => ! [B] : ( m1_subset_1(B,k6_margrel1) => ( k11_binarith(1,k13_binarith(k6_margrel1,A),k13_binarith(k6_margrel1,B)) = k8_margrel1 <=> ( A = k8_margrel1 & B = k8_margrel1 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_binarith,t13_binari_3,t45_margrel1,t25_finseq_4,t45_margrel1,d5_binarith,t38_margrel1,t45_margrel1,d5_binarith,t38_margrel1,t13_binari_3,t25_finseq_4,t45_margrel1,t19_binarith,d9_binarith,t19_binarith]), [file(binari_3,t14_binari_3),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(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(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(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(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(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(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(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(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(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(t30_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(A,1) = A ) ), file(power,t30_power), [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(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(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(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(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(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(t2_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)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( k9_binarith(A,B) = k9_binarith(A,C) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t117_finseq_2,t39_margrel1,t41_binarith,t42_binarith,t39_margrel1,t41_binarith,t42_binarith,t39_margrel1,t137_finseq_2,t137_finseq_2,t46_binarith,t46_binarith,d1_cqc_lang,d1_cqc_lang,t29_nat_1,t1_binari_3,t39_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,t29_nat_1,t1_binari_3,t39_margrel1,s1_binarith]), [file(binari_3,t2_binari_3),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(t2_jordan4,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(A,B) => k5_binarith(k1_nat_1(B,C),A) = k5_real_1(k1_nat_1(B,C),A) ) ) ) ) ), file(jordan4,t2_jordan4), [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(t76_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,B) => k4_nat_1(B,A) = B ) ) ) ), file(nat_1,t76_nat_1), [interesting(0.00)]). fof(t6_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => r2_hidden(k2_xcmplx_0(A,1),k2_finseq_1(k2_xcmplx_0(A,1))) ) ), file(finseq_1,t6_finseq_1), [interesting(0.00)]). fof(d4_finseq_4,definition,( ! [A,B,C] : ( ( v1_funct_1(C) & m2_relset_1(C,A,B) ) => ! [D] : ( r2_hidden(D,k1_relat_1(C)) => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ), file(finseq_4,d4_finseq_4), [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(t8_finseq_5,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k3_finseq_1(k7_finseq_1(k9_finseq_1(A),B)) = k1_nat_1(1,k3_finseq_1(B)) ) ), file(finseq_5,t8_finseq_5), [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(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(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) ) ) ) ), file(binarith,t50_binarith), [interesting(0.00)]). fof(t22_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( r1_xreal_0(A,k2_xcmplx_0(B,C)) <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ), file(xreal_1,t22_xreal_1), [interesting(0.00)]). 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 ) ) ) ), file(binarith,t53_binarith), [interesting(0.00)]). fof(t29_nat_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) => k3_nat_1(k3_nat_1(A,B),C) = k3_nat_1(A,k2_nat_1(B,C)) ) ) ) ), file(nat_2,t29_nat_2), [interesting(0.00)]). fof(t37_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) ) => ! [C] : ( v4_ordinal2(C) => ( r1_xreal_0(C,k3_finseq_1(k7_finseq_1(A,B))) => ( r1_xreal_0(C,k3_finseq_1(A)) | k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ) ), file(finseq_1,t37_finseq_1), [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(t62_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ( k4_nat_1(A,2) = 0 | k4_nat_1(A,2) = 1 ) ) ), file(nat_1,t62_nat_1), [interesting(0.00)]). fof(t51_binarith,theorem,( ! [A] : ( v4_ordinal2(A) => k5_binarith(A,A) = 0 ) ), file(binarith,t51_binarith), [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(t58_finseq_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) & v1_finseq_1(B) ) => k1_funct_1(k7_finseq_1(k9_finseq_1(A),B),1) = A ) ), file(finseq_1,t58_finseq_1), [interesting(0.00)]). fof(d5_real_1,definition,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> ~ ( r1_xreal_0(B,A) & B != A ) ) ) ) ), file(real_1,d5_real_1), [interesting(0.00)]). fof(t10_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [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) ) => ( ( k3_finseq_1(B) = A & k3_finseq_1(C) = A & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) ) => B = C ) ) ) ) ), file(finseq_2,t10_finseq_2), [interesting(0.00)]). fof(t77_finseq_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => m2_finseq_1(k2_finseq_2(A,C),B) ) ) ) ), file(finseq_2,t77_finseq_2), [interesting(0.00)]). fof(d13_margrel1,definition,( k7_margrel1 = 0 ), file(margrel1,d13_margrel1), [interesting(0.00)]). fof(d11_finseq_1,definition,( ! [A,B] : ( B = k13_finseq_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> m2_finseq_1(C,A) ) ) ), file(finseq_1,d11_finseq_1), [interesting(0.00)]). fof(t8_jordan2b,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => k3_finseq_1(k5_euclid(A)) = A ) ), file(jordan2b,t8_jordan2b), [interesting(0.00)]). fof(t110_finseq_2,theorem,( ! [A,B] : ( m2_finseq_1(B,A) => m1_subset_1(B,k4_finseq_2(k3_finseq_1(B),A)) ) ), file(finseq_2,t110_finseq_2), [interesting(0.00)]). fof(t4_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => k3_nat_1(0,A) = 0 ) ), file(nat_2,t4_nat_2), [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(t73_finseq_2,theorem,( ! [A] : k2_finseq_2(1,A) = k9_finseq_1(A) ), file(finseq_2,t73_finseq_2), [interesting(0.00)]). fof(t74_finseq_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : k2_finseq_2(k1_nat_1(A,1),B) = k7_finseq_1(k2_finseq_2(A,B),k9_finseq_1(B)) ) ), file(finseq_2,t74_finseq_2), [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(t71_nat_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(2,A) & A != 0 & A != 1 ) ) ), file(nat_1,t71_nat_1), [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(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(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_nat_1), [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(t23_nat_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( v1_abian(A) <=> k4_nat_1(A,2) = 0 ) ) ), file(nat_2,t23_nat_2), [interesting(0.00)]). fof(t25_nat_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) => ( ( r1_xreal_0(1,C) & r1_xreal_0(B,A) & r1_nat_1(k2_nat_1(2,C),B) ) => ( v1_abian(k3_nat_1(A,C)) <=> v1_abian(k3_nat_1(k5_binarith(A,B),C)) ) ) ) ) ) ), file(nat_2,t25_nat_2), [interesting(0.00)]). fof(t24_nat_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ~ v1_abian(A) <=> k4_nat_1(A,2) = 1 ) ) ), file(nat_2,t24_nat_2), [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(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(t8_finseq_2,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(k1_nat_1(B,1))) & ~ r2_hidden(A,k2_finseq_1(B)) & A != k1_nat_1(B,1) ) ) ) ), file(finseq_2,t8_finseq_2), [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(t11_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] : ( m1_subset_1(C,k6_margrel1) => k6_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C))) = k12_binarith(A,1,k6_margrel1,k6_binarith(A,B),k13_binarith(k6_margrel1,k11_margrel1(C))) ) ) ) ), file(binari_2,t11_binari_2), [interesting(0.00)]). fof(t20_finseq_2,theorem,( ! [A,B,C] : ( ( v1_relat_1(C) & v1_funct_1(C) & v1_finseq_1(C) ) => ! [D] : ( ( v1_relat_1(D) & v1_funct_1(D) & v1_finseq_1(D) ) => ( k7_finseq_1(C,k9_finseq_1(A)) = k7_finseq_1(D,k9_finseq_1(B)) => ( C = D & A = B ) ) ) ) ), file(finseq_2,t20_finseq_2), [interesting(0.00)]). fof(t19_nat_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(A,0) => k4_nat_1(k3_series_1(2,A),2) = 0 ) ) ), file(nat_2,t19_nat_2), [interesting(0.00)]). fof(t17_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ( ( r1_nat_1(A,B) & r1_xreal_0(1,B) & r1_xreal_0(1,C) & r1_xreal_0(C,A) ) => k3_nat_1(k5_binarith(B,C),A) = k6_xcmplx_0(k3_nat_1(B,A),1) ) ) ) ) ), file(nat_2,t17_nat_2), [interesting(0.00)]). fof(t18_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) => k3_nat_1(k3_series_1(2,A),k3_series_1(2,B)) = k3_series_1(2,k5_binarith(A,B)) ) ) ) ), file(nat_2,t18_nat_2), [interesting(0.00)]). fof(t20_nat_2,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ( ~ r1_xreal_0(A,0) => ( k4_nat_1(A,2) = 0 <=> k4_nat_1(k5_binarith(A,1),2) = 1 ) ) ) ), file(nat_2,t20_nat_2), [interesting(0.00)]). fof(t8_binari_2,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)) => ( B = 1 | k4_finseq_4(k5_numbers,k6_margrel1,k2_binari_2(A),B) = k7_margrel1 ) ) ) ) ), file(binari_2,t8_binari_2), [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(t7_binari_2,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)) & B = 1 ) => k4_finseq_4(k5_numbers,k6_margrel1,k2_binari_2(A),B) = k8_margrel1 ) ) ) ), file(binari_2,t7_binari_2), [interesting(0.00)]). 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) ) ) ) ), file(binarith,t5_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(t9_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( ~ r1_xreal_0(A,B) => k1_nat_1(k5_binarith(A,k2_xcmplx_0(B,1)),1) = k5_binarith(A,B) ) ) ) ), file(nat_2,t9_nat_2), [interesting(0.00)]). fof(t21_nat_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & v4_ordinal2(A) ) => ~ ( A != 1 & r1_xreal_0(A,1) ) ) ), file(nat_2,t21_nat_2), [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(t7_nat_2,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ! [C] : ( v4_ordinal2(C) => ! [D] : ( v4_ordinal2(D) => ( ( r1_xreal_0(A,B) & r1_xreal_0(C,B) & A = k2_xcmplx_0(k5_binarith(B,C),D) ) => C = k2_xcmplx_0(k5_binarith(B,A),D) ) ) ) ) ) ), file(nat_2,t7_nat_2), [interesting(0.00)]). fof(d1_nat_2,definition,( ! [A] : ( v4_ordinal2(A) => ( v1_realset1(A) <=> ( A = 0 | A = 1 ) ) ) ), file(nat_2,d1_nat_2), [interesting(0.00)]). fof(s2_nat_2,theorem, ( ( p1_s2_nat_2(2) & ! [A] : ( ( ~ v1_realset1(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ( p1_s2_nat_2(A) => p1_s2_nat_2(k1_nat_1(A,1)) ) ) ) => ! [A] : ( ( ~ v1_realset1(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => p1_s2_nat_2(A) ) ), file(nat_2,s2_nat_2), [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) ), inference(mizar_proof,[status(thm)],[t14_binari_3,t38_margrel1,t39_margrel1,d10_binarith,t48_binarith,t42_binarith,t41_binarith,t42_binarith,t2_binari_3,t14_binari_3,t38_margrel1,t39_margrel1,d10_binarith,t48_binarith,t41_binarith,t2_binari_3]), [file(binari_3,t18_binari_3),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(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)))) ) ) ) ) ) ), file(binarith,t45_binarith), [interesting(0.00)]). fof(t9_binari_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => k2_binari_2(k23_binop_2(A,1)) = k12_binarith(A,1,k6_margrel1,k2_binari_2(A),k13_binarith(k6_margrel1,k7_margrel1)) ) ), file(binari_2,t9_binari_2), [interesting(0.00)]). fof(t3_jordan4,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(A,B) => k5_binarith(k1_nat_1(B,C),A) = k1_nat_1(k5_binarith(B,A),C) ) ) ) ) ), file(jordan4,t3_jordan4), [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(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(d14_margrel1,definition,( k8_margrel1 = 1 ), file(margrel1,d14_margrel1), [interesting(0.00)]). fof(t52_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & r1_xreal_0(k6_xcmplx_0(B,A),0) ) ) ) ), file(xreal_1,t52_xreal_1), [interesting(0.00)]). fof(t22_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( A != 0 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => A != k1_nat_1(B,1) ) ) ) ), file(nat_1,t22_nat_1), [interesting(0.00)]). fof(t72_nat_1,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ( B != 0 => k3_nat_1(k2_nat_1(A,B),B) = A ) ) ) ), file(nat_1,t72_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(t5_nat_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => k3_nat_1(A,A) = 1 ) ), file(nat_2,t5_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(t19_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => ~ ( 0 != A & r1_xreal_0(A,0) ) ) ), file(nat_1,t19_nat_1), [interesting(0.00)]). fof(t15_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)) => k9_binarith(A,k6_binarith(A,B)) = k10_binop_2(k9_binop_2(k7_binop_2(k9_binarith(A,B)),k3_series_1(2,A)),1) ) ) ), file(binari_2,t15_binari_2), [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(t29_finseq_6,theorem,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_finseq_1(A) ) => k3_finseq_5(k3_finseq_5(A)) = A ) ), file(finseq_6,t29_finseq_6), [interesting(0.00)]). fof(t8_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,k6_binarith(A,B)) = k5_real_1(k3_series_1(2,A),1) ) ) ) ), inference(mizar_proof,[status(thm)],[t15_binari_2,t7_binari_3]), [file(binari_3,t8_binari_3),interesting(0.00)]). fof(t2_euclid,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k1_numbers,k1_euclid(A)) => k3_finseq_1(B) = A ) ) ), file(euclid,t2_euclid), [interesting(0.00)]).