Bounded encoded sparse-store update — controller internals

def Complexity.RAM.RegisterStore.Machine.entryUpdateMatchWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMatchReadTM tapes.entry).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed a match configuration in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateMissWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMissCopyTM tapes.entry).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed a miss-copy configuration in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateDeleteWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMissCleanupTM tapes.entry).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed a deletion-cleanup configuration in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateReplaceWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryReplaceCleanupTM tapes.replace).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed a replacement configuration in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateAppendWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryAppendRestoreTM tapes.replace).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed a final-append configuration in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateRemainingWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (TM.binaryPredTM tapes.remaining).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed the remaining-count predecessor in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateDeleteCountWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (TM.binaryPredTM tapes.resultCount).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed the deletion result-count predecessor in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateAppendCountWrap {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (TM.binarySuccTM tapes.resultCount).Q) : Complexity.Cfg n (entryUpdateTM tapes).Q

Embed the append result-count successor in the update controller.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryUpdateTestCfg {n : ℕ} (tapes : EntryUpdateTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) : Complexity.Cfg n (entryUpdateTM tapes).Q

Canonical loop-test controller configuration.

Equations

• Complexity.RAM.RegisterStore.Machine.entryUpdateTestCfg tapes inp work out = { state := Complexity.RAM.RegisterStore.Machine.EntryUpdateQ.test, input := inp, work := work, output := out }

def Complexity.RAM.RegisterStore.Machine.entryUpdateDoneCfg {n : ℕ} (tapes : EntryUpdateTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) : Complexity.Cfg n (entryUpdateTM tapes).Q

Canonical halted update-controller configuration.

Equations

• Complexity.RAM.RegisterStore.Machine.entryUpdateDoneCfg tapes inp work out = { state := Complexity.RAM.RegisterStore.Machine.EntryUpdateQ.done, input := inp, work := work, output := out }

def Complexity.RAM.RegisterStore.Machine.entryUpdateMarkFoundWork {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) : Fin n → Tape

Work family after the hit-dispatch transition records a match.

