proposition: Lemma cut1_cons : forall (a : Elt) (w : Word), dans a X -> cut1 (cons a w) = cons a (cut1 w).
proof: Proof. intros a w dans_a_X. unfold cut1, cut in |- *. elim (cut_spec w). intros x temp; elim temp; clear temp. intros b temp; elim temp; clear temp. intros inmon_X_x temp; elim temp; clear temp. elim (cut_spec (cons a w)). intros x' temp; elim temp; clear temp. intros b' temp; elim temp; clear temp. intros inmon_X_x' temp; elim temp; clear temp. intros App_eg' spec' App_eg spec. simpl in |- *. cut (inmonoid X x'). cut (Append x' b' = cons a w). clear inmon_X_x' App_eg'. generalize x'; clear x'; simple induction x'. intro App_nil_b'_eg_cons_a_w. absurd (dans a X). elim spec'. intro b'_nil. absurd (cons a w = nil). discriminate. rewrite <- b'_nil. rewrite <- App_nil_b'_eg_cons_a_w. trivial. intro temp; elim temp; clear temp. intros x0 N_dans_x0_X temp; elim temp; clear temp. intros w1 eg_b'_cons. replace a with x0. assumption. apply cons_cons_inv1 with w1 w. rewrite <- eg_b'_cons. assumption. assumption. intros x0 w0 Hyp App_eg_cons inmon_cons. apply cons_cons. apply cons_cons_inv1 with (Append w0 b') w. assumption. apply cut_unicite with w b' b. split. apply inmonoid_cons_inv with x0; assumption. split. apply cons_cons_inv2 with x0 a. assumption. assumption. split; auto. assumption. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata