proposition: Lemma crdv_iff n (x y : obstring n) : i_P x y <-> exists s t, derivable R s t /\ x = ienc s /\ y = ienc t /\ |s| <= n /\ |t| <= n.
proof: Proof. destruct x as [ [x HX]|], y as [ [y HY]|]; split; cbn; auto. { intros H. exists x, y. repeat setoid_rewrite obstring_ienc. now repeat split. } all: intros (s&t&H1&H2&H3&H4&H5). all: unshelve setoid_rewrite obstring_ienc in H2; [auto |]; unshelve setoid_rewrite obstring_ienc in H3; [auto |]. all: try discriminate. revert H2 H3. now intros [= ->] [= ->]. 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