Equations

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

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_match_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (entryMatchReadTM tapes.entry).Q} (hreach : (entryMatchReadTM tapes.entry).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateMatchWrap tapes cfg) (entryUpdateMatchWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_miss_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (entryMissCopyTM tapes.entry).Q} (hreach : (entryMissCopyTM tapes.entry).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateMissWrap tapes cfg) (entryUpdateMissWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_delete_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (entryMissCleanupTM tapes.entry).Q} (hreach : (entryMissCleanupTM tapes.entry).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateDeleteWrap tapes cfg) (entryUpdateDeleteWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_replace_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (entryReplaceCleanupTM tapes.replace).Q} (hreach : (entryReplaceCleanupTM tapes.replace).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateReplaceWrap tapes cfg) (entryUpdateReplaceWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_append_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (entryAppendRestoreTM tapes.replace).Q} (hreach : (entryAppendRestoreTM tapes.replace).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateAppendWrap tapes cfg) (entryUpdateAppendWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_remaining_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (TM.binaryPredTM tapes.remaining).Q} (hreach : (TM.binaryPredTM tapes.remaining).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateRemainingWrap tapes cfg) (entryUpdateRemainingWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_deleteCount_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (TM.binaryPredTM tapes.resultCount).Q} (hreach : (TM.binaryPredTM tapes.resultCount).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateDeleteCountWrap tapes cfg) (entryUpdateDeleteCountWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_appendCount_reachesIn_internal {n : ℕ} (tapes : EntryUpdateTapes n) {time : ℕ} {cfg next : Complexity.Cfg n (TM.binarySuccTM tapes.resultCount).Q} (hreach : (TM.binarySuccTM tapes.resultCount).reachesIn time cfg next) : (entryUpdateTM tapes).reachesIn time (entryUpdateAppendCountWrap tapes cfg) (entryUpdateAppendCountWrap tapes next)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_test_continue_internal {n : ℕ} (tapes : EntryUpdateTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hremaining : (work tapes.remaining).read ≠ Γ.blank) (hinput : TM.Parked inp) (hwork : ∀ (i : Fin n), TM.Parked (work i)) (houtput : TM.Parked out) : (entryUpdateTM tapes).step (entryUpdateTestCfg tapes inp work out) = some (entryUpdateMatchWrap tapes { state := (entryMatchReadTM tapes.entry).qstart, input := inp, work := work, output := out })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_test_found_internal {n : ℕ} (tapes : EntryUpdateTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hremaining : (work tapes.remaining).read = Γ.blank) (hfound : (work tapes.found).read = Γ.one) (hinput : TM.Parked inp) (hwork : ∀ (i : Fin n), TM.Parked (work i)) (houtput : TM.Parked out) : (entryUpdateTM tapes).step (entryUpdateTestCfg tapes inp work out) = some (entryUpdateDoneCfg tapes inp work out)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_test_zero_internal {n : ℕ} (tapes : EntryUpdateTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hremaining : (work tapes.remaining).read = Γ.blank) (hfound : (work tapes.found).read ≠ Γ.one) (hreplacement : (work tapes.replacement).read = Γ.blank) (hinput : TM.Parked inp) (hwork : ∀ (i : Fin n), TM.Parked (work i)) (houtput : TM.Parked out) : (entryUpdateTM tapes).step (entryUpdateTestCfg tapes inp work out) = some (entryUpdateDoneCfg tapes inp work out)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_test_append_internal {n : ℕ} (tapes : EntryUpdateTapes n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hremaining : (work tapes.remaining).read = Γ.blank) (hfound : (work tapes.found).read ≠ Γ.one) (hreplacement : (work tapes.replacement).read ≠ Γ.blank) (hinput : TM.Parked inp) (hwork : ∀ (i : Fin n), TM.Parked (work i)) (houtput : TM.Parked out) : (entryUpdateTM tapes).step (entryUpdateTestCfg tapes inp work out) = some (entryUpdateAppendWrap tapes { state := (entryAppendRestoreTM tapes.replace).qstart, input := inp, work := work, output := out })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_match_delete_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMatchReadTM tapes.entry).Q) (hhalt : (entryMatchReadTM tapes.entry).halted cfg) (hresult : (cfg.work tapes.entry.result).read = Γ.one) (hreplacement : (cfg.work tapes.replacement).read = Γ.blank) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateMatchWrap tapes cfg) = some (entryUpdateDeleteWrap tapes { state := (entryMissCleanupTM tapes.entry).qstart, input := cfg.input, work := entryUpdateMarkFoundWork tapes cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_match_replace_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMatchReadTM tapes.entry).Q) (hhalt : (entryMatchReadTM tapes.entry).halted cfg) (hresult : (cfg.work tapes.entry.result).read = Γ.one) (hreplacement : (cfg.work tapes.replacement).read ≠ Γ.blank) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateMatchWrap tapes cfg) = some (entryUpdateReplaceWrap tapes { state := (entryReplaceCleanupTM tapes.replace).qstart, input := cfg.input, work := entryUpdateMarkFoundWork tapes cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_match_miss_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMatchReadTM tapes.entry).Q) (hhalt : (entryMatchReadTM 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) : (entryUpdateTM tapes).step (entryUpdateMatchWrap tapes cfg) = some (entryUpdateMissWrap tapes { state := (entryMissCopyTM tapes.entry).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_miss_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMissCopyTM tapes.entry).Q) (hhalt : (entryMissCopyTM tapes.entry).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateMissWrap tapes cfg) = some (entryUpdateRemainingWrap tapes { state := (TM.binaryPredTM tapes.remaining).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_delete_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryMissCleanupTM tapes.entry).Q) (hhalt : (entryMissCleanupTM tapes.entry).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateDeleteWrap tapes cfg) = some (entryUpdateDeleteCountWrap tapes { state := (TM.binaryPredTM tapes.resultCount).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_replace_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryReplaceCleanupTM tapes.replace).Q) (hhalt : (entryReplaceCleanupTM tapes.replace).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateReplaceWrap tapes cfg) = some (entryUpdateRemainingWrap tapes { state := (TM.binaryPredTM tapes.remaining).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_append_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (entryAppendRestoreTM tapes.replace).Q) (hhalt : (entryAppendRestoreTM tapes.replace).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateAppendWrap tapes cfg) = some (entryUpdateAppendCountWrap tapes { state := (TM.binarySuccTM tapes.resultCount).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_remaining_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (TM.binaryPredTM tapes.remaining).Q) (hhalt : (TM.binaryPredTM tapes.remaining).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateRemainingWrap tapes cfg) = some (entryUpdateTestCfg tapes cfg.input cfg.work cfg.output)

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_deleteCount_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (TM.binaryPredTM tapes.resultCount).Q) (hhalt : (TM.binaryPredTM tapes.resultCount).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateDeleteCountWrap tapes cfg) = some (entryUpdateRemainingWrap tapes { state := (TM.binaryPredTM tapes.remaining).qstart, input := cfg.input, work := cfg.work, output := cfg.output })

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_step_appendCount_halt_internal {n : ℕ} (tapes : EntryUpdateTapes n) (cfg : Complexity.Cfg n (TM.binarySuccTM tapes.resultCount).Q) (hhalt : (TM.binarySuccTM tapes.resultCount).halted cfg) (hinput : TM.Parked cfg.input) (hwork : ∀ (i : Fin n), TM.Parked (cfg.work i)) (houtput : TM.Parked cfg.output) : (entryUpdateTM tapes).step (entryUpdateAppendCountWrap tapes cfg) = some (entryUpdateDoneCfg tapes cfg.input cfg.work cfg.output)