For \(a+0=a\), use the one-game induction scheme of Definition 2.6. Write \(a=\{ A^L\mid A^R\} \). By Definition 3.1, the left and right option lists of \(a+0\) are respectively

Every option has smaller birthday by Lemma 2.3, so the induction hypothesis identifies these entries literally with \(u\) and \(v\). Thus the two option lists agree with those of \(a\), and hence \(a+0=a\) as game trees. The proof of \(0+a=a\) is the same, with the summands interchanged.

For commutativity, use the two-game induction scheme of Definition 2.6. By Definition 3.1, a left option of \(a+b\) is either \(a^L+b\) or \(a+b^L\). In the first case Lemma 2.3 makes \((a^L,b)\) a smaller pair, and the induction hypothesis gives

the right-hand side is a left option of \(b+a\). In the second case the smaller pair \((a,b^L)\) gives

The two right-option cases are identical, and interchanging \(a,b\) gives the converse matching. Theorem 2.8 now yields \(a+b\sim b+a\).

Associativity is stronger: it is literal equality of game trees. Apply the one-game induction scheme of Definition 2.6 successively to \(a\), \(b\), and \(c\), generalizing the later variables at each stage. The resulting induction hypotheses are

and the analogous three identities for right options. Each recursive call is legitimate by Lemma 2.3; generalizing the later coordinates permits the other two games to remain unchanged.

Expanding Definition 3.1 twice, the left option lists are

We use \(\cup \) for the union of these finite option collections; formally, the underlying lists retain order and multiplicity. On the left the three sublists are parenthesized as \((A^L\cup B^L)\cup C^L\), whereas on the right they are parenthesized as \(A^L\cup (B^L\cup C^L)\). Associativity of finite-list concatenation first identifies these two parenthesizations. The lists then contain the same three families in the same order; only their entries differ. The first, second, and third induction hypotheses above give pointwise equality on \(A^L,B^L,C^L\), respectively. Consequently the three corresponding sublists are equal, and therefore the complete left lists are equal. Replacing \(A^L,B^L,C^L\) by \(A^R,B^R,C^R\) proves equality of the right lists in the same way. The two games have identical left and right option lists, so \(((a+b)+c)=a+(b+c)\) literally.

We first prove simultaneously, in both directions, the equivalence

Use the three-game induction scheme of Definition 2.6, with measure \(\operatorname {bd}(a)+\operatorname {bd}(b)+\operatorname {bd}(c)\), and use the comparison of Definition 2.4 throughout.

Suppose first that \(a+c\preceq b+c\). If \(a^L\) is a left option of \(a\) and \(b\preceq a^L\), the induction hypothesis for \((b,a^L,c)\) gives \(b+c\preceq a^L+c\). Transitivity from Theorem 2.7, together with the assumed comparison, gives \(a+c\preceq a^L+c\). This is impossible because Definition 3.1 makes \(a^L+c\) a left option of \(a+c\), while the left-option clause of the reflexive comparison \(a+c\preceq a+c\) forbids such an inequality. If \(b^R\) is a right option of \(b\) and \(b^R\preceq a\), the induction hypothesis gives \(b^R+c\preceq a+c\); composing with the assumed comparison contradicts the right-option clause of the reflexive comparison \(b+c\preceq b+c\). Thus \(a\preceq b\).

Conversely, assume \(a\preceq b\). By Definition 3.1, the left options of \(a+c\) are \(a^L+c\) and \(a+c^L\), while the right options of \(b+c\) are \(b^R+c\) and \(b+c^R\). If \(b+c\preceq a^L+c\), the induction hypothesis for \((b,a^L,c)\) gives \(b\preceq a^L\), contrary to the left-option clause of \(a\preceq b\). If \(b+c\preceq a+c^L\), the induction hypothesis for \((a,b,c^L)\) gives \(a+c^L\preceq b+c^L\). Transitivity would then give \(b+c\preceq b+c^L\), contradicting the left-option clause of the reflexive comparison \(b+c\preceq b+c\). The right-option cases are dual. A comparison \(b^R+c\preceq a+c\) reflects to \(b^R\preceq a\), which is forbidden by \(a\preceq b\). Finally, if \(b+c^R\preceq a+c\), the induction hypothesis for \((a,b,c^R)\) gives \(a+c^R\preceq b+c^R\); transitivity would imply \(a+c^R\preceq a+c\), contrary to the right-option clause of the reflexive comparison \(a+c\preceq a+c\). This proves the reverse implication in the displayed equivalence. Every recursive call decreases because the coordinate replaced in it is an option, hence has smaller birthday by Lemma 2.3.

