YES TRS: {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))), a(f(), 0()) -> a(s(), 0()), a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))), a(d(), 0()) -> 0(), a(p(), a(s(), x)) -> x} DP: Strict: {a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(f(), a(s(), x)) -> a#(p(), a(s(), x)), a#(f(), 0()) -> a#(s(), 0()), a#(d(), a(s(), x)) -> a#(s(), a(s(), a(d(), a(p(), a(s(), x))))), a#(d(), a(s(), x)) -> a#(s(), a(d(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(p(), a(s(), x))} Weak: {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))), a(f(), 0()) -> a(s(), 0()), a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))), a(d(), 0()) -> 0(), a(p(), a(s(), x)) -> x} EDG: {(a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(p(), a(s(), x))) (a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x)))) (a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(s(), a(d(), a(p(), a(s(), x))))) (a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(s(), a(s(), a(d(), a(p(), a(s(), x)))))) (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(s(), a(s(), a(d(), a(p(), a(s(), x)))))) (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(s(), a(d(), a(p(), a(s(), x))))) (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x)))) (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(p(), a(s(), x))) (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x)))) (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x))))) (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(p(), a(s(), x))) (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), 0()) -> a#(s(), 0()))} SCCS: Scc: {a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x)))} Scc: {a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x)))} SCC: Strict: {a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x)))} Weak: {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))), a(f(), 0()) -> a(s(), 0()), a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))), a(d(), 0()) -> 0(), a(p(), a(s(), x)) -> x} UR: {a(p(), a(s(), x)) -> x} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { p_1() -> 16* p_0() -> 12* d_1() -> 15* d_0() -> 11* s_1() -> 17* s_0() -> 10* a#_1(15, 19) -> 6* a#_0(11, 14) -> 6* a_1(17, 14) -> 18* a_1(17, 13) -> 18* a_1(17, 12) -> 18* a_1(17, 11) -> 18* a_1(17, 10) -> 18* a_1(17, 9) -> 18* a_1(16, 18) -> 19* a_0(14, 14) -> 9* a_0(14, 13) -> 9* a_0(14, 12) -> 9* a_0(14, 11) -> 9* a_0(14, 10) -> 9* a_0(14, 9) -> 9* a_0(13, 14) -> 9* a_0(13, 13) -> 9* a_0(13, 12) -> 9* a_0(13, 11) -> 9* a_0(13, 10) -> 9* a_0(13, 9) -> 9* a_0(12, 14) -> 9* a_0(12, 13) -> 14* a_0(12, 12) -> 9* a_0(12, 11) -> 9* a_0(12, 10) -> 9* a_0(12, 9) -> 9* a_0(11, 14) -> 9* a_0(11, 13) -> 9* a_0(11, 12) -> 9* a_0(11, 11) -> 9* a_0(11, 10) -> 9* a_0(11, 9) -> 9* a_0(10, 14) -> 13* a_0(10, 13) -> 13* a_0(10, 12) -> 13* a_0(10, 11) -> 13* a_0(10, 10) -> 13* a_0(10, 9) -> 13* a_0(9, 14) -> 9* a_0(9, 13) -> 9* a_0(9, 12) -> 9* a_0(9, 11) -> 9* a_0(9, 10) -> 9* a_0(9, 9) -> 9* 14 -> 9* 13 -> 14 | 9 12 -> 14 | 9 11 -> 14 | 9 10 -> 14 | 9 9 -> 19 | 14} Strict: {} Qed SCC: Strict: {a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x)))} Weak: {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))), a(f(), 0()) -> a(s(), 0()), a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))), a(d(), 0()) -> 0(), a(p(), a(s(), x)) -> x} UR: {a(p(), a(s(), x)) -> x} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { p_1() -> 16* p_0() -> 12* f_1() -> 15* f_0() -> 11* s_1() -> 17* s_0() -> 10* a#_1(15, 19) -> 6* a#_0(11, 14) -> 6* a_1(17, 14) -> 18* a_1(17, 13) -> 18* a_1(17, 12) -> 18* a_1(17, 11) -> 18* a_1(17, 10) -> 18* a_1(17, 9) -> 18* a_1(16, 18) -> 19* a_0(14, 14) -> 9* a_0(14, 13) -> 9* a_0(14, 12) -> 9* a_0(14, 11) -> 9* a_0(14, 10) -> 9* a_0(14, 9) -> 9* a_0(13, 14) -> 9* a_0(13, 13) -> 9* a_0(13, 12) -> 9* a_0(13, 11) -> 9* a_0(13, 10) -> 9* a_0(13, 9) -> 9* a_0(12, 14) -> 9* a_0(12, 13) -> 14* a_0(12, 12) -> 9* a_0(12, 11) -> 9* a_0(12, 10) -> 9* a_0(12, 9) -> 9* a_0(11, 14) -> 9* a_0(11, 13) -> 9* a_0(11, 12) -> 9* a_0(11, 11) -> 9* a_0(11, 10) -> 9* a_0(11, 9) -> 9* a_0(10, 14) -> 13* a_0(10, 13) -> 13* a_0(10, 12) -> 13* a_0(10, 11) -> 13* a_0(10, 10) -> 13* a_0(10, 9) -> 13* a_0(9, 14) -> 9* a_0(9, 13) -> 9* a_0(9, 12) -> 9* a_0(9, 11) -> 9* a_0(9, 10) -> 9* a_0(9, 9) -> 9* 14 -> 9* 13 -> 14 | 9 12 -> 14 | 9 11 -> 14 | 9 10 -> 14 | 9 9 -> 19 | 14} Strict: {} Qed