proposition: Lemma machine_flatten_equiv {x1 vs1 y1 x2 vs2} : machine x1 vs1 y1 -> eclosed x1 -> eclosed x2 -> Forall eclosed_future vs1 -> Forall eclosed_future vs2 -> map flatten_future vs1 = map flatten_future vs2 -> flatten x1 = flatten x2 -> exists y2, flatten y1 = flatten y2 /\ machine x2 vs2 y2.
proof: Proof. have H' : forall y1 (P Q : eterm -> Prop), (forall y2, P y2 -> Q y2) -> (exists y2 : eterm, flatten y1 = flatten y2 /\ P y2) -> (exists y2 : eterm, flatten y1 = flatten y2 /\ Q y2). { move=> > ? [y2] [??]. exists y2. firstorder done. } move=> H. elim: H x2 vs2. - move=> {}x1 xs1 {}vs1 {}y1 ? IH x2 vs2 /= [? [??]] ???. by apply: IH. - move=> {}x1 xs1 n1 {}vs1 {}y1 /machine_var_bound ? IH x2 vs2. rewrite flatten_closure_var_S. { done. } move=> /= [/bound_var_S_iff ? [??]]. move=> /IH /[apply] /[apply] /[apply] /[apply]. by apply. - move=> xs1 s1 t1 {}vs1 {}y1 ? IH [xs2 u] vs2 Hs1t1 Hu Hvs1 Hvs2 ?. elim /(@induction_ltof1 _ context_size): xs2 u Hu. move=> xs2 IH2 []. + move=> [|x2]. * move: xs2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /eclosed_var_0 ?. rewrite flatten_var /=. move=> /IH2. apply: unnest. { rewrite /context_size /= term_size_S. lia. } apply: unnest. { done. } apply: H' => y2 ?. by apply: machine_var_0. * move: xs2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /eclosed_var_S ? /flatten_eq_var_S /IH2. apply: unnest. { cbn. rewrite /list_sum term_size_S. lia. } apply: unnest. { done. } apply: H' => y2 ?. by apply: machine_var_S. + move=> s2 t2. move: Hs1t1. rewrite !flatten_app. move=> /eclosed_app [??] /eclosed_app [??]. move=> [+ ?] => /IH => /(_ ((true, closure xs2 t2) :: vs2)). apply: unnest. { done. } apply: unnest. { done. } apply: unnest. { by constructor. } apply: unnest. { by constructor. } apply: unnest. { cbn. by congruence. } move=> [y2] [? ?]. exists y2. split; [done|]. by apply: machine_app. + done. - move=> xs1 s1 z1 {}vs1 {}y1 ? IH [xs2 u] vs2 Hs1 Hu Hvs1 Hvs2 Hvs. elim /(@induction_ltof1 _ context_size): xs2 u Hu. move=> xs2 IH2 []. + move=> [|x2]. * move: xs2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /eclosed_var_0 ?. rewrite flatten_var /=. move=> /IH2. apply: unnest. { rewrite /context_size /= term_size_S. lia. } apply: unnest. { done. } apply: H' => y2 ?. by apply: machine_var_0. * move: xs2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /eclosed_var_S ? /flatten_eq_var_S /IH2. apply: unnest. { cbn. rewrite /list_sum term_size_S. lia. } apply: unnest. { done. } apply: H' => y2 ?. by apply: machine_var_S. + done. + move=> s2. move: Hvs1 => /Forall_cons_iff [Hz1 Hvs1]. move: vs2 Hvs Hvs2 {IH2} => [|[[] [xss2 t2]]vs2]; [done| |done]. move=> /= /cons_inj [] /pair_equal_spec [_] + ? /Forall_cons_iff [??] ? Hs. move=> /IH => /(_ ((false, closure xs2 s2) :: vs2)). apply: unnest. { done. } apply: unnest. { done. } apply: unnest. { by constructor. } apply: unnest. { by constructor. } apply: unnest. { cbn. by congruence. } apply: H' => y2 ?. by apply: machine_lam_swap. - move=> xss1 xts1 s1 t1 {}vs1 {}y1 ? IH [xs2 u] vs2 Ht1 Hu Hvs1 Hvs2 Hvs. elim /(@induction_ltof1 _ context_size): xs2 u Hu. move=> xs2 IH2 []. + move=> [|x2]. * move: xs2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /eclosed_var_0 ?. rewrite flatten_var /=. move=> /IH2. apply: unnest. { rewrite /context_size /= term_size_S. lia. } apply: unnest. { done. } apply: H' => y2 ?. by apply: machine_var_0. * move: xs2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /eclosed_var_S ? /flatten_eq_var_S /IH2. apply: unnest. { cbn. rewrite /list_sum term_size_S. lia. } apply: unnest. { done. } apply: H' => y2 ?. by apply: machine_var_S. + done. + move=> t2 /= ?. move: Hvs1 => /= /Forall_cons_iff [Hs1 Hvs1]. move: vs2 Hvs Hvs2 {IH2} => [|[[] [xss2 s2]]vs2]; [done|done|]. move=> /= /cons_inj [] /pair_equal_spec [_] Hs. move=> + /Forall_cons_iff [] /= [/boundE ? Hxss2] ? Ht. move=> /(IH (closure (closure xs2 (lam t2) :: xss2) s2)). apply: unnest. { move: Ht1 Hs1 => /= [??] [/boundE ??]. tauto. } apply: unnest. { cbn. tauto. } apply: unnest. { done. } apply: unnest. { done. } apply: unnest. { move: (Hs). rewrite /flatten -/flatten /= Ht. move=> []. rewrite -subst_subst_many. { move: Hs1 => /= [?]. rewrite map_map. apply: all_map_impl. by apply: eclosed_closed_flatten. } rewrite -subst_subst_many. { move: Hxss2. rewrite map_map. apply: all_map_impl. by apply: eclosed_closed_flatten. } by move=> ->. } apply: H' => y2 ?. by apply: machine_lam_subst. - move=> xs1 s1 [xs2 u] [|??]; [|done]. move=> _ _ _ _ _. elim /(@induction_ltof1 _ context_size): xs2 u. move=> xts2 IH2 []. + move=> [|x2]. * move: xts2 IH2 => [|[? ?] ?]; [done|]. move=> IH2. rewrite flatten_var /=. move=> /IH2. apply: unnest. { rewrite /context_size /= term_size_S. lia. } apply: H' => y2 ?. by apply: machine_var_0. * move: xts2 IH2 => [|[? ?] ?]; [done|]. move=> IH2 /flatten_eq_var_S /IH2. apply: unnest. { cbn. rewrite /list_sum term_size_S. lia. } apply: H' => y2 ?. by apply: machine_var_S. + done. + move=> s2 ?. eexists. split; [eassumption|]. by apply: machine_lam. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun