```(def-language language-for-interval-theory
(embedded-languages h-o-real-arithmetic)
(sorts (ii rr)))
```

```
(def-theory fixed-interval-theory
Remark: This entry is multiply defined. See:  [1] [2]
(component-theories h-o-real-arithmetic)
(language language-for-interval-theory)
(axioms
(interval-characterization
"forall(a,b:ii,x:rr, a<=x and x<=b implies #(x,ii))")
(non-degeneracy
"forsome(x,y:ii, x<y)")))
```

```
(def-theorem interval-bounding-lemma
Remark: This entry is multiply defined. See:  [1] [2]
"forall(x,y:rr, c,d :ii,
not(#(x,ii)) and not(#(y,ii)) and x<=c and c<=y
implies
x<d  and d<y)"

(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(x:rr,not(#(x,ii)));")
(apply-macete-with-minor-premises interval-characterization)
(instantiate-existential ("c" "d"))
simplify
(contrapose "with(y:rr,not(#(y,ii)));")
(apply-macete-with-minor-premises interval-characterization)
(instantiate-existential ("d" "c"))
simplify
))
(theory fixed-interval-theory))
```

```(def-theorem ()
"forall(a,c:ii,forsome(b:ii,a<=b and b<=c) implies a<=c)"
(theory fixed-interval-theory)
lemma
(proof
(

direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises transitivity-of-<=)
auto-instantiate-existential
)))
```

```(def-theorem ()
"forall(p:[ii,prop],
nonvacuous_q{p}
and
forsome(alpha:ii,
forall(theta:ii,p(theta) implies theta<=alpha))
implies
forsome(gamma:ii,
forall(theta:ii,p(theta) implies theta<=gamma)
and
forall(gamma_1:ii,
forall(theta:ii,p(theta) implies theta<=gamma_1)
implies
gamma<=gamma_1)))"
(theory fixed-interval-theory)
lemma
(proof
(

direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises completeness)
(instantiate-theorem completeness ("p"))
(instantiate-universal-antecedent "with(p:prop,forall(x_0:rr,not(p)));" ("x_0"))
(instantiate-universal-antecedent "with(p:prop,forall(alpha:rr,forsome(theta:rr,p)));"
("alpha"))
(contrapose "with(p:prop,not(p));")
simplify
(instantiate-existential ("gamma"))
simplify
simplify
(apply-macete-with-minor-premises interval-characterization)
(instantiate-universal-antecedent "with(gamma:rr,p:[ii,prop],
forall(theta:rr,p(theta) implies theta<=gamma));"
("x_0"))
(instantiate-universal-antecedent "with(gamma:rr,p:prop,
forall(gamma_1:rr,
forall(theta:rr,p) implies gamma<=gamma_1));"
("alpha"))
(simplify-antecedent "with(p:prop,not(p));")
(instantiate-existential ("alpha" "x_0"))
)))
```

```
(def-translation cpo-to-fixed-interval-theory