YES
Problem:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
Proof:
DP Processor:
DPs:
a#(b(x1)) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> c#(b(a(x1)))
b#(x1) -> a#(x1)
c#(c(x1)) -> b#(x1)
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
TDG Processor:
DPs:
a#(b(x1)) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> c#(b(a(x1)))
b#(x1) -> a#(x1)
c#(c(x1)) -> b#(x1)
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
graph:
c#(c(x1)) -> b#(x1) -> b#(x1) -> a#(x1)
b#(x1) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1)))
b#(x1) -> a#(x1) -> a#(b(x1)) -> b#(a(x1))
b#(x1) -> a#(x1) -> a#(b(x1)) -> a#(x1)
a#(b(x1)) -> c#(b(a(x1))) -> c#(c(x1)) -> b#(x1)
a#(b(x1)) -> b#(a(x1)) -> b#(x1) -> a#(x1)
a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1)))
a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> a#(x1)
Arctic Interpretation Processor:
dimension: 3
usable rules:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
interpretation:
[c#](x0) = [0 1 1]x0 + [0],
[b#](x0) = [-& 1 1 ]x0 + [0],
[a#](x0) = [-& 1 0 ]x0 + [0],
[-& 0 0 ] [0]
[c](x0) = [1 1 0 ]x0 + [0]
[0 0 1 ] [0],
[1 0 0] [0]
[b](x0) = [1 0 0]x0 + [0]
[1 0 0] [0],
[0 -& -&] [-&]
[a](x0) = [1 0 0 ]x0 + [0 ]
[1 0 0 ] [0 ]
orientation:
a#(b(x1)) = [2 1 1]x1 + [1] >= [-& 1 0 ]x1 + [0] = a#(x1)
a#(b(x1)) = [2 1 1]x1 + [1] >= [2 1 1]x1 + [1] = b#(a(x1))
a#(b(x1)) = [2 1 1]x1 + [1] >= [2 1 1]x1 + [1] = c#(b(a(x1)))
b#(x1) = [-& 1 1 ]x1 + [0] >= [-& 1 0 ]x1 + [0] = a#(x1)
c#(c(x1)) = [2 2 2]x1 + [1] >= [-& 1 1 ]x1 + [0] = b#(x1)
[0 -& -&] [-&]
a(x1) = [1 0 0 ]x1 + [0 ] >= x1 = x1
[1 0 0 ] [0 ]
[1 0 0] [0] [1 0 0] [0]
a(b(x1)) = [2 1 1]x1 + [1] >= [2 1 1]x1 + [1] = c(b(a(x1)))
[2 1 1] [1] [2 1 1] [1]
[1 0 0] [0] [0 -& -&] [-&]
b(x1) = [1 0 0]x1 + [0] >= [1 0 0 ]x1 + [0 ] = a(x1)
[1 0 0] [0] [1 0 0 ] [0 ]
[1 1 1] [0] [1 0 0] [0]
c(c(x1)) = [2 2 1]x1 + [1] >= [1 0 0]x1 + [0] = b(x1)
[1 1 2] [1] [1 0 0] [0]
problem:
DPs:
a#(b(x1)) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> c#(b(a(x1)))
b#(x1) -> a#(x1)
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
Restore Modifier:
DPs:
a#(b(x1)) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> c#(b(a(x1)))
b#(x1) -> a#(x1)
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
EDG Processor:
DPs:
a#(b(x1)) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> c#(b(a(x1)))
b#(x1) -> a#(x1)
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
graph:
b#(x1) -> a#(x1) -> a#(b(x1)) -> a#(x1)
b#(x1) -> a#(x1) -> a#(b(x1)) -> b#(a(x1))
b#(x1) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1)))
a#(b(x1)) -> b#(a(x1)) -> b#(x1) -> a#(x1)
a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> a#(x1)
a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1)))
SCC Processor:
#sccs: 1
#rules: 3
#arcs: 7/16
DPs:
b#(x1) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> a#(x1)
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
Arctic Interpretation Processor:
dimension: 3
usable rules:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
interpretation:
[b#](x0) = [0 0 1]x0 + [0],
[a#](x0) = [0 -& 0 ]x0 + [0],
[-& 0 0 ] [0 ]
[c](x0) = [0 0 0 ]x0 + [0 ]
[1 -& 0 ] [-&],
[0 -& 0 ] [0]
[b](x0) = [0 0 0 ]x0 + [0]
[1 0 1 ] [1],
[0 -& 0 ] [-&]
[a](x0) = [0 0 0 ]x0 + [-&]
[0 -& 0 ] [0 ]
orientation:
b#(x1) = [0 0 1]x1 + [0] >= [0 -& 0 ]x1 + [0] = a#(x1)
a#(b(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 + [1] = b#(a(x1))
a#(b(x1)) = [1 0 1]x1 + [1] >= [0 -& 0 ]x1 + [0] = a#(x1)
[0 -& 0 ] [-&]
a(x1) = [0 0 0 ]x1 + [-&] >= x1 = x1
[0 -& 0 ] [0 ]
[1 0 1] [1] [1 0 1] [1]
a(b(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 + [1] = c(b(a(x1)))
[1 0 1] [1] [1 0 1] [1]
[0 -& 0 ] [0] [0 -& 0 ] [-&]
b(x1) = [0 0 0 ]x1 + [0] >= [0 0 0 ]x1 + [-&] = a(x1)
[1 0 1 ] [1] [0 -& 0 ] [0 ]
[1 0 0] [0] [0 -& 0 ] [0]
c(c(x1)) = [1 0 0]x1 + [0] >= [0 0 0 ]x1 + [0] = b(x1)
[1 1 1] [1] [1 0 1 ] [1]
problem:
DPs:
b#(x1) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
Restore Modifier:
DPs:
b#(x1) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
EDG Processor:
DPs:
b#(x1) -> a#(x1)
a#(b(x1)) -> b#(a(x1))
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
graph:
b#(x1) -> a#(x1) -> a#(b(x1)) -> b#(a(x1))
a#(b(x1)) -> b#(a(x1)) -> b#(x1) -> a#(x1)
Arctic Interpretation Processor:
dimension: 4
usable rules:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
interpretation:
[b#](x0) = [0 0 1 0]x0 + [1],
[a#](x0) = [-& -& 0 -&]x0 + [0],
[0 0 0 0 ] [1 ]
[-& -& 0 0 ] [-&]
[c](x0) = [0 1 0 0 ]x0 + [0 ]
[0 0 0 0 ] [-&],
[0 1 0 0 ] [0]
[-& 0 0 -&] [0]
[b](x0) = [0 1 1 0 ]x0 + [1]
[-& 0 0 0 ] [1],
[0 0 0 0 ] [0]
[-& 0 0 -&] [0]
[a](x0) = [-& 0 0 -&]x0 + [0]
[-& 0 0 0 ] [1]
orientation:
b#(x1) = [0 0 1 0]x1 + [1] >= [-& -& 0 -&]x1 + [0] = a#(x1)
a#(b(x1)) = [0 1 1 0]x1 + [1] >= [0 1 1 0]x1 + [1] = b#(a(x1))
[0 0 0 0 ] [0]
[-& 0 0 -&] [0]
a(x1) = [-& 0 0 -&]x1 + [0] >= x1 = x1
[-& 0 0 0 ] [1]
[0 1 1 0] [1] [0 1 1 0] [1]
[0 1 1 0] [1] [0 1 1 0] [1]
a(b(x1)) = [0 1 1 0]x1 + [1] >= [0 1 1 0]x1 + [1] = c(b(a(x1)))
[0 1 1 0] [1] [0 1 1 0] [1]
[0 1 0 0 ] [0] [0 0 0 0 ] [0]
[-& 0 0 -&] [0] [-& 0 0 -&] [0]
b(x1) = [0 1 1 0 ]x1 + [1] >= [-& 0 0 -&]x1 + [0] = a(x1)
[-& 0 0 0 ] [1] [-& 0 0 0 ] [1]
[0 1 0 0] [1] [0 1 0 0 ] [0]
[0 1 0 0] [0] [-& 0 0 -&] [0]
c(c(x1)) = [0 1 1 1]x1 + [1] >= [0 1 1 0 ]x1 + [1] = b(x1)
[0 1 0 0] [1] [-& 0 0 0 ] [1]
problem:
DPs:
a#(b(x1)) -> b#(a(x1))
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
Restore Modifier:
DPs:
a#(b(x1)) -> b#(a(x1))
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
EDG Processor:
DPs:
a#(b(x1)) -> b#(a(x1))
TRS:
a(x1) -> x1
a(b(x1)) -> c(b(a(x1)))
b(x1) -> a(x1)
c(c(x1)) -> b(x1)
graph:
Qed