---
title: "閉じた符号の定義域の健全性と完全性"
module: L.Coding.CodeDomainAdequacy
lang: ja
site: "Bedrock"
description: "閉じた符号の定義域の健全性と完全性"
stage: "GCH の証明"
reading_order: 99
canonical: https://bedrock.institute/ja/L.Coding.CodeDomainAdequacy.html
html: L.Coding.CodeDomainAdequacy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeDomainAdequacy.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Environment, L.Coding.EnvironmentSet, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Quantification, L.Coding.EnvironmentTower, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.Coding.Closure, L.Coding.CodeShape, L.Coding.CodeSet, L.Ordinal]
routes: [gch-descriptions]
translations: [https://bedrock.institute/en/L.Coding.CodeDomainAdequacy.md, https://bedrock.institute/zh/L.Coding.CodeDomainAdequacy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
構文についての内部的な議論は、`L` の中の論理式キーの集合から始まります。本章は、候補となる符号領域と外部の論理式文法を二方向に比較します。領域の各要素は、ある論理式のキーへ単に復号でき、すべての真正な論理式キーは領域に属します。これらは符号の所属についての主張であり、符号化された論理式の真理や充足についての主張ではありません。

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

以下の議論では、排中律と命題的切り詰めを併用します。命題的切り詰めは、復号の証人を選び出すことなく、その存在だけを記録します。この切り詰めを除去できるのは、行き先も命題である場合に限られます。

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

`lem : LEM (ℓ-suc ℓ)` を仮定します。本章のすべての構成はこの仮定のもとで行われますが、仮定によって復号の結論が強くなるわけではありません。復号された論理式の証人は、命題的に切り詰められたままです。

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

本章は集合論の完全な一階言語を扱います。論理式には非有界の量化子に加えて二つの有界量化子があり、項は変数と定数から作られます。領域が集めて記述すべき対象は、これらです。

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

論理式キーは入れ子の順序対なので、対符号化の単射性により、キーの等しさからアリティ、タグ、ペイロードを復元できます。自然数のアリティはフォン・ノイマン数項で表され、構成可能な環境集合が有限パラメータベクトルの内部表現を与えます。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst; sucʟ; sucʟ-fst )
```

対象言語では、構造に従って組み立てたキーが候補領域に属することを表現できます。順序対の式が入れ子のキーを構成し、その妥当性定理が、得られた論理式の充足と、対応するホスト側の対符号への所属とを同一視します。

```agda
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.Model {ℓ} using ( container )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression
```

量化子の符号ではアリティが変わります。どちらの量化子でも本体は後続アリティのキーであり、有界量化子はさらに現在のアリティで正当な項をもちます。対、後続、拡張環境についての意味論的補題が、束縛子の下で起こるこれらの変化を正確に表します。

```agda
open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh
  ; pr-out; pr-in; down; fstS; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in
```

存在的なペイロードの記述は命題的に切り詰められ、ときには二重の証人を含みます。その内向きと外向きの読みは、この切り詰めを保ちます。十個の構成子タグは零から九までの数項で表され、別の環境塔が各符号を読むアリティを記録します。

```agda
  ; fillSnd; fillBoth; useSnd; useBoth
  ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; bigOr-in; bigOr-out )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower; nn )
open import L.Coding.CodeDomain {ℓ} using
```

記述 `codesAt` には、相補的な二つの部分があります。`shapeAt` は領域の既存要素を十種類の構成子形のいずれかとして読み、複合符号では直下の部分キーも領域に残ることを要求します。`closeAt` は生成する向きの主張であり、正当な項と既存の部分キーから対応する新しいキーが得られます。

```agda
  ( isTm; keyUp; keyExpr; atomKeyExpr; bndKeyExpr
  ; unKey; binKey; atomKey; bndKey
  ; Tags; shN; module Shape; shapeAt; module Close; closeAt; codesAt )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
```

構成子タグは `Fin 10` の要素です。その自然数値が十個のペイロード述語の一つを選び、その値は自動的に十未満です。環境は有限ベクトルであり、階層に格納される符号は入れ子の集合論的順序対です。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n )
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )
```

復号は互いに排他的な構成子の場合に分かれ、多くの場合、命題的に切り詰められた証人だけを返します。対の等しさは成分ごとに移され、不可能なタグは空型へ至ります。これらの操作から、単に存在する論理式を大域的に選ぶ復号写像は得られません。

```agda
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

累積階層は、集合値の順序対符号、フォン・ノイマン数項、アリティの後続演算を与えます。所属には小さなファイバー表示があり、階層の集合の等しさは命題です。これらの事実により、切り詰められた分解と、所属や等しさへのその消去が正当化されます。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )
```

構成可能な構造の台が `S` として固定され、以下のすべての環境と論理式の読みがその上にあります。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

符号の記述はすべて、`L` が担う一階構造で解釈されます。したがって、「組み立てたキーが `C` に属する」という主張には、対象言語の論理式としての形と、ホスト側の所属としての読みがあります。妥当性補題は、同じ主張のこの二つの形を同一視します。

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

## 記述の読み出し

まず、項の符号を記述します。集合 `t` がアリティ `ar` の項の符号であるのは、それが単に、タグ零と作業集合 `Wv` の要素の対、あるいはタグ一と集合 `ar` の要素の対であるときです。ここでの `ar` はまだ任意の集合です。それが数項だと分かってはじめて、第二の分岐から有界な変数の添字が復元されます。

```agda
IsTmV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
IsTmV Wv t ar = ∥ (Σ[ x ∈ V ℓ ] ((t ≡ pr (# 0) x) × ⟨ x ∈ Wv ⟩))
                ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# 1) i) × ⟨ i ∈ ar ⟩)) ∥₁
```

最初の三種類のペイロード述語は、原子論理式、二項結合子、偽を扱います。原子のペイロードは二つの正当な項符号へ単に分解され、二項のペイロードは候補領域にすでに属する同じアリティの二つの部分キーへ単に分解されます。偽のペイロードは直接の等式 `r = # 0` であり、存在証人をもちません。

```agda
module CodesSem (Wv Cv : V ℓ) where
  AtomP BinP ConP QuP BqP : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  AtomP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ u ∈ V ℓ ] ((r ≡ pr t u) × (IsTmV Wv t ar × IsTmV Wv u ar)) ∥₁
  BinP ar r = ∥ Σ[ a ∈ V ℓ ] Σ[ b ∈ V ℓ ] ((r ≡ pr a b) × (⟨ pr ar a ∈ Cv ⟩ × ⟨ pr ar b ∈ Cv ⟩)) ∥₁
  ConP ar r = r ≡ # 0
```

量化子のペイロードで一覧が完成します。非有界量化子のペイロードは、後続アリティにある下位キーです。有界量化子のペイロードは、現在のアリティで正当な項符号と、そのような下位キーとの対です。この非対称性は文法そのものに由来します。本体は後続アリティをもち、境界を表す項は量化された論理式と同じアリティをもちます。

```agda
  QuP ar r = ⟨ pr (sucV ar) r ∈ Cv ⟩
  BqP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ a ∈ V ℓ ] ((r ≡ pr t a) × (IsTmV Wv t ar × ⟨ pr (sucV ar) a ∈ Cv ⟩)) ∥₁
```

ペイロードの表はここからはじまります。タグ零と一が二つの原子の形を、タグ二と三が連言と選言の二項の形を担います。

```agda
  PayN : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PayN 0 = AtomP
  PayN 1 = AtomP
  PayN 2 = BinP
  PayN 3 = BinP
```

表は続き、タグ四が含意、タグ五が定数の偽、タグ六と七が二つの非有界量化子、タグ八が有界の全称を担います。

```agda
  PayN 4 = BinP
  PayN 5 = ConP
  PayN 6 = QuP
  PayN 7 = QuP
  PayN 8 = BqP
```

タグ九は有界存在量化子のペイロードを担います。補助族 `PayN` は十以上の自然数では空型ですが、正当な `Key` のタグは `Fin 10` から選ばれます。したがって、キーに現れうるのは零から九までの十種類だけです。

```agda
  PayN 9 = BqP
  PayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) _ _ = Empty.⊥*
```

アリティ `ar` でのキーとは、単に、十のタグの一つと、それに合った形のペイロードのことです。キーが何でないかに注意してください。キーは帰納的な構文木ではなく、その分解が一意なデータだとも主張していません。キーとは、集合として符号化された対が、既知の十の形のどれかに分解されるという、切り詰められた証拠なのです。

```agda
  Key : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  Key ar p = ∥ Σ[ k ∈ Fin 10 ] Σ[ r ∈ V ℓ ] ((p ≡ pr (# (toℕ k)) r) × PayN (toℕ k) ar r) ∥₁
```

候補となる項符号 `t`、アリティ集合 `ar`、作業集合 `Wv`、そしてそれぞれ数項零と一であることが分かっている二つの要素を含む環境を固定します。これらのタグ等式のもとで、対象言語の述語 `isTm` と外部の述語 `IsTmV Wv t ar` を正確に比較できます。

```agda
module _ {k : ℕ} (t ar w N0 N1 : Fin k) (δ : S ^ k)
  (q0 : fst (lookup N0 δ) ≡ # 0) (q1 : fst (lookup N1 δ) ≡ # 1) where
  private
    Wv = fst (lookup w δ)
```

外向きの読み出しは、対象言語の論理式の切り詰められた選言を消去します。定数の分岐では、存在量化が対の第二成分を取り出し、数項の等式がタグを揃え、所属が `IsTmV` へ入ります。結果は、切り詰められた定義の左の分岐です。

```agda
  isTm-out : ⟨ δ ⊨ isTm t ar w N0 N1 ⟩ → IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ))
  isTm-out = PT.rec squash₁
    (λ { (inl h) → PT.map
           (λ { (v , s , (e , v∈)) → inl (fst v , (e ∙ cong (λ a → pr a (fst v)) q0 , v∈)) })
           (sndEx-out t N0 (var i0 ∈̇ var (sh 2 w)) δ h)
```

変数の分岐は、数項一とアリティの集合で同じ三歩を繰り返し、右の分岐を作ります。二つの分岐合わせて、対象言語の認識と、集合レベルの `IsTmV` がまさに同値であることが言えます。

```agda
       ; (inr h) → PT.map
           (λ { (v , s , (e , v∈)) → inr (fst v , (e ∙ cong (λ a → pr a (fst v)) q1 , v∈)) })
           (sndEx-out t N1 (var i0 ∈̇ var (sh 2 ar)) δ h) })
```

内向きの読み出しは、同じ変換を逆向きに行います。定数の分岐では、充填の補題が証人 `x` を枠零の存在量化子の下に置き、対の等式が逆向きの数項の等式に沿って運ばれて、充足が対象言語の論理式の形と一致するようにします。

```agda
  isTm-in : IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ)) → ⟨ δ ⊨ isTm t ar w N0 N1 ⟩
  isTm-in = PT.rec (snd (δ ⊨ isTm t ar w N0 N1))
    (λ { (inl (x , (e , x∈))) →
           ∣ inl (fillSnd t δ (lookup N0 δ) (down (lookup w δ) x x∈)
                    (e ∙ cong (λ a → pr a x) (sym q0)) (var i0 ∈̇ var (sh 2 w)) x∈ N0 refl) ∣₁
```

変数の分岐は、数項一の枠の存在量化子の下に証人 `i` を満たし、対応する逆向きの等式に沿って運びます。二つの分岐が、この同値を両方向で閉じます。

```agda
       ; (inr (i , (e , i∈))) →
           ∣ inr (fillSnd t δ (lookup N1 δ) (down (lookup ar δ) i i∈)
                    (e ∙ cong (λ a → pr a i) (sym q1)) (var i0 ∈̇ var (sh 2 ar)) i∈ N1 refl) ∣₁ })
```

述語 `keyUp C ar r` は、一つの正確な所属、すなわち対 `(suc ar,r)` が `C` に属することを表します。その有界存在による表現は、`C` の実際の要素を選び、その要素を順に明らかにして、対の形と後続の等式の両方を確かめます。

```agda
module _ {k : ℕ} (C ar r : Fin k) (δ : S ^ k) where
  keyUp-out : ⟨ δ ⊨ keyUp C ar r ⟩ → ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩
  keyUp-out = PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
    (λ { (c' , (c'∈ , h)) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
      (λ { (s , (s∈ , h')) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
```

外向きには、対の論理式が選ばれた `C` の要素を `(ar',r)` と同一視し、後続の論理式が `ar'` を `suc ar` と同一視します。この二つの等式に沿って所属を移すと、`(suc ar,r) ∈ C` が得られます。切り詰められた証人はすべて、この所属命題へのみ消去されます。

```agda
        (λ { (ar' , (ar'∈ , (e , hs))) →
          subst (λ u → ⟨ u ∈ fst (lookup C δ) ⟩)
            (pr-out i2 i0 (sh 3 r) (ar' ∷ s ∷ c' ∷ δ) e
             ∙ cong (λ a → pr a (fst (lookup r δ))) (suc-out (sh 3 ar) i0 (ar' ∷ s ∷ c' ∷ δ) hs))
            c'∈ })
```

したがって、三層の有界な証人は、表示された対象が `C` の要素であることを確かめるためだけに使われます。その切り詰めを消去した結果、`keyUp-out` は外部の所属 `(suc ar,r) ∈ C` をちょうど与えます。

```agda
        h' })
      h })
```

内向きには、`(suc ar,r) ∈ C` から始めます。後続アリティを構成可能集合として提示し、それと `r` の順序対をまとめ、これらを三つの有界な証人として使います。すると、対と後続の論理式から `keyUp C ar r` の充足が再構成されます。

