;;; There are several domains defined in 
;;; daml-time.opt,  daml-time-event.opt, and daml-time-aggregates.opt:
;;;    daml-time-axis -- basics
;;;    daml-time-inf-points -- Assuming points at infinity
;;;    daml-time-inf-intervals -- Assuming infinite interval
;;;    daml-time-event -- associations between Temporal-entities
;;;        and things that change truth value over time
;;;    daml-time-axis-measure -- seconds, minutes, hath, etc.
;;;    daml-clock-calendar -- dates and such
;;;    daml-time-granularity -- granularity
;;;    daml-temporal-aggegates -- sequences of Temporal-entities

(define (domain set-theory)
   (:requirements :numbers)
   (:types Set)
   
   (:objects empty-set)

   (:predicates
       (member x - Object s - Set)
       (subset s1 s2 - Set)
      (cover s1 s2 - Set)

   )

   (:functions
       (card s - Set)
       - Integer
       
       (singleton x - Obj)
       (union s1 s2 - Set)
       (set-union s - Set) ;; s is a set of sets; (set-union s) is their union
       - Set
   )

   (:axioms
       (forall (x y)
          (iff (member y (singleton x))
               (= y x)))
      ;; Axiom "5.0-1"
      (forall (c s - Set)
         (if (cover c s)
             (forall (x)
                (iff (member x c)
                     (and (is Set x)
                          (subset x s))))))

      ;; Axiom "5.0-2"
      (forall (g s - Set)
         (iff (cover g s)
              (forall (x)
                 (iff (member x s)
                      (exists (s)
                         (and (member s g) (member x s)))))))

      ;; Axiom "5.0-3"
      (forall (g - Set)
         (and (cover g (set-union g))
              (forall (s - Set)
                 (if (cover g s)
                     (= s (set-union g))))))

   ))

(define (domain daml-time-axis)
   (:requirements :equality :fluents)
   (:extends set-theory)

   (:types Temporal-entity - Object
           Instant Interval - Temporal-entity  ;; Id "2.1-1, 2.1-2"
           Proper-interval - Interval)

   (:predicates
      (total-order)
      (totally-ordered-past)
      (pts-at-inf)
      (dense-time)
      (time-intervals-convex)
      (time-intervals-extensional)

      (begins t1 - Instant t2 - Temporal-entity)  ; Axiom "2.1-3"
      (ends t1 - Instant t2 - Temporal-entity)    ; Axiom "2.1-4"
      (begins-or-in t1 - Instant t2 - Temporal-entity) ;; Axiom "2.1-10"

      (inside t1 - Instant t2 - Temporal-entity)  ;; Axiom "2.1-9"

      (time-between tv - Temporal-entity ts1 ts2 - Instant) ;; Axiom "2.1-12"


      (before t1 t2 - Temporal-entity) ;; Axiom "2.2-1"
      (after t1 t2 - Temporal-entity)  ;; Axiom "2.2-2"

      (int-equals tp1 tp2 - Proper-interval)
      (int-before tp1 tp2 - Proper-interval)
      (int-after tp1 tp2 - Proper-interval)
      (int-meets tp1 tp2 - Proper-interval)
      (int-overlaps tp1 tp2 - Proper-interval)
      (int-starts tp1 tp2 - Proper-interval)
      (int-during tp1 tp2 - Proper-interval)
      (int-finishes tp1 tp2 - Proper-interval)
      (int-finished-by tp1 tp2 - Proper-interval)
      (int-contains tp1 tp2 - Proper-interval)
      (int-met-by tp1 tp2 - Proper-interval)
      (int-overlapped-by tp1 tp2 - Proper-interval)
      (int-started-by tp1 tp2 - Proper-interval)
      (starts-or-during tv1 tv2 - Proper-interval)
      (nonoverlap tv1 tv2 - Proper-interval)

      (posinf-interval int - Interval)
      (neginf-interval int - Interval)
      (halfinf-interval int - Interval)
      (inf-interval int - Interval)

      (concatenation int - Proper-interval s - Set)

    (posinf ti - Instant)
    (neginf ti - Instant)

   ))

