(def-theory-instance vector-spaces-over-rr (source vector-spaces) (target h-o-real-arithmetic) (translation fields-to-rr) (renamer vs-renamer))

(def-overloading + (h-o-real-arithmetic +) (vector-spaces-over-rr ++))

(def-overloading * (h-o-real-arithmetic *) (vector-spaces-over-rr **))

(def-constant sub_vv"lambda(x,y:uu,x+[-1]*y)"(theory vector-spaces-over-rr))

(def-algebraic-processor vector-space-algebraic-processor (language vector-spaces-over-rr) (base ((operations (+ ++) (* **) (sub sub_vv) (zero v0)))) (coefficient rr-algebraic-processor))

(def-overloading sub (h-o-real-arithmetic sub) (vector-spaces-over-rr sub_vv))

(def-theorem sub-lemma-for-processor"forall(y,x:uu,x-y=x+v0-y)"(theory vector-spaces-over-rr) (proof ( direct-inference-strategy unfold-defined-constants (force-substitution"x+(v0+[-1]*y)""x+v0+[-1]*y"(0)) (apply-macete-with-minor-premises %vector-zero-identity) (apply-macete-with-minor-premises %vector-plus-associativity) )))

(def-theorem ()"forall(x:uu,x+v0-x=v0)"(theory vector-spaces-over-rr) (proof ( direct-and-antecedent-inference-strategy unfold-defined-constants (force-substitution"x+(v0+[-1]*x)""x+v0+[-1]*x"(0)) (apply-macete-with-minor-premises %vector-zero-identity) (force-substitution"x+[-1]*x""(1+[-1])*x"(0)) (force-substitution"(1+[-1])""0"(0)) (apply-macete-with-minor-premises tr%scalar-multiplication-by-zero) simplify (apply-macete-with-minor-premises %vector-times-right-distributivity) (apply-macete-with-minor-premises %scalar-multiplication-by-one) (apply-macete-with-minor-premises %vector-plus-associativity) )))

(def-theory-processors vector-spaces-over-rr (algebraic-simplifier (vector-space-algebraic-processor ** ++ sub_vv)) (algebraic-term-comparator vector-space-algebraic-processor))

(def-language normed-linear-space-language (embedded-language vector-spaces-over-rr-language) (constants (norm"[uu,rr]")))

(def-theory normed-linear-spaces (language normed-linear-space-language) (component-theories vector-spaces-over-rr) (axioms (norm-totality"total_q{norm,[uu, rr]}"d-r-convergence transportable-macete) (positivity-of-norm"forall(x:uu, 0<=norm(x))"transportable-macete) (norm-zero"forall(x:uu, norm(x)=0 iff x = v0)"transportable-macete) (norm-scalar-multiplication"forall(x:uu, a:rr, norm(a**x) = abs(a) * norm(x))"transportable-macete) (norm-triangle-inequality"forall(x,y:uu, norm(x++y) <= norm(x) + norm(y))"transportable-macete)))

(def-theorem ()"forall(x,y,z:uu,norm(x+[-1]*z)<=norm(x+[-1]*y)+norm(y+[-1]*z))"(theory normed-linear-spaces) (proof ( (force-substitution"x+[-1]*z""(x+[-1]*y)+(y+[-1]*z)"(0)) (apply-macete-with-minor-premises norm-triangle-inequality) simplify )))

(def-theorem ()"forall(x,y,z:uu, norm([-1]*z+x)<=norm([-1]*z+y)+norm(x+[-1]*y))"(theory normed-linear-spaces) (proof ( (force-substitution"[-1]*z+x""([-1]*z+y)+(x+[-1]*y)"(0)) (apply-macete-with-minor-premises norm-triangle-inequality) simplify )))

(def-theorem ()"forall(x,y:uu,norm(x+[-1]*y)=norm([-1]*x+y))"(theory normed-linear-spaces) (proof ( (force-substitution"x+[-1]*y""[-1]*([-1]*x+y)"(0)) (apply-macete-with-minor-premises norm-scalar-multiplication) (apply-macete-with-minor-premises absolute-value-non-positive) simplify simplify )))

(def-theorem ()"forall(x,y:uu,x=y iff norm(x+[-1]*y)=0)"(theory normed-linear-spaces) (proof ( (apply-macete-with-minor-premises norm-zero) simplify )))

(def-theory-ensemble-instances metric-spaces force-under-quick-load (target-theories normed-linear-spaces normed-linear-spaces) (multiples 1 2) (theory-interpretation-check using-simplification) (sorts (pp uu uu)) (constants (dist"lambda(x,y:uu, norm(x-y))""lambda(x,y:uu, norm(x-y))")))

(def-theory-ensemble-overloadings metric-spaces (1 2))

(def-theorem closed-balls-are-defined"forall(b:uu,r:rr,#(ball(b,r)))"(theory normed-linear-spaces) (usages d-r-convergence) (proof ( unfold-defined-constants simplify-insistently )))

(def-theorem open-balls-are-defined"forall(b:uu,r:rr,#(open%ball(b,r)))"(theory normed-linear-spaces) (usages d-r-convergence) (proof ( unfold-defined-constants simplify-insistently )))

(def-theorem ()"norm(v0)=0"(usages rewrite) (theory normed-linear-spaces) (proof ( (apply-macete-with-minor-premises norm-zero) )))

(def-theorem norm-continuity-lemma"forall(x,y,z:uu, norm(x)-norm(y)<=norm(x-y))"(theory normed-linear-spaces) (proof ( (force-substitution"norm(x)-norm(y)<=norm(x-y)""norm((x-y)+y)<=norm(x-y)+norm(y)"(0)) (apply-macete-with-minor-premises norm-triangle-inequality) simplify )))

(def-theorem vs-addition-of-fractions-left"forall(a,b:rr,u,y:uu,a/b*u + y == (1/b)*(a*u+b*y))"(proof ( (apply-macete-with-minor-premises %vector-times-left-distributivity) (force-substitution"1/b*(b*y)""(1/b*b)*y"(0)) direct-and-antecedent-inference-strategy (case-split ("b=0")) simplify simplify (apply-macete-with-minor-premises %vector-times-associativity) )) (theory vector-spaces-over-rr))

(def-theorem vs-addition-of-fractions-right"forall(a,b:rr,u,y:uu, y+a/b*u == (1/b)*(a*u+b*y))"(proof ( (apply-macete-with-minor-premises %vector-times-left-distributivity) (force-substitution"1/b*(b*y)""(1/b*b)*y"(0)) direct-and-antecedent-inference-strategy (case-split ("b=0")) simplify simplify (apply-macete-with-minor-premises %vector-times-associativity) )) (theory vector-spaces-over-rr))

(def-theorem sub-replacement"forall(x,y:uu,x-y=x+[-1]*y)"(proof ( simplify )) (theory vector-spaces-over-rr))

(def-theorem vector-times-associativity-left"forall(a,b:rr,x:uu,a*(b*x)=(a*b)*x)"(proof ( simplify )) (theory vector-spaces-over-rr))

(def-compound-macete ns-fractional-expression-manipulation (repeat vs-addition-of-fractions-right vs-addition-of-fractions-left sub-replacement vector-times-associativity-left norm-scalar-multiplication))