---
title: "コードスロットを七つの構成子について閉じる"
module: L.Coding.SlotClosure
lang: ja
site: "Bedrock"
description: "コードスロットを七つの構成子について閉じる"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 53
canonical: https://bedrock.institute/ja/L.Coding.SlotClosure.html
html: L.Coding.SlotClosure.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SlotClosure.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Closure, L.Axioms.Numerals, L.Coding.SatisfactionTable]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SlotClosure.md, https://bedrock.institute/zh/L.Coding.SlotClosure.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# コードスロットを七つの構成子について閉じる

`L` の内部では、すべての論理式が台の要素として符号化され、すべての論理式が鍵をもちます。それは、アリティの数項を先に、コードを後に置く順序対です。ある上界のスロットは、一つの論理式とそのすべての部分論理式の鍵を集めるので、スロットは鍵の木であり、上界はそれに関する補題のインターフェースの引数にすぎません。本章は、スロットが閉じていることを証明します。複合論理式の鍵がスロットにあれば、その直接の部分論理式の鍵もそこにある。これは、部分論理式をもつ七つの構成子のそれぞれについて成り立ちます。

抽象的な閉包原理を、ここでは具体的な対象に適用します。論理式の構文木が生成する鍵の集合が `closedAt` を満たすことを示します。これは、それらの鍵に沿ってグラフを再帰的に定義するために必要な閉包条件そのものです。

言語の構成子のうち七つは部分論理式をもち、残りの三つはもちません。後者については閉じるべきものがありません。七つの場合はそれぞれ四つの動きからなります。スロットの要素を、それが鍵である論理式へ逆にたどり、場合の標識からその論理式の構成子を割り出し、部分の鍵を複合論理式自身のスロットへ戻し、そして全体のスロットへ持ち上げる、という四つです。

本章は三つの数学的対象を軸に進みます。アリティ `j` の論理式 `χ` の鍵 `keyʟ χ` は、数項 `j` と `χ` のコードの順序対であり、コードそのものは符号化のモジュールのエンコーディング `LCode.⌜ χ ⌝` です。スロット `slot B φ` は、そのような鍵の集合、すなわち `φ` とその部分論理式の木全体の鍵の集合です。そして `closedAt` は、スロットが七つの構成子、合取・選言・含意・二つの量化子・二つの有界量化子について閉じているという主張です。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.SlotClosure {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

論理式は対象言語の論理式であり、その充足は構成可能な構造の中で読まれます。以下の充足の記号は、つねにそこの充足を意味します。周囲の階層は、鍵とスロットを作る底の要素を供給します。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; Formula; _∧̇_; _∨̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

順序対は鍵を符号化し、成分は復元できるので、一つの鍵はアリティの成分とコードの成分に分解できます。構成可能な構造がコードを担い、符号化のモジュールは論理式のエンコーディング `⌜_⌝` とコード上の対の演算を定義します。そして閉包のモジュールは、七つの閉包の場合とその導入の形を、形ごとに述べます。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( module LCode; prʟ; prʟ-fst )
open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt )
```

充足表の章は、三つの中心の対象の出所です。そこでは、論理式の鍵 `keyʟ`、構成子の標識で論理式を分解する形状の補題 `keyʟ-shape`、論理式と上界に付けられたスロット `slot`、スロットの要素をその鍵である論理式へ戻す `slot-inv`、そして鍵の木についての部品の補題 `Parts` が定義されます。

```agda
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( keyʟ; keyʟ-shape; slot; satTable; slot-inv; module Parts )
```

スロットの要素は命題的切り詰めのもとでのみ逆にたどれるので、各場合はその切り詰めを命題へ消去します。アリティを保つ二項の場合の目標は二つの所属命題の連言であり、一項の場合と有界の場合の目標はそれぞれ一つの所属命題です。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
```

アリティは数項で記録され、アリティを上げる構成子は数項の後続を記録します。どちらも周囲の無限集合から来ます。

```agda
open InfinitySet using ( #_; sucV )
```

構成可能な構造の台は、本章のすべてのコード・鍵・スロットの住む型です。

```agda
open hPropStructure 𝒮ʟ
```

