/* For each time interval1, there is at least one time interval2 that is a proper part of time interval1.*/
context: _'time interval'
inv: _'time interval'._'time interval1 is proper part of time interval2'-->notEmpty()

/* If a time interval1 overlaps a time interval2, then the time interval1 is not before the time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances-->    
    forAll(t2 | 
     self.overlaps(t2)
       implies not self._'is before'(t2))

/* If a time interval1 does not overlap a time interval2, then the time interval1 is before the time interval2 or the time interval2 is before the time interval1.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
    forAll(t2 | 
      not self.overlaps(t2) 
      implies (self._'is before:(t2) or 
               t2._'is before'(self)))

/* A given time interval is not before the time interval.*/
context _'time interval'
inv: not self._'is before'(self)

/* If a time interval1 is before a time interval2, then the time interval2 is not before the time interval1.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
    forAll(t2 | 
     self._'is before'(t2) 
        implies not t2._'is before'(self))

/* Each time interval1 overlaps each time interval2 and time interval1 is not before time interval2 and time interval2 is not before time interval1, or time interval1 is before time interval2 and time interval1 does not overlap time interval2 and time interval2 is not before time interval1, or time interval2 is before time interval1 and time interval1 does not overlap time interval2 and time interval1 is not before time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances-->
    forAll(t2 |
     (self.overlaps(t2) 
       and not self._'is before'(t2)
       and not t2._'is before'(self))
    or (self.
_'
is before'(t2)
        and not self.overlaps(t2)
        and not t2._'is before'(self))
    or (t2._'is before'(self)
        and not self.overlaps(t2)
        and not self._'is before'(t2)))

/* If a time interval1 is before a time interval2 and the time interval2 is before a time interval3 then the time interval1 is before the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-->
     forAll(t2, t3 |
       self._'is before'(t2)
       and t2._'is before'(t3)
       implies self._'is before'(t3))

/* the time interval1 is before the time interval2 and the time interval1 is before a time interval3 and the time interval3 is before the time interval2*/
context _'time interval'
def: _'time interval1 is properly before time interval2'
     (t2: _'time interval')
     : Boolean = 
     self._'is before'(t2) and
     'time interval'.allInstances-->exists(t3 |
       self._'is before'(t3) and t3._'is before'(t2))

