Extra credit We claim that the language generated by the regular expression R consists of all winning boards:

R = b ∪ b(ba)^{∗}(ab)^{∗}b ∪ b(ba)^{∗}(ab∪bbba)(bb)^{+}(ab)^{∗}b ∪ b(ab)^{∗}(bb)^{+}(ba∪abbb)(ba)^{∗}b

We have to verify that each word in R is a winning board, and each winning word is in R. This may be taken as soundness and completeness of the construction.

Soundness: Each word in R is winning. We prove this by induction on the number of b’s in w, where w ∈ R. For k = 1 there is only one word b ∈ R, and this is winning. By the induction hypothesis we assume that all words in R with k b’s are winning. Let w be a word with k + 1 b’s. It has one of the following forms:

• bb, then b obtained by one jump is in R so bb is winning.

• b(ba)^{i+1}(ab)^{j}b, i, j ≥ 0, then b(ba)^{i}(ab)^{j}b ∈ R obtained by one leftmost jump is winning by the induction hypothesis.

• b(ba)^{i}(ab)(bb)^{j+1}(ab)^{l}b, where i = l = 0, then we obtain the word bbaa(bb)^{j} ∈ b(ab)^{∗}(bb) + (ba ∪ abbb)(ba)^{∗}b ⊂ R in one move.

• Similar arguments are used for b(ba)^{i}(ab)^{j+1}b, b(ba)^{i+1}(ab∪bbba)(bb)^{j+1}(ab)^{l}b et.c.

In all cases one can reduce w to a word v with k b’s that is a member of R.

Completeness: We must show that each winning word w is a member of R. To this end we again use induction on the number of b’s in w to show that w ∈ R. The base case is trivial k = 1: b ∈ R. For the inductive step assume that every winning word with k b’s is in R, and let w be a winning word with k + 1 b’s. Hence in one step towards the winning configuration w reduces to a word v with k b’s, where v ∈ R. We consider the possible cases for v:

• v = b, then w = bb ∈ R.

• v = b(ba)^{i}(ab)^{j}b, then

w ∈ ( \begin{matrix}& b(ba)^{i+1}(ab)^{j}b \\ ∪ & b(ba)^{i}(ab)^{j+1}b \\ ∪ & b(ba)^{i−1}bbba(ab)^{j−1}b \\ ∪ & b(ba)^{i−1}abbb(ab)^{j−1}b \end{matrix} ) ⊂ R.

• v = b(ba)^{i}ab(bb)^{j+1}(ab)^{l}b, then

w ∈ ( \begin{matrix}& b(ba)^{i+1}ab(bb)^{j+1}(ab)^{l}b \\ ∪ & b(ba)^{i}ab(bb)^{j+1}(ab)^{l+1}b \\ ∪ & b(ba)^{i−1}ab(bb)^{j+2}(ab)^{l}b \\ ∪ & b(ba)^{i−1}bbba(bb)^{j+1}(ab)^{l}b \end{matrix} ) ⊂ R

• The other cases are treated similarly.