YES TRS: {b(b(0(), y), x) -> y, c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))), a(y, 0()) -> b(y, 0())} DP: Strict: {c#(c(c(y))) -> b#(0(), y), c#(c(c(y))) -> c#(b(0(), y)), c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> a#(c(b(0(), y)), 0()), c#(c(c(y))) -> a#(a(c(b(0(), y)), 0()), 0()), a#(y, 0()) -> b#(y, 0())} Weak: {b(b(0(), y), x) -> y, c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))), a(y, 0()) -> b(y, 0())} EDG: {(c#(c(c(y))) -> a#(a(c(b(0(), y)), 0()), 0()), a#(y, 0()) -> b#(y, 0())) (c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> a#(a(c(b(0(), y)), 0()), 0())) (c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> a#(c(b(0(), y)), 0())) (c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0()))) (c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0())))) (c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> c#(b(0(), y))) (c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0())), c#(c(c(y))) -> b#(0(), y)) (c#(c(c(y))) -> a#(c(b(0(), y)), 0()), a#(y, 0()) -> b#(y, 0())) (c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> b#(0(), y)) (c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(b(0(), y))) (c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0())))) (c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0()))) (c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> a#(c(b(0(), y)), 0())) (c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> a#(a(c(b(0(), y)), 0()), 0()))} SCCS: Scc: {c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0()))} SCC: Strict: {c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(a(a(c(b(0(), y)), 0()), 0()))} Weak: {b(b(0(), y), x) -> y, c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))), a(y, 0()) -> b(y, 0())} POLY: Argument Filtering: pi(a) = 0, pi(c#) = 0, pi(c) = [0], pi(0) = [], pi(b) = [0,1] Usable Rules: {} Interpretation: [b](x0, x1) = x0 + x1, [c](x0) = x0 + 1, [0] = 0 Strict: {c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0())))} Weak: {b(b(0(), y), x) -> y, c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))), a(y, 0()) -> b(y, 0())} EDG: {(c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))), c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0()))))} SCCS: Scc: {c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0())))} SCC: Strict: {c#(c(c(y))) -> c#(c(a(a(c(b(0(), y)), 0()), 0())))} Weak: {b(b(0(), y), x) -> y, c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))), a(y, 0()) -> b(y, 0())} UR: {b(b(0(), y), x) -> y, c(c(c(y))) -> c(c(a(a(c(b(0(), y)), 0()), 0()))), a(y, 0()) -> b(y, 0())} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: {a_0(20, 20) -> 13* a_0(20, 19) -> 13* a_0(20, 18) -> 13* a_0(20, 17) -> 13* a_0(20, 16) -> 13* a_0(20, 15) -> 13* a_0(20, 14) -> 13* a_0(20, 13) -> 13* a_0(20, 12) -> 13* a_0(19, 20) -> 13* a_0(19, 19) -> 13* a_0(19, 18) -> 13* a_0(19, 17) -> 13* a_0(19, 16) -> 13* a_0(19, 15) -> 13* a_0(19, 14) -> 13* a_0(19, 13) -> 13* a_0(19, 12) -> 13* a_0(18, 20) -> 13* a_0(18, 19) -> 13* a_0(18, 18) -> 13* a_0(18, 17) -> 13* a_0(18, 16) -> 13* a_0(18, 15) -> 19* a_0(18, 14) -> 13* a_0(18, 13) -> 13* a_0(18, 12) -> 13* a_0(17, 20) -> 13* a_0(17, 19) -> 13* a_0(17, 18) -> 13* a_0(17, 17) -> 13* a_0(17, 16) -> 13* a_0(17, 15) -> 18* a_0(17, 14) -> 13* a_0(17, 13) -> 13* a_0(17, 12) -> 13* a_0(16, 20) -> 13* a_0(16, 19) -> 13* a_0(16, 18) -> 13* a_0(16, 17) -> 13* a_0(16, 16) -> 13* a_0(16, 15) -> 13* a_0(16, 14) -> 13* a_0(16, 13) -> 13* a_0(16, 12) -> 13* a_0(15, 20) -> 13* a_0(15, 19) -> 13* a_0(15, 18) -> 13* a_0(15, 17) -> 13* a_0(15, 16) -> 13* a_0(15, 15) -> 13* a_0(15, 14) -> 13* a_0(15, 13) -> 13* a_0(15, 12) -> 13* a_0(14, 20) -> 13* a_0(14, 19) -> 13* a_0(14, 18) -> 13* a_0(14, 17) -> 13* a_0(14, 16) -> 13* a_0(14, 15) -> 13* a_0(14, 14) -> 13* a_0(14, 13) -> 13* a_0(14, 12) -> 13* a_0(13, 20) -> 13* a_0(13, 19) -> 13* a_0(13, 18) -> 13* a_0(13, 17) -> 13* a_0(13, 16) -> 13* a_0(13, 15) -> 13* a_0(13, 14) -> 13* a_0(13, 13) -> 13* a_0(13, 12) -> 13* a_0(12, 20) -> 13* a_0(12, 19) -> 13* a_0(12, 18) -> 13* a_0(12, 17) -> 13* a_0(12, 16) -> 13* a_0(12, 15) -> 13* a_0(12, 14) -> 13* a_0(12, 13) -> 13* a_0(12, 12) -> 13* c#_0(20) -> 6* c_0(20) -> 14* c_0(19) -> 20* c_0(18) -> 14* c_0(17) -> 14* c_0(16) -> 17* c_0(15) -> 14* c_0(14) -> 14* c_0(13) -> 14* c_0(12) -> 14* 0_0() -> 15* b_0(20, 20) -> 12* b_0(20, 19) -> 12* b_0(20, 18) -> 12* b_0(20, 17) -> 12* b_0(20, 16) -> 12* b_0(20, 15) -> 12* b_0(20, 14) -> 12* b_0(20, 13) -> 12* b_0(20, 12) -> 12* b_0(19, 20) -> 12* b_0(19, 19) -> 12* b_0(19, 18) -> 12* b_0(19, 17) -> 12* b_0(19, 16) -> 12* b_0(19, 15) -> 12* b_0(19, 14) -> 12* b_0(19, 13) -> 12* b_0(19, 12) -> 12* b_0(18, 20) -> 12* b_0(18, 19) -> 12* b_0(18, 18) -> 12* b_0(18, 17) -> 12* b_0(18, 16) -> 12* b_0(18, 15) -> 19 | 12 b_0(18, 14) -> 12* b_0(18, 13) -> 12* b_0(18, 12) -> 12* b_0(17, 20) -> 12* b_0(17, 19) -> 12* b_0(17, 18) -> 12* b_0(17, 17) -> 12* b_0(17, 16) -> 12* b_0(17, 15) -> 18 | 12 b_0(17, 14) -> 12* b_0(17, 13) -> 12* b_0(17, 12) -> 12* b_0(16, 20) -> 12* b_0(16, 19) -> 12* b_0(16, 18) -> 12* b_0(16, 17) -> 12* b_0(16, 16) -> 12* b_0(16, 15) -> 12* b_0(16, 14) -> 12* b_0(16, 13) -> 12* b_0(16, 12) -> 12* b_0(15, 20) -> 16* b_0(15, 19) -> 16* b_0(15, 18) -> 16* b_0(15, 17) -> 16* b_0(15, 16) -> 16* b_0(15, 15) -> 16* b_0(15, 14) -> 16* b_0(15, 13) -> 16* b_0(15, 12) -> 16* b_0(14, 20) -> 12* b_0(14, 19) -> 12* b_0(14, 18) -> 12* b_0(14, 17) -> 12* b_0(14, 16) -> 12* b_0(14, 15) -> 12* b_0(14, 14) -> 12* b_0(14, 13) -> 12* b_0(14, 12) -> 12* b_0(13, 20) -> 12* b_0(13, 19) -> 12* b_0(13, 18) -> 12* b_0(13, 17) -> 12* b_0(13, 16) -> 12* b_0(13, 15) -> 12* b_0(13, 14) -> 12* b_0(13, 13) -> 12* b_0(13, 12) -> 12* b_0(12, 20) -> 12* b_0(12, 19) -> 12* b_0(12, 18) -> 12* b_0(12, 17) -> 12* b_0(12, 16) -> 12* b_0(12, 15) -> 13 | 12 b_0(12, 14) -> 12* b_0(12, 13) -> 12* b_0(12, 12) -> 12* 20 -> 12* 19 -> 12* 18 -> 12* 17 -> 12* 16 -> 12* 15 -> 12* 14 -> 12* 13 -> 12* 12 -> 13*} Strict: {} Qed