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)} UR: { 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() -> 10* a_0(10, 10) -> 7* a_0(10, 9) -> 7* a_0(10, 8) -> 7* a_0(10, 7) -> 7* a_0(9, 10) -> 7* a_0(9, 9) -> 7* a_0(9, 8) -> 7* a_0(9, 7) -> 7* a_0(8, 10) -> 7* a_0(8, 9) -> 7* a_0(8, 8) -> 7* a_0(8, 7) -> 7* a_0(7, 10) -> 7* a_0(7, 9) -> 7* a_0(7, 8) -> 7* a_0(7, 7) -> 7* c#_0(9) -> 5* c_0(10) -> 9* c_0(9) -> 8* c_0(8) -> 8* c_0(7) -> 8* 10 -> 9* 9 -> 8* 7 -> 8*} 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)} UR: { 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 2 Automaton: { 0_2() -> 14* 0_1() -> 11* 0_0() -> 9* a_2(11, 14) -> 15* a_1(11, 11) -> 13* a_1(10, 11) -> 12* a_1(9, 11) -> 12* a_1(8, 11) -> 12* a_1(7, 11) -> 12* a_0(10, 10) -> 7* a_0(10, 9) -> 10* a_0(10, 8) -> 7* a_0(10, 7) -> 7* a_0(9, 10) -> 7* a_0(9, 9) -> 10* a_0(9, 8) -> 7* a_0(9, 7) -> 7* a_0(8, 10) -> 7* a_0(8, 9) -> 10* a_0(8, 8) -> 7* a_0(8, 7) -> 7* a_0(7, 10) -> 7* a_0(7, 9) -> 10* a_0(7, 8) -> 7* a_0(7, 7) -> 7* c#_2(15) -> 5* c#_1(12) -> 5* c#_0(10) -> 5* c#_0(8) -> 5* c_1(13) -> 12* c_1(11) -> 13* c_0(10) -> 8* c_0(9) -> 8* c_0(8) -> 8* c_0(7) -> 8* 13 -> 12* 11 -> 13* 10 -> 8* 9 -> 8* 7 -> 8*} 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)} UR: { 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: { 0_1() -> 13* 0_0() -> 11* a_1(13, 13) -> 14* a_0(12, 12) -> 8* a_0(12, 11) -> 8* a_0(12, 10) -> 8* a_0(12, 9) -> 8* a_0(12, 8) -> 8* a_0(11, 12) -> 8* a_0(11, 11) -> 8* a_0(11, 10) -> 8* a_0(11, 9) -> 8* a_0(11, 8) -> 8* a_0(10, 12) -> 8* a_0(10, 11) -> 8* a_0(10, 10) -> 8* a_0(10, 9) -> 8* a_0(10, 8) -> 8* a_0(9, 12) -> 8* a_0(9, 11) -> 8* a_0(9, 10) -> 8* a_0(9, 9) -> 8* a_0(9, 8) -> 8* a_0(8, 12) -> 8* a_0(8, 11) -> 8* a_0(8, 10) -> 8* a_0(8, 9) -> 8* a_0(8, 8) -> 8* c#_1(15) -> 5* c#_0(12) -> 5* c#_0(9) -> 5* c_1(14) -> 15* c_1(13) -> 14* c_0(12) -> 9* c_0(11) -> 10* c_0(10) -> 12* c_0(9) -> 9* c_0(8) -> 9* 14 -> 15* 13 -> 14* 12 -> 9* 11 -> 10* 10 -> 12* 8 -> 9*} 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