Shared finite-state word predicates

The nonempty-word transducer is shared by direct Option and unary Degree certificates. Its machine clocks include the whole runtime input; it uses no work tapes.

def Turing.MultiTapeTM.Internal.WordPredicates.nonemptyT : Transducer Bool Bool

Emit a single Boolean indicating whether the input contains a symbol.

theorem Turing.MultiTapeTM.Internal.WordPredicates.nonemptyT_run_true (w : List Bool) : nonemptyT.run true w = []

After the first input symbol, no further output is emitted.