---
title: "構成可能階層の Δ₀ 記述"
module: L.GCH.HierarchyDescription
lang: ja
site: "Bedrock"
description: "構成可能階層の Δ₀ 記述"
stage: "GCH の証明"
reading_order: 106
canonical: https://bedrock.institute/ja/L.GCH.HierarchyDescription.html
html: L.GCH.HierarchyDescription.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/HierarchyDescription.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantOccurrences, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Numerals, L.Coding.Expressions, L.Coding.NumeralBound, L.Coding.CodeSet, L.Coding.Model, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.EnvironmentTower, L.Hierarchy, L.GCH.SkolemHull, L.Coding.SatisfactionGraphSet, L.GCH.SatisfactionDescription, L.GCH.DefinablePowerSetDescription, L.GCH.AdequateStages]
routes: [gch-descriptions, hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.HierarchyDescription.md, https://bedrock.institute/zh/L.GCH.HierarchyDescription.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
後の凝縮の議論では、ある集合が与えられた順序数における構成可能段階である、という主張を移す必要があります。初等性が移すのは論理式であって、外部で定義された演算 `Lset` ではありません。そこで本章は、同じ段階関係を認識する有界な対象言語の論理式を作り、第三の集合をすべての補助的な証人に共通する上界として用います。

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

この構成で用いる古典性は、固定された一つの排中律の実例だけに由来します。それでも有界存在の論理式は命題的に切り詰められた存在として読まれるため、古典的な背景から、隠れた表を大域的に選んだデータが得られるわけではありません。

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

宇宙レベル `ℓ` と、レベル `ℓ-suc ℓ` の命題に対する排中律を固定します。本章の論理式、読み補題、そして最終的な正しさの定理は、すべてこの一つの明示的な古典的仮定に相対して述べられます。

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

ここで対象言語に必要なのは、所属、連言、真、偽、有界量化子だけです。これらの構成子には構造に沿った Δ₀ の証人があります。後で定数が現れないことを示せば、定数域を空のアルファベットへ変えられます。こうして自由変数を残したまま、最終的な三変数の論理式をパラメータなしにします。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀; δ-∧; δ-∃∈ )
open import FOL.Manipulation.ConstantOccurrences using ( countFo )
open import FOL.Manipulation.ConstantMapping using ( embed )
```

同じ有界論理式は、構成可能な台の内部でも、周囲の累積階層でも読めます。Δ₀ 絶対性がこの二つの読みを同定します。所属帰納法は、より下の行から現在の表の行を検証し、外延性は、そこから得られる二つの所属の含意を段階の等しさへ変えます。

```agda
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀ )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr )
```

段階 `Lset b` は、それ以前の段階の定義可能冪集合から組み立てられます。その各要素は、ある `c ∈ b` に対する `𝒟ₒ (Lset c)` から来ており、そのような寄与はすべて `Lset b` に属します。所属についての内向きと外向きの規則がこの二方向を表し、順序数の事実が、後で使う添字が実際に段階の添字であることを保証します。

```agda
open import L.Constructible {ℓ} using
  ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )
```

一つの定義可能冪集合を内部で認識するには、論理式の符号、充足関係表、環境の塔が必要です。順序対の符号化は、各段階の添字をその記録された値と結びつけます。これらの補助集合はすべて同じ証人集合 `z` で有界化されるため、記述全体が Δ₀ にとどまります。

```agda
open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.NumeralBound {ℓ} lem using ( module Bound )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )
open import L.Coding.Model {ℓ} using ( container )
open import L.Coding.Quantification {ℓ} using
```

対象言語の内部では、集合として符号化された順序対の成分を非有界な演算で射影することはできません。代わりに、有界な成分論理式が小さな容器の中を動き、そこで対を読んだり埋めたりします。十個の名前付きスロットには符号化の記述で使う数項タグが入り、新しい証人で環境を拡張するときには、その名前をずらして位置を保ちます。

```agda
  ( sh; i0; i1; i2; i3; i8; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; down; suc-out; suc-in; sndEx; sndAll; bothAll
  ; sndEx-out; sndAll-in; bothAll-in; fillSnd; useSnd; useBoth; sndS )
open import L.Coding.CodeDomain {ℓ} using ( Tags; shN )
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; module Tower )
```

ここでは三つの意味論的な仕様が合流します。階層表は上界より下の対 `(c,Lset c)` を記録し、充足の記述は一つの段階上の真正な符号、環境、充足関係のデータを認識し、定義可能冪集合の記述は集合 `𝒟ₒ (Lset c)` を認識します。健全性が復元する表の性質は `Values` と `Entries` だけであり、完全性は正確な仕様 `IsHier` から始まります。

```agda
open import L.Hierarchy {ℓ} lem using ( hierL-spec; IsHier; hier-out; hier-in; Values; Entries )
open import L.GCH.SkolemHull {ℓ} lem using ( module Cnt; erase-Δ₀; isOrd-at-p; Δ₀-isOrd-at-p; _⊨ₚ_ )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; sat-complete )
open import L.GCH.DefinablePowerSetDescription {ℓ} lem using ( defAt; def-sound; def-complete )
```

完全性には、すべての補助的な証人を含む一つの共通段階が必要です。`γ` が十分で `c ∈ γ` なら、`Lset γ` は `c` で必要な階層表、符号集合、充足関係表、環境の塔を含みます。後続に関する閉性は次の段階もそこへ入れ、`ω ∈ γ` は十個の有限な数項タグをすべて与えます。

```agda
open import L.GCH.AdequateStages {ℓ} lem using ( Adequate; module Adequate; module At; Lset∈suc )
```

環境は構成可能集合からなる有限ベクトルです。有界な証人を導入すると、それは先頭に置かれ、以前の各スロットは一つずつ後ろへずれます。有限添字がこのずれを明示します。この管理によって、同じ段階、表、上界の名前を、入れ子になった複数の量化子の中でも保つことができます。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( _∷_; []; map; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.FinData using ( toℕ; weakenFin )
```

存在論理式の充足が保つのは命題的切り詰めだけです。適切なデータが存在することを記録し、どのデータを使ったかは忘れます。したがって、後で切り詰めを除去するときの行き先は常に命題です。ここでは所属が命題値であり、累積階層の集合の等しさも命題なので、証明で必要な二種類の結論はいずれも正当な行き先になります。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

十個の有限なタグは、階層内部の von Neumann 数項で表されます。零は空集合であり、後の各タグは集合論的な後続によって得られ、十個すべてが `ω` に属します。所属の読みは、これらの周囲の集合を、構成可能な台の要素としての表示と結びつけます。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV; ω )
```

構成可能モデルの台を `S` と書きます。その要素は、周囲の集合とその構成可能性の証明を組にして提示します。隠れた表と証人はすべてこの台の上で量化され、最後に見えるスロットも、値 `a`、その段階の添字 `p`、共通の上界 `z` をそれぞれ提示します。

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

`L` の内部での充足と周囲の階層での充足は異なる構造を使いますが、パラメータが `L` から来る Δ₀ 論理式については一致します。補題 `abs₀` が両者の橋です。この橋により、完全性は内部で論理式の充足を組み立て、健全性は移された論理式を周囲での段階の等しさとして読み戻せます。

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

論理式 `defIn w z N body` は、四重の有界存在量化子を使って、充足関係表 `T`、符号集合 `C`、環境の塔 `E`、値 `d` を `z` の中に置きます。充足の記述は `w` の値上の `T`、`C`、`E` を検証し、定義可能冪集合の記述は `d` をその値の定義可能冪集合と同定し、`body` はその `d` に対する追加の条件を述べます。充足が保つのはこれらの証人の命題的切り詰めだけであり、この論理式は `z` を一意には特徴づけません。

```agda
defIn : ∀ {k} → Fin k → Fin k → (Fin 10 → Fin k) → Formula S (4 + k) → Formula S k
defIn w z N body =
  ∃̇∈ (var z) (∃̇∈ (var (sh 1 z)) (∃̇∈ (var (sh 2 z)) (∃̇∈ (var (sh 3 z))
    (satAt i3 (sh 4 w) i2 i1 (shN 4 N) ∧̇ (defAt i0 (sh 4 w) i3 i2 (shN 4 N) ∧̇ body)))))
```

内向きの包含を表す `intoAt` は、各 `x ∈ v` が、それ以前の段階の添字 `c ∈ b` によって説明されることを述べます。すなわち、`f` の順序対の形をしたある要素が `c` で値 `w` を記録し、`x` は `w` の定義可能冪集合に属します。外側の有界な形は `∀[ x ∈ v ] ∃[ c ∈ b ] ...` であり、残りの有界な証人が、その行と冪集合を認識するためのデータを展開します。

```agda
intoAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
intoAt v b f z N =
  ∀̇∈ (var v) (∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f))
    (sndEx i0 i1 (defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)))))
```

逆向きの包含を表す `overAt` は、`c ∈ b` と、対 `(c,w)` として提示される `f` の要素を動きます。そのような提示ごとに、`w` の定義可能冪集合のすべての要素が `v` に属することを要求します。この節は、そのような対として提示されない `f` の要素については何も述べないため、候補表全体から任意の余分な要素を排除するものとは読めません。

```agda
overAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
overAt v b f z N =
  ∀̇∈ (var b) (∀̇∈ (var (sh 1 f))
    (sndAll i0 i1 (defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))))))
```

連言 `stepAt` は二つの包含をまとめます。`b` より下に記録された対の行に相対して、`intoAt` は `v` に余分な要素がないことを述べ、`overAt` は定義可能冪集合からの寄与が一つも欠けないことを述べます。表の値が正しいことは、後の読み補題が別に要求する仮定です。

```agda
stepAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
stepAt v b f z N = intoAt v b f z N ∧̇ overAt v b f z N
```

`approxAt` の前半は被覆を与えます。すべての `c ∈ b` について、`f` に順序対の形をした何らかの項目があります。後半は、`f` の要素が対 `(c,w)` として提示されたときに `stepAt w c f z N` を検査します。`f` の各要素が対であることも、記録された各第一成分が `b` より下にあることも述べません。したがって `approx-out` が復元するのは正確に `Values f b × Entries f b` であり、表全体と階層グラフとの等しさでも、大域的に余分な要素がないという性質でもありません。

```agda
approxAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
approxAt f b z N =
    ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇))
  ∧̇ ∀̇∈ (var f) (bothAll i0 (stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N)))
```

節 `hierAt a p f z N` は、`p` より下の近似と、`p` における最後の一段階を結びつけます。近似から `Values` と `Entries` が得られれば、最後の一段階は `a` を `Lset p` と同定します。逆に、正確な階層表 `IsHier p f` と十分な証人の供給があれば、二つの連言を埋められます。これは、最終的な三変数の論理式が有界な証人の背後に隠す、局所的な段階関係です。

```agda
hierAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
hierAt a p f z N = approxAt f p z N ∧̇ stepAt a p f z N
```

タグの節は、十の枠を数項に固定します。最初の枠には要素がないので、それは空集合です。

```agda
pins : ∀ {m} → (Fin 10 → Fin m) → Formula S m
pins N =
    ∀̇∈ (var (N f0)) ⊥̇
  ∧̇ ( sucAtL (N f0) (N f1) ∧̇ ( sucAtL (N f1) (N f2) ∧̇ ( sucAtL (N f2) (N f3)
  ∧̇ ( sucAtL (N f3) (N f4) ∧̇ ( sucAtL (N f4) (N f5) ∧̇ ( sucAtL (N f5) (N f6)
```

残りの九つの枠は九つの後続の主張でつながれ、こうして十の枠は、数項の 0 から 9 にちょうどなります。

```agda
  ∧̇ ( sucAtL (N f6) (N f7) ∧̇ ( sucAtL (N f7) (N f8) ∧̇ sucAtL (N f8) (N f9) ))))))))
```

## 階層表を表す有界な節

後の記述で十個のタグを使うには、対象言語での固定条件が意味論的な記録 `Tags γ N` と一致しなければなりません。次の二つの補題が両方向を示します。一方は `pins` から数項の等式を読み、もう一方はその等式から `pins` を再構成します。

```agda
module PinsRead {m : ℕ} (N : Fin 10 → Fin m) (γ : S ^ m) where
```

タグの節の読みは、まず最初の枠が空であることを示します。要素をもたないのです。

```agda
  pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N
  pins-out (h0 , hs) = go
    where
    q0 : fst (lookup (N f0) γ) ≡ # 0
    q0 = extensionalV (λ y → ⇔toPath
```

空であることは、両方向の外延性の議論です。最初の枠のどんな要素も偽の節と矛盾し、そもそも空集合には要素がありません。

```agda
      (λ y∈ → Empty.rec* (h0 (down (lookup (N f0) γ) y y∈) y∈))
      (λ y∈ → Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))))
```

補助補題 `up` は数項の鎖を一つ進めます。スロット `i` が `# k` を表し、`sucAtL i j` が成り立つなら、その健全な読みはスロット `j` を `sucV (# k)`、したがって数項 `# (suc k)` と同定します。

```agda
    up : (i j : Fin m) (k : ℕ) → ⟨ γ ⊨ sucAtL i j ⟩ → fst (lookup i γ) ≡ # k
       → fst (lookup j γ) ≡ # (suc k)
    up i j k h q = suc-out i j γ h ∙ cong sucV q
```

零についての等式から始め、最初の五つの後続の節によって `q1` から `q5` が順に得られます。したがって `f1` から `f5` が名付けるスロットは、それぞれ数項一から五と同定されます。

```agda
    q1 = up (N f0) (N f1) 0 (hs .fst) q0
    q2 = up (N f1) (N f2) 1 (hs .snd .fst) q1
    q3 = up (N f2) (N f3) 2 (hs .snd .snd .fst) q2
    q4 = up (N f3) (N f4) 3 (hs .snd .snd .snd .fst) q3
    q5 = up (N f4) (N f5) 4 (hs .snd .snd .snd .snd .fst) q4
```

残り四つの後続の節が同じ鎖を続け、`q6` から `q9` を与えます。これにより、スロット `f6` から `f9` は数項六から九と同定され、数項についての読みが完成します。

```agda
    q6 = up (N f5) (N f6) 5 (hs .snd .snd .snd .snd .snd .fst) q5
    q7 = up (N f6) (N f7) 6 (hs .snd .snd .snd .snd .snd .snd .fst) q6
    q8 = up (N f7) (N f8) 7 (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7
    q9 = up (N f8) (N f9) 8 (hs .snd .snd .snd .snd .snd .snd .snd .snd) q8
```

記録 `Tags γ N` は、`Fin 10` の各要素について対応する数項の等式を要求します。最初の四つの場合は `q0`、`q1`、`q2`、`q3` を返し、零から三までのタグに対応します。

```agda
    go : Tags γ N
    go zero = q0
    go (suc zero) = q1
    go (suc (suc zero)) = q2
    go (suc (suc (suc zero))) = q3
```

`go` の次の五つの場合は `q4` から `q8` を返します。入れ子の後続として書かれたこれらのパターンは、追加の算術的な議論なしに、タグ四から八を尽くします。

```agda
    go (suc (suc (suc (suc zero)))) = q4
    go (suc (suc (suc (suc (suc zero))))) = q5
    go (suc (suc (suc (suc (suc (suc zero)))))) = q6
    go (suc (suc (suc (suc (suc (suc (suc zero))))))) = q7
    go (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = q8
```

`Fin 10` に残る唯一の場合は、零の九回目の後続であり、`q9` を返します。これで場合分けは、`Tags γ N` が要求する十個すべての数項の等式を与えます。

```agda
    go (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = q9
```

逆向きには、スロットがすでに `Tags γ N` を満たすとします。零のスロットの要素と仮定されたものは、タグの等式に沿って空集合の要素へ移されるため、存在できません。同じタグの等式が、九つの後続の節を埋めるためのデータも与えます。

```agda
  pins-in : Tags γ N → ⟨ γ ⊨ pins N ⟩
  pins-in tg =
      (λ x x∈ → Empty.rec (∅-empty (fst x) (∈∈ₛ {a = fst x} {b = ∅} .fst
                  (subst (λ u → ⟨ fst x ∈ u ⟩) (tg f0) x∈))))
    , ( st f0 f1 refl , ( st f1 f2 refl , ( st f2 f3 refl , ( st f3 f4 refl , ( st f4 f5 refl , ( st f5 f6 refl
```

各後続の節は、二つのタグのスロットを対応する数項の等式に沿って書き換えた後、後続論理式の内向きの読みを適用して再構成します。

```agda
    , ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl ))))))))
    where
    st : (j k : Fin 10) → # (toℕ k) ≡ sucV (# (toℕ j)) → ⟨ γ ⊨ sucAtL (N j) (N k) ⟩
    st j k e = suc-in (N j) (N k) γ (tg k ∙ e ∙ cong sucV (sym (tg j)))
```

十個の名前付きスロットが必要な数項の値をもつ環境 `δ` を固定します。`w` にある底集合を `Wv`、`z` にある底集合を `Zv` とします。前者は定義可能性を解釈する段階であり、後者は四つの証人を含まなければならない共通の上界です。

```agda
module DefInRead {k : ℕ} (w z : Fin k) (N : Fin 10 → Fin k) (body : Formula S (4 + k))
  (δ : S ^ k) (tg : Tags δ N) where
  private
    Wv = fst (lookup w δ)
    Zv = fst (lookup z δ)
```

四つの証人は `T`、`C`、`E`、`d` の順に束縛されます。新しい束縛子は環境の先頭を拡張するため、本体は `d ∷ E ∷ C ∷ T ∷ δ` で評価されます。したがって先頭の四つのスロットは、定義可能冪集合の値、環境の塔、符号集合、充足関係表をこの順に指します。

```agda
  δ4 : (T C E d : S) → S ^ (4 + k)
  δ4 T C E d = d ∷ E ∷ C ∷ T ∷ δ
```

`defIn` を読むとき、四つの証人 `T`、`C`、`E`、`d` を囲む命題的切り詰めは保たれます。その結論が意図的に残すのは、`d ∈ z`、`d = 𝒟ₒ Wv`、そして拡張された環境で本体が成り立つことだけです。`T`、`C`、`E` が `z` に属する証明と、内部の充足および冪集合の記述の証明は、この弱い主張を導く途中で消費されます。

