(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR @l1 @l2 @t @t1 @t2 @x @xs )
(STRATEGY INNERMOST)
(RULES 
        append(@l1, @l2) -> append#1(@l1, @l2)
        append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
        append#1(nil, @l2) -> @l2
        subtrees(@t) -> subtrees#1(@t)
        subtrees#1(leaf) -> nil
        subtrees#1(node(@x, @t1, @t2)) -> subtrees#2(subtrees(@t1), @t1, @t2, @x)
        subtrees#2(@l1, @t1, @t2, @x) -> subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
        subtrees#3(@l2, @l1, @t1, @t2, @x) -> ::(node(@x, @t1, @t2), append(@l1, @l2))
        
)