Formal Grammar: derivation form posted on Wiki? Wiki describes the binary relation $\underset{\mbox{G}}{\implies}$ as &quot;G derives in one step&quot;.  I have a question on the condition when there are multiple productions for a single non-terminal.
Wiki defines $G = (N, \Sigma, P, S)$ and $\underset{\mbox{G}}{\implies} \subset (\Sigma \cup N)^* \times (\Sigma \cup N)^*$ where:
$(\underset{\mbox{G}}{x \implies y}) \iff \exists u,v,p,q \in (\Sigma \cup N)^* : (x = upv) \land ((p, q) \in P) \land (y = uqv)$
Then
$(\overset * {\underset{\mbox{G}}{x \implies y}})$ is defined as the refexive transitive closure.  Therefore applying $\underset{\mbox{G}}{\implies}$ multiple times results in the language of the grammar:
$\{w \in \Sigma^* | (\overset * {\underset{\mbox{G}}{S \implies w}})\}$
QUESTION
For the form $(\underset{\mbox{G}}{x \implies y})$ I consider the case of multiple rules $(p,q_0), (p, q_1) \in P$ for a non-terminal $N$.  If solving for $y$, $y$ will result in the string with only a single rule applied.  How should the derivation happen with multiple production rules?
I can see that supplying both arguments $(\Sigma \cup N)^* \times (\Sigma \cup N)^*$ to $\underset{\mbox{G}}{x \implies y}$ will yield all derivations.
You seem to be looking for a deterministic procedure that isn't there.
With multiple production rules, you solve in every possible way.  For instance, for the grammar
$S \rightarrow a \\ S \rightarrow aS$
we have
$
\underset{G}{S \implies a}, \\
\underset{G}{S \implies aS}, \\
\underset{G}{aS \implies aa}, \\
\underset{G}{aS \implies aaS}, \\
\ldots
$