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' に動かせて≡が
+ 保てるのでいずれ相手は死ぬ