6 6 6 6 6 + +
6 6 6 6 6 z y
6 6 6 6 + +
6 6 6 x
6 6
6 6 w
6 6 6 1
1 2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 22: Case6
- - - - - -
-- - - - - - y
- - - - -
-- - - x
-
-- - w
- -1
1 2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 23: Case ‘root’
定理10が実際の応用で適用されるのは，次のような場合である: xとwの位置に黒 石が着手され，このとき，図11の ‘ - ’のセルからなる集合は空セルの集合である．そ の後，交互に石を置いていく．部分局面F に後手（白）の着手が行われたとき，次に先 手は図12の深さ2の節点に関連する着手を行う．yのセルに先手が着手したとき，定 理10により，(t−x∧t−w∨t−b)∧(t−y∨x−y)が成り立つ．
実際の応用に際しては，部分局面における後手の着手に対して先手の応手を予め決 めておく．これにより，S上の着手を考慮せずに，盤面全体の探索（必勝手順の検証）
が進められる．こうして繰り返しの記述と場合分けが不要になり，検証も簡単になる．
次の3.3節で，σ連結とσ拡張を用いた先手勝ちの証明の実例を示す．
除）の対象とする．盤面全体のセルに対し先行排除をする必要がないため，場合分け の数が減少する．結果として，詳しい解析（深い探索）が必要ない．このことは次の 命題11によって得ることができる．
ここで，深い探索が必要でないとは，次のことを意味する．その局面は後手局面で あるが，この局面以降の後手の着手は強制される．すなわち，後手の着手はそれ以後 一意的に（あるいは複数あるが自明であるという意味で一意的に）定まる．ちょうど 将棋において，王手の連続で詰む場合，先手側の王手だけでなく，王側の応手も一意 的に決っていくという特別な状況に相当する．そこで，深い探索が必要でない局面に は，この強制着手手順を付記した先手勝ちの証明を与える．命題11では，この強制着 手手順をFで表す．
命題 11 次の8×8の盤面（後手局面）は先手（黒）勝ちである．
- - - - - -
-- - - - - - 4 3
- - - - -
-- - - x 2
- - + +
- - w 1
- -1
1 2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 24: 命題11 先手（黒）勝ち
F: ◦ {37, 28, 38} • ‘ 1 ’ ◦ {56} •‘ 2 ’ ◦ {64} • ‘ 3 ’ ◦ {81} •‘ 4 ’ （部分局面F に関するσ拡張（定理10））.
（証明）図24で示すように 54, 46のセル（黒石）をそれぞれx, wとする．‘ - ’ の セルからなる集合をF C，‘ + ’ のセルからなる集合をSとする．
F C上の空セルに後手が着手したときには，部分局面F に関するσ連結（図11）に 基づき先手は（σ連結の深さ2の節点に相当する）着手を行なうとする．
図11のすべての葉xに関連する局面に対し空セルの集合Kxが存在しAND-OR連 結Kx[tx∨tw∨tb]が成立する．定理8より，深さ偶数のすべての節点yに関連する局 面では，ある空セルの集合Kyが存在しAND-OR連結Ky[tx∨tw∨tb]が成立する．
また，S-lemmaよりS[xw]が成り立つ．
ある空セルの集合U が存在しS∩U =φかつKy ∩U =φかつU[wb]のとき，先手 勝ちであることを以下で示す．
S[xw]かつU[wb]かつS∩U =φより，(S∪U)[xw∧wb].（（1-1）より）
よって，(S∪U)[xw∧wb∧xb].（（1-5）より）
これより，(S∪U)[xb∧wb].（（1-2）と（1-6）より）
ここで，S∩U = φかつKy ∩U = φ より，(S∪U)∩Ky = φが成り立つ．また，
Ky[tx∨tw∨tb]が成り立つため，
(S∪U ∪Ky)[(tx∧xb∧wb)∨(tw∧xb∧wb)∨(tb∧xb∧wb)].（（3）より）
(S∪U∪Ky)[(tx∧xb∧wb∧tb)∨(tw∧xb∧wb∧tb)∨(tb∧xb∧wb)].（（1-5）
と（1-7）より）
(S∪U ∪Ky)[tb∨tb∨tb].（（1-2）と（1-7）より）
(S∪U ∪Ky)[tb].（（1-4）と（1-7）より）
同様に，ある空セルの集合Uが存在しS∩U =φかつKy ∩U =φかつU[xb]のと き，(S∪U ∪Ky)[tb]が成り立つ．
後手は先手のt−bを防ぐため，着手を37, 28, 38のどれかに強制される．次に，先 手は‘ 1 ’に着手する．このとき，T-lemma より ‘1’−bが成立するため（T-lemma の 空セルの集合をT とする），同様の理由により，後手は着手を56に強制される．上記 のような解析を繰り返すと，Fで示される強制着手が続く．
65, 75の空セルからなる集合をS1，73, 83の空セルからなる集合をS2とすると，黒
‘ 2 ’のときS-lemmaよりS1[‘1’‘2’]が成立し，黒‘ 3 ’のときS-lemmaよりS2[‘2’‘3’]が 成立する（図25）．‘3’と‘4’は直接連結するため，S2[‘2’‘4’]が成立する．
S1∩S2 =φより，(S1∪S2)[‘1’‘2’∧‘2’‘4’].（（1-1）より）
(S1 ∪S2)[‘1’‘2’∧‘2’‘4’∧‘1’‘4’].（（1-5）より）
(S1 ∪S2)[‘1’‘4’].（（1-2）と（1-6）より）
ここで，S1 ∩ T = φかつS2 ∩T = φより，(S1 ∪ S2)∩T = φである．よって，
C =T ∪S1∪S2とすると，C[‘1’b∧‘1’‘4’].（（1-1）より）
C[‘1’b∧‘1’‘4’∧‘4’b].（（1-1）より）
C[‘4’b].（（1-1）と（1-6）より）
また，定理10より，図12のすべての後手節点xに対し以下が成立する：図12のx が葉のとき，空セルの集合Kx′ ⊆e(S∪ {y})−Kxと和積形のAND-OR式γが存在し，
Kx′[γ]かつ(Kx∪Kx′)[(tx∨tw∨tb)∧(ty∨xy)]が成立し，xが葉でないとき，空セル の集合Kx′ ⊆e(S∪ {y})が存在し，Kx′[(tx∨tw∨tb)∧(ty∨xy)]が成立する．
xが葉のとき，以下が導ける．
(Kx∪Kx′)[(tx∧t‘4’)∨(tx∧x‘4’)∨(tw∧t‘4’)∨(tw∧x‘4’)∨(tb∧t‘4’)∨(tb∧x‘4’)].
（（2-1）より）
(Kx∪Kx′)[(tx∧t‘4’)∨(tx∧x‘4’∧t‘4’)∨(tw∧t‘4’)∨(tw∧x‘4’)∨(tb∧t‘4’)∨(tb∧x‘4’)].
（（1-5）と（1-7）より）
(Kx∪Kx′)[t‘4’∨t‘4’∨t‘4’∨(tw∧x‘4’)∨tb∨tb].（（1-2）と（1-7）より）
(Kx∪Kx′)[t‘4’∨(tw∧x‘4’)∨tb].（（1-4）と（1-7）より）
ここで，(Kx∪Kx′)∩C = φかつC[‘4’b]より，(Kx ∪Kx′ ∪C)[(t‘4’∧‘4’b)∨(tw∧ x‘4’∧‘4’b)∨(tb∧‘4’b)].（（2-1）より）
(Kx∪Kx′ ∪C)[(t‘4’∧‘4’b∧tb)∨(tw∧x‘4’∧‘4’b∧xb)∨(tb∧‘4’b)].（（1-5）と（1-7）
より）
(Kx∪Kx′ ∪C)[tb∨(tw∧xb)∨tb].（（1-2）と（1-7）より）
(Kx∪Kx′ ∪C)[tb∨(tw∧xb)].（（1-4）と（1-7）より）
ここで，(Kx∪Kx′)∩S =φかつC∩S =φより，(Kx∪Kx′∪C)∩S =φが成立する．また，
S[xw]が成立する．よって，L=Kx∪Kx′∪C∪Sとすると，L[(tb∧xw)∨(tw∧xb∧xw)].
（（3）より）
L[tb∨(tw∧xb∧xw)].（（1-2）と（1-7）より）
L[tb∨(tw∧xb∧xw∧wb)].（（1-5）と（1-6）と（1-7）より）
L[tb∨(tw∧xb∧xw∧wb∧tb)].（（1-5）と（1-6）と（1-7）より）
L[tb∨tb].（（1-2）と（1-6）と（1-7）より）
L[tb].（（1-4）より）
以上により，図24の盤面（後手局面）は先手勝ちである．
同様に，xが葉でないとき，t−bが成立することを導ける．
よって，命題11が成立する．
（証明終）
- - - - - -
-- - - - - - 4 3
- - - - - - + +
- - - x 2
- - + + + +
- - w 1 *
- - * * *
- * * * *
1 1
2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 25: 強制着手Fの後の局面
命題11と同様に，部分局面F に関するσ連結とσ拡張を用いることで，図26と図 27の盤面の先手勝ちを示せる．
図26では，初めの解析（先行排除）における後手の着手は47か48に絞られる．強 制着手は，前者に対してはF1となり，後者に対してはF2となる．これ以外の後手の 着手に対しては黒47か黒57によって先手勝ちとなる．
図27の強制着手をF3で示す．黒‘ 2 ’の着手のとき，76, 57, 67, 77, 68, 78の空セル からなる集合上で ‘ 2 ’−bが成り立つ．
このように，σ連結とσ拡張のおかげで，場合分けが減少し，使用する図も従来の方 法に比べて少数ですむ．
- - - - - -
-- - - - - - 6 5
- - - - -
-- - - x 4
- - + +
- - w 3
- - 1 2
-1
1 2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 26: 部分局面F に関するσ連結とσ拡張を用いた先手勝ちの盤面1
F1 : ◦ {47} • ‘ 3 ’ ◦ {56} • ‘ 4 ’ ◦ {64} • ‘ 5 ’ ◦ {81} • ‘ 6 ’ （部分局面F に関 するσ拡張）.
F2 : ◦ {48} •‘1’ ◦ {38} •‘ 2 ’ ◦ {57} •‘ 3 ’ ◦ {56} •‘ 4 ’ ◦ {64} •‘ 5 ’ ◦ {81}
• ‘ 6 ’ （部分局面F に関するσ拡張）.
- - - - - -
-- - - - - - 5 4
- - - - -
-- - - 3
- - + +
- - 2
-
-- 1
1 1
2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 27: 部分局面F に関するσ連結とσ拡張を用いた先手勝ちの盤面2
F3 : ◦ {38} • ‘ 1 ’ ◦ {47} • ‘ 2 ’ ◦ {56} • ‘ 3 ’ ◦ {64} • ‘ 4 ’ ◦ {81} • ‘ 5 ’ （部 分局面F に関するσ拡張）.
本論文のσ連結とσ拡張によって，8×8（初手54）の先手必勝手順を構成すること ができる．
必勝手順の証明木とは，準ゲーム木のことであり，偶数の深さの節点（∼P節点）の 子には，先行排除によって残った∼P の着手が関連付けられている（葉では先行排除 によりすべての着手が取り除かれている）．
本論文で構成した必勝手順の証明木を図28で示す（根以外の節点の数字は関連する 着手を示す）．根には，すべてのセルが空セルの局面から先手が初手54を着手した（後 手の）局面が関連付けられている．総節点数は13個で，先手局面に対応する節点が6 個，後手局面に対応する節点が7個からなっている．後手局面の節点では，（従来の必 勝手順のように）AND-OR連結に基づく先行排除が利用されている．それに加え，σ 連結とσ拡張に基づき，深い探索をしなくても（自明の強制着手によって）先手勝ち
を得られる局面（節点）は，証明木から排除されている．たとえば，根節点において，
白47の着手は，黒46によって命題11に帰結し先手勝ちとなるため，証明木から省か れている．同様に，白37，白28，白58の着手も黒46によって，先手勝ちとなる（図 26と図27）．これらの局面も証明木から取り除かれている．
54 45 56 57 55 46 47
38 27
48 46 46
56
図 28: 8×8（初手54）の証明木
本節の8×8（初手54）の必勝手順を示すために，基本となるσ連結は4個で（局面 F に関するσ連結を含む），そのうち1個はAB-propertyをもつAND-OR連結の着手 手順を示している（参考文献[17]のFigure 38）．さらに，部分局面F に関するσ連結 のバリエーションを2個用いる．よって，用いられるσ連結の総数は6個である．こ の必勝手順では，σ連結1個に対し1個のσ拡張を用いる（各σ連結に対し，定理10 のような証明を1個ずつ行っている）．よって，σ拡張の総数は6個である．
K. Noshitaの8×8（初手54）の必勝手順[18, 19]では，はじめに，必勝手順の証明 で用いられる主要な定理を示している．これらを証明するために必要な図面の数は31 個である．必勝手順の証明木の正しさを証明するために，各節点における（ユニオン 連結による）先行排除を示している．ここで用いられている図面の数は222個である．
証明文書全体で用いられている図面の数は，253個である．証明中では，ある節点（局 面）において，その祖先節点に同型の解析（先行排除）が現れる場合，祖先節点の解 析を参照することで，繰り返しの記述を省略している．必勝手順の証明木の節点数は，
108個である（後手節点は52個）．
本節の8×8（初手54）の必勝手順の正しさを証明する文書は，次のように構成され ている．最初に，主要なAND-OR連結を証明している．また，定理9と定理10のよ うに，先行排除で用いられるσ連結とσ拡張の正しさを証明している．これらを示す ために必要な図面の数は，34個である．必勝手順を示す証明木（図28）の各節点にお ける解析では，AND-OR連結による先行排除と，（命題11のような）σ 連結とσ拡張 を使った先手勝ちの証明が示されている．これらを示すために必要な図面の数は，65 個である（新技法を用いた証明は8個）．証明文書全体では，99個の図面を用いてい る．他の図を参照するなどの省略方法は用いていない．必勝手順の証明木の総節点数
は，前述したように，13個である（後手節点は7個）．
このように，σ連結とσ拡張を従来の証明法と併用することで，従来より簡単な形 で必勝手順を構築できる．