;; 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))))))