(STARTTERM
    CONSTRUCTOR-BASED)
(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)
(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))))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'bfs.raml', c.f. http://raml.tcs.ifi.lmu.de/)