Solution (source code)

= Solution

A <context-free grammar> is \b[an <ambiguous grammar> if some <word> in its generated <formal language> has two distinct <parse trees>]. Equivalently, that <word> has two distinct <leftmost derivations> from the start <nonterminal symbol>. A <leftmost derivation> always expands the leftmost remaining <nonterminal symbol>.

Two arbitrary <grammar derivations> of the same <word> do not by themselves prove ambiguity: expanding independent <nonterminal symbols> in a different order can describe the same <parse tree>. Requiring distinct <parse trees>, or distinct <leftmost derivations>, avoids that issue.
$$
\boxed{\text{Ambiguity means two distinct parse trees for at least one word}.}
$$