One-prefix work-tape loop combinator

TM.forWorkOnesTM driverIdx body consumes a consecutive prefix of 1 symbols from a work tape and invokes body once per symbol. It halts on the first non-1 without consuming it. This is the concrete unary-width driver used by the RAM snapshot word decoder.

Main results

• TM.ForWorkOnesLoopSpec.reachesIn composes an indexed exact-execution certificate for the full loop.
• TM.IsTransducer.forWorkOnesTM preserves one-way output safety.

theorem Complexity.TM.ForWorkOnesLoopSpec.reachesIn {n : ℕ} {driverIdx : Fin n} {body : TM n} {bodyTime : ℕ → ℕ} {total count value : ℕ} (spec : ForWorkOnesLoopSpec driverIdx body bodyTime total) (htotal : value + count = total) : (forWorkOnesTM driverIdx body).reachesIn (forWorkOnesLoopTime bodyTime value count) (spec.scanCfg value) spec.doneCfg

Exact remaining execution of a certified consecutive-one work loop.

theorem Complexity.TM.IsTransducer.forWorkOnesTM {n : ℕ} {driverIdx : Fin n} {body : TM n} (hbody : body.IsTransducer) : (TM.forWorkOnesTM driverIdx body).IsTransducer

Iterating a one-way-output body over a one-prefix remains a transducer.