YES Problem: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y Proof: DP Processor: DPs: a#(x,y) -> c#(y) a#(x,y) -> b#(0(),c(y)) a#(x,y) -> b#(x,b(0(),c(y))) c#(b(y,c(x))) -> a#(0(),0()) c#(b(y,c(x))) -> b#(a(0(),0()),y) c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y EDG Processor: DPs: a#(x,y) -> c#(y) a#(x,y) -> b#(0(),c(y)) a#(x,y) -> b#(x,b(0(),c(y))) c#(b(y,c(x))) -> a#(0(),0()) c#(b(y,c(x))) -> b#(a(0(),0()),y) c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y graph: c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) -> c#(b(y,c(x))) -> a#(0(),0()) c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) -> c#(b(y,c(x))) -> b#(a(0(),0()),y) c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) -> c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) -> c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) -> c#(b(y,c(x))) -> a#(0(),0()) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) -> c#(b(y,c(x))) -> b#(a(0(),0()),y) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) -> c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) -> c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> c#(y) c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(0(),c(y)) c#(b(y,c(x))) -> a#(0(),0()) -> a#(x,y) -> b#(x,b(0(),c(y))) a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> a#(0(),0()) a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> b#(a(0(),0()),y) a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) a#(x,y) -> c#(y) -> c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) SCC Processor: #sccs: 1 #rules: 4 #arcs: 15/49 DPs: c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) c#(b(y,c(x))) -> a#(0(),0()) a#(x,y) -> c#(y) TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y Matrix Interpretation Processor: dimension: 1 interpretation: [c#](x0) = x0, [a#](x0, x1) = x1 + 1, [b](x0, x1) = x0 + x1, [c](x0) = 1, [0] = 0, [a](x0, x1) = x0 + 1 orientation: c#(b(y,c(x))) = y + 1 >= y + 1 = c#(b(a(0(),0()),y)) c#(b(y,c(x))) = y + 1 >= 1 = c#(c(b(a(0(),0()),y))) c#(b(y,c(x))) = y + 1 >= 1 = a#(0(),0()) a#(x,y) = y + 1 >= y = c#(y) a(x,y) = x + 1 >= x + 1 = b(x,b(0(),c(y))) c(b(y,c(x))) = 1 >= 1 = c(c(b(a(0(),0()),y))) b(y,0()) = y >= y = y problem: DPs: c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) c#(b(y,c(x))) -> a#(0(),0()) TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y Matrix Interpretation Processor: dimension: 1 interpretation: [c#](x0) = 1, [a#](x0, x1) = 0, [b](x0, x1) = x0 + x1, [c](x0) = 0, [0] = 1, [a](x0, x1) = x0 + 1 orientation: c#(b(y,c(x))) = 1 >= 1 = c#(b(a(0(),0()),y)) c#(b(y,c(x))) = 1 >= 1 = c#(c(b(a(0(),0()),y))) c#(b(y,c(x))) = 1 >= 0 = a#(0(),0()) a(x,y) = x + 1 >= x + 1 = b(x,b(0(),c(y))) c(b(y,c(x))) = 0 >= 0 = c(c(b(a(0(),0()),y))) b(y,0()) = y + 1 >= y = y problem: DPs: c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) c#(b(y,c(x))) -> c#(c(b(a(0(),0()),y))) TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {16} transitions: a0(12,14) -> 11* a0(13,11) -> 11* a0(13,13) -> 11* a0(14,10) -> 11* a0(14,12) -> 11* a0(14,14) -> 11* a0(10,11) -> 11* a0(10,13) -> 11* a0(11,10) -> 11* a0(11,12) -> 11* a0(11,14) -> 11* a0(12,11) -> 11* a0(12,13) -> 11* a0(13,10) -> 11* a0(13,12) -> 11* a0(13,14) -> 11* a0(14,11) -> 11* a0(14,13) -> 11* a0(10,10) -> 17,11 a0(10,12) -> 11* a0(10,14) -> 11* a0(11,11) -> 11* a0(11,13) -> 11* a0(12,10) -> 11* a0(12,12) -> 11* 00() -> 10* c{#,1}(26) -> 14,15 b1(23,29) -> 24* b1(24,10) -> 25* b1(24,12) -> 25* b1(24,14) -> 25* b1(24,24) -> 31* b1(23,28) -> 29* b1(24,11) -> 25* b1(24,13) -> 25* a1(23,23) -> 24* 01() -> 23* c1(25) -> 26* c1(31) -> 25* c1(23) -> 28* c{#,0}(10) -> 14* c{#,0}(12) -> 14* c{#,0}(19) -> 16* c{#,0}(14) -> 14* c{#,0}(11) -> 14* c{#,0}(13) -> 14* b0(12,14) -> 13* b0(13,11) -> 13* b0(13,13) -> 11,13 b0(14,10) -> 13* b0(14,12) -> 13* b0(14,14) -> 13* b0(10,11) -> 13* b0(10,13) -> 11,17,13 b0(11,10) -> 13* b0(11,12) -> 13* b0(11,14) -> 13* b0(12,11) -> 13* b0(12,13) -> 11,13 b0(17,15) -> 18* b0(13,10) -> 13* b0(13,12) -> 13* b0(13,14) -> 13* b0(14,11) -> 13* b0(14,13) -> 11,13 b0(10,10) -> 13* b0(10,12) -> 13* b0(10,14) -> 13* b0(11,11) -> 13* b0(11,13) -> 11,13 b0(11,17) -> 30* b0(12,10) -> 13* b0(12,12) -> 13* c0(30) -> 18* c0(10) -> 12* c0(12) -> 19,12 c0(14) -> 12* c0(11) -> 12* c0(18) -> 19* c0(13) -> 12* 10 -> 11,17,13,15 11 -> 30,13,15 12 -> 11,13,15 13 -> 11,15 14 -> 11,13,15 17 -> 18* 24 -> 25* problem: DPs: c#(b(y,c(x))) -> c#(b(a(0(),0()),y)) TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {6} transitions: a0(3,1) -> 2* a0(3,3) -> 2* a0(4,2) -> 2* a0(4,4) -> 2* a0(1,2) -> 2* a0(1,4) -> 2* a0(2,1) -> 2* a0(2,3) -> 2* a0(3,2) -> 2* a0(3,4) -> 2* a0(4,1) -> 2* a0(4,3) -> 2* a0(1,1) -> 7,2 a0(1,3) -> 2* a0(2,2) -> 2* a0(2,4) -> 2* 00() -> 1* c{#,1}(11) -> 6* b1(9,16) -> 10* b1(10,1) -> 11* b1(10,7) -> 11* b1(9,15) -> 16* a1(9,9) -> 10* 01() -> 9* c1(9) -> 15* c{#,0}(8) -> 6* b0(3,1) -> 4* b0(3,3) -> 4* b0(4,2) -> 4* b0(4,4) -> 2,4 b0(1,2) -> 4* b0(1,4) -> 2,7,4 b0(2,1) -> 4* b0(2,3) -> 4* b0(7,5) -> 8* b0(3,2) -> 4* b0(3,4) -> 2,4 b0(4,1) -> 4* b0(4,3) -> 4* b0(1,1) -> 4* b0(1,3) -> 4* b0(2,2) -> 4* b0(2,4) -> 2,4 c0(2) -> 3* c0(4) -> 3* c0(1) -> 3* c0(3) -> 3* 1 -> 2,7,4,5 2 -> 4,5 3 -> 2,4,5 4 -> 2,5 7 -> 8* 10 -> 11* problem: DPs: TRS: a(x,y) -> b(x,b(0(),c(y))) c(b(y,c(x))) -> c(c(b(a(0(),0()),y))) b(y,0()) -> y Qed