Term Rewriting System R:

   [Y, U, V, X, W, Z]
   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))

Termination of R to be shown.


Removing the following rules from R which fullfill a polynomial ordering: 

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

where the Polynomial interpretation:
POL(concat(x_1, x_2)) = x_1 + x_2
POL(true) = 0
POL(leaf) = 1
POL(lessleaves(x_1, x_2)) = x_1 + x_2
POL(false) = 0
POL(cons(x_1, x_2)) = x_1 + x_2
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   concat(cons(U, V), Y) -> cons(U, concat(V, Y))
   lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))

where the Polynomial interpretation:
POL(concat(x_1, x_2)) = 2*x_1 + x_2
POL(lessleaves(x_1, x_2)) = 2 + x_1 + x_2
POL(cons(x_1, x_2)) = 1 + 2*x_1 + x_2
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.406 seconds.