(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))