```agda
  defIn-out : ⟨ δ ⊨ defIn w z N body ⟩
            → ∥ Σ[ T ∈ S ] Σ[ C ∈ S ] Σ[ E ∈ S ] Σ[ d ∈ S ]
                (⟨ fst d ∈ Zv ⟩ × ((fst d ≡ 𝒟ₒ Wv) × ⟨ δ4 T C E d ⊨ body ⟩)) ∥₁
  defIn-out = PT.rec squash₁ (λ { (T , (T∈ , h1)) → PT.rec squash₁ (λ { (C , (C∈ , h2)) →
    PT.rec squash₁ (λ { (E , (E∈ , h3)) → PT.map (λ { (d , (d∈ , (hs , (hd , hb)))) →
```

四重の切り詰めから証人を取り出した後、`def-sound` は充足の記述 `hs` と定義可能冪集合の記述 `hd` を組み合わせます。ここに残される唯一の等式は、その結論 `d = 𝒟ₒ Wv` であり、本体の証明はそのまま先へ渡されます。

```agda
      T , C , E , d , ( d∈ , ( def-sound i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) (lookup w δ) refl tg hs hd
                             , hb )) })
      h3 }) h2 }) h1 })
```

逆に、意味論的なデータから `defIn` を示すには、真正な証人を明示的に与える必要があります。`w` で表される構成可能な台 `W`、四つの集合とそれらが `z` に属する証明、真正な充足関係表、符号集合、環境の塔、定義可能冪集合とのそれぞれの同定、そして本体の証明を与えます。したがってこの向きでは、外向きの読みが意図的に忘れるデータを仮定します。

```agda
  defIn-in : (W : S) → Wv ≡ fst W → (T C E d : S)
           → ⟨ fst T ∈ Zv ⟩ → ⟨ fst C ∈ Zv ⟩ → ⟨ fst E ∈ Zv ⟩ → ⟨ fst d ∈ Zv ⟩
           → fst T ≡ fst (SatGraph.pairs W) → fst C ≡ fst (AllCodes W) → fst E ≡ fst (Tower.tower W)
           → fst d ≡ 𝒟ₒ (fst W) → ⟨ δ4 T C E d ⊨ body ⟩ → ⟨ δ ⊨ defIn w z N body ⟩
  defIn-in W qw T C E d T∈ C∈ E∈ d∈ qT qC qE qd hb =
```

内向きの読みでは、まず `sat-complete` が、真正な充足関係表、符号集合、環境の塔が `satAt` を満たすことを示します。次に `def-complete` が、その証明と与えられた `d` の等式を使って、定義可能冪集合の節を示します。与えられた本体の証明で連言が完成し、その後、四つの証人とそれぞれの所属証明が、入れ子の命題的切り詰めの中へ順に導入されます。

```agda
    ∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs
      , ( def-complete i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁
    where
    hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh 4 w) i2 i1 (shN 4 N) ⟩
    hs = sat-complete i3 (sh 4 w) i2 i1 (shN 4 N) (δ4 T C E d) W qw qT qC qE tg
```

述語 `Supply` は、`c` が順序数なら、`defIn` が必要とする四つの証人がすでに共通の上界の中にあることを述べます。その四つとは、段階 `Lset c` の充足グラフ、符号集合、環境の塔、および次の段階 `Lset (sucV c)` です。

```agda
Supply : (Zv : V ℓ) (c : V ℓ) → IsOrd c → Type (ℓ-suc ℓ)
Supply Zv c oc =
    ⟨ fst (SatGraph.pairs (LsetS c oc)) ∈ Zv ⟩
  × ( ⟨ fst (AllCodes (LsetS c oc)) ∈ Zv ⟩
  × ( ⟨ fst (Tower.tower (LsetS c oc)) ∈ Zv ⟩
```

第四の成分が次の段階であり、近似の後続の一歩に必要なものです。

```agda
  × ⟨ Lset (sucV c) ∈ Zv ⟩ ))
```

環境 `γ` における一つの候補となる階層の段階を固定します。候補の結果を `Vv`、それ以前の添字の集合を `Bv`、候補表の底集合を `Fv` と書きます。問うのは、`Fv` の関係する行が正しく、かつ存在すると分かったとき、二つの有界な包含から `Vv = Lset Bv` が強制されるかどうかです。

```agda
module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Vv = fst (lookup v γ)
    Bv = fst (lookup b γ)
    Fv = fst (lookup f γ)
```

共通の上界の底集合を `Zv` と書きます。これは、補助的な充足関係、符号、環境の塔、定義可能冪集合の証人をどこで見つけられるかを制御します。一段階から得たい等式には `Zv` は現れません。この上界は記述を可能にしますが、得られる段階の値の一部にはなりません。

```agda
    Zv = fst (lookup z γ)
```

内向きの本体では、`d` は `defIn` が認識する定義可能冪集合であり、`x` は外側の `v` 上の有界全称量化子が導入した要素です。原子論理式の本体は `x ∈ d` を述べます。記録された値 `w` を `Lset c` と同定すれば、これはある `c ∈ b` に対する `𝒟ₒ (Lset c)` への所属になります。

```agda
    intoBody : Formula S (5 + m)
    intoBody = defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)
```

`over` の本体は定義可能冪集合の記述であり、その内側の論理式は、記述された集合のすべての要素が候補となる次の値に属することを述べます。これは合併の等式に必要な逆向きの包含を与えます。

```agda
    overBody : Formula S (4 + m)
    overBody = defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
```

一段階の読み補題は、`Bv` より下の各対の行が正しい値をもつこと (`Values`) と、`Bv` より下の各添字に正準な行があること (`Entries`) を別々に仮定します。ちょうどこの二つの仮定のもとで、`stepAt` の二つの部分が反対向きの所属の含意を与え、外延性から `Vv = Lset Bv` が得られます。これらの仮定が制約するのは関係する対の行だけであり、候補表の無関係な要素を排除するものではありません。

```agda
  step-out : ⟨ γ ⊨ stepAt v b f z N ⟩ → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → Vv ≡ Lset Bv
  step-out (hi , ho) vals ents = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
    where
    fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ Lset Bv ⟩
    fwd x x∈ = PT.rec (snd (x ∈ Lset Bv)) (λ { (c , (c∈ , h1)) → PT.rec (snd (x ∈ Lset Bv))
```

前向きの包含では、`intoAt` が段階の添字 `c ∈ Bv`、表の対の行 `(c,w)`、そして `x` を含む定義可能冪集合の値 `d` を与えます。仮定 `Values` は `w` を `Lset c` と同定するので、`d = 𝒟ₒ (Lset c)` です。段階への内向きの規則 `Lset-in` が、この寄与から `x` を `Lset Bv` へ運びます。

```agda
      (λ { (q , (q∈ , h2)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (w , s , (eq , h3)) →
        PT.rec (snd (x ∈ Lset Bv)) (λ { (T , C , E , d , (d∈ , (qd , hx))) →
          Lset-in Bv (fst c) x c∈
            (subst (λ u → ⟨ x ∈ u ⟩)
              (qd ∙ cong 𝒟ₒ (vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) eq q∈))) hx) })
```

入れ子の存在形を読む各段階で、命題的切り詰めは保たれます。まず `sndEx-out` が、対の形をした表の項目から第二成分 `w` が単に存在することを復元し、次に `defIn-out` が、補助データと、`d` を `w` の定義可能冪集合と同定する等式が単に存在することを復元します。各切り詰めは、所属命題 `x ∈ Lset Bv` へ直接除去されます。

```agda
        (DefInRead.defIn-out i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) (w ∷ s ∷ q ∷ c ∷ xS ∷ γ) tg h3) })
        (sndEx-out i0 i1 intoBody (q ∷ c ∷ xS ∷ γ) h2) })
      h1 })
      (hi xS x∈)
      where
```

証明は周囲の要素 `x ∈ Vv` から始まりますが、論理式は構成可能な台 `S` の上で解釈されます。演算 `down` はこの所属証明を使って `x` を台の要素 `xS` として提示します。`xS` を環境の先頭に置くと、新しく束縛されたスロットは同じ底集合 `x` を表します。

```agda
      xS : S
      xS = down (lookup v γ) x x∈
```

`step-out` の逆向きの包含は、実際の段階 `Lset Bv` の要素を候補の値 `Vv` に入れます。これは `Lset Bv` の切り詰められた段階分解を消去し、`x` がその定義可能冪集合に属するような、より前の段階 `δ` についての主張へ帰着させます。

```agda
    bwd : (x : V ℓ) → ⟨ x ∈ Lset Bv ⟩ → ⟨ x ∈ Vv ⟩
    bwd x x∈ = PT.rec (snd (x ∈ Vv)) put (Lset-out Bv x x∈)
      where
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ Vv ⟩
      put (δ , (δ∈ , xD)) = PT.rec (snd (x ∈ Vv))
```

