(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(x) → x
a(b(x)) → b(b(c(a(c(x)))))
b(x) → x
c(c(x)) → a(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:
a(x) → x
b(a(x)) → c(a(c(b(b(x)))))
b(x) → x
c(c(x)) → a(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:
B(a(x)) → C(a(c(b(b(x)))))
B(a(x)) → A(c(b(b(x))))
B(a(x)) → C(b(b(x)))
B(a(x)) → B(b(x))
B(a(x)) → B(x)
C(c(x)) → A(x)
The TRS R consists of the following rules:
a(x) → x
b(a(x)) → c(a(c(b(b(x)))))
b(x) → x
c(c(x)) → a(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 1 SCC with 4 less nodes.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
B(a(x)) → B(x)
B(a(x)) → B(b(x))
The TRS R consists of the following rules:
a(x) → x
b(a(x)) → c(a(c(b(b(x)))))
b(x) → x
c(c(x)) → a(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) SemLabProof (SOUND transformation)
We found the following model for the rules of the TRSs R and P.
Interpretation over the domain with elements from 0 to 1.
a: x0
b: x0
c: 1 + x0
B: 0
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
B.0(a.0(x)) → B.0(x)
B.0(a.0(x)) → B.0(b.0(x))
B.1(a.1(x)) → B.1(b.1(x))
B.1(a.1(x)) → B.1(x)
The TRS R consists of the following rules:
a.0(x) → x
a.1(x) → x
b.0(a.0(x)) → c.1(a.1(c.0(b.0(b.0(x)))))
b.1(a.1(x)) → c.0(a.0(c.1(b.1(b.1(x)))))
b.0(x) → x
b.1(x) → x
c.1(c.0(x)) → a.0(x)
c.0(c.1(x)) → a.1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(10) Complex Obligation (AND)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
B.1(a.1(x)) → B.1(x)
B.1(a.1(x)) → B.1(b.1(x))
The TRS R consists of the following rules:
a.0(x) → x
a.1(x) → x
b.0(a.0(x)) → c.1(a.1(c.0(b.0(b.0(x)))))
b.1(a.1(x)) → c.0(a.0(c.1(b.1(b.1(x)))))
b.0(x) → x
b.1(x) → x
c.1(c.0(x)) → a.0(x)
c.0(c.1(x)) → a.1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
B.1(a.1(x)) → B.1(x)
B.1(a.1(x)) → B.1(b.1(x))
The following rules are removed from R:
a.1(x) → x
b.0(a.0(x)) → c.1(a.1(c.0(b.0(b.0(x)))))
b.0(x) → x
c.1(c.0(x)) → a.0(x)
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(B.1(x1)) = x1
POL(a.0(x1)) = x1
POL(a.1(x1)) = 1 + x1
POL(b.1(x1)) = x1
POL(c.0(x1)) = 1 + x1
POL(c.1(x1)) = x1
(13) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
b.1(a.1(x)) → c.0(a.0(c.1(b.1(b.1(x)))))
b.1(x) → x
a.0(x) → x
c.0(c.1(x)) → a.1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(14) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(15) YES
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
B.0(a.0(x)) → B.0(b.0(x))
B.0(a.0(x)) → B.0(x)
The TRS R consists of the following rules:
a.0(x) → x
a.1(x) → x
b.0(a.0(x)) → c.1(a.1(c.0(b.0(b.0(x)))))
b.1(a.1(x)) → c.0(a.0(c.1(b.1(b.1(x)))))
b.0(x) → x
b.1(x) → x
c.1(c.0(x)) → a.0(x)
c.0(c.1(x)) → a.1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(17) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
B.0(a.0(x)) → B.0(b.0(x))
B.0(a.0(x)) → B.0(x)
The following rules are removed from R:
a.0(x) → x
b.1(a.1(x)) → c.0(a.0(c.1(b.1(b.1(x)))))
b.1(x) → x
c.0(c.1(x)) → a.1(x)
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(B.0(x1)) = x1
POL(a.0(x1)) = 1 + x1
POL(a.1(x1)) = x1
POL(b.0(x1)) = x1
POL(c.0(x1)) = x1
POL(c.1(x1)) = 1 + x1
(18) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
b.0(a.0(x)) → c.1(a.1(c.0(b.0(b.0(x)))))
b.0(x) → x
a.1(x) → x
c.1(c.0(x)) → a.0(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(20) YES