YES TRS: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} DP: Strict: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(0())), c#(a(a(0(), x), y)) -> c#(0())} Weak: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} EDG: {(c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(0())) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(0()))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(c(c(y))) -> c#(a(y, 0()))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0()))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(0()))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(0())) (c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(0()))) (c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(0())) (c#(a(a(0(), x), y)) -> c#(c(0())), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(a(a(0(), x), y)) -> c#(c(0())), c#(c(c(y))) -> c#(a(y, 0()))) (c#(a(a(0(), x), y)) -> c#(c(0())), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(a(a(0(), x), y)) -> c#(c(0())), c#(a(a(0(), x), y)) -> c#(c(0()))) (c#(a(a(0(), x), y)) -> c#(c(0())), c#(a(a(0(), x), y)) -> c#(0()))} SCCS: Scc: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(0()))} SCC: Strict: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(0()))} Weak: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { 0_0() -> 2* c#_0(3) -> 1* c_0(2) -> 3* 2 -> 3*} Strict: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0())))} EDG: {(c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(c(c(y))) -> c#(a(y, 0()))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0()))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(c(0()))))} SCCS: Scc: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0())))} SCC: Strict: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(a(y, 0())), c#(a(a(0(), x), y)) -> c#(c(c(0())))} Weak: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { b_0() -> 2* 0_1() -> 6* 0_0() -> 3* a_1(3, 6) -> 7* a_0(3, 3) -> 5* a_0(2, 3) -> 4* c#_1(7) -> 1* c#_0(4) -> 1* c_0(5) -> 4* c_0(3) -> 5* 5 -> 4* 3 -> 5*} Strict: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))} EDG: {(c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))) (c#(a(a(0(), x), y)) -> c#(c(c(0()))), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(c(a(y, 0())))) (c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(c(0()))))} SCCS: Scc: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))} SCC: Strict: { c#(c(c(y))) -> c#(c(a(y, 0()))), c#(a(a(0(), x), y)) -> c#(c(c(0())))} Weak: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { 0_0() -> 2* a_0(2, 2) -> 3* c#_0(4) -> 1* c_0(3) -> 4* c_0(2) -> 3* 3 -> 4* 2 -> 3*} Strict: {c#(c(c(y))) -> c#(c(a(y, 0())))} EDG: {(c#(c(c(y))) -> c#(c(a(y, 0()))), c#(c(c(y))) -> c#(c(a(y, 0()))))} SCCS: Scc: {c#(c(c(y))) -> c#(c(a(y, 0())))} SCC: Strict: {c#(c(c(y))) -> c#(c(a(y, 0())))} Weak: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} POLY: Argument Filtering: pi(0) = [], pi(a) = [], pi(c#) = [0], pi(c) = [0] Usable Rules: {} Interpretation: [c#](x0) = x0 + 1, [a] = 0, [c](x0) = x0 + 1 Strict: {} Weak: { c(y) -> y, c(c(c(y))) -> c(c(a(y, 0()))), c(a(a(0(), x), y)) -> a(c(c(c(0()))), y)} Qed