proposition: Lemma MUREC_WCBV : MUREC_HALTING ⪯ converges.
proof: Proof. eapply reduces_transitive. 1:eapply MUREC_red. eapply L_recognisable_halt. exists (fun c n => match eval n 0 c [] with Some (inl n) => true | _ => false end). split. - econstructor. extract. - firstorder. + unfold evalfun in *. exists x0. destruct eval; try destruct s; try congruence. + exists x0. unfold evalfun in *. destruct eval; try destruct s; try congruence. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability(MuRec_computable LVector) Undecidability.L.Util(NaryApp ClosedLAdmissible) Undecidability(LOptions) Undecidability.L.Reductions.MuRec.MuRec_extract