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(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(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:
A(b(a(x1))) → A(b(b(a(x1))))
A(b(a(x1))) → B(b(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(x1))))
A(b(a(x1))) → B(b(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(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
↳ RFCMatchBoundsDPProof
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(x1))))
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(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 1.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
A(b(a(x1))) → A(b(b(a(x1))))
To find matches we regarded all rules of R and P:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
A(b(a(x1))) → A(b(b(a(x1))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
71, 72, 74, 75, 73, 77, 78, 76
Node 71 is start node and node 72 is final node.
Those nodes are connect through the following edges:
- 71 to 73 labelled A_1(0)
- 72 to 72 labelled #_1(0)
- 74 to 75 labelled b_1(0)
- 75 to 72 labelled a_1(0)
- 75 to 76 labelled a_1(1)
- 73 to 74 labelled b_1(0)
- 77 to 78 labelled b_1(1)
- 78 to 72 labelled a_1(1)
- 78 to 76 labelled a_1(1)
- 76 to 77 labelled b_1(1)