Here's my question:

Attempt:

So the set of theorems is $\displaystyle \{ B^j A^i \ : \ i \equiv 0 \mod 3\}$.

- The only axiom is $\displaystyle B$.

- The alphabet is $\displaystyle \{ A, B \}$

- Rules of inference (here $\displaystyle x$ and $\displaystyle y$ represent any string, possibly empty, of symbols from the alphabet):
For example $\displaystyle B^2A^6$ is a theorem of this system. To see this, we provide the following derivation:

- From $\displaystyle x$ infer $\displaystyle xAAA$
- From xyx infer xBx

1. $\displaystyle B$ (Axiom)

2. $\displaystyle BAAA$ (From 1 by rule 1)

3. $\displaystyle BAAAAAA$ (From 2 by rule 1)

4. $\displaystyle BBAAAAAA = B^2A^6$ (From 3 by rule 2)

Is this correct?