proposition: Lemma Post_CFG_2 x : rewt G [S] x -> exists A m, A <<= R /\ sigma m A = x /\ (m = S \/ m = a /\ A <> []).
proof: Proof. intros. induction H. - cbn. exists [], S. eauto. - inversion H0. subst. clear H0. destruct H1 as [ | [(? & ? & ?) % in_map_iff | (? & ? & ?) % in_map_iff] % in_app_iff]; inversion H0; subst. + eassumption. + destruct x0 as [u' v']. inversion H3. subst. destruct IHrewt as (A & m & HA & IHA & Hm). exists (A ++ [(u', v')]), S. repeat split. * eauto. * simpl_list. cbn. enough (~ S el x). { enough (~ S el y0). { eapply sigma_snoc with (s := S); eauto. assert (IH2 := IHA). eapply sigma_inv in IHA; eauto. { subst. eauto. } intros D. edestruct fresh_spec with (l := sym R ++ [a]); try reflexivity. eapply in_app_iff. left. eapply sym_mono. { eauto. } eauto. } eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H. rewrite Nat.eqb_refl in H. eapply notInZero. lia. } eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H. rewrite Nat.eqb_refl in H. eapply notInZero. lia. * eauto. + destruct x0 as [u' v']. inversion H3. subst. destruct IHrewt as (A & m & HA & IHA & Hm). exists (A ++ [(u', v')]), a. repeat split. * eauto. * simpl_list. cbn. enough (~ S el x). { enough (~ S el y0). { eapply sigma_snoc with (s := S); eauto. -- assert (IH2 := IHA). eapply sigma_inv in IHA; eauto. { subst. eauto. } intros D. edestruct fresh_spec with (l := sym R ++ [a]); try reflexivity. eapply in_app_iff. left. eapply sym_mono. { eauto. } eauto. } eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H. rewrite Nat.eqb_refl in H. eapply notInZero. lia. } eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H. rewrite Nat.eqb_refl in H. eapply notInZero. lia. * destruct A; cbn; firstorder congruence. 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