Function TIME-POINT.HOUR


Slots on this function:

Documentation:
TIME-POINT.HOUR denotes an hour of a time point.
Instance-Of: Function
Arity: 2
Domain: Time-point
Range: Hour-number

Other Related Axioms:

(=> (Time-Point.Hour $X $Y) (Hour-Number $Y))

(=> (Time-Point.Hour $X $Y) (Time-Point $X))

(<=> (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))))

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