proposition: Theorem MMA_computable_to_TM_computable k (R : Vector.t nat k -> nat -> Prop) : MMA_computable R -> TM_computable R.
proof: Proof. intros H. apply MMA_mon_computable_to_TM_computable. apply MMA_computable_to_MMA_mon_computable. apply H. Qed.
imports: Undecidability(TM.TM MinskyMachines.MMA) Undecidability(MinskyMachines.Reductions.MMA_computable_to_MMA_mon_computable TM.Reductions.MMA_mon_computable_to_TM_computable)