`Lset-out` がより前の添字 `δ` を示すと、完全性が正準な表の項目 `(δ, Lset δ)` を与えます。`over` の節をこの項目に適用し、さらに `defIn-out` がそこで有界化された集合 `d` を `𝒟ₒ (Lset δ)` と同一視します。したがって、その全称な本体は与えられた `x` を候補の値 `Vv` に入れます。この向きで使うのは `Entries` が与える正準な項目であり、`Values` への別の訴えは要りません。

```agda
        (λ { (T , C , E , d , (d∈ , (qd , hsub))) →
          hsub (down d x (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD)) (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD) })
        (DefInRead.defIn-out i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
          (w ∷ container q c w refl .fst ∷ q ∷ c ∷ γ) tg
          (useSnd i0 (q ∷ c ∷ γ) c w refl overBody i1 refl (ho c δ∈ q (ents c δ∈))))
```

名づけられる二つの対象は、符号化された引数と符号化された対です。どちらも、所属の証明を下降して台の要素として提示されます。

```agda
        where
        c : S
        c = down (lookup b γ) δ δ∈
        q : S
        q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
```

行の値 `w` は、対の提示から読まれ、本体の充足が消費する成分です。

```agda
        w : S
        w = sndS q δ (Lset δ) refl
```

ステップの条項の内向きの方向には、五つの仮定が要ります。界の順序数性、提案された値と界での段階の同定、界での表の正しさと完備さ、そして界の各要素のための補助の証人を証人の界の中に置く供給関数です。証明は二つの連言項に分かれます。

```agda
  step-in : (ob : IsOrd Bv) → Vv ≡ Lset Bv → Values (lookup f γ) Bv → Entries (lookup f γ) Bv
          → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
          → ⟨ γ ⊨ stepAt v b f z N ⟩
  step-in ob vq vals ents sup = into , over
    where
```

`into` の連言項は、提案された値の要素 `x` から外向きに読まれます。界での段階の切り詰められた分解が、より前の順序数と定義可能冪集合への所属を名指し、存在の導入がそれを二つの有界量化子に満たします。

```agda
    into : ⟨ γ ⊨ intoAt v b f z N ⟩
    into x x∈ = PT.rec squash₁ put (Lset-out Bv (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) vq x∈))
      where
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ fst x ∈ 𝒟ₒ (Lset δ) ⟩)
          → ⟨ (x ∷ γ) ⊨ ∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f)) (sndEx i0 i1 intoBody)) ⟩
```

入れ子になった有界存在量化子は、命題的切り詰めからデータを取り出すことなく満たされます。証明は `δ` を台の要素 `c` として提示し、`Entries` によって正準な対を `q` として提示し、`fillSnd` で対の分解を与えます。残る本体が `hb` です。充足は命題なので、各構成子は `∃[]-syntax` に組み込まれた命題的切り詰めを保ちます。

```agda
      put (δ , (δ∈ , xD)) =
        ∣ c , ( δ∈ , ∣ q , ( ents c δ∈ , fillSnd i0 (q ∷ c ∷ x ∷ γ) c w refl intoBody hb i1 refl ) ∣₁ ) ∣₁
        where
        oδ : IsOrd δ
        oδ = mem-ord {A = Bv} ob δ δ∈
```

三つの台の要素は、それぞれ異なる根拠から得られます。所属 `δ ∈ Bv` はより前の添字を `c` として提示し、正準な対が表に属するという証明はその対を `q` として提示し、`δ` の順序数性によって `LsetS` は段階 `Lset δ` を `w` として提示できます。有界な証人を組み立てる際には、これらの由来を区別することが大切です。

```agda
        c : S
        c = down (lookup b γ) δ δ∈
        q : S
        q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
        w : S
```

ここで `w` は構成可能な台における実際の段階 `Lset δ` です。供給の仮定を `δ` に適用すると、その充足関係表、符号集合、環境の塔、後継段階がいずれも `Zv` に属するという証明が得られます。この四つの界とそれらを同定する等式により、`defIn-in` は残る課題を数学的事実 `x ∈ 𝒟ₒ (Lset δ)` に帰着させます。

```agda
        w = LsetS δ oδ
        s = sup δ oδ δ∈
        hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩
        hb = DefInRead.defIn-in i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)
               (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) tg w refl
```

四つの有界な対象は、実際の充足関係表、符号集合、環境の塔、そして `Lset (sucV δ)` です。供給の仮定はそれぞれが `Zv` に属することを証明し、最初の三つは反射律によって記述が要求する構造と一致します。最後に `Lset-suc δ` が四つ目を `𝒟ₒ (Lset δ)` と同一視するので、もとの `x` の所属を論理式の本体へ移せます。

```agda
               (SatGraph.pairs w) (AllCodes w) (Tower.tower w) (LsetS (sucV δ) (suc-ord oδ))
               (s .fst) (s .snd .fst) (s .snd .snd .fst) (s .snd .snd .snd) refl refl refl (Lset-suc δ)
               (subst (λ u → ⟨ fst x ∈ u ⟩) (sym (Lset-suc δ)) xD)
```

`over` の連言を示すため、`c ∈ Bv`、表の要素 `q`、そして `q` を対 `(c,w)` として提示する仕方を固定します。すると正しさにより `w` は `Lset c` と同一視されます。残る目標は `y` について一様です。すべての `y ∈ 𝒟ₒ w` が候補の値 `Vv` に属さなければなりません。これは候補の値を `Bv` における段階と同一視するために必要な第二の包含です。

```agda
    over : ⟨ γ ⊨ overAt v b f z N ⟩
    over c c∈ q q∈ = sndAll-in i0 i1 overBody (q ∷ c ∷ γ) (λ w s s∈ w∈ e →
      let wq : fst w ≡ Lset (fst c)
          wq = vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) e q∈)
          oc : IsOrd (fst c)
```

`c` の順序数性は界から受け継がれ、段階は台の要素として提示され、供給の関数が `c` で四つの証人を作ります。

```agda
          oc = mem-ord {A = Bv} ob (fst c) c∈
          W : S
          W = LsetS (fst c) oc
          s' = sup (fst c) oc c∈
      in DefInRead.defIn-in i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
```

`c` における供給は、実際の充足関係表、符号集合、環境の塔、後継段階をすべて `Zv` の中に有界化するので、`defIn-in` は定義可能冪集合の記述を示せます。`y` がそこで記述された集合に属するとき、`Lset-suc c` によりこれは `y ∈ 𝒟ₒ (Lset c)` となり、さらに `c ∈ Bv` と `Lset-in` によって `y ∈ Lset Bv` が得られます。最後に `Vv ≡ Lset Bv` に沿って移せば、候補の値への所属が従います。

```agda
           (w ∷ s ∷ q ∷ c ∷ γ) tg W wq
           (SatGraph.pairs W) (AllCodes W) (Tower.tower W) (LsetS (sucV (fst c)) (suc-ord oc))
           (s' .fst) (s' .snd .fst) (s' .snd .snd .fst) (s' .snd .snd .snd) refl refl refl (Lset-suc (fst c))
           (λ y y∈d → subst (λ u → ⟨ fst y ∈ u ⟩) (sym vq)
             (Lset-in Bv (fst c) (fst y) c∈ (subst (λ u → ⟨ fst y ∈ u ⟩) (Lset-suc (fst c)) y∈d))))
```

近似の読み手は、表・界・証人の界・タグの対応・環境をパラメータとします。三つの基礎の集合が一度だけ名づけられます。

```agda
module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Fv = fst (lookup f γ)
    Bv = fst (lookup b γ)
    Zv = fst (lookup z γ)
```

ステップの本体は、四つずらした枠でのステップの条項です。

```agda
    stepBody : Formula S (4 + m)
    stepBody = stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N)
```

近似の条項の外向きの読み出しは、界での表の正しさと完備さを作ります。述語 `P` は、それぞれの入力について証明すべきことを記録します。記録された値がその入力での段階であること。結果が正確に `Values` と `Entries` であることに注意してください。表が対でない要素や、界の外を第一成分とする項目を含まないとは述べていません。

```agda
  approx-out : ⟨ γ ⊨ approxAt f b z N ⟩ → IsOrd Bv → Values (lookup f γ) Bv × Entries (lookup f γ) Bv
  approx-out (hd , hs) ob = vals , ents
    where
    P : V ℓ → Type (ℓ-suc ℓ)
    P c = ⟨ c ∈ Bv ⟩ → (w : S) → ⟨ pr c (fst w) ∈ Fv ⟩ → fst w ≡ Lset c
```

被覆の節は、各 `c ∈ Bv` に対して、第一成分が `c` である対を提示する表の要素が命題的に切り詰められた意味で存在すると述べます。その対を読むと値 `w` が現れ、もとの所属の証明は正準な記法 `pr c w` へ移されます。結果は命題的に切り詰められたままなので、`entryOf` は後の命題的推論に存在を与えますが、値を大域的に選ぶことはありません。

```agda
    entryOf : (c : S) → ⟨ fst c ∈ Bv ⟩ → ∥ Σ[ w ∈ S ] ⟨ pr (fst c) (fst w) ∈ Fv ⟩ ∥₁
    entryOf c c∈ = PT.rec squash₁
      (λ { (q , (q∈ , h)) → PT.map (λ { (w , s , (e , _)) → w , subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ })
                              (sndEx-out i0 i1 ⊤̇ (q ∷ c ∷ γ) h) })
      (hd c c∈)
```