ここで `S ^ n` は長さ `n` の環境ベクトルを表します。`_⊨_` と改名された関係は、その環境のもとで制限された構成可能構造の充足を読むものです。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
```

## 成分の鍵をスロットへ戻す

鍵の木は部品の補題に支配されます。`Parts.self` は、論理式自身の鍵が自分のスロットにあることを言い、`Parts.left`、`Parts.right`、`Parts.only` は、複合論理式のスロットが直接の部分のスロットの鍵を含むことを言います。これは構成子の木に沿った部分木の包含であり、部品の補題と逆にたどる操作によって与えられ、上界の順序や下方の閉じ方から来るものではありません。上界 `B` は、これらの補題のインターフェースの引数として渡されるだけです。したがって閉包の場合に必要なのは、読まれた対を部分の鍵として認めることです。以下の二つの補題がちょうどそれを行います。

```agda
module _ (B : S) where
  private
    Sl : ∀ {n} → Formula S n → S
    Sl = slot B
```

鍵の計算は、アリティ `j` の論理式 `χ` について次のように述べます。第一成分がアリティの数項 `# j`、第二成分が `⌜ χ ⌝` のコードの成分であるような対は、すべて鍵 `fst (keyʟ χ)` と等しくなります。三つの量は互いに別物です。`⌜ χ ⌝` は論理式のコードであり、その第一成分が鍵に入る量であり、鍵は数項を先頭に置く順序対です。

```agda
  key≡ : ∀ {j} (χ : Formula S j) (ar p : V ℓ) → # j ≡ ar
       → p ≡ fst LCode.⌜ χ ⌝ → pr ar p ≡ fst (keyʟ χ)
```

仮定は二つとも必要です。アリティの等式と、コードの成分の等式です。証明は、二つの計算法則を通る短い連鎖です。`j` の数項の第一成分は `# j` であり、符号化された対の第一成分は第一成分どうしの対です。

```agda
  key≡ {j} χ ar p qa qp =
      cong₂ pr (sym qa) qp
    ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst j))
    ∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝)
```

持ち上げられた形は、アリティが `suc j` である論理式 `χ` に対して同じことを述べます。このとき鍵の第一成分はアリティの数項の後続であり、これが構成子がアリティを上げるときに場合が読む量です。

```agda
  keyS≡ : ∀ {j} (χ : Formula S (suc j)) (ar p : V ℓ) → # j ≡ ar
        → p ≡ fst LCode.⌜ χ ⌝ → pr (sucV ar) p ≡ fst (keyʟ χ)
```

連鎖は同じで、後続をアリティの等式に沿って押し進めるだけです。`suc j` の数項の第一成分は `suc (# j)` であり、場合の持ち上げられた読みと一致します。

```agda
  keyS≡ {j} χ ar p qa qp =
      cong₂ pr (cong sucV (sym qa)) qp
    ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst (suc j)))
    ∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝)
```

## 七つの場合

場合の構成は、構成子ごとに要求される閉包の形に従います。証明される本体は四つで、形ごとに一つです。アリティを保つ二項の構成子、アリティを保つ一項の構成子、アリティを上げる一項の構成子、そして項とアリティが一段上がった論理式の対を取る二項の構成子です。同じ本体の中で二つの場合が違うのは、構成子の標識と、どの部分を手渡すかだけであり、どちらも引数です。それぞれの場合は四つの動きで進みます。スロットの要素を論理式へ逆にたどり、標識でその構成子を読み、部分の鍵をその論理式自身のスロットへ戻し、全体のスロットへ持ち上げます。

```agda
  module _ {n : ℕ} (φ : Formula S n) {k : ℕ} (γ : S ^ k) where
    private
      δ : S ^ (suc (suc (suc k)))
      δ = B ∷ satTable B φ ∷ Sl φ ∷ γ
```

閉包が証明される再帰は、固定された論理式 `φ` のスロットを索引とし、その環境は三つの名前付きの項目を運びます。上界、`φ` での充足表、そしてそのスロットです。環境の残りの枠は実例に委ねられます。

```agda
      Ci : Fin (suc (suc (suc k)))
      Ci = suc (suc zero)
```

位置 `Ci` は、この環境の中でスロットの占める索引です。どの場合も、スロットはちょうどこの位置で読まれます。

```agda
    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'` であるとき、そのときに限り、またそのような複合のペイロードは二つの部分のコードの順序対です。

