Right-scanner correctness

Exact simulation proof for TM.scanRightTM. A target work tape containing a completed binary string is scanned from cell one to its first append blank in |bits| + 1 steps. The input tape, output tape, and every unrelated work tape are preserved exactly when their heads read a non-▷ symbol.

The public compositional theorem is stated in Complexitylib.Models.TuringMachine.Subroutines.ScanRight.

Exact scanner steps

Exact scan loop

theorem Complexity.TM.scanRightTM_reachesIn_frame_internal {n : ℕ} (idx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hstring : (work₀ idx).HasBinaryString bits) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (scanRightTM idx).Q), (scanRightTM idx).reachesIn (bits.length + 1) { state := (scanRightTM idx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (scanRightTM idx).halted c' ∧ c'.input = inp₀ ∧ (∀ (i : Fin n), i ≠ idx → c'.work i = work₀ i) ∧ (c'.work idx).cells = (work₀ idx).cells ∧ (c'.work idx).HasBinaryPrefix bits ∧ c'.output = out₀

Internal proof of the public exact frame-preserving scanner endpoint. The run uses one transition per bit and one transition on the append blank.

theorem Complexity.TM.scanRightTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hstring : (work₀ idx).HasBinaryString bits) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (scanRightTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).HasBinaryPrefix bits ∧ out = out₀) (bits.length + 1)

Internal proof of the public frame-preserving bounded scanner contract.