/* the time interval1 is part of the time interval2 and the time interval2 is part of the time interval1*/
context _'time interval'
def: _'time interval1 equals time interval2'
      (t2: _'time interval)
      : Boolean =
     self._'is part of'(t2) and t2._'is 
                       part of'(self)

/* the time interval1 is before the time interval2 and the time interval1 is not before a time interval3 that is before the time interval2*/
context _'time interval'
def: _'time interval1 meets time interval2'
     (t2: _'time interval')
     : Boolean = 
     self._'is before'(t2) and
     not _'time interval'.allInstances-->
       exists(t3 |
           self._'is before'(t3)
           and t3_.'is before'(t2))

/* the time interval1 overlaps the time interval2 and a time interval3 is a proper part of the time interval1 and the time interval3 is before the time interval2*/
context _'time interval'
def: _'time interval1 properly overlaps time interval2'
     (t2: _'time interval')
     : Boolean = 
     self.overlaps(t2) and
     'time interval'.allInstances--> 
       exists(t3 |
       t3._'is a proper part of'(self)
       and t3._'is before'(t2))

/* the time interval1 is a proper part of the time interval2 and a time interval3 is a proper part of the time interval2 and a time interval4 is a proper part of the time interval2 and the time interval3 is before the time interval1 and the time interval1 is before the time interval4*/
context _'time interval'
def: _'time interval1 is properly during time interval2'
     (t2: _'time interval')
     : Boolean = 
     self._'is a proper part of'(t2) and
     'time interval'.allInstances--> 
         exists(t3, t4 |
          t3._'is a proper part of'(t2) and 
          t4._'is a proper part of'(t2) and
          t3._'is before'(self)
          and self._'is before'(t4))

/* time interval1 is a proper part of time interval2 and there exists no time interval3 that is a proper part of time interval2 and that is before time interval1*/
context _'time interval'
def: _'time interval1 starts time interval2'
     (t2: _'time interval')
     : Boolean = 
     self._'is a proper part of'(t2) and
     not 'time interval'.allInstances--> 
       exists(t3 |
          t3._'is a proper part of'(t2)
          and t3._'is before'(self))

/* time interval1 is a proper part of time interval2 and there exists no time interval3 that is a proper part of time interval2 and that is after time interval1*/
context _'time interval'
def: _'time interval1 finishes time interval2'
     (t2: _'time interval')
     : Boolean = 
     self._'is a proper part of'(t2) and
     not _'time interval'.allInstances--> 
       exists(t3 |
          t3._'is a proper part of'(t2)
          and self._'is before'(t3))

/* the time interval1 is properly before the time interval2 or the time interval1 meets the time interval2*/
context _'time interval'
def: _'time interval1 precedes time interval2'
     (t1: _'time interval', t2: _'time interval')
     : Boolean = 
     t1._'is properly before'(t2) or t1.meets(t2)

/* the time interval1 equals the time interval2 or the time interval1 meets the time interval2 or the time interval1 properly overlaps the time interval2 or the time interval1 starts the time interval2*/
context _'time interval'
def: _'time interval1 begins time interval2'
     (t1: _'time interval', t2: _'time interval')
     : Boolean = 
     t1.equals(t2) or 
     t1.meets(t2) or
     t1._'properly overlaps'(t2)
     t1.starts(t2)

/* the time interval1 equals the time interval2 or the time interval2 meets the time interval1 or the time interval2 properly overlaps the time interval1 or the time interval1 finishes the time interval2*/
context _'time interval'
def: _'time interval1 ends time interval2'
     (t1: _'time interval', t2: _'time interval')
     : Boolean = 
     t1.equals(t2) or 
     t2.meets(t1) or
     t2._'properly overlaps'(t1)
     t1.finishes(t2)

/* time interval1 is before time interval2 or time interval1 properly overlaps time interval2 or time interval1 starts time interval2 */
context _'time interval'
def: _'time interval1 begins before time 
      interval2' 
    (ti2:_ 'time interval')
    : Boolean =
    self._'is before'(ti2)
     or self.overlaps(ti2)
     or self.starts(ti2)

/* Each time interval begins before the time interval.*/
context _'time interval'
inv: self._'time interval1 begins before 
           time interval2'(self)

/* time interval1 is after time interval2 or time interval1 is properly overlapped by time interval2 or time interval1 ends time interval2*/
context _'time interval'
def: _'time interval1 ends after time 
      interval2' 
    (ti2: _'time interval')
    : Boolean =
    self._'is after'(ti2)
     or ti2._'properly overlaps'(self)
     or self.ends(ti2)

/* Each time interval ends after the time interval.*/
context _'time interval'
inv: self._'time interval1 ends after 
           time interval2'(self)

/* time interval1 follows time interval2 and  time interval1 precedes time interval3 */
context _'time interval'
def: _'time interval1 is between time 
      interval2 and time interval3'
     (t2: _'time interval',
      t3: _'time interval')
     : Boolean = 
     t2.precedes(self)
     and self.precedes(t3)

/* if the time interval1 includes the time interval2, then the time interval3 equals the time interval1*/
context _'time interval'
def: plus(t2: _'time interval')
      : _'time interval' =
    if self._'is before'(t2)
       or self._'properly overlaps'(t2)
      then _'time interval'.allInstances--> 
            exists(t3 | self.starts(t3)
             and t2.finishes(t3))
      else if t2._'is before'(self)
         or t2._'properly overlaps'(self)
      then _'time interval'.allInstances-->
            exists(t3 | t2.starts(t3)
             and self.finishes(t3))
      else if self._'part of'(t2)
      then t2
      else self
     endif

/* For each time interval1 and each time interval2, there is a time interval3 that is time interval1 plus time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances-->forAll(t2 |
'time interval'.allInstances-->exists(t3 |
self._'time interval1 plus time interval2 is time interval3'(t2, t3)))

/* If a time interval1 is part of a time interval3 and a time interval2 is part of the time interval3 then the time interval1 plus the time interval2 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
     forAll(t2, t3 |
      (self._'is part of'(t3)
         and t2._'is part of'(t3))
      implies self.plus(t2).
              'is part of'(t3))

/* A time interval1 plus a time interval2 is exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-->
    forAll(t2 |
      'time interval'.allInstances-->
       one(t4 | t4 = 
       self.plus(t2)))

/* time interval1 meets time interval2 and time interval3 is time interval1*/
context _'time interval'
def: _'to time interval'
      (t2: _'time interval')
      : _'time interval' =
     (self._'is properly before(t2) 
       implies self.plus(_'time interval'.  
         allInstances--> exists(t4 | 
          t4.meets(t2)
          and self.meets(t4))))
  or (self.meets(t2) implies self))

