fof(t18_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) => k3_binari_2(k23_binop_2(A,1),k3_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C)))) = k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_finseq_1,t14_binarith,d9_binarith,d5_binarith,d5_binarith,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,t7_binari_2,t50_margrel1,d4_binarith,t14_binarith,d9_binarith,d5_binarith,d5_binarith,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,t7_binari_2,t50_margrel1,d4_binarith,d8_binarith,d5_binarith,t7_binari_2,t33_binarith,t34_binarith,t13_binarith,t40_margrel1,d4_binarith,t11_binari_2,t9_binari_2,t45_binarith,t11_binari_2,t9_binari_2,t45_binarith,t2_binarith,d8_binarith,d5_binarith,t7_binari_2,t33_binarith,t34_binarith,t13_binarith,d4_binarith,t40_margrel1,d8_binarith,d5_binarith,t7_binari_2,t33_binarith,t34_binarith,t13_binarith,d4_binarith,t40_margrel1,t3_binarith,d2_binarith,t40_margrel1,t40_margrel1,t10_binarith,t9_binarith,t9_binarith,t40_margrel1,t40_margrel1,t22_binarith,t22_binarith,t22_binarith,t46_margrel1,t46_margrel1,t7_binarith,t7_binarith,d2_binarith,t10_binarith,t9_binarith,t9_binarith,t40_margrel1,t40_margrel1,t52_margrel1,t22_binarith,t46_margrel1,t7_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t52_margrel1,t16_binarith,t40_margrel1,t22_binarith,t52_margrel1,t16_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t22_binarith,t18_binarith,t50_margrel1,t120_finseq_2,t26_finseq_4,t117_finseq_2,t25_finseq_4,d9_finseq_1,t137_finseq_2,t16_binari_2,t16_binari_2,t3_binarith,t3_binarith,d2_binarith,t10_binarith,t9_binarith,t9_binarith,t40_margrel1,t40_margrel1,t40_margrel1,t22_binarith,t27_binarith,t27_binarith,d2_binarith,t34_binarith,t14_binarith,t34_binarith,t15_binarith,t14_binarith,t34_binarith,t15_binarith,t14_binarith,t15_binarith,t34_binarith,t15_binarith,t14_binarith,t15_binarith,t14_binarith,t5_finseq_1,t11_binari_2,t9_binari_2,d9_binarith,t3_binarith,t3_binarith,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,t3_binarith,t44_binarith,t9_binari_2,d9_binarith,t3_binarith,t3_binarith,t49_margrel1,t49_margrel1,t7_binarith,t7_binarith,t11_binari_2,t11_binari_2,t9_binari_2,t9_binari_2,d4_binarith,d8_binarith,t3_binarith,t3_binarith,t44_binarith,t14_binarith,t45_binarith,t11_binari_2,t44_binarith,d2_binarith,t10_binarith,t9_binarith,t9_binarith,t40_margrel1,t40_margrel1,t40_margrel1,t52_margrel1,t25_binarith,t27_binarith,d2_binarith,t10_binarith,t9_binarith,t9_binarith,t40_margrel1,t40_margrel1,t40_margrel1,t22_binarith,t27_binarith,t27_binarith,d2_binarith,t34_binarith,t15_binarith,t14_binarith,t16_binari_2,t16_binari_2,s1_binarith]), [file(binari_2,t18_binari_2),interesting(1.00)]). fof(t10_binari_2,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => k4_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,k2_binari_2(A),k13_binarith(k6_margrel1,k7_margrel1))) = 1 ) ), inference(mizar_proof,[status(thm)],[t117_finseq_2,t25_finseq_4,t5_finseq_1,t7_binari_2,t4_binari_2,t3_binarith,d3_binari_2,t3_binarith,d3_binari_2,t9_binari_2,t46_binarith,d1_cqc_lang,s1_binarith]), [file(binari_2,t10_binari_2),interesting(0.84)]). fof(t19_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)) => k7_binari_2(A,B,C) = k10_binarith(A,B,k3_binari_2(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_binari_2,d8_binarith]), [file(binari_2,t19_binari_2),interesting(0.76)]). 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) ) ) ), inference(mizar_proof,[status(thm)],[t25_finseq_4,t117_finseq_2,t25_finseq_4,t5_finseq_1,d4_binarith,d16_margrel1,t41_binarith,t30_power,t42_binarith,t25_finseq_4,t117_finseq_2,t25_finseq_4,t5_finseq_1,d4_binarith,d16_margrel1,t42_binarith,t30_power,t41_binarith,t40_binarith,t137_finseq_2,t11_binari_2,t46_binarith,t46_binarith,t38_margrel1,d16_margrel1,d1_cqc_lang,t30_power,t32_power,d1_cqc_lang,d16_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,t32_power,t30_power,t39_margrel1,s1_binarith]), [file(binari_2,t15_binari_2),interesting(0.76)]). 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)) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t109_finseq_2,t2_binarith,t7_binari_2,t7_binari_2,t2_binarith,t8_binari_2,t8_binari_2,t39_nat_1,t38_nat_1,t8_binari_2,t3_binarith,t8_finseq_2,l1_binari_2]), [file(binari_2,t9_binari_2),interesting(0.74)]). fof(t4_binari_2,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(2,k6_margrel1)) => ( A = k12_binarith(1,1,k6_margrel1,k13_binarith(k6_margrel1,k8_margrel1),k13_binarith(k6_margrel1,k7_margrel1)) => k4_binari_2(2,A) = 1 ) ) ), inference(mizar_proof,[status(thm)],[t120_finseq_2,d9_finseq_1,t26_finseq_4,t5_finseq_1,t7_finseq_1,d6_binarith,d1_cqc_lang,t38_margrel1,d3_binarith,t29_power,t26_finseq_4,t5_finseq_1,d6_binarith,d1_cqc_lang,t26_finseq_4,d7_binarith,d9_finseq_1,t6_finsop_1,t12_finsop_1,t12_finsop_1,d23_binop_2,d3_binari_2]), [file(binari_2,t4_binari_2),interesting(0.67)]). 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))) ) ) ) ), inference(mizar_proof,[status(thm)],[t109_finseq_2,t109_finseq_2,d4_binarith,t2_binarith,t2_binarith,d4_binarith,d4_binarith,t3_binarith,t3_binarith,t8_finseq_2,l1_binari_2]), [file(binari_2,t11_binari_2),interesting(0.60)]). fof(t3_binari_2,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(2,k6_margrel1)) => ( A = k12_binarith(1,1,k6_margrel1,k13_binarith(k6_margrel1,k7_margrel1),k13_binarith(k6_margrel1,k7_margrel1)) => k4_binari_2(2,A) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t120_finseq_2,d9_finseq_1,t26_finseq_4,t5_finseq_1,t7_finseq_1,d6_binarith,d1_cqc_lang,t26_finseq_4,t5_finseq_1,d6_binarith,d1_cqc_lang,t26_finseq_4,d7_binarith,d9_finseq_1,t6_finsop_1,t12_finsop_1,t12_finsop_1,d23_binop_2,d3_binari_2]), [file(binari_2,t3_binari_2),interesting(0.57)]). fof(t6_binari_2,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(2,k6_margrel1)) => ( A = k12_binarith(1,1,k6_margrel1,k13_binarith(k6_margrel1,k8_margrel1),k13_binarith(k6_margrel1,k8_margrel1)) => k4_binari_2(2,A) = k7_binop_2(1) ) ) ), inference(mizar_proof,[status(thm)],[t120_finseq_2,d9_finseq_1,t26_finseq_4,t38_margrel1,d3_binari_2,t32_power,t30_power,t30_power,t5_finseq_1,t7_finseq_1,d6_binarith,d1_cqc_lang,d3_binarith,t29_power,t26_finseq_4,t5_finseq_1,d6_binarith,d1_cqc_lang,d3_binarith,t30_power,t26_finseq_4,d7_binarith,d9_finseq_1,t6_finsop_1,t12_finsop_1,t12_finsop_1,d23_binop_2]), [file(binari_2,t6_binari_2),interesting(0.57)]). fof(t5_binari_2,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(2,k6_margrel1)) => ( A = k12_binarith(1,1,k6_margrel1,k13_binarith(k6_margrel1,k7_margrel1),k13_binarith(k6_margrel1,k8_margrel1)) => k4_binari_2(2,A) = k7_binop_2(2) ) ) ), inference(mizar_proof,[status(thm)],[t120_finseq_2,d9_finseq_1,t26_finseq_4,d3_binari_2,t38_margrel1,t32_power,t30_power,t30_power,t5_finseq_1,t7_finseq_1,d6_binarith,d1_cqc_lang,t26_finseq_4,t5_finseq_1,d6_binarith,d1_cqc_lang,t38_margrel1,d3_binarith,t30_power,t26_finseq_4,d7_binarith,d9_finseq_1,t6_finsop_1,t12_finsop_1,t12_finsop_1,d23_binop_2]), [file(binari_2,t5_binari_2),interesting(0.56)]). fof(t16_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) => k3_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C))) = k12_binarith(A,1,k6_margrel1,k3_binari_2(A,B),k13_binarith(k6_margrel1,k4_binarith(k11_margrel1(C),k11_binarith(A,k6_binarith(A,B),k2_binari_2(A))))) ) ) ) ), inference(mizar_proof,[status(thm)],[t11_binari_2,t9_binari_2,t45_binarith,t14_binarith]), [file(binari_2,t16_binari_2),interesting(0.52)]). fof(t12_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) => k4_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C))) = k10_binop_2(k9_binarith(A,B),k2_cqc_lang(k5_numbers,C,k7_margrel1,0,k3_series_1(2,A))) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_binarith,d3_binari_2,t46_binarith,d1_cqc_lang,d1_cqc_lang,t3_binarith,t38_margrel1,d3_binari_2,t46_binarith,d1_cqc_lang,t38_margrel1,t32_power,t30_power,d1_cqc_lang,t38_margrel1,t39_margrel1]), [file(binari_2,t12_binari_2),interesting(0.41)]). fof(t17_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) => k2_xcmplx_0(k4_binari_2(k23_binop_2(A,1),k3_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C)))),k2_cqc_lang(k5_numbers,k5_binari_2(k23_binop_2(A,1),k6_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C))),k2_binari_2(k23_binop_2(A,1))),k7_margrel1,0,k3_series_1(2,k23_binop_2(A,1)))) = k4_xcmplx_0(k4_binari_2(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t3_binarith,t49_margrel1,t49_margrel1,t11_binari_2,t11_binari_2,t9_binari_2,t9_binari_2,t14_binari_2,t10_binari_2,d1_cqc_lang,t12_binari_2,t15_binari_2,t12_binari_2,t38_margrel1,d16_margrel1,d1_cqc_lang,d1_cqc_lang,d16_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,t39_margrel1]), [file(binari_2,t17_binari_2),interesting(0.41)]). fof(t20_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) => k7_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))) = k12_binarith(A,1,k6_margrel1,k10_binarith(A,B,k3_binari_2(A,C)),k13_binarith(k6_margrel1,k4_binarith(k4_binarith(k4_binarith(D,k11_margrel1(E)),k11_binarith(A,k6_binarith(A,C),k2_binari_2(A))),k11_binarith(A,B,k3_binari_2(A,C))))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binari_2,t16_binari_2,t45_binarith,t34_binarith]), [file(binari_2,t20_binari_2),interesting(0.28)]). fof(t13_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) => k6_xcmplx_0(k2_xcmplx_0(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_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)))) = 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)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_binarith,t45_binarith,t12_binari_2,t3_binarith,t3_binarith,t44_binarith,t3_binarith,t3_binarith,t44_binarith,t12_binari_2,t12_binari_2,d1_cqc_lang,d1_cqc_lang,t14_binarith,t14_binarith,d16_margrel1,d16_margrel1,t50_margrel1,t50_margrel1,t52_margrel1,t49_margrel1,d1_cqc_lang,d1_cqc_lang,d1_cqc_lang,t12_binari_2,d1_cqc_lang,t38_margrel1,d1_cqc_lang,t38_margrel1,t30_power,t32_power,t12_binari_2,t39_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,t14_binarith,t13_binarith,d16_margrel1,t49_margrel1,t49_margrel1,d1_cqc_lang,t49_margrel1,t49_margrel1,d1_cqc_lang,t38_margrel1,d16_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,d16_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,t39_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,t14_binarith,t13_binarith,d16_margrel1,t49_margrel1,t49_margrel1,d1_cqc_lang,t52_margrel1,t49_margrel1,d1_cqc_lang,t38_margrel1,d16_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,d16_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,t39_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,t38_margrel1,t30_power,t32_power,t15_binarith,t14_binarith,d16_margrel1,t49_margrel1,t49_margrel1,d1_cqc_lang,t50_margrel1,t50_margrel1,t38_margrel1,d16_margrel1,d1_cqc_lang,d1_cqc_lang,t38_margrel1,d16_margrel1,d1_cqc_lang,t38_margrel1,d1_cqc_lang,t30_power,t32_power,t39_margrel1,t39_margrel1]), [file(binari_2,t13_binari_2),interesting(0.13)]). 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)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_binari_2]), [file(binari_2,t14_binari_2),interesting(0.13)]). 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(t14_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k7_margrel1,A) = A ) ), file(binarith,t14_binarith), [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(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(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(d1_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)) => ( B = k2_binari_2(A) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ( r2_hidden(C,k2_finseq_1(A)) => k4_finseq_4(k5_numbers,k6_margrel1,B,C) = k2_cqc_lang(k6_margrel1,C,1,k8_margrel1,k7_margrel1) ) ) ) ) ) ), file(binari_2,d1_binari_2), [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(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 ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_2,d1_cqc_lang]), [file(binari_2,t7_binari_2),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(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(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(t33_binarith,theorem,( k4_binarith(k8_margrel1,k7_margrel1) = k8_margrel1 ), file(binarith,t33_binarith), [interesting(0.00)]). fof(t34_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k2_binarith(k2_binarith(A,B),C) = k2_binarith(A,k2_binarith(B,C)) ) ) ) ), file(binarith,t34_binarith), [interesting(0.00)]). fof(t13_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(k8_margrel1,A) = k9_margrel1(A) ) ), file(binarith,t13_binarith), [interesting(0.00)]). fof(t40_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k9_margrel1(k9_margrel1(A)) = A ) ), file(margrel1,t40_margrel1), [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_binarith,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( ~ v1_xboole_0(C) => ! [D] : ( m1_subset_1(D,C) => ! [E] : ( m2_finseq_2(E,C,k4_finseq_2(B,C)) => ( r2_hidden(A,k2_finseq_1(B)) => k4_finseq_4(k5_numbers,C,k8_finseq_1(C,E,k12_finseq_1(C,D)),A) = k4_finseq_4(k5_numbers,C,E,A) ) ) ) ) ) ) ), file(binarith,t2_binarith), [interesting(0.00)]). fof(t3_binarith,theorem,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( ~ v1_xboole_0(B) => ! [C] : ( m1_subset_1(C,B) => ! [D] : ( m2_finseq_2(D,B,k4_finseq_2(A,B)) => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,D,k12_finseq_1(B,C)),k23_binop_2(A,1)) = C ) ) ) ) ), file(binarith,t3_binarith), [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(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(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(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(l1_binari_2,theorem,( ! [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)) => ( ( 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)) => k4_finseq_4(k5_numbers,k6_margrel1,B,D) = k4_finseq_4(k5_numbers,k6_margrel1,C,D) ) ) ) => B = C ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_finseq_1,d4_finseq_4,t10_finseq_2]), [file(binari_2,l1_binari_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 ) ) ) ) ), inference(mizar_proof,[status(thm)],[d1_binari_2,d1_cqc_lang]), [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(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(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(d2_binarith,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,B) = k1_binarith(k10_margrel1(k9_margrel1(A),B),k10_margrel1(A,k9_margrel1(B))) ) ) ), file(binarith,d2_binarith), [interesting(0.00)]). fof(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(t9_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k10_margrel1(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ), file(binarith,t9_binarith), [interesting(0.00)]). fof(t22_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k1_binarith(B,C)) = k1_binarith(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ), file(binarith,t22_binarith), [interesting(0.00)]). fof(t46_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,k9_margrel1(A)) = k7_margrel1 ) ), file(margrel1,t46_margrel1), [interesting(0.00)]). fof(t52_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k10_margrel1(B,C)) = k10_margrel1(k10_margrel1(A,B),C) ) ) ) ), file(margrel1,t52_margrel1), [interesting(0.00)]). fof(t16_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,A) = A ) ), file(binarith,t16_binarith), [interesting(0.00)]). fof(t18_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ), file(binarith,t18_binarith), [interesting(0.00)]). fof(t120_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_2(B,A,k4_finseq_2(2,A)) => ? [C] : ( m1_subset_1(C,A) & ? [D] : ( m1_subset_1(D,A) & B = k10_finseq_1(C,D) ) ) ) ) ), file(finseq_2,t120_finseq_2), [interesting(0.00)]). fof(t26_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ( k4_finseq_4(k5_numbers,A,k2_finseq_4(A,B,C),1) = B & k4_finseq_4(k5_numbers,A,k2_finseq_4(A,B,C),2) = C ) ) ) ) ), file(finseq_4,t26_finseq_4), [interesting(0.00)]). fof(t117_finseq_2,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_2(B,A,k4_finseq_2(1,A)) => ? [C] : ( m1_subset_1(C,A) & B = k12_finseq_1(A,C) ) ) ) ), file(finseq_2,t117_finseq_2), [interesting(0.00)]). fof(t25_finseq_4,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => k4_finseq_4(k5_numbers,A,k12_finseq_1(A,B),1) = B ) ) ), file(finseq_4,t25_finseq_4), [interesting(0.00)]). fof(d9_finseq_1,definition,( ! [A,B] : k10_finseq_1(A,B) = k7_finseq_1(k9_finseq_1(A),k9_finseq_1(B)) ), file(finseq_1,d9_finseq_1), [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(t27_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binarith(k9_margrel1(A),B)) = k10_margrel1(A,B) ) ) ), file(binarith,t27_binarith), [interesting(0.00)]). fof(t15_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k2_binarith(A,A) = k7_margrel1 ) ), file(binarith,t15_binarith), [interesting(0.00)]). fof(t44_binarith,theorem,( ! [A] : ( ( ~ v1_xboole_0(A) & m2_subset_1(A,k1_numbers,k5_numbers) ) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [D] : ( m1_subset_1(D,k6_margrel1) => ! [E] : ( m1_subset_1(E,k6_margrel1) => k11_binarith(A,B,C) = k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,B,k13_binarith(k6_margrel1,D)),k12_binarith(A,1,k6_margrel1,C,k13_binarith(k6_margrel1,E))),k23_binop_2(A,1)) ) ) ) ) ) ), file(binarith,t44_binarith), [interesting(0.00)]). fof(t25_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binarith(A,B)) = A ) ) ), file(binarith,t25_binarith), [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(t1_binari_2,theorem,( $true ), file(binari_2,t1_binari_2), [interesting(0.00)]). fof(d6_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)) => ! [D] : ( m2_finseq_2(D,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ( D = k7_binari_2(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,k3_binari_2(A,C),E)),k4_finseq_4(k5_numbers,k6_margrel1,k7_binarith(A,B,k3_binari_2(A,C)),E)) ) ) ) ) ) ) ) ), file(binari_2,d6_binari_2), [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(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(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(t38_margrel1,theorem,( k7_margrel1 != k8_margrel1 ), file(margrel1,t38_margrel1), [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(t30_power,theorem,( ! [A] : ( v1_xreal_0(A) => k3_power(A,1) = A ) ), file(power,t30_power), [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(d16_margrel1,definition,( ! [A] : ( v2_margrel1(A) => ( ( A = k7_margrel1 => k9_margrel1(A) = k8_margrel1 ) & ( A != k7_margrel1 => k9_margrel1(A) = k7_margrel1 ) ) ) ), file(margrel1,d16_margrel1), [interesting(0.00)]). fof(t7_finseq_1,theorem,( ! [A] : ( v4_ordinal2(A) => ! [B] : ( v4_ordinal2(B) => ( r1_xreal_0(A,B) <=> r1_tarski(k2_finseq_1(A),k2_finseq_1(B)) ) ) ) ), file(finseq_1,t7_finseq_1), [interesting(0.00)]). fof(d6_binarith,definition,( ! [A] : ( m2_subset_1(A,k1_numbers,k5_numbers) => ! [B] : ( m2_finseq_2(B,k6_margrel1,k4_finseq_2(A,k6_margrel1)) => ! [C] : ( m2_finseq_2(C,k5_numbers,k4_finseq_2(A,k5_numbers)) => ( C = k8_binarith(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ( r2_hidden(D,k2_finseq_1(A)) => k4_finseq_4(k5_numbers,k5_numbers,C,D) = k2_cqc_lang(k5_numbers,k4_finseq_4(k5_numbers,k6_margrel1,B,D),k7_margrel1,0,k3_series_1(2,k5_binarith(D,1))) ) ) ) ) ) ) ), file(binarith,d6_binarith), [interesting(0.00)]). fof(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(d7_binarith,definition,( ! [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,B) = k2_finsop_1(k5_numbers,k8_binarith(A,B),k47_binop_2) ) ) ), file(binarith,d7_binarith), [interesting(0.00)]). fof(t6_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m2_finseq_1(B,A) => ! [C] : ( m2_finseq_1(C,A) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k2_zfmisc_1(A,A),A) & m2_relset_1(D,k2_zfmisc_1(A,A),A) ) => ( v2_binop_1(D,A) => ( ( ~ v1_setwiseo(D,A) & ~ ( r1_xreal_0(1,k3_finseq_1(B)) & r1_xreal_0(1,k3_finseq_1(C)) ) ) | k2_finsop_1(A,k8_finseq_1(A,B,C),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,B,D),k2_finsop_1(A,C,D)) ) ) ) ) ) ) ), file(finsop_1,t6_finsop_1), [interesting(0.00)]). fof(t12_finsop_1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k2_zfmisc_1(A,A),A) & m2_relset_1(C,k2_zfmisc_1(A,A),A) ) => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ), file(finsop_1,t12_finsop_1), [interesting(0.00)]). fof(d23_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) & m2_relset_1(A,k2_zfmisc_1(k5_numbers,k5_numbers),k5_numbers) ) => ( A = k47_binop_2 <=> ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_binop_1(k5_numbers,k5_numbers,k5_numbers,A,B,C) = k23_binop_2(B,C) ) ) ) ) ), file(binop_2,d23_binop_2), [interesting(0.00)]). fof(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(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(t40_binarith,theorem,( ! [A] : ( m2_finseq_2(A,k6_margrel1,k4_finseq_2(1,k6_margrel1)) => ( A = k12_finseq_1(k6_margrel1,k7_margrel1) | A = k12_finseq_1(k6_margrel1,k8_margrel1) ) ) ), file(binarith,t40_binarith), [interesting(0.00)]). fof(t21_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) => k2_xcmplx_0(k6_xcmplx_0(k2_xcmplx_0(k4_binari_2(k23_binop_2(A,1),k7_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)))),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)),k3_binari_2(k23_binop_2(A,1),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)),k3_binari_2(k23_binop_2(A,1),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,k5_binari_2(k23_binop_2(A,1),k6_binarith(k23_binop_2(A,1),k12_binarith(A,1,k6_margrel1,C,k13_binarith(k6_margrel1,E))),k2_binari_2(k23_binop_2(A,1))),k7_margrel1,0,k3_series_1(2,k23_binop_2(A,1)))) = k6_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)))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_binari_2,t16_binari_2,t16_binari_2,t16_binari_2,t13_binari_2,t16_binari_2,t17_binari_2]), [file(binari_2,t21_binari_2),interesting(0.00)]). fof(t2_binari_2,theorem,( $true ), file(binari_2,t2_binari_2), [interesting(0.00)]).