proposition: Lemma enc_stack_combinations B rho C x X Y : rho ⊨ combinations B X Y -> eval rho X = M_enc_stack C -> eval rho Y = x -> x = M_enc_stack (derivation_step B C).
proof: Proof. Proof using M_ZF VIEQ. induction B as [|[s t] B IH] in rho,C,x,X,Y |-*. - cbn. rewrite VIEQ. now intros -> _ <-. - intros [x1[x2[[H1 H2]H3]]] R1 R2; fold sat in *. assert (x = x2 ∪ x1) as ->. { rewrite <- R2. cbn in H1. rewrite !eval_comp in H1. apply VIEQ, H1. } clear H1. cbn. fold (derivation_step B C). rewrite M_enc_stack_app. enough (x1 = M_enc_stack (derivation_step B C)) as E1. + enough (x2 = M_enc_stack (append_all C (s, t))) as E2 by now rewrite E1, E2. apply M_ext; intros u Hu. * apply H3 in Hu as [v [Hv[a [b Ha]]]]. cbn in Hv. erewrite !eval_comp, eval_ext, R1 in Hv; trivial. apply enc_stack_el' in Hv as (s'&t'&H&H'). enough (u = M_enc_card (s++s') (t++t')) as ->. { apply enc_stack_el. apply in_map_iff. now exists (s', t'). } cbn in Ha. rewrite !VIEQ in Ha. destruct Ha as [D1 D2]. rewrite D1 in H'. unfold M_enc_card in H'. apply opair_inj in H' as [-> ->]. rewrite D2; unfold M_enc_card, M_opair; repeat f_equal. all: rewrite eval_prep_string; cbn. all: apply M_prep_enc. * apply enc_stack_el' in Hu as (s'&t'&H&->). unfold append_all in H. eapply in_map_iff in H as [[a b][H H']]. cbn in H. apply H3. exists (M_enc_card a b). split. { cbn. erewrite !eval_comp, eval_ext, R1; trivial. now apply enc_stack_el. } exists (M_enc_string b), (M_enc_string a). split. -- cbn. apply VIEQ. reflexivity. -- cbn. apply VIEQ. rewrite !eval_prep_string. cbn. rewrite !M_prep_enc. injection H. intros -> ->. reflexivity. + eapply IH; eauto. unfold shift. now erewrite !eval_comp, eval_ext, R1. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)