fof(l2_bhsp_7,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(A,k6_real_1(1,k1_nat_1(B,1))) ) ) ) ), inference(mizar_proof,[status(thm)],[t124_xreal_1,t10_seq_4,t10_xreal_1,t78_xreal_1,t218_xcmplx_1]), [file(bhsp_7,l2_bhsp_7),interesting(1.00)]). fof(l11_bhsp_7,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(A,B))) ) ) => A = B ) ) ) ), inference(mizar_proof,[status(thm)],[t133_complex1]), [file(bhsp_7,l11_bhsp_7),interesting(0.97)]). fof(l3_bhsp_7,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(A,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ~ ( ~ r1_xreal_0(A,k6_real_1(1,k1_nat_1(C,1))) & r1_xreal_0(B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t124_xreal_1,t10_seq_4,t29_nat_1,t2_xreal_1,t10_xreal_1,t78_xreal_1,t29_nat_1,t218_xcmplx_1]), [file(bhsp_7,l3_bhsp_7),interesting(0.95)]). fof(t5_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m2_bhsp_5(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( m1_subset_1(C,k1_zfmisc_1(B)) => m2_bhsp_5(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d9_bhsp_5,t4_bhsp_7,d9_bhsp_5,d9_bhsp_5]), [file(bhsp_7,t5_bhsp_7),interesting(0.90)]). fof(l1_bhsp_7,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(k6_real_1(D,2),k18_complex1(k5_real_1(A,B))) & ~ r1_xreal_0(k6_real_1(D,2),k18_complex1(k5_real_1(B,C))) & r1_xreal_0(D,k18_complex1(k5_real_1(A,C))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t142_complex1,t10_xreal_1,t2_xreal_1]), [file(bhsp_7,l1_bhsp_7),interesting(0.90)]). fof(t4_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_bhsp_5(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( m1_subset_1(C,k1_zfmisc_1(B)) => m1_bhsp_5(C,A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_bhsp_5,d8_bhsp_5]), [file(bhsp_7,t4_bhsp_7),interesting(0.85)]). fof(t6_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( ( v1_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v2_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v1_setwiseo(u1_rlvect_1(A),u1_struct_0(A)) & v4_bhsp_3(A) ) => ! [B] : ( m2_bhsp_5(B,A) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),k6_supinf_1) & m2_relset_1(C,u1_struct_0(A),k6_supinf_1) ) => ( ( r1_tarski(B,k1_relat_1(C)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,B) => k8_funct_2(u1_struct_0(A),k6_supinf_1,C,D) = k2_bhsp_1(A,D,D) ) ) ) => ( v1_bhsp_6(B,A) <=> r1_bhsp_6(A,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t93_square_1,t1_chain_1,t78_square_1,d4_square_1,t10_bhsp_6,t34_bhsp_1,t78_square_1,t2_xreal_1,t5_bhsp_7,d9_bhsp_5,t1_xboole_1,t3_bhsp_7,d4_bhsp_1,d2_bhsp_1,d4_square_1,d2_bhsp_1,d1_absvalue,t1_bhsp_7,t131_xreal_1,t1_bhsp_7,t11_absvalue,t92_real_1,t50_xreal_1,t5_bhsp_7,d9_bhsp_5,t1_xboole_1,t3_bhsp_7,d2_bhsp_1,d4_bhsp_1,d4_square_1,t34_bhsp_1,t72_square_1,t95_square_1,t89_square_1,t89_square_1,t10_bhsp_6]), [file(bhsp_7,t6_bhsp_7),interesting(0.72)]). fof(t8_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( ( v1_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v2_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v1_setwiseo(u1_rlvect_1(A),u1_struct_0(A)) & v4_bhsp_3(A) ) => ! [B] : ( m2_bhsp_5(B,A) => ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),k6_supinf_1) & m2_relset_1(C,u1_struct_0(A),k6_supinf_1) ) => ( ( r1_tarski(B,k1_relat_1(C)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,B) => k8_funct_2(u1_struct_0(A),k6_supinf_1,C,D) = k2_bhsp_1(A,D,D) ) ) & v1_bhsp_6(B,A) ) => k2_bhsp_1(A,k2_bhsp_6(A,B),k2_bhsp_6(A,B)) = k3_bhsp_6(A,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t6_bhsp_7,t1_xboole_1,t5_bhsp_7,d9_bhsp_5,t3_bhsp_7,t73_real_1,t7_bhsp_7,d7_bhsp_6,t7_xboole_1,t8_xboole_1,t142_complex1,t10_xreal_1,t13_uniform1,t2_xreal_1,l11_bhsp_7]), [file(bhsp_7,t8_bhsp_7),interesting(0.60)]). fof(t7_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v1_bhsp_6(B,A) => ( v1_xboole_0(B) | ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( ( v1_finset_1(D) & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(D) & r1_tarski(D,B) & ! [E] : ( ( v1_finset_1(E) & m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( r1_tarski(D,E) & r1_tarski(E,B) & r1_xreal_0(C,k18_complex1(k5_real_1(k2_bhsp_1(A,k2_bhsp_6(A,B),k2_bhsp_6(A,B)),k2_bhsp_1(A,k1_bhsp_6(A,E),k1_bhsp_6(A,E))))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_bhsp_1,t121_real_2,t10_xreal_1,t127_real_2,d3_bhsp_6,d3_bhsp_6,d1_xboole_0,d2_xboole_0,t8_xboole_1,t17_bhsp_1,t16_bhsp_1,t142_complex1,t35_bhsp_1,t9_xreal_1,t8_xreal_1,t35_bhsp_1,t9_xreal_1,t8_xreal_1,t37_bhsp_1,t27_rlvect_1,t16_rlvect_1,d6_rlvect_1,t36_bhsp_1,t37_bhsp_1,t11_xboole_1,t10_xreal_1,t92_real_1,t10_xreal_1,t34_bhsp_1,t66_xreal_1,t11_xboole_1,t70_xreal_1,t10_xreal_1,t92_real_1,t88_xcmplx_1,t10_xreal_1,t92_real_1]), [file(bhsp_7,t7_bhsp_7),interesting(0.54)]). fof(t1_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),k6_supinf_1) & m2_relset_1(C,u1_struct_0(A),k6_supinf_1) ) => ( r1_bhsp_6(A,B,C) <=> ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(D,0) & ! [E] : ( ( v1_finset_1(E) & m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(E) & r1_tarski(E,B) & ! [F] : ( ( v1_finset_1(F) & m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(F) & r1_tarski(F,B) & r1_xboole_0(E,F) & r1_xreal_0(D,k18_complex1(k5_bhsp_5(k1_numbers,u1_struct_0(A),k33_binop_2,F,C))) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_bhsp_6,t141_xreal_1,t7_xboole_1,t8_xboole_1,t13_uniform1,d1_funct_2,t14_bhsp_5,d9_binop_2,l1_bhsp_7,t18_nat_1,t38_nat_1,t73_real_1,d1_zfmisc_1,s1_funct_2,s3_recdef_1,t7_xboole_1,t18_nat_1,t1_xboole_1,s1_nat_1,d1_xboole_0,t7_xboole_1,t63_xboole_1,t19_nat_1,t8_xreal_1,d5_real_1,t7_xboole_1,t38_nat_1,t1_xboole_1,s1_nat_1,t14_finset_1,d2_xboole_0,t8_xboole_1,s1_nat_1,d3_tarski,d5_funct_1,d1_zfmisc_1,t4_funct_2,s1_funct_2,t73_real_1,l2_bhsp_7,t7_absvalue,t36_xboole_1,t39_xboole_1,t12_xboole_1,t1_xboole_1,t79_xboole_1,d1_funct_2,t14_bhsp_5,d9_binop_2,t2_xreal_1,t138_complex1,t218_xreal_1,t2_xreal_1,t36_xboole_1,t39_xboole_1,t12_xboole_1,t1_xboole_1,t79_xboole_1,d1_funct_2,t14_bhsp_5,d9_binop_2,t2_xreal_1,t10_xreal_1,t36_xboole_1,t39_xboole_1,t12_xboole_1,t1_xboole_1,t79_xboole_1,t36_xboole_1,t39_xboole_1,t12_xboole_1,t1_xboole_1,t79_xboole_1,t2_xreal_1,t2_xreal_1,t10_xreal_1,d1_funct_2,t14_bhsp_5,d9_binop_2,d1_funct_2,t14_bhsp_5,d9_binop_2,t143_complex1,t2_xreal_1,t58_seq_4,d6_seq_2,d1_xreal_0,t73_real_1,l3_bhsp_7,t13_uniform1,t10_xreal_1,t36_xboole_1,t39_xboole_1,t12_xboole_1,t1_xboole_1,t79_xboole_1,t2_xreal_1,d1_funct_2,t14_bhsp_5,d9_binop_2,t21_absvalue,t13_uniform1,t10_xreal_1,t2_xreal_1,d6_bhsp_6]), [file(bhsp_7,t1_bhsp_7),interesting(0.45)]). fof(t3_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( ( v1_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v2_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v1_setwiseo(u1_rlvect_1(A),u1_struct_0(A)) ) => ! [B] : ( ( v1_finset_1(B) & m1_bhsp_5(B,A) ) => ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),k6_supinf_1) & m2_relset_1(C,u1_struct_0(A),k6_supinf_1) ) => ( ( r1_tarski(B,k1_relat_1(C)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,B) => k8_funct_2(u1_struct_0(A),k6_supinf_1,C,D) = k2_bhsp_1(A,D,D) ) ) ) => k2_bhsp_1(A,k1_bhsp_6(A,B),k1_bhsp_6(A,B)) = k5_bhsp_5(k1_numbers,u1_struct_0(A),k33_binop_2,B,C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t35_funct_1,d1_funct_2,t1_bhsp_6,t35_funct_1,t2_bhsp_7]), [file(bhsp_7,t3_bhsp_7),interesting(0.15)]). fof(t93_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k8_square_1(A),0) ) ) ), file(square_1,t93_square_1), [interesting(0.00)]). fof(t1_chain_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,A) & ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,A) & ~ r1_xreal_0(B,C) ) ) ) ) ) ), file(chain_1,t1_chain_1), [interesting(0.00)]). fof(t78_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(B,A) & r1_xreal_0(k5_square_1(B),k5_square_1(A)) ) ) ) ), file(square_1,t78_square_1), [interesting(0.00)]). fof(d4_square_1,definition,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(0,A) => ! [B] : ( v1_xreal_0(B) => ( B = k8_square_1(A) <=> ( r1_xreal_0(0,B) & k5_square_1(B) = A ) ) ) ) ) ), file(square_1,d4_square_1), [interesting(0.00)]). fof(t10_bhsp_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( ( v1_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v2_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v1_setwiseo(u1_rlvect_1(A),u1_struct_0(A)) & v4_bhsp_3(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v1_bhsp_6(B,A) <=> ! [C] : ( m1_subset_1(C,k1_numbers) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( ( v1_finset_1(D) & m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(D) & r1_tarski(D,B) & ! [E] : ( ( v1_finset_1(E) & m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(E) & r1_tarski(E,B) & r1_xboole_0(D,E) & r1_xreal_0(C,k3_bhsp_1(A,k1_bhsp_6(A,E))) ) ) ) ) ) ) ) ) ) ) ), file(bhsp_6,t10_bhsp_6), [interesting(0.00)]). fof(t34_bhsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_xreal_0(0,k3_bhsp_1(A,B)) ) ) ), file(bhsp_1,t34_bhsp_1), [interesting(0.00)]). fof(t2_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(A,B) & r1_xreal_0(B,C) ) => r1_xreal_0(A,C) ) ) ) ) ), file(xreal_1,t2_xreal_1), [interesting(0.00)]). fof(d9_bhsp_5,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( m2_bhsp_5(B,A) <=> ( m1_bhsp_5(B,A) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_hidden(C,B) => k2_bhsp_1(A,C,C) = 1 ) ) ) ) ) ) ), file(bhsp_5,d9_bhsp_5), [interesting(0.00)]). fof(d8_bhsp_5,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( m1_bhsp_5(B,A) <=> ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( ( r2_hidden(C,B) & r2_hidden(D,B) ) => ( C = D | k2_bhsp_1(A,C,D) = 0 ) ) ) ) ) ) ) ), file(bhsp_5,d8_bhsp_5), [interesting(0.00)]). fof(t1_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(B,C) ) => r1_tarski(A,C) ) ), file(xboole_1,t1_xboole_1), [interesting(0.00)]). fof(t35_funct_1,theorem,( ! [A,B] : ( r2_hidden(B,A) => k1_funct_1(k6_relat_1(A),B) = B ) ), file(funct_1,t35_funct_1), [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(t1_bhsp_6,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( ( v1_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v2_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v1_setwiseo(u1_rlvect_1(A),u1_struct_0(A)) ) => ! [B] : ( ( v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) => ( ( r1_tarski(B,k4_relset_1(u1_struct_0(A),u1_struct_0(A),C)) & ! [D] : ( r2_hidden(D,k4_relset_1(u1_struct_0(A),u1_struct_0(A),C)) => k1_funct_1(C,D) = D ) ) => k1_bhsp_6(A,B) = k5_bhsp_5(u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C) ) ) ) ) ) ), file(bhsp_6,t1_bhsp_6), [interesting(0.00)]). fof(d5_bhsp_5,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [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) ) => ( ( v1_binop_1(C,A) & v2_binop_1(C,A) & v1_setwiseo(C,A) ) => ! [D] : ( ( v1_finset_1(D) & m1_subset_1(D,k1_zfmisc_1(B)) ) => ! [E] : ( ( v1_funct_1(E) & v1_funct_2(E,B,A) & m2_relset_1(E,B,A) ) => ( r1_tarski(D,k1_relat_1(E)) => ! [F] : ( m1_subset_1(F,A) => ( F = k5_bhsp_5(A,B,C,D,E) <=> ? [G] : ( m2_finseq_1(G,B) & v2_funct_1(G) & k2_relat_1(G) = D & F = k2_finsop_1(A,k4_bhsp_5(A,B,E,G),C) ) ) ) ) ) ) ) ) ) ) ), file(bhsp_5,d5_bhsp_5), [interesting(0.00)]). fof(d1_bhsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_bhsp_1(A,B,C) = k8_funct_2(k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),k1_numbers,u1_bhsp_1(A),k1_domain_1(u1_struct_0(A),u1_struct_0(A),B,C)) ) ) ) ), file(bhsp_1,d1_bhsp_1), [interesting(0.00)]). fof(t9_bhsp_5,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( ( ~ v1_xboole_0(B) & v1_finset_1(B) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) => ( ( r1_tarski(B,k1_relat_1(C)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r2_hidden(D,B) & r2_hidden(E,B) ) => ( D = E | k1_funct_1(u1_bhsp_1(A),k4_tarski(k1_funct_1(C,D),k1_funct_1(C,E))) = 0 ) ) ) ) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),k1_numbers) & m2_relset_1(D,u1_struct_0(A),k1_numbers) ) => ( ( r1_tarski(B,k1_relat_1(D)) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(E,B) => k1_funct_1(D,E) = k1_funct_1(u1_bhsp_1(A),k4_tarski(k1_funct_1(C,E),k1_funct_1(C,E))) ) ) ) => ! [E] : ( m2_finseq_1(E,u1_struct_0(A)) => ( ( v2_funct_1(E) & k2_relat_1(E) = B ) => k1_funct_1(u1_bhsp_1(A),k4_tarski(k2_finsop_1(u1_struct_0(A),k4_bhsp_5(u1_struct_0(A),u1_struct_0(A),C,E),u1_rlvect_1(A)),k2_finsop_1(u1_struct_0(A),k4_bhsp_5(u1_struct_0(A),u1_struct_0(A),C,E),u1_rlvect_1(A)))) = k2_finsop_1(k1_numbers,k4_bhsp_5(k1_numbers,u1_struct_0(A),D,E),k33_binop_2) ) ) ) ) ) ) ) ) ), file(bhsp_5,t9_bhsp_5), [interesting(0.00)]). fof(t2_bhsp_7,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ( ( v1_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v2_binop_1(u1_rlvect_1(A),u1_struct_0(A)) & v1_setwiseo(u1_rlvect_1(A),u1_struct_0(A)) ) => ! [B] : ( ( v1_finset_1(B) & m1_bhsp_5(B,A) ) => ( ~ v1_xboole_0(B) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),u1_struct_0(A)) & m2_relset_1(C,u1_struct_0(A),u1_struct_0(A)) ) => ( ( r1_tarski(B,k1_relat_1(C)) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_hidden(D,B) => k8_funct_2(u1_struct_0(A),u1_struct_0(A),C,D) = D ) ) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,u1_struct_0(A),k1_numbers) & m2_relset_1(D,u1_struct_0(A),k1_numbers) ) => ( ( r1_tarski(B,k1_relat_1(D)) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(E,B) => k8_funct_2(u1_struct_0(A),k1_numbers,D,E) = k2_bhsp_1(A,E,E) ) ) ) => k2_bhsp_1(A,k5_bhsp_5(u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C),k5_bhsp_5(u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C)) = k5_bhsp_5(k1_numbers,u1_struct_0(A),k33_binop_2,B,D) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_bhsp_5,d5_bhsp_5,d8_bhsp_5,d1_bhsp_1,d1_bhsp_1,t9_bhsp_5,d1_bhsp_1]), [file(bhsp_7,t2_bhsp_7),interesting(0.00)]). fof(d4_bhsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_bhsp_1(A,B) = k9_square_1(k2_bhsp_1(A,B,B)) ) ) ), file(bhsp_1,d4_bhsp_1), [interesting(0.00)]). fof(d2_bhsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_bhsp_1(A) ) => ( v2_bhsp_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_numbers) => ( ( k1_bhsp_1(A,B,B) = 0 => B = k1_rlvect_1(A) ) & ( B = k1_rlvect_1(A) => k1_bhsp_1(A,B,B) = 0 ) & r1_xreal_0(0,k1_bhsp_1(A,B,B)) & k1_bhsp_1(A,B,C) = k1_bhsp_1(A,C,B) & k1_bhsp_1(A,k2_rlvect_1(A,B,C),D) = k3_real_1(k1_bhsp_1(A,B,D),k1_bhsp_1(A,C,D)) & k1_bhsp_1(A,k3_rlvect_1(A,B,E),C) = k4_real_1(E,k1_bhsp_1(A,B,C)) ) ) ) ) ) ) ) ), file(bhsp_1,d2_bhsp_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(d6_bhsp_6,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),k6_supinf_1) & m2_relset_1(C,u1_struct_0(A),k6_supinf_1) ) => ( r1_bhsp_6(A,B,C) <=> ? [D] : ( m1_subset_1(D,k1_numbers) & ! [E] : ( m1_subset_1(E,k1_numbers) => ~ ( ~ r1_xreal_0(E,0) & ! [F] : ( ( v1_finset_1(F) & m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(F) & r1_tarski(F,B) & ! [G] : ( ( v1_finset_1(G) & m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( r1_tarski(F,G) & r1_tarski(G,B) & r1_xreal_0(E,k18_complex1(k10_binop_2(D,k5_bhsp_5(k1_numbers,u1_struct_0(A),k33_binop_2,G,C)))) ) ) ) ) ) ) ) ) ) ) ) ), file(bhsp_6,d6_bhsp_6), [interesting(0.00)]). fof(t141_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t141_xreal_1), [interesting(0.00)]). fof(t7_xboole_1,theorem,( ! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) ), file(xboole_1,t7_xboole_1), [interesting(0.00)]). fof(t8_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_tarski(C,B) ) => r1_tarski(k2_xboole_0(A,C),B) ) ), file(xboole_1,t8_xboole_1), [interesting(0.00)]). fof(t13_uniform1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => k18_complex1(k5_real_1(A,B)) = k18_complex1(k5_real_1(B,A)) ) ) ), file(uniform1,t13_uniform1), [interesting(0.00)]). fof(t14_bhsp_5,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( ~ v1_xboole_0(B) => ! [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) ) => ( ( v1_binop_1(C,A) & v2_binop_1(C,A) & v1_setwiseo(C,A) ) => ! [D] : ( ( v1_finset_1(D) & m1_subset_1(D,k1_zfmisc_1(B)) ) => ! [E] : ( ( v1_finset_1(E) & m1_subset_1(E,k1_zfmisc_1(B)) ) => ( r1_xboole_0(D,E) => ! [F] : ( ( v1_funct_1(F) & v1_funct_2(F,B,A) & m2_relset_1(F,B,A) ) => ( ( r1_tarski(D,k1_relat_1(F)) & r1_tarski(E,k1_relat_1(F)) ) => ! [G] : ( ( v1_finset_1(G) & m1_subset_1(G,k1_zfmisc_1(B)) ) => ( G = k2_xboole_0(D,E) => k5_bhsp_5(A,B,C,G,F) = k2_binop_1(A,A,A,C,k5_bhsp_5(A,B,C,D,F),k5_bhsp_5(A,B,C,E,F)) ) ) ) ) ) ) ) ) ) ) ) ), file(bhsp_5,t14_bhsp_5), [interesting(0.00)]). fof(d9_binop_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) ) => ( A = k33_binop_2 <=> ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,A,B,C) = k9_binop_2(B,C) ) ) ) ) ), file(binop_2,d9_binop_2), [interesting(0.00)]). fof(t142_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => r1_xreal_0(k17_complex1(k2_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ), file(complex1,t142_complex1), [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(t18_nat_1,theorem,( ! [A] : ( v4_ordinal2(A) => r1_xreal_0(0,A) ) ), file(nat_1,t18_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(t73_real_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ~ r1_xreal_0(A,0) => ( ~ ( ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) ) & ~ ( ~ r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) & r1_xreal_0(C,B) ) ) ) ) ) ) ), file(real_1,t73_real_1), [interesting(0.00)]). fof(d1_zfmisc_1,definition,( ! [A,B] : ( B = k1_zfmisc_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> r1_tarski(C,A) ) ) ), file(zfmisc_1,d1_zfmisc_1), [interesting(0.00)]). fof(s1_funct_2,theorem, ( ! [A] : ~ ( r2_hidden(A,f1_s1_funct_2) & ! [B] : ~ ( r2_hidden(B,f2_s1_funct_2) & p1_s1_funct_2(A,B) ) ) => ? [A] : ( v1_funct_1(A) & v1_funct_2(A,f1_s1_funct_2,f2_s1_funct_2) & m2_relset_1(A,f1_s1_funct_2,f2_s1_funct_2) & ! [B] : ( r2_hidden(B,f1_s1_funct_2) => p1_s1_funct_2(B,k1_funct_1(A,B)) ) ) ), file(funct_2,s1_funct_2), [interesting(0.00)]). fof(s3_recdef_1,theorem,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & k1_relat_1(A) = k5_numbers & k1_funct_1(A,0) = f1_s3_recdef_1 & ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => k1_funct_1(A,k1_nat_1(B,1)) = f2_s3_recdef_1(B,k1_funct_1(A,B)) ) ) ), file(recdef_1,s3_recdef_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(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [interesting(0.00)]). fof(t63_xboole_1,theorem,( ! [A,B,C] : ( ( r1_tarski(A,B) & r1_xboole_0(B,C) ) => r1_xboole_0(A,C) ) ), file(xboole_1,t63_xboole_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(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(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(t14_finset_1,theorem,( ! [A,B] : ( ( v1_finset_1(A) & v1_finset_1(B) ) => v1_finset_1(k2_xboole_0(A,B)) ) ), file(finset_1,t14_finset_1), [interesting(0.00)]). fof(d2_xboole_0,definition,( ! [A,B,C] : ( C = k2_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) | r2_hidden(D,B) ) ) ) ), file(xboole_0,d2_xboole_0), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(t4_funct_2,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r1_tarski(k2_relat_1(B),A) => ( v1_funct_1(B) & v1_funct_2(B,k1_relat_1(B),A) & m2_relset_1(B,k1_relat_1(B),A) ) ) ) ), file(funct_2,t4_funct_2), [interesting(0.00)]). fof(t124_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(k5_xcmplx_0(A),0) ) & ~ ( ~ r1_xreal_0(k5_xcmplx_0(A),0) & r1_xreal_0(A,0) ) ) ) ), file(xreal_1,t124_xreal_1), [interesting(0.00)]). fof(t10_seq_4,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ! [B] : ( m2_subset_1(B,k1_numbers,k5_numbers) => r1_xreal_0(B,A) ) ) ), file(seq_4,t10_seq_4), [interesting(0.00)]). fof(t78_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k7_xcmplx_0(A,B),k7_xcmplx_0(A,C)) ) ) ) ) ), file(xreal_1,t78_xreal_1), [interesting(0.00)]). fof(t218_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k7_xcmplx_0(1,k5_xcmplx_0(A)) = A ) ), file(xcmplx_1,t218_xcmplx_1), [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(t36_xboole_1,theorem,( ! [A,B] : r1_tarski(k4_xboole_0(A,B),A) ), file(xboole_1,t36_xboole_1), [interesting(0.00)]). fof(t39_xboole_1,theorem,( ! [A,B] : k2_xboole_0(A,k4_xboole_0(B,A)) = k2_xboole_0(A,B) ), file(xboole_1,t39_xboole_1), [interesting(0.00)]). fof(t12_xboole_1,theorem,( ! [A,B] : ( r1_tarski(A,B) => k2_xboole_0(A,B) = B ) ), file(xboole_1,t12_xboole_1), [interesting(0.00)]). fof(t79_xboole_1,theorem,( ! [A,B] : r1_xboole_0(k4_xboole_0(A,B),B) ), file(xboole_1,t79_xboole_1), [interesting(0.00)]). fof(t138_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ), file(complex1,t138_complex1), [interesting(0.00)]). fof(t218_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ~ ( ~ r1_xreal_0(A,0) & r1_xreal_0(A,k7_xcmplx_0(A,2)) ) ) ), file(xreal_1,t218_xreal_1), [interesting(0.00)]). fof(t143_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => r1_xreal_0(k17_complex1(k6_xcmplx_0(A,B)),k3_real_1(k17_complex1(A),k17_complex1(B))) ) ) ), file(complex1,t143_complex1), [interesting(0.00)]). fof(t58_seq_4,theorem,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) <=> ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(B,0) & ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ? [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) & r1_xreal_0(C,D) & r1_xreal_0(B,k18_complex1(k5_real_1(k8_funct_2(k5_numbers,k1_numbers,A,D),k8_funct_2(k5_numbers,k1_numbers,A,C)))) ) ) ) ) ) ) ), file(seq_4,t58_seq_4), [interesting(0.00)]). fof(d6_seq_2,definition,( ! [A] : ( ( v1_funct_1(A) & v1_funct_2(A,k5_numbers,k1_numbers) & m2_relset_1(A,k5_numbers,k1_numbers) ) => ( v4_seq_2(A) <=> ? [B] : ( v1_xreal_0(B) & ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(C,0) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => ? [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) & r1_xreal_0(D,E) & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ), file(seq_2,d6_seq_2), [interesting(0.00)]). fof(d1_xreal_0,definition,( ! [A] : ( v1_xreal_0(A) <=> r2_hidden(A,k1_numbers) ) ), file(xreal_0,d1_xreal_0), [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(t21_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ! [D] : ( v1_xreal_0(D) => ( ( r1_xreal_0(k18_complex1(A),B) & r1_xreal_0(k18_complex1(C),D) ) => r1_xreal_0(k18_complex1(k2_xcmplx_0(A,C)),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(absvalue,t21_absvalue), [interesting(0.00)]). fof(t131_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) & r1_xreal_0(k3_xcmplx_0(A,B),0) ) ) ) ), file(xreal_1,t131_xreal_1), [interesting(0.00)]). fof(t11_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(k1_real_1(k18_complex1(A)),A) & r1_xreal_0(A,k18_complex1(A)) ) ) ), file(absvalue,t11_absvalue), [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(t50_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) => r1_xreal_0(0,k6_xcmplx_0(B,A)) ) ) ) ), file(xreal_1,t50_xreal_1), [interesting(0.00)]). fof(t72_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => r1_xreal_0(0,k5_square_1(A)) ) ), file(square_1,t72_square_1), [interesting(0.00)]). fof(t95_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( r1_xreal_0(0,A) & ~ r1_xreal_0(B,A) & r1_xreal_0(k8_square_1(B),k8_square_1(A)) ) ) ) ), file(square_1,t95_square_1), [interesting(0.00)]). fof(t89_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( r1_xreal_0(0,A) => k8_square_1(k5_square_1(A)) = A ) ) ), file(square_1,t89_square_1), [interesting(0.00)]). fof(t121_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) | ( r1_xreal_0(A,0) & r1_xreal_0(B,0) ) ) => r1_xreal_0(0,k3_xcmplx_0(A,B)) ) ) ) ), file(real_2,t121_real_2), [interesting(0.00)]). fof(t127_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ~ ( ( ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(B,0) ) | ( ~ r1_xreal_0(0,A) & ~ r1_xreal_0(0,B) ) ) & r1_xreal_0(k7_xcmplx_0(A,B),0) ) ) ) ), file(real_2,t127_real_2), [interesting(0.00)]). fof(d3_bhsp_6,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v1_bhsp_6(B,A) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( C = k2_bhsp_6(A,B) <=> ! [D] : ( m1_subset_1(D,k1_numbers) => ~ ( ~ r1_xreal_0(D,0) & ! [E] : ( ( v1_finset_1(E) & m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(E) & r1_tarski(E,B) & ! [F] : ( ( v1_finset_1(F) & m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( r1_tarski(E,F) & r1_tarski(F,B) & r1_xreal_0(D,k3_bhsp_1(A,k6_rlvect_1(A,C,k1_bhsp_6(A,F)))) ) ) ) ) ) ) ) ) ) ) ) ), file(bhsp_6,d3_bhsp_6), [interesting(0.00)]). fof(t17_bhsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_bhsp_1(A,B,k6_rlvect_1(A,C,D)) = k5_real_1(k2_bhsp_1(A,B,C),k2_bhsp_1(A,B,D)) ) ) ) ) ), file(bhsp_1,t17_bhsp_1), [interesting(0.00)]). fof(t16_bhsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_bhsp_1(A,k6_rlvect_1(A,B,C),D) = k5_real_1(k2_bhsp_1(A,B,D),k2_bhsp_1(A,C,D)) ) ) ) ) ), file(bhsp_1,t16_bhsp_1), [interesting(0.00)]). fof(t35_bhsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_xreal_0(k18_complex1(k2_bhsp_1(A,B,C)),k4_real_1(k3_bhsp_1(A,B),k3_bhsp_1(A,C))) ) ) ) ), file(bhsp_1,t35_bhsp_1), [interesting(0.00)]). fof(t9_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(A,B) & r1_xreal_0(C,D) ) => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ), file(xreal_1,t9_xreal_1), [interesting(0.00)]). fof(t37_bhsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_bhsp_1(A,k5_rlvect_1(A,B)) = k3_bhsp_1(A,B) ) ) ), file(bhsp_1,t37_bhsp_1), [interesting(0.00)]). fof(t27_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k6_rlvect_1(A,k1_rlvect_1(A),B) = k5_rlvect_1(A,B) ) ) ), file(rlvect_1,t27_rlvect_1), [interesting(0.00)]). fof(t16_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & l1_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( k2_rlvect_1(A,B,k5_rlvect_1(A,B)) = k1_rlvect_1(A) & k2_rlvect_1(A,k5_rlvect_1(A,B),B) = k1_rlvect_1(A) ) ) ) ), file(rlvect_1,t16_rlvect_1), [interesting(0.00)]). fof(d6_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_rlvect_1(A) ) => ( v4_rlvect_1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) ) ) ), file(rlvect_1,d6_rlvect_1), [interesting(0.00)]). fof(t36_bhsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_xreal_0(k3_bhsp_1(A,k4_rlvect_1(A,B,C)),k3_real_1(k3_bhsp_1(A,B),k3_bhsp_1(A,C))) ) ) ) ), file(bhsp_1,t36_bhsp_1), [interesting(0.00)]). fof(t11_xboole_1,theorem,( ! [A,B,C] : ( r1_tarski(k2_xboole_0(A,B),C) => r1_tarski(A,C) ) ), file(xboole_1,t11_xboole_1), [interesting(0.00)]). fof(t66_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(0,C) ) => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ), file(xreal_1,t66_xreal_1), [interesting(0.00)]). fof(t70_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ~ ( ~ r1_xreal_0(A,0) & ~ r1_xreal_0(C,B) & r1_xreal_0(k3_xcmplx_0(C,A),k3_xcmplx_0(B,A)) ) ) ) ) ), file(xreal_1,t70_xreal_1), [interesting(0.00)]). fof(t88_xcmplx_1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ( A != 0 => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ), file(xcmplx_1,t88_xcmplx_1), [interesting(0.00)]). fof(d7_bhsp_6,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(A) & v4_rlvect_1(A) & v5_rlvect_1(A) & v6_rlvect_1(A) & v7_rlvect_1(A) & v2_bhsp_1(A) & l1_bhsp_1(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,u1_struct_0(A),k6_supinf_1) & m2_relset_1(C,u1_struct_0(A),k6_supinf_1) ) => ( r1_bhsp_6(A,B,C) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( D = k3_bhsp_6(A,B,C) <=> ! [E] : ( m1_subset_1(E,k1_numbers) => ~ ( ~ r1_xreal_0(E,0) & ! [F] : ( ( v1_finset_1(F) & m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( ~ v1_xboole_0(F) & r1_tarski(F,B) & ! [G] : ( ( v1_finset_1(G) & m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) ) => ~ ( r1_tarski(F,G) & r1_tarski(G,B) & r1_xreal_0(E,k18_complex1(k10_binop_2(D,k5_bhsp_5(k1_numbers,u1_struct_0(A),k33_binop_2,G,C)))) ) ) ) ) ) ) ) ) ) ) ) ) ), file(bhsp_6,d7_bhsp_6), [interesting(0.00)]). fof(t133_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => ( ~ ( A != 0 & r1_xreal_0(k17_complex1(A),0) ) & ~ ( ~ r1_xreal_0(k17_complex1(A),0) & A = 0 ) ) ) ), file(complex1,t133_complex1), [interesting(0.00)]).