proposition: Lemma P_drv' p : i_P (fst p) (snd p) -> exists s t, derivable R s t /\ fst p == ienc s /\ snd p == ienc t.
proof: Proof. Proof using HS2 HS1 HI HD HE1 HE2 HE3 HER1 HER3. intros H. induction (psub_acc p) as [ [x' y'] _ IH]; cbn in *. destruct (HI H) as [(s&t&H1&H2&H3)|(s&t&u&v&H1&H2&H3&H4&H5)]; subst. - exists s, t. repeat split; trivial. now constructor. - destruct (IH (u,v)) as (s'&t'&H6&H7&H'); cbn in *; trivial; subst. + destruct H5 as [ [H5 H5r]|[ [H5 H5r]|[] ] ]. * now apply psub1. * now apply psub2. * now apply psub3. + exists (s++s'), (t++t'). repeat split. 1: now right. * apply (HE3 H2). eapply HE3. 2: apply ienc_iprep. apply iprep_respectful. easy. * apply (HE3 H3). eapply HE3. 2: apply ienc_iprep. apply iprep_respectful. easy. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation