YES Time: 0.025354 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} UR: { 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))) (flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> ++#(flatten x, flatten y)) (flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# y) (flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# x) (flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> ++#(flatten x, flatten y)) (flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> flatten# y) (flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> flatten# x) (flatten# ++(x, y) -> flatten# y, flatten# unit x -> flatten# x) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# x) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> ++#(rev y, rev x)) (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z)) (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z))) (flatten# ++(x, y) -> flatten# x, flatten# ++(unit x, y) -> ++#(flatten x, flatten y)) (flatten# ++(x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# y) (flatten# ++(x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# x) (flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> ++#(flatten x, flatten y)) (flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# y) (flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# x) (flatten# ++(x, y) -> flatten# x, flatten# unit x -> flatten# x) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# x) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> ++#(rev y, rev x)) (flatten# ++(unit x, y) -> flatten# x, flatten# unit x -> flatten# x) (flatten# ++(unit x, y) -> flatten# x, flatten# ++(x, y) -> flatten# x) (flatten# ++(unit x, y) -> flatten# x, flatten# ++(x, y) -> flatten# y) (flatten# ++(unit x, y) -> flatten# x, flatten# ++(x, y) -> ++#(flatten x, flatten y)) (flatten# ++(unit x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# x) (flatten# ++(unit x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# y) (flatten# ++(unit x, y) -> flatten# x, flatten# ++(unit x, y) -> ++#(flatten x, flatten y)) (flatten# unit x -> flatten# x, flatten# unit x -> flatten# x) (flatten# unit x -> flatten# x, flatten# ++(x, y) -> flatten# x) (flatten# unit x -> flatten# x, flatten# ++(x, y) -> flatten# y) (flatten# unit x -> flatten# x, flatten# ++(x, y) -> ++#(flatten x, flatten y)) (flatten# unit x -> flatten# x, flatten# ++(unit x, y) -> flatten# x) (flatten# unit x -> flatten# x, flatten# ++(unit x, y) -> flatten# y) (flatten# unit x -> flatten# x, flatten# ++(unit x, y) -> ++#(flatten x, flatten y)) (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(x, ++(y, z))) (++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(y, z)) (flatten# ++(unit x, y) -> flatten# y, flatten# unit x -> flatten# x) (flatten# ++(unit x, y) -> flatten# y, flatten# ++(x, y) -> flatten# x) (flatten# ++(unit x, y) -> flatten# y, flatten# ++(x, y) -> flatten# y) (flatten# ++(unit x, y) -> flatten# y, flatten# ++(x, y) -> ++#(flatten x, flatten y)) (flatten# ++(unit x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# x) (flatten# ++(unit x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# y) (flatten# ++(unit x, y) -> flatten# y, flatten# ++(unit x, y) -> ++#(flatten x, flatten y)) (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.645833 SCCS (3): Scc: {rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y} Scc: { flatten# unit x -> flatten# x, flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# y} Scc: {++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(x, y), z) -> ++#(y, z)} SCC (2): Strict: {rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [++](x0, x1) = x0 + x1 + 1, [flatten](x0) = x0 + 1, [unit](x0) = 1, [rev](x0) = 0, [nil] = 1, [rev#](x0) = x0 Strict: rev# ++(x, y) -> rev# y 1 + 1x + 1y >= 0 + 1y rev# ++(x, y) -> rev# x 1 + 1x + 1y >= 0 + 1x Weak: rev rev x -> x 0 + 0x >= 1x rev ++(x, y) -> ++(rev y, rev x) 0 + 0x + 0y >= 1 + 0x + 0y rev unit x -> unit x 0 + 0x >= 1 + 0x rev nil() -> nil() 0 >= 1 ++(++(x, y), z) -> ++(x, ++(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z ++(nil(), y) -> y 2 + 1y >= 1y ++(x, nil()) -> x 2 + 1x >= 1x flatten ++(unit x, y) -> ++(flatten x, flatten y) 3 + 0x + 1y >= 3 + 1x + 1y flatten ++(x, y) -> ++(flatten x, flatten y) 2 + 1x + 1y >= 3 + 1x + 1y flatten unit x -> flatten x 2 + 0x >= 1 + 1x flatten flatten x -> flatten x 2 + 1x >= 1 + 1x flatten nil() -> nil() 2 >= 1 Qed SCC (5): Strict: { flatten# unit x -> flatten# x, flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# y} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [++](x0, x1) = x0 + x1 + 1, [flatten](x0) = x0 + 1, [unit](x0) = x0 + 1, [rev](x0) = 0, [nil] = 1, [flatten#](x0) = x0 Strict: flatten# ++(unit x, y) -> flatten# y 2 + 1x + 1y >= 0 + 1y flatten# ++(unit x, y) -> flatten# x 2 + 1x + 1y >= 0 + 1x flatten# ++(x, y) -> flatten# y 1 + 1x + 1y >= 0 + 1y flatten# ++(x, y) -> flatten# x 1 + 1x + 1y >= 0 + 1x flatten# unit x -> flatten# x 1 + 1x >= 0 + 1x Weak: rev rev x -> x 0 + 0x >= 1x rev ++(x, y) -> ++(rev y, rev x) 0 + 0x + 0y >= 1 + 0x + 0y rev unit x -> unit x 0 + 0x >= 1 + 1x rev nil() -> nil() 0 >= 1 ++(++(x, y), z) -> ++(x, ++(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z ++(nil(), y) -> y 2 + 1y >= 1y ++(x, nil()) -> x 2 + 1x >= 1x flatten ++(unit x, y) -> ++(flatten x, flatten y) 3 + 1x + 1y >= 3 + 1x + 1y flatten ++(x, y) -> ++(flatten x, flatten y) 2 + 1x + 1y >= 3 + 1x + 1y flatten unit x -> flatten x 2 + 1x >= 1 + 1x flatten flatten x -> flatten x 2 + 1x >= 1 + 1x flatten nil() -> nil() 2 >= 1 Qed SCC (2): Strict: {++#(++(x, y), z) -> ++#(x, ++(y, z)), ++#(++(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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [++](x0, x1) = x0 + x1 + 1, [flatten](x0) = x0 + 1, [unit](x0) = 0, [rev](x0) = 0, [nil] = 1, [++#](x0, x1) = x0 Strict: ++#(++(x, y), z) -> ++#(y, z) 1 + 1x + 1y + 0z >= 0 + 1y + 0z ++#(++(x, y), z) -> ++#(x, ++(y, z)) 1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z Weak: rev rev x -> x 0 + 0x >= 1x rev ++(x, y) -> ++(rev y, rev x) 0 + 0x + 0y >= 1 + 0x + 0y rev unit x -> unit x 0 + 0x >= 0 + 0x rev nil() -> nil() 0 >= 1 ++(++(x, y), z) -> ++(x, ++(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z ++(nil(), y) -> y 2 + 1y >= 1y ++(x, nil()) -> x 2 + 1x >= 1x flatten ++(unit x, y) -> ++(flatten x, flatten y) 2 + 0x + 1y >= 3 + 1x + 1y flatten ++(x, y) -> ++(flatten x, flatten y) 2 + 1x + 1y >= 3 + 1x + 1y flatten unit x -> flatten x 1 + 0x >= 1 + 1x flatten flatten x -> flatten x 2 + 1x >= 1 + 1x flatten nil() -> nil() 2 >= 1 Qed