(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(b(b(x)))) → C(C(x))
b(b(c(c(x)))) → A(A(x))
c(c(a(a(x)))) → B(B(x))
A(A(C(C(x)))) → b(b(x))
C(C(B(B(x)))) → a(a(x))
B(B(A(A(x)))) → c(c(x))
a(a(a(a(a(a(a(a(a(a(x)))))))))) → A(A(A(A(A(A(x))))))
A(A(A(A(A(A(A(A(x)))))))) → a(a(a(a(a(a(a(a(x))))))))
b(b(b(b(b(b(b(b(b(b(x)))))))))) → B(B(B(B(B(B(x))))))
B(B(B(B(B(B(B(B(x)))))))) → b(b(b(b(b(b(b(b(x))))))))
c(c(c(c(c(c(c(c(c(c(x)))))))))) → C(C(C(C(C(C(x))))))
C(C(C(C(C(C(C(C(x)))))))) → c(c(c(c(c(c(c(c(x))))))))
B(B(a(a(a(a(a(a(a(a(x)))))))))) → c(c(A(A(A(A(A(A(x))))))))
A(A(A(A(A(A(b(b(x)))))))) → a(a(a(a(a(a(a(a(C(C(x))))))))))
C(C(b(b(b(b(b(b(b(b(x)))))))))) → a(a(B(B(B(B(B(B(x))))))))
B(B(B(B(B(B(c(c(x)))))))) → b(b(b(b(b(b(b(b(A(A(x))))))))))
A(A(c(c(c(c(c(c(c(c(x)))))))))) → b(b(C(C(C(C(C(C(x))))))))
C(C(C(C(C(C(a(a(x)))))))) → c(c(c(c(c(c(c(c(B(B(x))))))))))
a(a(A(A(x)))) → x
A(A(a(a(x)))) → x
b(b(B(B(x)))) → x
B(B(b(b(x)))) → x
c(c(C(C(x)))) → x
C(C(c(c(x)))) → x
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(A(x1)) = 3 + x1
POL(B(x1)) = 3 + x1
POL(C(x1)) = 3 + x1
POL(a(x1)) = 2 + x1
POL(b(x1)) = 2 + x1
POL(c(x1)) = 2 + x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a(a(b(b(x)))) → C(C(x))
b(b(c(c(x)))) → A(A(x))
c(c(a(a(x)))) → B(B(x))
A(A(C(C(x)))) → b(b(x))
C(C(B(B(x)))) → a(a(x))
B(B(A(A(x)))) → c(c(x))
a(a(a(a(a(a(a(a(a(a(x)))))))))) → A(A(A(A(A(A(x))))))
A(A(A(A(A(A(A(A(x)))))))) → a(a(a(a(a(a(a(a(x))))))))
b(b(b(b(b(b(b(b(b(b(x)))))))))) → B(B(B(B(B(B(x))))))
B(B(B(B(B(B(B(B(x)))))))) → b(b(b(b(b(b(b(b(x))))))))
c(c(c(c(c(c(c(c(c(c(x)))))))))) → C(C(C(C(C(C(x))))))
C(C(C(C(C(C(C(C(x)))))))) → c(c(c(c(c(c(c(c(x))))))))
a(a(A(A(x)))) → x
A(A(a(a(x)))) → x
b(b(B(B(x)))) → x
B(B(b(b(x)))) → x
c(c(C(C(x)))) → x
C(C(c(c(x)))) → x
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
B(B(a(a(a(a(a(a(a(a(x)))))))))) → c(c(A(A(A(A(A(A(x))))))))
A(A(A(A(A(A(b(b(x)))))))) → a(a(a(a(a(a(a(a(C(C(x))))))))))
C(C(b(b(b(b(b(b(b(b(x)))))))))) → a(a(B(B(B(B(B(B(x))))))))
B(B(B(B(B(B(c(c(x)))))))) → b(b(b(b(b(b(b(b(A(A(x))))))))))
A(A(c(c(c(c(c(c(c(c(x)))))))))) → b(b(C(C(C(C(C(C(x))))))))
C(C(C(C(C(C(a(a(x)))))))) → c(c(c(c(c(c(c(c(B(B(x))))))))))
Q is empty.
(3) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
B(B(a(a(a(a(a(a(a(a(x)))))))))) → c(c(A(A(A(A(A(A(x))))))))
A(A(A(A(A(A(b(b(x)))))))) → a(a(a(a(a(a(a(a(C(C(x))))))))))
C(C(b(b(b(b(b(b(b(b(x)))))))))) → a(a(B(B(B(B(B(B(x))))))))
B(B(B(B(B(B(c(c(x)))))))) → b(b(b(b(b(b(b(b(A(A(x))))))))))
A(A(c(c(c(c(c(c(c(c(x)))))))))) → b(b(C(C(C(C(C(C(x))))))))
C(C(C(C(C(C(a(a(x)))))))) → c(c(c(c(c(c(c(c(B(B(x))))))))))
The set Q consists of the following terms:
B(B(a(a(a(a(a(a(a(a(x0))))))))))
A(A(A(A(A(A(b(b(x0))))))))
C(C(b(b(b(b(b(b(b(b(x0))))))))))
B(B(B(B(B(B(c(c(x0))))))))
A(A(c(c(c(c(c(c(c(c(x0))))))))))
C(C(C(C(C(C(a(a(x0))))))))
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(A(A(A(x))))))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(A(A(x)))))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(A(x))))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(x)))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(x))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(x)
A1(A(A(A(A(A(b(b(x)))))))) → C1(C(x))
A1(A(A(A(A(A(b(b(x)))))))) → C1(x)
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(B(B(B(x))))))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(B(B(x)))))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(B(x))))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(x)))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(x))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(x)
B1(B(B(B(B(B(c(c(x)))))))) → A1(A(x))
B1(B(B(B(B(B(c(c(x)))))))) → A1(x)
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(C(C(C(x))))))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(C(C(x)))))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(C(x))))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(x)))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(x))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(x)
C1(C(C(C(C(C(a(a(x)))))))) → B1(B(x))
C1(C(C(C(C(C(a(a(x)))))))) → B1(x)
The TRS R consists of the following rules:
B(B(a(a(a(a(a(a(a(a(x)))))))))) → c(c(A(A(A(A(A(A(x))))))))
A(A(A(A(A(A(b(b(x)))))))) → a(a(a(a(a(a(a(a(C(C(x))))))))))
C(C(b(b(b(b(b(b(b(b(x)))))))))) → a(a(B(B(B(B(B(B(x))))))))
B(B(B(B(B(B(c(c(x)))))))) → b(b(b(b(b(b(b(b(A(A(x))))))))))
A(A(c(c(c(c(c(c(c(c(x)))))))))) → b(b(C(C(C(C(C(C(x))))))))
C(C(C(C(C(C(a(a(x)))))))) → c(c(c(c(c(c(c(c(B(B(x))))))))))
The set Q consists of the following terms:
B(B(a(a(a(a(a(a(a(a(x0))))))))))
A(A(A(A(A(A(b(b(x0))))))))
C(C(b(b(b(b(b(b(b(b(x0))))))))))
B(B(B(B(B(B(c(c(x0))))))))
A(A(c(c(c(c(c(c(c(c(x0))))))))))
C(C(C(C(C(C(a(a(x0))))))))
We have to consider all minimal (P,Q,R)-chains.
(7) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(A(A(A(x))))))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(A(A(x)))))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(A(x))))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(A(x)))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(A(x))
B1(B(a(a(a(a(a(a(a(a(x)))))))))) → A1(x)
A1(A(A(A(A(A(b(b(x)))))))) → C1(C(x))
A1(A(A(A(A(A(b(b(x)))))))) → C1(x)
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(B(B(B(x))))))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(B(B(x)))))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(B(x))))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(B(x)))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(B(x))
C1(C(b(b(b(b(b(b(b(b(x)))))))))) → B1(x)
B1(B(B(B(B(B(c(c(x)))))))) → A1(A(x))
B1(B(B(B(B(B(c(c(x)))))))) → A1(x)
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(C(C(C(x))))))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(C(C(x)))))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(C(x))))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(C(x)))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(C(x))
A1(A(c(c(c(c(c(c(c(c(x)))))))))) → C1(x)
C1(C(C(C(C(C(a(a(x)))))))) → B1(B(x))
C1(C(C(C(C(C(a(a(x)))))))) → B1(x)
Used ordering: Polynomial interpretation [POLO]:
POL(A(x1)) = 3 + x1
POL(A1(x1)) = 2 + 2·x1
POL(B(x1)) = 3 + x1
POL(B1(x1)) = 2 + 2·x1
POL(C(x1)) = 3 + x1
POL(C1(x1)) = 2 + 2·x1
POL(a(x1)) = 2 + x1
POL(b(x1)) = 2 + x1
POL(c(x1)) = 2 + x1
(8) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
B(B(a(a(a(a(a(a(a(a(x)))))))))) → c(c(A(A(A(A(A(A(x))))))))
A(A(A(A(A(A(b(b(x)))))))) → a(a(a(a(a(a(a(a(C(C(x))))))))))
C(C(b(b(b(b(b(b(b(b(x)))))))))) → a(a(B(B(B(B(B(B(x))))))))
B(B(B(B(B(B(c(c(x)))))))) → b(b(b(b(b(b(b(b(A(A(x))))))))))
A(A(c(c(c(c(c(c(c(c(x)))))))))) → b(b(C(C(C(C(C(C(x))))))))
C(C(C(C(C(C(a(a(x)))))))) → c(c(c(c(c(c(c(c(B(B(x))))))))))
The set Q consists of the following terms:
B(B(a(a(a(a(a(a(a(a(x0))))))))))
A(A(A(A(A(A(b(b(x0))))))))
C(C(b(b(b(b(b(b(b(b(x0))))))))))
B(B(B(B(B(B(c(c(x0))))))))
A(A(c(c(c(c(c(c(c(c(x0))))))))))
C(C(C(C(C(C(a(a(x0))))))))
We have to consider all minimal (P,Q,R)-chains.
(9) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(10) YES