fact: Definition Halt_MM (P : MM_PROBLEM) := match P with existT _ n (existT _ P v) => exists c v', eval (1, P) (1, v) (c, v') end.
imports: Coq(List Lia) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) Undecidability.MinskyMachines.MM