(define (addendum instants-and-intervals)
   (:domain daml-time-axis)
   (:axioms
      (forall (ti - Instant)
         (and (begins ti ti)   ;; Axiom "2.1-5"
              (ends ti ti)))   ;; Axiom "2.1-6"


      ;; Axiom "2.1-7"
      (forall (ti1 ti2 - Instant te - Interval)
         (if (and (begins ti1 te) (begins ti2 te))
             (= ti1 ti2)))

      ;; Axiom "2.1-8"
      (forall (ti1 ti2 - Instant te - Interval)
         (if (and (ends ti1 te) (ends ti2 te))
             (= ti1 ti2)))

      ;; Axiom "2.1-11"
      (forall (ts - Instant tv - Interval)
         (iff (begins-or-in ts tv)
              (or (begins ts tv)
                  (inside ts tv))))
         

      ;; Axiom "2.1-13"
      (forall (tv - Interval ts1 ts2 - Instant)
         (iff (time-between tv ts1 ts2)
              (and (begins ts1 tv)
                   (ends ts2 tv))))

      ;; Axiom "2.1-14"
      (forall (tv - Interval)
         (iff (is Proper-interval tv)
              (not (exists (ti - Instant)
                      (and (begins ti tv) (ends ti tv))))))

   ))

(define (addendum before-stuff)
   (:domain daml-time-axis)

   (:axioms
      ;; Axiom "2.2-3"
      (forall (t1 t2 - Interval)
         (iff (before t1 t2)
              (exists (ti1 ti2 - Instant)
                 (and (ends ti1 t1) (begins ti2 t2)
                      (before ti1 ti2)))))

      ;; Axiom "2.2-4"
      (forall (t1 t2 - Temporal-entity)
         (if (before t1 t2) (not (= t1 t2))))

      ;; Axiom "2.2-5"
      (forall (t1 t2 - Temporal-entity)
         (if (before t1 t2) (not (before t2 t1))))

      ;; Axiom "2.2-6"
      (forall (t1 t2 t3 - Temporal-entity)
         (if (and (before t1 t2) (before t2 t3))
             (before t1 t3)))

      ;; Axiom "2.2-8"
      (forall (tv - Proper-interval ti1 ti2 - Instant)
         (if (and (begins ti1 tv)
                  (ends ti2 tv))
             (before ti1 ti2)))


      ;; Axiom "2.2-7"
      (forall (tv - Interval ti1 ti2 - Instant)
         (if (and (begins ti1 tv)
                  (ends ti2 tv))
             (not (before ti2 ti1))))

      ;; Axiom "2.2-9"
      (forall (t1 t2 - Instant)
         (if (before t1 t2)
             (exists (tv - Interval) (time-between tv t1 t2))))

      ;; Axiom "2.2-10
      (forall (ts - Instant tv - Interval b e - Instant)
         (if (inside ts tv)
             (and (if (begins b tv) (before b ts))
                  (if (ends e tv) (before ts e)))))

      ;; Axiom "2.2-11"
      (forall (t1 t2 - Temporal-entity)
         (iff (after t1 t2) (before t2 t1)))

   ))

(define (addendum interval-relations)
   (:domain daml-time-axis)

   (:axioms
      ;; Axiom "2.3-1"
      (forall (t1 t2 - Proper-interval)
         (iff (int-equals t1 t2)
              (and (forall (b - Instant)
                      (iff (begins b t1) (begins b t2)))
                   (forall (e - Instant)
                      (iff (ends e t1) (ends e t2))))))
      ;; Axiom "2.3-2"
      (forall (t1 t2 - Proper-interval)
         (iff (int-before t1 t2) (before t1 t2)))

      ;; Axiom "2.3-3"
      (forall (t1 t2 - Proper-interval)
         (iff (int-meets t1 t2)
              (exists (ti - Instant)
                 (and (ends ti t1) (begins ti t2)))))

      ;; Axiom "2.3-4"
      (forall (t1 t2 - Proper-interval)
         (iff (int-overlaps t1 t2)
              (exists (e1 b2 - Instant)
                 (and (ends e1 t1)
                      (begins b2 t2)
                      (before b2 e1)
                      (forall (b1 - Instant)
                         (if (begins b1 t1)
                             (before b1 b2)))
                      (forall (e2 - Instant)
                         (if (ends e2 t2)
                             (before e1 e2)))))))

      ;; Axiom "2.3-5"
      (forall (tv1 tv2 - Proper-interval)
         (iff (int-starts tv1 tv2)
              (exists (b e1 e2 - Instant)
                (and (begins b tv1) 
                     (begins b tv2)
                     (ends e1 tv1)
                     (ends e2 tv2)
                     (before e1 e2)))))

      ;; Axiom "2.3-6"
      (forall (tv1 tv2 - Proper-interval)
         (iff (int-during tv1 tv2)
              (exists (e1 b1 e2 b2 - Instant)
                 (and (begins b1 tv1)
                      (ends e1 tv1)
                      (begins b2 tv2)
                      (ends e2 tv2)
                      (before b2 b1)
                      (before e1 e2)))))

      ;; Axiom "2.3-7"
      (forall (tv1 tv2 - Proper-interval)
         (iff (int-finishes tv1 tv2)
              (exists (b1 b2 e - Instant)
                 (and (ends e tv1)
                      (ends e tv2)
                      (begins b1 tv1)
                      (begins b2 tv2)
                      (before b2 b1)))))

      ;; Axiom "2.3-8"
      (forall (t1 t2 - Proper-interval)
         (iff (int-after t1 t2) (int-before t2 t1)))

      ;; Axiom "2.3-9"
      (forall (t1 t2 - Proper-interval)
         (iff (int-met-by t1 t2)
              (int-meets t2 t1)))

      ;; Axiom "2.3-10"
      (forall (t1 t2 - Proper-interval)
         (iff (int-overlapped-by t1 t2)
              (int-overlaps t2 t1)))

      ;; Axiom "2.3-11"
      (forall (t1 t2 - Proper-interval)
         (iff (int-started-by t1 t2)
              (int-starts t2 t1)))

      ;; Axiom "2.3-12"
      (forall (t1 t2 - Proper-interval)
         (iff (int-contains t1 t2) (int-during t2 t1)))

      ;; Axiom "2.3-13"
      (forall (tv1 tv2 - Proper-interval)
         (iff (int-finished-by tv1 tv2) (int-finishes tv2 tv1)))

      ;; Axiom "2.3-14"
      (forall (tv1 tv2 - Proper-interval)
         (iff (starts-or-during tv1 tv2)
              (or (int-starts tv1 tv2) (int-during tv1 tv2))))

      ;; Axiom "2.3-15"
      (forall (tv1 tv2 - Proper-interval)
         (iff (nonoverlap tv1 tv2)
              (or (int-before tv1 tv2)
                  (int-after tv1 tv2)
                  (int-meets tv1 tv2)
                  (int-met-by tv1 tv2))))

   ))

(define (addendum daml-time-extensions)
   (:domain daml-time-axis)

   (:axioms
       ;; Axiom "2.4-1"
       (iff (total-order)
            (forall (t1 t2 - Instant)
                    (or (before t1 t2) (= t1 t2) (before t2 t1))))

       ;; Axiom "2.4-2"
       (iff (totally-ordered-past)
            (forall (t1 t2 tf - Instant)
               (if (and (before t1 tf)
                        (before t2 tf))
                   (or (before t1 t2) (= t1 t2) (before t2 t1)))))

      ;; Axiom "2.4-3"
      (if (branching-time)
          (not (pts-at-inf)))

       ;; Axiom "2.4-4"
       (forall (pi ti - Instant)
          (if (posinf pi)
              (or (before ti pi) (= ti pi))))

       ;; Axiom "2.4-5"
       (forall (ti - Instant)
          (if (not (posinf ti))
              (exists (ti2 - Instant)
                 (before ti ti2))))

     ;; Axiom "2.4-6"
     (forall (ni ti - Instant)
        (if (neginf ni)
            (or (before ni ti) (= ti ni))))

       ;; Axiom "2.4-7"
       (forall (ti1 - Instant)
          (if (not (neginf ti1))
              (exists (ti2 - Instant)
                 (before ti2 ti1))))

       ;; Axiom "2.4-8"
       (and (forall (ptv - Interval)
               (if (posinf-interval ptv)
                   (not (exists (e - Instant)
                           (ends e ptv)))))
            (forall (ptv - Interval)
               (if (neginf-interval ptv)
                   (not (exists (e - Instant)
                           (begins e ptv))))))

       ;; Axiom "2.4-9"
       (forall (int - Interval)
          (if (posinf-interval int)
              (and (not (exists (ti)
                           (ends ti int)))
                   (forall (t1 - Instant)
                      (if (inside t1 int)
                          (exists (t2 - Instant)
                             (and (inside t2 int)
                                  (before t1 t2))))))))

       ;; Axiom "2.4-10"
       (forall (int - Interval)
          (if (neginf-interval int)
              (and (not (exists (ti)
                           (begins ti int)))
                   (forall (t1 - Instant)
                      (if (inside t1 int)
                          (exists (t2 - Instant)
                              (and (inside t2 int) (before t2 t1))))))))

       ;; Axiom "2.4-11"
       (forall (tv - Interval)
          (iff (halfinf-interval tv)
               (or (posinf-interval tv)
                   (neginf-interval tv))))

      ;; Axiom "2.4-15"
      (iff (pts-at-inf) (exists (ti) (posinf ti)))
      ;; Axiom "2.4-16"
      (iff (pts-at-inf) (exists (ti) (neginf ti)))

       ;; Axiom "2.4-14"
       (iff (exists (ti) (neginf ti))
            (not (exists (tv) (neginf-interval tv))))

      ;; Axiom "2.4-12"
      (forall (tv - Interval)
         (iff (inf-interval tv)
              (and (posinf-interval tv)
                   (neginf-interval tv))))

       ;; Axiom "2.4-13"
       (iff (exists (ti) (posinf ti))
            (not (exists (tv) (posinf-interval tv))))

        ;; Axiom "2.4-24"
        (if (not (pts-at-inf))
            (forall (ti - Instant)
               (exists (tv - Interval)
                  (and (posinf-interval tv)
                       (begins ti tv)))))

        ;; Axiom "2.4-25"
        (if (not (pts-at-inf))
            (forall (ti - Instant)
               (exists (tv - Interval)
                  (and (neginf-interval tv)
                  (ends ti tv)))))

       ;; Axiom "2.4-28"
       (if (dense-time)
           (forall (t1 t2 - Instant)
              (if (before t1 t2)
                  (exists (ti - Instant)
                     (and (before t1 ti) (before ti t2))))))

       ;; Axiom "2.4-29"
       (if (time-intervals-convex)
           (forall (int - Interval b e ti - Instant)
              (if (and (begins b int)
                       (ends e int)
                       (before b ti)
                       (before ti e))
                  (inside ti int))))

       ;; Axiom "2.4-30"
       (if (time-intervals-extensional)
           (forall (int1 int2 - Proper-interval)
              (if (int-equals int1 int2)
                  (= int1 int2))))

    ))

(define (addendum concat)
   (:domain daml-time-axis)

   (:axioms

       ;; Axiom "3.2-1"
       (forall (x - Proper-interval s - Set)
          (iff (concatenation x s)
               (and (forall (z - Instant)
                       (if (begins-or-in z x)
                           (exists (y - Proper-interval)
                              (and (member y s)
                                   (begins-or-in z y)))))
                    (forall (z - Instant)
                       (if (ends z x)
                           (exists (y - Proper-interval)
                              (and (member y s)
                                   (ends z y)))))
                    
                    (forall (y - Proper-interval)
                       (if (member y s)
                           (or (int-starts y x)
                               (int-during y x)
                               (int-finishes y x))))
                    (forall (y1 y2 - Proper-interval)
                       (if (and (member y1 s) (member y2 s))
                           (or (= y1 y2) (nonoverlap y1 y2)))))))
      ;; Axiom "3.2-2"
      (forall (x s)
         (if (concatenation x s)
             (and (exists! (y1) (and (member y1 s) (int-starts y1 x)))
                  (exists! (y2) (and (member y2 s) (int-finishes y2 x))))))

      ;; Axiom "3.2-3"
      (if (time-intervals-convex)
          (and (forall (x s)
                  (if (concatenation x s)
                      (and (forall (y1)
                              (if (member y1 s)
                                  (or (int-finishes y1 x)
                                      (exists! (y2)
                                         (and (member y2 s)
                                              (int-meets y1 y2))))))
                           (forall (y2)
                              (if (member y2 s)
                                  (or (int-starts y2 x)
                                      (exists! (y1)
                                         (and (member y2 s)
                                              (int-meets y1 y2)))))))))))

))



(define (domain daml-time-inf-points)
   (:extends daml-time-axis)

     (:objects positive-infinity negative-infinity - Instant)

   (:functions (beginning-of tv - Interval)
               (end-of tv - Interval)
               - Instant)

   (:axioms
      ;; Axiom "2.4-21"
      (pts-at-inf)
        ;; Axiom "2.4-17"
        (posinf positive-infinity)
        ;; Axiom "2.4-18"
        (neginf negative-infinity)
        (forall (tv - Interval ti - Instant)
           (and ;; Axiom "2.4-19"
                (iff (= (beginning-of tv) ti) (begins ti tv))
                ;; Axiom "2.4-20"
                (iff (= (end-of tv) ti) (ends ti tv))))


      ;; Axiom "2.4-22"
      (not (branching-time))))

(define (domain daml-time-inf-intervals)
   (:extends daml-time-axis)
  
   (:axioms
        ;; Axiom "2.4-23"
        (not (pts-at-inf))))

(define (domain daml-time-axis-measure)
   (:requirements :numbers)
   (:extends daml-time-axis)

   (:types Temporal-unit - Obj)

   (:objects infty - Number
             *second* *minute* *hour* *day* *week* *month* *year*
             - Temporal-unit

   )

   (:functions
       (seconds int - Interval)
       (minutes int - Interval)
       (hours int - Interval)
       (days int - Interval)
       (weeks int - Interval)
       (months int - Interval)
       (years int - Interval)
       - Number
       (duration int - Interval tu - Temporal-unit)
       - Number

    )

   (:predicates
      (hath n - Integer u - Temporal-unit x - Proper-interval)
      (second int - Proper-interval)
      (minute int - Proper-interval)
      (hour int - Proper-interval)
      (day int - Proper-interval)
      (week int - Proper-interval)
      (month int - Proper-interval)
      (year int - Proper-interval)

   )


   (:axioms
       ;; Axiom "3.2-4"
       (forall (n - Integer u - Temporal-unit x - Proper-interval)
          (iff (hath n u x)
               (exists (s - Set)
                  (and (= (card s) n)
                       (forall (z - Proper-interval)
                          (if (member z s) (= (duration z u) 1)))
                       (concatenation x s)))))

       (forall (int - Proper-interval)
          (and ;; Axiom "3.1-1"
               (= (seconds int) (duration int *second*))
               ;; Axiom "3.1-2"
               (= (minutes int) (duration int *minute*))
               ;; Axiom "3.1-3"
               (= (hours int) (duration int *hour*))
               ;; Axiom "3.1-4"
               (= (days int) (duration int *day*))
               ;; Axiom "3.1-5"
               (= (weeks int) (duration int *week*))
               ;; Axiom "3.1-6"
               (= (months int) (duration int *month*))
               ;; Axiom "3.1-7"
               (= (years int) (duration int *year*))))

       (forall (int - Proper-interval)
          (and ;; Axiom "3.1-8"
               (= (seconds int) (* 60 (minutes int)))
               ;; Axiom "3.1-9"
               (= (minutes int) (* 60 (hours int)))
               ;; Axiom "3.1-10"
               (= (hours int) (* 24 (days int)))
               ;; Axiom "3.1-11"
               (= (months int) (* 12 (years int)))))

       (forall (int - Proper-interval)
          (and ;; Axiom "3.3-1"
               (iff (second int) (= (seconds int) 1))
               ;; Axiom "3.3-2"
               (iff (minute int) (= (minutes int) 1))
               ;; Axiom "3.3-3"
               (iff (hour int) (= (hours int) 1))
               ;; Axiom "3.3-4"
               (iff (day int) (= (days int) 1))
               ;; Axiom "3.3-5"
               (iff (week int) (= (weeks int) 1))
               ;; Axiom "3.3-6"
               (iff (month int) (= (months int) 1))
               ;; Axiom "3.3-7"
               (iff (year int) (= (years int) 1))))

       (forall (int - Proper-interval)
          (and ;; Axiom "3.3-8"
               (if (minute int) (hath 60 *second* int))
               ;; Axiom "3.3-9"
               (if (hour int) (hath 60 *minute* int))
               ;; Axiom "3.3-10"
               (if (day int) (hath 24 *hour* int))
               ;; Axiom "3.3-11"
               (if (week int) (hath 7 *day* int))
               ;; Axiom "3.3-12"
               (if (year int) (hath 12 *month* int))))

   ))

