proposition: Lemma to_nat_toAddress {l instr r} : M = l ++ instr :: r -> sval (Fin.to_nat (toAddress (S (length l)))) = S (length l).
proof: Proof. move=> HM. rewrite /toAddress /=. case: (le_lt_dec maxState (S (length l))). - move: HM => /(f_equal (@length _)). rewrite app_length /=. lia. - move=> ?. by rewrite Fin.to_nat_of_nat. 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