```
"lambda(f:[pp_0,pp_1], x:pp_0,
forsome(a:rr, 0<=a and forall(y:pp_0,dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y)))))"
(theory metric-spaces-2-tuples))
```

```
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-existential ("min(1,eps/(1+a))"))
(weaken (0))
(unfold-single-defined-constant (0) min)
(case-split ("1<=eps/(1+a)"))
simplify
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("dist_0(x,y_\$0)*(a+dist_0(x,y_\$0))"))
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("(eps/(1+a))*(a+1)"))
(apply-macete-with-minor-premises monotone-product-lemma)
(cut-with-single-formula "min(1,eps/(1+a))<=1 and min(1,eps/(1+a))<=eps/(1+a)")
simplify
(apply-macete-with-minor-premises minimum-2nd-arg)
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
))

(usages transportable-macete)
(theory metric-spaces-2-tuples))
```

```(def-theory-ensemble-instances metric-spaces
(target-theories metric-spaces h-o-real-arithmetic h-o-real-arithmetic)
(sorts (pp pp rr rr))
(constants (dist dist "lambda(x,y:rr, abs(x-y))" "lambda(x,y:rr, abs(x-y))"))
(permutations (1) (0 1) (1 2)))
```

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

```
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-existential ("2*abs(x)"))
simplify
(force-substitution "x^2-y_\$1^2" "(x-y_\$1)*(x+y_\$1)" (0))
(force-substitution "x+y_\$1" "(x+x)+(y_\$1-x)" (0))
(apply-macete-with-minor-premises absolute-value-product)
(apply-macete-with-minor-premises monotone-product-lemma)
direct-and-antecedent-inference-strategy
simplify
simplify
simplify
unfold-defined-constants
(weaken (0 1 2 3))
(prove-by-logic-and-simplification 3)
simplify
simplify
))
(theory h-o-real-arithmetic))
```

```

(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-existential ("abs(a)"))
simplify
(force-substitution "a*x-a*y_\$1" "a*(x-y_\$1)" (0))
(apply-macete-with-minor-premises absolute-value-product)
simplify
simplify

))
(theory h-o-real-arithmetic))
```

```
(def-theorem square-is-continuous
"forall(x:rr, continuous%at%point(lambda(x:rr,x^2),x))"
(proof
(
)
)
(theory h-o-real-arithmetic))
```

```
(def-theorem multiplication-by-a-constant-is-continuous
"forall(a,x:rr,continuous%at%point(lambda(x:rr, a*x),x))"
(proof
(
))
(theory h-o-real-arithmetic))
```

```
(def-theorem composition-of-continuous-is-continuous
"forall(f:[pp,rr],g:[rr,rr],x:pp,
continuous%at%point(f,x) and continuous%at%point(g,f(x))
implies
continuous%at%point(g oo f,x))"

(proof
(

unfold-defined-constants
beta-reduce-with-minor-premises
direct-and-antecedent-inference-strategy
(auto-instantiate-universal-antecedent "with(g:[rr,rr],x:pp,f:[pp,rr],
forall(eps_\$0:rr,
0<eps_\$0
implies
forsome(delta_\$0:rr,
0<delta_\$0
and
forall(y_\$0:rr,
abs(f(x)-y_\$0)<=delta_\$0
implies
abs(g(f(x))-g(y_\$0))<=eps_\$0))));")
(instantiate-universal-antecedent "with(f:[pp,rr],x:pp,
forall(eps:rr,
0<eps
implies
forsome(delta:rr,
0<delta
and
forall(y:pp,
dist(x,y)<=delta implies abs(f(x)-f(y))<=eps))));" ("delta_\$0"))
(instantiate-existential ("delta"))
(backchain "with(eps_\$0:rr,g:[rr,rr],delta_\$0:rr,x:pp,f:[pp,rr],
forall(y_\$0:rr,
abs(f(x)-y_\$0)<=delta_\$0
implies
abs(g(f(x))-g(y_\$0))<=eps_\$0));")
(backchain "with(delta_\$0:rr,f:[pp,rr],delta:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta implies abs(f(x)-f(y))<=delta_\$0));")
(cut-with-single-formula "abs(f(x)-f(y_\$0))<=delta_\$0")
(instantiate-universal-antecedent "with(f:[pp,rr],x:pp,
forall(eps:rr,
0<eps
implies
forsome(delta:rr,
0<delta
and
forall(y:pp,
dist(x,y)<=delta implies abs(f(x)-f(y))<=eps))));" ("1"))
(simplify-antecedent "not(0<1);")
(cut-with-single-formula "abs(f(x)-f(x))<=1")
(backchain "with(f:[pp,rr],delta:rr,x:pp,
forall(y:pp,dist(x,y)<=delta implies abs(f(x)-f(y))<=1));")
simplify
))
(theory metric-spaces))
```

