そうか！ 参照ノードを入れればいい（他にも対策）

証明ストリング図のノードラベルが、メタ変数でラベルしているのか、システム内のラベルでラベルしているのが分からないという問題があった。

ラベルのテキストで区別するのは現実的ではないが、ノード形状で区別ならなんとかなる。まず、ノード種別を

1. インラインノード（クラスター含む）：そこに実際にあるノード／クラスター。
2. {参照ノード | 呼び出しノード}： ラベルだけがそこにあり、実体は別なところにある。

参照ノードは形状を変える。

1. ラベル（システム内の実際のラベル）の下に二重下線を必ず引く。
2. 形状は基本的に四角とする。
3. 参照ノードのラベルは、そのときの定理ライブラリによって解決される。
4. 必要があれば、定理ライブラリの定理本体の証明図で参照ノードを展開〈リプレース〉してよい。
5. 定理ライブラリの概念を厳密化する必要がある。

この方式は、いいか悪いか、もう少し実験しないと分からない。

---

LK流の証明はムービー方式と呼ぶことにして、NK流は対称的にスチル方式としたが、単なるスチルではない。単なるスチルならムービーのフレームもスチルだ。

• 修飾付き改竄〈かいざん〉スチル〈decorated altered still〉方式

リーズニングのそれぞれの基本手順〈組み込み基本リーズニング〉に対して、様々な修飾と改竄により変形の痕跡を残し、1枚のスチルのなかに変形過程を累積させて表現する。それが、修飾付き改竄スチル方式。