proposition: Lemma MuRec_computable_functional_iff {k} (R : Vector.t nat k -> nat -> Prop) : functional R -> MuRec_computable R <-> exists f : recalg k, (forall v m, ra_bs f v m -> R v m) /\ (forall v m, R v m -> exists m, ra_bs f v m).
proof: Proof. intros HR. split. - intros [f Hf]. exists f. split. + intros v m. eapply Hf. + intros. eexists. eapply Hf. eauto. - intros [f [Hf1 Hf2]]. exists f. intros v. split. + intros Hm. specialize (Hf2 _ _ Hm) as [m' Hm']. specialize (Hf1 _ _ Hm'). enough (m = m') as -> by eauto. firstorder. + eauto. Qed.
imports: Coq(List Vector Nat)