帰納段階では、`c ∈ Bv` を満たす任意の記録された対 `(c,w)` を検証します。その所属の証明から近似の第二の節が `stepAt w c` を与え、帰納の仮定が `c` より下の各入力での正しさを与えます。さらに被覆の節がそこで対応する正準な項目を与えます。したがって `StepRead.step-out` は、記録された値がちょうど `Lset c` であると結論できます。

```agda
    step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c
    step c IH c∈ w rec =
      StepRead.step-out i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) env tg
        (useBoth i0 (q ∷ γ) cS w refl stepBody (hs q rec)) vals' ents'
      where
```

ここで関係する集合を構成可能な台の中に提示します。所属 `c ∈ Bv` から台の要素 `cS` が得られ、`pr c (fst w)` が表に属するという仮定から `q` が得られます。値 `w` はすでに帰納述語へ渡された台の要素です。次の環境は、この三つの提示をステップの論理式が要求する枠に置きます。

```agda
      cS : S
      cS = down (lookup b γ) c c∈
      q : S
      q = down (lookup f γ) (pr c (fst w)) rec
      env : S ^ (4 + m)
```

拡張された環境は、ステップの読み出しのための四つの枠を組み立てます。界の順序数性がより小さい入力を界の下に制限し、より小さい入力での正しさの読み出しは、帰納の仮定の制限です。

```agda
      env = w ∷ cS ∷ container q cS w refl .fst ∷ q ∷ γ
      in' : (y : S) → ⟨ fst y ∈ c ⟩ → ⟨ fst y ∈ Bv ⟩
      in' y y∈ = ob .fst {x = c} {y = fst y} y∈ c∈
      vals' : Values (lookup f γ) c
      vals' y w' y∈ rec' = IH (fst y) y∈ (in' y y∈) w' rec'
```

より小さい入力での完備さも同じ制限で復元されます。より小さい入力ごとに、切り詰められた項目が消費され、帰納の仮定の値の等式が、正準な項目を所定の位置へ運びます。

```agda
      ents' : Entries (lookup f γ) c
      ents' y y∈ = PT.rec (snd (pr (fst y) (Lset (fst y)) ∈ Fv))
        (λ { (w' , rec') → subst (λ u → ⟨ pr (fst y) u ∈ Fv ⟩) (IH (fst y) y∈ (in' y y∈) w' rec') rec' })
        (entryOf y (in' y y∈))
```

`Bv` より下での正しさは、基礎にある入力 `c` に対する周囲の所属帰納によって得られます。述語 `P c` は `c ∈ Bv` を条件とします。この所属は定理を必要な界に制限すると同時に、`Bv` の順序数性を通じて、より小さい各入力に帰納の仮定を適用できるようにします。帰納の結論を任意の記録された値に適用すると `Values` が得られます。

```agda
    vals : Values (lookup f γ) Bv
    vals c w c∈ rec = ∈-induction {P = P} step (fst c) c∈ w rec
```

界での完備さは、切り詰められた項目と、今証明した正しさを合成します。値の等式が、記録された項目を正準な項目へ運びます。

```agda
    ents : Entries (lookup f γ) Bv
    ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ Fv))
      (λ { (w , rec) → subst (λ u → ⟨ pr (fst c) u ∈ Fv ⟩) (vals c w c∈ rec) rec })
      (entryOf c c∈)
```

近似の条項の内向きの方向は、より強い意味論的な仮定からはじまります。表が界で階層を実現することです。この非対称は意図的なものです。外向きの方向が証明するのは二つの表の条件だけで、内向きの方向が消費するのは、階層の完全な仕様です。

```agda
  approx-in : (ob : IsOrd Bv) → IsHier Bv (lookup f γ)
            → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
            → ⟨ γ ⊨ approxAt f b z N ⟩
  approx-in ob sp sup = dom , steps
    where
```

階層の仕様の外向きの読み出しは、記録されたそれぞれの対について、入力が界の下にあり、値がそこの段階に等しいと言います。

```agda
    hout : (c w : S) → ⟨ pr (fst c) (fst w) ∈ Fv ⟩ → ⟨ fst c ∈ Bv ⟩ × (fst w ≡ Lset (fst c))
    hout = hier-out Bv ob (lookup f γ) sp
```

内向きの読み出しは、界の下のすべての正準な対が記録されていると言います。

```agda
    hin : (c : S) → ⟨ fst c ∈ Bv ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ Fv ⟩
    hin = hier-in Bv ob (lookup f γ) sp
```

定義域の連言項は、界の下のそれぞれの入力で段階を提示し、正準な対を表の中へ注入することで証明されます。

```agda
    dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇)) ⟩
    dom c c∈ = ∣ q , ( hin c c∈ , fillSnd i0 (q ∷ c ∷ γ) c w refl ⊤̇ (λ z → z) i1 refl ) ∣₁
      where
      w : S
      w = LsetS (fst c) (mem-ord {A = Bv} ob (fst c) c∈)
```

正準な対は、所属の証明を下降して台の要素として提示されます。

```agda
      q : S
      q = down (lookup f γ) (pr (fst c) (Lset (fst c))) (hin c c∈)
```

近似の第二の連言は、表の各要素 `q` と、`q` を対 `(c,w)` として提示する各方法について示す必要があります。そのような提示のもとでは、階層の厳密な仕様から `c ∈ Bv` と `w ≡ Lset c` の両方が得られ、`c` におけるステップの論理式を証明する準備が整います。ここでは、候補の表の任意の要素がそのような対の提示をもつとは主張していません。

```agda
    steps : ⟨ γ ⊨ ∀̇∈ (var f) (bothAll i0 stepBody) ⟩
    steps q q∈ = bothAll-in i0 stepBody (q ∷ γ) (λ c w s s∈ c∈s w∈s e →
      let rec : ⟨ pr (fst c) (fst w) ∈ Fv ⟩
          rec = subst (λ u → ⟨ u ∈ Fv ⟩) e q∈
          c∈ : ⟨ fst c ∈ Bv ⟩
```

入力は、階層の外向きの読み出しによって界の下にあり、順序数性は受け継がれます。そして `StepRead.step-in` が、制限された正しさと完備さと、より小さい入力ごとの供給を含む、五つの仮定をすべて受け取ります。

```agda
          c∈ = hout c w rec .fst
          oc : IsOrd (fst c)
          oc = mem-ord {A = Bv} ob (fst c) c∈
      in StepRead.step-in i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) (w ∷ c ∷ s ∷ q ∷ γ) tg oc (hout c w rec .snd)
           (λ d w' d∈ rec' → hout d w' rec' .snd)
```

現在の入力 `c` より下での完全性は `hier-in` から得られます。順序数である界の推移性が `d ∈ c ∈ Bv` を `d ∈ Bv` に変え、そこで正準な項目の存在が分かります。補助的な界は別の根拠から来ます。与えられた供給関数 `sup` を同じ推移性に沿って制限したものです。したがって、階層の仕様が表の項目を与え、`sup` が四つの有界な符号化対象を与えます。

```agda
           (λ d d∈ → hin d (ob .fst {x = fst c} {y = fst d} d∈ c∈))
           (λ d od d∈ → sup d od (ob .fst {x = fst c} {y = d} d∈ c∈)))
```

階層の読みには四つの特別な枠があります。候補の段階 `a`、その段階の添字 `p`、近似表 `f`、そして共通の証人の界 `z` です。タグの写像は符号化の論理式が使う十個の数項の位置を解釈し、環境はこれらすべての枠に台の要素を与えます。

```agda
module HierRead {m : ℕ} (a p f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Av = fst (lookup a γ)
    Pv = fst (lookup p γ)
    Zv = fst (lookup z γ)
```

階層の論理式の健全性の定理はこう言います。論理式が成立し、順序数の枠が順序数であれば、層の枠は順序数の枠での段階に等しい、と。証明は、近似と最後のステップを別々に読みます。

```agda
  hier-sound : ⟨ γ ⊨ hierAt a p f z N ⟩ → IsOrd Pv → Av ≡ Lset Pv
  hier-sound (ha , hs) op = StepRead.step-out a p f z N γ tg hs (ve .fst) (ve .snd)
    where
    ve = ApproxRead.approx-out f p z N γ tg ha op
```

階層の論理式の完備性の定理は、添字の枠の順序数性、層の枠と段階の同定、添字での実際の階層の表、そして供給の関数を受け取り、充足を作ります。

```agda
  hier-complete : (op : IsOrd Pv) → Av ≡ Lset Pv → IsHier Pv (lookup f γ)
                → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Pv ⟩ → Supply Zv c oc)
                → ⟨ γ ⊨ hierAt a p f z N ⟩
  hier-complete op aq sp sup =
      ApproxRead.approx-in f p z N γ tg op sp sup
```

証明は、階層の仕様からの内向きの近似と、最後のステップを合成します。後者の正しさと完備さの条項は、より小さい入力ごとに、階層の仕様から外向きに読まれます。

