Shared unary machine constructors

The finite-state successor machine is shared by direct Degree and polynomial-time providers. Extracted unchanged from the direct list provider by worker /root/review_560.

def Turing.MultiTapeTM.Internal.Unary.unarySuccTransducer : Transducer Bool Bool

Prefix a unary symbol, including on empty input.

theorem Turing.MultiTapeTM.Internal.Unary.unarySuccRun (word : List Bool) : unarySuccTransducer.run true word = true :: word ∧ unarySuccTransducer.run false word = word

The successor transducer prefixes once, then copies every remaining symbol.