;; lisp2explicit: Mon Jul 28 14:42:02 EDT 2003
(defaxiom "2.1-1" (forall (t) (=> (instant t) (temporal-entity t))))
(defaxiom "2.1-2" (forall (T) (=> (interval T) (temporal-entity T))))
(defaxiom "2.1-3"
(forall (T) (=> (temporal-entity T) (or (instant T) (interval T)))))
(defaxiom "2.1-4"
(forall (t T) (=> (begins t T) (and (instant t) (temporal-entity T)))))
(defaxiom "2.1-5"
(forall (t T) (=> (ends t T) (and (instant t) (temporal-entity T)))))
(defaxiom "2.1-6" (forall (t) (<=> (instant t) (begins t t))))
(defaxiom "2.1-7" (forall (t) (<=> (instant t) (ends t t))))
(defaxiom "2.1-8"
(forall (T t1 t2)
(=> (and (and (temporal-entity T) (begins t1 T)) (begins t2 T))
(equals t1 t2))))
(defaxiom "2.1-9"
(forall (T t1 t2)
(=> (and (and (temporal-entity T) (ends t1 T)) (ends t2 T))
(equals t1 t2))))
(defaxiom "2.1-10"
(forall (t T) (=> (inside t T) (and (instant t) (interval T)))))
(defaxiom "2.1-11"
(forall (t T) (<=> (begins-or-in t T) (or (begins t T) (inside t T)))))
(defaxiom "2.1-12"
(forall (T t1 t2)
(=> (time-between T t1 t2)
(and (and (temporal-entity T) (instant t1)) (instant t2)))))
(defaxiom "2.1-13"
(forall (t1 t2)
(=> (not-equals t1 t2)
(forall (T)
(<=> (time-between T t1 t2) (and (begins t1 T) (ends t2 T)))))))
(defaxiom "2.1-14"
(forall (T)
(<=> (proper-interval T)
(and (interval T)
(forall (t1 t2)
(=> (and (begins t1 T) (ends t2 T)) (not-equals t1 t2)))))))
(defaxiom "2.2-1"
(forall (T1 T2)
(<=> (before T1 T2)
(exists (t1 t2)
(and (and (ends t1 T1) (begins t2 T2)) (before t1 t2))))))
(defaxiom "2.2-2"
(forall (T1 T2) (=> (before T1 T2) (not-equals T1 T2))))
(defaxiom "2.2-3"
(forall (T1 T2) (=> (before T1 T2) (not (before T2 T1)))))
(defaxiom "2.2-4"
(forall (T1 T2 T3)
(=> (and (before T1 T2) (before T2 T3)) (before T1 T3))))
(defaxiom "2.2-5"
(forall (T t1 t2)
(=> (and (and (interval T) (begins t1 T)) (ends t2 T))
(not (before t2 t1)))))
(defaxiom "2.2-6"
(forall (T t1 t2)
(=> (and (and (proper-interval T) (begins t1 T)) (ends t2 T))
(before t1 t2))))
(defaxiom "2.2-7"
(forall (t1 t2)
(=> (and (and (instant t1) (instant t2)) (before t1 t2))
(exists (T) (time-between T t1 t2)))))
(defaxiom "2.2-8"
(forall (t T t1 t2)
(=> (and (and (inside t T) (begins t1 T)) (ends t2 T))
(and (before t1 t) (before t t2)))))
(defaxiom "2.2-9" (forall (T1 T2) (<=> (after T1 T2) (before T2 T1))))
(defaxiom "2.3-1"
(forall (T1 T2)
(<=> (int-equals T1 T2)
(and (and (and (proper-interval T1) (proper-interval T2))
(forall (t1) (<=> (begins t1 T1) (begins t1 T2))))
(forall (t2) (<=> (ends t2 T1) (ends t2 T2)))))))
(defaxiom "2.3-2"
(forall (T1 T2)
(<=> (int-before T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(before T1 T2)))))
(defaxiom "2.3-3"
(forall (T1 T2)
(<=> (int-meets T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(exists (t) (and (ends t T1) (begins t T2)))))))
(defaxiom "2.3-4"
(forall (T1 T2)
(<=> (int-overlaps T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(exists (t2 t3)
(and (and (and (and (ends t2 T1) (begins t3 T2))
(before t3 t2))
(forall (t1) (=> (begins t1 T1) (before t1 t3))))
(forall (t4) (=> (ends t4 T2) (before t2 t4)))))))))
(defaxiom "2.3-5"
(forall (T1 T2)
(<=> (int-starts T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(exists (t2)
(and (and (ends t2 T1)
(forall (t1) (<=> (begins t1 T1) (begins t1 T2))))
(forall (t4) (=> (ends t4 T2) (before t2 t4)))))))))
(defaxiom "2.3-6"
(forall (T1 T2)
(<=> (int-during T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(exists (t1 t2)
(and (and (and (begins t1 T1) (ends t2 T1))
(forall (t3) (=> (begins t3 T2) (before t3 t1))))
(forall (t4) (=> (ends t4 T2) (before t2 t4)))))))))
(defaxiom "2.3-7"
(forall (T1 T2)
(<=> (int-finishes T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(exists (t1)
(and (and (begins t1 T1)
(forall (t3) (=> (begins t3 T2) (before t3 t1))))
(forall (t4) (<=> (ends t4 T2) (ends t4 T1)))))))))
(defaxiom "2.3-8"
(forall (T1 T2) (<=> (int-after T1 T2) (int-before T2 T1))))
(defaxiom "2.3-9"
(forall (T1 T2) (<=> (int-met-by T1 T2) (int-meets T2 T1))))
(defaxiom "2.3-10"
(forall (T1 T2) (<=> (int-overlapped-by T1 T2) (int-overlaps T2 T1))))
(defaxiom "2.3-11"
(forall (T1 T2) (<=> (int-started-by T1 T2) (int-starts T2 T1))))
(defaxiom "2.3-12"
(forall (T1 T2) (<=> (int-contains T1 T2) (int-during T2 T1))))
(defaxiom "2.3-13"
(forall (T1 T2) (<=> (int-finished-by T1 T2) (int-finishes T2 T1))))
(defaxiom "2.3-14"
(forall (T1 T2)
(<=> (starts-or-during T1 T2)
(or (int-starts T1 T2) (int-during T1 T2)))))
(defaxiom "2.3-15"
(forall (T1 T2)
(<=> (nonoverlap T1 T2)
(or (or (or (int-before T1 T2) (int-after T1 T2)) (int-meets T1 T2))
(int-met-by T1 T2)))))
(defaxiom "2.4-1"
(=> (Total-Order)
(forall (t1 t2)
(=> (and (instant t1) (instant t2))
(or (or (before t1 t2) (equals t1 t2)) (before t2 t1))))))
(defaxiom "2.4-2" (forall (t) (=> (posinf t) (instant t))))
(defaxiom "2.4-3" (forall (t) (=> (neginf t) (instant t))))
(defaxiom "2.4-4"
(forall (t t1)
(=> (and (instant t1) (posinf t)) (or (before t1 t) (equals t1 t)))))
(defaxiom "2.4-5"
(forall (t1)
(=> (and (instant t1) (not (posinf t1)))
(exists (t2) (and (instant t2) (before t1 t2))))))
(defaxiom "2.4-6"
(forall (t t1)
(=> (and (instant t1) (neginf t)) (or (before t t1) (equals t1 t)))))
(defaxiom "2.4-7"
(forall (t1)
(=> (and (instant t1) (not (neginf t1)))
(exists (t2) (and (instant t2) (before t2 t1))))))
(defaxiom "2.4-8"
(forall (t1 T)
(=> (and (posinf-interval T) (inside t1 T))
(exists (t2) (and (before t1 t2) (inside t2 T))))))
(defaxiom "2.4-9"
(forall (t1 T)
(=> (and (neginf-interval T) (inside t1 T))
(exists (t2) (and (before t2 t1) (inside t2 T))))))
(defaxiom "2.4-10"
(forall (T)
(<=> (halfinf-interval T)
(or (posinf-interval T) (neginf-interval T)))))
(defaxiom "2.4-11"
(forall (T)
(<=> (inf-interval T) (and (posinf-interval T) (neginf-interval T)))))
(defaxiom "2.4-12"
(<=> (exists (t) (posinf t)) (not (exists (T) (posinf-interval T)))))
(defaxiom "2.4-13"
(<=> (exists (t) (neginf t)) (not (exists (T) (neginf-interval T)))))
(defaxiom "2.4-14a" (=> (Pts-at-Inf) (exists (t) (posinf t))))
(defaxiom "2.4-15a" (=> (Pts-at-Inf) (exists (t) (neginf t))))
(defaxiom "2.4-14b"
(=> (No-Pts-at-Inf)
(forall (t)
(=> (instant t)
(exists (T) (and (posinf-interval T) (begins t T)))))))
(defaxiom "2.4-15b"
(=> (No-Pts-at-Inf)
(forall (t)
(=> (instant t) (exists (T) (and (neginf-interval T) (ends t T)))))))
(defaxiom "2.4-16"
(=> (Dense)
(forall (t1 t2)
(=> (and (and (instant t1) (instant t2)) (before t1 t2))
(exists (t) (and (and (instant t) (before t1 t)) (before t t2)))))))
(defaxiom "2.4-17"
(forall (t1 T t2 t)
(=> (Convex)
(=>
(and (and (and (begins t1 T) (ends t2 T)) (before t1 t))
(before t t2))
(inside t T)))))
(defaxiom "2.4-18"
(=> (Ext-Collapse)
(forall (T1 T2) (=> (int-equals T1 T2) (equals T1 T2)))))
(defaxiom "2.5-1" (forall (e t) (=> (at-time e t) (instant t))))
(defaxiom "2.5-2" (forall (e T) (=> (during e T) (interval T))))
(defaxiom "2.5-3"
(forall (e T t) (=> (and (during e T) (inside t T)) (at-time e t))))
(defaxiom "2.5-4"
(forall (e T T1)
(=> (and (during e T) (int-during T1 T)) (during e T1))))
(defaxiom "2.5-5"
(forall (T e) (=> (time-span T e) (and (temporal-entity T) (tseq T)))))
(defaxiom "2.5-6"
(forall (T e) (=> (and (time-span T e) (interval T)) (during e T))))
(defaxiom "2.5-7"
(forall (t e) (=> (and (time-span t e) (instant t)) (at-time e t))))
(defaxiom "2.5-8"
(forall (T e t)
(=>
(and (and (and (and (time-span T e) (interval T))
(not (inside t T)))
(not (begins t T)))
(not (ends t T)))
(not (at-time e t)))))
(defaxiom "2.5-9"
(forall (t e t1)
(=> (and (and (time-span t e) (instant t)) (not-equals t1 t))
(not (at-time e t1)))))
(defaxiom "3.1-1"
(forall (T) (equals (seconds T) (duration T *Second*))))
(defaxiom "3.1-2"
(forall (T) (equals (minutes T) (duration T *Minute*))))
(defaxiom "3.1-3" (forall (T) (equals (hours T) (duration T *Hour*))))
(defaxiom "3.1-4" (forall (T) (equals (days T) (duration T *Day*))))
(defaxiom "3.1-5" (forall (T) (equals (weeks T) (duration T *Week*))))
(defaxiom "3.1-6" (forall (T) (equals (months T) (duration T *Month*))))
(defaxiom "3.1-7" (forall (T) (equals (years T) (duration T *Year*))))
(defaxiom "3.1-8"
(forall (T u)
(=> (duration T u) (and (proper-interval T) (temporal-unit u)))))
(defaxiom "4.2-17"
(and (and (and (and (and (and (temporal-unit *Second*)
(temporal-unit *Minute*))
(temporal-unit *Hour*))
(temporal-unit *Day*))
(temporal-unit *Week*))
(temporal-unit *Month*))
(temporal-unit *Year*)))
(defaxiom "3.1-9"
(forall (T) (equals (seconds T) (times 60 (minutes T)))))
(defaxiom "3.1-10"
(forall (T) (equals (minutes T) (times 60 (hours T)))))
(defaxiom "3.1-11" (forall (T) (equals (hours T) (times 24 (days T)))))
(defaxiom "3.1-12" (forall (T) (equals (days T) (times 7 (weeks T)))))
(defaxiom "3.1-13"
(forall (T) (equals (months T) (times 12 (years T)))))
(defaxiom "3.2-1"
(forall (x S)
(<=> (concatenation x S)
(and (and (and (and (proper-interval x)
(forall (z)
(=> (begins-or-in z x)
(exists (y)
(and (member y S) (begins-or-in z y))))))
(forall (z)
(=> (equals (end-of x) z)
(exists (y)
(and (member y S) (equals (end-of y) z))))))
(forall (y)
(=> (member y S)
(or (or (int-starts y x) (int-during y x))
(int-finishes y x)))))
(forall (y1 y2)
(=> (and (member y1 S) (member y2 S))
(or (equals y1 y2) (nonoverlap y1 y2))))))))
(defaxiom "3.2-2"
(forall (N u x)
(<=> (Hath N u x)
(exists (S)
(and (and (equals (card S) N)
(forall (z) (=> (member z S) (equals (duration z u) 1))))
(concatenation x S))))))
(defaxiom "3.2-3"
(forall (N u x)
(=> (Hath N u x)
(and (and (integer N) (temporal-unit u)) (proper-interval x)))))
(defaxiom "3.3-1" (forall (T) (<=> (second T) (equals (seconds T) 1))))
(defaxiom "3.3-2" (forall (T) (<=> (minute T) (equals (minutes T) 1))))
(defaxiom "3.3-3" (forall (T) (<=> (hour T) (equals (hours T) 1))))
(defaxiom "3.3-4" (forall (T) (<=> (day T) (equals (days T) 1))))
(defaxiom "3.3-5" (forall (T) (<=> (week T) (equals (weeks T) 1))))
(defaxiom "3.3-6" (forall (T) (<=> (month T) (equals (months T) 1))))
(defaxiom "3.3-7" (forall (T) (<=> (year T) (equals (years T) 1))))
(defaxiom "3.3-8" (forall (T) (=> (minute T) (Hath 60 *Second* T))))
(defaxiom "3.3-9" (forall (T) (=> (hour T) (Hath 60 *Minute* T))))
(defaxiom "3.3-10" (forall (T) (=> (day T) (Hath 24 *Hour* T))))
(defaxiom "3.3-11" (forall (T) (=> (week T) (Hath 7 *Day* T))))
(defaxiom "3.3-12" (forall (T) (=> (year T) (Hath 12 *Month* T))))
(defaxiom "4.2-1"
(forall (y n x) (<=> (sec y n x) (equals (secFn n x) y))))
(defaxiom "4.2-2"
(forall (y n x) (<=> (sec y n x) (clock-int y n *Second* x))))
(defaxiom "4.2-3"
(forall (y n x) (<=> (minit y n x) (equals (minitFn n x) y))))
(defaxiom "4.2-4"
(forall (y n x) (<=> (minit y n x) (clock-int y n *Minute* x))))
(defaxiom "4.2-5"
(forall (y n x) (<=> (hr y n x) (equals (hrFn n x) y))))
(defaxiom "4.2-6"
(forall (y n x) (<=> (hr y n x) (clock-int y n *Hour* x))))
(defaxiom "4.2-7"
(forall (y n x) (<=> (da y n x) (equals (daFn n x) y))))
(defaxiom "4.2-8"
(forall (y n x) (<=> (da y n x) (cal-int y n *Day* x))))
(defaxiom "4.2-9"
(forall (y n x) (<=> (mon y n x) (equals (monFn n x) y))))
(defaxiom "4.2-10"
(forall (y n x) (<=> (mon y n x) (cal-int y n *Month* x))))
(defaxiom "4.2-11"
(forall (y n x) (<=> (yr y n x) (equals (yrFn n x) y))))
(defaxiom "4.2-12"
(forall (y n x) (<=> (yr y n x) (cal-int y n *Year* x))))
(defaxiom "4.2-13" (forall (y n x) (<=> (hr12 y n *am* x) (hr y n x))))
(defaxiom "4.2-14"
(forall (y n x) (<=> (hr12 y n *pm* x) (hr y (plus n 12) x))))
(defaxiom "4.2-15"
(forall (y n u x n-1) (<=> (cal-int y n u x) (clock-int y n-1 u x))))
(defaxiom "4.2-16"
(forall (y n u x)
(=> (cal-int y n u x)
(and (and (and (interval y) (integer n)) (temporal-unit u))
(interval x)))))
(defaxiom "4.2-17"
(forall (y n u x) (=> (cal-int y n u x) (starts-or-during y x))))
(defaxiom "4.2-18"
(forall (y n u x) (=> (cal-int y n u x) (equals (duration y u) 1))))
(defaxiom "4.2-19"
(forall (y n u x N)
(=> (and (cal-int y n u x) (Hath N u x))
(and (less-than 0 n) (less-than-or-equals n N)))))
(defaxiom "4.2-20"
(forall (N u x) (=> (Hath N u x) (exists! (y) (cal-int y 1 u x)))))
(defaxiom "4.2-21"
(forall (S N u x y)
(=> (and (Hath S N u x) (cal-int y 1 u x)) (int-starts y x))))
(defaxiom "4.2-22"
(forall (N u x) (=> (Hath N u x) (exists! (y) (cal-int y N u x)))))
(defaxiom "4.2-23"
(forall (N u x y)
(=> (and (Hath N u x) (cal-int y N u x)) (int-finishes y x))))
(defaxiom "4.2-24"
(forall (y1 n u x N)
(=> (and (and (cal-int y1 n u x) (Hath N u x)) (less-than n N))
(exists! (y2) (and (cal-int y2 (plus n 1) u x) (int-meets y1 y2))))))
(defaxiom "4.2-25"
(forall (y2 n u x N)
(=> (and (and (cal-int y2 n u x) (Hath N u x)) (less-than 1 n))
(exists! (y1)
(and (cal-int y1 (minus n 1) u x) (int-meets y1 y2))))))
(defaxiom "4.3-1"
(forall (y n x) (<=> (wk y n x) (equals (wkFn n x) y))))
(defaxiom "4.3-2"
(forall (y n x) (<=> (wk y n x) (cal-int y n *Week* x))))
(defaxiom "4.3-3"
(forall (y n x)
(<=> (dayofweek y n x)
(and (day y n x) (exists (n1 x1) (wk x n1 x1))))))
(defaxiom "4.3-4" (forall (y x) (<=> (dayofweek y 1 x) (Sunday y x))))
(defaxiom "4.3-5" (forall (y x) (<=> (dayofweek y 2 x) (Monday y x))))
(defaxiom "4.3-6" (forall (y x) (<=> (dayofweek y 3 x) (Tuesday y x))))
(defaxiom "4.3-7"
(forall (y x) (<=> (dayofweek y 4 x) (Wednesday y x))))
(defaxiom "4.3-8" (forall (y x) (<=> (dayofweek y 5 x) (Thursday y x))))
(defaxiom "4.3-9" (forall (y x) (<=> (dayofweek y 6 x) (Friday y x))))
(defaxiom "4.3-10"
(forall (y x) (<=> (dayofweek y 7 x) (Saturday y x))))
(defaxiom "4.3-11"
(forall (z)
(exists (x) (Tuesday (dayFn 1 (monFn 1 (yrFn 2002 (CE z)))) x))))
(defaxiom "4.3-12"
(forall (y x)
(<=> (weekday y x)
(or (or (or (or (Monday y x) (Tuesday y x)) (Wednesday y x))
(Thursday y x))
(Friday y x)))))
(defaxiom "4.3-13"
(forall (y x) (<=> (weekendday y x) (or (Saturday y x) (Sunday y x)))))
(defaxiom "4.4-1" (forall (y x) (<=> (mon y 1 x) (January y x))))
(defaxiom "4.4-2" (forall (y x) (<=> (mon y 2 x) (February y x))))
(defaxiom "4.4-3" (forall (y x) (<=> (mon y 3 x) (March y x))))
(defaxiom "4.4-4" (forall (y x) (<=> (mon y 4 x) (April y x))))
(defaxiom "4.4-5" (forall (y x) (<=> (mon y 5 x) (May y x))))
(defaxiom "4.4-6" (forall (y x) (<=> (mon y 6 x) (June y x))))
(defaxiom "4.4-7" (forall (y x) (<=> (mon y 7 x) (July y x))))
(defaxiom "4.4-8" (forall (y x) (<=> (mon y 8 x) (August y x))))
(defaxiom "4.4-9" (forall (y x) (<=> (mon y 9 x) (September y x))))
(defaxiom "4.4-10" (forall (y x) (<=> (mon y 10 x) (October y x))))
(defaxiom "4.4-11" (forall (y x) (<=> (mon y 11 x) (November y x))))
(defaxiom "4.4-12" (forall (y x) (<=> (mon y 12 x) (December y x))))
(defaxiom "4.4-13" (forall (m y) (=> (January m y) (Hath 31 *Day* m))))
(defaxiom "4.4-14" (forall (m y) (=> (March m y) (Hath 31 *Day* m))))
(defaxiom "4.4-15" (forall (m y) (=> (April m y) (Hath 30 *Day* m))))
(defaxiom "4.4-16" (forall (m y) (=> (May m y) (Hath 31 *Day* m))))
(defaxiom "4.4-17" (forall (m y) (=> (June m y) (Hath 30 *Day* m))))
(defaxiom "4.4-18" (forall (m y) (=> (July m y) (Hath 31 *Day* m))))
(defaxiom "4.4-19" (forall (m y) (=> (August m y) (Hath 31 *Day* m))))
(defaxiom "4.4-20"
(forall (m y) (=> (September m y) (Hath 30 *Day* m))))
(defaxiom "4.4-21" (forall (m y) (=> (October m y) (Hath 31 *Day* m))))
(defaxiom "4.4-22" (forall (m y) (=> (November m y) (Hath 30 *Day* m))))
(defaxiom "4.4-23" (forall (m y) (=> (December m y) (Hath 31 *Day* m))))
(defaxiom "4.4-24"
(forall (y)
(forall (z)
(<=> (leap-year y)
(exists (n x)
(and (year y n (CE z))
(or (divides 400 n)
(and (divides 4 n) (not (divides 100 n))))))))))
(defaxiom "4.4-25"
(forall (m y)
(=> (and (February m y) (leap-year y)) (Hath 29 *Day* m))))
(defaxiom "4.4-26"
(forall (m y)
(=> (and (February m y) (not (leap-year y))) (Hath 28 *Day* m))))
(defaxiom "4.4-27"
(forall (T)
(<=> (month T)
(exists (t1 t2 d1 d2 n m1 m2 n1 y1 y2 n2 e)
(and (and (begins t1 T) (ends t2 T))
(and (and (and (and (and (and (begins-or-in t1 d1)
(begins-or-in t2 d2))
(da d1 n m1))
(mon m1 n1 y1))
(yr y1 n2 e))
(da d2 n m2))
(or (mon m2 (plus n1 1) y1)
(exists (y2)
(and (and (equals n1 12) (mon m2 1 y2))
(yr y2 (plus n2 1) e))))))))))
(defaxiom "4.5-1"
(forall (t y m d h n s z)
(<=> (time-of t y m d h n s z)
(begins-or-in t
(secFn s (minFn n (hrFn h (daFn d (monFn m (yrFn y (CE z)))))))))))
(defaxiom "4.5-2"
(forall (t y m d h n s z)
(<=> (time-of t y m d h n s z)
(exists (s1 n1 h1 d1 m1 y1 e)
(and (and (and (and (and (and (and (begins-or-in t s1)
(sec s1 s n1))
(min n1 n h1))
(hr h1 h d1))
(da d1 d m1))
(mon m1 m y1))
(yr y1 y e))
(CEPred e z))))))
(defaxiom "4.5-3"
(forall (t y m d h n s z)
(<=> (time-of t y m d h n s z)
(exists (d1)
(and (and (and (and (and (and (and (temporal-description d1 t)
(equals (year-of d1) y))
(equals (month-of d1) m))
(equals (day-of d1) d))
(equals (hour-of d1) h))
(equals (minute-of d1) n))
(equals (second-of d1) s))
(equals (time-zone-of d1) z))))))
(defaxiom "4.5-4"
(forall (d1 y)
(=> (equals (year-of d1) y)
(exists (t) (temporal-description d1 t)))))
(defaxiom "4.5-5"
(forall (d1 m)
(=> (equals (month-of d1) m)
(exists (t) (temporal-description d1 t)))))
(defaxiom "4.5-6"
(forall (d1 d)
(=> (equals (day-of d1) d) (exists (t) (temporal-description d1 t)))))
(defaxiom "4.5-7"
(forall (d1 h)
(=> (equals (hour-of d1) h)
(exists (t) (temporal-description d1 t)))))
(defaxiom "4.5-8"
(forall (d1 n)
(=> (equals (minute-of d1) n)
(exists (t) (temporal-description d1 t)))))
(defaxiom "4.5-9"
(forall (d1 s)
(=> (equals (second-of d1) s)
(exists (t) (temporal-description d1 t)))))
(defaxiom "4.5-10"
(forall (d1 z)
(=> (equals (time-zone-of d1) z)
(exists (t) (temporal-description d1 t)))))
(defaxiom "6.1-1"
(forall (T1 T2)
(<=> (ibefore T1 T2)
(or (before T1 T2)
(and (and (proper-interval T1) (proper-interval T2))
(int-meets T1 T2))))))
(defaxiom "6.1-2"
(forall (t)
(forall (T1 T2)
(<=> (iinside-1 T1 T2)
(or (or (or (equals T1 T2)
(and (and (instant T1) (proper-interval T2))
(inside T1 T2)))
(and (and (and (exists (t) (begins t T1)) (ends t T1))
(proper-interval T2))
(inside t T2)))
(and (and (proper-interval T1) (proper-interval T2))
(or (or (or (int-starts T1 T2) (int-during T1 T2))
(int-finishes T1 T2))
(int-equals T1 T2))))))))
(defaxiom "6.1-3"
(forall (s)
(<=> (tseq s)
(and (forall (t) (=> (member t s) (temporal-entity t)))
(forall (t1 t2)
(=> (and (member t1 s) (member t2 s))
(or (or (equals t1 t2) (ibefore t1 t2)) (ibefore t2 t1))))))))
(defaxiom "6.1-4"
(forall (s p)
(<=> (tseqp s p)
(and (tseq s) (forall (t) (=> (member t s) (p t)))))))
(defaxiom "6.1-5"
(forall (t1 u t2)
(forall (s)
(=>
(<=> (uniform-tseq s)
(forall (t1 t2 u)
(and (and (member t1 s) (member t2 s)) (temporal-unit u))))
(equals (duration t1 u) (duration t2 u))))))
(defaxiom "6.1-6"
(forall (s1 s2)
(<=> (equiv-tseq s1 s2)
(and (and (tseq s1) (tseq s2))
(forall (t)
(=> (temporal-entity t)
(<=> (exists (t1) (and (member t1 s1) (iinside-1 t t1)))
(exists (t2) (and (member t2 s2) (iinside-1 t t2))))))))))
(defaxiom "6.1-7"
(forall (s)
(<=> (min-tseq s)
(forall (t1 t2)
(=> (and (member t1 s) (member t2 s))
(or (equals t1 t2)
(exists (t)
(and (and (ibefore t1 t) (ibefore t t2))
(not (member t s))))))))))
(defaxiom "6.1-8"
(forall (s1 s)
(<=> (min-equiv-tseq s1 s) (and (min-tseq s1) (equiv-tseq s1 s)))))
(defaxiom "6.1-9"
(forall (t s)
(<=> (iinside t s)
(or (and (and (temporal-entity t) (temporal-entity s))
(iinside-1 t s))
(and (and (temporal-entity t) (tseq s))
(exists (s1 t1)
(and (and (min-equiv-tseq s1 s) (member t1 s1))
(iinside-1 t t1))))))))
(defaxiom "6.1-10"
(forall (s s0)
(<=> (isubset s s0)
(and (and (tseq s) (tseq s0))
(forall (t) (=> (member t s) (iinside t s0)))))))
(defaxiom "6.1-11"
(forall (s1 s2)
(<=> (idisjoint s1 s2)
(and (and (tseq s1) (tseq s2))
(not (exists (t t1 t2)
(and (and (and (member t1 s1) (member t2 s2))
(iinside t t1))
(iinside t t2))))))))
(defaxiom "6.1-12"
(forall (t s)
(<=> (first t s)
(and (and (tseq s) (member t s))
(forall (t1)
(=> (member t1 s) (or (equals t1 t) (ibefore t t1))))))))
(defaxiom "6.1-13"
(forall (t s)
(<=> (last t s)
(and (and (tseq s) (member t s))
(forall (t1)
(=> (member t1 s) (or (equals t1 t) (ibefore t1 t))))))))
(defaxiom "6.1-14"
(forall (n)
(forall (t s)
(<=> (nth t n s)
(and (and (and (tseq s) (member t s)) (natnum n))
(exists (s1)
(and (forall (t1)
(<=> (member t1 s1)
(and (member t1 s) (ibefore t1 t))))
(equals (card s1) n-1))))))))
(defaxiom "6.1-15"
(forall (t1 t2 s n)
(<=> (nbetw t1 t2 s n)
(exists (s1)
(and (equals (card s1) n)
(forall (t)
(<=> (member t s1)
(and (and (ibefore t1 t) (ibefore t t2)) (member t s)))))))))
(defaxiom "6.1-16"
(forall (t s)
(<=> (convex-hull t s)
(and (and (and (tseq s) (interval t))
(forall (t1) (=> (first t1 s) (int-starts t1 t))))
(forall (t2) (=> (last t2 s) (int-finishes t2 t)))))))
(defaxiom "6.1-17"
(forall (t1 t2 s s0 p n)
(<=> (ngap t1 t2 s s0 p n)
(and (and (and (and (and (and (member t1 s) (member t2 s))
(tseqp s p))
(tseq s0))
(isubset s s0))
(natnum n))
(exists (s1)
(and (and (equals (card s1) n-1) (idisjoint s s1))
(forall (t)
(<=> (member t s1)
(and (and (and (iinside t s0) (p t)) (ibefore t1 t))
(ibefore t t2))))))))))
(defaxiom "6.1-18"
(forall (s s0 p n)
(<=> (everynthp s s0 p n)
(and (and (and (and (and (tseqp s p) (tseq s0)) (natnum n))
(exists (t1)
(and (first t1 s)
(not (exists (t)
(and (iinside t s0)
(ngap t t1 s s0 p n)))))))
(exists (t2)
(and (last t2 s)
(not (exists (t)
(and (iinside t s0) (ngap t2 t s s0 p n)))))))
(forall (t1)
(or (last t1) (exists (t2) (ngap t1 t2 s s0 p n0))))))))
(defaxiom "6.1-19"
(forall (s s0 p)
(<=> (everyp s s0 p)
(forall (t) (<=> (member t s) (and (iinside t s0) (p t)))))))
(defaxiom "6.1-20"
(forall (s1 s2)
(<=> (groups-into s1 s2)
(and (and (and (tseq s1) (tseq s2)) (iinside s1 s2))
(forall (t)
(=> (member t s2)
(exists (s)
(and (subset s s1)
(min-equiv-tseq (singleton-set t) s)))))))))
(defaxiom "6.1-21"
(forall (s1 s2 r)
(=>
(<=> (groups-periodically-into s1 s2 r)
(and (and (groups-into s1 s2) (natnum r))
(forall (t1 t2 s3)
(and (and (and (and (member t1 s2) (member t2 s2))
(nbetw t1 t2 s2 r-1))
(subset s3 s1))
(groups-into s3 (singleton-set t1))))))
(exists (s4)
(and (and (subset s4 s1) (groups-into s4 (singleton-set t2)))
(equals (card s3) (card s4)))))))
(defaxiom "6.2-1"
(forall (Phi)
(forall (u) (=> (temporal-unit u) (equals (duration Phi u) 0)))))
(defaxiom "6.2-2"
(forall (t u)
(=> (and (temporal-entity t) (temporal-unit u))
(equals (duration (singleton-set t) u) (duration t u)))))
(defaxiom "6.2-3"
(forall (s1 s2 u)
(=>
(and (and (and (tseq s1) (tseq s2)) (idisjoint s1 s2))
(temporal-unit u))
(equals (duration (union s1 s2) u)
(plus (duration s1 u) (duration s2 u))))))