in nat.maude
in a-graph.maude

fmod PATH is
   protecting NAT .
   protecting A-GRAPH .

   sorts Path Path? .
   subsorts Edge < Path < Path? .
   op _;_ : Path? Path? -> Path? [assoc] .
   ops source target : Path -> Node .
   op length : Path -> Nat .

   var E : Edge .
   var P : Path .

   cmb (E ; P) : Path if target(E) == source(P) .

   eq source(E ; P) = source(E) .
   eq target(P ; E) = target(E) .
   eq length(E) = s(0) .
   eq length(E ; P) = s(0) + length(P) .
endfm

red (b ; c ; d) .
***(
reduce in PATH : b ; c ; d .
rewrites: 13 in -10ms cpu (0ms real) (~ rewrites/second)
result Path: b ; c ; d
)

red length(b ; c ; d) .
***(
reduce in PATH : length(b ; c ; d) .
rewrites: 23 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(0)))
)

red (a ; b ; c) .
***(
reduce in PATH : a ; b ; c .
rewrites: 13 in -10ms cpu (0ms real) (~ rewrites/second)
result Path?: a ; b ; c
)

red source(a ; b ; c) .
***(
reduce in PATH : source(a ; b ; c) .
rewrites: 13 in -10ms cpu (0ms real) (~ rewrites/second)
result Error(Node): source(a ; b ; c)
)

red target(a ; b ; c) .
***(
reduce in PATH : target(a ; b ; c) .
rewrites: 13 in -10ms cpu (0ms real) (~ rewrites/second)
result Error(Node): target(a ; b ; c)
)

red length(a ; b ; c) .
***(
reduce in PATH : length(a ; b ; c) .
rewrites: 13 in -10ms cpu (0ms real) (~ rewrites/second)
result Error(Nat): length(a ; b ; c)
)