proposition: Theorem Derivestar_P_A_imp_Derivestar : forall x y : Word, Derivestar_P_A X d (x, y) (nil, nil) -> Derivestar R x y.
proof: Proof. intros x y Derivestar_P_A_x_y_nil_nil. elimtype (exists s2 : Word, Derivestar_P_A_3 (nil, (x, y)) (s2, (nil, nil))). intros s2 Derivestar_P_A_3_x_y. apply Derivegstar_Derivestar with X. replace x with (Append nil x). replace y with (Append s2 nil). apply Derivestar_P_A_3_imp_Derivegstar with y nil. assumption. trivial. replace y with (Append nil y). apply sym_equal. apply Derisvestar_P_A_3_conserve with x nil. assumption. trivial. trivial. apply Derivestar_P_A_2_imp_Derivestar_P_A_3. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata