Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。
module L.Coding.SlotClosure {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
L の内部では、すべての論理式が台の要素として符号化され、すべての論理式が鍵をもつ。それは、アリティの数項を先に、コードを後に置く順序対である。ある上界のスロットは、一つの論理式とそのすべての部分論理式の鍵を集めるので、スロットは鍵の木であり、上界はそれに関する補題のインターフェースの引数にすぎない。本章は、スロットが閉じていることを証明する。複合論理式の鍵がスロットにあれば、その直接の部分論理式の鍵もそこにある。これは、部分論理式をもつ七つの構成子のそれぞれについて成り立つ。
抽象的な閉包原理を、ここでは具体的な対象に適用する。論理式の構文木が生成する鍵の集合が closedAt を満たすことを示す。これは、それらの鍵に沿ってグラフを再帰的に定義するために必要な閉包条件そのものである。
言語の構成子のうち七つは部分論理式をもち、残りの三つはもたない。後者については閉じるべきものがない。七つの場合はそれぞれ四つの動きからなる。スロットの要素を、それが鍵である論理式へ逆にたどり、場合の標識からその論理式の構成子を割り出し、部分の鍵を複合論理式自身のスロットへ戻し、そして全体のスロットへ持ち上げる、という四つである。
本章は三つの数学的対象を軸に進む。アリティ j の論理式 χ の鍵 keyʟ χ は、数項 j と χ のコードの順序対であり、コードそのものは符号化のモジュールのエンコーディング LCode.⌜ χ ⌝ である。スロット slot B φ は、そのような鍵の集合、すなわち φ とその部分論理式の木全体の鍵の集合である。そして closedAt は、スロットが七つの構成子、合取・選言・含意・二つの量化子・二つの有界量化子について閉じているという主張である。
論理式は対象言語の論理式であり、その充足は構成可能な構造の中で読まれる。以下の充足の記号は、つねにそこの充足を意味する。周囲の階層は、鍵とスロットを作る底の要素を供給する。
順序対は鍵を符号化し、成分は復元できるので、一つの鍵はアリティの成分とコードの成分に分解できる。構成可能な構造がコードを担い、符号化のモジュールは論理式のエンコーディング ⌜_⌝ とコード上の対の演算を定義する。そして閉包のモジュールは、七つの閉包の場合とその導入の形を、形ごとに述べる。
充足表の章は、三つの中心の対象の出所である。そこでは、論理式の鍵 keyʟ、構成子の標識で論理式を分解する形状の補題 keyʟ-shape、論理式と上界に付けられたスロット slot、スロットの要素をその鍵である論理式へ戻す slot-inv、そして鍵の木についての部品の補題 Parts が定義される。
スロットの要素は命題的切り詰めのもとでのみ逆にたどれるので、各場合はその切り詰めを命題へ消去する。アリティを保つ二項の場合の目標は二つの所属命題の連言であり、一項の場合と有界の場合の目標はそれぞれ一つの所属命題である。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
using ( module InfinitySet )
アリティは数項で記録され、アリティを上げる構成子は数項の後続を記録する。どちらも周囲の無限集合から来る。
open InfinitySet using ( #_; sucV )
構成可能な構造の台は、本章のすべてのコード・鍵・スロットの住む型である。
open hPropView 𝒮ʟ
ここで Vec S n は長さ n の環境ベクトルを表す。_⊨_ と改名された関係は、その環境のもとで制限された構成可能構造の充足を読むものである。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )
成分の鍵をスロットへ戻す
鍵の木は部品の補題に支配される。Parts.self は、論理式自身の鍵が自分のスロットにあることを言い、Parts.left、Parts.right、Parts.only は、複合論理式のスロットが直接の部分のスロットの鍵を含むことを言う。これは構成子の木に沿った部分木の包含であり、部品の補題と逆にたどる操作によって与えられ、上界の順序や下方の閉じ方から来るものではない。上界 B は、これらの補題のインターフェースの引数として渡されるだけである。したがって閉包の場合に必要なのは、読まれた対を部分の鍵として認めることである。以下の二つの補題がちょうどそれを行う。
module _ (B : S) where
private
Sl : ∀ {n} → Formula S n → S
Sl = slot B
鍵の計算は、アリティ j の論理式 χ について次のように述べる。第一成分がアリティの数項 # j、第二成分が ⌜ χ ⌝ のコードの成分であるような対は、すべて鍵 (keyʟ χ) .fst と等しくなる。三つの量は互いに別物である。⌜ χ ⌝ は論理式のコードであり、その第一成分が鍵に入る量であり、鍵は数項を先頭に置く順序対である。
key≡ : ∀ {j} (χ : Formula S j) (ar p : V ℓ) → # j ≡ ar
→ p ≡ (LCode.⌜ χ ⌝) .fst → pr ar p ≡ (keyʟ χ) .fst
仮定は二つとも必要である。アリティの等式と、コードの成分の等式である。証明は、二つの計算法則を通る短い連鎖である。j の数項の第一成分は # j であり、符号化された対の第一成分は第一成分どうしの対である。
key≡ {j} χ ar p qa qp =
cong₂ pr (sym qa) qp
∙ cong (λ w → pr w ((LCode.⌜ χ ⌝) .fst)) (sym (numeralL-fst j))
∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝)
持ち上げられた形は、アリティが suc j である論理式 χ に対して同じことを述べる。このとき鍵の第一成分はアリティの数項の後続であり、これが構成子がアリティを上げるときに場合が読む量である。
keyS≡ : ∀ {j} (χ : Formula S (suc j)) (ar p : V ℓ) → # j ≡ ar
→ p ≡ (LCode.⌜ χ ⌝) .fst → pr (sucV ar) p ≡ (keyʟ χ) .fst
連鎖は同じで、後続をアリティの等式に沿って押し進めるだけである。suc j の数項の第一成分は suc (# j) であり、場合の持ち上げられた読みと一致する。
keyS≡ {j} χ ar p qa qp =
cong₂ pr (cong sucV (sym qa)) qp
∙ cong (λ w → pr w ((LCode.⌜ χ ⌝) .fst)) (sym (numeralL-fst (suc j)))
∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝)
七つの場合
場合の構成は、構成子ごとに要求される閉包の形に従う。証明される本体は四つで、形ごとに一つである。アリティを保つ二項の構成子、アリティを保つ一項の構成子、アリティを上げる一項の構成子、そして項とアリティが一段上がった論理式の対を取る二項の構成子である。同じ本体の中で二つの場合が違うのは、構成子の標識と、どの部分を手渡すかだけであり、どちらも引数である。それぞれの場合は四つの動きで進む。スロットの要素を論理式へ逆にたどり、標識でその構成子を読み、部分の鍵をその論理式自身のスロットへ戻し、全体のスロットへ持ち上げる。
module _ {n : ℕ} (φ : Formula S n) {k : ℕ} (γ : Vec S k) where
private
δ : Vec S (suc (suc (suc k)))
δ = B ∷ satTable B φ ∷ Sl φ ∷ γ
閉包が証明される再帰は、固定された論理式 φ のスロットを索引とし、その環境は三つの名前付きの項目を運ぶ。上界、φ での充足表、そしてそのスロットである。環境の残りの枠は実例に委ねられる。
Ci : Fin (suc (suc (suc k)))
Ci = suc (suc zero)
位置 Ci は、この環境の中でスロットの占める索引である。どの場合も、スロットはちょうどこの位置で読まれる。
binSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∶ Formula S m ] (Σ[ b' ∶ Formula S m ] (ψ ≡ op a' b')))
→ (∀ {m} (a' b' : Formula S m)
→ LCode.payOf (op a' b') ≡ prʟ LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
最初の本体は、アリティを保つ二項の構成子、すなわち合取・選言・含意の形を扱う。仮定は標識 k' を記述する。論理式がこの標識に対応するのは、同じアリティの二つの論理式による op a' b' であるとき、そのときに限り、またそのような複合のペイロードは二つの部分のコードの順序対である。
→ (∀ {m} (a' b' : Formula S m) (z : V ℓ)
→ ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op a' b')) .fst ⟩)
→ (∀ {m} (a' b' : Formula S m) (z : V ℓ)
→ ⟨ z ∈ (Sl b') .fst ⟩ → ⟨ z ∈ (Sl (op a' b')) .fst ⟩)
→ ⟨ δ ⊨ binShapeAt Ci k' (bothSameAt Ci) ⟩
二つの閉包の向きは、部品の補題が与える左と右の部分木の包含であり、結論は場合そのものである。スロットは、標識 k' について、両方の部分の鍵を返す形で閉じている。
binSame k' op get payOp inL inR = binSameClosed-in Ci k' δ
(λ c ar a b c∈ sh → rec₁
(isProp× ((pr (ar .fst) (a .fst) ∈ (Sl φ) .fst) .snd)
((pr (ar .fst) (b .fst) ∈ (Sl φ) .fst) .snd))
(λ { (m , ψ , (q , incl)) →
最初の動きは、スロットの要素 c を逆にたどることである。それは、単に、あるアリティ m の論理式 ψ の鍵であり、逆にたどる操作は、その鍵が φ のスロットに属することを返す。目標は二つの所属の連言で、isProp× により命題である。これが切り詰めの消去を正当にする。
let r = keyʟ-shape ψ k' (ar .fst) (pr (a .fst) (b .fst)) (sym q ∙ sh)
g = get ψ (r .fst)
a' = g .fst
b' = g .snd .fst
eψ = g .snd .snd
第二の動きは構成子を計算する。形状の補題は、場合の形状の証明を使って ψ を標識 k' と照合し、対応とともにアリティの等式とペイロードの等式を返す。そして分解の仮定が、ψ を二つの直接の部分論理式による op a' b' と書く。
pay = sym (prʟ-fst LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
∙ cong (λ p → p .fst) (sym (payOp a' b'))
∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
第三の動きは、ペイロードについての共有の計算である。要素 c は鍵の形の対であり、そのペイロードの成分は二つの部分のコードの成分を記録している。連鎖は、記録された成分が、成分ごとにコード ⌜ a' ⌝ と ⌜ b' ⌝ であることを証明する。構成子自身のペイロードの法則により ψ のペイロードは二つの部分のコードの対であり、形状の補題のペイロードの等式がそれを、c から読んだ対と結ぶのである。ここで三つの量を混同してはいけない。論理式全体のコード ⌜ ψ ⌝、その中のペイロードの成分、そして第一の枠にアリティを運ぶ最終の鍵である。
inψ : (χ : Formula S m) → ⟨ (keyʟ χ) .fst ∈ (Sl ψ) .fst ⟩
→ ⟨ (keyʟ χ) .fst ∈ (Sl φ) .fst ⟩
inψ χ h = incl ((keyʟ χ) .fst) h
in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
(sym (key≡ a' (ar .fst) (a .fst) (r .snd .fst) (sym (pr-inj pay .fst))))
第四の動きは鍵を戻す。まず補助が、逆にたどる操作が返す包含を使って、アリティ m の任意の論理式の鍵をそのスロットから φ のスロットへ持ち上げる。そして形状の補題のアリティの等式と、符号化の単射性が供給する第一成分の等式が key≡ に渡り、場合の読む対の所属が a' の鍵の所属へ書き換わる。
(inψ a' (subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
(inL a' b' _ (Parts.self B keyʟ a'))))
, subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
(sym (key≡ b' (ar .fst) (b .fst) (r .snd .fst) (sym (pr-inj pay .snd))))
右の成分は、右の閉包の向きと、単射性が供給する第二成分の等式で同じ組み立てを繰り返し、b' を含む対の所属へ書き換える。二つの半分が揃って、場合は証明される。
(inψ b' (subst (λ w → ⟨ (keyʟ b') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
(inR a' b' _ (Parts.self B keyʟ b')))) })
(slot-inv B φ (c .fst) c∈))
消去は逆にたどる操作から供給され、包含はまさにそこから来ている。両成分が揃えば、場合は証明される。
andC : ⟨ δ ⊨ binShapeAt Ci 2 (bothSameAt Ci) ⟩
andC = binSame 2 _∧̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ∧̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ∧̇ b') a' b')
合取は最初の実例である。a' ∧̇ b' のスロットは両方の連言支のスロットの鍵を含む。
orC : ⟨ δ ⊨ binShapeAt Ci 3 (bothSameAt Ci) ⟩
orC = binSame 3 _∨̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ∨̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ∨̇ b') a' b')
選言は同じ形の二つ目の実例で、固有の標識と固有の部品の補題を供給する。
impC : ⟨ δ ⊨ binShapeAt Ci 4 (bothSameAt Ci) ⟩
impC = binSame 4 _⇒̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ⇒̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ⇒̇ b') a' b')
含意は三つ目である。a' ⇒̇ b' のスロットは前件のスロットの鍵と後件のスロットの鍵を含み、場合は同じ四つの動きで証明される。
unSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∶ Formula S m ] (ψ ≡ op a'))
→ (∀ {m} (a' : Formula S m) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
補助定理 unSame は、アリティを保つ仮想的な一項演算について、同様の閉包原理を証明する。この言語の十個の構成子にはこの形がないため、closedAt はこの補助定理を使わない。
→ (∀ {m} (a' : Formula S m) (z : V ℓ)
→ ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op a')) .fst ⟩)
→ ⟨ δ ⊨ unShapeAt Ci k' (oneSameAt Ci) ⟩
閉包の向きと結論は、一成分の形である。返すことを求められるのは、ただ一つの部分論理式の鍵だけである。
unSame k' op get payOp inA = unSameClosed-in Ci k' δ
(λ c ar a c∈ sh → rec₁ ((pr (ar .fst) (a .fst) ∈ (Sl φ) .fst) .snd)
(λ { (m , ψ , (q , incl)) →
let r = keyʟ-shape ψ k' (ar .fst) (a .fst) (sym q ∙ sh)
g = get ψ (r .fst)
証明は、一つの成分で同じ四つの動きを走らせる。逆にたどる操作が ψ とその φ のスロットへの包含を産み、形状の補題が標識で分解し、読みはアリティとただ一つのコードだけに関わる。
a' = g .fst
eψ = g .snd
pay = cong (λ p → p .fst) (sym (payOp a'))
∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
ここでの共有の計算はより短い。op a' のペイロードは a' 自身のコードなので、連鎖は、要素 c に記録されたコードの成分を a' のコードの成分と同一視する。対を分解する必要はない。
(sym (key≡ a' (ar .fst) (a .fst) (r .snd .fst) (sym pay)))
(incl ((keyʟ a') .fst)
(subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
(inA a' _ (Parts.self B keyʟ a')))) })
(slot-inv B φ (c .fst) c∈))
第四の動きが場合を一度に組み立てる。a' の鍵は自分のスロットにあり、inA がそれを op a' のスロットへ移し、incl が φ のスロットへ持ち上げ、key≡ が書き換える。アリティの等式もそこに含まれる。
unSucc : (k' : ℕ) (op : ∀ {m} → Formula S (suc m) → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∶ Formula S (suc m) ] (ψ ≡ op a'))
→ (∀ {m} (a' : Formula S (suc m)) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
→ (∀ {m} (a' : Formula S (suc m)) (z : V ℓ)
第三の本体は、アリティを上げる一項の構成子、二つの量化子の形を扱う。仮定は持ち上げられた版である。標識 k' は、アリティの上がった論理式から op で作られる論理式ちょうどに対応し、ペイロードはその論理式のコードそのもの、そして一つの閉包の向きがその鍵を複合のスロットへ送る。
→ ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op a')) .fst ⟩)
→ ⟨ δ ⊨ unShapeAt Ci k' (oneSuccAt Ci) ⟩
読みと結論は持ち上げられた形を使う。場合が読む対は、アリティの数項の後続を先頭に置き、部分論理式の鍵が一成分の形で返ることを求める。
unSucc k' op get payOp inA = unSuccClosed-in Ci k' δ
(λ c ar a c∈ sh → rec₁ ((pr (sucV (ar .fst)) (a .fst) ∈ (Sl φ) .fst) .snd)
(λ { (m , ψ , (q , incl)) →
let r = keyʟ-shape ψ k' (ar .fst) (a .fst) (sym q ∙ sh)
g = get ψ (r .fst)
最初の二つの動きは同様である。要素を論理式へ逆にたどり、標識で、アリティの上がったただ一つの部分論理式へ分解する。
a' = g .fst
eψ = g .snd
pay = cong (λ p → p .fst) (sym (payOp a'))
∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
ペイロードの計算は、記録されたコード成分を部分論理式のコードと同一視する。一方、形の等式が与えるのは # m ≡ ar .fst である。後者が現れるのは、keyS≡ がこの等式に sucV を作用させるときだけである。
(sym (keyS≡ a' (ar .fst) (a .fst) (r .snd .fst) (sym pay)))
(incl ((keyʟ a') .fst)
(subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
(inA a' _ (Parts.self B keyʟ a')))) })
(slot-inv B φ (c .fst) c∈))
書き換えは keyS≡ を通る。これは # m ≡ ar .fst に sucV を作用させ、その結果をコード成分の等式と合わせて、場合が読む対を a' の鍵と同一視する。
binSucc : (k' : ℕ)
→ (op : ∀ {m} → Term S m → Formula S (suc m) → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ t ∶ Term S m ] (Σ[ a' ∶ Formula S (suc m) ] (ψ ≡ op t a')))
→ (∀ {m} (t : Term S m) (a' : Formula S (suc m))
第四の本体は有界量化子を扱う。その構成子は、項と、アリティの上がった論理式とを対にする。そのような複合のペイロードは項と部分論理式を順に符号化するが、論理式であるのは部分論理式だけなので、返すことを求められるのはその鍵だけである。
→ LCode.payOf (op t a') ≡ prʟ LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
→ (∀ {m} (t : Term S m) (a' : Formula S (suc m)) (z : V ℓ)
→ ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op t a')) .fst ⟩)
→ ⟨ δ ⊨ binShapeAt Ci k' (succSndAt Ci) ⟩
結論は第二成分の形である。場合が読む対は、持ち上げられたアリティを先に、論理式のコードの成分を後に置くものであり、部分論理式の鍵を返すことを求める。
binSucc k' op get payOp inA = binSuccClosed-in Ci k' δ
(λ c ar a b c∈ sh → rec₁ ((pr (sucV (ar .fst)) (b .fst) ∈ (Sl φ) .fst) .snd)
(λ { (m , ψ , (q , incl)) →
let r = keyʟ-shape ψ k' (ar .fst) (pr (a .fst) (b .fst)) (sym q ∙ sh)
g = get ψ (r .fst)
要素 c は鍵の形の対であり、そのペイロードは二つの成分を運ぶ。前に項 t のコードの成分、後に部分論理式 a' のコードの成分である。場合が読むのは、持ち上げられたアリティと第二成分である。
t = g .fst
a' = g .snd .fst
eψ = g .snd .snd
pay = sym (prʟ-fst LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
∙ cong (λ p → p .fst) (sym (payOp t a'))
共有の計算は、要素に記録されたペイロードを成分ごとに、⌜ t ⌝ᵗ と ⌜ a' ⌝ の符号化された対と同一視する。書き換えが消費するのは、符号化の単射性が供給する第二成分の等式である。項は第一成分に乗っていて、ここから外れる。
∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
(sym (keyS≡ a' (ar .fst) (b .fst) (r .snd .fst)
(sym (pr-inj pay .snd))))
(incl ((keyʟ a') .fst)
keyS≡ による書き換えは、アリティの等式と第二成分の等式を使い、場合の読む対の所属に着地する。第四の動きが、a' の鍵を自分のスロットと閉包の向きを通して φ のスロットへ持ち上げ、逆にたどる操作が包含を供給する。
(subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
(inA t a' _ (Parts.self B keyʟ a')))) })
(slot-inv B φ (c .fst) c∈))
二つの量化子が第三の本体を具体化する。それぞれが標識と分解と、定義的に成り立つペイロードの等式と、ただ一つの閉包の向きを供給する。∃̇ a' のスロットは a' のスロットの鍵を含み、全称も同様である。
exC : ⟨ δ ⊨ unShapeAt Ci 6 (oneSuccAt Ci) ⟩
exC = unSucc 6 ∃̇_ (λ _ m → m) (λ _ → refl)
(λ a' → Parts.only B keyʟ (∃̇ a') a')
全称量化子は同じ本体の二つ目の実例で、標識七と固有の部品の補題を供給する。
allC : ⟨ δ ⊨ unShapeAt Ci 7 (oneSuccAt Ci) ⟩
allC = unSucc 7 ∀̇_ (λ _ m → m) (λ _ → refl)
(λ a' → Parts.only B keyʟ (∀̇ a') a')
二つの有界量化子は、標識八と九で第四の本体を具体化する。∀̇∈ t a' のスロットは a' のスロットの鍵を含み、存在の有界量化子も同様である。
allInC : ⟨ δ ⊨ binShapeAt Ci 8 (succSndAt Ci) ⟩
allInC = binSucc 8 ∀̇∈ (λ _ m → m) (λ _ _ → refl)
(λ t a' → Parts.only B keyʟ (∀̇∈ t a') a')
存在の有界量化子は、七つの場合の最後である。
exInC : ⟨ δ ⊨ binShapeAt Ci 9 (succSndAt Ci) ⟩
exInC = binSucc 9 ∃̇∈ (λ _ m → m) (λ _ _ → refl)
(λ t a' → Parts.only B keyʟ (∃̇∈ t a') a')
七つの場合が閉包の主張 closedAt へ組み上がる。上界のもとでの φ のスロットは、部分論理式をもつどの構成子についても閉じている。これが、コードの上の再帰がその索引集について述べる仮定の解消である。だからこそ、そのような再帰は、複合のコードの各所で、直接の部分論理式の鍵に記録された値に頼れるのである。本章の三つの対象はそれぞれの役割を果たした。鍵は場合の読む対を同一視し、スロットの木が閉包の向きを供給し、closedAt が結果を集めた。
slotClosed : ⟨ δ ⊨ closedAt Ci ⟩
slotClosed = andC , (orC , (impC
, (exC , (allC , (allInC , exInC)))))