proposition: Theorem L_computable_to_MMA_computable {k} (R : Vector.t nat k -> nat -> Prop) : L_computable R -> MMA_computable R.
proof: Proof. move=> /L_computable_can_closed. by apply: L_computable_closed_to_MMA_computable. Qed.
imports: Undecidability(MinskyMachines.MMA L.L) Undecidability(MinskyMachines.Reductions.L_computable_closed_to_MMA_computable L.Util.ClosedLAdmissible) ssreflect ssrbool ssrfun