We consider "games" in the sense of ONAG. Conway's definition of a game $G$ as a pair $G = \{L \mid R \}$ of sets of games, together with the definitions of inequality and the arithmetic operations (ONAG, p.78), may be taken directly as a decision procedure for equality at least in the case of *short* games (i.e., games with a finite number of positions). See, for example, this naive Haskell implementation. However, the naive decision procedure seems to be hopelessly inefficient for all but the simplest examples (e.g., my laptop and patience are too limited to decide 3*3=9). In particular, this definition of the arithmetic operations leads to very large normal forms for games.

So my question is: has anyone tried to develop efficient algorithms for doing arithmetic with Conway games and deciding (in)equality? For simplicity (and to avoid issues of undecidability), you can limit to the case of short games. In particular, I wonder whether it is possible to compute efficiently with "the simplest form of a short game" (p.111)?