フックを合成しても deny と ask の規則は保たれる

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

1. どんなフックの決定 $\eta$ に対しても、$q \in \mathrm{Mat}_{\mathrm{deny}}(R)$ ならば $C_{\mu,R}(\eta, q) = \mathrm{block}$ であり、$q \in \mathrm{Mat}_{\mathrm{ask}}(R)$ ならば $C_{\mu,R}(\eta, q) \ne \mathrm{run}$ である。
2. $\eta = \mathrm{deny}$ ならば、$R$ の allow 規則とモードに関係なく $C_{\mu,R}(\eta, q) = \mathrm{block}$ である。
3. フックを 1 つ足すと、合成したフックの決定は順序 $\succ$ について下がらない。足したフックの決定が $\mathrm{deny}$ か $\bot$ のどちらかであれば、足したあとに $\mathrm{run}$ になる呼び出しは、足す前にも $\mathrm{run}$ である。
4. 命題 3.6 の 1 と 2 に当たる単調性が保たれる。すなわち、フックの決定を固定したとき、deny 規則を足しても $\mathrm{run}$ になる呼び出しは増えず、allow 規則を足しても、$R$ の deny 規則か ask 規則にマッチする呼び出しは $\mathrm{run}$ にならない。