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:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
bits(0) → 0
bits(s(x)) → s(bits(half(s(x))))
Q is empty.
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
bits(0) → 0
bits(s(x)) → s(bits(half(s(x))))
Q is empty.
The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
bits(0) → 0
bits(s(x)) → s(bits(half(s(x))))
Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:
bits(0) → 0
Used ordering:
Polynomial interpretation [25]:
POL(0) = 0
POL(bits(x1)) = 2 + x1
POL(half(x1)) = x1
POL(s(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
bits(s(x)) → s(bits(half(s(x))))
Q is empty.
The TRS is overlay and locally confluent. By [19] we can switch to innermost.
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
bits(s(x)) → s(bits(half(s(x))))
The set Q consists of the following terms:
half(0)
half(s(0))
half(s(s(x0)))
bits(s(x0))
We have reversed the following QTRS:
The set of rules R is
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
bits(0) → 0
bits(s(x)) → s(bits(half(s(x))))
The set Q is empty.
We have obtained the following QTRS:
0'(half(x)) → 0'(x)
0'(s(half(x))) → 0'(x)
s(s(half(x))) → half(s(x))
0'(bits(x)) → 0'(x)
s(bits(x)) → s(half(bits(s(x))))
The set Q is empty.
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
0'(half(x)) → 0'(x)
0'(s(half(x))) → 0'(x)
s(s(half(x))) → half(s(x))
0'(bits(x)) → 0'(x)
s(bits(x)) → s(half(bits(s(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:
0'(half(x)) → 0'(x)
0'(s(half(x))) → 0'(x)
s(s(half(x))) → half(s(x))
0'(bits(x)) → 0'(x)
s(bits(x)) → s(half(bits(s(x))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
112, 113, 114, 117, 115, 116, 118, 121, 119, 120
Node 112 is start node and node 113 is final node.
Those nodes are connect through the following edges:
- 112 to 114 labelled half_1(0)
- 112 to 113 labelled 0'_1(0), 0'_1(1)
- 112 to 115 labelled s_1(0)
- 113 to 113 labelled #_1(0)
- 114 to 113 labelled s_1(0)
- 114 to 118 labelled half_1(1)
- 114 to 119 labelled s_1(1)
- 117 to 113 labelled s_1(0)
- 117 to 118 labelled half_1(1)
- 117 to 119 labelled s_1(1)
- 115 to 116 labelled half_1(0)
- 116 to 117 labelled bits_1(0)
- 118 to 113 labelled s_1(1)
- 118 to 118 labelled half_1(1)
- 118 to 119 labelled s_1(1)
- 121 to 113 labelled s_1(1)
- 121 to 118 labelled half_1(1)
- 121 to 119 labelled s_1(1)
- 119 to 120 labelled half_1(1)
- 120 to 121 labelled bits_1(1)