proposition: Lemma comb_rel_rep C s t : M_is_rep (M_comb_rel s t) (M_enc_stack C) (M_enc_stack (append_all C (s, t))).
proof: Proof. Proof using M_ZF VIEQ. intros y. split. - intros (u&v&H&->) % enc_stack_el'. unfold append_all in H. apply in_map_iff in H as [[a b][H1 H2]]. cbn in H1. exists (M_enc_card a b). split; try now apply enc_stack_el. exists (M_enc_string a), (M_enc_string b). split; trivial. assert (u = s++a) as -> by congruence. assert (v = t++b) as -> by congruence. now rewrite !M_prep_enc. - intros (u&H&a&b&->&->). apply enc_stack_el' in H as [u[v[H1 H2]]]. apply opair_inj in H2 as [-> ->]. rewrite !M_prep_enc. apply enc_stack_el. apply in_map_iff. now exists (u, v). 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)