In \(a0\), the second factor has no options. Expanding the recursive cut in Definition 4.1 therefore gives two empty option lists, so \(a0=0\) as literal game trees. The same direct expansion of \(0a\) has no option in any of the four families, because the first factor has no options; hence \(0a=0\) literally as well.

For commutativity, use the two-game well-founded induction of Definition 2.6; every recursive pair is smaller by Lemma 2.3. Split an option according to the four families in Definition 4.1. For a same-side example, the \(LL\) option of \(ab\) determined by \((a^L,b^L)\) is

The \(LL\) option of \(ba\) determined by \((b^L,a^L)\) is

The induction hypotheses for the three smaller pairs \((a^L,b)\), \((a,b^L)\), and \((a^L,b^L)\) identify, respectively, \(a^Lb\sim ba^L\), \(ab^L\sim b^La\), and \(a^Lb^L\sim b^La^L\). Additive commutativity is Theorem 3.2, compatibility of addition with \(\sim \) is part of Theorem 3.3, and compatibility of negation with \(\sim \) is part of Theorem 3.5. These three results therefore make the two displayed options equivalent. The \(RR\) case is the identical calculation with \(a^L,b^L\) replaced by \(a^R,b^R\):

A mixed-side option changes family when the factors are swapped. The \(LR\) option

is matched not with another \(LR\) option, but with the \(RL\) option

of \(ba\). The induction hypotheses for \((a^L,b)\), \((a,b^R)\), and \((a^L,b^R)\) identify its three terms after the same additive rearrangement. Dually,

so an \(RL\) option of \(ab\) matches an \(LR\) option of \(ba\). Repeating these matches from \(ba\) back to \(ab\), for both the left and right option lists, supplies the four hypotheses of Theorem 2.8; hence \(ab\sim ba\). The two literal zero identities already prove both displayed zero laws.

Finally, prove the literal equality \(a1=a\) by the one-game induction of Definition 2.6. By Definition 2.1, \(1=\{ 0\mid \} \). Thus an \(LL\) option of \(a1\) is

and an \(RL\) option is the same expression with \(a^R\) in place of \(a^L\); the other two families are empty. The induction hypothesis gives \(a^L1=a^L\) and \(a^R1=a^R\), while the zero-product identity established above, the additive zero laws in Theorem 3.2, and the identity \(-0=0\) in Definition 3.4 reduce the displayed expressions to \(a^L\) and \(a^R\). Hence the left and right option lists of \(a1\) are literally those of \(a\). The commutativity conclusion already proved then gives \(1a\sim a\).

Prove the first equivalence by the three-game well-founded induction of Definition 2.6. Lemma 2.3 shows that every recursive triple is smaller. For an option of \(a(b+c)\), Definition 4.1 first distinguishes whether the changed coordinate is \(a\) or \(b+c\); in the second case, Definition 3.1 distinguishes whether the changed coordinate is \(b\) or \(c\). The matching option of \(ab+ac\) changes the same coordinate in the corresponding summand. Conversely, an option of the sum changes either \(ab\) or \(ac\), and Definition 4.1 determines the corresponding option on the left. This gives four left/right matching assertions, two in each direction.

For example, let \(a^L\) and \(b^L\) be left options. The corresponding \(LL\) option on the left is

The matching left option on the right is

The three smaller induction hypotheses give

Substitution in the definition of \(\operatorname {M}\) gives

The cancellation in the second step takes place in the auxiliary quotient of Definition 3.8, with its ordered additive group structure from Theorem 3.9. Every remaining membership branch uses one of the same two algebraic templates, according as the changed summand is \(b\) or \(c\); reverse-direction branches use symmetry of the resulting equivalence. Left and right options are placed as prescribed by Definition 4.1. Compatibility with sums and negatives and additive-group normalization follow from Theorem 3.9, which puts each pair of signed sums in the same form. By the quotient relation in Definition 3.8, equality of their classes is precisely game equivalence. The four matches now satisfy Theorem 2.8, proving \(a(b+c)\sim ab+ac\).

Finally,

The first equivalence uses product commutativity from Theorem 4.2; the middle equivalence is the left-distributive result just proved; and the last uses product commutativity inside the two summands together with addition congruence from Theorem 3.3.

Prove the first equivalence by the two-game induction of Definition 2.6. Let \(u'\) be either a left or a right option of \(u\), and let \(v'\) be either a left or a right option of \(v\). The three smaller induction hypotheses are

In the auxiliary quotient, these hypotheses give

Equality of the first and last classes means

Definition 3.4 gives \(({-v})^L=-v^R\) and \(({-v})^R=-v^L\). Consequently, applying \((*)\) to the indicated choices gives the two left-option matches

and the two right-option matches

The expressions on the right in the first display are precisely the negatives of the two right options of \(uv\), hence are left options of \(-(uv)\); those in the second display are the negatives of the two left options of \(uv\), hence are right options of \(-(uv)\). Reading the same matches in reverse supplies the converse directions. Thus Theorem 2.8 proves \(u(-v)\sim -(uv)\).

Finally,

The first and last steps use product commutativity from Theorem 4.2, with negation congruence from Theorem 3.5 in the last step; the middle step is the first equivalence.