proposition: Lemma Krivine_step_halt_cbn' ts ctx t Y : clos_refl_trans _ Krivine_step (ts, ctx, t) Y -> Forall eclosed ts -> eclosed (closure ctx t) -> (forall Z, not (Krivine_step Y Z)) -> halt_cbn ts ctx t.
proof: Proof. move E: (ts, ctx, t) => X /clos_rt_rt1n_iff H. elim: H ts ctx t E. - move=> [[ts ctx] t] > [-> -> ->]. move: t => [[|x]|s t|t]. + move: ctx => [|[??]?] /=. * move=> ? [/boundE]. lia. * move=> _ _ H. exfalso. apply: H. by constructor. + move: ctx => [|[??]?] /=. * move=> ? [/boundE]. lia. * move=> _ _ H. exfalso. apply: H. by constructor. + move=> _ _ H. exfalso. apply: H. by constructor. + move: ts => [|??] /=. * move=> *. by constructor. * move=> _ _ H. exfalso. apply: H. by constructor. - move=> [[??]?] [[??]?] ? /[dup] /Krivine_step_eclosed H1. move=> /Krivine_step_halt_cbn_step H _ IH ??? [???] *. subst. apply: H. apply: IH; tauto. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect