(define (domain daml-temporal-aggregates)
   (:extends daml-time-event daml-clock-calendar)
   
   (:types
       Temporal-seq - Set)

   (:predicates
      (time-span int - (Alt Temporal-entity Temporal-seq)
                 e - Eventuality)

    (ibefore t1 t2 - Temporal-entity)

     (iinside-1 t1 t2 - Temporal-entity)

    (tseqp s - Temporal-seq p - (Fun Prop (Obj)))

     (uniform-tseq s - Temporal-seq)

     (equiv-tseq s1 s2 - Temporal-seq)

     (min-tseq s - Temporal-seq)

     (min-equiv-tseq s1 s - Temporal-seq)

     (iinside tx - Temporal-entity s - (Alt Temporal-entity Temporal-seq))

     (isubset s1 s2 - Temporal-seq)

     (idisjoint s1 s2 - Temporal-seq)

     (first tx - Temporal-entity s - Temporal-seq)

     (last tx - Temporal-entity s - Temporal-seq)

     (nth tx - Temporal-entity n - Integer s - Temporal-seq)

     (nbetw tx1 tx2 - Temporal-entity s - Temporal-seq n - Integer)

     (convex-hull tv - Interval s - Temporal-seq)

     (ngap t1 t2 - Temporal-entity s1 s2 - Temporal-seq 
           p - (Fun Prop <- (Obj)) n - Integer)

     (everynthp s1 s2 - Temporal-seq p - (Fun Prop <- (Obj)) n - Integer)

     (everyp s1 s2 - Temporal-seq p - (Fun Prop <- (Obj)))

     (groups-into s1 s2 - Temporal-seq)

     (groups-periodically-into s1 s2 - Temporal-seq r - Integer)

   )
   (:functions
     (seq-duration s - Temporal-seq u - Temporal-unit)
     - Number

   )
   (:axioms
       ;; Axiom "2.5-6"
       (forall (tv - Interval e - Eventuality)
          (if (time-span tv e)
              (during e tv)))
       ;; Axiom "2.5-7"
       (forall (ti - Instant e - Eventuality)
          (if (time-span ti e)
              (at-time e ti)))
       ;; Axiom "2.5-8"
       (forall (tv - Interval ti - Instant e - Eventuality)
          (if (and (time-span tv e)
                   (not (inside ti tv))
                   (not (begins ti tv))
                   (not (ends ti tv)))
              (not (at-time e ti))))
       ;; Axiom "2.5-9"
       (forall (ti t1 - Instant e - Eventuality)
          (if (and (time-span ti e)
                   (not (= ti t1)))
              (not (at-time e t1))))
    ;; Axiom "6.1-1"
    (forall (t1 t2 - Temporal-entity)
       (iff (ibefore t1 t2)
            (or (before t1 t2) 
                (and (is Proper-interval t1) 
                     (is Proper-interval t2)
                     (int-meets t1 t2)))))

    ;; Axiom "6.1-2"
    (forall (t1 t2 - Temporal-entity)
       (iff (iinside-1 t1 t2)
            (or (= t1 t2) 
                (and (is Instant t1) 
                     (is Proper-interval t2)
                     (inside t1 t2))
                (exists (ti - Instant) 
                   (and (begins ti t1) 
                        (ends ti t1) 
                        (is Proper-interval t2) 
                        (inside ti t2)))
                (and (is Proper-interval t1) 
                     (is Proper-interval t2)
                     (or (int-starts t1 t2)
                         (int-during t1 t2)
                         (int-finishes t1 t2)
                         (int-equals t1 t2))))))


    ;; Axiom "6.1-3"
    (and (forall (s - Temporal-seq)
            (and (forall (x) (if (member x s) (is Temporal-entity x)))
                 (forall (t1 t2)
                       (if (and (member t1 s) (member t2 s))
                           (or (= t1 t2) (ibefore t1 t2) (ibefore t2 t1))))))

         (forall (s - Set)
            (if (and (forall (x) (if (member x s) (is Temporal-entity x)))
                     (forall (t1 t2)
                       (if (and (member t1 s) (member t2 s))
                           (or (= t1 t2) (ibefore t1 t2) (ibefore t2 t1)))))
                (is Temporal-seq s))))

    ;; Axiom "6.1-4"
    (forall (s - Temporal-seq p - (Fun Prop (Obj)))
       (iff (tseqp s p) 
            (forall (tx) (if (member tx s) (p tx)))))


    ;; Axiom "6.1-5"
    (forall (s - Temporal-seq)
       (iff (uniform-tseq s)
            (or (forall (x) (if (member x s) (is Instant x)))
                (and (forall (x) (if (member x s) (is Interval x)))
                     (forall (t1 t2 - Interval u - Temporal-unit)
                        (if (and (member t1 s) (member t2 s))
                            (= (duration t1 u) (duration t2 u))))))))


    ;; Axiom "6.1-6"
    (forall (s1 s2 - Temporal-seq)
       (iff (equiv-tseq s1 s2)
            (forall (tx - Temporal-entity)
               (iff (exists (t1) (and (member t1 s1) (iinside-1 tx t1)))
                    (exists (t2) (and (member t2 s2) (iinside-1 tx t2)))))))

     ;; Axiom "6.1-7"
     (forall (s - Temporal-seq)
        (iff (min-tseq s)
             (not (exists (tv1 tv2 - Proper-interval)
                     (and (member tv1 s) (member tv2 s)
                          (int-meets tv1 tv2))))))

     ;; Axiom "6.1-8"
     (forall (s1 s - Temporal-seq)
        (iff (min-equiv-tseq s1 s) 
             (and (min-tseq s1) (equiv-tseq s1 s))))

     ;; Axiom "6.1-9"
     (forall (tx - Temporal-entity s - (Alt Temporal-entity Temporal-seq))
        (iff (iinside tx s)
             (or (and (is Temporal-entity s)
                      (iinside-1 tx s))
                 (and (is Temporal-seq s)
                      (exists (s1 t1)
                         (and (min-equiv-tseq s1 s) 
                              (member t1 s1)
                              (iinside-1 tx t1)))))))

     ;; Axiom "6.1-10"
     (forall (s s0 - Temporal-seq)
        (iff (isubset s s0)
             (forall (tx - Temporal-entity)
               (if (member tx s) (iinside tx s0)))))

     ;; Axiom "6.1-11"
     (forall (s1 s2 - Temporal-seq)
        (iff (idisjoint s1 s2)
             (not (exists (tx t1 t2)
                     (and (member t1 s1) (member t2 s2) 
                          (iinside tx t1) (iinside tx t2))))))


     ;; Axiom "6.1-12"
     (forall (tx - Temporal-entity s - Temporal-seq)
        (iff (first tx s)
             (and (member tx s)
                  (forall (t1) 
                     (if (member t1 s) (or (= t1 tx) (ibefore tx t1)))))))


     ;; Axiom "6.1-13"
     (forall (tx - Temporal-entity s - Temporal-seq)
        (iff (last tx s)
             (and (member tx s)
                  (forall (t1) 
                     (if (member t1 s) (or (= t1 tx) (ibefore t1 tx)))))))

     ;; Axiom "6.1-14"
     (forall (tx - Temporal-entity n - Integer s - Temporal-seq)
        (iff (nth tx n s)
             (and (member tx s)
                  (exists (s1 - Set)
                     (and (forall (t1) 
                             (iff (member t1 s1) 
                                  (and (member t1 s) (ibefore t1 tx))))
                          (= (card s1) (- n 1)))))))

     ;; Axiom "6.1-15"
     (forall (t1 t2 - Temporal-entity s - Temporal-seq n - Integer)
        (iff (nbetw t1 t2 s n)
             (exists (s1)
                (and (= (card s1) n)
                     (forall (tx)
                        (iff (member tx s1) 
                             (and (ibefore t1 tx) (ibefore tx t2) (member tx s))))))))

     ;; Axiom "6.1-16"
     (forall (tv - Proper-interval s - Temporal-seq)
        (iff (convex-hull tv s)
             (and (forall (t1) (if (first t1 s) (int-starts t1 tv)))
                  (forall (t2) (if (last t2 s) (int-finishes t2 tv))))))

     ;; Axiom "6.1-17"
     (forall (t1 t2 - Temporal-entity s s0 - Temporal-seq 
              p - (Fun Prop <- (Obj)) n - Integer)
        (iff (ngap t1 t2 s s0 p n)
             (and (member t1 s) (member t2 s)
                  (tseqp s p) 
                  (isubset s s0) 
                  (>= n 0)
                  (exists (s1)
                     (and (= (card s1) (- n 1)) 
                          (idisjoint s s1)
                          (forall (tx)
                             (iff (member tx s1)
                                  (and (iinside tx s0) 
                                       (p tx)
                                       (ibefore t1 tx)
                                       (ibefore tx t2)))))))))

     ;; Axiom "6.1-18"
     (forall (s s0 p n)
        (iff (everynthp s s0 p n)
             (and (tseqp s p)
                  (>= n 0)
                  (exists (t1)
                     (and (first t1 s) 
                          (not (exists (tx) 
                                  (and (iinside tx s0) (ngap tx t1 s s0 p n))))))
                  (exists (t2)
                     (and (last t2 s) 
                          (not (exists (tx) 
                                  (and (iinside tx s0) (ngap t2 tx s s0 p n))))))
                  (forall (t1) 
                     (or (last t1 s) 
                         (exists (t2) (ngap t1 t2 s s0 p n)))))))

     ;; Axiom "6.1-19"
     (forall (s s0 - Temporal-seq p - (Fun Prop <- (Obj)))
        (iff (everyp s s0 p) 
             (forall (tx) 
                (iff (member tx s) (and (iinside tx s0) (p tx))))))

     ;; Axiom "6.1-20"
     (forall (s1 s2 - Temporal-seq)
       (iff (groups-into s1 s2)
            (and (forall (tv - Temporal-entity)
                    (if (member tv s1) (iinside tv s2)))
                 (forall (tx - Temporal-entity)
                    (if (member tx s2)
                        (exists (sub2 sub1 - Temporal-seq )
                           (and (subset sub1 s1)
                                (= (singleton tx) sub2)
                                (min-equiv-tseq sub2 sub1))))))))

     ;; Axiom "6.1-21"
     (forall (s1 s2 - Temporal-seq r - Integer)
        (iff (groups-periodically-into s1 s2 r)
             (and (groups-into s1 s2) 
                  (>= r 0)
                  (forall (t1 t2 s3)
                     (if (and (member t1 s2) (member t2 s2) 
                              (nbetw t1 t2 s2 (- r 1))
                              (subset s3 s1)
                              (exists (seq1 - Temporal-seq)
                                 (and (= (singleton t1) seq1)
                                      (groups-into s3 seq1))))
                         (exists (s4 seq2 - Temporal-seq)
                            (and (subset s4 s1)
                                 (= (singleton t2) seq2)
                                 (groups-into s4 seq2)
                                 (= (card s3) (card s4)))))))))

     ;; Axiom "6.2-1"
     (forall (u - Temporal-unit s - Temporal-seq)
        (if (= empty-set s)
            (= (seq-duration s u) 0)))

     ;; Axiom "6.2-2"
     (forall (tx - Interval u - Temporal-unit seq - Temporal-seq)
        (if (= (singleton tx) seq)
            (= (seq-duration seq u) (duration tx u))))

     ;; Axiom "6.2-3"
     (forall (s1 s2 - Temporal-seq u - Temporal-unit)
        (if (idisjoint s1 s2)
            (exists (seq - Temporal-seq)
               (and (= (union s1 s2) seq)
                    (= (seq-duration seq u)
                       (+ (seq-duration s1 u) (seq-duration s2 u)))))))

   )
)