(define (domain daml-time-granularity)
   (:extends daml-time-axis)
   
   (:types Granularity - Set)

   (:predicates
      (indisting x1 x2 - Obj g - Granularity)
   )

   (:functions
     (f-gran s - Set f - (Fun Set <- (Obj)))
     - Granularity

      (d-gran s - Set d - (Fun Number <- (Obj Obj)) a - Number)
      - Granularity

   )

   (:axioms

      ;; Axiom "5.0-4"
      (forall (x1 x2 - Object g - Granularity)
         (iff (indisting x1 x2 g)
              (exists (s) (and (member s g) (member x1 s) (member x2 s)))))
      ;; Axiom "5.0-5"
      (forall (s - Set g - Granularity f - (Fun Set <- (Obj)))
         (iff (= g (f-gran s f))
              (and (cover g s)
                   (forall (x1 x2) 
                      (iff (indisting x1 x2 g) 
                           (= (f x1) (f x2))))
                   (forall (c1 c2 - Set x1 x2 - Obj)
                      (if (and (member c1 g)
                               (member c2 g)
                               (member x1 c1)
                               (member x2 c2)
                               (= (f x1) (f x2)))
                          (= c1 c2))))))

   ;; Axiom "5.0-6"
   (forall (g - Granularity s - Set 
            d - (Fun Number <- (Obj Obj)) a - Number)
      (iff (= g (d-gran s d a))
           (and (cover g s)
                (forall (x1 x2) 
                   (iff (indisting x1 x2 g) 
                        (< (d x1 x2) a))))))

   ))