proposition: Theorem HaltMTM_to_HaltL : HaltMTM ⪯ HaltL.
proof: Proof. eexists (fun '(existT2 (Sigma, n) M tp) => (L.app mu (@ext _ _ _ (term_test (mk_mconfig (start M) tp))))). intros [ [Sigma n] M tp ]. cbn. unfold HaltL. setoid_rewrite eval_iff. split. - intros H. epose proof (Halt_red (mk_mconfig (start M) tp)) as [[v [H1 H2]] _]. + destruct H as (? & ? & ?). eexists (mk_mconfig _ _). rewrite <- TM_eval_iff. split. 2:eassumption. eapply TM_eval_halts. eassumption. + exists v. split; eauto. eapply equiv_lambda. eassumption. eassumption. - intros [t [H1 H2]]. epose proof (Halt_red (mk_mconfig (start M) tp)) as [_ [[q' t']]]. + eexists. eauto. + exists q', t'. eapply TM_eval_iff. eapply H. Qed.
imports: Undecidability(TM.TMEncoding TM.TMinL TM.Util.TM_facts) Undecidability.L(Computability.MuRec) Undecidability.Synthetic.Definitions