Relation TP=

• Defined in theory: Jat-generic
• Source code: job-assignment-generic.lisp

Slots on this relation:

Documentation:

a time point ?tp1 is equal to a time point ?tp2.

Instance-Of: Relation

Arity: 2

Equivalence Axioms:

(<=> (Tp= ?Tp1 ?Tp2)
     (And (= (Time-Point.Year ?Tp1) (Time-Point.Year ?Tp2))
          (= (Time-Point.Month ?Tp1) (Time-Point.Month ?Tp2))
          (= (Time-Point.Day ?Tp1) (Time-Point.Day ?Tp2))
          (= (Time-Point.Hour ?Tp1) (Time-Point.Hour ?Tp2))
          (= (Time-Point.Minute ?Tp1) (Time-Point.Minute ?Tp2))
          (= (Time-Point.Second ?Tp1) (Time-Point.Second ?Tp2))))

Other Related Axioms:

(Tp= (Tp+ (Time-Range.Start-Time ?Time-Range)
          (Time-Range.Duration ?Time-Range))
     (Time-Range.End-Time ?Time-Range))

(=> (Time-Range ?Time-Range)
    (Tp= (Tp+ (Time-Range.Start-Time ?Time-Range)
              (Time-Range.Duration ?Time-Range))
         (Time-Range.End-Time ?Time-Range)))

(<=> (Meets ?Tr1 ?Tr2)
     (Tp= (Time-Range.Start-Time ?Tr1) (Time-Range.Start-Time ?Tr2)))

(<=> (Equals ?Tr1 ?Tr2)
     (And (Tp= (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp= (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (Starts ?Tr1 ?Tr2)
     (And (Tp= (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp< (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (Finishes ?Tr1 ?Tr2)
     (And (Tp> (Time-Range.Start-Time ?Tr1)
               (Time-Range.Start-Time ?Tr2))
          (Tp= (Time-Range.End-Time ?Tr1) (Time-Range.End-Time ?Tr2))))

(<=> (Tp= ?Tp1 ?Tp2)
     (And (= (Time-Point.Year ?Tp1) (Time-Point.Year ?Tp2))
          (= (Time-Point.Month ?Tp1) (Time-Point.Month ?Tp2))
          (= (Time-Point.Day ?Tp1) (Time-Point.Day ?Tp2))
          (= (Time-Point.Hour ?Tp1) (Time-Point.Hour ?Tp2))
          (= (Time-Point.Minute ?Tp1) (Time-Point.Minute ?Tp2))
          (= (Time-Point.Second ?Tp1) (Time-Point.Second ?Tp2))))