```(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
(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
)))
```

```
"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))
```

```
"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