I have not looked into the details of the grammar, but proving that a grammar is unambiguous is typically done by proving that it is in, say, LL(1) or LR(1) (or

I have not looked into the details of the grammar, but proving that a grammar is unambiguous is typically done by proving that it is in, say, LL(1) or LR(1) (or some related family). This approach towards unambiguity has the additional advantage that it is easy to derive a parsing algporithm directly from the grammar that has nice theoretical properties (e.g. linear parsing time in the input length; where the hidden constant depends on the grammar).