proposition: Lemma Derive_P_A_2_imp_Der_P_A_2_App : forall x y : Word, Derivestar_P_A_2 (x, y) (nil, nil) -> forall u v : Word, Append u v = x -> inmonoid X u -> ex2 (fun w : Word => Append u w = y) (fun w : Word => Derivestar_P_A_2 (v, w) (nil, nil)).
proof: Proof. unfold Derivestar_P_A_2 in |- *. simple induction x. intros y Der_P_A_2 u v. elimtype (u = nil \/ (exists w : Word, (exists x : Elt, u = cons x w))). intros u_eg. rewrite u_eg. intros App_eg inmon_nil. exists y; auto. replace v with nil; trivial. intro temp; elim temp; clear temp; intros w temp; elim temp; clear temp. intros x0 eg_u. rewrite eg_u. intros cons_eg_nil. absurd (cons x0 (Append w v) = nil). discriminate. trivial. generalize u; clear u; simple induction u. auto. intros x1 w1 Hyp; apply or_intror; exists w1; exists x1; trivial. intros x0 w Hyp y Der_star_cons u v App_eg inmon_X. elimtype (u = nil \/ (exists w : Word, (exists x : Elt, u = cons x w))). intros u_eg. rewrite u_eg. replace v with (cons x0 w). exists y; trivial. replace v with (Append u v). auto. rewrite u_eg. trivial. intro temp; elim temp; clear temp; intros w1 temp; elim temp; clear temp. intros x1 eg_u. rewrite eg_u. elimtype (ex2 (fun v2 : Word => y = cons x0 v2) (fun v2 : Word => Derivestar_P_A_2 (w, v2) (nil, nil))). intros v2 y_eg Der_w_v2. elimtype (ex2 (fun w : Word => Append w1 w = v2) (fun w : Word => Rstar Conf Derive_P_A_2 (v, w) (nil, nil))). intros we App_w1_we_eg_v2 Rstar_Der. exists we. rewrite y_eg. replace (Append (cons x1 w1) we) with (cons x1 (Append w1 we)). apply cons_cons. apply cons_cons_inv1 with (Append w1 v) w. rewrite <- App_eg. rewrite eg_u. trivial. trivial. trivial. trivial. apply Hyp. trivial. apply cons_cons_inv2 with x1 x0. rewrite <- App_eg. rewrite eg_u. trivial. apply inmonoid_cons_inv with x1. rewrite <- eg_u. trivial. apply Der_cons_inv. replace x0 with x1. apply inmonoid_cons_inv2 with w1. rewrite <- eg_u. trivial. apply cons_cons_inv1 with (Append w1 v) w. rewrite <- App_eg. rewrite eg_u. trivial. assumption. clear inmon_X App_eg. generalize u; clear u; simple induction u. auto. intros x1 w1 tmp; apply or_intror; exists w1; exists x1; trivial. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata