Function Minute-Of

Instance-Of:
Binary-Relation, Function, Relation, Set
Domain: Time-Point
Range: Minute-Number
Arity: 2
Documentation: MINUTE-OF denotes a minute of a time point.

Implication Axioms mentioning Minute-Of:

(=> (Equals ?Time-Point-1 ?Time-Point-2)
    (=> (And (Time-Point ?Time-Point-1) (Time-Point ?Time-Point-2))
        (<=> (Equals ?Time-Point-1 ?Time-Point-2)
             (And (= (Year-Of ?Time-Point-1) (Year-Of ?Time-Point-2))
                  (= (Month-Of ?Time-Point-1)
                     (Month-Of ?Time-Point-2))
                  (= (Day-Of ?Time-Point-1) (Day-Of ?Time-Point-2))
                  (= (Hour-Of ?Time-Point-1) (Hour-Of ?Time-Point-2))
                  (= (Minute-Of ?Time-Point-1)
                     (Minute-Of ?Time-Point-2))
                  (= (Second-Of ?Time-Point-1)
                     (Second-Of ?Time-Point-2))))))

(=> (< ?Time-Point-1 ?Time-Point-2)
    (=> (And (Time-Point ?Time-Point-1) (Time-Point ?Time-Point-2))
        (<=> (< ?Time-Point-1 ?Time-Point-2)
             (Or (< (Year-Of ?Time-Point-1) (Year-Of ?Time-Point-2))
                 (And (= (Year-Of ?Time-Point-1)
                         (Year-Of ?Time-Point-2))
                      (Or (< (Month-Of ?Time-Point-1)
                             (Month-Of ?Time-Point-2))
                          (And (= (Month-Of ?Time-Point-1)
                                  (Month-Of ?Time-Point-2))
                               (Or (< (Day-Of ?Time-Point-1)
                                      (Day-Of ?Time-Point-2))
                                   (And (= (Day-Of ?Time-Point-1)
                                           (Day-Of ?Time-Point-2))
                                        (Or (< (Hour-Of ?Time-Point-1)
                                               (Hour-Of ?Time-Point-2))
                                            (And (= (Hour-Of ?Time-Point-1)
                                                    (Hour-Of ?Time-Point-2))
                                                 (Or (< (Minute-Of ?Time-Point-1)
                                                        (Minute-Of ?Time-Point-2))
                                                     (And (= (Minute-Of ?Time-Point-1)
                                                             (Minute-Of ?Time-Point-2))
                                                          (< (Second-Of ?Time-Point-1)
                                                             (Second-Of ?Time-Point-2)))))))))))))))