proposition: Lemma MUREC_red : recalg.MUREC_HALTING ⪯ UMUREC_HALTING.
proof: Proof. unshelve eexists. - intros f. exact (erase f). - unfold UMUREC_HALTING, MUREC_HALTING. intros f. split; intros []. + rewrite ra_bs_correct in H. eapply ra_bs_to_c in H as []. exists x0. eapply erase_correct in H. unfold evalfun. cbn in H. rewrite H. congruence. + unfold evalfun in H. destruct eval eqn:E; try congruence. destruct s; try congruence. eapply erase_correct with (v := vec_nil) in E. exists n. eapply ra_bs_correct. now eapply ra_bs_from_c. 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