Proving a grammar only generates words whose alternating digit sums are multiples of three
Rough hint: play around with the many equivalent models you have for regular languages.

For 1), I find problematic that the contribution of an already generated digit changes as more symbols are added to the front. Things would be easier if the grammar was right-linear.


   Convert the given grammar to an NFA and convert that one to a grammar with the simple construction, which always yields right-linear grammars. (You should have proven algorithms for both.) Determinising/minimising the intermediate automaton might also help the proof.


Then, you have to figure out an induction hypothesis on sentences that works and implies the statement (for words), and perform induction over the whole set of sentences (by the length of the derivation).


   For example, if a non-terminal $C$ can only end the derivation by deriving a $1$, then for any sentence of the form $wC$, either $w$ has even length and its alternating digit sum plus one divides three, or it has odd length.


For 2), build an automaton that you can easily show generates all such words.


   For instance, use a counter construction, that is count the alternating digit sum modulo three in the states.


Now you can show equivalence of this automaton and the one derived from the grammar in 1).