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