THEORY Intervals
  IMPORT THEORY PROJECTS
    /SimpleDEq THEORIES /SimpleDEq/Reals.dtf|org.eventb.theory.core.deployedTheoryRoot#Reals
  OPERATORS
    Infinity2Open expression (b: RReal)
      direct definition 
        { t | t |-> b : lt }
    Infinity2Closed expression (b: RReal)
      direct definition 
        { t | t |-> b : leq }
    Open2Infinity expression (a: RReal)
      direct definition 
        { t | a |-> t : lt }
    Closed2Infinity expression (a: RReal)
      direct definition 
        { t | a |-> t : leq }
    Open2Open expression (a: RReal,b: RReal)
      direct definition 
        { t | a |-> t : lt & t |-> b : lt }
    Open2Closed expression (a: RReal,b: RReal)
      direct definition 
        { t | a |-> t : lt & t |-> b : leq }
    Closed2Open expression (a: RReal,b: RReal)
      direct definition 
        { t | a |-> t : leq & t |-> b : lt }
    Closed2Closed expression (a: RReal,b: RReal)
      direct definition 
        { t | a |-> t : leq & t |-> b : leq }
  THEOREMS
    realPlusIsZero2Infinity: 
      RRealPlus = Closed2Infinity(Rzero)
    realMinusIsInfinity2Zero: 
      RRealMinus = Infinity2Closed(Rzero)
    c2c_existence: 
      ! a,b . a : RReal & b : RReal & a |-> b : leq => (# x . x : Closed2Closed(a,b))
    c2o_existence: 
      ! a,b . a : RReal & b : RReal & a |-> b : lt => (# x . x : Closed2Open(a,b))
    o2c_existence: 
      ! a,b . a : RReal & b : RReal & a |-> b : lt => (# x . x : Open2Closed(a,b))
    o2o_existence: 
      ! a,b . a : RReal & b : RReal & a |-> b : lt => (# x . x : Open2Open(a,b))
    boundaryInClosed2Closed: 
      ! a, b . a : RReal & b : RReal => (a : Closed2Closed(a,b) & b : Closed2Closed(a,b))
    boundaryInClosed2Open: 
      ! a, b . a : RReal & b : RReal => (a : Closed2Open(a,b))
    boundaryInOpen2Closed: 
      ! a, b . a : RReal & b : RReal => (b : Open2Closed(a,b))
    boundaryInInfinity2Closed: 
      ! b . b : RReal => (b : Infinity2Closed(b))
    boundaryInClosed2Infinity: 
      ! a . a : RReal => (a : Closed2Infinity(a))
    closed2ClosedLowerBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : leq =>
        lowerBound(leq, Closed2Closed(a,b), a)
    closed2OpenLowerBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        lowerBound(leq, Closed2Open(a,b), a)
    open2ClosedLowerBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        lowerBound(leq, Open2Closed(a,b), a)
    open2OpenLowerBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        lowerBound(leq, Open2Open(a,b), a)
    closed2InfinityLowerBound: 
      ! a . a : RReal =>
        lowerBound(leq, Closed2Infinity(a), a)
    open2InfinityLowerBound: 
      ! a . a : RReal =>
        lowerBound(leq, Open2Infinity(a), a)
    infinity2ClosedLowerBound: 
      ! b . b : RReal =>
        not lowerBounded(leq, Infinity2Closed(b))
    infinity2OpenLowerBound: 
      ! b . b : RReal =>
        not lowerBounded(leq, Infinity2Open(b))
    closed2ClosedInfimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : leq =>
        infimum(leq, Closed2Closed(a,b), a)
    closed2OpenInfimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        infimum(leq, Closed2Open(a,b), a)
    open2ClosedInfimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        infimum(leq, Open2Closed(a,b), a)
    open2OpenInfimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        infimum(leq, Open2Open(a,b), a)
    closed2InfinityInfimum: 
      ! a . a : RReal =>
        infimum(leq, Closed2Infinity(a), a)
    open2InfinityInfimum: 
      ! a . a : RReal =>
        infimum(leq, Open2Infinity(a), a)
    closed2ClosedMinimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : leq =>
        minimum(leq, Closed2Closed(a,b), a)
    closed2OpenMinimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        minimum(leq, Closed2Open(a,b), a)
    open2ClosedMinimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        not hasMinimum(leq, Open2Closed(a,b))
    open2OpenMinimum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        not hasMinimum(leq, Open2Open(a,b))
    closed2InfinityMinimum: 
      ! a . a : RReal =>
        minimum(leq, Closed2Infinity(a), a)
    open2InfinityMinimum: 
      ! a . a : RReal =>
        not hasMinimum(leq, Open2Infinity(a))
    infinity2ClosedMinimum: 
      ! b . b : RReal =>
        not hasMinimum(leq, Infinity2Closed(b))
    infinity2OpenMinimum: 
      ! b . b : RReal =>
        not hasMinimum(leq, Infinity2Open(b))
    closed2ClosedUpperBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : leq =>
        upperBound(leq, Closed2Closed(a,b), b)
    closed2OpenUpperBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        upperBound(leq, Closed2Open(a,b), b)
    open2ClosedUpperBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        upperBound(leq, Open2Closed(a,b), b)
    open2OpenUpperBound: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        upperBound(leq, Open2Open(a,b), b)
    closed2InfinityUpperBound: 
      ! a . a : RReal =>
        not upperBounded(leq, Closed2Infinity(a))
    open2InfinityUpperBound: 
      ! a . a : RReal =>
        not upperBounded(leq, Open2Infinity(a))
    infinity2ClosedUpperBound: 
      ! b . b : RReal =>
        upperBound(leq, Infinity2Closed(b), b)
    infinity2OpenUpperBound: 
      ! b . b : RReal =>
        upperBound(leq, Infinity2Open(b), b)
    closed2ClosedSupremum: 
      ! a, b . a : RReal & b : RReal & a |-> b : leq =>
        supremum(leq, Closed2Closed(a,b), b)
    closed2OpenSupremum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        supremum(leq, Closed2Open(a,b), b)
    open2ClosedSupremum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        supremum(leq, Open2Closed(a,b), b)
    open2OpenSupremum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        supremum(leq, Open2Open(a,b), b)
    infinity2ClosedSupremum: 
      ! b . b : RReal =>
        supremum(leq, Infinity2Closed(b), b)
    infinity2OpenSupremum: 
      ! b . b : RReal =>
        supremum(leq, Open2Infinity(b), b)
    closed2ClosedMaximum: 
      ! a, b . a : RReal & b : RReal & a |-> b : leq =>
        maximum(leq, Closed2Closed(a,b), b)
    closed2OpenMaximum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        not hasMaximum(leq, Closed2Open(a,b))
    open2ClosedMaximum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        maximum(leq, Open2Closed(a,b), b)
    open2OpenMaximum: 
      ! a, b . a : RReal & b : RReal & a |-> b : lt =>
        not hasMaximum(leq, Open2Open(a,b))
    closed2InfinityMaximum: 
      ! a . a : RReal =>
        not hasMaximum(leq, Closed2Infinity(a))
    open2InfinityMaximum: 
      ! a . a : RReal =>
        not hasMaximum(leq, Open2Infinity(a))
    infinity2ClosedMaximum: 
      ! b . b : RReal =>
        maximum(leq, Infinity2Closed(b), b)
    infinity2OpenMaximum: 
      ! b . b : RReal =>
        not hasMaximum(leq, Infinity2Open(b))
    c2cUc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : leq =>
          Closed2Closed(a,b) \/ Closed2Closed(b,c) = Closed2Closed(a,c)
    c2cUc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : lt =>
          Closed2Closed(a,b) \/ Closed2Open(b,c) = Closed2Open(a,c)
    o2cUc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : leq =>
          Open2Closed(a,b) \/ Closed2Closed(b,c) = Open2Closed(a,c)
    o2cUc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Closed(a,b) \/ Closed2Open(b,c) = Open2Open(a,c)
    inf2cUc2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : leq =>
          Infinity2Closed(b) \/ Closed2Closed(b,c) = Infinity2Closed(c)
    inf2cUc2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Closed(b) \/ Closed2Open(b,c) = Infinity2Open(c)
    c2cUc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : leq =>
          Closed2Closed(a,b) \/ Closed2Infinity(b) = Closed2Infinity(a)
    o2cUc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Closed(a,b) \/ Closed2Infinity(b) = Open2Infinity(a)
    inf2cUc2inf: 
      ! a .
        a : RReal =>
          Infinity2Closed(a) \/ Closed2Infinity(a) = RReal
    c2cUo2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : lt =>
          Closed2Closed(a,b) \/ Open2Closed(b,c) = Closed2Closed(a,c)
    c2cUo2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : lt =>
          Closed2Closed(a,b) \/ Open2Open(b,c) = Closed2Open(a,c)
    o2cUo2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Closed(a,b) \/ Open2Closed(b,c) = Open2Closed(a,c)
    o2cUo2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Closed(a,b) \/ Open2Open(b,c) = Open2Open(a,c)
    inf2cUo2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Closed(b) \/ Open2Closed(b,c) = Infinity2Closed(c)
    inf2cUo2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Closed(b) \/ Open2Open(b,c) = Infinity2Open(c)
    c2cUo2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : leq =>
          Closed2Closed(a,b) \/ Open2Infinity(b) = Closed2Infinity(a)
    o2cUo2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Closed(a,b) \/ Open2Infinity(b) = Open2Infinity(a)
    inf2cUo2inf: 
      ! a .
        a : RReal =>
          Infinity2Closed(a) \/ Open2Infinity(a) = RReal
    c2oUc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : leq =>
          Closed2Open(a,b) \/ Closed2Closed(b,c) = Closed2Closed(a,c)
    c2oUc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Closed2Open(a,b) \/ Closed2Open(b,c) = Closed2Open(a,c)
    o2oUc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : leq =>
          Open2Open(a,b) \/ Closed2Closed(b,c) = Open2Closed(a,c)
    o2oUc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Open(a,b) \/ Closed2Open(b,c) = Open2Open(a,c)
    inf2oUc2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : leq =>
          Infinity2Open(b) \/ Closed2Closed(b,c) = Infinity2Closed(c)
    inf2oUc2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Open(b) \/ Closed2Open(b,c) = Infinity2Open(c)
    c2oUc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Closed2Open(a,b) \/ Closed2Infinity(b) = Closed2Infinity(a)
    o2oUc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Open(a,b) \/ Closed2Infinity(b) = Open2Infinity(a)
    inf2oUc2inf: 
      ! a .
        a : RReal =>
          Infinity2Open(a) \/ Closed2Infinity(a) = RReal
    c2cCc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : leq =>
          Closed2Closed(a,b) /\ Closed2Closed(b,c) = {b}
    o2cCc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : leq =>
          Open2Closed(a,b) /\ Closed2Closed(b,c) = {b}
    c2cCc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : lt =>
          Closed2Closed(a,b) /\ Closed2Open(b,c) = {b}
    o2cCc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Closed(a,b) /\ Closed2Open(b,c) = {b}
    inf2cCc2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : leq =>
          Infinity2Closed(b) /\ Closed2Closed(b,c) = {b}
    inf2cCc2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Closed(b) /\ Closed2Open(b,c) = {b}
    c2cCc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : leq =>
          Closed2Closed(a,b) /\ Closed2Infinity(b) = {b}
    o2cCc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Closed(a,b) /\ Closed2Infinity(b) = {b}
    inf2cCc2inf: 
      ! a .
        a : RReal =>
          Infinity2Closed(a) /\ Closed2Infinity(a) = {a}
    c2oCc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : leq =>
          Closed2Open(a,b) /\ Closed2Closed(b,c) = {}
    o2oCc2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : leq =>
          Open2Open(a,b) /\ Closed2Closed(b,c) = {}
    c2oCc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Closed2Open(a,b) /\ Closed2Open(b,c) = {}
    o2oCc2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Open(a,b) /\ Closed2Open(b,c) = {}
    inf2oCc2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : leq =>
          Infinity2Open(b) /\ Closed2Closed(b,c) = {}
    inf2oCc2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Open(b) /\ Closed2Open(b,c) = {}
    c2oCc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Closed2Open(a,b) /\ Closed2Infinity(b) = {}
    o2oCc2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Open(a,b) /\ Closed2Infinity(b) = {}
    inf2oCc2inf: 
      ! a .
        a : RReal =>
          Infinity2Closed(a) /\ Closed2Infinity(a) = {}
    c2cCo2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : lt =>
          Closed2Closed(a,b) /\ Open2Closed(b,c) = {}
    o2cCo2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Closed(a,b) /\ Open2Closed(b,c) = {}
    c2cCo2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : leq & b |-> c : lt =>
          Closed2Closed(a,b) /\ Open2Open(b,c) = {}
    o2cCo2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Closed(a,b) /\ Open2Open(b,c) = {}
    inf2cCo2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Closed(b) /\ Open2Closed(b,c) = {}
    inf2cCo2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Closed(b) /\ Open2Open(b,c) = {}
    c2cCo2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : leq =>
          Closed2Closed(a,b) /\ Open2Infinity(b) = {}
    o2cCo2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Closed(a,b) /\ Open2Infinity(b) = {}
    inf2cCo2inf: 
      ! a .
        a : RReal =>
          Infinity2Closed(a) /\ Open2Infinity(a) = {}
    c2oCo2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Closed2Open(a,b) /\ Open2Closed(b,c) = {}
    o2oCo2c: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Open(a,b) /\ Open2Closed(b,c) = {}
    c2oCo2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Closed2Open(a,b) /\ Open2Open(b,c) = {}
    o2oCo2o: 
      ! a, b, c .
        a : RReal & b : RReal & c : RReal &
        a |-> b : lt & b |-> c : lt =>
          Open2Open(a,b) /\ Open2Open(b,c) = {}
    inf2oCo2c: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Open(b) /\ Open2Closed(b,c) = {}
    inf2oCo2o: 
      ! b, c .
        b : RReal & c : RReal &
        b |-> c : lt =>
          Infinity2Open(b) /\ Open2Open(b,c) = {}
    c2oCo2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Closed2Open(a,b) /\ Open2Infinity(b) = {}
    o2oCo2inf: 
      ! a, b .
        a : RReal & b : RReal &
        a |-> b : lt =>
          Open2Open(a,b) /\ Open2Infinity(b) = {}
    inf2oCo2inf: 
      ! a .
        a : RReal =>
          Infinity2Open(a) /\ Open2Infinity(a) = {}
  PROOF RULES
    minimumRew:
    Metavariables
      a: RReal
      b: RReal
    Rewrite Rules
      minClosed2Closed: Rmin(Closed2Closed(a,b))
        rhs1: a |-> b : leq => a
      minClosed2Open: Rmin(Closed2Open(a,b))
        rhs1: a |-> b : lt => a
      minClosed2Infinity: Rmin(Closed2Infinity(a))
        rhs1: TRUE => a
    maximumRew:
    Metavariables
      a: RReal
      b: RReal
    Rewrite Rules
      maxClosed2Closed: Rmax(Closed2Closed(a,b))
        rhs1: a |-> b : leq => b
      maxOpen2Closed: Rmax(Open2Closed(a,b))
        rhs1: a |-> b : lt => b
      maxInfinity2Closed: Rmax(Infinity2Closed(b))
        rhs1: TRUE => b
    infimumRew:
    Metavariables
      a: RReal
      b: RReal
    Rewrite Rules
      infClosed2Closed: Rinf(Closed2Closed(a,b))
        rhs1: a |-> b : leq => a
      infClosed2Open: Rinf(Closed2Open(a,b))
        rhs1: a |-> b : lt => a
      infOpen2Closed: Rinf(Open2Closed(a,b))
        rhs1: a |-> b : lt => a
      infOpen2Open: Rinf(Open2Open(a,b))
        rhs1: a |-> b : lt => a
      infClosed2Infinity: Rinf(Closed2Infinity(a))
        rhs1: TRUE => a
      infOpen2Infinity: Rinf(Open2Infinity(a))
        rhs1: TRUE => a
    supremumRew:
    Metavariables
      a: RReal
      b: RReal
    Rewrite Rules
      supClosed2Closed: Rsup(Closed2Closed(a,b))
        rhs1: a |-> b : leq => b
      supClosed2Open: Rsup(Closed2Open(a,b))
        rhs1: a |-> b : lt => b
      supOpen2Closed: Rsup(Open2Closed(a,b))
        rhs1: a |-> b : lt => b
      supOpen2Open: Rsup(Open2Open(a,b))
        rhs1: a |-> b : lt => b
      supInfinity2Closed: Rsup(Infinity2Closed(b))
        rhs1: TRUE => b
      supInfinity2Open: Rsup(Infinity2Open(b))
        rhs1: TRUE => b
    intervalURew:
    Metavariables
      a: RReal
      b: RReal
      c: RReal
    Rewrite Rules
      c2cUc2c_rew: Closed2Closed(a,b) \/ Closed2Closed(b,c)
        rhs1: TRUE => Closed2Closed(a,c)
      o2cUc2c_rew: Open2Closed(a,b) \/ Closed2Closed(b,c)
        rhs1: TRUE => Open2Closed(a,c)
      c2cUc2o_rew: Closed2Closed(a,b) \/ Closed2Open(b,c)
        rhs1: TRUE => Closed2Open(a,c)
      o2cUc2o_rew: Open2Closed(a,b) \/ Closed2Open(b,c)
        rhs1: TRUE => Open2Open(a,c)
      inf2cUc2c_rew: Infinity2Closed(b) \/ Closed2Closed(b,c)
        rhs1: TRUE => Infinity2Closed(c)
      inf2cUc2o_rew: Infinity2Closed(b) \/ Closed2Open(b,c)
        rhs1: TRUE => Infinity2Open(c)
      c2cUc2inf_rew: Closed2Closed(a,b) \/ Closed2Infinity(b)
        rhs1: TRUE => Closed2Infinity(a)
      o2cUc2inf_rew: Open2Closed(a,b) \/ Closed2Infinity(b)
        rhs1: TRUE => Open2Infinity(a)
      c2oUc2c_rew: Closed2Open(a,b) \/ Closed2Closed(b,c)
        rhs1: TRUE => Closed2Closed(a,c)
      o2oUc2c_rew: Open2Open(a,b) \/ Closed2Closed(b,c)
        rhs1: TRUE => Open2Closed(a,c)
      c2oUc2o_rew: Closed2Open(a,b) \/ Closed2Open(b,c)
        rhs1: TRUE => Closed2Open(a,c)
      o2oUc2o_rew: Open2Open(a,b) \/ Closed2Open(b,c)
        rhs1: TRUE => Open2Open(a,c)
      inf2oUc2c_rew: Infinity2Open(b) \/ Closed2Closed(b,c)
        rhs1: TRUE => Infinity2Closed(c)
      inf2oUc2o_rew: Infinity2Open(b) \/ Closed2Open(b,c)
        rhs1: TRUE => Infinity2Open(c)
      c2oUc2inf_rew: Closed2Open(a,b) \/ Closed2Infinity(b)
        rhs1: TRUE => Closed2Infinity(a)
      o2oUc2inf_rew: Open2Open(a,b) \/ Closed2Infinity(b)
        rhs1: TRUE => Open2Infinity(a)
      c2cUo2c_rew: Closed2Closed(a,b) \/ Open2Closed(b,c)
        rhs1: TRUE => Closed2Closed(a,c)
      o2cUo2c_rew: Open2Closed(a,b) \/ Open2Closed(b,c)
        rhs1: TRUE => Open2Closed(a,c)
      c2cUo2o_rew: Closed2Closed(a,b) \/ Open2Open(b,c)
        rhs1: TRUE => Closed2Open(a,c)
      o2cUo2o_rew: Open2Closed(a,b) \/ Open2Open(b,c)
        rhs1: TRUE => Open2Open(a,c)
      inf2cUo2c_rew: Infinity2Closed(b) \/ Open2Closed(b,c)
        rhs1: TRUE => Infinity2Closed(c)
      inf2cUo2o_rew: Infinity2Closed(b) \/ Open2Open(b,c)
        rhs1: TRUE => Infinity2Open(c)
      c2cUo2inf_rew: Closed2Closed(a,b) \/ Open2Infinity(b)
        rhs1: TRUE => Closed2Infinity(a)
      o2cUo2inf_rew: Open2Closed(a,b) \/ Open2Infinity(b)
        rhs1: TRUE => Open2Infinity(a)
    intervalCRew:
    Metavariables
      a: RReal
      b: RReal
      c: RReal
    Rewrite Rules
      c2cCc2c_rew: Closed2Closed(a,b) /\ Closed2Closed(b,c)
        rhs1: TRUE => {b}
      o2cCc2c_rew: Open2Closed(a,b) /\ Closed2Closed(b,c)
        rhs1: TRUE => {b}
      c2cCc2o_rew: Closed2Closed(a,b) /\ Closed2Open(b,c)
        rhs1: TRUE => {b}
      o2cCc2o_rew: Open2Closed(a,b) /\ Closed2Open(b,c)
        rhs1: TRUE => {b}
      inf2cCc2c_rew: Infinity2Closed(b) /\ Closed2Closed(b,c)
        rhs1: TRUE => {b}
      inf2cCc2o_rew: Infinity2Closed(b) /\ Closed2Open(b,c)
        rhs1: TRUE => {b}
      c2cCc2inf_rew: Closed2Closed(a,b) /\ Closed2Infinity(b)
        rhs1: TRUE => {b}
      o2cCc2inf_rew: Open2Closed(a,b) /\ Closed2Infinity(b)
        rhs1: TRUE => {b}
    intervalRealParts:
    Rewrite Rules
      RPlus2Int: RRealPlus
        rhs1: TRUE => Closed2Infinity(Rzero)
      Int2RPlus: Closed2Infinity(Rzero)
        rhs1: TRUE => RRealPlus
      RMinus2Int: RRealMinus
        rhs1: TRUE => Infinity2Closed(Rzero)
      Int2RMinus: Infinity2Closed(Rzero)
        rhs1: TRUE => RRealMinus
      RPlusStar2Int: RRealPlusStar
        rhs1: TRUE => Open2Infinity(Rzero)
      Int2RPlusStar: Open2Infinity(Rzero)
        rhs1: TRUE => RRealPlusStar
      RMinusStar2Int: RRealMinusStar
        rhs1: TRUE => Infinity2Open(Rzero)
      Int2RMinusStar: Infinity2Open(Rzero)
        rhs1: TRUE => RRealMinusStar
    intervalInclusion:
    Metavariables
      a1: RReal
      b1: RReal
      a2: RReal
      b2: RReal
    Rewrite Rules
      c2InfIncc2Inf: Closed2Infinity(a1) <: Closed2Infinity(a2)
        rhs1: TRUE => a2 |-> a1 : leq
      o2InfIncc2Inf: Open2Infinity(a1) <: Closed2Infinity(a2)
        rhs1: TRUE => a2 |-> a1 : leq
      c2InfInco2Inf: Closed2Infinity(a1) <: Open2Infinity(a2)
        rhs1: TRUE => a2 |-> a1 : lt
      o2InfInco2Inf: Open2Infinity(a1) <: Open2Infinity(a2)
        rhs1: TRUE => a2 |-> a1 : leq
      inf2cIncinf2c: Infinity2Closed(b1) <: Infinity2Closed(b2)
        rhs1: TRUE => b1 |-> b2 : leq
      inf2oIncinf2c: Infinity2Open(b1) <: Infinity2Closed(b2)
        rhs1: TRUE => b1 |-> b2 : leq
      inf2cIncinf2o: Infinity2Closed(b1) <: Infinity2Open(b2)
        rhs1: TRUE => b1 |-> b2 : lt
      inf2oIncinf2o: Infinity2Open(b1) <: Infinity2Open(b2)
        rhs1: TRUE => b1 |-> b2 : leq
      o2oIno2o: Open2Open(a1,b1) <: Open2Open(a2,b2)
        rhs1: TRUE => a1 |-> a2 : lt & b1 |-> b2 : gt
      c2oInc2c: Closed2Open(a1,b1) <: Closed2Closed(a2,b2)
        rhs1: TRUE => a1 |-> a2 : leq & b1 |-> b2 : geq
    intervalInclusion2:
    Metavariables
      a: RReal
      b: RReal
    Rewrite Rules
      s_o2oIno2Inf: Open2Open(a,b) <: Open2Infinity(a)
        rhs1: TRUE => TRUE
      s_o2cIno2Inf: Open2Closed(a,b) <: Open2Infinity(a)
        rhs1: TRUE => TRUE
      s_o2oInc2Inf: Open2Open(a,b) <: Closed2Infinity(a)
        rhs1: TRUE => TRUE
      s_o2cInc2Inf: Open2Closed(a,b) <: Closed2Infinity(a)
        rhs1: TRUE => TRUE
      s_c2oInc2Inf: Closed2Open(a,b) <: Closed2Infinity(a)
        rhs1: TRUE => TRUE
      s_c2cInc2Inf: Closed2Closed(a,b) <: Closed2Infinity(a)
        rhs1: TRUE => TRUE
      s_o2oIno2c: Open2Open(a,b) <: Open2Closed(a,b)
        rhs1: TRUE => TRUE
      s_o2oInc2o: Open2Open(a,b) <: Closed2Open(a,b)
        rhs1: TRUE => TRUE
      s_o2oInc2c: Open2Open(a,b) <: Closed2Closed(a,b)
        rhs1: TRUE => TRUE
      s_c2oInc2c: Closed2Open(a,b) <: Closed2Closed(a,b)
        rhs1: TRUE => TRUE
      s_o2cInc2c: Open2Closed(a,b) <: Closed2Closed(a,b)
        rhs1: TRUE => TRUE
    degenerated_intervals:
    Metavariables
      a: RReal
    Rewrite Rules
      c2c_single: Closed2Closed(a,a)
        rhs1: TRUE => {a}
      o2c_empty: Open2Closed(a,a)
        rhs1: TRUE => {} : POW(RReal)
      c2o_empty: Closed2Open(a,a)
        rhs1: TRUE => {} : POW(RReal)
      o2o_empty: Open2Open(a,a)
        rhs1: TRUE => {} : POW(RReal)
    intervalElements:
    Metavariables
      a: RReal
      b: RReal
    Rewrite Rules
      a_in_c2c: a : Closed2Closed(a,b)
        rhs1: TRUE => a |-> b : leq
      a_in_c2o: a : Closed2Open(a,b)
        rhs1: TRUE => a |-> b : lt
      b_in_c2c: b : Closed2Closed(a,b)
        rhs1: TRUE => a |-> b : leq
      b_in_o2c: b : Open2Closed(a,b)
        rhs1: TRUE => a |-> b : lt
      a_in_c2inf: a : Closed2Infinity(a)
        rhs1: TRUE => TRUE
      b_in_inf2c: b : Infinity2Closed(b)
        rhs1: TRUE => TRUE
END