二人零和有限確定完全情報ゲームが先手不敗か後手不敗のどちらかであることを証明できるから証明してみた

二人零和有限確定完全情報ゲームGでプレイヤーA,B2人が対戦、A先手、かつ下記とする。

• [仮定1] A,Bいずれも自分の手番で手xを打てば相手の負けが確定する場合、ミスなくその手xを打つ

Gのゲーム木の高さについて、それが2以下の場合首記定理の成立は自明なので、3以上の場合を考える。
Gの状態は、互いに背反な下記4種類しかない。

• Ab: Aの手番で、Aの合法手が存在する
• AX: Aの手番で、Aの合法手が存在しない(A負けまたはAB引き分け)
• Ba: Bの手番で、Bの合法手が存在する
• BX: Bの手番で、Bの合法手が存在しない(B負けまたはAB引き分け)

ゲームの終わり方としてはAXかBXのどちらかしかなく両者は背反だから、Gのゲーム木の葉はAXのものとBXのものの混在であり、それ以外にない。
さらに手番が交互という制約が存在するから、葉から2ノードだけ根側のノードから葉に至る経路はAb→Ba→AX か、Ba→Ab→BXのいずれかのみで他にない。

さて、Ab→Ba→AX のケースを考える。このノードAbにおいて、Ab→BXのタイプの遷移が別途存在するなら、仮定1よりAはそちらを実行するから、Ab→Ba→AXのかわりにAb→BXでゲームが終わる。そうでないなら、Abの時点でAXでゲームが終わることが決定づけられる(∵Bについての仮定1)。
前者の場合、Gのルールを変えることなく非到達ノードBa、AXを消去できる。後者の場合、(Gのルールを変えることにはなるが)Ab→Ba→AXというパスをAXに置き換えてもAXでゲームが終わるという結論が変わらないから、いずれにせよゲームの勝敗を変えることなくBaとAXを消去できる。

Ba→Ab→BXのケースにおけるBaの局面について考えても同じ事で、AbとBXを消去できる。

上記消去操作を可能な限り繰り返すと、有限回の反復で次の2通りのうちいずれかが残る(A先手なので根は必ずAbである)。
　[1] 根からの全てのパスがAb→Ba→AXのタイプ
　[2] 根からの全てのパスがAb→BXのタイプ
[1]なら後手不敗、[2]なら先手不敗。(おわり)