fmod TIME is

    sorts Time Hour Min Sec .

    op _:_:_ : Hour Min Sec -> Time .
    
    op _.hour : Time -> Hour .
    op _.min : Time -> Min .
    op _.sec : Time -> Sec .
    
    var H : Hour .
    var M : Min .
    var S : Sec .
    
    eq (H : M : S).hour = H .
    eq (H : M : S).min = M .
    eq (H : M : S).sec = S .
endfm