proposition: Lemma cut_unicite : forall u a b a' b' : Word, inmonoid X a /\ Append a b = u /\ (b = nil \/ ex2 (fun x : Elt => ~ dans x X) (fun x : Elt => exists w : Word, b = cons x w)) -> inmonoid X a' /\ Append a' b' = u /\ (b' = nil \/ ex2 (fun x : Elt => ~ dans x X) (fun x : Elt => exists w : Word, b' = cons x w)) -> a = a'.
proof: Proof. intros u a b a' b' temp1 temp2; elim temp1; elim temp2; clear temp1; clear temp2. intros inmon temp inmon' temp'; elim temp; elim temp'; clear temp; clear temp'. intros App spec_or App' spec_or'. elimtype (exists w : Word, a = Append a' w /\ b' = Append w b \/ a' = Append a w /\ b = Append w b'). intros x temp; elim temp; clear temp. pattern a' at 2 in |- *. replace a' with (Append a' nil). generalize x; clear x; simple induction x. intro temp; elim temp. auto. intros x0 w Hyp temp; elim temp; clear temp. intros a_eg b'_eg. absurd (dans x0 X). elim spec_or'. rewrite b'_eg. intro cons_nil. absurd (cons x0 (Append w b) = nil). discriminate. assumption. intro temp; elim temp; clear temp. intros x1 N_dans_x1 temp; elim temp; clear temp. intros w' b'_eg_2. replace x0 with x1. assumption. apply cons_cons_inv1 with w' (Append w b). rewrite <- b'_eg_2. assumption. apply inmonoid_cons_inv2 with w. apply inmonoid_Append_inv2 with a'. rewrite <- a_eg. assumption. apply Append_w_nil. pattern a at 2 in |- *. replace a with (Append a nil). generalize x; clear x; simple induction x. intro temp; elim temp. auto. intros x0 w Hyp temp; elim temp; clear temp. intros a'_eg b_eg. absurd (dans x0 X). elim spec_or. rewrite b_eg. intro cons_nil. absurd (cons x0 (Append w b') = nil). discriminate. assumption. intro temp; elim temp; clear temp. intros x1 N_dans_x1 temp; elim temp; clear temp. intros w' b_eg_2. replace x0 with x1. assumption. apply cons_cons_inv1 with w' (Append w b'). rewrite <- b_eg_2. assumption. apply inmonoid_cons_inv2 with w. apply inmonoid_Append_inv2 with a. rewrite <- a'_eg. assumption. apply Append_w_nil. apply Append_Append. rewrite App'; assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata