Is Halted iff normal

theorem isHalted_iff_normal {p : Program} {s : State} :    s.isHalted p ↔ Relation.Normal (Step p) s := by  constructor  · intro hhalted ⟨s', hstep⟩    exact Step.no_step_of_halted hhalted hstep  · intro hnormal    -- If not halted, then p[s.pc]? = some instr for some instruction    by_contra hnothalted    simp only [State.isHalted, not_le] at hnothalted    have hlt : s.pc < p.length := hnothalted    have hinstr : p[s.pc]? = some p[s.pc] := List.getElem?_eq_getElem hlt    -- Any instruction can step, contradicting hnormal    cases hp : p[s.pc] with    | Z n => exact hnormal ⟨_, Step.zero (hp ▸ hinstr)⟩    | S n => exact hnormal ⟨_, Step.succ (hp ▸ hinstr)⟩    | T m n => exact hnormal ⟨_, Step.transfer (hp ▸ hinstr)⟩    | J m n q =>      by_cases heq : s.regs.read m = s.regs.read n      · exact hnormal ⟨_, Step.jump_eq (hp ▸ hinstr) heq⟩      · exact hnormal ⟨_, Step.jump_ne (hp ▸ hinstr) heq⟩