Structured RAM Hamming-weight program — proof internals

theorem Complexity.RAM.Structured.Hamming.program_measured_internal (bits : List Bool) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore bits) final (stepCount bits) cost space ∧ cost ≤ timeBound bits.length ∧ space ≤ spaceBound bits.length ∧ final lengthReg = weight bits