YES Time: 0.019062 TRS: { rev nil() -> nil(), rev rev x -> x, rev ++(x, y) -> ++(rev y, rev x), ++(x, nil()) -> x, ++(x, ++(y, z)) -> ++(++(x, y), z), ++(nil(), y) -> y, ++(.(x, y), z) -> .(x, ++(y, z)), make x -> .(x, nil())} DP: DP: { rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y, rev# ++(x, y) -> ++#(rev y, rev x), ++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)} TRS: { rev nil() -> nil(), rev rev x -> x, rev ++(x, y) -> ++(rev y, rev x), ++(x, nil()) -> x, ++(x, ++(y, z)) -> ++(++(x, y), z), ++(nil(), y) -> y, ++(.(x, y), z) -> .(x, ++(y, z)), make x -> .(x, nil())} UR: { rev nil() -> nil(), rev rev x -> x, rev ++(x, y) -> ++(rev y, rev x), ++(x, nil()) -> x, ++(x, ++(y, z)) -> ++(++(x, y), z), ++(nil(), y) -> y, ++(.(x, y), z) -> .(x, ++(y, z))} EDG: {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y)) (rev# ++(x, y) -> ++#(rev y, rev x), ++#(.(x, y), z) -> ++#(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)) -> ++#(x, y)) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> ++#(rev y, rev x)) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# x) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z)) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# x) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> ++#(rev y, rev x))} EDG: {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y)) (rev# ++(x, y) -> ++#(rev y, rev x), ++#(.(x, y), z) -> ++#(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)) -> ++#(x, y)) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> ++#(rev y, rev x)) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# y) (rev# ++(x, y) -> rev# x, rev# ++(x, y) -> rev# x) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z)) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# x) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y) (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> ++#(rev y, rev x))} EDG: {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y)) (rev# ++(x, y) -> ++#(rev y, rev x), ++#(.(x, y), z) -> ++#(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)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z))} EDG: {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y)) (rev# ++(x, y) -> ++#(rev y, rev x), ++#(.(x, y), z) -> ++#(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)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z)) (++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z))} STATUS: arrows: 0.722222 SCCS (1): Scc: {++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)} SCC (3): Strict: {++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z)} Weak: { rev nil() -> nil(), rev rev x -> x, rev ++(x, y) -> ++(rev y, rev x), ++(x, nil()) -> x, ++(x, ++(y, z)) -> ++(++(x, y), z), ++(nil(), y) -> y, ++(.(x, y), z) -> .(x, ++(y, z)), make x -> .(x, nil())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [++](x0, x1) = x0 + x1 + 1, [.](x0, x1) = 0, [rev](x0) = x0 + 1, [make](x0) = 0, [nil] = 1, [++#](x0, x1) = x0 Strict: ++#(.(x, y), z) -> ++#(y, z) 0 + 0x + 0y + 1z >= 0 + 0y + 1z ++#(x, ++(y, z)) -> ++#(++(x, y), z) 1 + 0x + 1y + 1z >= 0 + 0x + 0y + 1z ++#(x, ++(y, z)) -> ++#(x, y) 1 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: make x -> .(x, nil()) 0 + 0x >= 0 + 0x ++(.(x, y), z) -> .(x, ++(y, z)) 1 + 0x + 0y + 1z >= 0 + 0x + 0y + 0z ++(nil(), y) -> y 2 + 1y >= 1y ++(x, ++(y, z)) -> ++(++(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z ++(x, nil()) -> x 2 + 1x >= 1x rev ++(x, y) -> ++(rev y, rev x) 2 + 1x + 1y >= 3 + 1x + 1y rev rev x -> x 2 + 1x >= 1x rev nil() -> nil() 2 >= 1 SCCS (1): Scc: {++#(.(x, y), z) -> ++#(y, z)} SCC (1): Strict: {++#(.(x, y), z) -> ++#(y, z)} Weak: { rev nil() -> nil(), rev rev x -> x, rev ++(x, y) -> ++(rev y, rev x), ++(x, nil()) -> x, ++(x, ++(y, z)) -> ++(++(x, y), z), ++(nil(), y) -> y, ++(.(x, y), z) -> .(x, ++(y, z)), make x -> .(x, nil())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [++](x0, x1) = 1, [.](x0, x1) = x0 + 1, [rev](x0) = x0 + 1, [make](x0) = 0, [nil] = 1, [++#](x0, x1) = x0 Strict: ++#(.(x, y), z) -> ++#(y, z) 1 + 0x + 1y + 0z >= 0 + 1y + 0z Weak: make x -> .(x, nil()) 0 + 0x >= 2 + 0x ++(.(x, y), z) -> .(x, ++(y, z)) 1 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z ++(nil(), y) -> y 1 + 0y >= 1y ++(x, ++(y, z)) -> ++(++(x, y), z) 1 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z ++(x, nil()) -> x 1 + 0x >= 1x rev ++(x, y) -> ++(rev y, rev x) 2 + 0x + 0y >= 1 + 0x + 0y rev rev x -> x 2 + 1x >= 1x rev nil() -> nil() 2 >= 1 Qed