GE:=proc(x,y) local xR, yL: evalb( {true,seq( evalb( not GE(y,xR)), xR in x[2])}={true} and {true,seq( evalb( not GE(yL,x)), yL in y[1])}={true} ): end: #LE(x,y) is x<=y? LE:=proc(x,y):GE(y,x): end: #EQ(x,y): is x=y in Conway's sense EQ:=proc(x,y): GE(x,y) and LE(x,y):end: #GT(x,y): x>y ? GT:=proc(x,y): GE(x,y) and not GE(y,x) : end: #LT(x,y): x= member of R (x[2]) if member(true,{seq(seq(GE(xL,xR), xL in x[1]), xR in x[2])}) then RETURN(false): fi: true: end: #ADD(x,y): x+y=[{xL+y,x+yL}, {xR+y,x+yR}] ADD:=proc(x,y) local xL, xR, yL, yR: option remember: [ { seq( ADD(xL,y), xL in x[1]), seq( ADD(x,yL), yL in y[1])}, { seq( ADD(xR,y), xR in x[2]), seq( ADD(x,yR), yR in y[2])} ]: end: #SN(N): the surreal rendition of the pos. integer N SN:=proc(N) option remember: if N=0 then [{},{}]: else [ {SN(N-1)}, {}]: fi: end: Minus:=proc(x) local xR, xL: option remember: [ {seq(Minus(xR), xR in x[2])}, {seq(Minus(xL), xL in x[1])} ]: end: NaiveMul := proc(a, n) option remember: if n = 0 then return [{}, {}]: fi: return ADD(a, NaiveMul(a, n-1)): end: CheckNaiveMul := proc(K) local i, j: for i from 1 to K do for j from 1 to K do if not EQ(NaiveMul(SN(i), j), SN(i*j)) then return false: fi: od: od: return true: end: MUL := proc(x, y) local nx1, nx2, ny1, ny2: option remember: nx1 := {seq(seq(Minus(ADD(MUL(xL,y), MUL(x,yL)), MUL(xL,yL)) , yL in y[1]), xL in x[1])}: nx2 := {seq(seq(Minus(ADD(MUL(xR,y), MUL(x,yR)), MUL(xR,yR)) , yR in y[2]), xR in x[2])}: ny1 := {seq(seq(Minus(ADD(MUL(xL,y), MUL(x,yR)) ,MUL(xL,yR)) , yR in y[2]), xL in x[1])}: ny2 := {seq(seq(Minus(ADD(MUL(xR,y), MUL(x,yL)), MUL(xR,yL)) , yL in y[1]), xR in x[2])}: return [nx1 union nx2, ny1 union ny2]: end: