YES
Problem:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
c(d(x1)) -> d(c(b(a(x1))))
Proof:
String Reversal Processor:
a(b(a(x1))) -> c(b(x1))
b(b(b(x1))) -> b(c(x1))
c(x1) -> b(a(x1))
d(c(x1)) -> a(b(c(d(x1))))
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 1] [0]
[d](x0) = [1 1 1]x0 + [1]
[1 1 1] [0],
[1 0 0] [0]
[c](x0) = [1 1 1]x0 + [1]
[1 0 1] [1],
[1 0 0]
[b](x0) = [1 0 0]x0
[0 0 0] ,
[1 0 0] [0]
[a](x0) = [1 1 0]x0 + [1]
[1 1 0] [1]
orientation:
[1 0 0] [0] [1 0 0] [0]
a(b(a(x1))) = [2 0 0]x1 + [1] >= [2 0 0]x1 + [1] = c(b(x1))
[2 0 0] [1] [1 0 0] [1]
[1 0 0] [1 0 0]
b(b(b(x1))) = [1 0 0]x1 >= [1 0 0]x1 = b(c(x1))
[0 0 0] [0 0 0]
[1 0 0] [0] [1 0 0]
c(x1) = [1 1 1]x1 + [1] >= [1 0 0]x1 = b(a(x1))
[1 0 1] [1] [0 0 0]
[2 0 1] [1] [1 0 1] [0]
d(c(x1)) = [3 1 2]x1 + [3] >= [2 0 2]x1 + [1] = a(b(c(d(x1))))
[3 1 2] [2] [2 0 2] [1]
problem:
a(b(a(x1))) -> c(b(x1))
b(b(b(x1))) -> b(c(x1))
c(x1) -> b(a(x1))
String Reversal Processor:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
DP Processor:
DPs:
a#(b(a(x1))) -> c#(x1)
a#(b(a(x1))) -> b#(c(x1))
b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> b#(x1)
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
TDG Processor:
DPs:
a#(b(a(x1))) -> c#(x1)
a#(b(a(x1))) -> b#(c(x1))
b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> b#(x1)
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
graph:
b#(b(b(x1))) -> c#(b(x1)) -> c#(x1) -> a#(b(x1))
b#(b(b(x1))) -> c#(b(x1)) -> c#(x1) -> b#(x1)
c#(x1) -> b#(x1) -> b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(c(x1))
c#(x1) -> a#(b(x1)) -> a#(b(a(x1))) -> c#(x1)
a#(b(a(x1))) -> b#(c(x1)) -> b#(b(b(x1))) -> c#(b(x1))
a#(b(a(x1))) -> c#(x1) -> c#(x1) -> a#(b(x1))
a#(b(a(x1))) -> c#(x1) -> c#(x1) -> b#(x1)
Arctic Interpretation Processor:
dimension: 1
interpretation:
[b#](x0) = -2x0 + 0,
[c#](x0) = x0 + 1,
[a#](x0) = -2x0 + 0,
[c](x0) = 4x0 + 3,
[b](x0) = 2x0 + 1,
[a](x0) = 2x0 + 1
orientation:
a#(b(a(x1))) = 2x1 + 1 >= x1 + 1 = c#(x1)
a#(b(a(x1))) = 2x1 + 1 >= 2x1 + 1 = b#(c(x1))
b#(b(b(x1))) = 2x1 + 1 >= 2x1 + 1 = c#(b(x1))
c#(x1) = x1 + 1 >= -2x1 + 0 = b#(x1)
c#(x1) = x1 + 1 >= x1 + 0 = a#(b(x1))
a(b(a(x1))) = 6x1 + 5 >= 6x1 + 5 = b(c(x1))
b(b(b(x1))) = 6x1 + 5 >= 6x1 + 5 = c(b(x1))
c(x1) = 4x1 + 3 >= 4x1 + 3 = a(b(x1))
problem:
DPs:
a#(b(a(x1))) -> c#(x1)
a#(b(a(x1))) -> b#(c(x1))
b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
EDG Processor:
DPs:
a#(b(a(x1))) -> c#(x1)
a#(b(a(x1))) -> b#(c(x1))
b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
graph:
b#(b(b(x1))) -> c#(b(x1)) -> c#(x1) -> a#(b(x1))
c#(x1) -> a#(b(x1)) -> a#(b(a(x1))) -> c#(x1)
c#(x1) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(c(x1))
a#(b(a(x1))) -> b#(c(x1)) -> b#(b(b(x1))) -> c#(b(x1))
a#(b(a(x1))) -> c#(x1) -> c#(x1) -> a#(b(x1))
Arctic Interpretation Processor:
dimension: 2
interpretation:
[b#](x0) = [-& 0 ]x0 + [2],
[c#](x0) = [-& 1 ]x0 + [0],
[a#](x0) = [-& 0 ]x0 + [0],
[0 1 ] [1]
[c](x0) = [-& 2 ]x0 + [1],
[0 0 ] [0]
[b](x0) = [-& 1 ]x0 + [0],
[0 0 ] [1]
[a](x0) = [-& 1 ]x0 + [1]
orientation:
a#(b(a(x1))) = [-& 2 ]x1 + [2] >= [-& 1 ]x1 + [0] = c#(x1)
a#(b(a(x1))) = [-& 2 ]x1 + [2] >= [-& 2 ]x1 + [2] = b#(c(x1))
b#(b(b(x1))) = [-& 2 ]x1 + [2] >= [-& 2 ]x1 + [1] = c#(b(x1))
c#(x1) = [-& 1 ]x1 + [0] >= [-& 1 ]x1 + [0] = a#(b(x1))
[0 2 ] [2] [0 2 ] [1]
a(b(a(x1))) = [-& 3 ]x1 + [3] >= [-& 3 ]x1 + [2] = b(c(x1))
[0 2 ] [1] [0 2 ] [1]
b(b(b(x1))) = [-& 3 ]x1 + [2] >= [-& 3 ]x1 + [2] = c(b(x1))
[0 1 ] [1] [0 1 ] [1]
c(x1) = [-& 2 ]x1 + [1] >= [-& 2 ]x1 + [1] = a(b(x1))
problem:
DPs:
a#(b(a(x1))) -> b#(c(x1))
b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
EDG Processor:
DPs:
a#(b(a(x1))) -> b#(c(x1))
b#(b(b(x1))) -> c#(b(x1))
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
graph:
b#(b(b(x1))) -> c#(b(x1)) -> c#(x1) -> a#(b(x1))
c#(x1) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(c(x1))
a#(b(a(x1))) -> b#(c(x1)) -> b#(b(b(x1))) -> c#(b(x1))
Arctic Interpretation Processor:
dimension: 3
interpretation:
[b#](x0) = [1 1 0]x0 + [0],
[c#](x0) = [1 1 1]x0 + [1],
[a#](x0) = [0 1 1]x0 + [0],
[0 0 1] [0]
[c](x0) = [0 0 1]x0 + [0]
[1 0 0] [1],
[1 0 0 ] [1 ]
[b](x0) = [-& -& 0 ]x0 + [-&]
[0 -& -&] [0 ],
[-& 1 0 ] [0]
[a](x0) = [-& 1 0 ]x0 + [0]
[0 0 1 ] [0]
orientation:
a#(b(a(x1))) = [1 2 2]x1 + [1] >= [1 1 2]x1 + [1] = b#(c(x1))
b#(b(b(x1))) = [3 2 2]x1 + [3] >= [2 1 1]x1 + [2] = c#(b(x1))
c#(x1) = [1 1 1]x1 + [1] >= [1 0 1]x1 + [1] = a#(b(x1))
[1 1 2] [1] [1 1 2] [1]
a(b(a(x1))) = [1 1 2]x1 + [1] >= [1 0 0]x1 + [1] = b(c(x1))
[0 2 1] [1] [0 0 1] [0]
[3 2 2] [3] [1 0 0] [1]
b(b(b(x1))) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = c(b(x1))
[2 1 1] [2] [2 1 1] [2]
[0 0 1] [0] [0 -& 1 ] [0]
c(x1) = [0 0 1]x1 + [0] >= [0 -& 1 ]x1 + [0] = a(b(x1))
[1 0 0] [1] [1 0 0 ] [1]
problem:
DPs:
a#(b(a(x1))) -> b#(c(x1))
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
EDG Processor:
DPs:
a#(b(a(x1))) -> b#(c(x1))
c#(x1) -> a#(b(x1))
TRS:
a(b(a(x1))) -> b(c(x1))
b(b(b(x1))) -> c(b(x1))
c(x1) -> a(b(x1))
graph:
c#(x1) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(c(x1))
SCC Processor:
#sccs: 0
#rules: 0
#arcs: 1/4