YES
0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 RFCMatchBoundsTRSProof (⇔, 0 ms)
↳4 YES
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))))
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))))
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 consists of the following enumerated nodes:
2, 4, 6, 7, 8, 9, 14, 15, 16, 17
Node 2 is start node and node 4 is final node.
Those nodes are connected through the following edges: