(STRATEGY
    INNERMOST)

(VAR
    e11 e12 e21 e22 edges u v x x'
    xs xs' y)
(DATATYPES
    A = µX.< S(X), E(X, X), Cons(X, X), 0, Nil, True, False >)
(SIGNATURES
    getNodeFromEdge :: [A x A] -> A
    via :: [A x A x A x A] -> A
    member :: [A x A] -> A
    eqEdge :: [A x A] -> A
    notEmpty :: [A] -> A
    reach :: [A x A x A] -> A
    goal :: [A x A x A] -> A
    !EQ :: [A x A] -> A
    and :: [A x A] -> A
    via[Ite] :: [A x A x A x A x A] -> A
    via[Let] :: [A x A x A x A x A] -> A
    member[Ite] :: [A x A x A] -> A
    reach[Ite] :: [A x A x A x A] -> A
    eqEdge[Ite] :: [A x A x A x A x A] -> A)
(RULES
    getNodeFromEdge(S(S(x'))
                   ,E(x,y)) -> y
    via(u
       ,v
       ,Cons(E(x,y),xs)
       ,edges) -> via[Ite](!EQ(u,x)
                          ,u
                          ,v
                          ,Cons(E(x,y),xs)
                          ,edges)
    getNodeFromEdge(S(0())
                   ,E(x,y)) -> x
    member(x',Cons(x,xs)) ->
      member[Ite](eqEdge(x',x)
                 ,x'
                 ,Cons(x,xs))
    getNodeFromEdge(0(),E(x,y)) -> x
    eqEdge(E(e11,e12),E(e21,e22)) ->
      eqEdge[Ite](and(!EQ(e11,e21)
                     ,!EQ(e12,e22))
                 ,e21
                 ,e22
                 ,e11
                 ,e12)
    via(u,v,Nil(),edges) -> Nil()
    notEmpty(Cons(x,xs)) -> True()
    notEmpty(Nil()) -> False()
    member(x,Nil()) -> False()
    reach(u,v,edges) ->
      reach[Ite](member(E(u,v),edges)
                ,u
                ,v
                ,edges)
    goal(u,v,edges) -> reach(u
                            ,v
                            ,edges)
    !EQ(S(x),S(y)) ->= !EQ(x,y)
    !EQ(0(),S(y)) ->= False()
    !EQ(S(x),0()) ->= False()
    !EQ(0(),0()) ->= True()
    and(False(),False()) ->= False()
    and(True(),False()) ->= False()
    and(False(),True()) ->= False()
    and(True(),True()) ->= True()
    via[Ite](True()
            ,u
            ,v
            ,Cons(E(x,y),xs)
            ,edges) ->= via[Let](u
                                ,v
                                ,Cons(E(x,y),xs)
                                ,edges
                                ,reach(y,v,edges))
    via[Let](u
            ,v
            ,Cons(x,xs)
            ,edges
            ,Nil()) ->= via(u,v,xs,edges)
    via[Let](u
            ,v
            ,Cons(x,xs)
            ,edges
            ,Cons(x',xs')) ->= Cons(x
                                   ,Cons(x',xs'))
    via[Ite](False()
            ,u
            ,v
            ,Cons(x,xs)
            ,edges) ->= via(u,v,xs,edges)
    member[Ite](False()
               ,x'
               ,Cons(x,xs)) ->= member(x',xs)
    reach[Ite](False()
              ,u
              ,v
              ,edges) ->= via(u,v,edges,edges)
    reach[Ite](True(),u,v,edges) ->=
      Cons(E(u,v),Nil())
    member[Ite](True(),x,xs) ->=
      True()
    eqEdge[Ite](False()
               ,e21
               ,e22
               ,e11
               ,e12) ->= False()
    eqEdge[Ite](True()
               ,e21
               ,e22
               ,e11
               ,e12) ->= True())