fmod PATH is pr QID . sorts Node Edge Path . subsort Qid < Node . subsort Edge < Path . op _->_ : Node Node -> Edge [ctor prec 40]. op _:_ : Path Path -> [Path] [ctor assoc prec 50]. var N N' : Node . var E : Edge . var P Q : Path . op source : Path -> Node . eq source((N -> N') : P:[Path]) = N . eq source(N -> N') = N . op target : Path -> Node . eq target(P : (N -> N')) = N' . eq target(N -> N') = N' . cmb target(P:[Path]) : Node if P:[Path] : Path . cmb (P : Q) : Path if target(P) = source(Q) . endfm