Commutativity from Theorem 3.2 turns the displayed equivalence into the corresponding equivalence for addition on the left. If \(a\preceq c\) and \(b\preceq d\), change first one summand and then the other, and compose the two inequalities using Theorem 2.7; this proves two-variable monotonicity. Suppose, for example, that \(a\prec c\) and \(b\preceq d\). Weak monotonicity gives \(a+b\preceq c+d\). If the reverse comparison held, then

Cancelling the common summand \(b\) by the displayed translation equivalence would give \(c\preceq a\), contradicting \(a\prec c\). Thus \(a+b\prec c+d\). Strictness in the second variable is proved symmetrically. Applying the weak result in both directions proves compatibility with \(\sim \).

Use the two-game induction scheme of Definition 2.6 to prove

Assume first \(a\preceq b\). By Definition 3.4, a left option of \(-b\) has the form \(-b^R\), and a right option of \(-a\) has the form \(-a^L\). If \(-a\preceq -b^R\), the induction hypothesis for \((b^R,a)\) gives \(b^R\preceq a\), contradicting the right-option clause of \(a\preceq b\) in Definition 2.4. Likewise, if \(-a^L\preceq -b\), the induction hypothesis for \((b,a^L)\) gives \(b\preceq a^L\), contradicting the left-option clause. These are exactly the two clauses required for \(-b\preceq -a\).

Conversely, assume \(-b\preceq -a\). To verify \(a\preceq b\), let \(a^L\) be a left option of \(a\). A comparison \(b\preceq a^L\) would, by the induction hypothesis for \((b,a^L)\), imply \(-a^L\preceq -b\), contradicting the right-option clause of \(-b\preceq -a\). The argument for a right option \(b^R\) is the same: \(b^R\preceq a\) would imply \(-a\preceq -b^R\), contradicting the left-option clause. Each induction step is valid by Lemma 2.3.

Applying the displayed equivalence to both weak inequalities in Definition 2.5 proves the stated biconditional for equivalence. Applying it to the forward weak inequality and to the excluded reverse inequality proves the strict-order equivalence. Both conclusions use Definitions 2.4 and 2.5.

We argue by induction on \(\operatorname {bd}(x)\), using the one-game scheme of Definition 2.6. Put \(s=x+(-x)\). We prove the two inequalities in the definition of \(s\sim 0\) from Definition 2.5. Since \(0=\{ \, \mid \, \} \) by Definition 2.1, the clauses involving options of \(0\) are vacuous.

By Definitions 3.1 and 3.4, a left option of \(s\) is either

In the first case \(x^L+(-x^L)\) is a right option of \(\ell \); in the second case \(x^R+(-x^R)\) is a right option of \(\ell \). By Lemma 2.3 and the induction hypothesis, the indicated self-cancelling game is equivalent to \(0\), and in particular is weakly below \(0\). Therefore \(0\preceq \ell \) would violate the right-option clause of that comparison. This verifies the left-option clause of \(s\preceq 0\).

Similarly, a right option of \(s\) is either

The first has \(x^R+(-x^R)\) as a left option, and the second has \(x^L+(-x^L)\) as a left option. The induction hypothesis makes that left option weakly above \(0\). Thus \(r\preceq 0\) would violate its left-option clause. This proves \(0\preceq s\), and hence \(x+(-x)\sim 0\). Commutativity from Theorem 3.2 gives \((-x)+x\sim 0\).