/* if the time interval1 starts the time interval2 then the time interval3 finishes the time interval2 and the time interval1 meets the time interval3*/
context _'time interval'
def: _'minus starting interval'
  (t2: _'time interval', 
   t3: _'time interval')
  : Boolean =
  t2.starts(self)
  implies t3.finishes(t2)
   and self.meets(t3)

/* If a time interval1 starts a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
     forAll(t2, t3, t4 | 
     (t3 = 
       t2._'minus starting interval'(self)
     and (t4._'is part of'(t2)
     and not t4.overlaps(self))
     implies t4._'is part of'(t3)))

/* If a time interval1 starts a time interval2 then the time interval1 starts the time interval2 complementing exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances --> 
     forAll(t2 |
      'time interval'.allInstances -->
       isUnique(t2._'minus starting 
                interval'(self))

/* if the time interval1 finishes the time interval2 then the time interval3 starts the time interval2 and the time interval1 is met by the time interval3*/
context _'time interval'
def: _'minus finishing interval'
  (t2: _'time interval', 
   t3: _'time interval')
  : Boolean =
  t2.finishes(self)
  implies t3.starts(t2)
   and t3.meets(self)

/* If a time interval1 finishes a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
     forAll(t2, t3, t4 | 
     (t3 = 
       t2._'minus finishing interval'(self)
     and (t4._'is part of'(t2)
     and not t4.overlaps(self))
     implies t4_.'is part of'(t3)))

/* If a time interval1 finishes a time interval2 then the time interval1 finishes the time interval2 complementing exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances --> 
     forAll(t2 |
      'time interval'.allInstances -->
       isUnique(t2._'minus finishing 
                interval'(self))

/* For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
      forAll(t2 | t2._'is properly 
                      during'(self)                                                     
      implies _'time interval'.allInstances
       --> exists(t3 | t3.starts(self) 
           and t3.meets(t2)))

/* For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
       forAll(t2 | t2._'is properly 
                       during'(self)
         implies _'time interval'.
             allInstances--> exists(t3 | 
             t3.ends(self) 
              and t2.meets(t3)))

/* if the time interval1 overlaps the time interval2, then the time interval3 finishes the time interval1 and starts the time interval2*/
context _'time interval'
def: _'intersected with '
      (t2: _'time interval')
      : _'time interval' =
      self.overlaps(t2)
      implies 
       'time interval'.allInstances-->
        exists(t3 | t3.finishes(self)
         and t3.starts(t2))

