/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/bintrees.trs

The program

(VAR U V W X Y Z)
(RULES

concat(leaf,Y) ->  Y
concat(cons(U,V),Y) -> cons(U,concat(V,Y))
lessleaves(X,leaf) -> false
lessleaves(leaf,cons(W,Z)) -> true
lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend