proposition: Lemma in_out_code_halt (p : nat) : if halt' (toState p) then out_code p (1, M) else in_code p (1, M).
proof: Proof. rewrite /halt' /toState. case: (le_lt_dec maxState p). { move=> ? /=. rewrite Nat.eqb_refl. by lia. } move: p => [|p] ? /=; rewrite ?Nat.eqb_refl; by lia. 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