/* If a time interval1 intersects a time interval2 with a time interval3 and a time interval4 is part of the time interval1 and the time interval4 is part of the time interval2, then the time interval4 is part of the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances--> 
     forAll(t2, t3, t4 |
        (self.overlaps(t2)
        and t4._'is part of'(self)
        and t4_.'is part of'(t2))
       implies
        t4._'is part of'(
          self._'intersected with'(t2)))

/* If a time interval1 overlaps a time inteval2, then the time interval1 intersects a time interval2 with exactly one time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-->forAll(t2 |
      self.overlaps(t2) implies
      'time interval'.allInstances-->
      isUnique(self._'intersected 
                     with'(t2)))

/* If a time interval1 is properly before a time interval2 then the time interval1 meets a time interval3 and the time interval3 meets the time interval2 and the time interval1 plus the time interval2 is a time interval4 and the time interval1 starts the time interval4 complementing a time interval5 and the time interval2 finishes the time interval4 complementing a time interval6 and the time interval5 intersects the time interval6 with the time interval3.*/
context _'time interval'
inv: _'time interval'.allInstances-->   
    forAll(t2|
     self._'is properly before'(t2)
     implies
     'time interval'.allInstances--> 
       exists(t3, t4, t5, t6|
        self.meets(t3)
        and t3.meets(t2)
        and t4 = self.plus(t2)
        and t5 = t4._'minus starting 
                     interval'(self)
        and t6 = t4._'minus finishing
                     interval(t2)
        and t3 = t5._'intersected 
                     with"(t6)))

/* Each duration ≤ the duration.*/
context duration
inv: self._'is less or equal'(self))

/* Each duration1 ≤ each duration2 or duration2 ≤ duration1.*/
context duration
inv: duration.allInstances-->forAll(d2 |
     self._'is less or equal(d2)
     or d2._'is less or equal'(self)

/* If some duration1 ≤ some duration2 and the duration2 ≤ the duration1, then the duration1 equals the duration2.*/
context duration
inv: duration.allInstances-->forAll(d2 |
     self._'is less or equal'(d2)
     and d2._'is less or equal'(self)
     implies self = d2)

/* If some duration1 ≤ some duration2 and the duration2 ≤ the duration3 then the duration1 ≤ the duration3.*/
context duration
inv: duration.allInstances-->forAll(d2, d3 |
    self._'is less or equal'(d2)
    and d2._'is less or equal(d3)
    implies self._'is less or equal'(d3))

/* duration1 ≤ duration2 and duration1 does not equal duration2 */
context duration
def: _'is less than'(d2: duration)
     : Boolean =
     self._'is less or equal'(d2)
     and not self.equals(d2)

/* If a duration4 equals a duration1 plus a duration2, and a duration5 equals duration4 plus duration3, and a duration6 equals duration2 plus duration3, then duration5 equals duration1 plus duration6.*/
context duration
inv: duration.allInstances-->
   forAll(d2, d3 |
     (self._'plus duration'(d2)
      ._'plus duration'(d3))
       .equals(self._'plus duration'
         (d2._'plus duration'(d3))))

/* Each duration1 plus duration2 equals duration2 plus duration1.*/
context duration
inv: duration.allInstances-->forAll(d2 |
     self._'plus duration'(d2).equals
     (d2._'plus duration'(self)))

/* Each duration1 plus duration2 equals duration2 plus duration1.*/
context duration
inv: self = self._'plus duration'(D0):

/* D0 equals each duration1 plus some duration2.*/
context duration
inv: duration.allInstances-->exists(d2 |
      D0 = self + d2)

/* For each number and each duration1, there is a duration2 that is number times duration1.*/
context duration
inv: Integer.allInstances-->forAll(n |
     self._'times number'(n)
      .oclIsKindOf(duration))

/* If a duration3 equals a number1 times (a duration1 plus a duration2) then duration3 equals (number1 times duration1) plus (number1 times duration2).*/
context duration
inv: duration.allInstances-->forAll(d2 |
     Integer.allInstances-->forAll(n |
     self._'plus duration'(d2)
      ._'times number'(n).equals(
        self._'times number'(n)
         .self._'plus duration'(
           d2._'times number'(n)))))

/* If a (number1 plus a number2) times a duration1 equals a duration2, then duration2 equals (number1 times duration1) plus (number2 times duration1).*/
context duration
inv: Integer.allInstances-->
 forAll(n1, n2 |
  self._'times number'(n1 + n2).equals(
   self._'times number'(n1)._'plus duration'
    (self_.'times number'(n2))))

/* Each time interval has exactly one duration.*/
context _'time interval'
self._'particular duration'-->size() = 1

/* The duration of each time interval is greater than D0.*/
context _'time interval'
inv: self.duration > D0

/* The duration of no time interval equals D0.*/
context _'time interval'
inv: not self.duration = D0

/* For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0.*/
context _'time interval'
inv: _
'time interval'.allInstances-->forAll(t2 |
  not ((self.duration() + t2.duration()) = D0))

/* For each time interval1 and each time interval2 that is a part of time interval1, the duration of time interval2 is less than or equal to the duration of time interval1.*/
context _'time interval'
'time interval'.allInstances-->forAll(t2 |
  self._'is part of'(t2)
  implies self_.'particular duration'
            .'is less than'(
                d2._'particular duration'))

/* For each time interval1 and each time interval2 that meets a time interval1, the duration of  time interval1 plus time interval2 is equal to the duration of time interval1 plus the duration of time interval2.*/
context _'time interval'
'time interval'_.allInstances-->forAll(t2 |
  self.meets(t2)
  implies self.plus(t2)._'particular duration'
   .equals(self._'particular duration'
    ._'plus duration'(t2._'particular duration')))

/* For each time interval2 and each time interval3 that finishes time interval2, the duration of  the time interval1 that starts time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.*/
context "time interval1 starts time interval2 
         complementing time interval3"
inv: self."time interval1".duration = 
     self."time interval2".duration - 
     self."time interval3".duration

/* For each time interval2 and each time interval3 that finishes time interval2, the duration of  the time interval1 that starts time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.*/
context _'time interval'
'time interval'.allInstances-->forAll(t2 |
  self.starts(t2)
  implies t2._'minus starting 
             interval'(self)
    ._'particular duration'.equals(
      t2._'particular duration'.
          'minus duration'(
       self._'particular duration')))

/* For each time interval2 and each time interval3 that starts time interval2, the duration of  the time interval1 that finishes time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.*/
context _'time interval1 finishes time 
    interval2 complementing time interval3'
inv: self._'time interval1'.duration = 
     self._'time interval2'.duration - 
     self._'time interval3'.duration

/* For each time interval2 and each time interval3 that starts time interval2, the duration of  the time interval1 that finishes time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.*/
context _'time interval'
'time interval'.allInstances-->forAll(t2 |
  self.finishes(t2)
  implies t2._'minus finishing interval'(self)
    ._'particular duration'.equals(
      t2._'particular duration'._'minus duration'(
       self._'particular duration')))

/* Duration  D0.*/
context _'time interval'
def: _'is duration before'
     (d: duration)
     : _'time interval' = 
     'time interval'.allInstances-->
         exists(t2, t3 |
          t2._'is before'(self)
          and t2.meets(t3)
          and t3.meets(self)
          and t3._'particular duration'
                .equals(d))

/* Duration  D0.*/
context _'time interval'
def: _'is duration after'
     (d: duration)
     : _'time interval' = 
     'time interval'.allInstances-->
         exists(t2, t3 |
          t2._'is after'(self)
          and self.meets(t3)
          and t3.meets(t2)
          and t3_.'particular duration'
                .equals(d))

/* the occurrence occurs throughout some time interval2 that is part of the time interval*/
context _'occurrence'
def: _'occurrence occurs within time interval'
      (t: _'time interval') : Boolean
      t._'part of'-->exists(t2 | 
        self._'occurrence occurs throughout
         time interval'(t2))

/* the occurrence occurs throughout the occurrence interval and the occurrence does not occur within some time interval2 that meets the occurrence interval and the occurrence does not occur within some time interval3 that is met by the occurrence interval*/
context _'occurrence'
def: _'occurrence occurs for time interval'
     (t: _'time interval') : Boolean
     self._'occurrence occurs throughout time interval'
       (t)
     and self._'is met by'-->forAll(t2 |
         not self._'occurrence occurs throughout
                   time interval'(t2))
     and self._'meets"-->forAll(t3 |
         not self._'occurrence occurs throughout
                   time interval'(t3))

/* the occurrence occurs for some occurrence interval and the duration is the duration of the occurrence interval*/
context _'occurrence'
def: _'occurrence lasts for duration'(d: duration)
     : Boolean
     self._'occurrence occurs for time interval')
       .duration = d

/* the occurrence interval of occurrence1 precedes the occurrence interval of occurrence2*/
context _'occurrence'
def: _'occurrence1 precedes occurrence2'
     (o2: _'occurrence') : Boolean
     self._'occurs for' < o2._'occurs for'

/* If some occurrence1 precedes some occurrence2, and if the occurrence2 precedes some occurrence3, then occurrence1 precedes occurrence3.*/
context _'occurrence'
inv: self._'precedes'-->exists(o2 | 
       o2._'precedes'-->exists(o3 | implies 
        self._'precedes'-->contains(o3)))

/* the occurrence interval of occurrence1 starts before the occurrence interval of occurrence2*/
context _'occurrence'
def: _'occurrence1 starts before occurrence2'
     (o2: _'occurrence') : Boolean
  self._'occurs for'.
   'time interval starts before time interval'(o2._'occurs for')

/* the occurrence interval of occurrence1 ends before the occurrence interval of occurrence2  */
context _'occurrence'
def: _'occurrence1 ends before occurrence2'
     (o2: _'occurrence') : Boolean
  self._'occurs for'.
   'time interval ends before time interval'(o2._'occurs for')

/* the occurrence interval of occurrence1 overlaps the occurrence interval of occurrence2*/
context _'occurrence'
def: _'occurrence1 overlaps occurrence2'
      (o2: _'occurrence') : Boolean
      self._'occurs for'._overlaps(o2._'occurs for')

/* each occurrence of situation kind1 precedes each occurrence of situation kind2  */
context _'situation kind'
def: _'situation kind1 precedes situation kind2'
     (s2: _'situation kind') : Boolean
     self._'occurrence'.precedes(s2._'occurrence')

/* each occurrence of situation kind1 starts before each occurrence of situation kind*/
context _'situation kind'
def: _'situation kind1 precedes situation kind2'
     (s2: _'situation kind') : Boolean
     self.occurrence._'starts before'(s2.occurrence)

/* each occurrence of situation kind1 ends before each occurrence of situation kind2 */
context _'situation kind'
def: _'situation kind1 precedes situation kind2'
     (s2: _'situation kind') : Boolean
     self.occurrence._'ends before'(s2.occurrence)

/* each occurrence of situation kind1 overlaps some occurrence of situation kind2*/
context _'situation kind' 
def: _'situation kind1 overlaps
      situation kind2' 
     (s2: _'situation kind') : Boolean  
     self._'occurrence'.overlaps 
        (s2._'occurrence')

/* each table entry of the time table is the occurrence interval of some individual situation kind that is a member of the schedule*/
context _'schedule'
def: _'schedule has time table'(t: _'time table')
     : Boolean = 
     t._'table entry'-->forAll(te |
       self.member-->exists(i | 
        i._'individual situation kind occurs over time 
           interval'(te)))

/* the time table period of the time table of the schedule.*/
context schedule
def: _'schedule has time span'(t: time interval)
     : Boolean
     self._'time table'._'time table period' == t

/* If the index1 of some sequence position1 of some sequence equals the index2 of some sequence position2 of the sequence then sequence position1 is sequence position2.*/
context sequence:
inv: self._'sequence position'-->forAll(sp1 | 
      self._'sequence position'-->forAll(sp2 | 
       indexOf(sp1) = indexOf(sp2) implies sp1 = sp2))

/* Each sequence position has at most one next sequence position. */
context _'sequence position'
inv: self._'sequence position1 precedes sequence position2'
      ( self._'next sequence position')
     and self._'sequence position2'-->forAll(sp2 |
         self._'next sequence position'.index <= sp2.index)

/* the member is the member of a sequence position of the sequence*/
context sequence
def: _'member participates in sequence'
     (member: thing, s: sequence)
     : Boolean = 
     self._'sequence position'-->exists(sp | 
      sp.member = member)

/* The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.*/
context sequence
def: _'member has index in sequence'
     (member: thing, i: integer, s: sequence)
     : Boolean =
     self._'sequence position'-->exists(sp | 
       sp.index = index and sp.member = member)

/* The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.*/
context sequence 
def: _'index of member in sequence'
      (member: thing, s sequence) 
      : integer =
      self._'sequence position'-->select(sp | 
       sp.member = member).index

/* The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.*/
context sequence
def: _'member with index in sequence'
                     (index: integer, s sequence)
     : thing =
     self._'sequence position'-->select(sp | 
       sp.index = index).member

/* The concept corresponds to each member of the sequence.*/
context sequence
def: _'sequence is of concept'(c: concept) 
      : Boolean =
     sequence._'sequence position'.member-->forAll(m | 
                  'concept corresponds to instance'(c m))

/* The index of the index origin position equals the index origin value of the sequence.*/
context sequence
inv: sequence._'index origin value' = 
       sequence._'index origin position'.index

/* sequence that each sequence position of the sequence that is not the first position of the sequence is next after a sequence position2, and the index of the sequence position equals 1 plus the index of the sequence position2*/
context _'consecutive sequence'
inv: self._'sequence position'-->forAll(sp |
      not (self._'first position'-->exists()
        and sp = self._'first position')
        implies self._'sequence position'.indexOf(sp) =
          1 + self._'sequence position' 
              -->indexOf(sp._'previous sequence position'))

/* sequence that each member of the sequence is the member of at most one sequence position of the sequence*/
context sequence
inv: self.member-->forall(m | 
        self._'sequence position'.member-->isUnique (m2 |
           m = m2))

/* member1 participates in the unique sequence and member2 participates in the unique sequence and each sequence position1 of member1 in the unique sequence precedes each sequence position2 of member2 in the unique sequence*/
context sequence
def: _'member1 precedes member2 in unique sequence'
     (m1: thing, m2: thing) : Boolean =
    self.member-->includes(m1)
      and self.member-->includes(m2)
      and m1._'sequence position'-->forall(sp1 |
           m2._'sequence position'-->forall(sp2 |
            'sequence position1 precedes 
               sequence position2'(sp1, sp2)))

/* the first member is the member of the first position of the sequence*/
context _'sequence'
def: _'sequence has first member'
      (s: _'sequence') : thing =
     self._'first position'.member

/* the last member is the member of the last position of the sequence*/
context _'sequence'
def: _'sequence has last member
      (s: sequence) : thing = 
      self._'last position'.member

/* thing is the member of exactly one sequence position in the unique sequence and next member is the member of some sequence position of the unique sequence that succeeds the sequence position of the thing*/
context "unique sequence"
def: "next member is next after member in unique sequence"
      (nm: thing, m: thing) : Boolean =
      self."sequence position".member-->count(m) = 1
      and self."sequence position"-->select(member = m).
        "next sequence position".member = nm

/* The last member of each sequence has no next member.*/
context sequence
inv: self._'last member'-->exists() implies
     not self._'last member'._'next member'-->exists()

/* Each member that participates in a unique sequence and that has no next member in the unique sequence is the last member of the unique sequence.*/
context _'unique sequence'
inv: self.member-->forAll(m |
       not m._'next member'-->exists()
           implies m = self._'last member')

/* thing is the member of exactly one sequence position in the unique sequence and previous member is the member of some sequence position of the unique sequence that is just before the sequence position of the thing*/
context _'unique sequence'
def: _'previous member is just before member in unique 
      sequence'(pm: thing, m: thing) : Boolean =
      self._'sequence position'.member-->count(m) = 1
      and self._'sequence position'-->select(member = m).
        'previous sequence position'.member = pm

/* The first member of each sequence has no previous member.*/
context sequence
inv: self._'first member'-->exists() implies
     not self._'first member'._'previous member'-->exists()

/* Each member that participates in a unique sequence and that has no previous member in the unique sequence is the first member of the unique sequence.*/
context _'unique sequence'
inv: self.member-->forAll(m |
       not m._'previous member'-->exists()
           implies m = self._'first member')

/* Each part is part of the part.*/
context thing
inv: self.part-->exists(self)

/* If the part is part of the whole and the whole is part of the part then the part is the whole.*/
context thing
inv: self.whole-->exists(p | 
                  p.whole -->exists(self))
     implies self = self.whole

/* If the part is part of some whole and the whole is part of some part3 then the part is part of part3.*/
context thing
inv: self.whole-->exists(whole |
      whole.whole-->exists(part3 |
       part3 implies self._'part of'(part3)))

/* There exists a part3 that is part of the part1 and the part3 is part of the part2.*/
context thing
inv: self.overlap-->forAll(part2 |
      self.part-->exists(part3 |
       part2.part-->exists(part3)))

/* the part is part of the whole and the whole is not part of the part*/
context thing
inv: self._'proper part'-->forall(pp | 
      pp <> self)

/* If a part1 is a proper part of a whole then there exists a part2 that is a proper part of the whole and part2 does not overlap part1.*/
context thing
inv: self._'proper part'-->forAll(part1 |
      self._'proper part'-->exists(part2 |
        not part2.overlaps(part1)))