fact: Definition MMA_computable {k} (R : Vector.t nat k -> nat -> Prop) := exists n : nat, exists P : list (mm_instr (Fin.t (1 + k + n))), forall v : Vector.t nat k, (forall m, R v m <-> exists c (v' : Vector.t nat (k + n)), (1, P) // (1, (0 :: v) ++ (Vector.const 0 n)) ~~> (c, m :: v')).
imports: Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) Undecidability.MinskyMachines.MM Vector