Copy a raw work-tape output — proof internals

Tape.HasOutput deliberately leaves cells after the terminating blank unconstrained. This module proves that TM.copyWorkToWorkTM nevertheless copies such an output to a fresh work tape: it reads only the advertised bits and their first blank delimiter.

Public statements are in Complexitylib.Models.TuringMachine.Subroutines.CopyWorkOutput.

Exact copy loop

Hoare specification

theorem Complexity.TM.copyWorkToWorkTM_reachesIn_of_hasOutput_internal {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) {inp out : Tape} {work : Fin n → Tape} (hsrcHead : (work src).head = 1) (hsrcOutput : (work src).HasOutput x) (hdst : (work dst).HasBinaryPrefix []) : ∃ (c' : Cfg n (copyWorkToWorkTM src dst).Q), (copyWorkToWorkTM src dst).reachesIn (x.length + 1) { state := (copyWorkToWorkTM src dst).qstart, input := inp, work := work, output := out } c' ∧ (copyWorkToWorkTM src dst).halted c' ∧ (c'.work src).cells = (work src).cells ∧ (c'.work src).head = x.length + 1 ∧ (c'.work src).HasOutput x ∧ (c'.work dst).HasBinaryPrefix x ∧ (c'.work dst).cells 0 = (work dst).cells 0

Exact raw-output copy from a concrete tape configuration.

theorem Complexity.TM.copyWorkToWorkTM_hoareTime_of_hasOutput_internal {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) (source : Tape) : (copyWorkToWorkTM src dst).HoareTime (fun (_inp : Tape) (work : Fin n → Tape) (_out : Tape) => work src = source ∧ source.head = 1 ∧ source.HasOutput x ∧ (work dst).HasBinaryPrefix []) (fun (_inp : Tape) (work : Fin n → Tape) (_out : Tape) => (work src).cells = source.cells ∧ (work src).head = x.length + 1 ∧ (work src).HasOutput x ∧ (work dst).HasBinaryPrefix x) (x.length + 1)

A raw HasOutput source is copied exactly through its first blank. Arbitrary source cells after that delimiter are preserved and ignored.

Exact frame preservation

theorem Complexity.TM.copyWorkToWorkTM_hoareTime_frame_of_hasOutput_internal {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) (source : Tape) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → (work' src).cells = source.cells → (work' src).head = x.length + 1 → (work' src).HasOutput x → (work' dst).HasBinaryPrefix x → (work' dst).cells 0 = Γ.start → inp' = inp → out' = out → (∀ (i : Fin n), i ≠ src → i ≠ dst → work' i = work i) → P inp' work' out') : (copyWorkToWorkTM src dst).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => work src = source ∧ source.head = 1 ∧ source.HasOutput x ∧ work dst = (Tape.init []).move Dir3.right ∧ inp.read ≠ Γ.start ∧ out.read ≠ Γ.start ∧ 1 ≤ out.head ∧ (∀ (i : Fin n), i ≠ src → i ≠ dst → (work i).read ≠ Γ.start ∧ 1 ≤ (work i).head) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => (work src).cells = source.cells ∧ (work src).head = x.length + 1 ∧ (work src).HasOutput x ∧ (work dst).HasBinaryPrefix x ∧ (work dst).cells 0 = Γ.start ∧ P inp work out) (x.length + 1)

Frame-rich raw-output copy. The input tape, output tape, and unrelated work tapes are preserved exactly, allowing an arbitrary predicate to be threaded through the copy.