proposition: Lemma read_instr {p instr} : (p, [instr]) <sc (1, M) -> exists q, sval (Fin.to_nat (toState p)) = S q /\ nth_error M q = Some instr /\ p = S q.
proof: Proof. rewrite /toState. case: (le_lt_dec maxState p). { move=> ? [?] [?] [/(f_equal (@length _))]. rewrite app_length /=. by lia. } move=> Hp [l] [r] [HM H'p]. exists (length l). by rewrite Fin.to_nat_of_nat /= HM nth_error_app2 ?Nat.sub_diag. Qed.
imports: Undecidability.MinskyMachines(MM MMA.mma_defs) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL.EqDec List Vector Lia PeanoNat Compare_dec ssreflect ssrbool ssrfun