YES
Problem:
b(a(b(x1))) -> b(a(a(a(b(x1)))))
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1)
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
b(a(a(b(b(x1))))) -> b(x1)
b(b(a(a(b(x1))))) -> b(x1)
b(a(a(a(b(a(b(x1))))))) -> b(x1)
b(a(b(a(a(a(b(x1))))))) -> b(x1)
Proof:
String Reversal Processor:
b(a(b(x1))) -> b(a(a(a(b(x1)))))
b(a(a(b(a(a(a(b(x1)))))))) -> b(b(a(a(a(b(a(a(b(a(a(b(x1))))))))))))
b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1)
b(b(b(a(a(a(b(x1))))))) -> b(a(a(a(b(b(b(x1)))))))
b(b(a(a(b(x1))))) -> b(x1)
b(a(a(b(b(x1))))) -> b(x1)
b(a(b(a(a(a(b(x1))))))) -> b(x1)
b(a(a(a(b(a(b(x1))))))) -> b(x1)
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 0]
[a](x0) = [0 0 1]x0
[0 0 0] ,
[1 1 0] [0]
[b](x0) = [0 0 0]x0 + [0]
[1 1 0] [1]
orientation:
[2 2 0] [1] [1 1 0] [0]
b(a(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(a(a(b(x1)))))
[2 2 0] [2] [1 1 0] [1]
[1 1 0] [0] [1 1 0] [0]
b(a(a(b(a(a(a(b(x1)))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(b(a(a(a(b(a(a(b(a(a(b(x1))))))))))))
[1 1 0] [1] [1 1 0] [1]
[1 1 0] [0] [1 1 0] [0]
b(a(a(a(b(a(a(a(b(x1))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
[1 1 0] [1] [1 1 0] [1]
[1 1 0] [0] [1 1 0] [0]
b(b(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(a(a(b(b(b(x1)))))))
[1 1 0] [1] [1 1 0] [1]
[1 1 0] [0] [1 1 0] [0]
b(b(a(a(b(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
[1 1 0] [1] [1 1 0] [1]
[1 1 0] [0] [1 1 0] [0]
b(a(a(b(b(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
[1 1 0] [1] [1 1 0] [1]
[2 2 0] [1] [1 1 0] [0]
b(a(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
[2 2 0] [2] [1 1 0] [1]
[2 2 0] [1] [1 1 0] [0]
b(a(a(a(b(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
[2 2 0] [2] [1 1 0] [1]
problem:
b(a(a(b(a(a(a(b(x1)))))))) -> b(b(a(a(a(b(a(a(b(a(a(b(x1))))))))))))
b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1)
b(b(b(a(a(a(b(x1))))))) -> b(a(a(a(b(b(b(x1)))))))
b(b(a(a(b(x1))))) -> b(x1)
b(a(a(b(b(x1))))) -> b(x1)
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 0]
[a](x0) = [0 0 1]x0
[0 1 0] ,
[1 0 1] [0]
[b](x0) = [0 0 0]x0 + [1]
[0 0 0] [0]
orientation:
[1 0 1] [1] [1 0 1] [1]
b(a(a(b(a(a(a(b(x1)))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(b(a(a(a(b(a(a(b(a(a(b(x1))))))))))))
[0 0 0] [0] [0 0 0] [0]
[1 0 1] [2] [1 0 1] [0]
b(a(a(a(b(a(a(a(b(x1))))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(x1)
[0 0 0] [0] [0 0 0] [0]
[1 0 1] [1] [1 0 1] [1]
b(b(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(a(a(a(b(b(b(x1)))))))
[0 0 0] [0] [0 0 0] [0]
[1 0 1] [0] [1 0 1] [0]
b(b(a(a(b(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(x1)
[0 0 0] [0] [0 0 0] [0]
[1 0 1] [0] [1 0 1] [0]
b(a(a(b(b(x1))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(x1)
[0 0 0] [0] [0 0 0] [0]
problem:
b(a(a(b(a(a(a(b(x1)))))))) -> b(b(a(a(a(b(a(a(b(a(a(b(x1))))))))))))
b(b(b(a(a(a(b(x1))))))) -> b(a(a(a(b(b(b(x1)))))))
b(b(a(a(b(x1))))) -> b(x1)
b(a(a(b(b(x1))))) -> b(x1)
String Reversal Processor:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
b(a(a(b(b(x1))))) -> b(x1)
b(b(a(a(b(x1))))) -> b(x1)
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 0] [0]
[a](x0) = [0 0 1]x0 + [1]
[0 1 0] [0],
[1 0 1]
[b](x0) = [1 0 1]x0
[0 0 0]
orientation:
[2 0 2] [3] [2 0 2] [3]
b(a(a(a(b(a(a(b(x1)))))))) = [2 0 2]x1 + [3] >= [2 0 2]x1 + [3] = b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
[0 0 0] [0] [0 0 0] [0]
[2 0 2] [1] [2 0 2] [1]
b(a(a(a(b(b(b(x1))))))) = [2 0 2]x1 + [1] >= [2 0 2]x1 + [1] = b(b(b(a(a(a(b(x1)))))))
[0 0 0] [0] [0 0 0] [0]
[1 0 1] [1] [1 0 1]
b(a(a(b(b(x1))))) = [1 0 1]x1 + [1] >= [1 0 1]x1 = b(x1)
[0 0 0] [0] [0 0 0]
[1 0 1] [1] [1 0 1]
b(b(a(a(b(x1))))) = [1 0 1]x1 + [1] >= [1 0 1]x1 = b(x1)
[0 0 0] [0] [0 0 0]
problem:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
DP Processor:
DPs:
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1)))))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1)))))))
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
EDG Processor:
DPs:
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1)))))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1)))))))
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
graph:
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1)))))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1))))))
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1)))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1)))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(b(x1))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(a(b(b(x1)))))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(b(a(a(a(b(x1))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(b(b(a(a(a(b(x1)))))))
SCC Processor:
#sccs: 1
#rules: 2
#arcs: 14/49
DPs:
b#(a(a(a(b(a(a(b(x1)))))))) -> b#(a(a(a(b(b(x1))))))
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
Bounds Processor:
bound: 1
enrichment: match-dp
automaton:
final states: {1}
transitions:
b0(57) -> 58*
b0(2) -> 3*
b0(74) -> 75*
b0(39) -> 40*
b0(71) -> 72*
b0(56) -> 57*
b0(36) -> 37*
b0(58) -> 59*
b0(33) -> 34*
b0(3) -> 4*
b0(85) -> 86*
b{#,1}(46) -> 47*
a1(45) -> 46*
a1(44) -> 45*
a1(43) -> 44*
b1(42) -> 43*
b1(41) -> 42*
b1(83) -> 84*
f40() -> 2*
b{#,0}(17) -> 18*
b{#,0}(7) -> 1*
a0(35) -> 36*
a0(15) -> 16*
a0(5) -> 6*
a0(72) -> 73*
a0(62) -> 63*
a0(37) -> 38*
a0(64) -> 65*
a0(34) -> 35*
a0(14) -> 15*
a0(4) -> 5*
a0(16) -> 17*
a0(6) -> 7*
a0(93) -> 94*
a0(73) -> 74*
a0(38) -> 39*
1 -> 18*
3 -> 14*
7 -> 33*
17 -> 56*
18 -> 1*
34 -> 57,85
36 -> 41*
40 -> 34,3
46 -> 71*
47 -> 18,1
57 -> 34,85,64
58 -> 62*
59 -> 3*
63 -> 5*
65 -> 5*
74 -> 83*
75 -> 15*
84 -> 42*
86 -> 93,33
94 -> 5*
problem:
DPs:
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
Restore Modifier:
DPs:
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
EDG Processor:
DPs:
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
graph:
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1))))) ->
b#(a(a(a(b(b(b(x1))))))) -> b#(a(a(a(b(x1)))))
Matrix Interpretation Processor: dim=4
interpretation:
[b#](x0) = [0 0 0 1]x0,
[0 0 0 1]
[0 0 0 0]
[a](x0) = [0 1 0 0]x0
[1 0 0 0] ,
[0 1 0 1] [0]
[1 0 1 1] [0]
[b](x0) = [0 0 0 0]x0 + [1]
[0 0 0 0] [0]
orientation:
b#(a(a(a(b(b(b(x1))))))) = [0 1 0 1]x1 + [1] >= [0 1 0 1]x1 = b#(a(a(a(b(x1)))))
[0] [0]
[0] [0]
b(a(a(a(b(a(a(b(x1)))))))) = [1] >= [1] = b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
[0] [0]
[0 1 0 1] [1] [0 1 0 1] [1]
[0 1 0 1] [1] [0 1 0 1] [1]
b(a(a(a(b(b(b(x1))))))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(b(b(a(a(a(b(x1)))))))
[0 0 0 0] [0] [0 0 0 0] [0]
problem:
DPs:
TRS:
b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
Qed