proposition: Lemma halt_cbn_flatten_iff {ts1 ts2 ctx1 ctx2 s1 s2} : halt_cbn ts1 ctx1 s1 -> map flatten ts1 = map flatten ts2 -> flatten (closure ctx1 s1) = flatten (closure ctx2 s2) -> halt_cbn ts2 ctx2 s2.
proof: Proof. move=> H. elim: H ts2 ctx2 s2; clear ts1 ctx1 s1. - move=> ts ctx t ctx' ? IH ts2 ctx2 s2. rewrite flatten_var_0. by move=> /IH /[apply]. - move=> ts1 ctx1 n t ? IH ts2 ctx2 s2. rewrite flatten_var_S. by move=> /IH /[apply]. - move=> ts1 ctx1 s t ? IH ts2 ctx2 s2. elim /(Nat.measure_induction _ context_size): ctx2 s2. move=> ctx2 IH' []. + move: ctx2 IH' => [|[ctx'2 t'2] ctx2] IH'. { by case. } move=> [|n]. * rewrite flatten_var_0. move=> /= ??. apply: halt_var_0. apply: IH' => //=. rewrite /context_size /=. lia. * rewrite flatten_var_S. move=> /= ??. apply: halt_var_S. apply: IH' => //=. rewrite /context_size /=. lia. + move=> ??? /= [] /IH {}IH ?. apply: halt_app. apply: IH => //=. by congr cons. + done. - move=> t1 ts1 ctx1 s1 ? IH [|t2 ts2] ctx2 s2; first done. move=> [Ht1t2 ?]. elim /(Nat.measure_induction _ context_size): ctx2 s2. move=> ctx2 IH' []. + move: ctx2 IH' => [|[ctx'2 t'2] ctx2] IH'. { by case. } move=> [|n]. * rewrite flatten_var_0. move=> /= ?. apply: halt_var_0. apply: IH' => //=. rewrite /context_size /=. lia. * rewrite flatten_var_S. move=> /= ?. apply: halt_var_S. apply: IH' => //=. rewrite /context_size /=. lia. + done. + move=> s2 /= [Hs1s2]. apply: halt_lam_ts. apply: IH => //=. by rewrite Ht1t2 !flatten_cons Hs1s2. - move=> ctx1 s1 [|t2 ts2] ctx2 s2; last done. move=> _. elim /(Nat.measure_induction _ context_size): ctx2 s2. move=> ctx2 IH' []. + move: ctx2 IH' => [|[ctx'2 t'2] ctx2] IH'. { by case. } move=> [|n]. * rewrite flatten_var_0. move=> /= ?. apply: halt_var_0. apply: IH' => //=. rewrite /context_size /=. lia. * rewrite flatten_var_S. move=> /= ?. apply: halt_var_S. apply: IH' => //=. rewrite /context_size /=. lia. + done. + move=> *. by apply: halt_lam. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect