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