A placed machine's window

⚠️ Unreviewed by Bolton

A machine placed in a block of a larger tape space runs exactly as it did, so a window it keeps on its own tapes is a window the placed machine keeps — provided the tapes on either side are inside that window too, which they are: they never move.

Main results

• TM.placeWorkTM_reaches_reflect — every configuration a placed run reaches is a placed one
• TM.placeWorkTM_keepsWindow_of_reaches — and so the source's window transfers

theorem Complexity.TM.placeWorkTM_reaches_reflect {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c₀ : Cfg n tm.Q) (hinv : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → 1 ≤ (extras i).head) (D : Cfg (pre + n + post) (placeWorkTM pre post tm).Q) : (placeWorkTM pre post tm).reaches (tm.placeWorkCfg pre post extras c₀) D → ∃ (c : Cfg n tm.Q), tm.reaches c₀ c ∧ D = tm.placeWorkCfg pre post extras c

Every configuration a placed run reaches is a placed configuration. The frame never changes, so the run is the source's run under the embedding.

theorem Complexity.TM.placeWorkTM_keepsWindow_of_reaches {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c₀ : Cfg n tm.Q) (hinv : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → 1 ≤ (extras i).head) {inputLength space : ℕ} (hextraW : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).head ≤ space) (htm : ∀ (c : Cfg n tm.Q), tm.reaches c₀ c → c.WithinDecisionSpace inputLength space) (D : Cfg (pre + n + post) (placeWorkTM pre post tm).Q) : (placeWorkTM pre post tm).reaches (tm.placeWorkCfg pre post extras c₀) D → D.WithinDecisionSpace inputLength space

A placed machine keeps its source's window, given that the tapes on either side sit inside it.