/home/nowonder/forschung/aprove/TPDB05/TRS/AG01/#3.14.trs

The program

(from AG01 3.14)
(VAR u v w y z)
(RULES
concat(leaf,y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
less_leaves(x,leaf) -> false
less_leaves(leaf,cons(w,z)) -> true
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend