```
(def-theory ultrametric-spaces
(component-theories h-o-real-arithmetic)
(language metric-spaces-language)
(axioms
(positivity-of-distance
"forall(x,y:pp, 0<=dist(x,y))" transportable-macete)
(point-separation-for-distance
"forall(x,y:pp, x=y iff dist(x,y)=0)" transportable-macete)
(ultrametric-symmetry-of-distance
"forall(x,y:pp, dist(x,y) = dist(y,x))" transportable-macete)
(ultrametric-inequality-for-distance
"forall(x,y,z:pp, dist(x,z)<=max(dist(x,y),dist(y,z)))" transportable-macete)))
```

```
(def-theorem ultrametic-spaces-are-metric
"forall(x,y,z:pp,dist(x,z)<=dist(x,y)+dist(y,z))"
(theory ultrametric-spaces)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "dist(x,z)<=max(dist(x,y),dist(y,z))")
(move-to-sibling 1)
(apply-macete-with-minor-premises ultrametric-inequality-for-distance)
(cut-with-single-formula
"forall(a,b:rr, 0<=a and 0<=b implies max(a,b)<=a+b)")
(instantiate-universal-antecedent
"with(p:prop,forall(a,b:rr,p));" ("dist(x,y)" "dist(y,z)"))
(simplify-antecedent "with(p:prop,not(p));")
(simplify-antecedent "with(p:prop,not(p));")
simplify
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) max)
(case-split ("a<=b"))
simplify
simplify
)))
```

```
(def-theorem ultrametric-distance-bound-lemma
"forall(x,y,z:pp, eps:rr,
dist(x,y)<=eps and dist(y,z)<=eps implies dist(x,z)<=eps)"
(theory ultrametric-spaces)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "dist(x,z)<=max(dist(x,y),dist(y,z))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(r:rr,z,x:pp,dist(x,z)<=max(r,r));")
(unfold-single-defined-constant (0) max)
(case-split ("dist(x,y)<=dist(y,z)"))
simplify
simplify)
(apply-macete-with-minor-premises ultrametric-inequality-for-distance)
)))
```

```(def-theory-ensemble-instances metric-spaces
(target-theories ultrametric-spaces ultrametric-spaces)
(permutations  (0) (0 1))
(theory-interpretation-check using-simplification)
(sorts (pp pp pp))
(constants (dist dist dist)))
```

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

```
(def-theorem intersecting-balls-are-comparable
"forall(x,y:pp, r,s:rr, 0<=r and r<=s and
nonempty_indic_q{ball(x,r) inters ball(y,s)}
implies
ball(x,r) subseteq ball(y,s))"
(theory ultrametric-spaces)
(proof
(
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(x_\$0:pp,f:sets[pp],x_\$0 in f);")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%ball-membership-condition)
direct-and-antecedent-inference-strategy
insistent-direct-inference
(apply-macete-with-minor-premises tr%ball-membership-condition)
direct-inference
(apply-macete-with-minor-premises ultrametric-distance-bound-lemma)
auto-instantiate-existential
(apply-macete-with-minor-premises ultrametric-distance-bound-lemma)
(instantiate-existential ("x"))
(block
(script-comment "`instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises tr%ultrametric-symmetry-of-distance)
simplify)
simplify
)))
```

```
(def-theorem cauchy-ultrametric-condition
"forall(x:[zz,pp],
cauchy(x) iff
forall(eps:rr,
0<eps implies
forsome(n:zz, forall(m:zz, n<=m implies dist(x(m),x(m+1))<=eps))))"
(theory ultrametric-spaces)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%cauchy-double-index-characterization)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0)")
(auto-instantiate-universal-antecedent "with(x:[zz,pp],
forall(eps:rr,
0<eps
implies
forsome(n:zz,
forall(p,q:zz,
n<=p and n<=q implies dist(x(p),x(q))<=eps))));")
(instantiate-existential ("n"))
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(auto-instantiate-universal-antecedent "with(x:[zz,pp],
forall(eps:rr,
0<eps
implies
forsome(n:zz,
forall(m:zz,n<=m implies dist(x(m),x(m+1))<=eps))));")
(instantiate-existential ("n"))
(apply-macete-with-minor-premises ultrametric-distance-bound-lemma)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("x(n)"))
(move-to-ancestor 1)
(cut-with-single-formula "forall(q:zz, n<=q implies dist(x(q),x(n))<=eps)")
(block
(script-comment "`cut-with-single-formula' at (0)")
direct-and-antecedent-inference-strategy
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2)")
(apply-macete-with-minor-premises tr%ultrametric-symmetry-of-distance)
simplify))
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction integer-inductor ("q"))
(block
(script-comment "`induction' at (0 0 0)")
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
(block
(script-comment "`instantiate-existential' at (0 1 0 0 0 1)")
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"

("n"))
(simplify-antecedent "with(p:prop,not(p));")))
(block
(script-comment "`induction' at (0 1 0 0 0 0 0)")
(apply-macete-with-minor-premises ultrametric-distance-bound-lemma)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("x(t)"))
(apply-macete-with-minor-premises tr%ultrametric-symmetry-of-distance)
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"

("t"))
simplify)
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"
("t")))))
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));" ("p"))
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));" ("q")))
)))
```