Straight line halts from regs

theorem straight_line_halts_from_regs {p : Program} (hsl : p.IsStraightLine) (r : Regs) :    ∃ s, Steps p ⟨0, r⟩ s ∧ s.isHalted p ∧ s.pc = p.length := by  suffices h : ∀ s : State, s.pc ≤ p.length → ∃ s', Steps p s s' ∧ s'.pc = p.length by    obtain ⟨s', hsteps, hpc'⟩ := h ⟨0, r⟩ (Nat.zero_le _)    exact ⟨s', hsteps, Nat.le_of_eq hpc'.symm, hpc'⟩  intro s hpc_le  generalize hrem : p.length - s.pc = remaining  induction remaining using Nat.strong_induction_on generalizing s with  | h n ih =>  by_cases hhalted : s.pc ≥ p.length  · grind  · have jmp : ¬p[s.pc].IsJump := by apply hsl; grind    have := Step.of_nonJump (by lia) jmp    grind [Relation.ReflTransGen.head]