YES TRS: { 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))} RUF: Strict: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)), lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))} Weak: {} DP: Strict: { concat#(cons(U, V), Y) -> concat#(V, Y), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z), lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))} Weak: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)), lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))} EDG: {(lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z), concat#(cons(U, V), Y) -> concat#(V, Y)) (lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V), concat#(cons(U, V), Y) -> concat#(V, Y)) (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V)) (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z)) (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))) (concat#(cons(U, V), Y) -> concat#(V, Y), concat#(cons(U, V), Y) -> concat#(V, Y))} SCCS: Scc: {lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))} Scc: {concat#(cons(U, V), Y) -> concat#(V, Y)} SCC: Strict: {lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))} Weak: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)), lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))} POLY: Argument Filtering: pi(lessleaves#) = [0,1], pi(lessleaves) = [], pi(cons) = [0,1], pi(concat) = 0 Usable Rules: {} Interpretation: [lessleaves#](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1 + 1 Strict: {} Weak: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)), lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))} Qed SCC: Strict: {concat#(cons(U, V), Y) -> concat#(V, Y)} Weak: { concat(cons(U, V), Y) -> cons(U, concat(V, Y)), lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))} SPSC: Simple Projection: pi(concat#) = 0 Strict: {} Qed