fact: Definition MM_HALTS_ON_ZERO (P : MM_PROBLEM) := match P with existT _ n (existT _ P v) => (1,P) // (1,v) ~~> (0,vec_zero) end.
imports: Coq(List Lia) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) Undecidability.MinskyMachines.MM