• branch=trunk inherited from [9165bd3629]
• sym-trunk inherited from [9165bd3629]

Modified lib/doc/nim.txt from [b75bd46f8bc82eec] to [afbe18987eb71e60].

    45     45       注意：
    46     46         必勝 + 必勝 = 必敗
    47     47       は成り立たない！ *2 + *1 は 初手で *1 + *1 に行けるのでこれは勝てる
    48     48   
    49     49   補題：G+G は必敗
    50     50   　- まねっこmoveをされると負けるしかない
    51     51   
           52  +-------------------------------------------------------------------------------------------
    52     53   補題：A≡A', B≡B' ならば A+B≡A'+B'
    53     54     - A+B+A'+B' = (A+A')+(B+B') = 必敗+必敗 = 必敗
    54     55   
    55         -補題：Ai≡Ai' ならば {A0,A1,A2,...}≡{A0',A1',A2',...}
    56         -　- {A0,A1,A2,...}+{A0',A1',A2',...} は必敗。なぜならこちらがどう動かしても
    57         -    A0+A0', A1+A1', A2+A2', ... のいずれかの必敗状態に遷移させられるから。
    58         -
    59         --------------------------------------------------------------------------------------------
    60     56   定理【ゲームの和はxor】
    61     57     - *n1 + *n2 = *(n1 xor n2)
    62     58     - より一般的に G1≡*n1, G2≡*n2 ならば、G1 + G2 ≡ *(n1 xor n2)
    63     59   
    64     60     証明
    65     61       - *n1 + *n2 + *(n1 xor n2) が必敗であることを言えば良い。
    66     62       - (n1 xor n2 xor (n1 xor n2)) は 0 である
................................................................................

    71     67           >> つまりa,b,cのどれかは^xすると減ることを言えばよい。
    72     68           >> a,b,cのうち最上位ビットが立っているものが奇数個ならxも立つのでxorすれば減る
    73     69           >> 偶数個(2個)なら、その最上位ビットを無視した残りをa',b',c'とするとこれも
    74     70           >> xorがxなので数学的帰納法的にやることにより巧い減らし方が見つかる。
    75     71       - よって最終局面"全部 0"になるのは絶対に自分のターン
    76     72   
    77     73   -------------------------------------------------------------------------------------------
           74  +補題：Ai≡Ai' ならば {A0,A1,A2,...}≡{A0',A1',A2',...}
           75  +　- {A0,A1,A2,...}+{A0',A1',A2',...} は必敗。なぜならこちらがどう動かしても
           76  +    A0+A0', A1+A1', A2+A2', ... のいずれかの必敗状態に遷移させられるから。
           77  +
    78     78   定理【ゲームの状態遷移はmex】
    79     79     - {*n1, ..., *nk} ≡ *mex(n1,...,nk)
    80     80         where mex(S) = min(nat \setminus S)
    81     81   
    82     82     - より一般的に G1≡*n1, ..., Gk≡*nk ならば、G={G1, ..., Gk} ≡ *mex(n1,...,nk)
    83     83       帰納的に、全てのゲームはなんらかの *n と等価
    84     84   
................................................................................

    91     91         で両側等価を保ててしまう。
    92     92   
    93     93   
    94     94   -------------------------------------------------------------------------------------------
    95     95   まとめ
    96     96   
    97     97   ・一手動かした次の局面が *n1 または *n2 または ... なゲーム
    98         -　　{*n1, ..., *nk} = *mex(n1, ..., nk)
           98  +　　{*n1, ..., *nk} ≡ *mex(n1, ..., nk)
           99  +
    99    100   ・ゲーム *n1 と *n2 とどちらかを選んで一手進められるゲーム
   100         -　　*n1 + *n2 = *(n1 xor n2)
   101         -・ゲーム *n1 と *n2 とどちらか一方または両方一気に進められるゲーム
   102         -　　*n1 <+> *n2 = *(n1 + n2)     //単に１個の山なのとかわらない
   103         -・両方一手ずつ進めるゲーム？？？？？
   104         -　　*n1 X *n2 = ?
          101  +　　*n1 + *n2 ≡ *(n1 xor n2)
          102  +
          103  +
          104  +-------------------------------------------------------------------------------------------
          105  +その他のゲームの組み合わせ（証明があやしい）
          106  +
          107  +定理： ゲーム *n1 と *n2 とどちらか一方または両方一気に進められるゲーム
          108  +　　*n1 <+> *n2 ≡ *(n1 + n2)
          109  +証明： 単に１個の山なのとかわらないので勝敗一致どころか同型
          110  +
          111  +補題：A≡A' かつ B≡B' ならば (A<+>B)≡(A'<+>B')。
          112  +　　　ゆえに一般に G1≡*n1, G2≡*n2 ならば G1<+>G2 ≡ *(n1+n2)
          113  +証明：(A<+>B)+(A'<+>B')が必敗であることを言えばよい。
          114  +　　　相手がどう動かしても A<+>B ==> a<+>b
          115  +　　　a+a'、b+b'が必敗であるように (a<+>b)+(a'<+>b') と動かせる。
          116  +　　　いずれ相手は死ぬ
          117  +
          118  +
          119  +定理： 先手はゲーム *n1、後手はゲーム *n2 を交互に一手ずつ進めるゲーム
          120  +　　*n1 X *n2 ≡ *(n1<=n2 ? 0 : n2+1)
          121  +　　　　　　  後手
          122  +　　       0 1 2 3 4
          123  +　　------+----------
          124  +　　先手 0|0 0 0 0 0
          125  +　　     1|1 0 0 0 0
          126  +　　     2|1 2 0 0 0
          127  +　　     3|1 2 3 0 0
          128  +　　     4|1 2 3 4 0
          129  +　左辺のゲームのmex計算してみるとこうなる。
          130  +
          131  +補題：A≡A' かつ B≡B' ならば (A X B)≡(A' X B')。
          132  +　　　ゆえに一般に G1≡*n1, G2≡*n2 ならば G1 X G2 ≡ *(n1<=n2 ? 0 : n2+1)
          133  +証明：AxB + A'xB' を Bxa + A'xB' と動かされたら Bxa + B'xa' に動かせて≡が
          134  +　　　保てるのでいずれ相手は死ぬ