(define (domain daml-clock-calendar)
   (:extends daml-time-axis-measure)
   
   (:types Time-standard AM/PM - Object
           Era - Proper-interval
     Temporal-description - Object

   )

   (:objects *am* *pm* - AM/PM)

   (:predicates
       (sec y - Proper-interval n - Integer x - Proper-interval)

       (minit y - Proper-interval n - Integer x - Proper-interval)

       (hr y - Proper-interval n - Integer x - Proper-interval)
       (hr12 y - Proper-interval n - Integer ap - AM/PM x - Proper-interval)
       (da y - Proper-interval n - Integer x - Proper-interval)
       (dayofweek y - Proper-interval n - Integer x - Proper-interval)
       (wk y - Proper-interval n - Integer x - Proper-interval)
       (mon y - Proper-interval n - Integer x - Proper-interval)
       (yr y - Proper-interval n - Integer x - Proper-interval)

       (clock-int y - Proper-interval n - Integer u - Temporal-unit
                  x - Proper-interval)

       (cal-int y - Proper-interval n - Integer u - Temporal-unit
                x - Proper-interval)

       (time-of ti - Instant y m d h n s - Integer z - Time-standard)

     (sunday y x - Proper-interval)
     (monday  y x - Proper-interval)
     (tuesday y x - Proper-interval)
     (wednesday y x - Proper-interval)
     (thursday y x - Proper-interval)
     (friday y x - Proper-interval)
     (saturday y x - Proper-interval)

       (weekday x y - Proper-interval)
       (weekendday x y - Proper-interval)

     (leap-year y - Proper-interval)

       (january y x - Proper-interval)
       (february y x - Proper-interval)
       (march y x - Proper-interval)
       (april y x - Proper-interval)
       (may y x - Proper-interval)
       (june y x - Proper-interval)
       (july y x - Proper-interval)
       (august y x - Proper-interval)
       (september y x - Proper-interval)
       (october y x - Proper-interval)
       (november y x - Proper-interval)
       (december y x - Proper-interval)

     (temporal-description-of d - Temporal-description
                              tx - Temporal-entity)

   )

   (:functions
       (common-era s - Time-standard) - Era

       (secFn n - Integer x - Proper-interval)

       (minitFn n - Integer x - Proper-interval)

       (hrFn n - Integer x - Proper-interval)
       (daFn n - Integer x - Proper-interval)
       (dayofweekFn n - Integer x - Proper-interval)
       (wkFn n - Integer x - Proper-interval)
       (monFn n - Integer x - Proper-interval)
       (yrFn n - Integer x - Proper-interval)

       (nth-subinterval n - Integer u - Temporal-unit x - Proper-interval)
       - Proper-interval

     (year-of d - Temporal-description)
     (month-of d - Temporal-description)
     (day-of d - Temporal-description)
     (hour-of d - Temporal-description)
     (minute-of d - Temporal-description)
     (second-of d - Temporal-description)
     - Number
     (time-zone-of d - Temporal-description)
     - Time-standard

   )

   (:facts (time-intervals-extensional))

   (:axioms
       ;; Axiom "4.2-1"
       (forall (x y - Proper-interval n - Integer)
          (and (iff (sec y n x)
                    (clock-int y n *second* x))
               (iff (sec y n x)
                    (= (secFn n x) y))))

       ;; Axiom "4.2-2"
       (forall (x y - Proper-interval n - Integer)
          (and (iff (minit y n x)
                    (clock-int y n *minute* x))
               (iff (minit y n x)
                    (= (minitFn n x) y))))

       ;; Axiom "4.2-3"
       (forall (x y - Proper-interval n - Integer)
          (and (iff (hr y n x)
                    (clock-int y n *hour* x))
               (iff (hr y n x)
                    (= (hrFn n x) y))))

       ;; Axiom "4.2-4"
       (forall (x y - Proper-interval n - Integer)
          (and (iff (da y n x)
                    (cal-int y n *day* x))
               (iff (da y n x)
                    (= (daFn n x) y))))

       ;; Axiom "4.2-5"
       (forall (x y - Proper-interval n - Integer)
          (and (iff (mon y n x)
                    (cal-int y n *month* x))
               (iff (mon y n x)
                    (= (monFn n x) y))))

       ;; Axiom "4.2-6"
       (forall (x y - Proper-interval n - Integer)
          (and (iff (yr y n x)
                    (cal-int y n *year* x))
               (iff (yr y n x)
                    (= (yrFn n x) y))))

       ;; Axiom "4.2-7"
       (forall (n - Integer u - Temporal-unit x y - Proper-interval)
          (iff (= y (nth-subinterval n u x))
               (clock-int y n u x)))

       ;; Axiom "4.2-8"
       (forall (n - Integer x - Proper-interval)
          (= (secFn n x)
             (nth-subinterval n *second* x)))

       ;; Axiom "4.2-9"
       (forall (n - Integer x - Proper-interval)
          (= (minitFn n x)
             (nth-subinterval n *minute* x)))

       ;; Axiom "4.2-10"
       (forall (n - Integer x - Proper-interval)
          (= (hrFn n x)
             (nth-subinterval n *hour* x)))


       ;; Axiom "4.2-11"
       (forall (n - Integer x - Proper-interval)
          (= (daFn n x)
             (nth-subinterval n *day* x)))

       ;; Axiom "4.2-12"
       (forall (n - Integer x - Proper-interval)
          (= (monFn n x)
             (nth-subinterval n *month* x)))


       ;; Axiom "4.2-13"
       (forall (n - Integer x - Proper-interval)
          (= (yrFn n x)
             (nth-subinterval n *year* x)))

       (forall (x y - Proper-interval n - Integer)
          (and ;; Axiom "4.2-14"
               (iff (hr12 y n *am* x)
                    (hr y n x))
               ;; Axiom "4.2-15"
               (iff (hr12 y n *pm* x)
                    (hr y (+ n 12) x))))

       ;; Axiom "4.2-16"
       (forall (y x - Proper-interval n - Integer u - Temporal-unit)
          (iff (cal-int y n u x) (clock-int y (- n 1) u x)))

      ;; Axiom "4.2-17"
      (forall (y - Proper-interval n - Integer u - Temporal-unit
               x - Proper-interval)
         (if (cal-int y n u x)
             (starts-or-during y x)))

      ;; Axiom "4.2-18"
      (forall (y - Proper-interval n - Integer u - Temporal-unit
               x - Proper-interval)
         (if (cal-int y n u x)
             (= (duration y u) 1)))

       ;; Axiom "4.2-19"
       (forall (y x - Proper-interval u - Temporal-unit n N - Integer)
          (if (and (cal-int y n u x) (hath N u x))
              (and (< 1 n) (=< n N))))

       ;; Axiom "4.2-20"
       (forall (n - Integer u - Temporal-unit x - Proper-interval)
          (if (hath n u x)
              (int-starts (nth-subinterval 0 u x)
                          x)))

       ;; Axiom "4.2-21"
       (forall (n - Integer u - Temporal-unit x - Proper-interval)
          (if (hath n u x)
              (int-finishes (nth-subinterval (- n 1) u x)
                            x)))

       ;; Axiom "4.2-22"
       (forall (n - Integer u - Temporal-unit x - Proper-interval)
          (if (hath n u x)
              (forall (i - Integer)
                 (if (and (=< 0 i) (< i n))
                     (int-meets (nth-subinterval i u x)
                                (nth-subinterval (+ i 1) u x))))))

       (forall (x y - Proper-interval n - Integer)
          (and ;; Axiom "4.3-1"
               (iff (wk y n x)
                    (cal-int y n *week* x))
               ;; Axiom "4.3-2"
               (iff (wk y n x)
                    (= (wkFn n x) y))))

       ;; Axiom "4.3-3"
       (forall (y x - Proper-interval n - Integer)
          (iff (dayofweek y n x)
               (and (da y n x)
                    (exists (n1 - Integer x1 - Proper-interval)
                       (wk x n1 x1)))))

       ;; Axiom "4.3-4"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 1 x)
               (sunday y x)))

       ;; Axiom "4.3-5"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 2 x)
               (monday y x)))

       ;; Axiom "4.3-6"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 3 x)
               (tuesday y x)))

       ;; Axiom "4.3-7"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 4 x)
               (wednesday y x)))

       ;; Axiom "4.3-8"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 5 x)
               (thursday y x)))

       ;; Axiom "4.3-9"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 6 x)
               (friday y x)))

       ;; Axiom "4.3-10"
       (forall (y x - Proper-interval)
          (iff (dayofweek y 7 x)
               (saturday y x)))

       ;; Axiom "4.3-11"
       (forall (z - Time-standard)
          (exists (x - Proper-interval)
             (tuesday (daFn 1 (monFn 1 (yrFn 2002 (common-era z))))
                      x)))


       ;; Axiom "4.3-12"
       (forall (y x - Proper-interval)
          (iff (weekday y x)
               (or (monday y x) (tuesday y x) (wednesday y x)
                   (thursday y x) (friday y x))))

       ;; Axiom "4.3-13"
       (forall (y x - Proper-interval)
          (iff (weekendday y x) (or (saturday y x) (sunday y x))))


       ;; Axiom "4.4-1"
       (forall (y x - Proper-interval)
          (iff (mon y 1 x) (january y x)))

       ;; Axiom "4.4-2"
       (forall (y x - Proper-interval)
          (iff (mon y 2 x) (february y x)))

       ;; Axiom "4.4-3"
       (forall (y x - Proper-interval)
          (iff (mon y 3 x) (march y x)))

       ;; Axiom "4.4-4"
       (forall (y x - Proper-interval)
          (iff (mon y 4 x) (april y x)))

       ;; Axiom "4.4-5"
       (forall (y x - Proper-interval)
          (iff (mon y 5 x) (may y x)))

       ;; Axiom "4.4-6"
       (forall (y x - Proper-interval)
          (iff (mon y 6 x) (june y x)))

       ;; Axiom "4.4-7"
       (forall (y x - Proper-interval)
          (iff (mon y 7 x) (july y x)))

       ;; Axiom "4.4-8"
       (forall (y x - Proper-interval)
          (iff (mon y 8 x) (august y x)))

       ;; Axiom "4.4-9"
       (forall (y x - Proper-interval)
          (iff (mon y 9 x) (september y x)))

       ;; Axiom "4.4-10"
       (forall (y x - Proper-interval)
          (iff (mon y 10 x) (october y x)))

       ;; Axiom "4.4-11"
       (forall (y x - Proper-interval)
          (iff (mon y 11 x) (november y x)))

       ;; Axiom "4.4-12"
       (forall (y x - Proper-interval)
          (iff (mon y 12 x) (december y x)))

       ;; Axiom "4.4-13"
       (forall (m y - Proper-interval)
          (if (january m y) (hath 31 *day* m)))

       ;; Axiom "4.4-14"
       (forall (m y - Proper-interval)
          (if (march m y) (hath 31 *day* m)))

       ;; Axiom "4.4-15"
       (forall (m y - Proper-interval)
          (if (april m y) (hath 30 *day* m)))

       ;; Axiom "4.4-16"
       (forall (m y - Proper-interval)
          (if (may m y) (hath 31 *day* m)))

       ;; Axiom "4.4-17"
       (forall (m y - Proper-interval)
          (if (june m y) (hath 30 *day* m)))

       ;; Axiom "4.4-18"
       (forall (m y - Proper-interval)
          (if (july m y) (hath 31 *day* m)))

       ;; Axiom "4.4-19"
       (forall (m y - Proper-interval)
          (if (august m y) (hath 31 *day* m)))

       ;; Axiom "4.4-20"
       (forall (m y - Proper-interval)
          (if (september m y) (hath 30 *day* m)))

       ;; Axiom "4.4-21"
       (forall (m y - Proper-interval)
          (if (october m y) (hath 31 *day* m)))

       ;; Axiom "4.4-22"
       (forall (m y - Proper-interval)
          (if (november m y) (hath 30 *day* m)))

       ;; Axiom "4.4-23"
       (forall (m y - Proper-interval)
          (if (december m y) (hath 31 *day* m)))

       ;; Axiom "4.4-24"
       (forall (y - Proper-interval z - Time-standard)
          (iff (leap-year y)
               (exists (n - Integer)
                  (and (yr y n (common-era z))
                       (or (divides 400 n)
                           (and (divides 4 n) (not (divides 100 n))))))))

       ;; Axiom "4.4-25"
       (forall (m y - Proper-interval)
          (if (and (february m y) (leap-year y))
              (hath 29 *day* m)))

       ;; Axiom "4.4-26"
       (forall (m y - Proper-interval)
          (if (and (february m y) (not (leap-year y)))
              (hath 28 *day* m)))

       ;; Axiom "4.4-27"
       (forall (int - Proper-interval)
          (iff (month int)
               (exists (d1 d2 - Proper-interval
                        n n1 n2 - Integer
                        m1 m2 y1 y2 e - Proper-interval
                        mb me - Instant)
                  (and (begins mb int)
                       (ends me int)
                       (begins-or-in mb d1)
                       (begins-or-in me d2)
                       (da d1 n m1)
                       (mon m1 n1 y1)
                       (yr y1 n2 e)
                       (da d2 n m2)
                       (or (mon m2 (+ n1 1) y1)
                           (exists (y2 - Proper-interval)
                              (and (= n1 12)
                                   (mon m2 1 y2)
                                   (yr y2 (+ n2 1) e))))))))

       ;; Axiom "4.5-1"
       (forall (ti - Instant
                y m d h n s - Integer
                z - Time-standard)
          (iff (time-of ti y m d h n s z)
               (begins-or-in ti
                  (secFn
                     s (minitFn
                        n (hrFn h (daFn d (monFn m (yrFn y (common-era z))))))))))

   ;; Axiom "4.5-2"
   (forall (ti y m d h n s z)
           (iff (time-of ti y m d h n s z)
                (exists (d1)
                        (and (temporal-description-of d1 ti)
                             (= (year-of d1) y)
                             (= (month-of d1) m) (= (day-of d1) d)
                             (= (hour-of d1) h)
                             (= (minute-of d1) n)
                             (= (second-of d1) s)
                             (= (time-zone-of d1) z)))))


   ))