(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 
    force-under-quick-load
    (source complete-partial-order)
    (target fixed-interval-theory)
    (fixed-theories h-o-real-arithmetic)
    (constant-pairs
      (prec "lambda(x,y:ii,x<=y)")
      (rev%prec "lambda(a,b:ii,b<=a)"))
    (sort-pairs (uu ii))
    (theory-interpretation-check using-simplification))