Function Start-Time-Of

Instance-Of:
Binary-Relation, Function, Relation, Set
Domain: Time-Range
Range: Time-Point
Arity: 2
Documentation: (START-TIME-OF 'tr) denotes a start time of a time range tr.

Implication Axioms mentioning Start-Time-Of:

(=> (And (Time-Range ?Time-Range-1) (Time-Range ?Time-Range-2))
    (<=> (Equals ?Time-Range-1 ?Time-Range-2)
         (And (Equals (Start-Time-Of ?Time-Range-1)
                      (Start-Time-Of ?Time-Range-2))
              (Equals (End-Time-Of ?Time-Range-1)
                      (End-Time-Of ?Time-Range-2)))))

(=> (Time-Range ?Time-Range)
    (Equals (+ (Start-Time-Of ?Time-Range) (Duration-Of ?Time-Range))
            (End-Time-Of ?Time-Range)))

(=> (During ?Time-Range-1 ?Time-Range-2)
    (> (Start-Time-Of ?Time-Range-1) (Start-Time-Of ?Time-Range-2)))

(=> (Overlaps ?Time-Range-1 ?Time-Range-2)
    (< (Start-Time-Of ?Time-Range-2) (End-Time-Of ?Time-Range-1)))

(=> (Overlaps ?Time-Range-1 ?Time-Range-2)
    (< (Start-Time-Of ?Time-Range-1) (Start-Time-Of ?Time-Range-2)))


Equivalence Axioms mentioning Start-Time-Of:

(<=> (Before ?Time-Range-1 ?Time-Range-2)
     (< (End-Time-Of ?Time-Range-1) (Start-Time-Of ?Time-Range-2)))

(<=> (After ?Time-Range-1 ?Time-Range-2)
     (< (End-Time-Of ?Time-Range-2) (Start-Time-Of ?Time-Range-1)))

(<=> (Meets ?Time-Range-1 ?Time-Range-2)
     (Equals (End-Time-Of ?Time-Range-1)
             (Start-Time-Of ?Time-Range-2)))

(<=> (During ?Time-Range-1 ?Time-Range-2)
     (And (> (Start-Time-Of ?Time-Range-1)
             (Start-Time-Of ?Time-Range-2))
          (< (End-Time-Of ?Time-Range-1) (End-Time-Of ?Time-Range-2))))

(<=> (Overlaps ?Time-Range-1 ?Time-Range-2)
     (And (< (Start-Time-Of ?Time-Range-1)
             (Start-Time-Of ?Time-Range-2))
          (< (Start-Time-Of ?Time-Range-2)
             (End-Time-Of ?Time-Range-1))
          (< (End-Time-Of ?Time-Range-1) (End-Time-Of ?Time-Range-2))))