proposition: Lemma mm2_stop_index_iff {P: list mm2_instr} {x} : mm2_stop P x <-> fst x = 0 \/ length P < fst x.
proof: Proof. split. - move: x => [[|i] [a b]] /=; [lia|]. move=> H. suff: not (i < length P) by lia. move=> /nth_error_Some. move Hinstr: (nth_error P i) => [instr|]; [|done]. move=> /nth_error_Some_mm2_instr_at_iff in Hinstr. have [y Hy] := @mm2_progress instr (S i, (a, b)). move=> _. apply: (H y). by exists instr. - move=> Hx y Hxy. case: Hxy Hx. move=> ? [/mm2_instr_at_bounds]. lia. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun