proposition: Fact mm_nat_bound_spec l : Forall (fun x => x < mm_nat_bound l) (mm_linstr_vars l).
proof: Proof. cut (Forall (fun x => x <= lmax (mm_linstr_vars l)) (mm_linstr_vars l)). + apply Forall_impl; intros; unfold mm_nat_bound; lia. + apply lmax_spec; auto. Qed.
imports: List Arith Lia Max Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines(env mm_defs mme_defs mme_utils) Undecidability.MuRec.Util(recalg ra_mm_env)