リーズニング・ステージとプログラミング

ステージ内に居るシーケントは：

1. 事実シーケント
2. 質問シーケント〈問題シーケント | ゴール〉

やること：

1. 事実シーケントの構成（味方を増強する）
2. 質問シーケントの分解（敵を衰弱させる／消滅させる）

ステージの種類は：

1. 連言導入用ステージ（連言成分〈ファクター | フィールド〉ごとにエリア）
2. 全称導入用ステージ
3. 選言除去用ステージ（選言成分〈ケース〉ごとにエリア）
4. 存在除去用ステージ
5. 含意導入用ステージ（k個の仮定があればk引数関数ができる）
6. 否定導入用（背理法用）ステージ
7. 帰納法用ステージ（帰納的定義ごとに各種）

プログラミングとの対応：

ステージ	プログラミング・パターン
連言導入用	タプル型戻し-関数用
全称導入用	パラメータ付き型戻し-多相関数用
選言除去用	ユニオン型引数-関数用 ケース文
存在除去用	パラメータ付き型引数用-多相関数
含意導入用	ラムダ抽象用
否定導入用	継続渡し変換用
帰納法用	帰納的定義-関数用

プログラミング・パターンは、コードのボイラープレート。