```agda
            → (∀ {m} (a' b' : Formula S m) (z : V ℓ)
               → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩)
            → (∀ {m} (a' b' : Formula S m) (z : V ℓ)
               → ⟨ z ∈ fst (Sl b') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩)
            → ⟨ δ ⊨ binShapeAt Ci k' (bothSameAt Ci) ⟩
```

二つの閉包の向きは、部品の補題が与える左と右の部分木の包含であり、結論は場合そのものです。スロットは、標識 `k'` について、両方の部分の鍵を返す形で閉じています。

```agda
    binSame k' op get payOp inL inR = binSameClosed-in Ci k' δ
      (λ c ar a b c∈ sh → PT.rec
        (isProp× (snd (pr (fst ar) (fst a) ∈ fst (Sl φ)))
                 (snd (pr (fst ar) (fst b) ∈ fst (Sl φ))))
        (λ { (m , ψ , (q , incl)) →
```

最初の動きは、スロットの要素 `c` を逆にたどることです。それは、単に、あるアリティ `m` の論理式 `ψ` の鍵であり、逆にたどる操作は、その鍵が `φ` のスロットに属することを返します。目標は二つの所属の連言で、`isProp×` により命題です。これが切り詰めの消去を正当にします。

```agda
          let r  = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh)
              g  = get ψ (r .fst)
              a' = g .fst
              b' = g .snd .fst
              eψ = g .snd .snd
```

第二の動きは構成子を計算します。形状の補題は、場合の形状の証明を使って `ψ` を標識 `k'` と照合し、対応とともにアリティの等式とペイロードの等式を返します。そして分解の仮定が、`ψ` を二つの直接の部分論理式による `op a' b'` と書きます。

```agda
              pay = sym (prʟ-fst LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
                  ∙ cong fst (sym (payOp a' b'))
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
```

第三の動きは、ペイロードについての共有の計算です。要素 `c` は鍵の形の対であり、そのペイロードの成分は二つの部分のコードの成分を記録しています。連鎖は、記録された成分が、成分ごとにコード `⌜ a' ⌝` と `⌜ b' ⌝` であることを証明します。構成子自身のペイロードの法則により `ψ` のペイロードは二つの部分のコードの対であり、形状の補題のペイロードの等式がそれを、`c` から読んだ対と結ぶのです。ここで三つの量を混同してはいけません。論理式全体のコード `⌜ ψ ⌝`、その中のペイロードの成分、そして第一の枠にアリティを運ぶ最終の鍵です。

```agda
              inψ : (χ : Formula S m) → ⟨ fst (keyʟ χ) ∈ fst (Sl ψ) ⟩
                  → ⟨ fst (keyʟ χ) ∈ fst (Sl φ) ⟩
              inψ χ h = incl (fst (keyʟ χ)) h
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
               (sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym (pr-inj pay .fst))))
```

第四の動きは鍵を戻します。まず補助が、逆にたどる操作が返す包含を使って、アリティ `m` の任意の論理式の鍵をそのスロットから `φ` のスロットへ持ち上げます。そして形状の補題のアリティの等式と、符号化の単射性が供給する第一成分の等式が `key≡` に渡り、場合の読む対の所属が `a'` の鍵の所属へ書き換わります。

```agda
               (inψ a' (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                 (inL a' b' _ (Parts.self B keyʟ a'))))
           , subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
               (sym (key≡ b' (fst ar) (fst b) (r .snd .fst) (sym (pr-inj pay .snd))))
```

右の成分は、右の閉包の向きと、単射性が供給する第二成分の等式で同じ組み立てを繰り返し、`b'` を含む対の所属へ書き換えます。二つの半分が揃って、場合は証明されます。

```agda
               (inψ b' (subst (λ w → ⟨ fst (keyʟ b') ∈ fst (Sl w) ⟩) (sym eψ)
                 (inR a' b' _ (Parts.self B keyʟ b')))) })
        (slot-inv B φ (fst c) c∈))
```

消去は逆にたどる操作から供給され、包含はまさにそこから来ています。両成分が揃えば、場合は証明されます。

```agda
    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'` のスロットは両方の連言支のスロットの鍵を含みます。

```agda
    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')
```

選言は同じ形の二つ目の実例で、固有の標識と固有の部品の補題を供給します。

