The whole enumerator, in space

⚠️ Unreviewed by Bolton

Five of the machine's six phases are short, and their windows come from their running times; the sixth is the counting loop, whose window is one iteration wide. Composing them is what TM.seqTM_keepsWindowOn is for.

Main results

• PolyExists.afterCopyX_heads — how far the copy phase can leave a head
• PolyExists.enumPark_keepsWindowOn and the other per-phase windows

theorem Complexity.PolyExists.afterCopyX_heads (k : ℕ) (x : List Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : afterCopyX k x inp work out) (i : Fin (enumTapes k)) : (work i).head ≤ x.length + 1

The copy phase leaves every head inside the input's width.

theorem Complexity.PolyExists.copiedBank_head (k : ℕ) (x : List Bool) (i : Fin (enumTapes k)) : (copiedBank k x i).head = 1

theorem Complexity.PolyExists.enumPark_keepsWindowOn (k : ℕ) (x : List Bool) (W : ℕ) (hW : 1 ≤ W) : TM.skipTM.KeepsWindowOn (fun (c : Cfg (enumTapes k) TM.skipTM.Q) => c.state = TM.skipTM.qstart ∧ c.input = Tape.init (List.map Γ.ofBool x) ∧ (c.work = fun (x : Fin (enumTapes k)) => Tape.init []) ∧ c.output = Tape.init []) x.length W

The parking phase's window.

theorem Complexity.PolyExists.copyX_keepsWindowOn (k : ℕ) (x : List Bool) (W : ℕ) (hW : 1 + (x.length + 1) ≤ W) : (TM.copyInputToWorkTM (xIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.copyInputToWorkTM (xIdx k)).Q) => c.state = (TM.copyInputToWorkTM (xIdx k)).qstart ∧ c.input = strTape x ∧ (c.work = fun (x : Fin (enumTapes k)) => TM.blankTape) ∧ c.output = TM.blankTape) x.length W

The input copy's window.

theorem Complexity.PolyExists.rewindX_keepsWindowOn (k : ℕ) (x : List Bool) (B W : ℕ) (hB : x.length + 1 ≤ B) (hW : x.length + 1 + (1 + 1 + (2 * (max (B + 2) (1 * (B + 3) + 1) + 1) + 1)) ≤ W) : (TM.parkRewindTM [xIdx k]).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.parkRewindTM [xIdx k]).Q) => c.state = (TM.parkRewindTM [xIdx k]).qstart ∧ afterCopyX k x c.input c.work c.output) x.length W

The rewind's window.

theorem Complexity.PolyExists.prologue_keepsWindowOn (k : ℕ) (p q : Polynomial ℕ) (x : List Bool) (W : ℕ) (hW : 1 + prologueTime p q x.length ≤ W) : (prologueTM k p q).KeepsWindowOn (fun (c : Cfg (enumTapes k) (prologueTM k p q).Q) => c.state = (prologueTM k p q).qstart ∧ c.input = strTape x ∧ c.work = copiedBank k x ∧ c.output = TM.blankTape) x.length W

The prologue's window.

theorem Complexity.PolyExists.epilogue_keepsWindowOn (k : ℕ) (x : List Bool) (N H A R : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (W : ℕ) (hW : 1 + epilogueTime A ≤ W) : (epilogueTM k).KeepsWindowOn (fun (c : Cfg (enumTapes k) (epilogueTM k).Q) => c.state = (epilogueTM k).qstart ∧ c.input = I ∧ c.work = enumBank k x N H N A R ∧ c.output = NTM.outSlot Γw.one) x.length W

The epilogue's window.

theorem Complexity.PolyExists.enumTM_keepsWindowOn {k : ℕ} (M : TM k) {L' : Language} (p q : Polynomial ℕ) (x : List Bool) (N H A R W : ℕ) (hloopW : ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).KeepsWindowOn (fun (c : Cfg (enumTapes k) ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q) => c.state = ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).qstart ∧ NTM.tallyPre (cIdx k) (aIdx k) (rIdx k) (strTape x) (enumRest k x N H 1) (enumP L' x) 0 c.input c.work c.output) x.length W) {bnd : ℕ} (hloopC : ((bodyTM M).loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).HoareTime (NTM.tallyPre (cIdx k) (aIdx k) (rIdx k) (strTape x) (enumRest k x N H 1) (enumP L' x) 0) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ work = enumBank k x N H N A R ∧ out = NTM.outSlot Γw.one) bnd) (hprologuePost : (prologueTM k p q).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ work = copiedBank k x ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ work = enumBank k x N H 0 0 0 ∧ out = TM.blankTape) (prologueTime p q x.length)) (B : ℕ) (hBx : x.length + 1 ≤ B) (hWpark : 1 ≤ W) (hWcopy : 1 + (x.length + 1) ≤ W) (hWrewind : x.length + 1 + (1 + 1 + (2 * (max (B + 2) (1 * (B + 3) + 1) + 1) + 1)) ≤ W) (hWprol : 1 + prologueTime p q x.length ≤ W) (hWepi : 1 + epilogueTime A ≤ W) (c : Cfg (enumTapes k) (enumTM M p q).Q) : (enumTM M p q).reaches ((enumTM M p q).initCfg x) c → c.WithinDecisionSpace x.length W

The whole machine keeps a window. Five short phases, whose windows come from their running times, and one long loop, whose window is one iteration wide.