proposition: Lemma Halt_red cfg : Halt' cfg <-> converges (mu (ext ((fun k => LOptions.isSome (loopM (M := M) cfg k))))).
proof: Proof. split; intros. - destruct H as (f & ? & k & ?). edestruct (mu_complete) with (P:= ext (fun k0 : nat => isSome (loopM cfg k0))) (n:=k). + Lproc. + intros. eexists. rewrite !ext_is_enc. now Lsimpl. + Lsimpl. now rewrite H0. + exists (ext x). split. eauto. Lproc. - destruct H as (v & ? & ?). edestruct mu_sound as (k & ? & ? & _). + eapply term_test. + intros. eexists. now Lsimpl'. + eassumption. + eauto. + subst. assert ((ext (fun k : nat => LOptions.isSome (loopM cfg k))) (ext k) == ext (LOptions.isSome (loopM cfg k))) by now Lsimpl. rewrite H1 in H2. clear H1. eapply unique_normal_forms in H2; try Lproc. eapply inj_enc in H2. destruct (loopM cfg k) eqn:E. * exists m. split. 2: eauto. unfold loopM in E. now eapply loop_fulfills in E. * inv H2. Qed.
imports: Undecidability.L.Datatypes(LOptions) Undecidability.L(Computability.MuRec) Undecidability.TM(TM_facts) Undecidability.L.TM.TMinL.TMinL_extract