```
(def-theorem sum-of-continuous-is-continuous
"forall(f,g:[pp,rr], x:pp,
continuous%at%point(f,x) and continuous%at%point(g,x)
implies
continuous%at%point(lambda(x:pp,f(x)+g(x)),x))"
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("eps_\$0/2"))
(simplify-antecedent "with(p:prop, not(p))")
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("eps_\$0/2"))
(simplify-antecedent "with(p:prop, not(p))")
(cut-with-single-formula "min(delta,delta_\$0)<=delta and min(delta,delta_\$0)<=delta_\$0")
(instantiate-existential ("min(delta,delta_\$0)"))
unfold-defined-constants
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("abs(f(x)-f(y_\$1))+abs(g(x)-g(y_\$1))"))
(cut-with-single-formula "#(f(x)) and #(g(x)) and #(f(y_\$1)) and #(g(y_\$1))")
unfold-defined-constants
(weaken (1 2 3 4 5 6 7))
(prove-by-logic-and-simplification 3)
simplify
(instantiate-universal-antecedent "with(eps_\$0:rr,f:[pp,rr],delta_\$0:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta_\$0 implies abs(f(x)-f(y))<=eps_\$0/2));" ("y_\$1"))
(contrapose "with(p:prop, not(p))")
simplify
(instantiate-universal-antecedent "with(eps_\$0:rr,g:[pp,rr],delta:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta implies abs(g(x)-g(y))<=eps_\$0/2));" ("y_\$1"))
(contrapose "with(p:prop, not(p))")
simplify
simplify
(cut-with-single-formula "abs(f(x)-f(y_\$1))<=eps_\$0/2 and abs(g(x)-g(y_\$1))<=eps_\$0/2")
simplify
direct-inference
(backchain "with(eps_\$0:rr,f:[pp,rr],delta_\$0:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta_\$0 implies abs(f(x)-f(y))<=eps_\$0/2));")
simplify
(backchain "with(eps_\$0:rr,g:[pp,rr],delta:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta implies abs(g(x)-g(y))<=eps_\$0/2));")
simplify
(instantiate-universal-antecedent "with(eps_\$0:rr,f:[pp,rr],delta_\$0:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta_\$0 implies abs(f(x)-f(y))<=eps_\$0/2));" ("y_\$1"))
(instantiate-universal-antecedent "with(eps_\$0:rr,g:[pp,rr],delta:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta implies abs(g(x)-g(y))<=eps_\$0/2));" ("y_\$1"))
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises minimum-2nd-arg)
)
)
(usages transportable-macete)
(theory metric-spaces))
```

```(def-schematic-macete abstraction-for-sum
"with(a,b:rr, lambda(x:pp,a+b)=lambda(x:pp,lambda(x:pp,a)(x)+lambda(x:pp,b)(x)))"
(theory metric-spaces)
null)

```

```(def-schematic-macete abstraction-for-square
"with(a:rr, lambda(x:pp,a^2)=lambda(x:rr,x^2) oo lambda(x:pp,a))"
(theory metric-spaces)
null)
```

```(def-schematic-macete abstraction-for-scalar-product
"with(a,c:rr, lambda(x:pp,a * c)=lambda(x:rr,a * x) oo lambda(x:pp, c))"
(theory metric-spaces)
null)
```

```
(def-compound-macete abstraction
(sound
(series abstraction-for-sum
abstraction-for-scalar-product
abstraction-for-square)
beta-reduce-unstoppably
beta-reduce-unstoppably))
```

```
(def-compound-macete composite-continuity-macete
(series
(repeat
abstraction
sum-of-continuous-is-continuous
composition-of-continuous-is-continuous
square-is-continuous
multiplication-by-a-constant-is-continuous)
tr%unary-eta-reduction))
```

```
(def-theorem product-in-terms-of-squares-lemma
Remark: This entry is multiply defined. See:  [1] [2]
"forall(a,b:rr, a*b=1/2*((a+b)^2+[-1]*(a^2+b^2)))"

(proof
(
simplify
))
(theory h-o-real-arithmetic))
```

```
(def-theorem continuous-at-point-defined
"forall(f:[pp_0,pp_1], x:pp_0, continuous%at%point(f,x) implies #(f(x)))"
(theory metric-spaces-2-tuples)
(usages transportable-macete)
(proof

(
(unfold-single-defined-constant (0) continuous%at%point)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
(simplify-antecedent "not(0<1);")
(cut-with-single-formula "dist_1(f(x),f(x))<=1")
(backchain "with(f:[pp_0,pp_1],delta:rr,x:pp_0,
forall(y:pp_0,
dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=1));")
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
)
))
```

