proposition: Lemma machine_inverse_simulation x vs y : machine x vs y -> eclosed x -> Forall eclosed_future vs -> L.eval (traverse (flatten x) vs) (flatten y).
proof: Proof. elim; cbn. - move=> {}x xs {}vs {}y _ IH. move=> [?] [??]. by apply: IH. - move=> {}x xs n {}vs {}y _ IH. move=> [/bound_var_S_iff] /[dup] /boundE Hxsn ? [? ?]. rewrite flatten_var. rewrite (nth_indep _ _ (var n)). { rewrite map_length. cbn. lia. } by apply: IH. - move=> xs s t {}vs {}y _ IH. move=> [/boundE] [??] ??. by apply: IH; [|constructor]. - move=> xs s z {}vs {}y _ IH [??] /Forall_cons_iff [??]. by apply: IH; [|constructor]. - move=> xss xts s t {}vs {}y _ IH. move=> [??] /Forall_cons_iff /= [[/boundE]] ? Hxss ?. apply: step_eval. { apply: traverse_step. by apply: stepApp. } suff -> : subst (subst_many s 1 (map flatten xss)) 0 (lam (subst_many t 1 (map flatten xts))) = subst_many s 0 (lam (subst_many t 1 (map flatten xts)) :: map flatten xss) by apply: IH. apply subst_subst_many. rewrite map_map. apply: all_map_impl Hxss. by apply: eclosed_closed_flatten. - move=> {}xs s *. by apply: eval_abs. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun