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} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { p_1() -> 20* p_0() -> 16* d_1() -> 19* d_0() -> 15* f_0() -> 14* 0_0() -> 13 | 11 s_1() -> 21* s_0() -> 12* a#_1(19, 23) -> 8* a#_0(15, 18) -> 8* a_1(21, 18) -> 22* a_1(21, 17) -> 22* a_1(21, 16) -> 22* a_1(21, 15) -> 22* a_1(21, 14) -> 22* a_1(21, 13) -> 22* a_1(21, 12) -> 22* a_1(21, 11) -> 22* a_1(20, 22) -> 23* a_0(18, 18) -> 11* a_0(18, 17) -> 11* a_0(18, 16) -> 11* a_0(18, 15) -> 11* a_0(18, 14) -> 11* a_0(18, 13) -> 11* a_0(18, 12) -> 11* a_0(18, 11) -> 11* a_0(17, 18) -> 11* a_0(17, 17) -> 11* a_0(17, 16) -> 11* a_0(17, 15) -> 11* a_0(17, 14) -> 11* a_0(17, 13) -> 11* a_0(17, 12) -> 11* a_0(17, 11) -> 11* a_0(16, 18) -> 11* a_0(16, 17) -> 18* a_0(16, 16) -> 11* a_0(16, 15) -> 11* a_0(16, 14) -> 11* a_0(16, 13) -> 11* a_0(16, 12) -> 11* a_0(16, 11) -> 11* a_0(15, 18) -> 11* a_0(15, 17) -> 11* a_0(15, 16) -> 11* a_0(15, 15) -> 11* a_0(15, 14) -> 11* a_0(15, 13) -> 11* a_0(15, 12) -> 11* a_0(15, 11) -> 11* a_0(14, 18) -> 11* a_0(14, 17) -> 11* a_0(14, 16) -> 11* a_0(14, 15) -> 11* a_0(14, 14) -> 11* a_0(14, 13) -> 11* a_0(14, 12) -> 11* a_0(14, 11) -> 11* a_0(13, 18) -> 11* a_0(13, 17) -> 11* a_0(13, 16) -> 11* a_0(13, 15) -> 11* a_0(13, 14) -> 11* a_0(13, 13) -> 11* a_0(13, 12) -> 11* a_0(13, 11) -> 11* a_0(12, 18) -> 17* a_0(12, 17) -> 17* a_0(12, 16) -> 17* a_0(12, 15) -> 17* a_0(12, 14) -> 17* a_0(12, 13) -> 17* a_0(12, 12) -> 17* a_0(12, 11) -> 17* a_0(11, 18) -> 11* a_0(11, 17) -> 11* a_0(11, 16) -> 11* a_0(11, 15) -> 11* a_0(11, 14) -> 11* a_0(11, 13) -> 11* a_0(11, 12) -> 11* a_0(11, 11) -> 11* 18 -> 11* 17 -> 18 | 11 16 -> 18 | 11 15 -> 18 | 11 14 -> 18 | 11 13 -> 18 | 11 12 -> 18 | 11 11 -> 23 | 18} 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} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { p_1() -> 20* p_0() -> 16* d_0() -> 15* f_1() -> 19* f_0() -> 14* 0_0() -> 13 | 11 s_1() -> 21* s_0() -> 12* a#_1(19, 23) -> 8* a#_0(14, 18) -> 8* a_1(21, 18) -> 22* a_1(21, 17) -> 22* a_1(21, 16) -> 22* a_1(21, 15) -> 22* a_1(21, 14) -> 22* a_1(21, 13) -> 22* a_1(21, 12) -> 22* a_1(21, 11) -> 22* a_1(20, 22) -> 23* a_0(18, 18) -> 11* a_0(18, 17) -> 11* a_0(18, 16) -> 11* a_0(18, 15) -> 11* a_0(18, 14) -> 11* a_0(18, 13) -> 11* a_0(18, 12) -> 11* a_0(18, 11) -> 11* a_0(17, 18) -> 11* a_0(17, 17) -> 11* a_0(17, 16) -> 11* a_0(17, 15) -> 11* a_0(17, 14) -> 11* a_0(17, 13) -> 11* a_0(17, 12) -> 11* a_0(17, 11) -> 11* a_0(16, 18) -> 11* a_0(16, 17) -> 18* a_0(16, 16) -> 11* a_0(16, 15) -> 11* a_0(16, 14) -> 11* a_0(16, 13) -> 11* a_0(16, 12) -> 11* a_0(16, 11) -> 11* a_0(15, 18) -> 11* a_0(15, 17) -> 11* a_0(15, 16) -> 11* a_0(15, 15) -> 11* a_0(15, 14) -> 11* a_0(15, 13) -> 11* a_0(15, 12) -> 11* a_0(15, 11) -> 11* a_0(14, 18) -> 11* a_0(14, 17) -> 11* a_0(14, 16) -> 11* a_0(14, 15) -> 11* a_0(14, 14) -> 11* a_0(14, 13) -> 11* a_0(14, 12) -> 11* a_0(14, 11) -> 11* a_0(13, 18) -> 11* a_0(13, 17) -> 11* a_0(13, 16) -> 11* a_0(13, 15) -> 11* a_0(13, 14) -> 11* a_0(13, 13) -> 11* a_0(13, 12) -> 11* a_0(13, 11) -> 11* a_0(12, 18) -> 17* a_0(12, 17) -> 17* a_0(12, 16) -> 17* a_0(12, 15) -> 17* a_0(12, 14) -> 17* a_0(12, 13) -> 17* a_0(12, 12) -> 17* a_0(12, 11) -> 17* a_0(11, 18) -> 11* a_0(11, 17) -> 11* a_0(11, 16) -> 11* a_0(11, 15) -> 11* a_0(11, 14) -> 11* a_0(11, 13) -> 11* a_0(11, 12) -> 11* a_0(11, 11) -> 11* 18 -> 11* 17 -> 18 | 11 16 -> 18 | 11 15 -> 18 | 11 14 -> 18 | 11 13 -> 18 | 11 12 -> 18 | 11 11 -> 23 | 18} Strict: {} Qed