```agda
    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'` のスロットは前件のスロットの鍵と後件のスロットの鍵を含み、場合は同じ四つの動きで証明されます。

```agda
    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` はこの補助定理を使いません。

```agda
           → (∀ {m} (a' : Formula S m) (z : V ℓ)
              → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩)
           → ⟨ δ ⊨ unShapeAt Ci k' (oneSameAt Ci) ⟩
```

閉包の向きと結論は、一成分の形です。返すことを求められるのは、ただ一つの部分論理式の鍵だけです。

```agda
    unSame k' op get payOp inA = unSameClosed-in Ci k' δ
      (λ c ar a c∈ sh → PT.rec (snd (pr (fst ar) (fst a) ∈ fst (Sl φ)))
        (λ { (m , ψ , (q , incl)) →
          let r  = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh)
              g  = get ψ (r .fst)
```

証明は、一つの成分で同じ四つの動きを走らせます。逆にたどる操作が `ψ` とその `φ` のスロットへの包含を産み、形状の補題が標識で分解し、読みはアリティとただ一つのコードだけに関わります。

```agda
              a' = g .fst
              eψ = g .snd
              pay = cong fst (sym (payOp a'))
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
```

ここでの共有の計算はより短いです。`op a'` のペイロードは `a'` 自身のコードなので、連鎖は、要素 `c` に記録されたコードの成分を `a'` のコードの成分と同一視します。対を分解する必要はありません。

```agda
               (sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay)))
               (incl (fst (keyʟ a'))
                 (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                   (inA a' _ (Parts.self B keyʟ a')))) })
        (slot-inv B φ (fst c) c∈))
```

第四の動きが場合を一度に組み立てます。`a'` の鍵は自分のスロットにあり、`inA` がそれを `op a'` のスロットへ移し、`incl` が `φ` のスロットへ持ち上げ、`key≡` が書き換えます。アリティの等式もそこに含まれます。

```agda
    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` で作られる論理式ちょうどに対応し、ペイロードはその論理式のコードそのもの、そして一つの閉包の向きがその鍵を複合のスロットへ送ります。

```agda
              → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩)
           → ⟨ δ ⊨ unShapeAt Ci k' (oneSuccAt Ci) ⟩
```

読みと結論は持ち上げられた形を使います。場合が読む対は、アリティの数項の後続を先頭に置き、部分論理式の鍵が一成分の形で返ることを求めます。

```agda
    unSucc k' op get payOp inA = unSuccClosed-in Ci k' δ
      (λ c ar a c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst a) ∈ fst (Sl φ)))
        (λ { (m , ψ , (q , incl)) →
          let r  = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh)
              g  = get ψ (r .fst)
```

最初の二つの動きは同様です。要素を論理式へ逆にたどり、標識で、アリティの上がったただ一つの部分論理式へ分解します。

```agda
              a' = g .fst
              eψ = g .snd
              pay = cong fst (sym (payOp a'))
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
```

ペイロードの計算は、記録されたコード成分を部分論理式のコードと同一視します。一方、形の等式が与えるのは `# m ≡ fst ar` です。後者が現れるのは、`keyS≡` がこの等式に `sucV` を作用させるときだけです。

```agda
               (sym (keyS≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay)))
               (incl (fst (keyʟ a'))
                 (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                   (inA a' _ (Parts.self B keyʟ a')))) })
        (slot-inv B φ (fst c) c∈))
```

書き換えは `keyS≡` を通ります。これは `# m ≡ fst ar` に `sucV` を作用させ、その結果をコード成分の等式と合わせて、場合が読む対を `a'` の鍵と同一視します。

```agda
    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))
```

第四の本体は有界量化子を扱います。その構成子は、項と、アリティの上がった論理式とを対にします。そのような複合のペイロードは項と部分論理式を順に符号化しますが、論理式であるのは部分論理式だけなので、返すことを求められるのはその鍵だけです。

```agda
               → LCode.payOf (op t a') ≡ prʟ LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
            → (∀ {m} (t : Term S m) (a' : Formula S (suc m)) (z : V ℓ)
               → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op t a')) ⟩)
            → ⟨ δ ⊨ binShapeAt Ci k' (succSndAt Ci) ⟩
```

