(STRATEGY
    INNERMOST)

(VAR
    h i u v x y)
(DATATYPES
    A = µX.< 0, true, s(X), false, empty, edge(X, X, X) >)
(SIGNATURES
    eq :: [A x A] -> A
    or :: [A x A] -> A
    union :: [A x A] -> A
    reach :: [A x A x A x A] -> A
    if_reach_1 :: [A x A x A x A x A] -> A
    if_reach_2 :: [A x A x A x A x A] -> A)
(RULES
    eq(0(),0()) -> true()
    eq(0(),s(x)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    or(true(),y) -> true()
    or(false(),y) -> y
    union(empty(),h) -> h
    union(edge(x,y,i),h) -> edge(x
                                ,y
                                ,union(i,h))
    reach(x,y,empty(),h) -> false()
    reach(x,y,edge(u,v,i),h) ->
      if_reach_1(eq(x,u)
                ,x
                ,y
                ,edge(u,v,i)
                ,h)
    if_reach_1(true()
              ,x
              ,y
              ,edge(u,v,i)
              ,h) -> if_reach_2(eq(y,v)
                               ,x
                               ,y
                               ,edge(u,v,i)
                               ,h)
    if_reach_2(true()
              ,x
              ,y
              ,edge(u,v,i)
              ,h) -> true()
    if_reach_2(false()
              ,x
              ,y
              ,edge(u,v,i)
              ,h) -> or(reach(x,y,i,h)
                       ,reach(v,y,union(i,h),empty()))
    if_reach_1(false()
              ,x
              ,y
              ,edge(u,v,i)
              ,h) -> reach(x,y,i,edge(u,v,h)))