proposition: Theorem Parser1 : forall u : Word, {LL u} + {~ LL u}.
proof: Proof. intros. elimtype ({L u} + {~ L u}). intro Hyp. left. cut (l_egal L LL). intro temp; elim temp. unfold l_inclus in |- *. intros. auto. unfold L, LL, wa, wd, d, f_R_d, f_X_d in |- *. apply equiv_APD_Gram. exact H. unfold not in |- *. intro Hyp. right. intro LL_u. apply Hyp. cut (l_egal L LL). intro temp; elim temp. unfold l_inclus in |- *. intros. auto. unfold L, LL, wa, wd, d, f_R_d, f_X_d in |- *. apply equiv_APD_Gram. exact H. unfold L in |- *. apply axiom_APD with P. unfold P, wd, wa, d, f_R_d, f_X_d in |- *. apply X_P_wd_wa_d. exact H. Qed.
imports: Ensf more_words PushdownAutomata gram gram_aut