```
(def-translation complete-partial-order-to-h-o-real-arithmetic
(source complete-partial-order)
(target h-o-real-arithmetic)
(fixed-theories h-o-real-arithmetic)
(constant-pairs
(prec <=)
(rev%prec "lambda(a,b:rr,b<=a)"))
(sort-pairs (uu rr))
(theory-interpretation-check using-simplification))

```

```(def-transported-symbols
(prec%increasing
rev%prec%increasing
prec%majorizes
prec%minorizes
prec%sup
prec%inf
prec%lim%inf
prec%lim%sup)
(translation complete-partial-order-to-h-o-real-arithmetic)
(renamer partial-order-rr-renamer))
```

```
(def-translation index-families
(source mappings-into-a-partial-order)
(target generic-theory-1)
(fixed-theories h-o-real-arithmetic)
(constant-pairs (prec <=))
(sort-pairs (uu rr))
(theory-interpretation-check using-simplification))
```

```
(def-theorem sum-inequality-macete
"forall(x,y,z,u:rr, x<=z and y<=u implies x+y<=z+u)"
(proof (simplify))
(theory h-o-real-arithmetic))
```

```
(def-theorem sup-sum
"forall(f,g:[ind_1,rr], #(sup(ran{f})) and #(sup(ran{g})) and nonempty_indic_q{dom{f} inters dom{g}} implies sup(ran{lambda(x:ind_1,f(x)+g(x))})<=sup(ran{f})+sup(ran{g}))"
(proof

(direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "f(n_\$0)<=sup(ran{f}) and g(n_\$0)<=sup(ran{g})")
simplify
(apply-macete-with-minor-premises tr%prec%sup-dominates-values)
direct-and-antecedent-inference-strategy
simplify-insistently
simplify-insistently
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly
(instantiate-existential ("x_\$0"))
(incorporate-antecedent "with(x_\$0:ind_1,g,f:[ind_1,rr],x_\$0 in dom{f} inters dom{g})")
simplify
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
(instantiate-existential ("sup(ran{f})+sup(ran{g})"))
(cut-with-single-formula "f(n_\$1)<=sup(ran{f}) and g(n_\$1)<=sup(ran{g})")
simplify
(apply-macete-with-minor-premises tr%prec%sup-dominates-values)
direct-and-antecedent-inference-strategy
simplify
simplify))
(theory generic-theory-1))
```