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

0 QTRS
↳1 QTRS Reverse (⇔)
↳2 QTRS
↳3 RFCMatchBoundsTRSProof (⇔)
↳4 TRUE

(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:

2941186, 2941187, 2941188, 2941189, 2941190, 2941191, 2941192, 2941194, 2941195, 2941193

Node 2941186 is start node and node 2941187 is final node.

Those nodes are connect through the following edges:

  • 2941186 to 2941188 labelled half_1(0)
  • 2941186 to 2941187 labelled 0'_1(0), 0'_1(1)
  • 2941186 to 2941189 labelled s_1(0)
  • 2941187 to 2941187 labelled #_1(0)
  • 2941188 to 2941187 labelled s_1(0)
  • 2941188 to 2941192 labelled half_1(1)
  • 2941188 to 2941193 labelled s_1(1)
  • 2941189 to 2941190 labelled half_1(0)
  • 2941190 to 2941191 labelled bits_1(0)
  • 2941191 to 2941187 labelled s_1(0)
  • 2941191 to 2941192 labelled half_1(1)
  • 2941191 to 2941193 labelled s_1(1)
  • 2941192 to 2941187 labelled s_1(1)
  • 2941192 to 2941192 labelled half_1(1)
  • 2941192 to 2941193 labelled s_1(1)
  • 2941194 to 2941195 labelled bits_1(1)
  • 2941195 to 2941187 labelled s_1(1)
  • 2941195 to 2941192 labelled half_1(1)
  • 2941195 to 2941193 labelled s_1(1)
  • 2941193 to 2941194 labelled half_1(1)

(4) TRUE