MAYBE Time: 0.001741 TRS: { 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))} DP: DP: { concat#(cons(u, v), y) -> concat#(v, y), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))} TRS: { 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))} UR: { concat(leaf(), y) -> y, concat(cons(u, v), y) -> cons(u, concat(v, y))} EDG: {(less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v)) (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z)) (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))} STATUS: arrows: 0.812500 SCCS (1): Scc: {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))} SCC (1): Strict: {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))} Weak: { 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))} Open