```agda
    , StepRead.step-in a p f z N γ tg op aq
        (λ c w c∈ rec → hier-out Pv op (lookup f γ) sp c w rec .snd)
        (hier-in Pv op (lookup f γ) sp) sup
```

## 近似と完成した階層を読む

内部のモジュールは、対象言語の中で構成可能階層を最終的に表す論理式を封印します。

```agda
module Inner where
```

十四枠の環境は十個の数項タグから始まります。`weakenFin` を繰り返すと、各添字は数値上の位置を変えずに `Fin 14` へ埋め込まれるので、`N14` は零番から九番までの枠を占めます。これは、先頭の十項がフォン・ノイマン数項である、後に用いる具体的な環境と一致します。

```agda
  N14 : Fin 10 → Fin 14
  N14 k = weakenFin (weakenFin (weakenFin (weakenFin k)))
```

末尾の四つの枠が内側の論理式の数学的データを完成させます。十番の枠は表 `ff`、十一番は候補の段階 `aa`、十二番はその段階の添字 `pp`、十三番は共通の界 `zz` を保持します。したがって環境全体の順序は、十個のタグに続いて `f`、`a`、`p`、`z` となります。

```agda
  ff aa pp zz : Fin 14
  ff = sh 10 (i0 {3})
  aa = sh 11 (i0 {2})
  pp = sh 12 (i0 {1})
  zz = sh 13 (i0 {0})
```

内側の論理式は二つの数学的要件を連言します。`pins N14` は最初の十枠を符号化の記述に必要な数項タグとして固定し、`hierAt aa pp ff zz N14` は `ff` が `pp` より下の階層を近似し、`aa` が `pp` におけるその次の値であり、補助データがすべて `zz` で有界化されることを述べます。不透明性により、この大きな論理式は証明済みの読み補題の背後に保たれます。

```agda
  opaque
    inner : Formula S 14
    inner = pins N14 ∧̇ hierAt aa pp ff zz N14
```

有界性を証明するため、検査器はこの局所的な範囲で `inner` と、封印された記述 `satAt`、`defAt` を展開できます。この限定された展開により、大きな連言が原子論理式、結合子、有界量化子だけから作られていることが分かります。この証明境界の外では、展開された論理式を正規化するのではなく、読み補題によって数学的内容を取り出します。

```agda
  opaque
    unfolding inner satAt defAt
```

局所的な展開の後、`checkΔ₀ inner tt` は構造的な `Δ₀` の証人を与えます。`inner` に現れる量化子はすべて有界です。これはこの特定の論理式に対する構文的な検証であり、`checkΔ₀` が有界性を双方向に決定するという主張ではありません。外側のモジュールとそこから公開される結果は、引き続き `lem : LEM (ℓ-suc ℓ)` をパラメータとします。

```agda
    Δ₀-inner : Δ₀ inner
    Δ₀-inner = checkΔ₀ inner tt
```

封印された論理式の読み出しも、同じ展開の境界を通して公開されます。

```agda
  opaque
    unfolding inner
```

連言の外向きの読み出しは、その二つの連言項の対です。連言とは命題の対だからです。

```agda
    inner-out : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → ⟨ γ ⊨ pins N14 ⟩ × ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩
    inner-out γ h = h
```

逆に、pin の節と階層の節の証明は、それらの連言を満たすために必要な二つの成分をなします。`inner-out` と合わせると、後で必要となる正確な二方向が得られます。大きな論理式から二つの数学的部分を取り出すことも、両方を証明した後で論理式を再構成することもできます。

```agda
    inner-in : (γ : S ^ 14) → ⟨ γ ⊨ pins N14 ⟩ → ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ → ⟨ γ ⊨ inner ⟩
    inner-in γ h1 h2 = h1 , h2
```

`suc n` 個の位置をもつ外側の環境に対して、`lastFin` はその最後の位置を表します。以下の各適用では、その位置に新しい存在量化子の界となる共通の集合が置かれています。有界量化子が導入する証人は本体の新しい先頭位置を占め、`lastFin` が指す位置ではありません。

```agda
  lastFin : {n : ℕ} → Fin (suc n)
  lastFin {zero} = zero
  lastFin {suc n} = suc (lastFin {n})
```

演算 `wrap` は、本体の先頭にある証人の位置を存在量化し、その証人が外側の最後の位置で名づけられた集合に属することを要求します。そのため、有界性を保ったまま項数が一つ減ります。この演算を繰り返すことで、十個の数項タグと表がそれぞれ量化され、いずれも共通の界 `z` の要素であることが要求されます。

```agda
  wrap : {n : ℕ} → Formula S (suc (suc n)) → Formula S (suc n)
  wrap {n} φ = ∃̇∈ (var (lastFin {n})) φ
```

Δ₀ の証人は、包む操作の下でも保たれます。有界の存在量化は、それ自体が有界の構成だからです。

```agda
  δ-wrap : {n : ℕ} {φ : Formula S (suc (suc n))} → Δ₀ φ → Δ₀ (wrap {n} φ)
  δ-wrap d = δ-∃∈ d
```

五回の包む操作が、十の数項の枠のうち五つを消費し、自由な位置を十四から九へと一つずつ減らします。

```agda
  s13 = wrap {12} inner
  s12 = wrap {11} s13
  s11 = wrap {10} s12
  s10 = wrap {9}  s11
  s9  = wrap {8}  s10
```

さらに五回の包む操作が、自由な位置を九から四へ減らし、層・順序数の添字・表・証人の界だけを残します。

```agda
  s8  = wrap {7}  s9
  s7  = wrap {6}  s8
  s6  = wrap {5}  s7
  s5  = wrap {4}  s6
  s4  = wrap {3}  s5
```

十一回目の包みは、再び `z` を界として、残る補助的な枠である階層の表 `f` を存在量化します。自由な位置はちょうど三つ、順に `(a,p,z)`、すなわち候補の段階、その段階の添字、共通の証人の界だけになります。したがって `three` は三項論理式であって文ではありません。後の消去は使われていない定数領域を取り除きますが、この三つの自由変数は取り除きません。

```agda
  three : Formula S 3
  three = wrap {2} s4
```

証人の論理式は十一回包まれます。共通の界の内側で導入された有界の存在量化子の一つひとつに対応します。各包みが Δ₀ の証拠の一層を加えるため、包まれた論理式は全体を通して有界のままです。

```agda
  Δ₀-three : Δ₀ three
  Δ₀-three =
    δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap
      (δ-wrap (δ-wrap (δ-wrap (δ-wrap Δ₀-inner))))))))))
```

包まれた論理式に定数が含まれないことを確かめるため、この計算では密封された `inner`、`satAt`、`defAt` の定義を参照できます。この局所的な展開が明らかにするのは出現回数の簡約に必要な構文だけであり、周囲の議論では大きな論理式そのものを読み補題と書き補題を通して扱います。

```agda
  opaque
    unfolding inner satAt defAt
```

`three` における定数の出現回数は零です。残る三つの位置は `a`、`p`、`z` のための自由変数であり、定数ではありません。この計算のために密封された部分を展開すると、論理式のすべての項が変数から作られているため、等式は定義的に簡約されます。

```agda
    count-three : countFo three ≡ 0
    count-three = refl
```

`three` は定数を含まないので、消去は定数域を構成可能な台から空の型へ変えつつ、変数と量化子の構造を保ちます。したがって得られる `erased` は無パラメータですが、アリティは三のままです。これを元の定数域へ埋め込むと `three` が復元されます。

```agda
  erased : Formula (⊥* {ℓ-suc ℓ}) 3
  erased = Cnt.erase three count-three
```

消去は Δ₀ の証拠も保ちます。変更されるのは、もともと出現しない定数記号だけです。そのため `three` の各有界量化子は有界なままであり、同じ構造的な議論によって `erased` が Δ₀ であることが示されます。

```agda
  Δ₀-erased : Δ₀ erased
  Δ₀-erased = erase-Δ₀ three count-three Δ₀-three
```

意味論的には、一層の包みは命題的に切り詰められた有界の証人です。境界の要素 `x` が本体を満たすたびに `P` が得られるなら、`unwrap` はその切り詰められた存在を `P` へ除去します。`P : hProp` という宣言が、この除去に必要な命題性をちょうど与えます。

```agda
  unwrap : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) {P : hProp (ℓ-suc ℓ)}
         → ((x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ P ⟩)
         → ⟨ γ ⊨ wrap {n} φ ⟩ → ⟨ P ⟩
  unwrap φ γ {P} k h = PT.rec (snd P) (λ { (x , xz , hx) → k x xz hx }) h
```

`wrap-in` は、名指された要素とその拡張での本体の充足から、有界の存在量化を組み立てます。有界の存在量化子の導入規則です。

```agda
  wrap-in : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) (x : S)
          → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ wrap {n} φ ⟩
  wrap-in φ γ x m h = ∣ x , (m , h) ∣₁
```

## 構成可能な階層を表すパラメータなし論理式

表に現れる論理式 `levelFo` には、三つの自由な位置 `(a,p,z)` があります。これは `p` が順序数であるという主張と、`z` で有界化された消去後の階層記述との連言です。したがって健全性の結論が `a` と `p` だけに言及しても、`z` は論理式の入力として残ります。