```
(def-theorem product-of-continous-is-continuous
"forall(f,g:[pp,rr], x:pp, continuous%at%point(f,x) and continuous%at%point(g,x) implies
continuous%at%point(lambda(x:pp, f(x)*g(x)),x))"
(theory metric-spaces)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises product-in-terms-of-squares-lemma)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(f(x)) and #(g(x))")
(apply-macete-with-minor-premises composite-continuity-macete)
simplify
(apply-macete-with-minor-premises tr%continuous-at-point-defined)
simplify
)))
```

```
(def-theorem dist-uniformly-continuous
"forall(y:pp,uniformly%continuous(lambda(x:pp,dist(x,y))))"
(usages transportable-macete)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
auto-instantiate-existential
(cut-with-single-formula "abs(dist(x_\$1,y)-dist(y_\$1,y))<=dist(x_\$1,y_\$1)")
simplify
(apply-macete-with-minor-premises dist-continuity-lemma)
))
(theory metric-spaces))
```

```
(def-theorem constant-uniformly-continuous
"forall(r:rr,uniformly%continuous(lambda(x:pp,r)))"
(usages transportable-macete)
(theory metric-spaces)
(proof

(
unfold-defined-constants
direct-and-antecedent-inference-strategy
auto-instantiate-existential
(unfold-single-defined-constant (0) abs)
simplify
)))
```

```
(def-theorem constant-is-continuous
"forall(r:rr,x:pp, continuous%at%point(lambda(x:pp,r),x))"
(usages transportable-macete)
(theory metric-spaces)
(proof

(
unfold-defined-constants
direct-and-antecedent-inference-strategy
auto-instantiate-existential
(unfold-single-defined-constant (0) abs)
simplify
)))
```

```
(def-theorem identity-uniformly-continuous
"uniformly%continuous(lambda(x:pp,x))"
(usages transportable-macete)
(theory metric-spaces)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
auto-instantiate-existential
)))

```

```
(def-theorem composition-of-continuous-special-case
"forall(f:[pp,pp],g:[pp,rr],x:pp,
continuous%at%point(f,x) and continuous%at%point(g,f(x))
implies
continuous%at%point(g oo f,x))"
(proof
(

unfold-defined-constants
beta-reduce-with-minor-premises
direct-and-antecedent-inference-strategy
(auto-instantiate-universal-antecedent "with(p:prop,forall(eps:rr,  0<eps implies p))")
(instantiate-universal-antecedent "with(p:prop,forall(eps:rr,  0<eps implies p))" ("delta_\$0"))
(instantiate-existential ("delta"))
(backchain "with(eps_\$0:rr,g:[pp,rr],delta_\$0:rr,x:pp,f:[pp,pp],
forall(y_\$0:pp,
dist(f(x),y_\$0)<=delta_\$0
implies
abs(g(f(x))-g(y_\$0))<=eps_\$0));")
(backchain "with(delta_\$0:rr,f:[pp,pp],delta:rr,x:pp,
forall(y:pp,
dist(x,y)<=delta implies dist(f(x),f(y))<=delta_\$0));")
(cut-with-single-formula "dist(f(x),f(y_\$0))<=delta_\$0")
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
(simplify-antecedent "not(0<1);")
(cut-with-single-formula "dist(f(x),f(x))<=1")
(backchain "with(f:[pp,pp],delta:rr,x:pp,
forall(y:pp,dist(x,y)<=delta implies dist(f(x),f(y))<=1));")
simplify
))
(usages transportable-macete)
(theory metric-spaces))
```

```(def-schematic-macete transportable-abstraction-for-sum
"with(a,b:rr, lambda(x:ind_1,a+b)=lambda(x:ind_1,lambda(x:ind_1,a)(x)+lambda(x:ind_1,b)(x)))"
(theory generic-theory-1)
transportable
null)

```

```(def-schematic-macete transportable-abstraction-for-product
"with(a,c:rr, lambda(x:ind_1,a * c)=lambda(x:ind_1,lambda(x:ind_1,a)(x) * lambda(x:ind_1, c)(x)))"
(theory generic-theory-1)
transportable
null)
```

```
(def-compound-macete real-fn-abstraction
(sound
(series transportable-abstraction-for-sum
transportable-abstraction-for-product)
beta-reduce-unstoppably
beta-reduce-unstoppably))
```

```
(def-compound-macete polynomial-continuity-macete
(series
(repeat
(without-minor-premises exp-out)
real-fn-abstraction
tr%sum-of-continuous-is-continuous
tr%product-of-continous-is-continuous
tr%constant-is-continuous
beta-reduce)
tr%unary-eta-reduction))
```