```agda
  keyUp-in : ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩ → ⟨ δ ⊨ keyUp C ar r ⟩
  keyUp-in h = ∣ c' , (h , ∣ c .fst , (c .snd .fst , ∣ ar' , (c .snd .snd .fst
    , ( pr-in i2 i0 (sh 3 r) (ar' ∷ c .fst ∷ c' ∷ δ) (sym (cong (λ a → pr a (fst (lookup r δ))) (sucʟ-fst (lookup ar δ))))
      , suc-in (sh 3 ar) i0 (ar' ∷ c .fst ∷ c' ∷ δ) (sucʟ-fst (lookup ar δ)) )) ∣₁) ∣₁) ∣₁
    where
```

具体的には、`ar'` が `suc ar` を表し、`c'` が `C` の要素 `(suc ar,r)` を表します。さらに `c'` とともに与えられる包含集合が、論理式で使う有界所属の鎖を証します。それぞれの基礎集合の等式により、内部の証人が意図した外部の対を表すことが保証されます。

```agda
    ar' : S
    ar' = sucʟ (lookup ar δ)
    c' : S
    c' = down (lookup C δ) (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ))) h
    c = container c' ar' (lookup r δ) (cong (λ a → pr a (fst (lookup r δ))) (sym (sucʟ-fst (lookup ar δ))))
```

候補領域 `C`、アリティ値 `A`、タグ値 `N`、ペイロード `a` を固定します。これらから組み立てる単項キーは、入れ子の対 `(A,(N,a))` です。

```agda
module _ {k : ℕ} (C ar N a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

`unKey` の外向きの読みは、入れ子のキー `(A,(N,a))` が `C` に属することを正確に述べます。順序対の式の妥当性により、対象言語の所属は、ホスト側のこの集合所属へ変換されます。

```agda
  unKey-out : ⟨ δ ⊨ unKey C ar N a ⟩ → ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩
  unKey-out = E.member-out (keyExpr ar N (E.slot a)) (var C) δ
```

妥当性は逆向きにも使えます。所属 `(A,(N,a)) ∈ C` から、対象言語の述語 `unKey` の充足が得られます。したがって、キーの条項とホスト側での読みは、双方向に一致します。

```agda
  unKey-in : ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩ → ⟨ δ ⊨ unKey C ar N a ⟩
  unKey-in = E.member-in (keyExpr ar N (E.slot a)) (var C) δ
