Index: lib/doc/nim.txt
==================================================================
--- lib/doc/nim.txt
+++ lib/doc/nim.txt
@@ -47,18 +47,14 @@
     は成り立たない！ *2 + *1 は 初手で *1 + *1 に行けるのでこれは勝てる
 
 補題：G+G は必敗
 　- まねっこmoveをされると負けるしかない
 
+-------------------------------------------------------------------------------------------
 補題：A≡A', B≡B' ならば A+B≡A'+B'
   - A+B+A'+B' = (A+A')+(B+B') = 必敗+必敗 = 必敗
 
-補題：Ai≡Ai' ならば {A0,A1,A2,...}≡{A0',A1',A2',...}
-　- {A0,A1,A2,...}+{A0',A1',A2',...} は必敗。なぜならこちらがどう動かしても
-    A0+A0', A1+A1', A2+A2', ... のいずれかの必敗状態に遷移させられるから。
-
--------------------------------------------------------------------------------------------
 定理【ゲームの和はxor】
   - *n1 + *n2 = *(n1 xor n2)
   - より一般的に G1≡*n1, G2≡*n2 ならば、G1 + G2 ≡ *(n1 xor n2)
 
   証明
@@ -73,10 +69,14 @@
         >> 偶数個(2個)なら、その最上位ビットを無視した残りをa',b',c'とするとこれも
         >> xorがxなので数学的帰納法的にやることにより巧い減らし方が見つかる。
     - よって最終局面"全部 0"になるのは絶対に自分のターン
 
 -------------------------------------------------------------------------------------------
+補題：Ai≡Ai' ならば {A0,A1,A2,...}≡{A0',A1',A2',...}
+　- {A0,A1,A2,...}+{A0',A1',A2',...} は必敗。なぜならこちらがどう動かしても
+    A0+A0', A1+A1', A2+A2', ... のいずれかの必敗状態に遷移させられるから。
+
 定理【ゲームの状態遷移はmex】
   - {*n1, ..., *nk} ≡ *mex(n1,...,nk)
       where mex(S) = min(nat \setminus S)
 
   - より一般的に G1≡*n1, ..., Gk≡*nk ならば、G={G1, ..., Gk} ≡ *mex(n1,...,nk)
@@ -93,12 +93,42 @@
 
 -------------------------------------------------------------------------------------------
 まとめ
 
 ・一手動かした次の局面が *n1 または *n2 または ... なゲーム
-　　{*n1, ..., *nk} = *mex(n1, ..., nk)
+　　{*n1, ..., *nk} ≡ *mex(n1, ..., nk)
+
 ・ゲーム *n1 と *n2 とどちらかを選んで一手進められるゲーム
-　　*n1 + *n2 = *(n1 xor n2)
-・ゲーム *n1 と *n2 とどちらか一方または両方一気に進められるゲーム
-　　*n1 <+> *n2 = *(n1 + n2)     //単に１個の山なのとかわらない
-・両方一手ずつ進めるゲーム？？？？？
-　　*n1 X *n2 = ?
+　　*n1 + *n2 ≡ *(n1 xor n2)
+
+
+-------------------------------------------------------------------------------------------
+その他のゲームの組み合わせ（証明があやしい）
+
+定理： ゲーム *n1 と *n2 とどちらか一方または両方一気に進められるゲーム
+　　*n1 <+> *n2 ≡ *(n1 + n2)
+証明： 単に１個の山なのとかわらないので勝敗一致どころか同型
+
+補題：A≡A' かつ B≡B' ならば (A<+>B)≡(A'<+>B')。
+　　　ゆえに一般に G1≡*n1, G2≡*n2 ならば G1<+>G2 ≡ *(n1+n2)
+証明：(A<+>B)+(A'<+>B')が必敗であることを言えばよい。
+　　　相手がどう動かしても A<+>B ==> a<+>b
+　　　a+a'、b+b'が必敗であるように (a<+>b)+(a'<+>b') と動かせる。
+　　　いずれ相手は死ぬ
+
+
+定理： 先手はゲーム *n1、後手はゲーム *n2 を交互に一手ずつ進めるゲーム
+　　*n1 X *n2 ≡ *(n1<=n2 ? 0 : n2+1)
+　　　　　　  後手
+　　       0 1 2 3 4
+　　------+----------
+　　先手 0|0 0 0 0 0
+　　     1|1 0 0 0 0
+　　     2|1 2 0 0 0
+　　     3|1 2 3 0 0
+　　     4|1 2 3 4 0
+　左辺のゲームのmex計算してみるとこうなる。
+
+補題：A≡A' かつ B≡B' ならば (A X B)≡(A' X B')。
+　　　ゆえに一般に G1≡*n1, G2≡*n2 ならば G1 X G2 ≡ *(n1<=n2 ? 0 : n2+1)
+証明：AxB + A'xB' を Bxa + A'xB' と動かされたら Bxa + B'xa' に動かせて≡が
+　　　保てるのでいずれ相手は死ぬ