(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-constant dseq 
    "lambda(delta:rr, lambda(x:rr, delta*(floor(x/delta))))"
    (theory h-o-real-arithmetic))

(def-theorem dseq-definedness 
    "forall(delta,x:rr, 0<delta implies #(dseq(delta)(x)))"
    (theory fixed-interval-theory)
    (proof
      (
        (unfold-single-defined-constant (0) dseq)
        direct-and-antecedent-inference-strategy
        (instantiate-theorem floor-definedness ("x/delta"))
        simplify
        )))

(def-theorem dseq-distance-bound 
    "forall(x,delta:rr, 0<delta implies dseq(delta)(x)<=x and x<dseq(delta)(x)+delta)"
    (theory fixed-interval-theory)
    (proof
      (
        direct-inference
        direct-inference
        unfold-defined-constants
        (cut-with-single-formula "forsome(n:zz, floor(x/delta)=n)")
        (antecedent-inference "with(p:prop,forsome(n:zz,p));")
        (backchain-repeatedly ("with(n,z:zz,z=n);"))
        (incorporate-antecedent "with(n,z:zz,z=n);")
        (apply-macete-with-minor-premises floor-characterization)
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (cut-with-single-formula "total_q{floor,[rr,zz]}")
        (instantiate-existential ("floor(x/delta)"))
        simplify
        (apply-macete-with-minor-premises floor-definedness)
        )))

(def-constant delta%width 
    "lambda(delta:rr, 0<delta and forsome(x,y:ii, delta<=y-x))"
    (theory fixed-interval-theory))

(def-theorem dseq-quasi-invariance 
    "forall(delta:rr,
          delta%width(delta)
              implies 
          forall(x:ii,
              #(dseq(delta)(x),ii) or #(dseq(delta)(x)+delta,ii)))"
    (proof
      (
        (unfold-single-defined-constant (0) delta%width)
        direct-and-antecedent-inference-strategy
        (contrapose "with(x_$0,y:ii,delta:rr,delta<=y-x_$0);")
        (cut-with-single-formula "(dseq(delta)(x)<x_$0 and x_$0<dseq(delta)(x)+delta) and 
                                                            (dseq(delta)(x)<y and y<dseq(delta)(x)+delta)")
        simplify
        (apply-macete-with-minor-premises interval-bounding-lemma)
        (cut-with-single-formula "dseq(delta)(x)<=x and x<dseq(delta)(x)+delta")
        direct-inference
        (instantiate-existential ("x"))
        simplify
        (apply-macete-with-minor-premises dseq-distance-bound)
        (apply-macete-with-minor-premises dseq-definedness)
        (apply-macete-with-minor-premises dseq-definedness)
        ))
    (theory fixed-interval-theory))

(def-theorem dseq-distance-bound-corollary 
    "forall(delta:rr,
          delta%width(delta)
              implies 
          forall(x:ii,#(if(#(dseq(delta)(x),ii), dseq(delta)(x),dseq(delta)(x)+delta),ii)))"
    (proof
      (
        direct-and-antecedent-inference-strategy
        sort-definedness
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula " #(dseq(delta)(x),ii) or #(dseq(delta)(x)+delta,ii)")
        (antecedent-inference "with(p,q:prop, p or q)")
        (apply-macete-with-minor-premises dseq-quasi-invariance)
        ))
    (theory fixed-interval-theory))

(def-theorem ()
    "forall(x,y,z:ii,abs(x+[-1]*z)<=abs(x+[-1]*y)+abs(y+[-1]*z))"
    (theory fixed-interval-theory)
    (proof
      (
        (force-substitution "x+[-1]*z" "(x+[-1]*y)+(y+[-1]*z)" (0))
        (apply-macete-with-minor-premises triangle-inequality)
        simplify
        ))
    )

(def-theorem ()
    "forall(x,y:ii,abs(x+[-1]*y)=abs([-1]*x+y))"
    (theory fixed-interval-theory)
    (proof
      (
        (force-substitution "([-1]*x+y)" "[-1]*(x+[-1]*y)" (0))
        (apply-macete-with-minor-premises absolute-value-product)
        (apply-macete absolute-value-non-positive)
        simplify
        simplify
        )))

(def-theorem ()
    "forall(x,y:ii,x=y iff abs(x+[-1]*y)=0)"
    (theory fixed-interval-theory)
    (proof
      (
        (apply-macete-with-minor-premises absolute-value-zero)
        simplify
        
        )))

(def-theory mappings-from-an-interval 
    (component-theories fixed-interval-theory metric-spaces))

(def-theorem ()
    "forall(x,y,z:ii,abs([-1]*z+x)<=abs([-1]*z+y)+abs(x+[-1]*y))"
    (theory  fixed-interval-theory)
    (proof
      (
        (force-substitution "[-1]*z+x" "([-1]*z+y)+(x+[-1]*y)" (0))
        (apply-macete-with-minor-premises triangle-inequality)
        simplify
        )))

(def-theory-ensemble-instances metric-spaces 
    force-under-quick-load
    (target-theories fixed-interval-theory metric-spaces)
    (permutations  (0) (0 1))
    (theory-interpretation-check using-simplification)
    (sorts (pp ii pp))
    (constants (dist "lambda(x,y:ii, abs(x-y))" dist))
    (special-renamings
      (ball ii%ball)
      (open%ball ii%open%ball)
      (lim ii%lim)
      (closure ii%closure)
      (uniformly%continuous uniformly%continuous%ii%pp)
      (lipschitz%bound ii%lipschitz%bound)
      (lipschitz%bound%on ii%lipschitz%bound%on)))

(def-theory-ensemble-overloadings metric-spaces (1 2))

(def-constant step%fn 
    "lambda(f:[ii,pp],
          forsome(delta:rr,
              0<delta
                and 
              forall(x,y:ii,
                  dseq(delta)(x)=dseq(delta)(y) implies f(x)=f(y))))"
    (theory mappings-from-an-interval))

(def-constant delta%step%approximant 
    "lambda(delta:rr,f:[ii,pp],
            lambda(x:ii,
                f(if(#(dseq(delta)(x),ii), dseq(delta)(x),dseq(delta)(x)+delta))))"
      (theory mappings-from-an-interval))

(def-theorem delta-step-is-a-step-fn 
    "forall(delta:rr,f:[ii,pp],
              delta%width(delta) and total_q{f,[ii,pp]}
                                                implies 
                                            step%fn(delta%step%approximant(delta,f)))"
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        (backchain-repeatedly ("with(a,b:rr,a=b)"))
        (cut-with-single-formula "#(if(#(dseq(delta)(y_$1),ii), 
                            dseq(delta)(y_$1), dseq(delta)(y_$1)+delta),ii)")
        (apply-macete-with-minor-premises dseq-distance-bound-corollary)
        (unfold-single-defined-constant-globally delta%width)
        direct-and-antecedent-inference-strategy
        auto-instantiate-existential
        ))
    (theory mappings-from-an-interval))

(def-theorem step-functions-approximate 
    "forall(f:[ii,pp], eps:rr, 
          0<eps and uniformly%continuous(f) and total_q{f,[ii,pp]}
            implies 
          forsome(g:[ii,pp],
            step%fn(g) and forall(x:ii, dist(f(x),g(x))<=eps)))"
    (theory mappings-from-an-interval)
    (proof
      (
        (unfold-single-defined-constant (0) uniformly%continuous%ii%pp)
        direct-and-antecedent-inference-strategy
        (auto-instantiate-universal-antecedent "with(f:[ii,pp],
    forall(eps:rr,
        0<eps
          implies 
        forsome(delta:rr,
            0<delta
              and 
            forall(x,y:ii,
                #(f(x)) and #(f(y)) and abs(x-y)<=delta
                  implies 
                dist(f(x),f(y))<=eps))));")
        (cut-with-single-formula "forsome(delta_1:rr, delta%width(delta_1) and delta_1<=delta)")
        (antecedent-inference "with(p:prop,forsome(delta_1:rr,p));")
        (instantiate-existential ("delta%step%approximant(delta_1,f)"))
        (apply-macete-with-minor-premises delta-step-is-a-step-fn)
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant (0) delta%step%approximant)
        (backchain "with(p:prop,forall(x,y:ii,p));")
        direct-and-antecedent-inference-strategy
        (backchain "with(f:[ii,pp],total_q{f,[ii,pp]});")
        (apply-macete-with-minor-premises commutative-law-for-addition)
        (apply-macete-with-minor-premises dseq-distance-bound-corollary)
        (unfold-single-defined-constant (0) abs)
        (cut-with-single-formula
          "dseq(delta_1)(x_$0)<=x_$0 and x_$0<dseq(delta_1)(x_$0)+delta_1")
        (prove-by-logic-and-simplification 3)
        (apply-macete-with-minor-premises dseq-distance-bound)
        (incorporate-antecedent "with(p:prop,p and p);")
        (unfold-single-defined-constant (0) delta%width)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises commutative-law-for-addition)
        (apply-macete-with-minor-premises dseq-distance-bound-corollary)
        (unfold-single-defined-constant-globally delta%step%approximant)
        (unfold-single-defined-constant (0) delta%width)
        (cut-with-single-formula "forsome(x,y:ii, x<y)")
        (instantiate-existential ("min(y-x,delta)"))
        (unfold-single-defined-constant (0) min)
        (prove-by-logic-and-simplification 3)
        (instantiate-existential ("x" "y"))
        (apply-macete-with-minor-premises minimum-1st-arg)
        (apply-macete-with-minor-premises minimum-2nd-arg)
        (apply-macete-with-minor-premises non-degeneracy)
        )))