Conway \(B\), Theorem 4.11, applied to \(x_1\sim x_2\) gives \(x_1y_1\sim x_2y_1\). To replace the second factor, use product commutativity from Theorem 4.2, apply Theorem 4.11 to \(y_1\sim y_2\) with common factor \(x_2\), and commute back. This gives \(x_2y_1\sim x_2y_2\). Transitivity of game equivalence in Theorem 2.7 composes the two replacements.

Use the three-game well-founded induction of Definition 2.6. Lemma 2.3 makes every option replacement smaller. We strengthen the induction statement as follows: associativity may be used for any triple whose three birthdays are bounded by those of \((a,b,c)\), provided at least one bound is strict. Thus, if \(a',b',c'\) are chosen options, the induction hypothesis contains all seven equivalences

We next compare a nested product option under the two bracketings. For options \(a',b',c'\), we claim that:

We prove this by expanding the left side and the right side separately. First, \(\operatorname {M}(a',b;a,b')=a'b+ab'-a'b'\), so distributivity gives

This is where the second equivalence of Lemma 4.4 is used: right-distributivity produces the terms

Substituting the seven strengthened induction hypotheses into this equality gives

For the other bracketing, \(\operatorname {M}(b',c;b,c')=b'c+bc'-b'c'\). Expanding directly gives

Here the first equivalence of Lemma 4.4 is used in the two terms

The right sides of the last two class expansions differ only by the order and association of their summands. The additive commutative group structure of Theorem 3.9 therefore gives

This proves the claim.

We now apply this claim to the option families of Definition 4.1. First choose an \(LL\) option of \((ab)c\) whose selected left option of \(ab\) is itself \(LL\). For \(a^L\in A^L,b^L\in B^L,c^L\in C^L\), it is

The game \(\operatorname {M}(b^L,c;b,c^L)\) is an \(LL\) left option of \(bc\), so

is an \(LL\) left option of \(a(bc)\). The preceding calculation with \((a',b',c')=(a^L,b^L,c^L)\) gives \(L\sim L'\).

For a mixed example, choose an \(LR\) right option of \((ab)c\), again using an \(LL\) left option of \(ab\). With \(c^R\in C^R\), it is

Now \(\operatorname {M}(b^L,c;b,c^R)\) is an \(LR\) right option of \(bc\), and

is the corresponding \(LR\) right option of \(a(bc)\). The calculation with \((a',b',c')=(a^L,b^L,c^R)\) gives \(R\sim R'\).

The remaining cases choose \(a^R,b^R,c^L,c^R\) according to the outer and inner \(LL,RR,LR,RL\) families. Reversing the calculation matches options from \(a(bc)\) back to \((ab)c\). Definition 2.9 shows that every chosen option of \(a,b,c\) is surreal, so the seven strengthened recursive associativity statements apply. Thus the left and right option lists match up to equivalence in both directions. Theorem 2.8 yields \((ab)c\sim a(bc)\).