証明に現れる還元を全て列挙する。
コレらが還元になっている事は後で示す。
F以外は全て強還元である。
A〜Gの図の定義も兼ねている。

@A|B (初手実行)
ーー  | ㊀ー
㊀ーー | ー㊀ー

AB|C,D(初手実行)
    | ◯   
㊀ー  | ー㊀  ㊀㊀
 ㊀ー | ー㊀ー、 ー㊀

BC|E(初手実行)
ー   | ー◯  
㊀㊀  | ㊀ー◯

CE|B(終端優先)
ー ◯  | ㊀◯  
㊀ー◯ | ー㊀◯

DD|F,G(初手実行)
    |  ◯
㊀㊀  | ㊀ー◯ ㊀㊀◯
  ㊀ |   ㊀、  ー◯

EF|B(終端優先)
 ◯  | ◯ ◯
㊀ー◯ | ー㊀◯ 
  ㊀ |   ㊀

FG|B(終端除去)
    | ㊀◯
㊀㊀◯ | ー㊀◯