YES TRS: { h(x, c(y, z)) -> h(c(s(y), x), z), h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z)))} DP: Strict: { h#(x, c(y, z)) -> h#(c(s(y), x), z), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))} Weak: { h(x, c(y, z)) -> h(c(s(y), x), z), h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z)))} EDG: {(h#(x, c(y, z)) -> h#(c(s(y), x), z), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))) (h#(x, c(y, z)) -> h#(c(s(y), x), z), h#(x, c(y, z)) -> h#(c(s(y), x), z)) (h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z))), h#(x, c(y, z)) -> h#(c(s(y), x), z)) (h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z))), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z))))} SCCS: Scc: { h#(x, c(y, z)) -> h#(c(s(y), x), z), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))} SCC: Strict: { h#(x, c(y, z)) -> h#(c(s(y), x), z), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))} Weak: { h(x, c(y, z)) -> h(c(s(y), x), z), h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z)))} BOUND: Bound: match(-raise)-DP-bounded by 2 Automaton: { 0_1() -> 17* 0_0() -> 12* s_2(18) -> 21* s_2(14) -> 23* s_2(13) -> 23* s_2(12) -> 23* s_2(10) -> 23* s_2(9) -> 23* s_1(17) -> 18* s_1(14) -> 15* s_1(13) -> 15* s_1(12) -> 15* s_1(10) -> 15* s_1(9) -> 15* s_0(14) -> 13* s_0(13) -> 13* s_0(12) -> 13* s_0(10) -> 13* s_0(9) -> 13* c_2(23, 22) -> 24* c_2(21, 24) -> 22* c_2(21, 22) -> 22* c_2(21, 16) -> 22* c_2(21, 14) -> 22* c_2(21, 13) -> 22* c_2(21, 12) -> 22* c_2(21, 10) -> 22* c_2(21, 9) -> 22* c_1(18, 20) -> 20* c_1(18, 19) -> 20* c_1(15, 24) -> 16* c_1(15, 16) -> 16* c_1(15, 14) -> 16* c_1(15, 13) -> 16* c_1(15, 12) -> 16* c_1(15, 10) -> 16* c_1(15, 9) -> 16* c_1(14, 20) -> 19* c_1(14, 14) -> 19* c_1(14, 13) -> 19* c_1(14, 12) -> 19* c_1(14, 10) -> 19* c_1(14, 9) -> 19* c_1(13, 20) -> 19* c_1(13, 14) -> 19* c_1(13, 13) -> 19* c_1(13, 12) -> 19* c_1(13, 10) -> 19* c_1(13, 9) -> 19* c_1(12, 20) -> 19* c_1(12, 14) -> 19* c_1(12, 13) -> 19* c_1(12, 12) -> 19* c_1(12, 10) -> 19* c_1(12, 9) -> 19* c_1(10, 20) -> 19* c_1(10, 14) -> 19* c_1(10, 13) -> 19* c_1(10, 12) -> 19* c_1(10, 10) -> 19* c_1(10, 9) -> 19* c_1(9, 20) -> 19* c_1(9, 14) -> 19* c_1(9, 13) -> 19* c_1(9, 12) -> 19* c_1(9, 10) -> 19* c_1(9, 9) -> 19* c_0(14, 14) -> 10* c_0(14, 13) -> 10* c_0(14, 12) -> 10* c_0(14, 10) -> 10* c_0(14, 9) -> 10* c_0(13, 14) -> 14* c_0(13, 13) -> 14* c_0(13, 12) -> 14* c_0(13, 10) -> 14* c_0(13, 9) -> 14* c_0(12, 14) -> 10* c_0(12, 13) -> 10* c_0(12, 12) -> 10* c_0(12, 10) -> 10* c_0(12, 9) -> 10* c_0(10, 14) -> 10* c_0(10, 13) -> 10* c_0(10, 12) -> 10* c_0(10, 10) -> 10* c_0(10, 9) -> 10* c_0(9, 14) -> 10* c_0(9, 13) -> 10* c_0(9, 12) -> 10* c_0(9, 10) -> 10* c_0(9, 9) -> 10* h#_2(24, 20) -> 6* h#_2(24, 14) -> 6* h#_2(24, 13) -> 6* h#_2(24, 12) -> 6* h#_2(24, 10) -> 6* h#_2(24, 9) -> 6* h#_2(22, 20) -> 6* h#_2(22, 19) -> 6* h#_1(24, 20) -> 6* h#_1(22, 20) -> 6* h#_1(16, 20) -> 6* h#_1(16, 14) -> 6* h#_1(16, 13) -> 6* h#_1(16, 12) -> 6* h#_1(16, 10) -> 6* h#_1(16, 9) -> 6* h#_1(14, 20) -> 6* h#_1(13, 20) -> 6* h#_1(12, 20) -> 6* h#_1(10, 20) -> 6* h#_1(9, 20) -> 6* h#_0(14, 14) -> 6* h#_0(14, 13) -> 6* h#_0(14, 12) -> 6* h#_0(14, 10) -> 6* h#_0(14, 9) -> 6* h#_0(13, 14) -> 6* h#_0(12, 14) -> 6* h#_0(10, 14) -> 6* h#_0(9, 14) -> 6* h_0(14, 14) -> 9* h_0(14, 13) -> 9* h_0(14, 12) -> 9* h_0(14, 10) -> 9* h_0(14, 9) -> 9* h_0(13, 14) -> 9* h_0(13, 13) -> 9* h_0(13, 12) -> 9* h_0(13, 10) -> 9* h_0(13, 9) -> 9* h_0(12, 14) -> 9* h_0(12, 13) -> 9* h_0(12, 12) -> 9* h_0(12, 10) -> 9* h_0(12, 9) -> 9* h_0(10, 14) -> 9* h_0(10, 13) -> 9* h_0(10, 12) -> 9* h_0(10, 10) -> 9* h_0(10, 9) -> 9* h_0(9, 14) -> 9* h_0(9, 13) -> 9* h_0(9, 12) -> 9* h_0(9, 10) -> 9* h_0(9, 9) -> 9*} Strict: {h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))} EDG: {(h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z))), h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z))))} SCCS: Scc: {h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))} SCC: Strict: {h#(c(s(x), c(s(0()), y)), z) -> h#(y, c(s(0()), c(x, z)))} Weak: { h(x, c(y, z)) -> h(c(s(y), x), z), h(c(s(x), c(s(0()), y)), z) -> h(y, c(s(0()), c(x, z)))} SPSC: Simple Projection: pi(h#) = 0 Strict: {} Qed