fof(t39_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(k5_real_1(k3_bhsp_1(A,B),k3_bhsp_1(A,C))),k3_bhsp_1(A,k6_rlvect_1(A,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t38_bhsp_1,t43_rlvect_1,t28_rlvect_1,t26_rlvect_1,t36_bhsp_1,t22_xreal_1,t47_rlvect_1,t37_bhsp_1,t26_xreal_1,t12_absvalue]), [file(bhsp_1,t39_bhsp_1),interesting(1.00)]). fof(l6_bhsp_1,theorem,( r2_hidden(k1_rlvect_1(c1),u1_struct_0(k1_rlsub_1(c1))) ), inference(mizar_proof,[status(thm)],[l3_bhsp_1,d1_tarski]), [file(bhsp_1,l6_bhsp_1),interesting(0.96)]). fof(t38_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(k5_real_1(k3_bhsp_1(A,B),k3_bhsp_1(A,C)),k3_bhsp_1(A,k6_rlvect_1(A,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_rlvect_1,t28_rlvect_1,t26_rlvect_1,t36_bhsp_1,t22_xreal_1]), [file(bhsp_1,t38_bhsp_1),interesting(0.93)]). 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))) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_bhsp_1,d2_bhsp_1,t72_square_1,d2_bhsp_1,d2_bhsp_1,t89_square_1,t96_square_1,t21_bhsp_1,d4_square_1,d4_square_1,t35_bhsp_1,t11_absvalue,t2_xreal_1,t66_xreal_1,t9_xreal_1,t8_xreal_1,t34_bhsp_1,t34_bhsp_1,t9_xreal_1,t78_square_1]), [file(bhsp_1,t36_bhsp_1),interesting(0.88)]). fof(t42_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)) => r1_xreal_0(k5_bhsp_1(A,B,C),k3_real_1(k5_bhsp_1(A,B,D),k5_bhsp_1(A,D,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_rlvect_1,t28_rlvect_1,t43_rlvect_1,t43_rlvect_1,t41_rlvect_1,t47_rlvect_1,t36_bhsp_1]), [file(bhsp_1,t42_bhsp_1),interesting(0.83)]). fof(l3_bhsp_1,theorem,( u1_struct_0(k1_rlsub_1(c1)) = k6_domain_1(u1_struct_0(c1),k1_rlvect_1(c1)) ), inference(mizar_proof,[status(thm)],[d3_rlsub_1]), [file(bhsp_1,l3_bhsp_1),interesting(0.79)]). fof(l7_bhsp_1,theorem,( k1_funct_1(c2,k1_domain_1(u1_struct_0(c1),u1_struct_0(c1),k1_rlvect_1(c1),k1_rlvect_1(c1))) = 0 ), inference(mizar_proof,[status(thm)],[l6_bhsp_1,l5_bhsp_1]), [file(bhsp_1,l7_bhsp_1),interesting(0.76)]). fof(t50_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)) => r1_xreal_0(k5_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,D,C)),k3_real_1(k5_bhsp_1(A,C,B),k5_bhsp_1(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_rlvect_1,t47_rlvect_1,t36_bhsp_1,t37_bhsp_1]), [file(bhsp_1,t50_bhsp_1),interesting(0.76)]). fof(t48_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)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => r1_xreal_0(k5_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,D,E)),k3_real_1(k5_bhsp_1(A,B,D),k5_bhsp_1(A,C,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_rlvect_1,t41_rlvect_1,t41_rlvect_1,t43_rlvect_1,t36_bhsp_1,t37_bhsp_1]), [file(bhsp_1,t48_bhsp_1),interesting(0.75)]). fof(t47_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)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => r1_xreal_0(k5_bhsp_1(A,k4_rlvect_1(A,B,C),k4_rlvect_1(A,D,E)),k3_real_1(k5_bhsp_1(A,B,D),k5_bhsp_1(A,C,E))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_rlvect_1,d6_rlvect_1,t45_rlvect_1,d6_rlvect_1,d6_rlvect_1,d6_rlvect_1,t36_bhsp_1]), [file(bhsp_1,t47_bhsp_1),interesting(0.71)]). 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))) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_bhsp_1]), [file(bhsp_1,t35_bhsp_1),interesting(0.70)]). fof(t19_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)) => k2_bhsp_1(A,k1_rlvect_1(A),B) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t16_rlvect_1,d2_bhsp_1,t13_bhsp_1]), [file(bhsp_1,t19_bhsp_1),interesting(0.69)]). 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) ) ) ), inference(mizar_proof,[status(thm)],[d1_absvalue,t29_rlvect_1,t33_bhsp_1]), [file(bhsp_1,t37_bhsp_1),interesting(0.68)]). fof(t24_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(k9_square_1(k2_bhsp_1(A,B,B)),k9_square_1(k2_bhsp_1(A,C,C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_bhsp_1,d2_bhsp_1,t82_square_1,t7_absvalue,d2_bhsp_1,d2_bhsp_1,d1_xreal_0,d2_bhsp_1,t21_bhsp_1,d2_bhsp_1,d2_bhsp_1,d2_bhsp_1,t72_square_1,t132_complex1,d2_bhsp_1,t10_quin_1,d1_quin_1,t177_real_2,t52_xreal_1,t161_complex1,t94_square_1,t89_square_1,t97_square_1]), [file(bhsp_1,t24_bhsp_1),interesting(0.67)]). fof(t29_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_bhsp_1(A,B,k1_rlvect_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[t19_bhsp_1,d3_bhsp_1]), [file(bhsp_1,t29_bhsp_1),interesting(0.65)]). 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)) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,d4_square_1]), [file(bhsp_1,t34_bhsp_1),interesting(0.62)]). fof(t6_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) ) => k2_bhsp_1(A,k1_rlvect_1(A),k1_rlvect_1(A)) = 0 ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1]), [file(bhsp_1,t6_bhsp_1),interesting(0.56)]). fof(t33_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => k3_bhsp_1(B,k3_rlvect_1(B,C,A)) = k4_real_1(k18_complex1(A),k3_bhsp_1(B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t72_square_1,d2_bhsp_1,d2_bhsp_1,d2_bhsp_1,t97_square_1,t158_complex1]), [file(bhsp_1,t33_bhsp_1),interesting(0.55)]). fof(t41_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)) => k5_bhsp_1(A,B,B) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t28_rlvect_1,t32_bhsp_1]), [file(bhsp_1,t41_bhsp_1),interesting(0.55)]). fof(t69_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v5_seqm_3(B) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,B,C) = k1_funct_1(B,k3_real_1(C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t68_bhsp_1,t22_normsp_1,t23_normsp_1,t24_normsp_1,d4_normsp_1]), [file(bhsp_1,t69_bhsp_1),interesting(0.55)]). fof(t20_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)) => k2_bhsp_1(A,B,k1_rlvect_1(A)) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t19_bhsp_1]), [file(bhsp_1,t20_bhsp_1),interesting(0.52)]). fof(t68_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v5_seqm_3(B) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k2_normsp_1(A,B,C) = k1_funct_1(B,k3_real_1(C,1)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_normsp_1,t21_normsp_1,t22_normsp_1,t23_normsp_1,t24_normsp_1,d4_normsp_1]), [file(bhsp_1,t68_bhsp_1),interesting(0.52)]). fof(t70_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v5_seqm_3(B) <=> ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,B,C) = k2_normsp_1(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t69_bhsp_1,t23_normsp_1,t24_normsp_1,d4_normsp_1]), [file(bhsp_1,t70_bhsp_1),interesting(0.50)]). fof(t21_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)) => k2_bhsp_1(A,k4_rlvect_1(A,B,C),k4_rlvect_1(A,B,C)) = k3_real_1(k3_real_1(k2_bhsp_1(A,B,B),k4_real_1(2,k2_bhsp_1(A,B,C))),k2_bhsp_1(A,C,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,d2_bhsp_1,d2_bhsp_1]), [file(bhsp_1,t21_bhsp_1),interesting(0.45)]). fof(t10_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & v2_bhsp_1(C) & l1_bhsp_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k2_bhsp_1(C,k4_rlvect_1(C,k3_rlvect_1(C,D,A),k3_rlvect_1(C,E,B)),F) = k3_real_1(k4_real_1(A,k2_bhsp_1(C,D,F)),k4_real_1(B,k2_bhsp_1(C,E,F))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,d2_bhsp_1,d2_bhsp_1]), [file(bhsp_1,t10_bhsp_1),interesting(0.44)]). fof(t76_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k6_normsp_1(A,B,1) = B ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,d9_rlvect_1,t113_funct_2]), [file(bhsp_1,t76_bhsp_1),interesting(0.38)]). fof(t23_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)) => k2_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,B,C)) = k3_real_1(k5_real_1(k2_bhsp_1(A,B,B),k4_real_1(2,k2_bhsp_1(A,B,C))),k2_bhsp_1(A,C,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_bhsp_1,t17_bhsp_1,t17_bhsp_1]), [file(bhsp_1,t23_bhsp_1),interesting(0.37)]). fof(t71_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,B,C) = k8_bhsp_1(A,B,k6_bhsp_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,d10_bhsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t71_bhsp_1),interesting(0.28)]). fof(t11_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & v2_bhsp_1(C) & l1_bhsp_1(C) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(C)) => ! [E] : ( m1_subset_1(E,u1_struct_0(C)) => ! [F] : ( m1_subset_1(F,u1_struct_0(C)) => k2_bhsp_1(C,D,k4_rlvect_1(C,k3_rlvect_1(C,E,A),k3_rlvect_1(C,F,B))) = k3_real_1(k4_real_1(A,k2_bhsp_1(C,D,E)),k4_real_1(B,k2_bhsp_1(C,D,F))) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_bhsp_1]), [file(bhsp_1,t11_bhsp_1),interesting(0.22)]). fof(t73_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(B)) & m2_relset_1(C,k5_numbers,u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(B)) & m2_relset_1(D,k5_numbers,u1_struct_0(B)) ) => k6_normsp_1(B,k8_bhsp_1(B,C,D),A) = k8_bhsp_1(B,k6_normsp_1(B,C,A),k6_normsp_1(B,D,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,d5_normsp_1,d9_rlvect_1,d8_normsp_1,d8_normsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t73_bhsp_1),interesting(0.22)]). fof(t74_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & v2_bhsp_1(C) & l1_bhsp_1(C) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(C)) & m2_relset_1(D,k5_numbers,u1_struct_0(C)) ) => k6_normsp_1(C,D,k3_real_1(A,B)) = k8_bhsp_1(C,k6_normsp_1(C,D,A),k6_normsp_1(C,D,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,d9_rlvect_1,d8_normsp_1,d8_normsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t74_bhsp_1),interesting(0.19)]). fof(t19_rlsub_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) & l2_rlvect_1(A) ) => ! [B] : ( m1_rlsub_1(B,A) => k1_rlvect_1(B) = k1_rlvect_1(A) ) ) ), file(rlsub_1,t19_rlsub_1), [interesting(0.00)]). fof(d3_rlsub_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) & l2_rlvect_1(A) ) => ! [B] : ( ( v2_rlvect_1(B) & m1_rlsub_1(B,A) ) => ( B = k1_rlsub_1(A) <=> u1_struct_0(B) = k1_struct_0(A,k1_rlvect_1(A)) ) ) ) ), file(rlsub_1,d3_rlsub_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(t13_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(B,A) => k1_funct_1(k2_funcop_1(A,C),B) = C ) ), file(funcop_1,t13_funcop_1), [interesting(0.00)]). fof(l5_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k1_rlsub_1(c1))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k1_rlsub_1(c1))) => k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),A,B)) = 0 ) ) ), inference(mizar_proof,[status(thm)],[t13_funcop_1]), [file(bhsp_1,l5_bhsp_1),interesting(0.00)]). fof(l8_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k1_rlsub_1(c1))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k1_rlsub_1(c1))) => k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),A,B)) = k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),B,A)) ) ) ), inference(mizar_proof,[status(thm)],[l3_bhsp_1,d1_tarski]), [file(bhsp_1,l8_bhsp_1),interesting(0.00)]). fof(l9_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k1_rlsub_1(c1))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k1_rlsub_1(c1))) => ! [C] : ( m1_subset_1(C,u1_struct_0(k1_rlsub_1(c1))) => k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),k4_rlvect_1(k1_rlsub_1(c1),A,B),C)) = k3_real_1(k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),A,C)),k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[l3_bhsp_1,d1_tarski,l3_bhsp_1,l7_bhsp_1,d1_tarski]), [file(bhsp_1,l9_bhsp_1),interesting(0.00)]). fof(l10_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(k1_rlsub_1(c1))) => ! [B] : ( m1_subset_1(B,u1_struct_0(k1_rlsub_1(c1))) => ! [C] : ( m1_subset_1(C,k1_numbers) => k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),k3_rlvect_1(k1_rlsub_1(c1),A,C),B)) = k4_real_1(C,k8_funct_2(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers,c2,k1_domain_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1)),A,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[l3_bhsp_1,d1_tarski,l3_bhsp_1,l7_bhsp_1,d1_tarski]), [file(bhsp_1,l10_bhsp_1),interesting(0.00)]). fof(l11_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,u1_struct_0(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2))) => ! [B] : ( m1_subset_1(B,u1_struct_0(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2))) => ! [C] : ( m1_subset_1(C,u1_struct_0(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2))) => ! [D] : ( m1_subset_1(D,k1_numbers) => ( ( k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,A) = 0 => A = k1_rlvect_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2)) ) & ( A = k1_rlvect_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2)) => k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,A) = 0 ) & r1_xreal_0(0,k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,A)) & k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,B) = k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),B,A) & k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),k2_rlvect_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,B),C) = k3_real_1(k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,C),k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),B,C)) & k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),k3_rlvect_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,D),B) = k4_real_1(D,k1_bhsp_1(g1_bhsp_1(u1_struct_0(k1_rlsub_1(c1)),u2_struct_0(k1_rlsub_1(c1)),u1_rlvect_1(k1_rlsub_1(c1)),u2_rlvect_1(k1_rlsub_1(c1)),c2),A,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t19_rlsub_1,l3_bhsp_1,l7_bhsp_1,d1_tarski,t13_funcop_1,l8_bhsp_1,l9_bhsp_1,l10_bhsp_1]), [file(bhsp_1,l11_bhsp_1),interesting(0.00)]). fof(l2_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) & l2_rlvect_1(A) ) ), file(bhsp_1,l2_bhsp_1), [interesting(0.00)]). fof(t57_funcop_1,theorem,( ! [A,B,C] : ( r2_hidden(C,B) => ( v1_funct_1(k2_funcop_1(A,C)) & v1_funct_2(k2_funcop_1(A,C),A,B) & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ), file(funcop_1,t57_funcop_1), [interesting(0.00)]). fof(l4_bhsp_1,theorem, ( v1_funct_1(k2_funcop_1(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),0)) & v1_funct_2(k2_funcop_1(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),0),k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers) & m2_relset_1(k2_funcop_1(k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),0),k2_zfmisc_1(u1_struct_0(k1_rlsub_1(c1)),u1_struct_0(k1_rlsub_1(c1))),k1_numbers) ), inference(mizar_proof,[status(thm)],[t57_funcop_1]), [file(bhsp_1,l4_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(t29_rlvect_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) & l2_rlvect_1(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k5_rlvect_1(A,B) = k3_rlvect_1(A,B,k1_real_1(1)) ) ) ), file(rlvect_1,t29_rlvect_1), [interesting(0.00)]). fof(t12_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)) => k2_bhsp_1(A,k5_rlvect_1(A,B),C) = k2_bhsp_1(A,B,k5_rlvect_1(A,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_rlvect_1,d2_bhsp_1,d2_bhsp_1,t29_rlvect_1]), [file(bhsp_1,t12_bhsp_1),interesting(0.00)]). fof(t13_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)) => k2_bhsp_1(A,k5_rlvect_1(A,B),C) = k1_real_1(k2_bhsp_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t29_rlvect_1,d2_bhsp_1]), [file(bhsp_1,t13_bhsp_1),interesting(0.00)]). fof(t14_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)) => k2_bhsp_1(A,B,k5_rlvect_1(A,C)) = k1_real_1(k2_bhsp_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_bhsp_1]), [file(bhsp_1,t14_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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,t13_bhsp_1]), [file(bhsp_1,t16_bhsp_1),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)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,t13_bhsp_1]), [file(bhsp_1,t17_bhsp_1),interesting(0.00)]). fof(t18_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)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => k2_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,D,E)) = k3_real_1(k5_real_1(k5_real_1(k2_bhsp_1(A,B,D),k2_bhsp_1(A,B,E)),k2_bhsp_1(A,C,D)),k2_bhsp_1(A,C,E)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t16_bhsp_1,t17_bhsp_1,t17_bhsp_1]), [file(bhsp_1,t18_bhsp_1),interesting(0.00)]). fof(t1_bhsp_1,theorem,( $true ), file(bhsp_1,t1_bhsp_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(t22_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)) => k2_bhsp_1(A,k4_rlvect_1(A,B,C),k6_rlvect_1(A,B,C)) = k5_real_1(k2_bhsp_1(A,B,B),k2_bhsp_1(A,C,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,t17_bhsp_1,t17_bhsp_1]), [file(bhsp_1,t22_bhsp_1),interesting(0.00)]). fof(t25_bhsp_1,theorem,( $true ), file(bhsp_1,t25_bhsp_1), [interesting(0.00)]). fof(d3_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)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_bhsp_1(A,B,C) <=> k2_bhsp_1(A,B,C) = 0 ) ) ) ) ), file(bhsp_1,d3_bhsp_1), [interesting(0.00)]). fof(t26_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_bhsp_1(A,B,C) => r1_bhsp_1(A,B,k5_rlvect_1(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_1,t13_bhsp_1,d3_bhsp_1]), [file(bhsp_1,t26_bhsp_1),interesting(0.00)]). fof(t27_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_bhsp_1(A,B,C) => r1_bhsp_1(A,k5_rlvect_1(A,B),C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_1,t13_bhsp_1,d3_bhsp_1]), [file(bhsp_1,t27_bhsp_1),interesting(0.00)]). fof(t15_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)) => k2_bhsp_1(A,k5_rlvect_1(A,B),k5_rlvect_1(A,C)) = k2_bhsp_1(A,B,C) ) ) ) ), inference(mizar_proof,[status(thm)],[t13_bhsp_1,t13_bhsp_1]), [file(bhsp_1,t15_bhsp_1),interesting(0.00)]). fof(t28_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_bhsp_1(A,B,C) => r1_bhsp_1(A,k5_rlvect_1(A,B),k5_rlvect_1(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_1,t15_bhsp_1,d3_bhsp_1]), [file(bhsp_1,t28_bhsp_1),interesting(0.00)]). fof(t2_bhsp_1,theorem,( $true ), file(bhsp_1,t2_bhsp_1), [interesting(0.00)]). fof(t30_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_bhsp_1(A,B,C) => k2_bhsp_1(A,k4_rlvect_1(A,B,C),k4_rlvect_1(A,B,C)) = k3_real_1(k2_bhsp_1(A,B,B),k2_bhsp_1(A,C,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_1,t21_bhsp_1]), [file(bhsp_1,t30_bhsp_1),interesting(0.00)]). fof(t31_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_bhsp_1(A,B,C) => k2_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,B,C)) = k3_real_1(k2_bhsp_1(A,B,B),k2_bhsp_1(A,C,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d3_bhsp_1,t23_bhsp_1]), [file(bhsp_1,t31_bhsp_1),interesting(0.00)]). fof(t43_rlvect_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v3_rlvect_1(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)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k6_rlvect_1(A,C,D)) = k4_rlvect_1(A,k6_rlvect_1(A,B,C),D) ) ) ) ) ), file(rlvect_1,t43_rlvect_1), [interesting(0.00)]). fof(t28_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,B,B) = k1_rlvect_1(A) ) ) ), file(rlvect_1,t28_rlvect_1), [interesting(0.00)]). fof(t26_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,B,k1_rlvect_1(A)) = B ) ) ), file(rlvect_1,t26_rlvect_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(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(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(t96_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) & k8_square_1(A) = k8_square_1(B) ) => A = B ) ) ) ), file(square_1,t96_square_1), [interesting(0.00)]). fof(t82_square_1,theorem,( k9_square_1(0) = 0 ), file(square_1,t82_square_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(d1_xreal_0,definition,( ! [A] : ( v1_xreal_0(A) <=> r2_hidden(A,k1_numbers) ) ), file(xreal_0,d1_xreal_0), [interesting(0.00)]). fof(t132_complex1,theorem,( ! [A] : ( v1_xcmplx_0(A) => r1_xreal_0(0,k17_complex1(A)) ) ), file(complex1,t132_complex1), [interesting(0.00)]). fof(t10_quin_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(0,k2_xcmplx_0(k2_xcmplx_0(k3_xcmplx_0(A,k5_square_1(D)),k3_xcmplx_0(B,D)),C)) ) => ( r1_xreal_0(A,0) | r1_xreal_0(k1_quin_1(A,B,C),0) ) ) ) ) ) ), file(quin_1,t10_quin_1), [interesting(0.00)]). fof(d1_quin_1,definition,( ! [A] : ( v1_xcmplx_0(A) => ! [B] : ( v1_xcmplx_0(B) => ! [C] : ( v1_xcmplx_0(C) => k1_quin_1(A,B,C) = k6_xcmplx_0(k5_square_1(B),k3_xcmplx_0(k3_xcmplx_0(4,A),C)) ) ) ) ), file(quin_1,d1_quin_1), [interesting(0.00)]). fof(t177_real_2,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ! [C] : ( v1_xreal_0(C) => ( ( r1_xreal_0(k3_xcmplx_0(B,A),C) => ( r1_xreal_0(A,0) | r1_xreal_0(B,k7_xcmplx_0(C,A)) ) ) & ( r1_xreal_0(k3_xcmplx_0(B,A),C) => ( r1_xreal_0(0,A) | r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) & ( r1_xreal_0(C,k3_xcmplx_0(B,A)) => ( r1_xreal_0(A,0) | r1_xreal_0(k7_xcmplx_0(C,A),B) ) ) & ( r1_xreal_0(C,k3_xcmplx_0(B,A)) => ( r1_xreal_0(0,A) | r1_xreal_0(B,k7_xcmplx_0(C,A)) ) ) ) ) ) ) ), file(real_2,t177_real_2), [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(t161_complex1,theorem,( ! [A] : ( v1_xreal_0(A) => k7_square_1(k17_complex1(A)) = k5_square_1(A) ) ), file(complex1,t161_complex1), [interesting(0.00)]). fof(t94_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(A,B) ) => r1_xreal_0(k8_square_1(A),k8_square_1(B)) ) ) ) ), file(square_1,t94_square_1), [interesting(0.00)]). fof(t97_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(0,A) & r1_xreal_0(0,B) ) => k8_square_1(k3_xcmplx_0(A,B)) = k3_xcmplx_0(k8_square_1(A),k8_square_1(B)) ) ) ) ), file(square_1,t97_square_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(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(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(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(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(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(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(t47_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)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k2_rlvect_1(A,C,k5_rlvect_1(A,B)) ) ) ) ), file(rlvect_1,t47_rlvect_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(t158_complex1,theorem,( ! [A] : ( v1_xreal_0(A) => k8_square_1(k5_square_1(A)) = k17_complex1(A) ) ), file(complex1,t158_complex1), [interesting(0.00)]). fof(t26_xreal_1,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( r1_xreal_0(A,B) <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ), file(xreal_1,t26_xreal_1), [interesting(0.00)]). fof(t12_absvalue,theorem,( ! [A] : ( v1_xreal_0(A) => ! [B] : ( v1_xreal_0(B) => ( ( r1_xreal_0(k4_xcmplx_0(A),B) & r1_xreal_0(B,A) ) <=> r1_xreal_0(k18_complex1(B),A) ) ) ) ), file(absvalue,t12_absvalue), [interesting(0.00)]). fof(t3_bhsp_1,theorem,( $true ), file(bhsp_1,t3_bhsp_1), [interesting(0.00)]). fof(t40_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)) => k4_bhsp_1(A,B,C) = k4_bhsp_1(A,C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[t47_rlvect_1,t37_bhsp_1]), [file(bhsp_1,t40_bhsp_1),interesting(0.00)]). fof(t10_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,k1_rlvect_1(A)) = B & k2_rlvect_1(A,k1_rlvect_1(A),B) = B ) ) ) ), file(rlvect_1,t10_rlvect_1), [interesting(0.00)]). fof(t41_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)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k6_rlvect_1(A,B,k2_rlvect_1(A,C,D)) = k6_rlvect_1(A,k6_rlvect_1(A,B,D),C) ) ) ) ) ), file(rlvect_1,t41_rlvect_1), [interesting(0.00)]). fof(t92_square_1,theorem,( ! [A] : ( v1_xreal_0(A) => ( ( r1_xreal_0(0,A) & k8_square_1(A) = 0 ) => A = 0 ) ) ), file(square_1,t92_square_1), [interesting(0.00)]). fof(t32_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,B) = 0 <=> B = k1_rlvect_1(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,t92_square_1,d2_bhsp_1,d2_bhsp_1,t82_square_1]), [file(bhsp_1,t32_bhsp_1),interesting(0.00)]). fof(t35_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)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A) => B = C ) ) ) ) ), file(rlvect_1,t35_rlvect_1), [interesting(0.00)]). fof(t43_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)) => ( ~ ( B != C & k5_bhsp_1(A,B,C) = 0 ) & ~ ( k5_bhsp_1(A,B,C) != 0 & B = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t32_bhsp_1,t35_rlvect_1,t41_bhsp_1]), [file(bhsp_1,t43_bhsp_1),interesting(0.00)]). fof(t44_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(0,k5_bhsp_1(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t34_bhsp_1]), [file(bhsp_1,t44_bhsp_1),interesting(0.00)]). fof(t45_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)) => ( ~ ( B != C & r1_xreal_0(k5_bhsp_1(A,B,C),0) ) & ~ ( ~ r1_xreal_0(k5_bhsp_1(A,B,C),0) & B = C ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_bhsp_1,t44_bhsp_1,t41_bhsp_1]), [file(bhsp_1,t45_bhsp_1),interesting(0.00)]). fof(t46_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)) => k5_bhsp_1(A,B,C) = k9_square_1(k2_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,B,C))) ) ) ) ), file(bhsp_1,t46_bhsp_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(t45_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)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B)) ) ) ) ), file(rlvect_1,t45_rlvect_1), [interesting(0.00)]). fof(t49_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)) => k5_bhsp_1(A,k6_rlvect_1(A,B,C),k6_rlvect_1(A,D,C)) = k5_bhsp_1(A,B,D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_rlvect_1,t41_rlvect_1,t41_rlvect_1,t43_rlvect_1,t28_rlvect_1,t26_rlvect_1]), [file(bhsp_1,t49_bhsp_1),interesting(0.00)]). fof(t4_bhsp_1,theorem,( $true ), file(bhsp_1,t4_bhsp_1), [interesting(0.00)]). fof(t51_bhsp_1,theorem,( $true ), file(bhsp_1,t51_bhsp_1), [interesting(0.00)]). fof(t52_bhsp_1,theorem,( $true ), file(bhsp_1,t52_bhsp_1), [interesting(0.00)]). fof(t53_bhsp_1,theorem,( $true ), file(bhsp_1,t53_bhsp_1), [interesting(0.00)]). fof(t54_bhsp_1,theorem,( $true ), file(bhsp_1,t54_bhsp_1), [interesting(0.00)]). fof(d5_normsp_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) & l2_rlvect_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k3_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k4_rlvect_1(A,k2_normsp_1(A,B,E),k2_normsp_1(A,C,E)) ) ) ) ) ) ) ), file(normsp_1,d5_normsp_1), [interesting(0.00)]). fof(t113_funct_2,theorem,( ! [A,B,C] : ( ( v1_funct_1(C) & v1_funct_2(C,A,B) & m2_relset_1(C,A,B) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,A,B) & m2_relset_1(D,A,B) ) => ( ! [E] : ( m1_subset_1(E,A) => k1_funct_1(C,E) = k1_funct_1(D,E) ) => C = D ) ) ) ), file(funct_2,t113_funct_2), [interesting(0.00)]). fof(t55_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k3_normsp_1(A,B,C) = k3_normsp_1(A,C,B) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_normsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t55_bhsp_1),interesting(0.00)]). fof(t56_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => k8_bhsp_1(A,B,k8_bhsp_1(A,C,D)) = k8_bhsp_1(A,k8_bhsp_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d5_normsp_1,d5_normsp_1,d6_rlvect_1,d5_normsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t56_bhsp_1),interesting(0.00)]). fof(d4_normsp_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v5_seqm_3(B) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,D) = C ) ) ) ) ) ), file(normsp_1,d4_normsp_1), [interesting(0.00)]). fof(t57_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( ( v5_seqm_3(B) & v5_seqm_3(C) & D = k8_bhsp_1(A,B,C) ) => v5_seqm_3(D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_normsp_1,d4_normsp_1,d4_normsp_1,d5_normsp_1]), [file(bhsp_1,t57_bhsp_1),interesting(0.00)]). fof(d6_normsp_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) & l2_rlvect_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k4_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k6_rlvect_1(A,k2_normsp_1(A,B,E),k2_normsp_1(A,C,E)) ) ) ) ) ) ) ), file(normsp_1,d6_normsp_1), [interesting(0.00)]). fof(t58_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( ( v5_seqm_3(B) & v5_seqm_3(C) & D = k4_normsp_1(A,B,C) ) => v5_seqm_3(D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_normsp_1,d4_normsp_1,d4_normsp_1,d6_normsp_1]), [file(bhsp_1,t58_bhsp_1),interesting(0.00)]). fof(d8_normsp_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) & l2_rlvect_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k6_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k3_rlvect_1(A,k2_normsp_1(A,B,E),C) ) ) ) ) ) ) ), file(normsp_1,d8_normsp_1), [interesting(0.00)]). fof(t59_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(B)) & m2_relset_1(C,k5_numbers,u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(B)) & m2_relset_1(D,k5_numbers,u1_struct_0(B)) ) => ( ( v5_seqm_3(C) & D = k6_normsp_1(B,C,A) ) => v5_seqm_3(D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_normsp_1,d4_normsp_1,d8_normsp_1]), [file(bhsp_1,t59_bhsp_1),interesting(0.00)]). fof(t5_bhsp_1,theorem,( $true ), file(bhsp_1,t5_bhsp_1), [interesting(0.00)]). fof(t60_bhsp_1,theorem,( $true ), file(bhsp_1,t60_bhsp_1), [interesting(0.00)]). fof(t61_bhsp_1,theorem,( $true ), file(bhsp_1,t61_bhsp_1), [interesting(0.00)]). fof(t62_bhsp_1,theorem,( $true ), file(bhsp_1,t62_bhsp_1), [interesting(0.00)]). fof(t63_bhsp_1,theorem,( $true ), file(bhsp_1,t63_bhsp_1), [interesting(0.00)]). fof(t64_bhsp_1,theorem,( $true ), file(bhsp_1,t64_bhsp_1), [interesting(0.00)]). fof(t65_bhsp_1,theorem,( $true ), file(bhsp_1,t65_bhsp_1), [interesting(0.00)]). fof(t66_bhsp_1,theorem,( $true ), file(bhsp_1,t66_bhsp_1), [interesting(0.00)]). fof(t67_bhsp_1,theorem,( $true ), file(bhsp_1,t67_bhsp_1), [interesting(0.00)]). fof(t27_normsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( v5_seqm_3(B) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & k2_relat_1(B) = k1_struct_0(A,C) ) ) ) ) ), file(normsp_1,t27_normsp_1), [interesting(0.00)]). fof(t21_normsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & k2_relat_1(B) = k1_struct_0(A,C) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,C) = k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,1)) ) ) ) ) ), file(normsp_1,t21_normsp_1), [interesting(0.00)]). fof(t22_normsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,C) = k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,1)) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,C) = k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,D)) ) ) ) ) ) ), file(normsp_1,t22_normsp_1), [interesting(0.00)]). fof(t23_normsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,C) = k8_funct_2(k5_numbers,u1_struct_0(A),B,k1_nat_1(C,D)) ) ) => ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,C) = k8_funct_2(k5_numbers,u1_struct_0(A),B,D) ) ) ) ) ) ), file(normsp_1,t23_normsp_1), [interesting(0.00)]). fof(t24_normsp_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ~ ( ! [C] : ( m2_subset_1(C,k1_numbers,k5_numbers) => ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,C) = k8_funct_2(k5_numbers,u1_struct_0(A),B,D) ) ) & ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k8_funct_2(k5_numbers,u1_struct_0(A),B,D) = C ) ) ) ) ) ), file(normsp_1,t24_normsp_1), [interesting(0.00)]). fof(d10_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ( C = k6_bhsp_1(A,B) <=> ! [D] : ( m2_subset_1(D,k1_numbers,k5_numbers) => k2_normsp_1(A,C,D) = k5_rlvect_1(A,k2_normsp_1(A,B,D)) ) ) ) ) ) ), file(bhsp_1,d10_bhsp_1), [interesting(0.00)]). fof(d12_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k7_bhsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k4_rlvect_1(A,k2_normsp_1(A,B,E),C) ) ) ) ) ) ) ), file(bhsp_1,d12_bhsp_1), [interesting(0.00)]). fof(t72_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => B = k7_bhsp_1(A,B,k1_rlvect_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d12_bhsp_1,t10_rlvect_1,t113_funct_2]), [file(bhsp_1,t72_bhsp_1),interesting(0.00)]). fof(d9_rlvect_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_rlvect_1(A) ) => ( v7_rlvect_1(A) <=> ( ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k3_rlvect_1(A,C,B),k3_rlvect_1(A,D,B)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k3_real_1(B,C)) = k2_rlvect_1(A,k3_rlvect_1(A,D,B),k3_rlvect_1(A,D,C)) ) ) ) & ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( m1_subset_1(C,k1_numbers) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => k3_rlvect_1(A,D,k4_real_1(B,C)) = k3_rlvect_1(A,k3_rlvect_1(A,D,C),B) ) ) ) & ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_rlvect_1(A,B,1) = B ) ) ) ) ), file(rlvect_1,d9_rlvect_1), [interesting(0.00)]). fof(t75_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( m1_subset_1(B,k1_numbers) => ! [C] : ( ( ~ v3_struct_0(C) & v3_rlvect_1(C) & v4_rlvect_1(C) & v5_rlvect_1(C) & v6_rlvect_1(C) & v7_rlvect_1(C) & v2_bhsp_1(C) & l1_bhsp_1(C) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(C)) & m2_relset_1(D,k5_numbers,u1_struct_0(C)) ) => k6_normsp_1(C,D,k4_real_1(A,B)) = k6_normsp_1(C,k6_normsp_1(C,D,B),A) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,d9_rlvect_1,d8_normsp_1,d8_normsp_1,t113_funct_2]), [file(bhsp_1,t75_bhsp_1),interesting(0.00)]). fof(t77_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => k6_normsp_1(A,B,k1_real_1(1)) = k6_bhsp_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,t29_rlvect_1,d10_bhsp_1,t113_funct_2]), [file(bhsp_1,t77_bhsp_1),interesting(0.00)]). fof(d7_normsp_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) & l2_rlvect_1(A) ) => ! [B] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => ( D = k5_normsp_1(A,B,C) <=> ! [E] : ( m2_subset_1(E,k1_numbers,k5_numbers) => k2_normsp_1(A,D,E) = k6_rlvect_1(A,k2_normsp_1(A,B,E),C) ) ) ) ) ) ) ), file(normsp_1,d7_normsp_1), [interesting(0.00)]). fof(t78_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] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k5_normsp_1(A,C,B) = k7_bhsp_1(A,C,k5_rlvect_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_normsp_1,d12_bhsp_1,t113_funct_2]), [file(bhsp_1,t78_bhsp_1),interesting(0.00)]). fof(t79_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,B,C) = k6_bhsp_1(A,k4_normsp_1(A,C,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,t47_rlvect_1,d6_normsp_1,d10_bhsp_1,t113_funct_2]), [file(bhsp_1,t79_bhsp_1),interesting(0.00)]). fof(t7_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,k4_rlvect_1(A,C,D)) = k3_real_1(k2_bhsp_1(A,B,C),k2_bhsp_1(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1]), [file(bhsp_1,t7_bhsp_1),interesting(0.00)]). fof(t80_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => B = k5_normsp_1(A,B,k1_rlvect_1(A)) ) ) ), inference(mizar_proof,[status(thm)],[d7_normsp_1,t26_rlvect_1,t113_funct_2]), [file(bhsp_1,t80_bhsp_1),interesting(0.00)]). fof(t30_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)) => k5_rlvect_1(A,k5_rlvect_1(A,B)) = B ) ) ), file(rlvect_1,t30_rlvect_1), [interesting(0.00)]). fof(t81_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => B = k6_bhsp_1(A,k6_bhsp_1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[d10_bhsp_1,d10_bhsp_1,t30_rlvect_1,t113_funct_2]), [file(bhsp_1,t81_bhsp_1),interesting(0.00)]). fof(t82_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,B,k8_bhsp_1(A,C,D)) = k4_normsp_1(A,k4_normsp_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,d5_normsp_1,t41_rlvect_1,d6_normsp_1,d6_normsp_1,t113_funct_2]), [file(bhsp_1,t82_bhsp_1),interesting(0.00)]). fof(t83_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,k8_bhsp_1(A,B,C),D) = k8_bhsp_1(A,B,k4_normsp_1(A,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,d5_normsp_1,d6_rlvect_1,d6_normsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t83_bhsp_1),interesting(0.00)]). fof(t84_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] : ( ( v1_funct_1(B) & v1_funct_2(B,k5_numbers,u1_struct_0(A)) & m2_relset_1(B,k5_numbers,u1_struct_0(A)) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(A)) & m2_relset_1(C,k5_numbers,u1_struct_0(A)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(A)) & m2_relset_1(D,k5_numbers,u1_struct_0(A)) ) => k4_normsp_1(A,B,k4_normsp_1(A,C,D)) = k8_bhsp_1(A,k4_normsp_1(A,B,C),D) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d6_normsp_1,d6_normsp_1,t43_rlvect_1,d6_normsp_1,d5_normsp_1,t113_funct_2]), [file(bhsp_1,t84_bhsp_1),interesting(0.00)]). fof(t48_rlvect_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & l2_rlvect_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k3_rlvect_1(B,k6_rlvect_1(B,C,D),A) = k6_rlvect_1(B,k3_rlvect_1(B,C,A),k3_rlvect_1(B,D,A)) ) ) ) ) ), file(rlvect_1,t48_rlvect_1), [interesting(0.00)]). fof(t85_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( ( v1_funct_1(C) & v1_funct_2(C,k5_numbers,u1_struct_0(B)) & m2_relset_1(C,k5_numbers,u1_struct_0(B)) ) => ! [D] : ( ( v1_funct_1(D) & v1_funct_2(D,k5_numbers,u1_struct_0(B)) & m2_relset_1(D,k5_numbers,u1_struct_0(B)) ) => k6_normsp_1(B,k4_normsp_1(B,C,D),A) = k4_normsp_1(B,k6_normsp_1(B,C,A),k6_normsp_1(B,D,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d8_normsp_1,d6_normsp_1,t48_rlvect_1,d8_normsp_1,d8_normsp_1,d6_normsp_1,t113_funct_2]), [file(bhsp_1,t85_bhsp_1),interesting(0.00)]). fof(t8_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k2_bhsp_1(B,C,k3_rlvect_1(B,D,A)) = k4_real_1(A,k2_bhsp_1(B,C,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1]), [file(bhsp_1,t8_bhsp_1),interesting(0.00)]). fof(t9_bhsp_1,theorem,( ! [A] : ( m1_subset_1(A,k1_numbers) => ! [B] : ( ( ~ v3_struct_0(B) & v3_rlvect_1(B) & v4_rlvect_1(B) & v5_rlvect_1(B) & v6_rlvect_1(B) & v7_rlvect_1(B) & v2_bhsp_1(B) & l1_bhsp_1(B) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(B)) => ! [D] : ( m1_subset_1(D,u1_struct_0(B)) => k2_bhsp_1(B,k3_rlvect_1(B,C,A),D) = k2_bhsp_1(B,C,k3_rlvect_1(B,D,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_bhsp_1,d2_bhsp_1]), [file(bhsp_1,t9_bhsp_1),interesting(0.00)]).