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