- 単に「コンテキスト」は混合コンテキスト
- 純コンテキスト＝宣言コンテキスト
- 混合コンテキスト＝宣言と定義のリスト
- 定義は、宣言（x:A）と割り当て（x:=t）のペア
- シーケントは三種類： 判断シーケント、事実シーケント、質問シーケント
- 判断シーケントは、コンテキスト〈前提〉〈premises〉、結論命題〈conclusion proposition〉、証拠からなる。
- 事実シーケントは、コンテキスト〈前提〉、結論命題からなる。
- 質問シーケントは、コンテキスト〈前提〉、ターゲット命題からなる。
- シーケントの前提は宣言コンテキスト〈純コンテキスト〉に限る。定義は環境コンテキストに入れる。
混合コンテキスト原理：
- 混合コンテキストと、判断の列は同値である。互いに相互変換できる。
パック／アンパック原理：
- 判断シーケントは、混合コンテキスト内に、宣言と割り当てのペアとしてパックできる。
- 混合コンテキスト内のパックされた定義を、判断シーケントまたは事実シーケントとしてアンパックして取り出すことができる。
宣言コンテキスト、混合コンテキスト、判断・事実・質問の概念で整理された。
- 宣言コンテキストは指標として使える。
- 判断は単一ターゲットの手続きである。判断の証拠は、手続きのボディである。
- 事実はプロファイルである。
- 一般の手続きは多判断となる。
- 環境コンテキスト（混合コンテキストが許される）と多判断の集まりが組織化を与える。
- さらにステージの入れ子構造で構造化できる。
- 入れ子のステージとシーケントから構成されるフレームの時間的遷移系列としてムービーができる。
- 出現する名前〈ラベル〉は名前空間階層と別名機構〈openコマンド〉、名前登録（別な名前空間に別名を作成する）で制御する。
- シリアライズと散文化〈prosify〉でムービーをテキストドキュメントにする。
