YES 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: 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} 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, i(x))) -> 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), 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)) (:#(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)) (:#(:(x, y), z) -> :#(x, :(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)) (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(x, :(y, i(x))) -> i#(y)) (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(e(), x) -> i#(x)) (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(:(x, y), z) -> :#(x, :(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) -> i#(y)) (:#(:(x, y), z) -> :#(x, :(z, i(y))), :#(i(x), :(y, x)) -> i#(y)) (:#(:(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, z))) -> i#(z)) (:#(x, :(y, :(i(x), z))) -> i#(z), i#(:(x, y)) -> :#(y, x)) (:#(:(x, y), z) -> i#(y), i#(:(x, y)) -> :#(y, x)) (:#(e(), x) -> i#(x), i#(:(x, y)) -> :#(y, x)) (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))} SCCS: 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: 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: Argument Filtering: pi(i#) = [0], pi(i) = 0, pi(:#) = [0,1], pi(:) = [0,1], pi(e) = [] Usable Rules: {} Interpretation: [:#](x0, x1) = x0 + x1 + 1, [i#](x0) = x0 + 1, [:](x0, x1) = x0 + x1 + 1, [e] = 0 Strict: { :#(e(), x) -> i#(x), :#(:(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} 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: Scc: {:#(:(x, y), z) -> :#(x, :(z, i(y)))} SCC: 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