(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x))) → a(b(b(a(x))))
b(b(b(x))) → b(b(x))
Q is empty.
(1) RootLabelingProof (EQUIVALENT transformation)
We used plain root labeling [ROOTLAB] with the following heuristic:
LabelAll: All function symbols get labeled
As Q is empty the root labeling was sound AND complete.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a_{b_1}(b_{a_1}(a_{a_1}(x))) → a_{b_1}(b_{b_1}(b_{a_1}(a_{a_1}(x))))
a_{b_1}(b_{a_1}(a_{b_1}(x))) → a_{b_1}(b_{b_1}(b_{a_1}(a_{b_1}(x))))
b_{b_1}(b_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(x))
b_{b_1}(b_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{b_1}(x))
Q is empty.
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A_{B_1}(b_{a_1}(a_{a_1}(x))) → A_{B_1}(b_{b_1}(b_{a_1}(a_{a_1}(x))))
A_{B_1}(b_{a_1}(a_{a_1}(x))) → B_{B_1}(b_{a_1}(a_{a_1}(x)))
A_{B_1}(b_{a_1}(a_{b_1}(x))) → A_{B_1}(b_{b_1}(b_{a_1}(a_{b_1}(x))))
A_{B_1}(b_{a_1}(a_{b_1}(x))) → B_{B_1}(b_{a_1}(a_{b_1}(x)))
The TRS R consists of the following rules:
a_{b_1}(b_{a_1}(a_{a_1}(x))) → a_{b_1}(b_{b_1}(b_{a_1}(a_{a_1}(x))))
a_{b_1}(b_{a_1}(a_{b_1}(x))) → a_{b_1}(b_{b_1}(b_{a_1}(a_{b_1}(x))))
b_{b_1}(b_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(x))
b_{b_1}(b_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{b_1}(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.
(6) TRUE