proposition: Theorem L_computable_closed_to_MMA_computable {k} (R : Vector.t nat k -> nat -> Prop) : L_computable_closed R -> MMA_computable R.
proof: Proof. move=> [s] [Hs] s_spec. apply: Argument.MMA_computable_R. - eassumption. - move=> v. by case: (s_spec v). - move=> v. by case: (s_spec v). Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun