(def-language language-for-interval-in-cpo
    (embedded-languages complete-partial-order)
    (constants 
      (bot uu)
      (top uu)))

(def-theory interval-in-cpo 
    (component-theories complete-partial-order)
    (language language-for-interval-in-cpo)
    (axioms
      (non-triviality "bot prec top")))

(def-theorem ()
    "lambda(x:uu,bot prec x and x prec top)(bot)"
    (theory interval-in-cpo)
    (proof
      (
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises prec-reflexivity)
        (apply-macete-with-minor-premises non-triviality)
        )))

(def-atomic-sort ii 
    "lambda(x:uu, bot prec x and x prec top)"
    (theory interval-in-cpo)
    (witness "bot"))

(def-theorem ()
    "forall(a,c:ii,
        forsome(b:ii,a prec b and b prec c) implies a prec c)"
    lemma
    (theory interval-in-cpo)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises prec-transitivity)
        auto-instantiate-existential
        )))

(def-theorem interval-characterization 
  Remark: This entry is multiply defined. See:  [1] [2] [3]
    "forall(a,b:ii,x:uu, a prec x and x prec b implies #(x,ii))"
    (theory interval-in-cpo)
    (proof
      (
        
        
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises ii-defining-axiom_interval-in-cpo)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises prec-transitivity)
        (instantiate-existential ("a"))
        (cut-with-single-formula "#(a,ii)")
        (incorporate-antecedent "with(a:ii,#(a,ii));")
        (apply-macete-with-minor-premises ii-defining-axiom_interval-in-cpo)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises prec-transitivity)
        (instantiate-existential ("b"))
        (cut-with-single-formula "#(b,ii)")
        (incorporate-antecedent "with(b:ii,#(b,ii));")
        (apply-macete-with-minor-premises ii-defining-axiom_interval-in-cpo)
        direct-and-antecedent-inference-strategy
        )))

(def-theorem ()
    "forall(p:[ii,prop],
        nonvacuous_q{p}
            and 
          forsome(alpha:ii,
              forall(theta:ii,p(theta) implies theta prec alpha))
            implies 
          forsome(gamma:ii,
              forall(theta:ii,p(theta) implies theta prec gamma)
                and 
              forall(gamma_1:ii,
                  forall(theta:ii,p(theta) implies theta prec gamma_1)
                    implies 
                  gamma prec gamma_1)))"
    lemma
    (theory interval-in-cpo)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem prec-completeness ("lambda(x:ii,p(x))"))
        (simplify-antecedent "with(p:prop,forall(x_0:uu,not(p)));")
        (instantiate-universal-antecedent "with(p:prop,forall(x_$1:ii,not(p)));"
				            ("x_0"))
        (instantiate-universal-antecedent "with(p:prop,forall(alpha:uu,forsome(theta:uu,p)));"
				            ("with(alpha:ii, alpha)"))
        (contrapose "with(p:prop,not(p));")
        (backchain "with(p:prop,forall(theta:ii,p implies p));")
        (cut-with-single-formula "#(gamma,ii)")
        (move-to-sibling 1)
        (apply-macete-with-minor-premises interval-characterization)
        (instantiate-existential ("alpha" "x_0"))
        (backchain "with(gamma:uu,p:prop,
    forall(theta:uu,
        lambda(x:ii,p)(theta) implies theta prec gamma));")
        beta-reduce-repeatedly
        (backchain "with(gamma:uu,p:prop,
    forall(gamma_1:uu,
        forall(theta:uu,p) implies gamma prec gamma_1));")
        direct-and-antecedent-inference-strategy
        (backchain "with(alpha:ii,p:[ii,prop],
    forall(theta:ii,p(theta) implies theta prec alpha));")
        (instantiate-existential ("gamma"))
        (backchain "with(gamma:uu,p:prop,
    forall(theta:uu,
        lambda(x:ii,p)(theta) implies theta prec gamma));")
        beta-reduce-repeatedly
        simplify    )))

(def-translation relativize-to-interval 
    force-under-quick-load
    (source complete-partial-order)
    (target interval-in-cpo)
    (fixed-theories h-o-real-arithmetic)
    (constant-pairs
      (prec "lambda(x,y:ii, x prec y)"))
    (sort-pairs (uu ii))
    (theory-interpretation-check using-simplification))