Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

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.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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.

(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] 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:

912685, 912686, 912687, 912689, 912690, 912688, 912691, 912694, 912692, 912693

Node 912685 is start node and node 912686 is final node.

Those nodes are connect through the following edges:

• 912685 to 912687 labelled half_1(0)
• 912685 to 912686 labelled 0'_1(0), 0'_1(1)
• 912685 to 912688 labelled s_1(0)
• 912686 to 912686 labelled #_1(0)
• 912687 to 912686 labelled s_1(0)
• 912687 to 912691 labelled half_1(1)
• 912687 to 912692 labelled s_1(1)
• 912689 to 912690 labelled bits_1(0)
• 912690 to 912686 labelled s_1(0)
• 912690 to 912691 labelled half_1(1)
• 912690 to 912692 labelled s_1(1)
• 912688 to 912689 labelled half_1(0)
• 912691 to 912686 labelled s_1(1)
• 912691 to 912691 labelled half_1(1)
• 912691 to 912692 labelled s_1(1)
• 912694 to 912686 labelled s_1(1)
• 912694 to 912691 labelled half_1(1)
• 912694 to 912692 labelled s_1(1)
• 912692 to 912693 labelled half_1(1)
• 912693 to 912694 labelled bits_1(1)

(4) TRUE