(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(x)) → C(x)
b(c(x)) → A(x)
c(a(x)) → B(x)
A(C(x)) → b(x)
C(B(x)) → a(x)
B(A(x)) → c(x)
a(a(a(a(a(x))))) → A(A(A(x)))
A(A(A(A(x)))) → a(a(a(a(x))))
b(b(b(b(b(x))))) → B(B(B(x)))
B(B(B(B(x)))) → b(b(b(b(x))))
c(c(c(c(c(x))))) → C(C(C(x)))
C(C(C(C(x)))) → c(c(c(c(x))))
B(a(a(a(a(x))))) → c(A(A(A(x))))
A(A(A(b(x)))) → a(a(a(a(C(x)))))
C(b(b(b(b(x))))) → a(B(B(B(x))))
B(B(B(c(x)))) → b(b(b(b(A(x)))))
A(c(c(c(c(x))))) → b(C(C(C(x))))
C(C(C(a(x)))) → c(c(c(c(B(x)))))
a(A(x)) → x
A(a(x)) → x
b(B(x)) → x
B(b(x)) → x
c(C(x)) → x
C(c(x)) → x
Q is empty.
(1) QTRS Reverse (EQUIVALENT transformation)
We applied the QTRS Reverse Processor [REVERSE].
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
b(a(x)) → C(x)
c(b(x)) → A(x)
a(c(x)) → B(x)
C(A(x)) → b(x)
B(C(x)) → a(x)
A(B(x)) → c(x)
a(a(a(a(a(x))))) → A(A(A(x)))
A(A(A(A(x)))) → a(a(a(a(x))))
b(b(b(b(b(x))))) → B(B(B(x)))
B(B(B(B(x)))) → b(b(b(b(x))))
c(c(c(c(c(x))))) → C(C(C(x)))
C(C(C(C(x)))) → c(c(c(c(x))))
a(a(a(a(B(x))))) → A(A(A(c(x))))
b(A(A(A(x)))) → C(a(a(a(a(x)))))
b(b(b(b(C(x))))) → B(B(B(a(x))))
c(B(B(B(x)))) → A(b(b(b(b(x)))))
c(c(c(c(A(x))))) → C(C(C(b(x))))
a(C(C(C(x)))) → B(c(c(c(c(x)))))
A(a(x)) → x
a(A(x)) → x
B(b(x)) → x
b(B(x)) → x
C(c(x)) → x
c(C(x)) → x
Q is empty.
(3) 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:
b(a(x)) → C(x)
c(b(x)) → A(x)
a(c(x)) → B(x)
C(A(x)) → b(x)
B(C(x)) → a(x)
A(B(x)) → c(x)
a(a(a(a(a(x))))) → A(A(A(x)))
A(A(A(A(x)))) → a(a(a(a(x))))
b(b(b(b(b(x))))) → B(B(B(x)))
B(B(B(B(x)))) → b(b(b(b(x))))
c(c(c(c(c(x))))) → C(C(C(x)))
C(C(C(C(x)))) → c(c(c(c(x))))
A(a(x)) → x
a(A(x)) → x
B(b(x)) → x
b(B(x)) → x
C(c(x)) → x
c(C(x)) → x
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(a(B(x))))) → A(A(A(c(x))))
b(A(A(A(x)))) → C(a(a(a(a(x)))))
b(b(b(b(C(x))))) → B(B(B(a(x))))
c(B(B(B(x)))) → A(b(b(b(b(x)))))
c(c(c(c(A(x))))) → C(C(C(b(x))))
a(C(C(C(x)))) → B(c(c(c(c(x)))))
Q is empty.
(5) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(a(B(x))))) → A(A(A(c(x))))
b(A(A(A(x)))) → C(a(a(a(a(x)))))
b(b(b(b(C(x))))) → B(B(B(a(x))))
c(B(B(B(x)))) → A(b(b(b(b(x)))))
c(c(c(c(A(x))))) → C(C(C(b(x))))
a(C(C(C(x)))) → B(c(c(c(c(x)))))
The set Q consists of the following terms:
a(a(a(a(B(x0)))))
b(A(A(A(x0))))
b(b(b(b(C(x0)))))
c(B(B(B(x0))))
c(c(c(c(A(x0)))))
a(C(C(C(x0))))
(7) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A1(a(a(a(B(x))))) → C1(x)
B1(A(A(A(x)))) → A1(a(a(a(x))))
B1(A(A(A(x)))) → A1(a(a(x)))
B1(A(A(A(x)))) → A1(a(x))
B1(A(A(A(x)))) → A1(x)
B1(b(b(b(C(x))))) → A1(x)
C1(B(B(B(x)))) → B1(b(b(b(x))))
C1(B(B(B(x)))) → B1(b(b(x)))
C1(B(B(B(x)))) → B1(b(x))
C1(B(B(B(x)))) → B1(x)
C1(c(c(c(A(x))))) → B1(x)
A1(C(C(C(x)))) → C1(c(c(c(x))))
A1(C(C(C(x)))) → C1(c(c(x)))
A1(C(C(C(x)))) → C1(c(x))
A1(C(C(C(x)))) → C1(x)
The TRS R consists of the following rules:
a(a(a(a(B(x))))) → A(A(A(c(x))))
b(A(A(A(x)))) → C(a(a(a(a(x)))))
b(b(b(b(C(x))))) → B(B(B(a(x))))
c(B(B(B(x)))) → A(b(b(b(b(x)))))
c(c(c(c(A(x))))) → C(C(C(b(x))))
a(C(C(C(x)))) → B(c(c(c(c(x)))))
The set Q consists of the following terms:
a(a(a(a(B(x0)))))
b(A(A(A(x0))))
b(b(b(b(C(x0)))))
c(B(B(B(x0))))
c(c(c(c(A(x0)))))
a(C(C(C(x0))))
We have to consider all minimal (P,Q,R)-chains.
(9) 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:
A1(a(a(a(B(x))))) → C1(x)
B1(A(A(A(x)))) → A1(a(a(a(x))))
B1(A(A(A(x)))) → A1(a(a(x)))
B1(A(A(A(x)))) → A1(a(x))
B1(A(A(A(x)))) → A1(x)
B1(b(b(b(C(x))))) → A1(x)
C1(B(B(B(x)))) → B1(b(b(b(x))))
C1(B(B(B(x)))) → B1(b(b(x)))
C1(B(B(B(x)))) → B1(b(x))
C1(B(B(B(x)))) → B1(x)
C1(c(c(c(A(x))))) → B1(x)
A1(C(C(C(x)))) → C1(c(c(c(x))))
A1(C(C(C(x)))) → C1(c(c(x)))
A1(C(C(C(x)))) → C1(c(x))
A1(C(C(C(x)))) → C1(x)
Used ordering: Polynomial interpretation [POLO]:
POL(A(x1)) = 3 + x1
POL(A1(x1)) = 2·x1
POL(B(x1)) = 3 + x1
POL(B1(x1)) = 2·x1
POL(C(x1)) = 3 + x1
POL(C1(x1)) = 2·x1
POL(a(x1)) = 2 + x1
POL(b(x1)) = 2 + x1
POL(c(x1)) = 2 + x1
(10) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
a(a(a(a(B(x))))) → A(A(A(c(x))))
b(A(A(A(x)))) → C(a(a(a(a(x)))))
b(b(b(b(C(x))))) → B(B(B(a(x))))
c(B(B(B(x)))) → A(b(b(b(b(x)))))
c(c(c(c(A(x))))) → C(C(C(b(x))))
a(C(C(C(x)))) → B(c(c(c(c(x)))))
The set Q consists of the following terms:
a(a(a(a(B(x0)))))
b(A(A(A(x0))))
b(b(b(b(C(x0)))))
c(B(B(B(x0))))
c(c(c(c(A(x0)))))
a(C(C(C(x0))))
We have to consider all minimal (P,Q,R)-chains.
(11) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(12) YES