```agda
levelFo : Formula (⊥* {ℓ-suc ℓ}) 3
levelFo = isOrd-at-p ∧̇ Inner.erased
```

`levelFo` の二つの連言項はいずれも Δ₀ であり、Δ₀ のクラスは連言について閉じています。したがって連言の構成子は、非有界量化子を導入することなく、二つの有界性の証拠を `Δ₀-levelFo` の証拠へまとめます。

```agda
Δ₀-levelFo : Δ₀ levelFo
Δ₀-levelFo = δ-∧ Δ₀-isOrd-at-p Inner.Δ₀-erased
```

読みの補題は、定数のない任意の Δ₀ 論理式に対して三つのパスを合成します。制限された台から周囲の階層への Δ₀ 絶対性、空の定数域の埋め込みによる充足の不変性、そして空の解釈の一意性です。結果は二つの充足の命題の等式です。

```agda
read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : S ^ n)
     → (δ ⊨ embed φ) ≡ (map fst δ ⊨ₚ φ)
read {n} {φ} dφ δ =
    AbsL.abs₀ (mapΔ₀ Empty.rec* dφ) δ
  ∙ embed-⊨ 𝒮ᵥ {K = S} fst φ (map fst δ)
```

このパスの最後の等式が扱うのは定数の解釈です。定数域が空なので、どの解釈も各点で空型の除去から得られる解釈と一致します。関数外延性がそれを正準な空の解釈と同一視し、その結果、直前の埋め込みの比較は同じ無パラメータ論理式の外側での読みへ到達します。

```agda
  ∙ cong (λ ι → SemVᵃ.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ)
         (funExt (λ b → Empty.rec* b))
```

外向きの順序数の読みは、順序数性の原子の二つの節を、`p` の基底集合の推移性とその各要素の推移性へと展開します。すべての項目は `p` の提示を通して降ろされます。

```agda
ord-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ → IsOrd (fst p)
ord-out a p z h =
    ( λ {x} {y} y∈x x∈p → h .fst (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x )
  , ( λ x x∈p {y} {u} u∈y y∈x →
        h .snd (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x
```

順序数性の第二の条項では、`x ∈ p`、`y ∈ x`、`u ∈ y` を取ります。この三段の所属を構成可能な台へ降ろすと、論理式の第二の連言項から `u ∈ x` が得られます。これは `p` の各要素 `x` の推移性そのものであり、第一の条項と合わせて `IsOrd p` が得られます。

```agda
          (down (down (down p x x∈p) y y∈x) u u∈y) u∈y )
```

内向きの順序数の読みは、順序数性の証明から二つの節を組み立てます。すべての項目は `L` の要素としてまとめられます。

```agda
ord-in : (a p z : S) → IsOrd (fst p) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩
ord-in a p z op =
    (λ x x∈p y y∈x → op .fst {x = fst x} {y = fst y} y∈x x∈p)
  , (λ x x∈p y y∈x u u∈y → op .snd (fst x) x∈p {x = fst y} {y = fst u} u∈y y∈x)
```

健全性の議論はここから、隠された論理式を十四のスロットで読む形に移ります。目的は、有界な補助証人を捨てつつ、その数学的帰結、すなわちスロット `a` の値がスロット `p` を添字とする構成可能な段階であることを残すことです。

```agda
private
  module Sound where
    open Inner
```

`finish` 補題は `inner` の二つの連言項を分けて読みます。pins の読み補題は第一項を、階層の読み補題が必要とする十個の数項の等式へ変えます。第二項の近似から `hier-sound` が復元するのは `Values × Entries` だけですが、`p` の順序数性が与えられれば、それで最後のステップを `a = Lset p` と読むには十分です。ここでは、隠れた表に不正な形の要素がないことも、`p` の外を第一成分とする項目がないことも主張していません。

```agda
    finish : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → IsOrd (fst (lookup pp γ))
           → fst (lookup aa γ) ≡ Lset (fst (lookup pp γ))
    finish γ h op = HierRead.hier-sound aa pp ff zz N14 γ tg (inner-out γ h .snd) op
      where
      tg : Tags γ N14
```

固定された数項は pins の読みによって外向きに読まれ、対象言語の節から十の数項の等式が導かれます。

```agda
      tg = PinsRead.pins-out N14 γ (inner-out γ h .fst)
```

内部の健全性補題は、構成可能な台の三要素 `a`、`p`、`z` から始め、そこで `embed levelFo` が成り立つと仮定します。まず消去の逆等式を用いて、十一回包まれた論理式の充足を復元します。求める結論は、`a` の基礎集合と、`p` の基礎集合を添字とする `Lset` とを比較するものです。

```agda
    sound-L : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed levelFo ⟩ → fst a ≡ Lset (fst p)
    sound-L a p z (ho , hφ) =
      go (subst (λ ψ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ ψ ⟩) (Cnt.erase-inv three count-three) hφ)
      where
      ordp : IsOrd (fst p)
```

順序数性の連言項は、外向きの順序数の読みを通して `p` の順序数性の証明を生み出します。これが階層の読みの残りの入力です。

```agda
      ordp = ord-out a p z ho
```

最後まで残す等式を命題 `G` としてまとめます。累積階層の集合は h-集合をなすので、`setIsSet` によりこの等式型が `hProp` であることが分かります。したがって、命題的に切り詰められた各有界証人を、特定の証人を外へ取り出すことなく `G` へ除去できます。

```agda
      G : hProp (ℓ-suc ℓ)
      G = (fst a ≡ Lset (fst p)) , setIsSet (fst a) (Lset (fst p))
```

健全性は十一の有界の存在量化を一つずつ展開し、切り詰められた証人を命題の等式の中で消費します。展開の順序は論理式の束縛の順序を反映します。

```agda
      go : ⟨ (a ∷ p ∷ z ∷ []) ⊨ three ⟩ → ⟨ G ⟩
      go =
        unwrap s4 (a ∷ p ∷ z ∷ []) {G} λ F mF →
        unwrap s5 (F ∷ a ∷ p ∷ z ∷ []) {G} λ x9 m9 →
        unwrap s6 (x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x8 m8 →
```

続く五回の除去で、数項の証人 `x7` から `x3` までを復元します。各段階で環境は先頭側へ伸びますが、最後のスロットは常に `z` のままです。十一個の証人はすべてこの共通の境界から得られます。

```agda
        unwrap s7 (x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x7 m7 →
        unwrap s8 (x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x6 m6 →
        unwrap s9 (x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x5 m5 →
        unwrap s10 (x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x4 m4 →
        unwrap s11 (x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x3 m3 →
```

最も内側の証人が展開を完成させます。十四スロットの環境と順序数性の証明が finish の補題に渡され、二つの基底集合の等式が生まれます。

```agda
        unwrap s12 (x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x2 m2 →
        unwrap s13 (x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x1 m1 →
        unwrap inner (x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G}
          λ x0 m0 hm →
            finish (x0 ∷ x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) hm ordp
```

周囲の集合 `a`、`p`、`z` が構成可能であるとき、それぞれの構成可能性の証拠によって、これらを構成可能な台の要素として提示できます。Δ₀ 絶対性を逆向きに読むと、`levelFo` の周囲での充足がそれらの提示による充足へ移り、内部の健全性の議論を適用できます。基礎集合へ戻せば `a = Lset p` が得られます。したがって、三つの入力がすべて構成可能であることは明示的な仮定であり、論理式から導かれる結論ではありません。

```agda
level-sound : (a p z : V ℓ) → ⟨ isL a ⟩ → ⟨ isL p ⟩ → ⟨ isL z ⟩
            → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ levelFo ⟩ → a ≡ Lset p
level-sound a p z la lp lz h =
  Sound.sound-L (a , la) (p , lp) (z , lz)
    (subst ⟨_⟩ (sym (read Δ₀-levelFo ((a , la) ∷ (p , lp) ∷ (z , lz) ∷ []))) h)
```

完全性のため、妥当性のデータをもつ `lam` と順序数 `p ∈ lam` を固定します。順序数性のフィールドにより `lam` は段階の添字となり、対応する段階は `Lset lam` です。残るフィールドは後者閉包、`ω` の所属、および `lam` の下で必要となる符号化の証人を与えます。これらを用いて、特定の境界 `Lset lam` が段階 `Lset p` の記述に必要なすべての証人を含むことを示します。

```agda
private
  module Complete (lam : V ℓ) (ad : Adequate lam) (p : V ℓ) (op : IsOrd p) (p∈λ : ⟨ p ∈ lam ⟩) where
    open Inner
    open Adequate lam ad using ( ord; succ; ω∈; wit )
```

十分な段階 `lam` の推移性は、その順序数性から取り出されます。入れ子になった二つの所属が一つに合成されます。

```agda
    private
      tr : (x y : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ lam ⟩
      tr x y x∈ y∈ = ord .fst {x = x} {y = y} y∈ x∈
```

空集合は十分な段階に属します。`∅ ∈ ω ∈ lam` の連鎖に推移性を適用した結果です。

```agda
      ∅∈λ : ⟨ ∅ ∈ lam ⟩
      ∅∈λ = tr ω ∅ ω∈ (#∈ω zero)
```

数項の有界性の議論を、`lam` における構成可能階層へ特殊化します。順序数性、後者閉包、`∅ ∈ lam` から、各模型数項の基礎集合が `Lset lam` に属することが従います。これが、後で十個のタグ数項すべてに必要となる共通の境界を与えます。

```agda
      module B = Bound lam ord succ ∅∈λ using ( num∈λ )
```

`K = Lset lam` と置きます。これは第三の自由入力 `zS` が表す共通の境界集合です。階層表、十個の数項、そして各行を正当化するすべての補助集合が `K` に属することを示す必要があります。

```agda
      K : V ℓ
      K = Lset lam
```

`c ∈ lam` なら、後者閉包から `sucV c ∈ lam` が得られます。後者段階についての標準的な事実により `Lset c ∈ Lset (sucV c)` となり、さらに `sucV c ∈ lam` に沿う単調性によって、この所属を `Lset c ∈ K` へ持ち上げられます。後では同じ補題を `sucV c` に適用し、後者閉包をもう一度用いて `Lset (sucV c) ∈ K` を得ます。これが `c` の行に必要な定義可能冪集合の証人です。

```agda
      Lset∈K : (c : V ℓ) → ⟨ c ∈ lam ⟩ → ⟨ Lset c ∈ K ⟩
      Lset∈K c c∈ = Lset-mono {α = lam} {β = sucV c} (succ c c∈) (Lset∈suc c)
```

数項の有界性定理は、まず模型の数項の基礎集合を `K` に入れます。射影等式 `numeralL-fst` がその集合を周囲のフォン・ノイマン数項 `# k` と同一視し、それに沿う輸送から `# k ∈ K` が得られます。したがって十個の数項の証人は、階層表と同じ境界を満たします。

```agda
      num∈K : (k : ℕ) → ⟨ # k ∈ K ⟩
      num∈K k = subst (λ u → ⟨ u ∈ K ⟩) (numeralL-fst k) (B.num∈λ k)
```

四つの集合に名前が与えられます。段階 `Lset p`、順序数 `p`、段階 `Lset lam`、そして `p` における階層の表で、それぞれ適切な台の中にあります。

```agda
    aS pS zS F : S
    aS = LsetS p op
    pS = p , At.cL p op
    zS = LsetS lam ord
    F = At.hier p op
```

環境 `E` はここで、十四のスロットへの完全な割り当てを記録します。先頭から順に、数項 `0` から `9`、`p` における実際の階層表、意図した値 `Lset p`、添字 `p`、そして共通の境界 `Lset lam` が並びます。これは `inner` がデータを読むスロットの順序とちょうど一致します。

```agda
    E : S ^ 14
    E = nn 0 ∷ nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9
      ∷ F ∷ aS ∷ pS ∷ zS ∷ []
```

タグの仮定は、最初の四つのタグのスロットを、それぞれみずからの数項と定義的に同一視します。

```agda
    tg : Tags E N14
    tg zero = refl
    tg (suc zero) = refl
    tg (suc (suc zero)) = refl
    tg (suc (suc (suc zero))) = refl
```

続く五つの場合は、添字 4 から 8 までのタグのスロットを検証します。各参照は `E` の対応する項目へ簡約されるので、これらのスロットは定義上それぞれ数項 `4` から `8` です。

```agda
    tg (suc (suc (suc (suc zero)))) = refl
    tg (suc (suc (suc (suc (suc zero))))) = refl
    tg (suc (suc (suc (suc (suc (suc zero)))))) = refl
    tg (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl
    tg (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
```

最後の場合は、添字 9 にある十番目のタグのスロットが数項 `9` であることを確かめます。これで `Tags E N14` が要求する十個の等式が、明示された環境上の計算によってすべて得られました。

```agda
    tg (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
```

順序数 `p` の各要素 `c` に対して、供給の補題は四つの対象、すなわち充足のグラフ、コードの集合、環境の塔、次の段階 `Lset (sucV c)` を `K` に入れます。連鎖 `c ∈ p ∈ lam` と `lam` の推移性によって、まず `c` が `lam` に属することが分かり、妥当性の証人を使えるようになります。

```agda
    sup : (c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ p ⟩ → Supply K c oc
    sup c oc c∈ = w .snd .snd .fst , ( w .snd .fst , ( w .snd .snd .snd , Lset∈K (sucV c) (succ c c∈λ) ))
      where
      c∈λ : ⟨ c ∈ lam ⟩
      c∈λ = tr p c p∈λ c∈
```

それぞれの `c` の証人は妥当性のデータから読まれ、順序数のすべての要素のための供給が閉じられます。

```agda
      w = wit c c∈λ oc
```

内側の論理式はここで `E` において成り立ちます。pins の書き補題が数項の連言項を与えます。階層の連言項については、`hier-complete` が `p` の順序数性、候補となる値と `Lset p` の反射的な同一視、`hierL-spec` が与える正確な階層表、そして妥当性から上で各行について導いた供給を用います。ここでは強化された段階仮定を使いません。

```agda
    hm : ⟨ E ⊨ inner ⟩
    hm = inner-in E (PinsRead.pins-in N14 E tg)
           (HierRead.hier-complete aa pp ff zz N14 E tg op refl (hierL-spec p (At.cL p op) op) sup)
```

`p` における妥当性の証人は、実際の階層表 `F` の基礎集合を共通の境界集合 `K` に入れます。これにより、`F` を最も外側の有界な証人として導入するために必要な所属の証拠が得られます。

```agda
    FK : ⟨ fst F ∈ K ⟩
    FK = wit p p∈λ op .fst
```

残る仕事は、階層表と数項のデータを十一個の有界存在量化子の内側へ隠すことです。最も外側の導入には実際の階層表 `F` を用い、その `K` への所属は直前に示しました。続く二回の導入には数項 `9` と `8` を用い、それぞれが同じ共通の境界に属するという証拠を添えます。

```agda
    h3 : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ three ⟩
    h3 =
      wrap-in s4 (aS ∷ pS ∷ zS ∷ []) F FK (
      wrap-in s5 (F ∷ aS ∷ pS ∷ zS ∷ []) (nn 9) (num∈K 9) (
      wrap-in s6 (nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 8) (num∈K 8) (
```

同じ導入規則によって数項 `7` から `3` までを挿入します。それらの所属証明はすべて `num∈K` から得られるので、各量化子の証人は `K = Lset lam` の内部にあります。周囲で非有界な探索を行って証人を得ているわけではありません。

```agda
      wrap-in s7 (nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 7) (num∈K 7) (
      wrap-in s8 (nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 6) (num∈K 6) (
      wrap-in s9 (nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 5) (num∈K 5) (
      wrap-in s10 (nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 4) (num∈K 4) (
      wrap-in s11 (nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 3) (num∈K 3) (
```

最後に数項 `2`、`1`、`0` を挿入します。最後の導入後に得られる拡張環境はちょうど `E` であり、そこで `hm` がすでに `inner` を証明しています。したがって、入れ子になった導入によって、十一回包まれた論理式が表に残る三つ組 `(Lset p,p,Lset lam)` で満たされることが示されます。

```agda
      wrap-in s12 (nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 2) (num∈K 2) (
      wrap-in s13 (nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 1) (num∈K 1) (
      wrap-in inner (nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 0) (num∈K 0)
        hm))))))))))
```

消去の逆等式は、`erased` を構成可能な定数域へ埋め込むと `three` が復元されることを述べます。したがって、その等式の逆向きに `h3` を輸送すれば、同じ三スロットの環境における `embed erased` の充足が得られます。変わるのは定数域だけであり、十一個の有界証人とその共通の境界は、すでに構成したもののままです。

```agda
    hφ : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ embed erased ⟩
    hφ = subst (λ ψ → ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ ψ ⟩) (sym (Cnt.erase-inv three count-three)) h3
```

完全性は二つの連言項から組み立てられます。順序数性の原子は `ord-in` によって成り立ち、消去後の証人の論理式は証明されたばかりの輸送によって成り立ちます。読みの補題が両方を周囲の充足の中へ移します。

```agda
    complete : ⟨ (Lset p ∷ p ∷ Lset lam ∷ []) ⊨ₚ levelFo ⟩
    complete = subst ⟨_⟩ (read Δ₀-levelFo (aS ∷ pS ∷ zS ∷ [])) (ord-in aS pS zS op , hφ)
```

完全性定理は、ここで得られる存在方向を正確に述べます。`γ` が十分で順序数 `p` を含むなら、三つ組 `(Lset p,p,Lset γ)` は `levelFo` を満たします。後の `CondensationTransfer` では、この Δ₀ の核の外側に非有界存在量化子を加え、三つの座標すべてを初等性によって移し、健全性を用いて移された第一座標を対応する構成可能な段階として認識します。この定理は、任意の第三座標が使えるとも、第三座標が論理式によって一意に定まるとも主張しません。

```agda
level-complete : (γ : V ℓ) → Adequate γ → (p : V ℓ) → IsOrd p → ⟨ p ∈ γ ⟩
               → ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩
level-complete γ ad p op p∈ = Complete.complete γ ad p op p∈
```