proposition: Theorem reduction : KrivineMclosed_HALT ⪯ SNclosed.
proof: Proof. exists (fun '(exist _ t _) => exist _ _ (subst_enc_state nil nil t)). move=> [t Ht] /=. split. - move=> ?. apply: step'_step_SN. by apply: halt_cbn_rt_step'. - move=> /SN_terminates_step'. move=> /(terminates_reflection step'_det Krivine_step_steps' Krivine_step_dec (sync_intro _ _ _)). move=> [[[ts' ctx'] t']] []. move=> /Krivine_step_halt_cbn'. apply; [by constructor|]. split; [|done]. apply /L_facts.closed_dcl. apply: term_facts.closed_I=> k. by rewrite term_facts.L_subst_Lambda_subst; [|apply: Ht]. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect Undecidability.Synthetic.Definitions