Proving a grammar only generates words whose alternating digit sums are multiples of three This is homework and I'm looking for a push in the right direction. Proofs were never something I was properly taught, so now they're kind of a weak point.

Here's the problem:


  The following grammar generates numbers in binary notation ($C$ is the
  start symbol):
  
  $\qquad \begin{align}C &amp;\to C 0 \mid A 1 \mid 0 \\
                       A &amp;\to B 0 \mid C 1 \mid 1 \\
                       B &amp;\to A 0 \mid B 1
          \end{align}$
  
  
  Prove that the alternating sums of the digits of the generated
  numbers are multiples of $3$. The alternating sum of $w=w_0\dots w_n$ is defined as $\sum_{i=0}^n (-1)^i \cdot w_i$. As an example, $C$
  generates $1001$ via $C \Rightarrow A1 \Rightarrow B01 \Rightarrow A001 \Rightarrow 1001$ with alternating sum of $0$;
  clearly, $0$ is a multiple of $3$.
  Prove that all such numbers (i.e.,
  numbers whose alternating sum is a multiple of 3) are generated by the
  grammar.
  


I'm thinking I need to show that the grammar can only generate strings which are made up of repeated subsequences of digits which always add up to 0, 3, or -3. But I'm not sure how to show that it can only generate those three subsequences.

I also have worked out these thoughts:


Consider that any even number of consecutive 1s is irrelevant, as they cancel each other out.
Consider that all zeros are in of themselves irrelevant, as they add nothing.
Consider then that the only relevant pattern is that of alternating 1s and zeros, and where this pattern starts and ends.
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).