YES Time: 0.013850 TRS: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} DP: DP: {:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z, :#(x, :(y, i x)) -> i# y, :#(e(), x) -> i# x, :#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y, :#(i x, :(y, x)) -> i# y, :#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)} TRS: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} EDG: {(:#(:(x, y), z) -> :#(z, i y), :#(i x, :(y, :(x, z))) -> i# z) (:#(:(x, y), z) -> :#(z, i y), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> :#(z, i y), :#(i x, :(y, x)) -> i# y) (:#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y) (:#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> :#(z, i y)) (:#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(:(x, y), z) -> :#(z, i y), :#(e(), x) -> i# x) (:#(:(x, y), z) -> :#(z, i y), :#(x, :(y, i x)) -> i# y) (:#(:(x, y), z) -> :#(z, i y), :#(x, :(y, :(i x, z))) -> i# z) (:#(:(x, y), z) -> :#(z, i y), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> i# y, i# :(x, y) -> :#(y, x)) (:#(x, :(y, :(i x, z))) -> i# z, i# :(x, y) -> :#(y, x)) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(i x, :(y, x)) -> i# y) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(:(x, y), z) -> i# y) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(z, i y)) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(e(), x) -> i# x) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, i x)) -> i# y) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z) (:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(i x, :(y, :(x, z))) -> i# z) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(i x, :(y, x)) -> i# y) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> i# y) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y)) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(e(), x) -> i# x) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(x, :(y, i x)) -> i# y) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(x, :(y, :(i x, z))) -> i# z) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (i# :(x, y) -> :#(y, x), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (i# :(x, y) -> :#(y, x), :#(x, :(y, :(i x, z))) -> i# z) (i# :(x, y) -> :#(y, x), :#(x, :(y, i x)) -> i# y) (i# :(x, y) -> :#(y, x), :#(e(), x) -> i# x) (i# :(x, y) -> :#(y, x), :#(:(x, y), z) -> :#(x, :(z, i y))) (i# :(x, y) -> :#(y, x), :#(:(x, y), z) -> :#(z, i y)) (i# :(x, y) -> :#(y, x), :#(:(x, y), z) -> i# y) (i# :(x, y) -> :#(y, x), :#(i x, :(y, x)) -> i# y) (i# :(x, y) -> :#(y, x), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (i# :(x, y) -> :#(y, x), :#(i x, :(y, :(x, z))) -> i# z) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> :#(i z, y)) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(x, :(y, i x)) -> i# y) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(e(), x) -> i# x) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(:(x, y), z) -> :#(z, i y)) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(:(x, y), z) -> i# y) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, x)) -> i# y) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> :#(i z, y)) (:#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z) (:#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)) (:#(i x, :(y, x)) -> i# y, i# :(x, y) -> :#(y, x)) (:#(x, :(y, i x)) -> i# y, i# :(x, y) -> :#(y, x)) (:#(e(), x) -> i# x, i# :(x, y) -> :#(y, x))} SCCS (1): Scc: {:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z, :#(x, :(y, i x)) -> i# y, :#(e(), x) -> i# x, :#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y, :#(i x, :(y, x)) -> i# y, :#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)} SCC (11): Strict: {:#(x, :(y, :(i x, z))) -> :#(i z, y), :#(x, :(y, :(i x, z))) -> i# z, :#(x, :(y, i x)) -> i# y, :#(e(), x) -> i# x, :#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(z, i y), :#(:(x, y), z) -> i# y, :#(i x, :(y, x)) -> i# y, :#(i x, :(y, :(x, z))) -> :#(i z, y), :#(i x, :(y, :(x, z))) -> i# z, i# :(x, y) -> :#(y, x)} Weak: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [:](x0, x1) = x0 + x1 + 1, [i](x0) = x0, [e] = 0, [:#](x0, x1) = x0 + x1 + 1, [i#](x0) = x0 + 1 Strict: i# :(x, y) -> :#(y, x) 2 + 1x + 1y >= 1 + 1x + 1y :#(i x, :(y, :(x, z))) -> i# z 3 + 2x + 1y + 1z >= 1 + 1z :#(i x, :(y, :(x, z))) -> :#(i z, y) 3 + 2x + 1y + 1z >= 1 + 1y + 1z :#(i x, :(y, x)) -> i# y 2 + 2x + 1y >= 1 + 1y :#(:(x, y), z) -> i# y 2 + 1x + 1y + 1z >= 1 + 1y :#(:(x, y), z) -> :#(z, i y) 2 + 1x + 1y + 1z >= 1 + 1y + 1z :#(:(x, y), z) -> :#(x, :(z, i y)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z :#(e(), x) -> i# x 1 + 1x >= 1 + 1x :#(x, :(y, i x)) -> i# y 2 + 2x + 1y >= 1 + 1y :#(x, :(y, :(i x, z))) -> i# z 3 + 2x + 1y + 1z >= 1 + 1z :#(x, :(y, :(i x, z))) -> :#(i z, y) 3 + 2x + 1y + 1z >= 1 + 1y + 1z Weak: EDG: {(:#(:(x, y), z) -> :#(x, :(z, i y)), :#(:(x, y), z) -> :#(x, :(z, i y))) (:#(:(x, y), z) -> :#(x, :(z, i y)), :#(e(), x) -> i# x)} SCCS (1): Scc: {:#(:(x, y), z) -> :#(x, :(z, i y))} SCC (1): Strict: {:#(:(x, y), z) -> :#(x, :(z, i y))} Weak: { :(x, x) -> e(), :(x, e()) -> x, :(x, :(y, :(i x, z))) -> :(i z, y), :(x, :(y, i x)) -> i y, :(e(), x) -> i x, :(:(x, y), z) -> :(x, :(z, i y)), :(i x, :(y, x)) -> i y, :(i x, :(y, :(x, z))) -> :(i z, y), i e() -> e(), i :(x, y) -> :(y, x), i i x -> x} SPSC: Simple Projection: pi(:#) = 0 Strict: {} Qed