Bounded sparse-entry scan — controller internals

def Complexity.RAM.RegisterStore.Machine.entryScanBodyWrap {n : ℕ} (tapes : EntryScanTapes n) (cfg : Complexity.Cfg n (entryScanStepTM tapes.entry).Q) : Complexity.Cfg n (entryScanTM tapes).Q

Embed an entry-step configuration in the bounded scan controller.

Equations

• Complexity.RAM.RegisterStore.Machine.entryScanBodyWrap tapes cfg = { state := Sum.inr (Sum.inl cfg.state), input := cfg.input, work := cfg.work, output := cfg.output }

def Complexity.RAM.RegisterStore.Machine.entryScanPredWrap {n : ℕ} (tapes : EntryScanTapes n) (cfg : Complexity.Cfg n (TM.binaryPredTM tapes.count).Q) : Complexity.Cfg n (entryScanTM tapes).Q

Embed a binary-predecessor configuration in the bounded scan controller.

Equations

• Complexity.RAM.RegisterStore.Machine.entryScanPredWrap tapes cfg = { state := Sum.inr (Sum.inr cfg.state), input := cfg.input, work := cfg.work, output := cfg.output }

def Complexity.RAM.RegisterStore.Machine.entryScanDoneCfg {n : ℕ} (tapes : EntryScanTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) : Complexity.Cfg n (entryScanTM tapes).Q

Canonical halted controller configuration with the supplied tapes.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryScanTestCfg {n : ℕ} (tapes : EntryScanTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) : Complexity.Cfg n (entryScanTM tapes).Q

Canonical loop-test controller configuration with the supplied tapes.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_body_reachesIn_internal {n : ℕ} (tapes : EntryScanTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (entryScanStepTM tapes.entry).Q} (hreach : (entryScanStepTM tapes.entry).reachesIn time cfg next) : (entryScanTM tapes).reachesIn time (entryScanBodyWrap tapes cfg) (entryScanBodyWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_pred_reachesIn_internal {n : ℕ} (tapes : EntryScanTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (TM.binaryPredTM tapes.count).Q} (hreach : (TM.binaryPredTM tapes.count).reachesIn time cfg next) : (entryScanTM tapes).reachesIn time (entryScanPredWrap tapes cfg) (entryScanPredWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_step_test_zero_internal {n : ℕ} (tapes : EntryScanTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcount : (work tapes.count).read = Γ.blank) (hinput : TM.Parked inp) (hwork : ∀ (i : Fin n), TM.Parked (work i)) (houtput : TM.Parked out) : (entryScanTM tapes).step { state := Sum.inl EntryScanPhase.test, input := inp, work := work, output := out } = some { state := Sum.inl EntryScanPhase.done, input := inp, work := work, output := out }

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_step_test_positive_internal {n : ℕ} (tapes : EntryScanTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hcount : (work tapes.count).read ≠ Γ.blank) (hinput : TM.Parked inp) (hwork : ∀ (i : Fin n), TM.Parked (work i)) (houtput : TM.Parked out) : (entryScanTM tapes).step { state := Sum.inl EntryScanPhase.test, input := inp, work := work, output := out } = some (entryScanBodyWrap tapes { state := (entryScanStepTM tapes.entry).qstart, input := inp, work := work, output := out })

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_step_body_hit_internal {n : ℕ} (tapes : EntryScanTapes n) (cfg : Complexity.Cfg n (entryScanStepTM tapes.entry).Q) (hhalt : (entryScanStepTM tapes.entry).halted cfg) (hresult : (cfg.work tapes.entry.result).read = Γ.one) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryScanTM tapes).step (entryScanBodyWrap tapes cfg) = some (entryScanDoneCfg tapes cfg.input cfg.work cfg.output)

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_step_body_miss_internal {n : ℕ} (tapes : EntryScanTapes n) (cfg : Complexity.Cfg n (entryScanStepTM tapes.entry).Q) (hhalt : (entryScanStepTM tapes.entry).halted cfg) (hresult : (cfg.work tapes.entry.result).read ≠ Γ.one) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryScanTM tapes).step (entryScanBodyWrap tapes cfg) = some (entryScanPredWrap tapes { state := (TM.binaryPredTM tapes.count).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryScanTM_step_pred_halt_internal {n : ℕ} (tapes : EntryScanTapes n) (cfg : Complexity.Cfg n (TM.binaryPredTM tapes.count).Q) (hhalt : (TM.binaryPredTM tapes.count).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryScanTM tapes).step (entryScanPredWrap tapes cfg) = some (entryScanTestCfg tapes cfg.input cfg.work cfg.output)