許可される複合コマンドのサブコマンドは単独でも許可される

命題 5.2（「ツールと権限」§5）・ ✓公理まで証明済み

定義 5.1 の判定について次が成り立つ。

$\mathrm{dec}^\ast_R(c) = \mathrm{allow}$ ならば、 $\mathrm{sub}(c)$ のすべてのサブコマンド $c_i$ について $\mathrm{dec}^\ast_R(c_i) = \mathrm{allow}$ である。
$R$ の allow 規則が $(\mathrm{allow}, \pi)$ だけで、 $c' \not\models \pi$ とする。このとき、 $c \models \pi$ であるどんな $c$ についても、 $\mathrm{sub}(c \mathbin{\texttt{\&\&}} c')$ が $c'$ を含むならば $\mathrm{dec}^\ast_R(c \mathbin{\texttt{\&\&}} c') \ne \mathrm{allow}$ である。
文字列全体を照合する素朴な方式（ $\mathrm{dec}_R$ をそのまま複合コマンドの文字列に適用する方式）では、1 が成り立たない例が存在する。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。

証明で明示的に参照している定理は、まだありません。