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(c(a(b(c(a(a(a(x1))))))))) → a(a(a(a(b(c(a(b(c(a(b(c(x1))))))))))))
Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ Strip Symbols Proof
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(c(a(b(c(a(a(a(x1))))))))) → a(a(a(a(b(c(a(b(c(a(b(c(x1))))))))))))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(b(c(a(b(c(a(a(a(x1))))))))) → a(a(a(a(b(c(a(b(c(a(b(c(x1))))))))))))
The set Q is empty.
We have obtained the following QTRS:
a(a(a(c(b(a(c(b(a(x))))))))) → c(b(a(c(b(a(c(b(a(a(a(a(x))))))))))))
The set Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ Strip Symbols Proof
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(c(b(a(c(b(a(x))))))))) → c(b(a(c(b(a(c(b(a(a(a(a(x))))))))))))
Q is empty.
We were given the following TRS:
a(b(c(a(b(c(a(a(a(x1))))))))) → a(a(a(a(b(c(a(b(c(a(b(c(x1))))))))))))
By stripping symbols from the only rule of the system, we obtained the following TRS:
b(c(a(b(c(a(a(a(x1)))))))) → a(a(a(b(c(a(b(c(a(b(c(x1)))))))))))
↳ QTRS
↳ QTRS Reverse
↳ Strip Symbols Proof
↳ QTRS
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
b(c(a(b(c(a(a(a(x1)))))))) → a(a(a(b(c(a(b(c(a(b(c(x1)))))))))))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(b(c(a(b(c(a(a(a(x1))))))))) → a(a(a(a(b(c(a(b(c(a(b(c(x1))))))))))))
The set Q is empty.
We have obtained the following QTRS:
a(a(a(c(b(a(c(b(a(x))))))))) → c(b(a(c(b(a(c(b(a(a(a(a(x))))))))))))
The set Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ Strip Symbols Proof
↳ QTRS Reverse
↳ QTRS
↳ Strip Symbols Proof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(c(b(a(c(b(a(x))))))))) → c(b(a(c(b(a(c(b(a(a(a(a(x))))))))))))
Q is empty.
We were given the following TRS:
a(a(a(c(b(a(c(b(a(x))))))))) → c(b(a(c(b(a(c(b(a(a(a(a(x))))))))))))
By stripping symbols from the only rule of the system, we obtained the following TRS:
a(a(a(c(b(a(c(b(x)))))))) → c(b(a(c(b(a(c(b(a(a(a(x)))))))))))
↳ QTRS
↳ QTRS Reverse
↳ Strip Symbols Proof
↳ QTRS Reverse
↳ QTRS
↳ Strip Symbols Proof
↳ QTRS
↳ RFCMatchBoundsTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(c(b(a(c(b(x)))))))) → c(b(a(c(b(a(c(b(a(a(a(x)))))))))))
Q is empty.
Termination of the TRS R could be shown with a Match Bound [6,7] of 1. This implies Q-termination of R.
The following rules were used to construct the certificate:
a(a(a(c(b(a(c(b(x)))))))) → c(b(a(c(b(a(c(b(a(a(a(x)))))))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
407, 408, 414, 415, 411, 412, 409, 416, 413, 410, 418, 417, 424, 425, 421, 422, 419, 426, 423, 420, 428, 427
Node 407 is start node and node 408 is final node.
Those nodes are connect through the following edges:
- 407 to 409 labelled c_1(0)
- 408 to 408 labelled #_1(0)
- 414 to 415 labelled c_1(0)
- 415 to 416 labelled b_1(0)
- 411 to 412 labelled c_1(0)
- 412 to 413 labelled b_1(0)
- 409 to 410 labelled b_1(0)
- 416 to 417 labelled a_1(0)
- 416 to 419 labelled c_1(1)
- 413 to 414 labelled a_1(0)
- 410 to 411 labelled a_1(0)
- 418 to 408 labelled a_1(0)
- 418 to 419 labelled c_1(1)
- 417 to 418 labelled a_1(0)
- 417 to 419 labelled c_1(1)
- 424 to 425 labelled c_1(1)
- 425 to 426 labelled b_1(1)
- 421 to 422 labelled c_1(1)
- 422 to 423 labelled b_1(1)
- 419 to 420 labelled b_1(1)
- 426 to 427 labelled a_1(1)
- 426 to 419 labelled c_1(1)
- 423 to 424 labelled a_1(1)
- 420 to 421 labelled a_1(1)
- 428 to 408 labelled a_1(1)
- 428 to 419 labelled c_1(1)
- 427 to 428 labelled a_1(1)
- 427 to 419 labelled c_1(1)