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