Step to Standard Form

theorem Step.toStandardForm {p : Program} {s s' : State} (hstep : Step p s s') :    Step p.toStandardForm s s' ∨    (s'.isHalted p ∧ ∃ s₂, Step p.toStandardForm s s₂ ∧      s₂.isHalted p.toStandardForm ∧ s'.regs = s₂.regs) := by  cases hstep with  | zero hinstr =>    left    exact Step.zero (by simp [Program.getElem?_toStandardForm, hinstr])  | succ hinstr =>    left    exact Step.succ (by simp [Program.getElem?_toStandardForm, hinstr])  | transfer hinstr =>    left    exact Step.transfer (by simp [Program.getElem?_toStandardForm, hinstr])  | @jump_ne m n q hinstr hne =>    left    have hcap : p.toStandardForm[s.pc]? = some (Instr.J m n (min q p.length)) := by      simp [Program.getElem?_toStandardForm, hinstr]    exact Step.jump_ne hcap hne  | @jump_eq m n q hinstr heq =>    have (x : ℕ) (h : min q p.length = x) : p.toStandardForm[s.pc]? = some (Instr.J m n x) := by      grind [Program.getElem?_toStandardForm, Instr.capJump]    by_cases q ≤ p.length    · grind [Step.jump_eq]    · right      split_ands      · grind [State.isHalted]      · use ⟨p.length, s.regs⟩        grind [State.isHalted, Program.toStandardForm_length]