Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
B(a(b(x1))) → A(x1)
A(a(x1)) → A(b(a(x1)))
B(a(b(x1))) → A(c(a(x1)))
A(a(x1)) → B(a(x1))
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B(a(b(x1))) → A(x1)
A(a(x1)) → A(b(a(x1)))
B(a(b(x1))) → A(c(a(x1)))
A(a(x1)) → B(a(x1))
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B(a(b(x1))) → A(x1)
A(a(x1)) → A(b(a(x1)))
A(a(x1)) → B(a(x1))
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
B(a(b(x1))) → A(x1)
The remaining pairs can at least be oriented weakly.
A(a(x1)) → A(b(a(x1)))
A(a(x1)) → B(a(x1))
Used ordering: Polynomial Order [21,25] with Interpretation:
POL( A(x1) ) = x1 + 1
POL( c(x1) ) = max{0, -1}
POL( b(x1) ) = x1
POL( B(x1) ) = x1 + 1
POL( a(x1) ) = x1 + 1
The following usable rules [17] were oriented:
b(a(b(x1))) → a(c(a(x1)))
a(a(x1)) → a(b(a(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(a(x1)) → A(b(a(x1)))
A(a(x1)) → B(a(x1))
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RFCMatchBoundsDPProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(a(x1)) → A(b(a(x1)))
The TRS R consists of the following rules:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 5.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
A(a(x1)) → A(b(a(x1)))
To find matches we regarded all rules of R and P:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
A(a(x1)) → A(b(a(x1)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 201, 200, 203, 202, 204, 205, 207, 206
Node 180 is start node and node 181 is final node.
Those nodes are connect through the following edges:
- 180 to 182 labelled A_1(0)
- 180 to 188 labelled A_1(1)
- 181 to 181 labelled #_1(0)
- 182 to 183 labelled b_1(0)
- 182 to 186 labelled a_1(1)
- 183 to 181 labelled a_1(0)
- 183 to 184 labelled a_1(1)
- 183 to 190 labelled a_1(2)
- 183 to 194 labelled a_1(3)
- 184 to 185 labelled b_1(1)
- 184 to 186 labelled a_1(1)
- 184 to 192 labelled a_1(2)
- 185 to 181 labelled a_1(1)
- 185 to 184 labelled a_1(1)
- 185 to 190 labelled a_1(2)
- 185 to 194 labelled a_1(3)
- 186 to 187 labelled c_1(1)
- 187 to 181 labelled a_1(1)
- 187 to 184 labelled a_1(1)
- 187 to 185 labelled a_1(1)
- 187 to 190 labelled a_1(2)
- 187 to 191 labelled a_1(1)
- 187 to 194 labelled a_1(3)
- 187 to 195 labelled a_1(1)
- 188 to 189 labelled b_1(1)
- 189 to 186 labelled a_1(1)
- 190 to 191 labelled b_1(2)
- 190 to 186 labelled a_1(1)
- 190 to 192 labelled a_1(2)
- 190 to 198 labelled a_1(3)
- 191 to 186 labelled a_1(2)
- 191 to 184 labelled a_1(2), a_1(1)
- 191 to 181 labelled a_1(2)
- 191 to 190 labelled a_1(2)
- 191 to 192 labelled a_1(2)
- 191 to 194 labelled a_1(3), a_1(2)
- 191 to 198 labelled a_1(2)
- 192 to 193 labelled c_1(2)
- 193 to 185 labelled a_1(2)
- 193 to 190 labelled a_1(2)
- 193 to 196 labelled a_1(3)
- 193 to 191 labelled a_1(2)
- 193 to 194 labelled a_1(3)
- 193 to 200 labelled a_1(4)
- 193 to 195 labelled a_1(2)
- 193 to 202 labelled a_1(4)
- 193 to 206 labelled a_1(5)
- 194 to 195 labelled b_1(3)
- 195 to 192 labelled a_1(3)
- 195 to 198 labelled a_1(3)
- 196 to 197 labelled b_1(3)
- 196 to 198 labelled a_1(3)
- 196 to 186 labelled a_1(1)
- 196 to 204 labelled a_1(4)
- 196 to 192 labelled a_1(2)
- 197 to 190 labelled a_1(3), a_1(2)
- 197 to 194 labelled a_1(3)
- 197 to 186 labelled a_1(3)
- 197 to 184 labelled a_1(3), a_1(1)
- 197 to 181 labelled a_1(3)
- 197 to 200 labelled a_1(4)
- 198 to 199 labelled c_1(3)
- 199 to 195 labelled a_1(3)
- 199 to 191 labelled a_1(3)
- 199 to 190 labelled a_1(2)
- 199 to 194 labelled a_1(3)
- 199 to 196 labelled a_1(3)
- 199 to 202 labelled a_1(4)
- 199 to 200 labelled a_1(4)
- 199 to 206 labelled a_1(5)
- 201 to 198 labelled a_1(4)
- 200 to 201 labelled b_1(4)
- 203 to 192 labelled a_1(4)
- 203 to 194 labelled a_1(4)
- 203 to 204 labelled a_1(4)
- 202 to 203 labelled b_1(4)
- 202 to 204 labelled a_1(4)
- 204 to 205 labelled c_1(4)
- 205 to 195 labelled a_1(4)
- 205 to 200 labelled a_1(4)
- 205 to 202 labelled a_1(4)
- 205 to 201 labelled a_1(4)
- 205 to 206 labelled a_1(5)
- 207 to 204 labelled a_1(5)
- 207 to 198 labelled a_1(5)
- 206 to 207 labelled b_1(5)
We have reversed the following QTRS:
The set of rules R is
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
The set Q is empty.
We have obtained the following QTRS:
a(a(x)) → a(b(a(x)))
b(a(b(x))) → a(c(a(x)))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(x)) → a(b(a(x)))
b(a(b(x))) → a(c(a(x)))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
The set Q is empty.
We have obtained the following QTRS:
a(a(x)) → a(b(a(x)))
b(a(b(x))) → a(c(a(x)))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(x)) → a(b(a(x)))
b(a(b(x))) → a(c(a(x)))
Q is empty.