結論は第二成分の形です。場合が読む対は、持ち上げられたアリティを先に、論理式のコードの成分を後に置くものであり、部分論理式の鍵を返すことを求めます。

```agda
    binSucc k' op get payOp inA = binSuccClosed-in Ci k' δ
      (λ c ar a b c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst b) ∈ fst (Sl φ)))
        (λ { (m , ψ , (q , incl)) →
          let r  = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh)
              g  = get ψ (r .fst)
```

要素 `c` は鍵の形の対であり、そのペイロードは二つの成分を運びます。前に項 `t` のコードの成分、後に部分論理式 `a'` のコードの成分です。場合が読むのは、持ち上げられたアリティと第二成分です。

```agda
              t  = g .fst
              a' = g .snd .fst
              eψ = g .snd .snd
              pay = sym (prʟ-fst LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
                  ∙ cong fst (sym (payOp t a'))
```

共有の計算は、要素に記録されたペイロードを成分ごとに、`⌜ t ⌝ᵗ` と `⌜ a' ⌝` の符号化された対と同一視します。書き換えが消費するのは、符号化の単射性が供給する第二成分の等式です。項は第一成分に乗っていて、ここから外れます。

```agda
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
               (sym (keyS≡ a' (fst ar) (fst b) (r .snd .fst)
                 (sym (pr-inj pay .snd))))
               (incl (fst (keyʟ a'))
```

`keyS≡` による書き換えは、アリティの等式と第二成分の等式を使い、場合の読む対の所属に着地します。第四の動きが、`a'` の鍵を自分のスロットと閉包の向きを通して `φ` のスロットへ持ち上げ、逆にたどる操作が包含を供給します。

```agda
                 (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                   (inA t a' _ (Parts.self B keyʟ a')))) })
        (slot-inv B φ (fst c) c∈))
```

二つの量化子が第三の本体を具体化します。それぞれが標識と分解と、定義的に成り立つペイロードの等式と、ただ一つの閉包の向きを供給します。`∃̇ a'` のスロットは `a'` のスロットの鍵を含み、全称も同様です。

```agda
    exC : ⟨ δ ⊨ unShapeAt Ci 6 (oneSuccAt Ci) ⟩
    exC = unSucc 6 ∃̇_ (λ _ m → m) (λ _ → refl)
            (λ a' → Parts.only B keyʟ (∃̇ a') a')
```

全称量化子は同じ本体の二つ目の実例で、標識七と固有の部品の補題を供給します。

```agda
    allC : ⟨ δ ⊨ unShapeAt Ci 7 (oneSuccAt Ci) ⟩
    allC = unSucc 7 ∀̇_ (λ _ m → m) (λ _ → refl)
             (λ a' → Parts.only B keyʟ (∀̇ a') a')
```

二つの有界量化子は、標識八と九で第四の本体を具体化します。`∀̇∈ t a'` のスロットは `a'` のスロットの鍵を含み、存在の有界量化子も同様です。

```agda
    allInC : ⟨ δ ⊨ binShapeAt Ci 8 (succSndAt Ci) ⟩
    allInC = binSucc 8 ∀̇∈ (λ _ m → m) (λ _ _ → refl)
               (λ t a' → Parts.only B keyʟ (∀̇∈ t a') a')
```

存在の有界量化子は、七つの場合の最後です。

```agda
    exInC : ⟨ δ ⊨ binShapeAt Ci 9 (succSndAt Ci) ⟩
    exInC = binSucc 9 ∃̇∈ (λ _ m → m) (λ _ _ → refl)
              (λ t a' → Parts.only B keyʟ (∃̇∈ t a') a')
```

七つの場合が閉包の主張 `closedAt` へ組み上がります。上界のもとでの `φ` のスロットは、部分論理式をもつどの構成子についても閉じています。これが、コードの上の再帰がその索引集について述べる仮定の解消です。だからこそ、そのような再帰は、複合のコードの各所で、直接の部分論理式の鍵に記録された値に頼れるのです。本章の三つの対象はそれぞれの役割を果たしました。鍵は場合の読む対を同一視し、スロットの木が閉包の向きを供給し、`closedAt` が結果を集めました。

```agda
    slotClosed : ⟨ δ ⊨ closedAt Ci ⟩
    slotClosed = andC , (orC , (impC
               , (exC , (allC , (allInC , exInC)))))
```