Binary-counter certificates

The binary counter Cslib.BitString.increment is realized by a two-state transducer. Its degree and polynomial-time certificates support polynomial-space enumeration; the plain polynomial-space calculus is in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain.

Main results

• Turing.MultiTapeTM.ComputableTidilyInDegree.increment: the binary counter in linear time.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.increment: the binary counter in polynomial time.

The binary counter

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.increment : ComputableTidilyInDegree Cslib.BitString.increment encBits encBits 1 1

The binary counter in linear time.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.increment : ComputableTidilyInPolyTime Cslib.BitString.increment encBits encBits

The binary counter in polynomial time.