(STRATEGY
    INNERMOST)

(VAR
    @a @as @futurequeue @queue
    @sofar @t @t' @t1 @t2 @toreverse
    @ts @x @x_1 @x_2 @x_3 @xs @y
    @y_1 @y_2 @y_3)
(DATATYPES
    A = µX.< ::(X, X), nil, leaf, node(X, X, X), #false, #true, #0, #neg(X), #pos(X), #s(X) >)
(SIGNATURES
    #equal :: [A x A] -> A
    appendreverse :: [A x A] -> A
    appendreverse#1 :: [A x A] -> A
    bfs :: [A x A x A] -> A
    bfs#1 :: [A x A x A] -> A
    bfs#2 :: [A x A] -> A
    bfs#3 :: [A x A x A x A] -> A
    bfs#4 :: [A x A x A x A x A x A x A] -> A
    bfs2 :: [A x A] -> A
    bfs2#1 :: [A x A] -> A
    dfs :: [A x A] -> A
    dfs#1 :: [A x A] -> A
    dfs#2 :: [A x A x A x A] -> A
    dfs#3 :: [A x A x A x A x A x A] -> A
    dobfs :: [A x A] -> A
    dodfs :: [A x A] -> A
    reverse :: [A] -> A
    #and :: [A x A] -> A
    #eq :: [A x A] -> A)
(RULES
    #equal(@x,@y) ->= #eq(@x,@y)
    appendreverse(@toreverse
                 ,@sofar) ->
      appendreverse#1(@toreverse
                     ,@sofar)
    appendreverse#1(::(@a,@as)
                   ,@sofar) -> appendreverse(@as
                                            ,::(@a,@sofar))
    appendreverse#1(nil(),@sofar) ->
      @sofar
    bfs(@queue,@futurequeue,@x) ->
      bfs#1(@queue,@futurequeue,@x)
    bfs#1(::(@t,@ts)
         ,@futurequeue
         ,@x) -> bfs#3(@t
                      ,@futurequeue
                      ,@ts
                      ,@x)
    bfs#1(nil(),@futurequeue,@x) ->
      bfs#2(@futurequeue,@x)
    bfs#2(::(@t,@ts),@x) ->
      bfs(reverse(::(@t,@ts))
         ,nil()
         ,@x)
    bfs#2(nil(),@x) -> leaf()
    bfs#3(leaf()
         ,@futurequeue
         ,@ts
         ,@x) -> bfs(@ts,@futurequeue,@x)
    bfs#3(node(@y,@t1,@t2)
         ,@futurequeue
         ,@ts
         ,@x) -> bfs#4(#equal(@x,@y)
                      ,@futurequeue
                      ,@t1
                      ,@t2
                      ,@ts
                      ,@x
                      ,@y)
    bfs#4(#false()
         ,@futurequeue
         ,@t1
         ,@t2
         ,@ts
         ,@x
         ,@y) -> bfs(@ts
                    ,::(@t2,::(@t1,@futurequeue))
                    ,@x)
    bfs#4(#true()
         ,@futurequeue
         ,@t1
         ,@t2
         ,@ts
         ,@x
         ,@y) -> node(@y,@t1,@t2)
    bfs2(@t,@x) -> bfs2#1(dobfs(@t
                               ,@x)
                         ,@x)
    bfs2#1(@t',@x) -> dobfs(@t',@x)
    dfs(@queue,@x) -> dfs#1(@queue
                           ,@x)
    dfs#1(::(@t,@ts),@x) -> dfs#2(@t
                                 ,@t
                                 ,@ts
                                 ,@x)
    dfs#1(nil(),@x) -> leaf()
    dfs#2(leaf(),@t,@ts,@x) ->
      dfs(@ts,@x)
    dfs#2(node(@a,@t1,@t2)
         ,@t
         ,@ts
         ,@x) -> dfs#3(#equal(@a,@x)
                      ,@t
                      ,@t1
                      ,@t2
                      ,@ts
                      ,@x)
    dfs#3(#false()
         ,@t
         ,@t1
         ,@t2
         ,@ts
         ,@x) -> dfs(::(@t1,::(@t2,@ts))
                    ,@x)
    dfs#3(#true()
         ,@t
         ,@t1
         ,@t2
         ,@ts
         ,@x) -> @t
    dobfs(@t,@x) -> bfs(::(@t,nil())
                       ,nil()
                       ,@x)
    dodfs(@t,@x) -> dfs(::(@t,nil())
                       ,@x)
    reverse(@xs) ->
      appendreverse(@xs,nil())
    #and(#false(),#false()) ->=
      #false()
    #and(#false(),#true()) ->=
      #false()
    #and(#true(),#false()) ->=
      #false()
    #and(#true(),#true()) ->=
      #true()
    #eq(#0(),#0()) ->= #true()
    #eq(#0(),#neg(@y)) ->= #false()
    #eq(#0(),#pos(@y)) ->= #false()
    #eq(#0(),#s(@y)) ->= #false()
    #eq(#neg(@x),#0()) ->= #false()
    #eq(#neg(@x),#neg(@y)) ->=
      #eq(@x,@y)
    #eq(#neg(@x),#pos(@y)) ->=
      #false()
    #eq(#pos(@x),#0()) ->= #false()
    #eq(#pos(@x),#neg(@y)) ->=
      #false()
    #eq(#pos(@x),#pos(@y)) ->=
      #eq(@x,@y)
    #eq(#s(@x),#0()) ->= #false()
    #eq(#s(@x),#s(@y)) ->= #eq(@x
                              ,@y)
    #eq(::(@x_1,@x_2)
       ,::(@y_1,@y_2)) ->=
      #and(#eq(@x_1,@y_1)
          ,#eq(@x_2,@y_2))
    #eq(::(@x_1,@x_2),leaf()) ->=
      #false()
    #eq(::(@x_1,@x_2),nil()) ->=
      #false()
    #eq(::(@x_1,@x_2)
       ,node(@y_1,@y_2,@y_3)) ->=
      #false()
    #eq(leaf(),::(@y_1,@y_2)) ->=
      #false()
    #eq(leaf(),leaf()) ->= #true()
    #eq(leaf(),nil()) ->= #false()
    #eq(leaf()
       ,node(@y_1,@y_2,@y_3)) ->=
      #false()
    #eq(nil(),::(@y_1,@y_2)) ->=
      #false()
    #eq(nil(),leaf()) ->= #false()
    #eq(nil(),nil()) ->= #true()
    #eq(nil()
       ,node(@y_1,@y_2,@y_3)) ->=
      #false()
    #eq(node(@x_1,@x_2,@x_3)
       ,::(@y_1,@y_2)) ->= #false()
    #eq(node(@x_1,@x_2,@x_3)
       ,leaf()) ->= #false()
    #eq(node(@x_1,@x_2,@x_3)
       ,nil()) ->= #false()
    #eq(node(@x_1,@x_2,@x_3)
       ,node(@y_1,@y_2,@y_3)) ->=
      #and(#eq(@x_1,@y_1)
          ,#and(#eq(@x_2,@y_2)
               ,#eq(@x_3,@y_3))))