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
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
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
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.
A(a(x1)) → B(a(x1))
The remaining pairs can at least be oriented weakly.
B(a(b(x1))) → A(x1)
A(a(x1)) → A(b(a(x1)))
Used ordering: Polynomial Order [21,25] with Interpretation:
POL( A(x1) ) = x1
POL( c(x1) ) = 0
POL( b(x1) ) = x1
POL( B(x1) ) = max{0, x1 - 1}
POL( a(x1) ) = x1 + 1
The following usable rules [17] were oriented:
a(a(x1)) → a(b(a(x1)))
b(a(b(x1))) → a(c(a(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ 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)))
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
↳ 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.
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
↳ RFCMatchBoundsTRSProof
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.
Termination of the TRS R could be shown with a Match Bound [6,7] of 5. This implies Q-termination of R.
The following rules were used to construct the certificate:
a(a(x)) → a(b(a(x)))
b(a(b(x))) → a(c(a(x)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 115, 114, 117, 116, 118, 119, 121, 120
Node 92 is start node and node 93 is final node.
Those nodes are connect through the following edges:
- 92 to 94 labelled a_1(0)
- 92 to 96 labelled a_1(0)
- 92 to 102 labelled a_1(1)
- 93 to 93 labelled #_1(0)
- 94 to 95 labelled c_1(0)
- 95 to 93 labelled a_1(0)
- 95 to 98 labelled a_1(1)
- 95 to 104 labelled a_1(2)
- 95 to 108 labelled a_1(3)
- 96 to 97 labelled b_1(0)
- 96 to 100 labelled a_1(1)
- 97 to 93 labelled a_1(0)
- 97 to 98 labelled a_1(1)
- 97 to 104 labelled a_1(2)
- 97 to 108 labelled a_1(3)
- 98 to 99 labelled b_1(1)
- 98 to 100 labelled a_1(1)
- 98 to 106 labelled a_1(2)
- 99 to 93 labelled a_1(1)
- 99 to 98 labelled a_1(1)
- 99 to 104 labelled a_1(2)
- 99 to 108 labelled a_1(3)
- 100 to 101 labelled c_1(1)
- 101 to 93 labelled a_1(1)
- 101 to 98 labelled a_1(1)
- 101 to 99 labelled a_1(1)
- 101 to 104 labelled a_1(2)
- 101 to 105 labelled a_1(1)
- 101 to 108 labelled a_1(3)
- 101 to 109 labelled a_1(1)
- 102 to 103 labelled b_1(1)
- 103 to 100 labelled a_1(1)
- 104 to 105 labelled b_1(2)
- 104 to 100 labelled a_1(1)
- 104 to 106 labelled a_1(2)
- 104 to 112 labelled a_1(3)
- 105 to 100 labelled a_1(2)
- 105 to 98 labelled a_1(2), a_1(1)
- 105 to 93 labelled a_1(2)
- 105 to 104 labelled a_1(2)
- 105 to 106 labelled a_1(2)
- 105 to 108 labelled a_1(3), a_1(2)
- 105 to 112 labelled a_1(2)
- 106 to 107 labelled c_1(2)
- 107 to 99 labelled a_1(2)
- 107 to 104 labelled a_1(2)
- 107 to 110 labelled a_1(3)
- 107 to 105 labelled a_1(2)
- 107 to 108 labelled a_1(3)
- 107 to 114 labelled a_1(4)
- 107 to 109 labelled a_1(2)
- 107 to 116 labelled a_1(4)
- 107 to 120 labelled a_1(5)
- 108 to 109 labelled b_1(3)
- 109 to 106 labelled a_1(3)
- 109 to 112 labelled a_1(3)
- 110 to 111 labelled b_1(3)
- 110 to 112 labelled a_1(3)
- 110 to 100 labelled a_1(1)
- 110 to 118 labelled a_1(4)
- 110 to 106 labelled a_1(2)
- 111 to 104 labelled a_1(3), a_1(2)
- 111 to 108 labelled a_1(3)
- 111 to 100 labelled a_1(3)
- 111 to 98 labelled a_1(3), a_1(1)
- 111 to 93 labelled a_1(3)
- 111 to 114 labelled a_1(4)
- 112 to 113 labelled c_1(3)
- 113 to 109 labelled a_1(3)
- 113 to 105 labelled a_1(3)
- 113 to 104 labelled a_1(2)
- 113 to 108 labelled a_1(3)
- 113 to 110 labelled a_1(3)
- 113 to 116 labelled a_1(4)
- 113 to 114 labelled a_1(4)
- 113 to 120 labelled a_1(5)
- 115 to 112 labelled a_1(4)
- 114 to 115 labelled b_1(4)
- 117 to 106 labelled a_1(4)
- 117 to 108 labelled a_1(4)
- 117 to 118 labelled a_1(4)
- 116 to 117 labelled b_1(4)
- 116 to 118 labelled a_1(4)
- 118 to 119 labelled c_1(4)
- 119 to 109 labelled a_1(4)
- 119 to 114 labelled a_1(4)
- 119 to 116 labelled a_1(4)
- 119 to 115 labelled a_1(4)
- 119 to 120 labelled a_1(5)
- 121 to 118 labelled a_1(5)
- 121 to 112 labelled a_1(5)
- 120 to 121 labelled b_1(5)