MAYBE Time: 0.008630 TRS: { flatten nil() -> nil(), flatten flatten x -> flatten x, flatten unit x -> flatten x, flatten ++(x, y) -> ++(flatten x, flatten y), flatten ++(unit x, y) -> ++(flatten x, flatten y), ++(x, nil()) -> x, ++(nil(), y) -> y, ++(++(x, y), z) -> ++(x, ++(y, z)), rev nil() -> nil(), rev unit x -> unit x, rev ++(x, y) -> ++(rev y, rev x), rev rev x -> x} DP: DP: { flatten# unit x -> flatten# x, flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> ++#(flatten x, flatten y), flatten# ++(unit x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# y, flatten# ++(unit x, y) -> ++#(flatten x, flatten y), ++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(y, z), rev# ++(x, y) -> ++#(rev y, rev x), rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y} TRS: { flatten nil() -> nil(), flatten flatten x -> flatten x, flatten unit x -> flatten x, flatten ++(x, y) -> ++(flatten x, flatten y), flatten ++(unit x, y) -> ++(flatten x, flatten y), ++(x, nil()) -> x, ++(nil(), y) -> y, ++(++(x, y), z) -> ++(x, ++(y, z)), rev nil() -> nil(), rev unit x -> unit x, rev ++(x, y) -> ++(rev y, rev x), rev rev x -> x} EDG: {(flatten# ++(unit x, y) -> ++#(flatten x, flatten y), ++#(++(x, y), z) -> ++#(y, z)) (flatten# ++(unit x, y) -> ++#(flatten x, flatten y), ++#(++(x, y), z) -> ++#(x, ++(y, z))) (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z)) (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z))) (rev# ++(x, y) -> ++#(rev y, rev x), ++#(++(x, y), z) -> ++#(x, ++(y, z))) (rev# ++(x, y) -> ++#(rev y, rev x), ++#(++(x, y), z) -> ++#(y, z)) (flatten# ++(x, y) -> ++#(flatten x, flatten y), ++#(++(x, y), z) -> ++#(x, ++(y, z))) (flatten# ++(x, y) -> ++#(flatten x, flatten y), ++#(++(x, y), z) -> ++#(y, z))} STATUS: arrows: 0.944444 SCCS (1): Scc: {++#(++(x, y), z) -> ++#(y, z)} SCC (1): Strict: {++#(++(x, y), z) -> ++#(y, z)} Weak: { flatten nil() -> nil(), flatten flatten x -> flatten x, flatten unit x -> flatten x, flatten ++(x, y) -> ++(flatten x, flatten y), flatten ++(unit x, y) -> ++(flatten x, flatten y), ++(x, nil()) -> x, ++(nil(), y) -> y, ++(++(x, y), z) -> ++(x, ++(y, z)), rev nil() -> nil(), rev unit x -> unit x, rev ++(x, y) -> ++(rev y, rev x), rev rev x -> x} Open