proposition: Lemma stuck_step2I {s s'} : sync s s' -> out_code (fst s) (1, M) -> Sim.stuck step2 s'.
proof: Proof. case => i v bs _ _ /= Hi t' /=. rewrite /halt' /= /toAddress. case: (le_lt_dec maxState i) => /=. { rewrite Nat.eqb_refl => ?. by case. } move=> H'i. have ? : i = 0 by lia. subst i. suff -> : Fin.of_nat_lt H'i = pos0. { rewrite Nat.eqb_refl. by case. } rewrite [RHS](esym (Fin.of_nat_to_nat_inv pos0)). by apply: Fin.of_nat_ext. Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun