proposition: Lemma reduction_full x : (exists A, A <<= R /\ A <> [] /\ sigma a A = x) <-> L G x.
proof: Proof. split. - intros (A & ? & ? & ?). subst. destruct Post_CFG_1' with (A := A); intuition. split. + eassumption. + eapply terminal_iff_G. rewrite sigma_eq. intros E. edestruct fresh_spec with (l := sym R ++ [a]); try reflexivity. eapply in_app_iff in E as [ | [ | ? % tau2_gamma ] % in_app_iff]. * eapply in_app_iff. left. eapply sym_mono; eauto. now eapply tau1_sym. * eapply in_app_iff. right. eauto. * eapply in_app_iff. left. eapply sym_mono; eauto. now eapply tau2_sym. - intros [(A & m & HA & HE & Hm) % Post_CFG_2 ?]. subst. destruct Hm as [-> | [-> ?]]. + eapply terminal_iff_G in H. exfalso. rewrite sigma_eq in H. eapply H. eauto. + exists A. eauto. Qed.
imports: Setoid Morphisms List Arith Lia Undecidability.CFG.CFP Undecidability.CFG.CFG Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions