Input length into a register

inputLenRegTM q scans the input tape in lockstep with register q, writing one mark per input bit, then rewinds both heads to cell 1: from the bumped initial configuration it puts regTape |x| in register q, restoring the input tape exactly. This is the reduction emitter's only input-reading machine besides the start-clause emitter, and the last hand-rolled machine of the campaign (docs/A5-ReductionEmitter.md).

def Complexity.TM.inputLenRegTM {n : ℕ} (q : Fin n) : TM n

Measure the input length into register q: lockstep scan right over the input bits writing marks, then lockstep rewind.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.inputLenRegTM_hoareTime {n : ℕ} (q : Fin n) (x : List Bool) (work₀ : Fin n → Tape) (ys : List Bool) (hwork₀ : ∀ (i : Fin n), i ≠ q → Parked (work₀ i)) (hq : work₀ q = regTape 0) : (inputLenRegTM q).HoareTime (EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } work₀ ys) (EmitPred { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } (Function.update work₀ q (regTape x.length)) ys) (2 * x.length + 4)

inputLenRegTM Hoare specification. From the bumped initial input and regTape 0 in q, reach regTape |x| in q, restoring the input exactly.