Function TIME-RANGE-UNIT

• Defined in theory: Job-assignment-task
• Source code: job-assignment-task.lisp

Slots on this function:

Documentation:

A time-range class of discrete-time-range-class has its own minimun unit of duration.

Instance-Of: Function

Arity: 2

Domain: Discrete-time-range-class

Range: Duration

Other Related Axioms:

(Forall (?I)
        (=> (Instance-Of ?I ?Class)
            (And (Measured-By (Time-Range.Start-Time ?I)
                              (Time-Range-Unit ?Class))
                 (Measured-By (Time-Range.End-Time ?I)
                              (Time-Range-Unit ?Class)))))

(Inherited-Facet-Value Slot-Cardinality
                       Discrete-Time-Range-Class
                       Time-Range-Unit
                       1)

(<=> (Discrete-Time-Range-Class ?Class)
     (And (Class ?Class)
          (Value-Cardinality ?Class Time-Range-Unit 1)
          (Forall (?I)
                  (=> (Instance-Of ?I ?Class)
                      (And (Measured-By (Time-Range.Start-Time ?I)
                                        (Time-Range-Unit ?Class))
                           (Measured-By (Time-Range.End-Time ?I)
                                        (Time-Range-Unit ?Class)))))))

(=> (Time-Range-Unit $X $Y) (Duration $Y))

(=> (Time-Range-Unit $X $Y) (Discrete-Time-Range-Class $X))

(Forall (?I)
        (=> (Instance-Of ?I ?Class)
            (= (Time-Range.Duration ?I) (Time-Range-Unit ?Class))))

(<=> (Unit-Time-Range-Class ?Class)
     (And (Discrete-Time-Range-Class ?Class)
          (Forall (?I)
                  (=> (Instance-Of ?I ?Class)
                      (= (Time-Range.Duration ?I)
                         (Time-Range-Unit ?Class))))))