```

二項構成子について、二つのペイロード成分 `a` と `b` を固定します。その順序対 `P=(a,b)` がキー `(A,(N,P))` のペイロードとなり、アリティとタグは単項の場合と同じ外側の位置を占めます。

```agda
module _ {k : ℕ} (C ar N a b : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

二つの引数の値から順序対 `P = (a,b)` を作ります。この対が、入れ子の二項キー `(A,(N,P))` のペイロードです。

```agda
    P = pr (fst (lookup a δ)) (fst (lookup b δ))
```

`binKey` の外向きの読みは、所属 `(A,(N,(a,b))) ∈ C` にほかなりません。この形は、アリティ、構成子タグ、対にした引数という符号化の三つの論理的な層を保ちます。

```agda
  binKey-out : ⟨ δ ⊨ binKey C ar N a b ⟩ → ⟨ pr A (pr Nv P) ∈ Cv ⟩
  binKey-out = E.member-out (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ
```

内向きの読み出しはその逆向きであり、他のキーの条項と同じく、二者は論理式の主張と集合の所属を同一視します。

```agda
  binKey-in : ⟨ pr A (pr Nv P) ∈ Cv ⟩ → ⟨ δ ⊨ binKey C ar N a b ⟩
  binKey-in = E.member-in (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ
```

原子キーのペイロードは二つの項符号です。各項符号はそれぞれの項タグと引数をもち、その二つの項符号の対が、原子構成子のタグと共通のアリティの下に置かれます。

```agda
module _ {k : ℕ} (C ar N Nx x Ny y : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

二つの項符号を `T=(Nx,x)`、`U=(Ny,y)` と書きます。この段階では `Nx` と `Ny` は環境から得た任意のタグ値であり、それらが零または一であるという条件は、原子の閉性の場合を具体化するときに課されます。

```agda
    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    U = pr (fst (lookup Ny δ)) (fst (lookup y δ))
```

原子の条件を外向きに読むと、`(A,(N,(T,U))) ∈ C` となります。ここで `T` と `U` は二つの項符号です。最も外側の対がアリティを、その次が原子タグを、最も内側の対が二つの項を記録します。

```agda
  atomKey-out : ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩ → ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩
  atomKey-out = E.member-out (atomKeyExpr ar N Nx x Ny y) (var C) δ
```

内向きの読み出しはその逆向きで、これまでのどのキーの条項と同じく、原子の場合を両方向で閉じます。

```agda
  atomKey-in : ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩ → ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩
  atomKey-in = E.member-in (atomKeyExpr ar N Nx x Ny y) (var C) δ
```

有界量化子のキーのペイロードには、異なる二つの成分があります。境界を表す項符号と、本体を表す部分論理式の符号です。共通する外側のデータは、やはり現在のアリティ `A` と有界量化子タグ `N` です。

```agda
module _ {k : ℕ} (C ar N Nx x a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

境界項の符号を `T=(Nx,x)`、本体の符号を `Av` と書きます。項は現在のアリティで検査され、本体のキーは後続アリティで検査されます。両者を別々のペイロード成分として保つことで、この文法上の非対称が記録されます。

```agda
    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    Av = fst (lookup a δ)
```

有界キーの条件を外向きに読むと、`(A,(N,(T,Av))) ∈ C` となります。最も内側の対には、境界項の符号と本体の符号がこの順で入ります。この所属だけでは、どちらの成分が正当であることもまだ主張しません。

```agda
  bndKey-out : ⟨ δ ⊨ bndKey C ar N Nx x a ⟩ → ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩
  bndKey-out = E.member-out (bndKeyExpr ar N Nx x a) (var C) δ
```

逆に、`(A,(N,(T,Av)))` が `C` に属することから `bndKey` の充足が得られます。二方向の読みが確立するのは構造的な所属の同値だけです。`T` の正当性と、後続アリティにおける `Av` の所属は、周囲のペイロード述語が別に与えます。

```agda
  bndKey-in : ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩ → ⟨ δ ⊨ bndKey C ar N Nx x a ⟩
  bndKey-in = E.member-in (bndKeyExpr ar N Nx x a) (var C) δ
```

ここで、候補となる符号領域 `C`、作業集合 `W`、そして零から九までの数項であることが証明された十個の環境要素を固定します。すると各タグについて、対象言語のペイロード記述を、対応する外部の述語 `AtomP`、`BinP`、`ConP`、`QuP`、`BqP` と比較できます。

```agda
module PayRead {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (9 + m))
  (tg : Tags δ (shN 9 N)) where
  private
    Cv = fst (lookup (sh 9 C) δ)
    Wv = fst (lookup (sh 9 w) δ)
```

各ペイロードの読みでは、`A` が記録されたアリティを、`R` が生のペイロードを表します。タグ零と一の等式を取り出しておくのは、原子と有界量化子のペイロードがともに項符号を認識する必要があり、項の二つの正当な形がちょうどこの二タグを使うからです。

```agda
    A = fst (lookup i5 δ)
    R = fst (lookup i0 δ)
    q0 = tg f0
    q1 = tg f1
    rS = lookup i0 δ
```

比較の両側では、同じ基礎集合 `Wv` と `Cv` を使います。したがって、構文的なペイロード論理式が述べる `Wv` への項の所属と `Cv` への部分キーの所属は、五つの外部ペイロード述語のパラメータと正確に一致します。

```agda
    module Sh = Shape C w N
  open CodesSem Wv Cv
```

原子の本体は、ペイロードの二成分がともに、記録されたアリティで項符号の述語を満たすことを要求します。これに対して二項の本体は、両成分が同じアリティのキーとして候補領域に現れることを要求します。どちらのペイロードも対として符号化されますが、二つの条件は異なります。

```agda
  private
    tmBody : Formula S (12 + m)
    tmBody = isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ isTm i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1))
    binBody : Formula S (12 + m)
    binBody = appAt (sh 12 C) i8 i1 ∧̇ appAt (sh 12 C) i8 i0
```

最後のペイロード形は二つの有界量化子を扱います。その本体は、境界を表す項が現在のアリティで合法であることと、本体のキーが後続アリティで符号集合に属することを要求します。

```agda
    bqBody : Formula S (12 + m)
    bqBody = isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ keyUp (sh 12 C) i8 i0
```

原子ペイロードを外向きに読むと、二つの存在束縛が除かれ、項 `t` と `u`、等式 `R ≡ pr t u`、および両方の項がアリティ `A` で合法であることの証明が得られます。項の読みは 0 と 1 のタグ等式を用いて、二つの充足証明を対応する切り詰められた項の形へ変換します。

```agda
  atom-out : ⟨ δ ⊨ Sh.atomPay ⟩ → AtomP A R
  atom-out h = PT.map
    (λ { (t , u , s , (e , (ht , hu))) → fst t , fst u
       , ( e , ( isTm-out i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 ht
               , isTm-out i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 hu ) ) })
```

この消費は、二重の存在消去の一つの適用にすぎません。証人 `t`、`u` と容器を取り出し、残りの連言をペイロードのデータへ処理します。

```agda
    (bothEx-out i0 tmBody δ h)
```

内向きの読みは、データから充足を組み立て直します。切り詰められた合法性の証明は、目標もまた切り詰められた充足であるため消去でき、二つの項はそれぞれずらした文脈を通して合法性の原子に入ります。

```agda
  atom-in : AtomP A R → ⟨ δ ⊨ Sh.atomPay ⟩
  atom-in = PT.rec (snd (δ ⊨ Sh.atomPay))
    (λ { (t , u , (e , (ht , hu))) →
      fillBoth i0 δ (fstS rS t u e) (sndS rS t u e) e tmBody
        ( isTm-in i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (δ12 t u e) q0 q1 ht
```

二つ目の合法性の証明も同じ方法で入れます。補助環境 `δ12` は、`R ≡ pr t u` によって選ばれた二つの成分、その対を証明するコンテナ、元の環境からなり、二つの項の原子式はまさにこの環境で解釈されます。

```agda
        , isTm-in i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (δ12 t u e) q0 q1 hu ) })
    where
    δ12 : (t u : V ℓ) (e : R ≡ pr t u) → S ^ (12 + m)
    δ12 t u e = sndS rS t u e ∷ fstS rS t u e ∷ container rS (fstS rS t u e) (sndS rS t u e) e .fst ∷ δ
```

二項ペイロードを外向きに読むと、ペイロード `a` と `b`、等式 `R ≡ pr a b`、および `pr A a` と `pr A b` がともに符号集合に属することが得られます。二つの適用原子式の妥当性が、拡張環境におけるこれらの所属を同定します。

```agda
  bin-out : ⟨ δ ⊨ Sh.binPay ⟩ → BinP A R
  bin-out h = PT.map
    (λ { (a , b , s , (e , (ha , hb))) → fst a , fst b
       , ( e , ( subst ⟨_⟩ (appAt-adequate (sh 12 C) i8 i1 (b ∷ a ∷ s ∷ δ)) ha
               , subst ⟨_⟩ (appAt-adequate (sh 12 C) i8 i0 (b ∷ a ∷ s ∷ δ)) hb ) ) })
```

原子の場合と同じく、二項の条件の二重の存在量化は一度の消去で処理されます。

```agda
    (bothEx-out i0 binBody δ h)
```

内向きの読みは、名指された下位コードで二つの存在量化子を満たします。二つの適用の原子は、妥当性を逆向きに辿ってずらした文脈の中で充足されます。

```agda
  bin-in : BinP A R → ⟨ δ ⊨ Sh.binPay ⟩
  bin-in = PT.rec (snd (δ ⊨ Sh.binPay))
    (λ { (a , b , (e , (ha , hb))) →
      fillBoth i0 δ (fstS rS a b e) (sndS rS a b e) e binBody
        ( subst ⟨_⟩ (sym (appAt-adequate (sh 12 C) i8 i1 (δ12 a b e))) ha
```

二項の場合の補助定義も同じずらした文脈の形を記録します。今度は周囲の値 `a` と `b` から組み立てられます。

```agda
        , subst ⟨_⟩ (sym (appAt-adequate (sh 12 C) i8 i0 (δ12 a b e))) hb ) })
    where
    δ12 : (a b : V ℓ) (e : R ≡ pr a b) → S ^ (12 + m)
    δ12 a b e = sndS rS a b e ∷ fstS rS a b e ∷ container rS (fstS rS a b e) (sndS rS a b e) e .fst ∷ δ
```

偽のペイロードには下位データがありません。その論理式は `R` が 0 タグのスロットに格納された値に等しいことを述べ、`ConP A R` は `R ≡ # 0` を述べます。0 タグの等式と合成することで外向きの方向が得られます。

```agda
  con-out : ⟨ δ ⊨ Sh.conPay ⟩ → ConP A R
  con-out h = h ∙ q0
```

逆に、等式 `R ≡ # 0` を 0 タグの等式の逆向きと合成すると、`R` が 0 タグのスロットの値に等しいことが示されます。これは偽のペイロードの充足そのものです。

```agda
  con-in : ConP A R → ⟨ δ ⊨ Sh.conPay ⟩
  con-in h = h ∙ sym q0
```

どちらの非有界量化子でも、ペイロードは後続アリティにおける本体のキーです。後続キーの読みは、このペイロード論理式の充足を `pr (sucV A) R` が符号集合に属することへ変換します。

```agda
  qu-out : ⟨ δ ⊨ Sh.quPay ⟩ → QuP A R
  qu-out = keyUp-out (sh 9 C) i5 i0 δ
```

逆向きには、`pr (sucV A) R` が符号集合に属することから後続キーの論理式に必要な証人が得られ、量化子ペイロードが証明されます。

```agda
  qu-in : QuP A R → ⟨ δ ⊨ Sh.quPay ⟩
  qu-in = keyUp-in (sh 9 C) i5 i0 δ
```

有界量化子のペイロードを外向きに読むと、項 `t`、本体のペイロード `a`、等式 `R ≡ pr t a` が得られます。さらに、`t` がアリティ `A` で合法であることと、本体のキー `pr (sucV A) a` が符号集合に属することも得られます。

```agda
  bq-out : ⟨ δ ⊨ Sh.bqPay ⟩ → BqP A R
  bq-out h = PT.map
    (λ { (t , a , s , (e , (ht , ha))) → fst t , fst a
       , ( e , ( isTm-out i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (a ∷ t ∷ s ∷ δ) q0 q1 ht
               , keyUp-out (sh 12 C) i8 i0 (a ∷ t ∷ s ∷ δ) ha ) ) })
```

有界の本体の二重の存在量化は、他の場所と同じく二重の消去で処理されます。

```agda
    (bothEx-out i0 bqBody δ h)
```

内向きの読みでは、境界の項がずらした文脈を通して合法性の原子に入ります。

```agda
  bq-in : BqP A R → ⟨ δ ⊨ Sh.bqPay ⟩
  bq-in = PT.rec (snd (δ ⊨ Sh.bqPay))
    (λ { (t , a , (e , (ht , ha))) →
      fillBoth i0 δ (fstS rS t a e) (sndS rS t a e) e bqBody
        ( isTm-in i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (δ12 t a e) q0 q1 ht
```

本体の鍵は後続の鍵の補題を通して入り、補助定義は境界の値とその容器から作られるずらした文脈の形を記録します。

```agda
        , keyUp-in (sh 12 C) i8 i0 (δ12 t a e) ha ) })
    where
    δ12 : (t a : V ℓ) (e : R ≡ pr t a) → S ^ (12 + m)
    δ12 t a e = sndS rS t a e ∷ fstS rS t a e ∷ container rS (fstS rS t a e) (sndS rS t a e) e .fst ∷ δ
```

タグの読みはタグの上の再帰で選ばれます。タグ 0 と 1 が二つの原子式、タグ 2、3、4 が三つの二項結合子です。

```agda
  payN-out : (k : ℕ) → ⟨ δ ⊨ Sh.payN k ⟩ → PayN k A R
  payN-out 0 = atom-out
  payN-out 1 = atom-out
  payN-out 2 = bin-out
  payN-out 3 = bin-out
```

タグ 5、6、7 は偽と二つの非有界の量化子を、タグ 8 は有界の全称を担います。

```agda
  payN-out 4 = bin-out
  payN-out 5 = con-out
  payN-out 6 = qu-out
  payN-out 7 = qu-out
  payN-out 8 = bq-out
```

タグ 9 が有界の存在です。タグ 10 以上は構成子を名指さないためペイロードは空であり、読みはその空のデータの上の恒等写像です。

```agda
  payN-out 9 = bq-out
  payN-out (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h
```

内向きの読みも同じ再帰で選ばれ、タグごとに一つの節をもちます。

```agda
  payN-in : (k : ℕ) → PayN k A R → ⟨ δ ⊨ Sh.payN k ⟩
  payN-in 0 = atom-in
  payN-in 1 = atom-in
  payN-in 2 = bin-in
  payN-in 3 = bin-in
```

タグ 4 から 7 までが一覧を続けます。最後の二項結合子、偽、そして二つの非有界の量化子です。

```agda
  payN-in 4 = bin-in
  payN-in 5 = con-in
  payN-in 6 = qu-in
  payN-in 7 = qu-in
  payN-in 8 = bq-in
```

タグ 9 が一覧を完成させます。10 以上を読むべきものはありません。そのようなタグをもつ合法な鍵はないからです。

```agda
  payN-in 9 = bq-in
  payN-in (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h
```

十通りの読みは、周囲の環境を七項目だけ拡張した環境でタグ付きペイロードを解釈します。符号集合と定数アルファベットは周囲の項目から読み、`N` は周囲の環境にある十個の位置を選びます。タグの仮定は、それらの値をそれぞれ数項 0 から 9 までと同定します。

```agda
module TenRead {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (7 + m))
  (tg : Tags δ (shN 7 N)) where
  private
    Cv = fst (lookup (sh 7 C) δ)
    Wv = fst (lookup (sh 7 w) δ)
```

新たに束縛された項目のうち、`A` はアリティであり、`P` はキーとして認識すべきタグ付きペイロードです。`P` の集合レベルの表示を保つことで、タグとそのペイロード `r` を選んだときに等式 `P ≡ pr (# (toℕ j)) r` を実現できます。

```agda
    A = fst (lookup i3 δ)
    P = fst (lookup i0 δ)
    pS = lookup i0 δ
    module Sh = Shape C w N
  open CodesSem Wv Cv
```

タグの読みは、`j` 番目のタグの原子の充足を鍵へ変換します。切り詰められた証人は添字 `r` と容器の対であり、符号化の等式は、`j` 番目のタグのスロットが `j` の数項を名指すというタグの等式に沿って輸送され、ペイロードはタグ `j` での読みによって読まれます。

```agda
  at-out : (j : Fin 10) → ⟨ δ ⊨ Sh.at j ⟩ → Key A P
  at-out j h = PT.map
    (λ { (r , s , (e , hp)) → j , fst r
       , ( e ∙ cong (λ a → pr a (fst r)) (tg j)
         , PayRead.payN-out C w N (r ∷ s ∷ δ) tg (toℕ j) hp ) })
```

タグの原子の二重の存在量化はみずからの消去で処理されるため、読みが添字を選ぶことはありません。充足が与える一つを展開するだけです。

```agda
    (sndEx-out i0 (sh 7 (N j)) (Sh.pay j) δ h)
```

内向きの方向は、鍵から充足を組み立てます。証人の項目はずらした値で満たされ、ペイロードは拡張された文脈の上で内向きに読まれ、タグの等式が名指しのスロットを `j` の数項と同一視します。

```agda
  at-in : (j : Fin 10) (r : V ℓ) (e : P ≡ pr (# (toℕ j)) r) → PayN (toℕ j) A r → ⟨ δ ⊨ Sh.at j ⟩
  at-in j r e pay =
    fillSnd i0 δ (lookup (sh 7 (N j)) δ) rS e' (Sh.pay j)
      (PayRead.payN-in C w N (rS ∷ container pS (lookup (sh 7 (N j)) δ) rS e' .fst ∷ δ) tg (toℕ j) pay)
      (sh 7 (N j)) refl
```

改名された値は `j` の数項と選ばれた項目を対にし、符号化の等式はタグの等式と逆向きに合成されて、拡張された名指しが正しいスロットに触れるようにします。

```agda
    where
    rS : S
    rS = sndS pS (# (toℕ j)) r e
    e' : P ≡ pr (fst (lookup (sh 7 (N j)) δ)) (fst rS)
    e' = e ∙ cong (λ a → pr a r) (sym (tg j))
```

十通りの外向きの読みは選言を消費し、証人が名指すタグのところでタグの読みを引用します。

```agda
  ten-out : ⟨ δ ⊨ Sh.ten ⟩ → Key A P
  ten-out h = PT.rec squash₁ (λ { (j , hj) → at-out j hj }) (bigOr-out δ 9 Sh.at h)
```

内向きの読みは、証人の現れたタグで選言に入り、ペイロードもそのタグで内向きに読まれます。二つの方向合わせて、十通りの選言の充足と、合法な鍵をもつことは同じことだと述べています。

```agda
  ten-in : Key A P → ⟨ δ ⊨ Sh.ten ⟩
  ten-in = PT.rec (snd (δ ⊨ Sh.ten))
    (λ { (j , r , (e , pay)) → bigOr-in δ 9 Sh.at j (at-in j r e pay) })
```

形の読みは三つの周囲の集合を固定します。候補となる符号集合 `C`、定数アルファベット `w`、そしてアリティと族の対からなる塔 `E` です。それぞれの基礎にある反復集合は、符号の所属、定数項の合法性、塔に属する証人 `(ar,F)` に用いられます。

```agda
module ShapeRead {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Cv = fst (lookup C γ)
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)
```

選ばれた要素 `c` と塔の証人 `(ar,F)` に対し、残りの論理式はペイロード `p` を選び、`c ≡ pr ar p` を要求し、十通りのタグ形に照らして `p` を検査します。このように、入れ子になった証人は外側のアリティと内側のタグ付きペイロードを別々に明らかにします。

```agda
    module Sh = Shape C w N
    inner : Formula S (5 + m)
    inner = sndEx i4 i1 Sh.ten
  open CodesSem Wv Cv
```

`Shaped c` は形の節から取り出されるデータをそのまま記録します。`pr ar F` が `E` に属し、`c ≡ pr ar p` が成り立ち、`p` がアリティ `ar` における合法なタグ付きペイロードとなる `ar`、`F`、`p` が存在します。この存在データはすべて命題的に切り詰められており、分解の一意性は主張しません。

```agda
  Shaped : V ℓ → Type (ℓ-suc ℓ)
  Shaped c = ∥ Σ[ ar ∈ V ℓ ] Σ[ F ∈ V ℓ ] Σ[ p ∈ V ℓ ]
               (⟨ pr ar F ∈ Ev ⟩ × ((c ≡ pr ar p) × Key ar p)) ∥₁
```

符号集合の各 `c` について、外向きの読みはまず `E` の要素 `q` を得ます。`q` を分解すると `ar` と `F` および等式 `q ≡ pr ar F` が得られ、内側の存在量化からは `p`、等式 `c ≡ pr ar p`、十通りのペイロード論理式の充足が得られます。

```agda
  shape-out : ⟨ γ ⊨ shapeAt C w E N ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)
  shape-out h c c∈ = PT.rec squash₁
    (λ { (q , (q∈ , hb)) → PT.rec squash₁
      (λ { (ar , F , s , (eq , hs)) → PT.map
        (λ { (p , s' , (ec , ht)) →
```

等式 `q ≡ pr ar F` は、既知の `q` の `E` への所属を `pr ar F` の所属へ輸送します。`c` に関する等式は保持され、十通りの読みが残りの充足証明を `Key ar p` へ変換します。

```agda
          fst ar , fst F , fst p
          , ( subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈
            , ( ec , TenRead.ten-out C w N (p ∷ s' ∷ F ∷ ar ∷ s ∷ q ∷ c ∷ γ) tg ht ) ) })
        (sndEx-out i4 i1 Sh.ten (F ∷ ar ∷ s ∷ q ∷ c ∷ γ) hs) })
      (bothEx-out i0 inner (q ∷ c ∷ γ) hb) })
```

元の形の充足は符号集合の要素について全称量化されています。これを `c` とその所属証明に適用すると、上で除去した存在データが得られ、`Shaped (fst c)` の構成が完了します。

```agda
    (h c c∈)
```

内向きの方向では、符号集合の各要素 `c` が切り詰められた形のデータをもつと仮定します。その切り詰めを除去すると、`ar`、`F`、`p` とともに、`pr ar F` の `E` への所属、`c` に関する等式、`Key ar p` が得られます。目標自体が命題なので、この除去は正当です。

```agda
  shape-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)) → ⟨ γ ⊨ shapeAt C w E N ⟩
  shape-in k c c∈ = PT.rec (snd ((c ∷ γ) ⊨ ∃̇∈ (var (sh 1 E)) (bothEx i0 inner)))
    (λ { (ar , F , p , (q∈ , (ec , key))) →
      let qS = down (lookup E γ) (pr ar F) q∈
          arS = fstS qS ar F refl
```

`pr ar F` が `E` に属することから集合レベルの表示 `qS` が得られ、その二成分がそれぞれ `ar` と `F` を表します。これとは別に、等式 `c ≡ pr ar p` は `c` の内部でペイロードの表示 `pS` を選びます。二つの対コンテナが、入れ子の存在論理式に必要な環境を与えます。

```agda
          FS = sndS qS ar F refl
          δ2 = qS ∷ c ∷ γ
          cq = container qS arS FS refl
          δ5 = FS ∷ arS ∷ cq .fst ∷ δ2
          pS = sndS c ar p ec
```

内側の論理式はアリティと表のデータで満たされ、十通りの選言は鍵で満たされます。こうして形の充足の全体が、実際のデータから組み上がります。

```agda
          cp = container c arS pS ec
          δ7 = pS ∷ cp .fst ∷ δ5
      in ∣ qS , ( q∈ , fillBoth i0 δ2 arS FS refl inner
            (fillSnd i4 δ5 arS pS ec Sh.ten
              (TenRead.ten-in C w N δ7 tg key) i1 refl) ) ∣₁ })
```

仮定した形の割り当てを `c` とその所属に適用すると、内向きの構成で用いる切り詰められた証人がちょうど得られます。外向きの方向と合わせると、符号集合の各要素について、形の論理式の充足が命題 `Shaped` と一致することが分かります。

```agda
    (k c c∈)
```

塔の要素を `q ≡ pr ar F` と分解した後で、各閉性の節を解釈します。得られる四項目の拡張では、`A` は固定されたアリティ `ar` です。符号集合と定数アルファベットは周囲の環境から引き続き参照でき、タグ等式もシフト後に保たれます。

```agda
module CloseRead {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (4 + m)) (tg : Tags δ (shN 4 N)) where
  private
    Cv = fst (lookup (sh 4 C) δ)
    A = fst (lookup i1 δ)
    arS = lookup i1 δ
```

この固定アリティで、閉性条件は、必要な形の入力に十個の構成子のいずれかを適用すると結果が再び符号集合に属することを述べます。各節について、外向きと内向きの読みは、その有界論理式を対応する閉性と同定します。

```agda
    CS = lookup (sh 4 C) δ
    module Cl = Close C w N
```

原子の閉性の節を外向きに読むと、`X` が選ぶ境界から任意の `x` を取り、さらに `x` で拡張した環境で `Y` が選ぶ境界から任意の `y` を取れます。その結果、アリティ `A`、構成子タグ `k`、項の形を示すタグ `Nx` と `Ny` をもつ原子キーが符号集合に属することが得られます。

```agda
  atomClose-out : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m))
                → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
                → (x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩
  atomClose-out k Nx Ny X Y h x y x∈ y∈ =
```

この所属は、三つのタグの等式に沿って輸送されます。節はタグつきのスロットで述べられる一方、鍵は三つのタグの数項で書かれるからです。

```agda
    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny)))))
      (atomKey-out (sh 6 C) i3 (sh 6 (N k)) (sh 6 (N Nx)) i1 (sh 6 (N Ny)) i0 (y ∷ x ∷ δ) (h x x∈ y y∈))
```

内向きの方向は節を組み立て直します。すべての対に対する性質が与えられていれば、与えられた `x` と `y` で具体化し、名指しの等式を逆向きに走らせれば足ります。

```agda
  atomClose-in : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m))
               → ((x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                  → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩)
               → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
  atomClose-in k Nx Ny X Y g x x∈ y y∈ =
```

所属は逆向きの改名に沿ってタグつきのスロットへ輸送され、閉包の節の導入規則がこの場合を閉じます。

```agda
    atomKey-in (sh 6 C) i3 (sh 6 (N k)) (sh 6 (N Nx)) i1 (sh 6 (N Ny)) i0 (y ∷ x ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny))))))
        (g x y x∈ y∈))
```

二項の閉性の節は、符号集合の二つの要素 `c₁` と `c₂` を量化します。等式 `fst c₁ ≡ pr A (fst a)` と `fst c₂ ≡ pr A (fst b)` は、固定アリティ `A` におけるそれぞれのペイロード `a` と `b` を取り出します。すると、この節はペイロード `pr (fst a) (fst b)` をもつ二項キーが再び符号集合に属することを述べます。

```agda
  binClose-out : (k : Fin 10) → ⟨ δ ⊨ Cl.binClose k ⟩
               → (c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
               → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
               → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩
  binClose-out k h c₁ c₂ a b c₁∈ c₂∈ e₁ e₂ =
```

所属はタグの改名に沿って輸送され、二重に入れ子になった全称の層は有界量化子の消去の補題によって処理されます。各項目はみずからの対の容器を通して内側の節に入ります。

```agda
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k)))
      (binKey-out (sh 10 C) i7 (sh 10 (N k)) i3 i0 δ10
        (useSnd i0 δ8 arS b e₂ (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0) i5 refl
          (useSnd i0 (c₁ ∷ δ) arS a e₁ inner i2 refl (h c₁ c₁∈) c₂ c₂∈)))
    where
```

`c₁` を選んで `pr A a` と表した後、内側の論理式は符号集合の第二の符号 `c₂` を量化し、それを `pr A b` として取り出します。次に、タグ `k` と対にしたペイロード `pr a b` からなる二項キーが符号集合に属することを要求します。補助環境は `c₁` と `c₂` の二つの分解を記録します。

```agda
    inner : Formula S (7 + m)
    inner = ∀̇∈ (var (sh 7 C)) (sndAll i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0))
    δ7 : S ^ (7 + m)
    δ7 = a ∷ container c₁ arS a e₁ .fst ∷ c₁ ∷ δ
    δ8 : S ^ (8 + m)
```

量化子の条項では、下位キーと、そのアリティを定めるデータを同時に覚えておく必要があります。環境 `δ8` は、候補となる引数 `a`、後続アリティの候補 `ar'`、両者の関係を証明する順序対、下位キー `c₁` を含みます。有界量化子を扱う `δ10` には、境界となる項も加わります。

```agda
    δ8 = c₂ ∷ δ7
    δ10 : S ^ (10 + m)
    δ10 = b ∷ container c₂ arS b e₂ .fst ∷ δ8
```

二項閉包の条項を内向きに読むときは、対応する数学的な閉包則から出発します。同じアリティをもつ二つの下位キーが領域に属するなら、それらから作られる複合キーも領域に属します。二つの全称量化は、選んだ下位キーを明示するためのものです。

```agda
  binClose-in : (k : Fin 10)
              → ((c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
                 → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
                 → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩)
              → ⟨ δ ⊨ Cl.binClose k ⟩
```

二つの量化された成分を論理式が定める順に導入すると、対応する拡張環境が得られます。最も内側の含意では、仮定した閉包則から複合キーの所属が得られ、タグの等式 `tg k` が、表示されたタグを `binKey` の要求する数項に揃えます。

```agda
  binClose-in k g c₁ c₁∈ = sndAll-in i0 i2 (∀̇∈ (var (sh 7 C)) (sndAll i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0))) (c₁ ∷ δ) (λ a s s∈ a∈ e₁ c₂ c₂∈ →
    sndAll-in i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0) (c₂ ∷ a ∷ s ∷ c₁ ∷ δ) (λ b s' s'∈ b∈ e₂ →
      binKey-in (sh 10 C) i7 (sh 10 (N k)) i3 i0 (b ∷ s' ∷ c₂ ∷ a ∷ s ∷ c₁ ∷ δ)
        (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k))))
          (g c₁ c₂ a b c₁∈ c₂∈ e₁ e₂))))
```

偽の符号には調べるべき下位符号がありません。したがって、その閉包条項を外向きに読むには、ペイロードが零の数項に等しいことを用い、タグの等式に沿って輸送すれば十分です。

```agda
  conClose-out : (k : Fin 10) → ⟨ δ ⊨ Cl.conClose k ⟩ → ⟨ pr A (pr (# (toℕ k)) (# 0)) ∈ Cv ⟩
  conClose-out k h =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong₂ pr (tg k) (tg f0)))
      (unKey-out (sh 4 C) i1 (sh 4 (N k)) (sh 4 (N f0)) δ h)
```

逆に、偽のキーの所属を同じ等式に沿って反対向きに輸送すれば、閉包条項の充足が得られます。この場合には再帰的な前提がなく、零のペイロードだけでキーが完全に定まります。

```agda
  conClose-in : (k : Fin 10) → ⟨ pr A (pr (# (toℕ k)) (# 0)) ∈ Cv ⟩ → ⟨ δ ⊨ Cl.conClose k ⟩
  conClose-in k h =
    unKey-in (sh 4 C) i1 (sh 4 (N k)) (sh 4 (N f0)) δ
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong₂ pr (tg k) (tg f0)))) h)
```

非有界量化子の条項は、量化された成分を明示して外向きに読まれます。領域の下位キー `c₁`、その表示 `c₁ = pr ar' a`、そして等式 `ar' = sucV A` が与えられれば、現在のアリティでの量化子のキーが領域に属します。三つの仮定は、前者のスライスの要素のデータそのものです。

```agda
  quClose-out : (k : Fin 10) → ⟨ δ ⊨ Cl.quClose k ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
              → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩
  quClose-out k h c₁ ar' a c₁∈ e₁ es =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (fst a)) (tg k)))
```

証明では、`a`、`ar'`、コンテナを環境に加え、後続の等式を用いて含意の結論へ進み、八つのスロットをもつ環境で `unKey` の所属を読み取ります。さらにタグの等式に沿って輸送し、タグ `k` が表す数項に対応する所属を得ます。

```agda
      (unKey-out (sh 8 C) i5 (sh 8 (N k)) i0 δ8
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ unKey (sh 8 C) i5 (sh 8 (N k)) i0) (h c₁ c₁∈)
          (suc-in i5 i1 δ8 es)))
    where
    δ8 : S ^ (8 + m)
```

拡張された環境は、量化された三つの成分を、含意が読む順に、もとの成分とともにまとめます。

```agda
    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ
```

内向きに読むときは、条項で量化された二つの成分を導入します。拡張環境には、後続アリティの候補 `ar'` とペイロード `a` が入り、後続の等式が含意の前提を与えます。

```agda
  quClose-in : (k : Fin 10)
             → ((c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.quClose k ⟩
  quClose-in k g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ unKey (sh 8 C) i5 (sh 8 (N k)) i0) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs →
```

これらのデータに仮定した閉包則を適用し、得られた所属をタグの等式に沿って輸送すると、`unKey` の結論が得られます。これで、非有界量化子の条項を内向きに読む証明が完成します。

```agda
    unKey-in (sh 8 C) i5 (sh 8 (N k)) i0 (a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (fst a)) (tg k))))
        (g c₁ ar' a c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs))))
```

有界量化子の条項には前提が一つ加わります。後続アリティでの本体キーに加えて、現在のアリティで正しい境界項 `x` が必要です。得られるペイロードは、量化子のタグ、項のタグ `Nx`、その項、本体のペイロードを入れ子の順序対として記録します。

```agda
  bqClose-out : (k Nx : Fin 10) (X : Fin (8 + m)) → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → (e₁ : fst c₁ ≡ pr (fst ar') (fst a)) → fst ar' ≡ sucV A
              → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ)) ⟩
              → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩
  bqClose-out k Nx X h c₁ ar' a c₁∈ e₁ es x x∈ =
```

証明では、境界を表す項を環境に加え、その環境で有界キーの消去を適用します。二つのタグ等式は、それぞれ量化子の構成子と項の構成子に対応し、入れ子の対を結論で指定された形へ輸送します。

```agda
    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx)))))
      (bndKey-out (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1 (x ∷ δ8)
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1))
          (h c₁ c₁∈) (suc-in i5 i1 δ8 es) x x∈))
```

八つの枠の環境は、非有界の場合と同じまとめ方を繰り返し、界の枠は消去に使われます。

```agda
    where
    δ8 : S ^ (8 + m)
    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ
```

内向きに読むため、型に示された数学的閉包則を仮定します。この規則が任意の拡張環境 `s` について量化されているのは、境界を表す項を選ぶ集合が、その環境で評価されるからです。

```agda
  bqClose-in : (k Nx : Fin 10) (X : Fin (8 + m))
             → ((c₁ ar' a s : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ s ∷ c₁ ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩
```

量化された下位キーのデータと境界を表す項を導入し、得られた環境で仮定した閉包則を適用します。その結論を二つのタグ等式に沿って輸送すると、`bndKey` が要求する所属が得られ、有界量化子の条項を内向きに読む証明が完成します。

```agda
  bqClose-in k Nx X g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1)) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs x x∈ →
    bndKey-in (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1 (x ∷ a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx))))))
        (g c₁ ar' a s c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs) x x∈)))
```

## 健全性：各要素の復号

健全性を証明するため、ここまでに得た三つの記述を結びます。数値タグは十種類の構成子を識別し、形と閉包の論理式は集合内部の符号を記述し、`AllCodes` はそれらの符号を外部の論理式文法へ結び戻します。関係する性質は命題なので、代表を選ばずに切り詰められた証人を除去できます。

```agda
open import L.Coding.Expressions {ℓ} using ( tagAtL-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeShape {ℓ} using
  ( shapedAt; shaped-in; ShapeWit; BinWit; bothTm; fstTm; noneB; isTmAt )
open import L.Coding.CodeSet {ℓ} lem using
```

標準的な符号集合は、この比較の両方向を与えます。その要素は論理式キーとして読め、どの論理式にも標準的なキーがあります。残りの導入からは、記録されたアリティの証人と、二つの命題の連言も命題であるという事実を得ます。

```agda
  ( AllCodes; AllCodes-out; key∈AllCodes; keyS; codeS; witnessAt-out )
open import Cubical.Foundations.HLevels using ( isProp× )
```

定数として現れうる要素をもつ作業集合 `Wv` と、候補となる符号領域 `Cv` を固定します。以下の議論はこの二つの集合をパラメータとし、この時点では `Cv` が標準的な領域 `AllCodes` であるとは仮定しません。

```agda
module _ (Wv Cv : V ℓ) where
  open CodesSem Wv Cv
```

どのペイロード条件 `PayN n ar r` も命題です。タグ 0 から 4 については命題的切り詰めから直ちに従います。対応する条件は、適切な成分が単に存在することだけを述べるからです。

```agda
  isPropPayN : (n : ℕ) (ar r : V ℓ) → isProp (PayN n ar r)
  isPropPayN 0 ar r = squash₁
  isPropPayN 1 ar r = squash₁
  isPropPayN 2 ar r = squash₁
  isPropPayN 3 ar r = squash₁
```

残りの構成子タグでも、各ペイロードに応じた形で同じ原理を用います。偽のペイロードは零に一意に等しく、非有界量化子は命題値をとる `Cv` への所属を要求し、有界量化子は再び切り詰められた存在を用います。

```agda
  isPropPayN 4 ar r = squash₁
  isPropPayN 5 ar r = setIsSet r (# 0)
  isPropPayN 6 ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN 7 ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN 8 ar r = squash₁
```

タグ 9 も切り詰められた存在によって扱われます。十種類の構成子タグを越える数項ではペイロード型が空であり、空型は命題です。したがって `PayN` は、どの自然数タグについても命題値をとります。

```agda
  isPropPayN 9 ar r = squash₁
  isPropPayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ar r = Empty.isProp⊥*
```

キーを揃える補題は、アリティ `ar` での `Key` を、同じ集合の別の分解 `p = (# n, r)` でのペイロードへ変えます。対の単射性と数項の単射性が、タグとペイロードを別々に揃えます。そして `PayN n ar r` は命題なので、切り詰められたキーをそこへ消去できます。

```agda
  keyAt : (ar p : V ℓ) → Key ar p → (n : ℕ) (r : V ℓ) → p ≡ pr (# n) r → PayN n ar r
  keyAt ar p key n r e = PT.rec (isPropPayN n ar r)
    (λ { (k , r' , (e' , pay)) →
      let q = pr-inj (sym e ∙ e')
      in subst2 (λ j x → PayN j ar x) (sym (#-inj′ (q .fst))) (sym (q .snd)) pay })
```

この除去を `key` に適用すると、位置合わせが完了します。`Key` から得たタグとペイロードは、指定された数項 `n` とペイロード `r` へすでに輸送されています。

```agda
    key
```

最初の復元の補題は、項の符号の主張を、形の章の項の述語の充足へ変換します。任意の枠に対して述べられ、切り詰められた `IsTmV` を、命題値の充足へ消去することで証明されます。

```agda
tmWit : ∀ {j} (ti Ni Ai : Fin j) (env : S ^ j)
      → IsTmV (fst (lookup Ai env)) (fst (lookup ti env)) (fst (lookup Ni env))
      → ⟨ env ⊨ isTmAt ti Ni Ai ⟩
tmWit ti Ni Ai env = PT.rec (snd (env ⊨ isTmAt ti Ni Ai))
  (λ { (inl (x , (e , x∈))) →
```

定数の分岐では、`down` が証人 `x` を作業集合 `Wv` の要素として表示します。タグの妥当性が順序対の等式を輸送し、もとの所属証明がもう一方の連言肢を与えます。得られた証拠は、形の述語の左の選言肢に入ります。

```agda
         ∣ inl ∣ down (lookup Ai env) x x∈
           , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc ti) 0 zero (down (lookup Ai env) x x∈ ∷ env))) e
             , x∈ ) ∣₁ ∣₁
     ; (inr (i , (e , i∈))) →
         ∣ inr ∣ down (lookup Ni env) i i∈
```

変数の分岐は、数項の枠で添字を提示して、同じ構成を繰り返します。二つの分岐合わせて、項の符号から形の充足への変換に選択が不要であることが分かります。

```agda
           , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc ti) 1 zero (down (lookup Ni env) i i∈ ∷ env))) e
             , i∈ ) ∣₁ ∣₁ })
```

これで候補領域 `C` の健全性を述べられます。定数字母表が集合 `W` であり、十個のタグ枠に正しい数項が入り、環境集合に記録された各アリティが自然数の数項であり、`C` が形の記述を満たすと仮定します。これらの仮定から、`C` の各要素を論理式キーとして復元します。

```agda
module CodesSound {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (arity : (n F : S) → ⟨ pr (fst n) (fst F) ∈ fst (lookup E γ) ⟩ → ∥ Σ[ k ∈ ℕ ] (fst n ≡ # k) ∥₁)
  (hs : ⟨ γ ⊨ shapeAt C w E N ⟩) where
  private
```

`Cv` を候補領域の基礎となる集合、`CS` を構成可能性の証明とともにその集合をまとめた、構成可能構造内の表示と書きます。同様に、`Wv` と `Ev` は作業集合と環境集合の基礎となる集合を表します。これらの略記により、所属の主張で使うホスト側の集合と、一階環境で使う証明つきの表示とを区別します。

```agda
    Cv = fst (lookup C γ)
    CS = lookup C γ
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)
    module SR = ShapeRead C w E N γ tg
```

以後、すべてのペイロード条件を、固定した作業集合 `Wv` と候補領域 `Cv` に相対して解釈します。

```agda
  open CodesSem Wv Cv
```

証明ではいくつかの補助補題を通して、形の論理式の中に隠されたペイロード情報を順に復元します。

```agda
  private
```

選んだ要素 `c` に対し、環境 `δ' c` は候補領域と `c` を元の環境の前に置きます。その要素についての形の述語は、この環境で解釈されます。

```agda
    δ' : S → S ^ (2 + m)
    δ' c = CS ∷ c ∷ γ
```

揃えの補題 `at` が健全性の中心です。要素 `c` での形の充足から、切り詰められた形の証人を取り出し、対の等式を目標の分解と揃え、`keyAt` を適用してペイロードを番号つきの分解へ移します。ペイロードが命題なので、この消去は正当です。

```agda
    at : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (ar r : V ℓ) → fst c ≡ pr ar (pr (# n) r)
       → PayN n ar r
    at c c∈ n ar r e = PT.rec (isPropPayN Wv Cv n ar r)
      (λ { (ar' , F , p , (q∈ , (ec , key))) →
        let q = pr-inj (sym ec ∙ e)
```

アリティの等式は最後に輸送されます。形の証人と目標の分解が、アリティを異なる集合で提示するかもしれないからです。ペイロードの源は、その要素での、章の仮定の形の読み出しです。

```agda
        in subst (λ a → PayN n a r) (q .fst) (keyAt Wv Cv ar' p key n r (q .snd)) })
      (SR.shape-out hs c c∈)
```

二項の抽出器は、二項のペイロードを、同じアリティの領域の中の二つの下位キーへ変換します。その主張はタグの等式を明示します。ペイロードが、示された対と揃えなければならない番号つきの分解で得られたものだからです。

```agda
    binAt : (k : ℕ) → PayN k ≡ BinP → (c ar a b : S) → ⟨ fst c ∈ Cv ⟩
          → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
          → ⟨ pr (fst ar) (fst a) ∈ Cv ⟩ × ⟨ pr (fst ar) (fst b) ∈ Cv ⟩
    binAt k eq c ar a b c∈ e = PT.rec (isProp× (snd (pr (fst ar) (fst a) ∈ Cv)) (snd (pr (fst ar) (fst b) ∈ Cv)))
      (λ { (a' , b' , (er , (ha , hb))) →
```

対の単射性が等式を二つの成分の等式に分け、それぞれの下位キーが所定の位置へ運ばれます。ペイロードの源は、番号つきのタグでその要素に適用した揃えの補題です。

```agda
        let q = pr-inj er
        in subst (λ u → ⟨ pr (fst ar) u ∈ Cv ⟩) (sym (q .fst)) ha
         , subst (λ u → ⟨ pr (fst ar) u ∈ Cv ⟩) (sym (q .snd)) hb })
      (subst (λ P → P (fst ar) (pr (fst a) (fst b))) eq (at c c∈ k (fst ar) (pr (fst a) (fst b)) e))
```

有界量化子の抽出補題は、有界ペイロードから、その本体キーが後続アリティで属することを導きます。証明では、切り詰められたペイロードを除去し、対の第二成分についての等式に沿って内側の所属を輸送します。

```agda
    bqAt : (k : ℕ) → PayN k ≡ BqP → (c ar a b : S) → ⟨ fst c ∈ Cv ⟩
         → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
         → ⟨ pr (sucV (fst ar)) (fst b) ∈ Cv ⟩
    bqAt k eq c ar a b c∈ e = PT.rec (snd (pr (sucV (fst ar)) (fst b) ∈ Cv))
      (λ { (t , a' , (er , (ht , ha))) →
```

有界ペイロードを表示された入れ子の順序対に揃えると、その本体成分は後続アリティでのキーそのものです。対応する成分の等式に沿ってこの所属を輸送すれば、求める結論が得られます。

```agda
        subst (λ u → ⟨ pr (sucV (fst ar)) u ∈ Cv ⟩) (sym (pr-inj er .snd)) ha })
      (subst (λ P → P (fst ar) (pr (fst a) (fst b))) eq (at c c∈ k (fst ar) (pr (fst a) (fst b)) e))
```

これらの抽出補題から、符号上の再帰に必要な下向き閉包が得られます。三つの二項結合子のそれぞれについて、複合キーが領域に属すれば、その二つの直接の下位キーも同じアリティで領域に属します。

```agda
    hcl : (c : S) → ⟨ δ' c ⊨ closedAt zero ⟩
    hcl c =
        binSameClosed-in zero 2 (δ' c) (binAt 2 refl)
      , ( binSameClosed-in zero 3 (δ' c) (binAt 3 refl)
      , ( binSameClosed-in zero 4 (δ' c) (binAt 4 refl)
```

量化子についても、アリティの変化を伴う同様の結論が成り立ちます。アリティ `n` の非有界または有界量化子キーは、後続アリティでの本体キーを含みます。有界の場合には、ペイロードの形を確認したあと、境界項の成分を取り除きます。

```agda
      , ( unSuccClosed-in zero 6 (δ' c) (λ c' ar a c'∈ e → at c' c'∈ 6 (fst ar) (fst a) e)
      , ( unSuccClosed-in zero 7 (δ' c) (λ c' ar a c'∈ e → at c' c'∈ 7 (fst ar) (fst a) e)
      , ( binSuccClosed-in zero 8 (δ' c) (bqAt 8 refl)
      ,   binSuccClosed-in zero 9 (δ' c) (bqAt 9 refl) )))))
```

あとは、候補領域の任意の要素 `c'` の完全な形を復元します。形の記述が切り詰められた分解を与え、環境についての仮定がそのアリティを自然数の数項と同定し、`Key` がタグとペイロードを同定します。復元結果は全体を通して切り詰められたままです。

```agda
    wit : (c c' : S) → ⟨ fst c' ∈ Cv ⟩ → ∥ ShapeWit (sh 2 w) (δ' c) c' ∥₁
    wit c c' c'∈ = PT.rec squash₁
      (λ { (ar , F , p , (q∈ , (ec , key))) → PT.rec squash₁
        (λ { (k , r , (e' , pay)) →
          let qS = down (lookup E γ) (pr ar F) q∈
```

復元したデータは、関係する集合の内部の表示として与えられます。`qS` は環境の要素を、`arS` はそのアリティを、`pS` は符号化されたペイロードを、`rS` は内側のペイロードを表示します。これらの表示の等式を合成したものがキーの等式 `ek` です。

```agda
              arS = fstS qS ar F refl
              pS = sndS c' ar p ec
              rS = sndS pS (# (toℕ k)) r e'
              ek : fst c' ≡ pr (fst arS) (pr (# (toℕ k)) (fst rS))
              ek = ec ∙ cong (pr ar) e'
```

補題 `fill` は、復元されたタグを場合分けします。十種類の各タグについて、対応するペイロード条件を、形の論理式の該当する分岐の証人へ変換します。

```agda
          in fill k c' arS rS pay ek })
        key })
      (SR.shape-out hs c' c'∈)
      where
      env4 : (c' arS b a : S) → S ^ (6 + m)
```

補助環境は、二つのペイロード成分と後続アリティを記録します。これにより、二項結合子と量化された論理式の各分岐を解釈するための変数が揃います。

```agda
      env4 c' arS b a = b ∷ a ∷ arS ∷ c' ∷ δ' c
```

二項ペイロードが主張するのは、二つの成分が存在し、その順序対が表示されたペイロードに等しく、それぞれに対応するキーが領域に属することだけです。補助補題 `pairWit` は、これらのデータを形の論理式の対応する分岐が要求する証人へ変換します。

```agda
      pairWit : (k : ℕ) (rel : Formula S (4 + (2 + m))) (c' arS rS : S)
              → fst c' ≡ pr (fst arS) (pr (# k) (fst rS))
              → (t u : V ℓ) → fst rS ≡ pr t u
              → ((tS uS : S) → fst tS ≡ t → fst uS ≡ u → ⟨ env4 c' arS uS tS ⊨ rel ⟩)
              → BinWit k rel (δ' c) c'
```

順序対符号化の単射性によって、ペイロードの等式は二つの成分の等式に分かれます。これらをアリティの表示と複合キーの等式に合わせると、二つの所属証明が `BinWit` の要求する四つの欄に収まります。

```agda
      pairWit k rel c' arS rS ek t u er g =
        arS , (fstS rS t u er , (sndS rS t u er
        , ( ek ∙ cong (λ v → pr (fst arS) (pr (# k) v)) er
          , g (fstS rS t u er) (sndS rS t u er) refl refl )))
```

原子論理式では、ペイロードの二つの成分がともに、記録されたアリティで正しい項符号でなければなりません。各成分に `tmWit` を適用すると、この二つの意味的条件が `bothTm` の二つの連言肢へ変わります。

```agda
      both : (c' arS : S) (t u : V ℓ) → IsTmV Wv t (fst arS) → IsTmV Wv u (fst arS)
           → (tS uS : S) → fst tS ≡ t → fst uS ≡ u → ⟨ env4 c' arS uS tS ⊨ bothTm (sh 2 w) ⟩
      both c' arS t u ht hu tS uS qt qu =
          tmWit (suc zero) (suc (suc zero)) (sh 4 (sh 2 w)) (env4 c' arS uS tS)
            (subst (λ x → IsTmV Wv x (fst arS)) (sym qt) ht)
```

第二成分も同じように扱われ、復元された二つの項の証人が、原子ペイロードに必要な連言を証明します。

```agda
        , tmWit zero (suc (suc zero)) (sh 4 (sh 2 w)) (env4 c' arS uS tS)
            (subst (λ x → IsTmV Wv x (fst arS)) (sym qu) hu)
```

有界量化子で必要なのは、境界項が現在のアリティで正しいことだけです。そのため、対応する補助補題はペイロードの第一成分だけに `tmWit` を適用します。

```agda
      first : (c' arS : S) (t u : V ℓ) → IsTmV Wv t (fst arS)
            → (tS uS : S) → fst tS ≡ t → fst uS ≡ u → ⟨ env4 c' arS uS tS ⊨ fstTm (sh 2 w) ⟩
      first c' arS t u ht tS uS qt qu =
        tmWit (suc zero) (suc (suc zero)) (sh 4 (sh 2 w)) (env4 c' arS uS tS)
          (subst (λ x → IsTmV Wv x (fst arS)) (sym qt) ht)
```

タグ 0 は所属を表します。そのペイロードには二つの正しい項符号が含まれるので、二項の補助補題が、復元した項の証拠を用いて形の論理式の最も左の分岐を証明します。

```agda
      fill : (k : Fin 10) (c' arS rS : S) → PayN (toℕ k) (fst arS) (fst rS)
           → fst c' ≡ pr (fst arS) (pr (# (toℕ k)) (fst rS))
           → ∥ ShapeWit (sh 2 w) (δ' c) c' ∥₁
      fill zero c' arS rS pay ek = PT.map
        (λ { (t , u , (er , (ht , hu))) → inl (pairWit 0 (bothTm (sh 2 w)) c' arS rS ek t u er (both c' arS t u ht hu)) })
```

タグ 1 は等号を表し、次の分岐で同じ二項の議論によって扱われます。タグ 2 からは二項結合子が始まります。そこでも同じ順序対の分析を用いますが、復元される二つの成分は項符号ではなく、下位論理式のキーです。

```agda
        pay
      fill (suc zero) c' arS rS pay ek = PT.map
        (λ { (t , u , (er , (ht , hu))) → inr (inl (pairWit 1 (bothTm (sh 2 w)) c' arS rS ek t u er (both c' arS t u ht hu))) })
        pay
      fill (suc (suc zero)) c' arS rS pay ek = PT.map
```

三つの二項結合子の充足の場合は一様です。ペイロードは二つの下位コード `a` と `b` を名指し、証人はそのタグの位置での `pairWit` であり、境界の項はなくペイロードの条件も空です。二項の節には余分な要求がないからです。選言の入れ子の深さが、十通りの和の中でのタグの位置を示します。

```agda
        (λ { (a , b , (er , _)) → inr (inr (inl (pairWit 2 noneB c' arS rS ek a b er (λ _ _ _ _ b → b)))) })
        pay
      fill (suc (suc (suc zero))) c' arS rS pay ek = PT.map
        (λ { (a , b , (er , _)) → inr (inr (inr (inl (pairWit 3 noneB c' arS rS ek a b er (λ _ _ _ _ b → b))))) })
        pay
```

含意は第四の二項タグを占め、同じ構成に従います。偽はこれと異なり、ペイロードが数項の零です。そのため証人に必要なのはアリティとペイロードの等式だけであり、`numeralL-fst` が数項の基底集合について必要な等式を与えます。

```agda
      fill (suc (suc (suc (suc zero)))) c' arS rS pay ek = PT.map
        (λ { (a , b , (er , _)) → inr (inr (inr (inr (inl (pairWit 4 noneB c' arS rS ek a b er (λ _ _ _ _ b → b)))))) })
        pay
      fill (suc (suc (suc (suc (suc zero))))) c' arS rS pay ek =
        ∣ inr (inr (inr (inr (inr (inl (arS , (rS , (ek , pay ∙ sym (numeralL-fst 0))))))))) ∣₁
```

二つの非有界の量化子もやはり一様です。ペイロードは後続のアリティの下位の鍵であり、証人の条件はそのデータ上の恒等です。量化子の節が項の要求を加えることはないからです。存在と全称を区別するのはタグの位置だけです。

```agda
      fill (suc (suc (suc (suc (suc (suc zero)))))) c' arS rS pay ek =
        ∣ inr (inr (inr (inr (inr (inr (inl (arS , (rS , (ek , (λ b → b)))))))))) ∣₁
      fill (suc (suc (suc (suc (suc (suc (suc zero))))))) c' arS rS pay ek =
        ∣ inr (inr (inr (inr (inr (inr (inr (inl (arS , (rS , (ek , (λ b → b))))))))))) ∣₁
      fill (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) c' arS rS pay ek = PT.map
```

有界の全称は項の層を加えます。ペイロードには要素 `a` のほかに合法な境界の項 `t` が含まれ、証人はその項のために単項の読み `first` を使い、有界の鍵の形の項のスロットを `fstTm` が名指します。

```agda
        (λ { (t , a , (er , (ht , _))) → inr (inr (inr (inr (inr (inr (inr (inr (inl
          (pairWit 8 (fstTm (sh 2 w)) c' arS rS ek t a er (first c' arS t a ht)))))))))) })
        pay
      fill (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) c' arS rS pay ek = PT.map
        (λ { (t , a , (er , (ht , _))) → inr (inr (inr (inr (inr (inr (inr (inr (inr
```

有界存在は有界全称と同じペイロードの形をもちますが、最後のタグを占めます。これで十通りの場合が、四つの原子式、三つの二項結合子、偽、有界量化子と非有界量化子という論理式の構成子をちょうど覆います。

```agda
          (pairWit 9 (fstTm (sh 2 w)) c' arS rS ek t a er (first c' arS t a ht)))))))))) })
        pay
```

形の健全性の補題は、以上の構成を要素ごとにまとめます。符号集合の各要素 `c` に対して、`shaped-in` は先ほど構成した証人を `shapedAt` の充足証明へ変換します。符号を復号するときに必要なのは、まさにこの局所的な形の事実です。

```agda
    hsh : (c : S) → ⟨ δ' c ⊨ shapedAt zero (sh 2 w) ⟩
    hsh c = shaped-in zero (sh 2 w) (δ' c) (wit c)
```

閉包の節は、非原子の七つの構成子すべてに対して一度に証明されます。三つの二項結合子は `binAt` で処理されます。タグのペイロードを読み、対の符号化の単射性を通して二つの下位コードの所属を取り出すのです。

```agda
  closed : ⟨ γ ⊨ closedAt C ⟩
  closed =
      binSameClosed-in C 2 γ (binAt 2 refl)
    , ( binSameClosed-in C 3 γ (binAt 3 refl)
    , ( binSameClosed-in C 4 γ (binAt 4 refl)
```

二つの非有界の量化子は後続のアリティで読みを引用して処理され、二つの有界の量化子は `bqAt` が境界の項も読み取って処理します。七つの項目が合わさって、周囲の環境で `closedAt C` が認められます。

```agda
    , ( unSuccClosed-in C 6 γ (λ c' ar a c'∈ e → at c' c'∈ 6 (fst ar) (fst a) e)
    , ( unSuccClosed-in C 7 γ (λ c' ar a c'∈ e → at c' c'∈ 7 (fst ar) (fst a) e)
    , ( binSuccClosed-in C 8 γ (bqAt 8 refl)
    ,   binSuccClosed-in C 9 γ (bqAt 9 refl) )))))
```

復号定理は本章の最初の主要結果です。記述を満たす符号集合の各要素 `c` から、命題的切り詰めのもとで、自然数 `k`、アリティ `k` の論理式 `ψ`、および `fst c ≡ fst (keyS W ψ)` が得られます。したがって、この定理が主張するのは対応する論理式キーの存在であり、復号関数の選択や一意性ではありません。

```agda
  key-out : (c : S) → ⟨ fst c ∈ Cv ⟩
          → ∥ Σ[ k ∈ ℕ ] Σ[ ψ ∈ Formula ⟪ fst W ⟫ k ] (fst c ≡ fst (keyS W ψ)) ∥₁
  key-out c c∈ = PT.rec squash₁
    (λ { (ar , F , p , (q∈ , (ec , key))) → PT.rec squash₁
      (λ { (k , qk) → PT.map (λ { (ψ , e) → k , ψ , e })
```

まず `c` の切り詰められた形のデータから、アリティの項目、表、そして対応するキー条件を満たすペイロードを得ます。アリティについての仮定により、記録されたアリティはある数項 `# k` と同一視されます。これを先に得た下向き閉性と合わせると、`witnessAt-out` は、なお切り詰めのもとで、キーの基底集合が `fst c` であるアリティ `k` の論理式を復元します。

```agda
        (witnessAt-out W (suc w) zero (c ∷ γ) qw
          ∣ CS , (c∈ , (hcl c , hsh c)) ∣₁
          k (sndS c ar p ec) (ec ∙ cong (λ a → pr a p) qk)) })
      (arity (fstS (down (lookup E γ) (pr ar F) q∈) ar F refl)
             (sndS (down (lookup E γ) (pr ar F) q∈) ar F refl) q∈) })
```

必要な形のデータは、仮定した形の節と `c` の所属証明に `shape-out` を適用して得られるものにほかなりません。

```agda
    (SR.shape-out hs c c∈)
```

## 完全性：各論理式の符号化

ここで、有限の添字に関する二つの算術の事実が入ります。`n` 未満の自然数を `Fin n` の正しい添字へ変換することと、添字をみずからの数項を通して往復させることです。

```agda
open import L.Ordinal {ℓ} using ( ∈#-elim )
open import Cubical.Data.FinData.Properties using ( fromℕ'; toFromId' )
```

完全性を示すため、符号領域のスロット `C`、アルファベットのスロット `w`、アリティ塔のスロット `E` を固定し、十個のタグが正しく解釈されると仮定します。さらに、すべての正準な塔の要素が `E` に属し、上向きの閉包条項が成り立つと仮定します。目標は、アルファベット上のすべての論理式のキーが `C` に属することです。

```agda
module CodesComplete {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (arity∈ : (n : ℕ) → ⟨ pr (# n) (fst (envSet W n)) ∈ fst (lookup E γ) ⟩)
  (hc : ⟨ γ ⊨ closeAt C w E N ⟩) where
  open Alphabet W
```

符号領域のスロットが指す基底集合を `Cv` と書きます。完全性では、すべての真正な論理式キーがこの集合に属することを示します。

```agda
  private
    Cv = fst (lookup C γ)
```

アルファベットのすべての定数はアルファベットのスロットに属します。二つの台の同一視こそが、埋め込みの所属を環境の中へ輸送する根拠です。

```agda
    ι∈w : (q : Ab) → ⟨ ι q ∈ fst (lookup w γ) ⟩
    ι∈w q = subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈ q)
```

各アルファベット要素は、スロット `w` の内部要素によって表されます。`down` はその外部表現と上で得た所属証明を組にし、対応する要素 `ιS q : S` を作ります。

```agda
    ιS : Ab → S
    ιS q = down (lookup w γ) (ι q) (ι∈w q)
```

アリティ `n` の正準な塔の項目、すなわち数項 `n` と長さ `n` の環境の集合の対も同じように降ろされ、閉包の節をそこで引用できるようにします。

```agda
    qS : ℕ → S
    qS n = down (lookup E γ) (pr (# n) (fst (envSet W n))) (arity∈ n)
```

四スロットの文脈は、降ろされた塔の項目、数項、それらの対の容器、そして再び降ろされた項目を組み立て、閉包の節が期待する枠組みに一致させます。

```agda
    δ4 : ℕ → S ^ (4 + m)
    δ4 n = envSet W n ∷ nn n ∷ container (qS n) (nn n) (envSet W n) refl .fst ∷ qS n ∷ γ
```

完全な閉包の節はこの文脈で成り立ちます。仮定が、閉包の節がすべての正準な塔の項目で成り立つと言っているからです。

```agda
    frame : (n : ℕ) → ⟨ δ4 n ⊨ Close.all C w N ⟩
    frame n = useBoth i0 (qS n ∷ γ) (nn n) (envSet W n) refl (Close.all C w N) (hc (qS n) (arity∈ n))
```

閉包の読みは、それぞれの数項みずからの文脈で再び開かれ、すべてのアリティが十八の節のコピーを得ます。

```agda
    module CR (n : ℕ) = CloseRead C w N (δ4 n) tg
```

`n` 未満のすべての変数の添字は、`n` の数項より下の数項を名指します。フォン・ノイマンの数項の単調性によって、変数の添字がそのアリティの数項の要素として認められるのです。

```agda
    var∈ : (n : ℕ) (i : Fin n) → ⟨ # (toℕ i) ∈ # n ⟩
    var∈ n i = #mono (toℕ i) n (toℕ<n i)
```

構造帰納法は、所属原子式の四つの場合から始まります。各場合で、原子閉包条項を固定したアリティ `n` において具体化します。左右の項はそれぞれアルファベットの定数またはそのアリティの変数であり、直前の補題が対応する所属証明を与えます。

```agda
  key-in : ∀ {n} (ψ : Formula Ab n) → ⟨ fst (keyS W ψ) ∈ Cv ⟩
  key-in {n} (con x ∈̇ con y) = CR.atomClose-out n f0 f0 f0 (sh 4 w) (sh 5 w) (frame n .fst) (ιS x) (ιS y) (ι∈w x) (ι∈w y)
  key-in {n} (con x ∈̇ var j) = CR.atomClose-out n f0 f0 f1 (sh 4 w) i2 (frame n .snd .fst) (ιS x) (nn (toℕ j)) (ι∈w x) (var∈ n j)
  key-in {n} (var i ∈̇ con y) = CR.atomClose-out n f0 f1 f0 i1 (sh 5 w) (frame n .snd .snd .fst) (nn (toℕ i)) (ιS y) (var∈ n i) (ι∈w y)
  key-in {n} (var i ∈̇ var j) = CR.atomClose-out n f0 f1 f1 i1 i2 (frame n .snd .snd .snd .fst) (nn (toℕ i)) (nn (toℕ j)) (var∈ n i) (var∈ n j)
```

四つの等号原子式についても、等号のタグを用いて同じ議論を行います。連言では、まず帰納法の仮定によって二つの部分式のキーを `C` に入れ、次に二項閉包の節によって、それらを対にした連言のキーも `C` に入れます。

```agda
  key-in {n} (con x ≐ con y) = CR.atomClose-out n f1 f0 f0 (sh 4 w) (sh 5 w) (frame n .snd .snd .snd .snd .fst) (ιS x) (ιS y) (ι∈w x) (ι∈w y)
  key-in {n} (con x ≐ var j) = CR.atomClose-out n f1 f0 f1 (sh 4 w) i2 (frame n .snd .snd .snd .snd .snd .fst) (ιS x) (nn (toℕ j)) (ι∈w x) (var∈ n j)
  key-in {n} (var i ≐ con y) = CR.atomClose-out n f1 f1 f0 i1 (sh 5 w) (frame n .snd .snd .snd .snd .snd .snd .fst) (nn (toℕ i)) (ιS y) (var∈ n i) (ι∈w y)
  key-in {n} (var i ≐ var j) = CR.atomClose-out n f1 f1 f1 i1 i2 (frame n .snd .snd .snd .snd .snd .snd .snd .fst) (nn (toℕ i)) (nn (toℕ j)) (var∈ n i) (var∈ n j)
  key-in {n} (a ∧̇ b) = CR.binClose-out n f2 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (keyS W b) (codeS W a) (codeS W b) (key-in a) (key-in b) refl refl
```

選言と含意は、それぞれのタグで同じ二項の段階を用い、偽は零をペイロードとして定数閉包の節から `C` に入ります。二つの非有界量化子では、帰納法の仮定をアリティ `suc n` の本体に用い、量化子閉包の節によってその本体のキーからアリティ `n` のキーを作ります。

```agda
  key-in {n} (a ∨̇ b) = CR.binClose-out n f3 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (keyS W b) (codeS W a) (codeS W b) (key-in a) (key-in b) refl refl
  key-in {n} (a ⇒̇ b) = CR.binClose-out n f4 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (keyS W b) (codeS W a) (codeS W b) (key-in a) (key-in b) refl refl
  key-in {n} ⊥̇ = CR.conClose-out n f5 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst)
  key-in {n} (∃̇ a) = CR.quClose-out n f6 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl
  key-in {n} (∀̇ a) = CR.quClose-out n f7 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl
```

有界の全称には二つの閉包の引数があります。後続のアリティの下位の鍵と、現在のアリティの合法な境界の項です。境界が定数のとき項の項目はアルファベットの埋め込みから、変数のときは数項の所属から来ます。

```agda
  key-in {n} (∀̇∈ (con x) a) =
    CR.bqClose-out n f8 f0 (sh 8 w) (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (ιS x) (ι∈w x)
  key-in {n} (∀̇∈ (var i) a) =
    CR.bqClose-out n f8 f1 i5 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (nn (toℕ i)) (var∈ n i)
  key-in {n} (∃̇∈ (con x) a) =
```

有界の存在量化がみずからのタグで同じ二つの引数を繰り返し、構造的帰納を完成させます。すべてのアリティのすべての論理式の鍵が、閉じた定義域の中にあるのです。

```agda
    CR.bqClose-out n f9 f0 (sh 8 w) (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (ιS x) (ι∈w x)
  key-in {n} (∃̇∈ (var i) a) =
    CR.bqClose-out n f9 f1 i5 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd ) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (nn (toℕ i)) (var∈ n i)
```

## 正準な閉じた符号の定義域

最後に、正準な符号領域が実際にこの記述を満たすことを示します。符号スロットには `AllCodes W` を、アリティのスロットには `W` 上の環境塔を表させ、等式 `qC` と `qE` でそれぞれの同一視を記録します。

```agda
module CodesHolds {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qC : fst (lookup C γ) ≡ fst (AllCodes W))
  (qE : fst (lookup E γ) ≡ fst (Tower.tower W)) (tg : Tags γ N) where
  open Alphabet W
  private
```

符号領域、アルファベット、アリティ塔の各スロットが指す基底集合を、それぞれ `Cv`、`Wv`、`Ev` と書きます。三つの名前は役割の違いを明確にします。論理式キーの所属は `Cv` で、定数の表現は `Wv` で、正準なアリティ要素は `Ev` で調べます。

```agda
    Cv = fst (lookup C γ)
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)
    open CodesSem Wv Cv
```

集合 `Wv′` がすべてのアルファベット要素の表現を含むと仮定します。このとき、どの項も `Wv′` 上で正しい符号をもちます。定数ではその表現について与えられた所属証明を使い、変数では添字の数項がアリティの数項に属することを使います。ここでは項の適格性を符号の性質としてだけ用いるため、得られる証人は命題的に切り詰められています。

```agda
    tmV : ∀ {n} (Wv′ : V ℓ) → ((q : Ab) → ⟨ ι q ∈ Wv′ ⟩) → (t : Term Ab n) → IsTmV Wv′ (ct t) (# n)
    tmV Wv′ into (con q) = ∣ inl (ι q , (refl , into q)) ∣₁
    tmV {n} Wv′ into (var i) = ∣ inr (# (toℕ i) , (refl , #mono (toℕ i) n (toℕ<n i))) ∣₁
```

アルファベットの定数は、二つの台の同一視を通して、環境のアルファベットのスロットに属します。

```agda
    ι∈w : (q : Ab) → ⟨ ι q ∈ Wv ⟩
    ι∈w q = subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈ q)
```

`AllCodes W` の定義により、アルファベット上のすべての論理式キーはそこに属します。この所属証明を `qC` に沿って輸送すれば、同じキーが符号スロットの指す集合 `Cv` に属することが得られます。

```agda
    mem : ∀ {n} (ψ : Formula Ab n) → ⟨ fst (keyS W ψ) ∈ Cv ⟩
    mem ψ = subst (λ u → ⟨ fst (keyS W ψ) ∈ u ⟩) (sym qC) (key∈AllCodes W ψ)
```

同様に、環境塔には数項 `# n` と環境集合 `envSet W n` の対である正準な項目が含まれます。その所属証明を `qE` に沿って輸送すると、この項目がアリティ集合 `Ev` に属することが分かります。

```agda
    entry∈ : (n : ℕ) → ⟨ pr (# n) (fst (envSet W n)) ∈ Ev ⟩
    entry∈ n = subst (λ u → ⟨ pr (# n) (fst (envSet W n)) ∈ u ⟩) (sym qE) (Tower.tower-in′ W n)
```

項の読みは、証明されたばかりの一般的な項の合法性のアルファベットにおける実例です。

```agda
    tm : ∀ {n} (t : Term Ab n) → IsTmV Wv (ct t) (# n)
    tm = tmV Wv ι∈w
```

各論理式は、それ自身のアリティにおける正しいキーを定めます。証明は論理式の構造に沿って再帰します。原子式では二つの項の正しい符号を組み合わせ、連言と選言では、すでに得られた二つの部分式キーの所属証明を組み合わせます。

```agda
    keyOf : ∀ {n} (ψ : Formula Ab n) → Key (# n) (cd ψ)
    keyOf (t ∈̇ u) = ∣ f0 , pr (ct t) (ct u) , (refl , ∣ ct t , ct u , (refl , (tm t , tm u)) ∣₁) ∣₁
    keyOf (t ≐ u) = ∣ f1 , pr (ct t) (ct u) , (refl , ∣ ct t , ct u , (refl , (tm t , tm u)) ∣₁) ∣₁
    keyOf (a ∧̇ b) = ∣ f2 , pr (cd a) (cd b) , (refl , ∣ cd a , cd b , (refl , (mem a , mem b)) ∣₁) ∣₁
    keyOf (a ∨̇ b) = ∣ f3 , pr (cd a) (cd b) , (refl , ∣ cd a , cd b , (refl , (mem a , mem b)) ∣₁) ∣₁
```

含意は同じ対を繰り返し、偽は零のペイロードとその定義的な等式を運び、二つの非有界の量化子は項の要求なしに部分式の鍵を包みます。

```agda
    keyOf (a ⇒̇ b) = ∣ f4 , pr (cd a) (cd b) , (refl , ∣ cd a , cd b , (refl , (mem a , mem b)) ∣₁) ∣₁
    keyOf ⊥̇ = ∣ f5 , # 0 , (refl , refl) ∣₁
    keyOf (∃̇ a) = ∣ f6 , cd a , (refl , mem a) ∣₁
    keyOf (∀̇ a) = ∣ f7 , cd a , (refl , mem a) ∣₁
    keyOf (∀̇∈ t a) = ∣ f8 , pr (ct t) (cd a) , (refl , ∣ ct t , cd a , (refl , (tm t , mem a)) ∣₁) ∣₁
```

有界の量化子は境界の項と部分式の鍵を対にして再帰を完成させます。すべての論理式 `ψ` に対して、`keyOf ψ` は `ψ` みずからのアリティでの合法な鍵なのです。

```agda
    keyOf (∃̇∈ t a) = ∣ f9 , pr (ct t) (cd a) , (refl , ∣ ct t , cd a , (refl , (tm t , mem a)) ∣₁) ∣₁
```

正準な実例の形の節が従います。`AllCodes W` のすべての要素は論理式へ復号され、そのアリティと表の対は塔に属し、ペイロードは合法な鍵です。形の読みはこのデータを要素ごとに受け取ります。

```agda
    shape : ⟨ γ ⊨ shapeAt C w E N ⟩
    shape = ShapeRead.shape-in C w E N γ tg (λ c c∈ → PT.map
      (λ { (n , ψ , e) → # n , fst (envSet W n) , cd ψ , (entry∈ n , (e , keyOf ψ)) })
      (AllCodes-out W c (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈)))
```

復号の補助補題はアリティを明示的に固定します。符号領域の要素 `c` の基底集合が `pr (# n) z` なら、命題的切り詰めのもとで、`z ≡ cd ψ` を満たすアリティがちょうど `n` の論理式 `ψ` が存在します。つまり、外側の数項によってアリティが固定されてから、ペイロードが符号化する論理式が復元されます。

```agda
    decodeAt : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z
             → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
    decodeAt c c∈ n z e = PT.map
      (λ { (n₁ , ψ₁ , e₁) →
        let q = pr-inj (sym e₁ ∙ e)
```

証明は要素を外向きに読み、対と数項の単射性によって二つのアリティを整え、アリティの等式に沿って論理式を輸送します。ついで符号化の等式を逆向きに読んでペイロードを確定します。

```agda
            nq = #-inj′ (q .fst)
        in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) })
      (AllCodes-out W c (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
```

項の復号の主張は、界の集合によってパラメータ化されます。界のすべての要素は、切り詰めの範囲で、タグの数項とみずからを対にする符号をもつ項へ復号されます。

```agda
    TmDec : ∀ {n} → Fin 10 → V ℓ → Type (ℓ-suc ℓ)
    TmDec {n} Nx bound = (x : V ℓ) → ⟨ x ∈ bound ⟩ → ∥ Σ[ t ∈ Term Ab n ] (ct t ≡ pr (# (toℕ Nx)) x) ∥₁
```

定数はアルファベットの埋め込みのファイバーを通して復号されます。アルファベットのスロットの要素はあるアルファベットの項目の埋め込まれた像であり、その項目こそが求める定数です。

```agda
    conDec : ∀ {n} → TmDec {n} f0 Wv
    conDec x x∈ = ∣ con (fib .fst) , cong (pr (# 0)) (fib .snd) ∣₁
      where
      fib : Σ[ q ∈ Ab ] (ι q ≡ x)
      fib = ∈-asFiber {a = x} {b = fst W} (subst (λ u → ⟨ x ∈ u ⟩) qw x∈)
```

変数は数項の消去を通して復号されます。アリティの数項の要素は `n` 未満の自然数であり、正しい添字へ変換し直せ、符号化の等式はその往復に沿って輸送されます。

```agda
    varDec : (n : ℕ) (A : V ℓ) → A ≡ # n → TmDec {n} f1 A
    varDec n A qa x x∈ = PT.map
      (λ { (j , (p , ex)) → var (fromℕ' n j p) , cong (pr (# 1)) (cong #_ (toFromId' n j p) ∙ sym ex) })
      (∈#-elim n x (subst (λ u → ⟨ x ∈ u ⟩) qa x∈))
```

環境塔の一つの項目 `q` を固定し、そこに記録されたアリティが `# n` と等しいと仮定します。局所文脈 `δ4` は、閉包論理式が要求する四つの値、すなわちアリティ表、アリティの数項、その項目と表を結ぶ容器、そして項目自身を与えます。

```agda
    module At (q : S) (q∈ : ⟨ fst q ∈ Ev ⟩) (ar F s : S) (n : ℕ) (qa : fst ar ≡ # n) where
      private
        δ4 : S ^ (4 + m)
        δ4 = F ∷ ar ∷ s ∷ q ∷ γ
        A = fst ar
```

この固定した文脈のもとで、`CloseRead` は各閉包論理式の充足を対応する数学的な閉包性へ変換し、`Close` はその論理式自体を与えます。

```agda
        module CR = CloseRead C w N δ4 tg
        module Cl = Close C w N
```

補助補題 `in-key` は、等式に沿って正準なキーの所属証明を輸送します。`x` が論理式 `ψ` のキーの基底集合に等しければ、その正準なキーが `Cv` に属するという既知の事実から `x ∈ Cv` が得られます。

```agda
        in-key : ∀ {k} (ψ : Formula Ab k) (x : V ℓ) → x ≡ fst (keyS W ψ) → ⟨ x ∈ Cv ⟩
        in-key ψ x e = subst (λ u → ⟨ u ∈ Cv ⟩) (sym e) (mem ψ)
```

タグ `Nx` と要素 `x` に対し、`TmAt Nx x` は、項 `t` と、`t` の符号が `Nx` の数項と `x` の対であることを述べる等式からなる Σ 型です。先の復号の主張とは異なり、この局所的な型は命題的に切り詰められていません。

```agda
        TmAt : (Nx : Fin 10) (x : V ℓ) → Type (ℓ-suc ℓ)
        TmAt Nx x = Σ[ t ∈ Term Ab n ] (ct t ≡ pr (# (toℕ Nx)) x)
```

同様に、`FoAt k z` は、アリティ `k` の論理式 `ψ` と等式 `z ≡ cd ψ` からなる Σ 型です。論理式とその符号化の等式は、どちらも利用可能なデータとして保持されます。

```agda
        FoAt : (k : ℕ) (z : V ℓ) → Type (ℓ-suc ℓ)
        FoAt k z = Σ[ ψ ∈ Formula Ab k ] (z ≡ cd ψ)
```

原子の閉包の節は、二つの項の復号から証明されます。第一座標の要素の復号と第二座標の要素の復号が与えられれば、原子の鍵は対象言語の構成子によって二つの項から作られ、符号化の等式がそれを名指された鍵と同一視します。

```agda
        atomIn : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m))
               → (op : Term Ab n → Term Ab n → Formula Ab n)
               → ((t u : Term Ab n) → cd (op t u) ≡ pr (# (toℕ k)) (pr (ct t) (ct u)))
               → TmDec Nx (fst (lookup X δ4)) → ((x : S) → TmDec Ny (fst (lookup Y (x ∷ δ4))))
               → ⟨ δ4 ⊨ Cl.atomClose k Nx Ny X Y ⟩
```

二つの座標を別々に復号します。第一座標から項 `t` とその符号化の等式を得て、その座標を文脈に加えた後、第二座標から項 `u` とその符号化の等式を得ます。

```agda
        atomIn k Nx Ny X Y op code dx dy = CR.atomClose-in k Nx Ny X Y (λ x y x∈ y∈ →
          let d1 : ∥ TmAt Nx (fst x) ∥₁
              d1 = dx (fst x) x∈
              d2 : ∥ TmAt Ny (fst y) ∥₁
              d2 = dy x (fst y) y∈
```

集合 `G` は、アリティ、原子式のタグ、符号化された二つの座標から作る候補の原子式キーです。`Cv` への所属は命題なので、切り詰められた二つの項の復号を順にこの目標へ消去できます。それぞれの符号化の等式により `G` は論理式 `op t u` のキーと同一視され、その所属は `in-key` から得られます。

```agda
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y))))
          in PT.rec (snd (G ∈ Cv))
            (λ { (t , et) → PT.rec (snd (G ∈ Cv))
              (λ { (u , eu) → in-key (op t u) G
```

最後の等式は三段階で組み立てます。`qa` が外側のアリティを揃え、二つの項の符号化等式が対になったペイロードを揃え、`op` の定義等式が原子タグを揃えます。この等式に沿って正準なキーの所属証明を輸送すれば、原子閉包の証明が完了します。

```agda
                (cong₂ pr qa (cong (pr (# (toℕ k))) (cong₂ pr (sym et) (sym eu)) ∙ sym (code t u))) })
              d2 })
            d1)
```

二項結合子では、二つの直接の部分論理式は、複合論理式と同じアリティ `n` をもちます。仮定により二つの下位キーの第一成分は `# n` と書かれているので、この成分を記録されたアリティに揃えれば、`decodeAt` が各ペイロードをアリティ `n` の論理式の符号として復元します。

```agda
        binIn : (k : Fin 10) (op : Formula Ab n → Formula Ab n → Formula Ab n)
              → ((a b : Formula Ab n) → cd (op a b) ≡ pr (# (toℕ k)) (pr (cd a) (cd b)))
              → ⟨ δ4 ⊨ Cl.binClose k ⟩
        binIn k op code = CR.binClose-in k (λ c₁ c₂ a b c₁∈ c₂∈ e₁ e₂ →
          let d1 : ∥ FoAt n (fst a) ∥₁
```

`decodeAt` を二度適用すると、符号が二つのペイロード成分に等しい論理式 `ψ₁` と `ψ₂` が、それぞれ単に得られます。集合 `G` は、記録されたアリティ、選んだ結合子タグ、この二成分からすでに組み立てられた複合キーです。

```agda
              d1 = decodeAt c₁ c₁∈ n (fst a) (e₁ ∙ cong (λ v → pr v (fst a)) qa)
              d2 : ∥ FoAt n (fst b) ∥₁
              d2 = decodeAt c₂ c₂∈ n (fst b) (e₂ ∙ cong (λ v → pr v (fst b)) qa)
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (pr (fst a) (fst b)))
```

切り詰められた二つの証人を順に除去すると、実際の論理式 `ψ₁` と `ψ₂` を扱えばよくなります。それぞれの符号の等式により `G` は `op ψ₁ ψ₂` のキーと同一視されるので、正準な所属証明 `in-key` から必要な二項閉包条項が得られます。

```agda
          in PT.rec (snd (G ∈ Cv))
            (λ { (ψ₁ , ea) → PT.rec (snd (G ∈ Cv))
              (λ { (ψ₂ , eb) → in-key (op ψ₁ ψ₂) G
                (cong₂ pr qa (cong (pr (# (toℕ k))) (cong₂ pr ea eb) ∙ sym (code ψ₁ ψ₂))) })
              d2 })
```

外側の除去が最初に復元した論理式を与え、符号領域が選んだ二項結合子について閉じていることの証明が完了します。

```agda
            d1)
```

偽には部分論理式がなく、そのペイロードは数項零だけです。記録されたアリティと選んだタグを `c₀` の正準な符号に揃えれば、`in-key` により得られたキーが符号領域に属することが示されます。

```agda
        conIn : (k : Fin 10) (c₀ : Formula Ab n) → cd c₀ ≡ pr (# (toℕ k)) (# 0) → ⟨ δ4 ⊨ Cl.conClose k ⟩
        conIn k c₀ code = CR.conClose-in k (in-key c₀ (pr A (pr (# (toℕ k)) (# 0))) (cong₂ pr qa (sym code)))
```

変数を一つ束縛すると、本体のアリティは `n` から `suc n` に変わります。したがって量化子の閉包に関する仮定は、直接の下位キーを後続アリティに置き、`decodeAt` はちょうどそのアリティをもつ論理式の本体を復元します。

```agda
        quIn : (k : Fin 10) (op : Formula Ab (suc n) → Formula Ab n)
             → ((a : Formula Ab (suc n)) → cd (op a) ≡ pr (# (toℕ k)) (cd a))
             → ⟨ δ4 ⊨ Cl.quClose k ⟩
        quIn k op code = CR.quClose-in k (λ c₁ ar' a c₁∈ e₁ es →
          let d1 : ∥ FoAt (suc n) (fst a) ∥₁
```

外側のアリティ、量化子タグ、本体の符号から組み立てたキーを `G` とします。切り詰められた本体を `ψ₁` として復元すると、その符号の等式により `G` は `op ψ₁` のキーと同一視され、正準な所属証明から量化子の閉包条項が従います。

```agda
              d1 = decodeAt c₁ c₁∈ (suc n) (fst a) (e₁ ∙ cong (λ v → pr v (fst a)) (es ∙ cong sucV qa))
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (fst a))
          in PT.rec (snd (G ∈ Cv))
            (λ { (ψ₁ , ea) → in-key (op ψ₁) G (cong₂ pr qa (cong (pr (# (toℕ k))) ea ∙ sym (code ψ₁))) })
```

復元した本体を除去することで、符号領域が選んだ非有界量化子について閉じていることの証明が完了します。

```agda
            d1)
```

有界量化子は、アリティ `suc n` の本体と、アリティ `n` の境界項をともに含みます。そのため `bqIn` は、本体キーにすでに使える復号に加えて、境界を収める環境成分についての項の復号仮定を受け取ります。

```agda
        bqIn : (k Nx : Fin 10) (X : Fin (8 + m))
             → (op : Term Ab n → Formula Ab (suc n) → Formula Ab n)
             → ((t : Term Ab n) (a : Formula Ab (suc n)) → cd (op t a) ≡ pr (# (toℕ k)) (pr (ct t) (cd a)))
             → ((ar' a s' c₁ : S) → TmDec Nx (fst (lookup X (a ∷ ar' ∷ s' ∷ c₁ ∷ δ4))))
             → ⟨ δ4 ⊨ Cl.bqClose k Nx X ⟩
```

項の復号仮定は境界の所属証明から境界項を復元し、`decodeAt` は後続アリティの下位キーから本体を復元します。どちらの結果も命題的に切り詰められています。閉包の目標が要求するのは完成したキーの所属であって、復号結果を大域的に選ぶことではないからです。

```agda
        bqIn k Nx X op code dx = CR.bqClose-in k Nx X (λ c₁ ar' a s' c₁∈ e₁ es x x∈ →
          let d1 : ∥ TmAt Nx (fst x) ∥₁
              d1 = dx ar' a s' c₁ (fst x) x∈
              d2 : ∥ FoAt (suc n) (fst a) ∥₁
              d2 = decodeAt c₁ c₁∈ (suc n) (fst a) (e₁ ∙ cong (λ v → pr v (fst a)) (es ∙ cong sucV qa))
```

ここでキー `G` のペイロードは入れ子になっており、まず境界項の符号、次に本体の符号が置かれています。一つ目の切り詰めの除去で実際の項 `t` を取り出し、二つ目で本体の符号に対応する論理式を取り出します。

```agda
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a)))
          in PT.rec (snd (G ∈ Cv))
            (λ { (t , et) → PT.rec (snd (G ∈ Cv))
              (λ { (ψ₁ , ea) → in-key (op t ψ₁) G
```

復元した項 `t` と本体 `ψ₁` が得られると、それぞれの符号の等式により `G` は `op t ψ₁` のキーと同一視されます。正準な所属証明から有界量化子の条項が得られ、二つの切り詰めの除去は、証人を導入した順序とは逆に閉じられます。

```agda
                (cong₂ pr qa (cong (pr (# (toℕ k))) (cong₂ pr (sym et) ea) ∙ sym (code t ψ₁))) })
              d2 })
            d1)
```

一つの論理式 `Cl.all` は十八の閉包条項をまとめています。最初の八条項は二つの原子関係を扱います。各関係について、左右の項はそれぞれ独立に定数または変数です。定数は `w` への所属から復号され、変数は添字がアリティの数項に属することから復号されます。

```agda
      all : ⟨ δ4 ⊨ Cl.all ⟩
      all =
          atomIn f0 f0 f0 (sh 4 w) (sh 5 w) _∈̇_ (λ _ _ → refl) conDec (λ _ → conDec)
        , ( atomIn f0 f0 f1 (sh 4 w) i2 _∈̇_ (λ _ _ → refl) conDec (λ _ → varDec n A qa)
        , ( atomIn f0 f1 f0 i1 (sh 5 w) _∈̇_ (λ _ _ → refl) (varDec n A qa) (λ _ → conDec)
```

四つの条項が所属原子における定数と変数の全組合せを覆い、これと並行する四つの条項が等号原子を覆います。これで八つの原子閉包条項が揃い、残る十条項が論理結合子と量化子を扱います。

```agda
        , ( atomIn f0 f1 f1 i1 i2 _∈̇_ (λ _ _ → refl) (varDec n A qa) (λ _ → varDec n A qa)
        , ( atomIn f1 f0 f0 (sh 4 w) (sh 5 w) _≐_ (λ _ _ → refl) conDec (λ _ → conDec)
        , ( atomIn f1 f0 f1 (sh 4 w) i2 _≐_ (λ _ _ → refl) conDec (λ _ → varDec n A qa)
        , ( atomIn f1 f1 f0 i1 (sh 5 w) _≐_ (λ _ _ → refl) (varDec n A qa) (λ _ → conDec)
        , ( atomIn f1 f1 f1 i1 i2 _≐_ (λ _ _ → refl) (varDec n A qa) (λ _ → varDec n A qa)
```

続く六つの条項は、連言、選言、含意、偽、二つの非有界量化子を扱います。各構成子には正準なタグと定義的な符号化の等式が添えられているので、対応する補助補題が構成されたキーを直接挿入できます。

```agda
        , ( binIn f2 _∧̇_ (λ _ _ → refl)
        , ( binIn f3 _∨̇_ (λ _ _ → refl)
        , ( binIn f4 _⇒̇_ (λ _ _ → refl)
        , ( conIn f5 ⊥̇ refl
        , ( quIn f6 ∃̇_ (λ _ → refl)
```

最後の四つの条項は、有界全称量化と有界存在量化を扱います。それぞれについて、境界が定数の場合と変数の場合が一つずつあり、`conDec` と `varDec` が、それらが外側のアリティで正しい項であることを示します。これで入れ子の組は `Cl.all` の全成分を与えます。

```agda
        , ( quIn f7 ∀̇_ (λ _ → refl)
        , ( bqIn f8 f0 (sh 8 w) ∀̇∈ (λ _ _ → refl) (λ _ _ _ _ → conDec)
        , ( bqIn f8 f1 i5 ∀̇∈ (λ _ _ → refl) (λ _ _ _ _ → varDec n A qa)
        , ( bqIn f9 f0 (sh 8 w) ∃̇∈ (λ _ _ → refl) (λ _ _ _ _ → conDec)
        ,   bqIn f9 f1 i5 ∃̇∈ (λ _ _ → refl) (λ _ _ _ _ → varDec n A qa) ))))))))))))))))
```

あとは、環境塔の各要素 `q` で閉包条項を示します。環境塔の定理により、命題的切り詰めのもとで、`q` はある `n` に対応する正準な要素 `(# n, envSet W n)` として表されます。その第一成分の等式が記録されたアリティを `# n` に揃えるので、`At.all` にまとめた十八の条項をその要素に適用できます。

```agda
    close : ⟨ γ ⊨ closeAt C w E N ⟩
    close q q∈ = bothAll-in i0 (Close.all C w N) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ e →
      PT.rec (snd ((F ∷ ar ∷ s ∷ q ∷ γ) ⊨ Close.all C w N))
        (λ { (n , qp) → At.all q q∈ ar F s n (pr-inj (sym e ∙ qp) .fst) })
        (Tower.tower-out W q (subst (λ u → ⟨ fst q ∈ u ⟩) qE q∈)))
```

これで正準な符号領域 `AllCodes W` は `codesAt` の両部分を満たします。`shape` は、各要素が記録されたアリティと十種類の正しいペイロード形のいずれかをもつことを示し、`close` は、正しい直接の構成要素から組み立てたすべてのキーが領域に属することを示します。ここで確立されたのは符号領域そのものの妥当性です。その構文的記述は、真正な論理式キーをちょうどすべて収めています。

```agda
  holds : ⟨ γ ⊨ codesAt C w E N ⟩
  holds = shape , close
```

## まとめ

二つの方向は正準な符号領域の上で一致します。健全性は `AllCodes W` の各要素を記録されたアリティにおける論理式キーへ復号し、完全性はすべての真正な論理式キーをその領域へ戻します。`CodesHolds` は、内部の形と閉性の記述がこの二つの結論を支えることを示します。