proposition: Lemma M_combinations_spec B rho x y a b : M_combinations B x y -> eval rho a = x -> eval rho b = y -> rho ⊨ combinations B a b.
proof: Proof. Proof using VIEQ. induction B in y,a,b,rho|-*; cbn. - rewrite VIEQ. now intros -> _ ->. - destruct a0 as [s t]. intros (y1&y2&H1&H2&H3) Ha Hb. exists y1, y2. repeat split. + cbn. apply VIEQ. erewrite !eval_comp. unfold funcomp. cbn. change (eval (fun x => rho x) b) with (eval rho b). now rewrite Hb. + eapply (IHB _ y1); trivial. erewrite !eval_comp. unfold funcomp. cbn. change (eval (fun x => rho x) a) with (eval rho a). now rewrite Ha. + intros (u & Hu & c & d' & H) % H3. exists u. split. * cbn. erewrite !eval_comp. erewrite eval_ext, Ha; trivial. * exists d', c. cbn. rewrite !VIEQ, !eval_prep_string. apply H. + intros (u & Hu & c & d' & H). apply H3. exists u. split. * cbn in Hu. erewrite !eval_comp in Hu. rewrite <- Ha. apply Hu. * exists d', c. cbn in H. rewrite !VIEQ, !eval_prep_string in H. apply H. 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)