Finite numeric structured-RAM switches -- proof internals #
theorem
Complexity.RAM.Structured.Switch.select_exec_internal
{count test one : ℕ}
(branch : Fin count → Cmd)
(initial final : Store)
{code branchSteps : ℕ}
(hcode : code < count)
(htest : initial test = code)
(hone : initial one = 1)
(hne : test ≠ one)
(hbranch : ∃ (cost : ℕ) (space : ℕ), Exec (branch ⟨code, hcode⟩) (cleared initial test) final branchSteps cost space)
:
theorem
Complexity.RAM.Structured.Switch.select_measured_internal
{count test one indexBound valueBound : ℕ}
(branch : Fin count → Cmd)
(initial final : Store)
{code branchSteps branchCost : ℕ}
(hcode : code < count)
(htest : initial test = code)
(hone : initial one = 1)
(hne : test ≠ one)
(htestIndex : test < indexBound)
(hinitial : Internal.StoreEnvelope indexBound valueBound initial)
(hbranch :
Internal.MeasuredRuns (branch ⟨code, hcode⟩) (cleared initial test) final branchSteps branchCost
(Internal.envelopeSpace indexBound valueBound))
:
Internal.MeasuredRuns (select count test one branch) initial final (stepCount code branchSteps)
(costBound code branchCost (Internal.valueWidth valueBound)) (Internal.envelopeSpace indexBound valueBound)