Copy a raw work-tape output

These theorems let TM.copyWorkToWorkTM consume a source satisfying Tape.HasOutput, even when cells after the terminating blank contain arbitrary junk. The fresh destination receives a canonical Tape.HasBinaryPrefix.

Main results

• TM.copyWorkToWorkTM_reachesIn_of_hasOutput — exact concrete copy run
• TM.copyWorkToWorkTM_hoareTime_of_hasOutput — exact raw-output copy
• TM.copyWorkToWorkTM_hoareTime_frame_of_hasOutput — copy with frame preservation

theorem Complexity.TM.copyWorkToWorkTM_reachesIn_of_hasOutput {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

Starting at cell one, copy exactly the source's advertised output in |x| + 1 steps, preserving all source cells and the destination's cell zero.

theorem Complexity.TM.copyWorkToWorkTM_hoareTime_of_hasOutput {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)

Copy a raw HasOutput source to a fresh destination in exactly the usual linear bound. Source cells are preserved, including arbitrary trailing junk.

theorem Complexity.TM.copyWorkToWorkTM_hoareTime_frame_of_hasOutput {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, output, and unrelated work tapes are preserved exactly while the source is copied to the fresh destination.