proposition: Lemma L_computable_to_TM_computable k (R : Vector.t nat k -> nat -> Prop) : L_computable R -> TM_computable R.
proof: Proof. intros H. apply MMA_mon_computable_to_TM_computable. apply MMA_computable_to_MMA_mon_computable. apply L_computable_to_MMA_computable. exact H. Qed.
imports: Undecidability(MinskyMachines.Reductions.L_computable_to_MMA_computable MinskyMachines.Reductions.MMA_computable_to_MMA_mon_computable TM.Reductions.MMA_mon_computable_to_TM_computable L.L TM.TM)