Finite-state structured RAM scanners — proof internals

theorem Complexity.RAM.Structured.Scanner.program_measured_internal (spec : Spec) (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec (program spec) (inputStore spec bits) final (stepCount spec bits.length) cost space ∧ cost ≤ timeBound spec bits.length ∧ space ≤ spaceBound spec bits.length ∧ final lengthReg = Input.bitValue (spec.accept (List.foldl spec.step spec.initial bits))

theorem Complexity.RAM.Structured.Scanner.typed_program_measured_internal {State : Type} [FinEnum State] (typed : TypedSpec State) (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec (program typed.numeric) (inputStore typed.numeric bits) final (stepCount typed.numeric bits.length) cost space ∧ cost ≤ timeBound typed.numeric bits.length ∧ space ≤ spaceBound typed.numeric bits.length ∧ final lengthReg = Input.bitValue (typed.accept (List.foldl typed.step typed.initial bits))