```
(def-constant ff%dist
"lambda(f,g:ff, fn%dist(f,g))"
```

```
(def-theorem ff%dist-is-bounded
"forall(f,g:ff, ff%dist(f,g)<=1)"
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally ff%dist)
(cut-with-single-formula "forsome(f_1,g_1:total%fns, f=f_1 and g=g_1)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p);")
(backchain "with(p:prop,p);")
(backchain "with(p:prop,p);")
(weaken (0))
(apply-macete-with-minor-premises tr%fn%dist-is-bounded))
(instantiate-existential ("f" "g"))
)))
```

```
(def-theorem stop-is-in-ff
"#(stop_ff,ff)"
lemma
(proof
(
(apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory)
(apply-macete-with-minor-premises stop-is-a-failure)
)))
```

```
(def-theorem positivity-of-ff%dist
"forall(x,y:ff,0<=ff%dist(x,y))"
lemma
(proof
(
(unfold-single-defined-constant-globally ff%dist)
)))
```

```(def-theorem ()
"forall(x,y:ff,x=y iff ff%dist(x,y)=0)"
lemma
(proof
(
(unfold-single-defined-constant-globally ff%dist)
)))
```

```(def-theorem ()
"forall(x,y:ff,ff%dist(x,y)=ff%dist(y,x))"
lemma
(proof
(
(unfold-single-defined-constant-globally ff%dist)
simplify
direct-and-antecedent-inference-strategy
(cut-with-single-formula "0<=fn%dist(y,x)")
)))
```

```(def-theorem ()
"forall(x,y,z:ff,ff%dist(x,z)<=ff%dist(x,y)+ff%dist(y,z))"
lemma
(proof
(
(unfold-single-defined-constant-globally ff%dist)
)))
```

```
(source pointed-metric-spaces)
(fixed-theories h-o-real-arithmetic)
(sort-pairs (pp ff))
(constant-pairs (a_0 stop_ff) (dist ff%dist))
(theory-interpretation-check using-simplification))
```

```(def-transported-symbols (complete cauchy lim)
(renamer pms-to-gm)
)
```

```
(def-theorem ff-completeness
"ff%complete"
(proof
(
(cut-with-single-formula "sub%complete")
(move-to-sibling 1)
(apply-macete-with-minor-premises completeness-of-ff)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "sub%complete;")
unfold-defined-constants
unfold-defined-constants
(unfold-single-defined-constant-globally ff%dist))
)))
```

```
```

```(def-theorem ()
"forsome(h:[ind_1,ff],total_q{h,[ind_1,ff]})"
(proof
(
(instantiate-existential ("with(f:ff, lambda(x:ind_1,f))"))
simplify-insistently
)))
```

```(def-theorem ()
"forall(h:[ind_1,ff],
total_q{h,[ind_1,ff]}
iff
(total_q{h,[ind_1,ff]}
and
#(sup(lambda(a:rr,
if(forsome(u:ind_1,
a=ff%dist(stop_ff,h(u))),
an%individual,
?unit%sort))))))"
lemma
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
simplify-insistently
(instantiate-existential ("with(u:ind_1, ff%dist(stop_ff,h(u)))"))
(block
(script-comment "`instantiate-existential' at (0)")
(instantiate-existential ("u"))
(cut-with-single-formula "0<=ff%dist(stop_ff,h(u))")
(apply-macete-with-minor-premises positivity-of-ff%dist)
(apply-macete-with-minor-premises stop-is-in-ff))
(cut-with-single-formula "0<=ff%dist(stop_ff,h(u))"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0)")
(instantiate-existential ("1"))
(unfold-single-defined-constant-globally majorizes)
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(r,x_\$0:rr,x_\$0=r);")
(apply-macete-with-minor-premises ff%dist-is-bounded))
)))
```

```
(source mappings-into-a-pointed-metric-space)
(fixed-theories h-o-real-arithmetic)
(sort-pairs (bfun (pred "lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})")))
(theory-interpretation-check using-simplification))
```

```(def-transported-symbols (bfun%dist)
(renamer  mpms-to-pgm)
)
```

```(def-theorem ()
"forall(x,y,z:bfun, bfun%dist(x,z)<=bfun%dist(x,y)+bfun%dist(y,z))"
lemma
(proof existing-theorem))
```

```(def-theorem ()
"forall(x,y:bfun, 0<=bfun%dist(x,y))"
lemma
(proof existing-theorem))
```

```(def-theorem ()
"forall(x,y:bfun, bfun%dist(x,y)=bfun%dist(y,x))"
lemma
(proof existing-theorem))
```

```(def-theorem ()
"forall(x,y:bfun, x=y iff bfun%dist(x,y)=0)"
lemma
(proof existing-theorem))
```

```(def-theorem ()
"forall(f,g:[ind_1,ff],
#(ff%dist_p(f,g))
implies
total_q{f,[ind_1,ff]} and total_q{g,[ind_1,ff]})"
lemma
(proof
(
(unfold-single-defined-constant-globally ff%dist_p)
simplify
)))
```

```(def-theory-ensemble-instances metric-spaces
(permutations (0) (0 1))
(sorts (pp (pred "lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})")
(pred "lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})")))
(constants (dist ff%dist_p ff%dist_p))
(special-renamings
(complete ff%complete_p)
(contraction ff%contraction_p)
(mu ff%mu_p)))
```

```
(def-theorem parametrized-completeness
"ff%complete_p"
(proof
(
(assume-transported-theorem
bfun-completeness
(backchain "with(p:prop,p);")
(apply-macete-with-minor-premises ff-completeness)
)))
```

```
(def-theorem parametrized-definedness-of-mu-for-contractions-lemma
definedness-of-mu-for-contractions
lemma
(proof existing-theorem))
```

```
(def-theorem parametrized-condition-for-contractions-on-function-spaces-lemma
condition-for-contractions-on-function-spaces
lemma
(proof existing-theorem))
```

```
(def-atomic-sort ff_p
"lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})"

```

```
(def-theorem parametrized-definedness-of-mu-for-contractions
"forall(f:[ff_p->ff_p],
ff%contraction_p(f) and total_q{f,[ff_p->ff_p]}
implies
#(ff%mu_p(f)))"
(proof
(
(unfold-single-defined-constant-globally ff%contraction_p)
simplify-insistently
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises parametrized-definedness-of-mu-for-contractions-lemma)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises parametrized-completeness)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(unfold-single-defined-constant-globally ff%contraction_p)
simplify-insistently
auto-instantiate-existential)
(backchain "with(f:[ff_p,ff_p],total_q{f,[ff_p,ff_p]});")
)))
```