---
title: "包とその崩壊を L の内部に置く"
module: L.GCH.ConstructibleHull
lang: ja
site: "Bedrock"
description: "包とその崩壊を L の内部に置く"
stage: "GCH の証明"
reading_order: 116
canonical: https://bedrock.institute/ja/L.GCH.ConstructibleHull.html
html: L.GCH.ConstructibleHull.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/ConstructibleHull.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.Renaming, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Presentation, V.Coding, V.Collapse, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Infinity, L.Axioms.Numerals, L.Recursion, L.Recursion.Graph, L.Definability, L.Coding.Model, L.Coding.Expressions, L.Coding.Environment, L.Coding.EnvironmentSet, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.CodeConstructibility, L.Coding.UniformSatisfaction, L.Choice.CanonicalNames, L.Choice.NameComparison, L.Choice.InternalWellOrder, L.Choice.StageOrders, L.WellOrder.Base, L.GCH.CardinalSquareLaw, L.GCH.OrderType, L.GCH.OmegaRecursion, L.GCH.SkolemHull, L.InjectionComposition, L.GCH.AdequateStages, L.Coding.SatisfactionGraphSet, L.GCH.CondensationTransfer, V.Model]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.ConstructibleHull.md, https://bedrock.institute/zh/L.GCH.ConstructibleHull.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 包とその崩壊を L の内部に置く

凝縮の議論には、外の包だけでは足りません。包そのものと、崩壊の各値が `L` に属する必要があります。本章は、崩壊を符号化し、包を ω 反復として表すことで、これらの所属の事実を証明します。

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

本章は古典論理のもとで進みます。モデル自身のレベルの後続での排中律の実例を使います。これは選択の構成が帯びるのと同じ仮定であり、ここで仮定される古典的な事実はこれだけです。

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

モジュールはこの仮定をパラメータとします。したがって以下の主張はすべてそれに相対的であり、漠然とした排中律の原理に訴えるものではありません。

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

本章は集合論の一階言語で語ります。論理式は構成可能な構造の台の上で組み立てられ、その定数は `L` の要素を名指します。定数は任意の対応に沿って改名でき、充足は改名で変わります。これが、崩壊と包を記述するための語彙です。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ⊥̇ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
```

論理式の読みは、改名によって環境の間を移動します。改名は充足にとって無害です。周囲の階層は、所属に沿う帰納、集合の外延性、そして「要素＝添字とその所属の証明」という提示の仕方という、背景の事実を供給します。

```agda
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Presentation {ℓ} using ( member; fiber )
```

議論は、`L` のすべての集合の住む場所からはじまります。順序数で添字づけられた段階の塔です。集合の崩壊はその要素だけから計算され、構成可能性は所属に沿って伝わります。示すべきは、この局所的な計算が `L` の外に出ないことです。包は推移的ではないので、議論は崩壊についての大域的な事実を使えず、段階ごとに、値が内側にとどまることを改めて導きます。

```agda
open import V.Coding {ℓ} using ( pr; module VCode )
open import V.Collapse {ℓ} using ( module Collapse )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-out; Lset→isL; 𝒟ₒ; 𝒟ₒ∋⊆
        ; Lset-layer; layer-trans )
```

構成可能集合 `ωʟ` は周囲の `ω` を表し、その仕様は要素を内部の数項と同定します。後では分出によって有界な切片と一段階の閉包を切り出します。どちらの演算も、結果が再び `L` の要素です。それが、構成全体を、その記述対象の宇宙の内側に保つのです。

```agda
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )
```

置換が値を表へ集めます。グラフが定義可能な再帰は `L` の要素となり、各入力で一意な値が「単に存在する」だけで十分です。定義可能性が論理式の定数を解釈し、モデル側の対と数項の符号化が、項目とその名前を供給します。

```agda
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to RecursionGraph )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate; consAtL; consAtL-adequate )
```

環境はパラメータのベクトルを一つの集合として符号化し、ベクトルはそこから復元されます。充足の橋は内部の充足を外側で読み、符号の集合がすべての符号を `L` の一つの要素に集め、構成可能な合併が、構成が途中で集めた部分を結合します。

```agda
open import L.Coding.Environment {ℓ} using ( env; cons )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envS; Ix; envOver; module Recover )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( graph; envFor; envFor-graph )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; keyS; key∈AllCodes )
open import L.Coding.CodeConstructibility {ℓ} using ( cupʟ; cupʟ-inl; cupʟ-inr )
```

一様な充足の表は、すべての符号にその充足集合を割り当て、外側で読めます。正準名の構成は、数項と、定数を持たない論理式のコードを `Lset ω` に置きます。そのような論理式にも自由変数の枠は残りえます。段階の内部の整列順序は要素を、まず誕生の段階、つぎに名前で比較します。

```agda
open import L.Coding.UniformSatisfaction {ℓ} lem using ( val-sat )
open import L.Choice.CanonicalNames {ℓ} lem using ( limitCode; numeral∈limit; pr∈limit )
open import L.Choice.NameComparison {ℓ} lem using ( freeCode-in; freeCode-out )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf )
```

狭義の整列順序の上の最小元の探索は、住民のある族から最小元を返します。関係そのものも、二つの読みをもつ対の集合になり、順序型の章が、崩壊の表を記述する三つの述語を述べます。

```agda
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; leastOf; isPropLeastOf )
  renaming ( Tri to Tri∙; lt to tri-lt; eq to tri-eq; gt to tri-gt )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( module Relation; isL-ord )
open import L.GCH.OrderType {ℓ} lem
```

正しさ、入力での完備さ、値の条項は、それぞれ二つの充足の読みをもつ論理式です。内部 ω 再帰は、モデル自身の `ω` に沿って、定義可能な二項のステップを反復します。包の要素は、任意の入れ子の深さの符号に名指されるので、一度の分離で包を作ることはできません。`ω` に沿って、定義可能な一段階の閉包を反復することではじめて届きます。閉包を ω 回作らねばならない理由はこれです。

```agda
  using ( Holds; Complete; Src; ValueIs; Correct
        ; completeAt; complete-in; complete-out
        ; valueAt; value-in; value-out
        ; correctAt; correct-in; correct-out )
open import L.GCH.OmegaRecursion {ℓ} lem using ( module Iterate )
```

証明は結びついた二つの部分からなります。まず局所的な崩壊表により、構成可能な台の各崩壊値が構成可能であることを示します。次に Skolem 包を有限閉包段階の合併として実現し、台自身の構成可能性を得て、第一の議論を適用します。

```agda
open import L.GCH.SkolemHull {ℓ} lem using ( module HullStage; module Frame )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.CondensationTransfer {ℓ} lem using ( module Condense )
```

入れ子になった包の符号には有限の深さがあり、パラメータ符号の深さの最大値から計算されます。この深さが、その値の現れる閉包段階を上から評価します。

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Nat.Properties using ( max )
open import Cubical.Data.Nat.Order using ( _≤_; left-≤-max; right-≤-max )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
```

有限パラメータベクトルにより、一つの証人符号は有限個の先行する値に依存できます。空集合、単集合、非順序対から、これらのパラメータとその順序対を階層内で表す集合符号を作れます。

```agda
import Cubical.Data.Empty as Empty
open import Cubical.Foundations.Prelude using ( subst2; J )
open import Cubical.Data.Vec using ( Vec; _∷_; []; lookup )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⁅_,_⁆; ⁅_⁆s; module InfinitySet )
```

フォン・ノイマンの後者と数項により、有限閉包段階を `ω` の内部で整理します。非順序対は、グラフと環境に使う順序対を符号化する材料にもなります。

```agda
open import V.Model {ℓ} using ( pair-spec )
open InfinitySet {ℓ} using ( ω; sucV; #_ )
open import Cubical.Foundations.HLevels
  using ( isPropΣ; isPropΠ; isPropΠ2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

存在の主張は、その証人を別の命題の証明にだけ使う段階まで命題的切断のまま保ちます。累積階層の等式は命題なので、崩壊の議論では集合の等式を示す際にこの切断されたデータを除去できます。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
```

二つの所属を区別する必要があります。外側の所属は累積階層の関係です。一方、構成可能な台の要素は外側の集合とその構成可能性の証明を組にし、台上の所属はその基底集合を通して読まれます。

```agda
open hPropStructure 𝒮ᵥ
module CS = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
```

定数が `L` の要素である論理式について、`⊨` は `L` のクラスモデルでの充足を表します。恒等写像による定数の付け替えは、環境も充足も変えません。

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

`i0` から `i6` までの七つの名前が、最初の七つの de Bruijn 添字を略記します。長い環境の枠ごとに一つです。

```agda
private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0
```

各後続添字は直前の添字をより大きな有限型へ移します。名前は枠ごとに続きます。

```agda
  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
```

これらは自由変数の位置であり、後の束縛子が環境を拡張すると読み方が移動します。

```agda
  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5
```

台の要素はその基礎の集合で決まります。構成可能性が命題だからです。基礎の集合が等しい台の要素は等しく、補助 `S≡` が、同じ基礎の集合から台の要素を組み立て直す場所で、その同定を行います。

```agda
  S≡ : {x y : CS.S} → fst x ≡ fst y → x ≡ y
  S≡ = Σ≡Prop (λ v → snd (isL v))
```

改名 `ρs` は二つの枠を入れ替えます。入れ替えた順で書かれた、ある対についての論理式を、元の順で読むためのものです。ステップの論理式を一方の枠の順で証明し、別の順で使うときに使われます。

```agda
  ρs : Fin 2 → Fin 2
  ρs zero = suc zero
  ρs (suc zero) = zero
```

改名 `ρf` は `w` を第零スロットに保ち、`Z` を第一スロットから第二スロットへ送り、次段階の候補 `Z'` が占める中央のスロットを飛ばします。

```agda
  ρf : Fin 2 → Fin 3
  ρf zero = zero
  ρf (suc zero) = suc (suc zero)
```

`ρs` の一致は、入れ替えた環境が、動いた枠で元の環境と同じ要素を載せていると言います。どちらの場合も反射性で証明できます。各枠が、同じ要素のある位置へ送られるからです。

```agda
  ags : (Z'' w : CS.S) → Ren.Agrees ρs (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ [])
  ags Z'' w zero = refl
  ags Z'' w (suc zero) = refl
```

任意の構成可能な台 `M` を固定します。

```agda
  agf : (w Z' Z : CS.S) → Ren.Agrees ρf (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ [])
  agf w Z' Z zero = refl
  agf w Z' Z (suc zero) = refl
```

## 構成可能な台の崩壊は L にとどまる

崩壊の議論が使うのは `M` の構成可能性と、その内部に残る先行者だけであり、推移性は仮定しません。

```agda
module PiIn (Mʟ : CS.S) where
```

選んだ構成可能な台の基底集合を `M` とします。付随する証明により、後に `M` から持ち上げる各要素が構成可能であることが保証されます。

```agda
  M : S
  M = fst Mʟ
```

`π x` は、`x` の要素のうち `M` にも属するものの崩壊値から作られ、`πX` は `x ∈ M` に対する値 `π x` を集めます。この制限された先行者関係により、`M` の推移性を仮定せずに定義できます。

```agda
  module C = Collapse M using ( Fiber; π; π-compute; πX; πX-member; π∈-fwd )
```

構成可能性は要素へ受け継がれるので、各 `y ∈ M` は構成可能です。したがって `y` をその証明と組にし、構成可能な台の要素として扱えます。

```agda
  memL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL y ⟩
  memL y y∈M = isL-trans {x = M} {y = y} y∈M (snd Mʟ)
```

持ち上げ `up` は、要素を台の要素としてまとめます。最初の補題は、崩壊値を外向きに読みます。`π x` の要素はどれも、`x` の、`M` に属する要素の崩壊です。これは崩壊の計算の条項、すなわち「`π x` は `x` の `M` の中の要素の上の崩壊の像に等しい」という恒等式から従います。

```agda
  up : (y : S) → ⟨ y ∈ˢ M ⟩ → CS.S
  up y y∈M = y , memL y y∈M
  π-mem-out : (x w : S) → ⟨ w ∈ˢ C.π x ⟩
            → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) ∥₁
  π-mem-out x w w∈ = PT.map mk (subst (λ u → ⟨ w ∈ˢ u ⟩) (C.π-compute x) w∈)
```

この変換は、崩壊自身のファイバーの証人を、要素についての主張へ変えます。ファイバーは、提示された添字と、「提示された要素の崩壊が `w` に等しい」証明を組にします。提示された要素は、崩壊が取られる `x` の要素です。

```agda
    where
    mk : Σ[ p ∈ C.Fiber x ] (C.π (⟪ x ⟫↪ (p .fst)) ≡ w)
       → Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w))
    mk (p , q) = ⟪ x ⟫↪ (p .fst)
               , ( member x (p .fst)
```

`M` の所属関係は三つの自由変数スロットで表され、`Relation` により環境 `y ∷ x ∷ e ∷ []` で読まれます。第三スロットは符号化された対を載せ、論理式は `y ∈ M`、`x ∈ M`、`y ∈ x` を主張します。

```agda
                 , ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = M} .snd (p .snd)
                 , q )
  private
    module Membership = Relation Mʟ Mʟ
      ((var i1 ∈̇ con Mʟ) ∧̇ ((var i0 ∈̇ con Mʟ) ∧̇ (var i1 ∈̇ var i0)))
```

関係のホスト側の読みは、三つの所属の連言そのものです。この妥当性があるから、対象言語の論理式と外側の主張は互いに代わり合えます。

```agda
      (λ y x → (fst y ∈ˢ M) ⊓ ((fst x ∈ˢ M) ⊓ (fst y ∈ˢ fst x)))
      (λ y x z h → h) (λ y x z h → h)
```

関係はモデルの要素になります。台の要素の対からなる集合で、二つの読み出しによって導入と消去ができます。関係が台で界されているので、対の集合は分離で切り出せるほど小さいのです。

```agda
  R : CS.S
  R = Membership.rel
```

導入の読み出しは、両端の所属と、その間の所属を示します。それがこの対での関係の内容です。

```agda
  R-in : (y x : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst x ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst x ⟩
       → Holds R y x
  R-in y x my mx yx = Membership.into y x my mx (my , mx , yx)
```

消去の読み出しは、同じ三つの所属を返します。二方向合わせて、この関係が妥当であること、ホスト側の主張よりも強くも弱くもないことが分かります。

```agda
  R-out : (y x : CS.S) → Holds R y x
        → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst x ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst x ⟩
  R-out = Membership.pair-out
```

崩壊の論理式は、値と実引数の枠の上に立ち、大域的ではなく局所的です。こう言います。関係 `R` に対して正しく、実引数で完備であり、そこでの値が与えられた値であるような表 `F` が、単に存在する、と。一つの大域的な関数のグラフを主張するのではなく、各実引数でそのような表の存在だけを述べるのです。だからこの論理式は、推移的でない台の上でも成立します。

```agda
  opaque
    piFo : Formula CS.S 2
    piFo = ∃̇ ( correctAt i0 R
             ∧̇ ( completeAt i0 R i2 ∧̇ valueAt i0 R i2 i1 ) )
```

論理式の外向きの読み出しは、充足を三つの成分にほどきます。正しい表、実引数での完備さ、値の条項です。それぞれの連言項が、順序型の章自身の射影によって束縛子の外へ運ばれます。

```agda
    piFo-out : (v p : CS.S) → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
             → ∥ Σ[ F ∈ CS.S ] (Correct F R × (Complete F R p × ValueIs F R p v)) ∥₁
    piFo-out v p = PT.map (λ { (F , (hc , (hm , hv))) → F
      , ( correct-out i0 R (F ∷ v ∷ p ∷ []) hc
        , ( complete-out i0 R i2 (F ∷ v ∷ p ∷ []) hm
```

最も内側の射影がほどきを終えます。値の条項は、実引数での表の項目についての通常の主張として届きます。

```agda
          , value-out i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) })
```

内向きの読みでは、存在量化の証人として表 `F` を選び、その正しさ、入力での完全性、値の条項の証明を与えます。外向きの読みと合わせると、この論理式は意図した内容と正確に対応します。

```agda
    piFo-in : (v p F : CS.S) → Correct F R → Complete F R p → ValueIs F R p v
            → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
    piFo-in v p F hc hm hv = ∣ F
      , ( correct-in i0 R (F ∷ v ∷ p ∷ []) hc
        , ( complete-in i0 R i2 (F ∷ v ∷ p ∷ []) hm
```

一意性は、所属に沿う帰納が一回で証明します。動機はこう言います。台の構成可能な要素 `x` のそれぞれで、その関係に対して正しく `x` で完備な表は、`x` の崩壊を値として割り当てる、と。構成可能性も所属も、表の項目が台の要素の対であるために、動機とともに運ばれます。

```agda
          , value-in i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) ∣₁
  private
    Pv : CS.S → S → Type (ℓ-suc ℓ)
    Pv F x = (xL : ⟨ isL x ⟩) → ⟨ x ∈ˢ M ⟩ → (v : CS.S)
           → Complete F R (x , xL) → ValueIs F R (x , xL) v → fst v ≡ C.π x
```

帰納は、周囲の階層の所属に沿って走ります。崩壊そのものがそうやって定義されているからです。`x` での動機を証明するには、`x` のすべての要素での動機を証明します。

```agda
  value-val′ : (F : CS.S) → Correct F R → (x : S) → Pv F x
  value-val′ F hc = ∈-induction {P = Pv F} go
    where
    go : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → Pv F y) → Pv F x
    go x IH xL x∈M v cmp val =
```

ステップは要素を比較します。記録された値と崩壊は同じ要素をもち、周囲の階層の外延性がそれを等しさへ変えます。入力は台の要素として提示されるので、その項目は台の上で型づけられます。

```agda
      extensionalV {a = fst v} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w))
      where
      xS : CS.S
      xS = x , xL
```

前向き：記録された値の要素 `w` を台に載せ、値の条項が、関係の項目と、そこの表の項目を作ります。載せるとき、記録された値から受け継いだ構成可能性を `w` とともに包みます。

```agda
      fwd : (w : S) → ⟨ w ∈ˢ fst v ⟩ → ⟨ w ∈ˢ C.π x ⟩
      fwd w w∈ = PT.rec (snd (w ∈ˢ C.π x)) read (val wS .fst w∈)
        where
        wS : CS.S
        wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)
```

源の証人は関係の事実 `ry` と表の項目 `fy` に分かれます。`ry` から `y ∈ M` と `y ∈ x` を読み、`fy` に帰納法の仮定を適用して `w` を `π y` と同定し、`π∈-fwd` によって `w` を `π x` に入れます。

```agda
        read : Σ[ y ∈ CS.S ] (Holds R y xS × Holds F y wS) → ⟨ w ∈ˢ C.π x ⟩
        read (y , (ry , fy)) =
          subst (λ t → ⟨ t ∈ˢ C.π x ⟩) e (C.π∈-fwd x (fst y) y∈x y∈M)
          where
          y∈M : ⟨ fst y ∈ˢ M ⟩
```

関係の項目はさらに、その成分が入力の下にあるとも言い、これが帰納の仮定を解き放ちます。その成分での表の値は成分の崩壊に等しい、と。この等式を崩壊の読み出しと合成すれば、`w` の同定が終わります。

```agda
          y∈M = R-out y xS ry .fst
          y∈x : ⟨ fst y ∈ˢ x ⟩
          y∈x = R-out y xS ry .snd .snd
          e : C.π (fst y) ≡ w
          e = sym (IH (fst y) y∈x (snd y) y∈M wS (hc y wS fy .fst) (hc y wS fy .snd))
```

後ろ向き：崩壊の要素 `w` は、すでに証明した外向きの読みによって、台の中の入力の成分へと分解され、その成分の崩壊が `w` になります。元の実引数 `x` における表の完備さを前者 `y` に適用すると、項目 `(y,u)` が得られます。

```agda
      bwd : (w : S) → ⟨ w ∈ˢ C.π x ⟩ → ⟨ w ∈ˢ fst v ⟩
      bwd w w∈ = PT.rec (snd (w ∈ˢ fst v)) read (π-mem-out x w w∈)
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst v ⟩
        read (y , (y∈x , y∈M , e)) = PT.rec (snd (w ∈ˢ fst v)) inner (cmp yS ry)
```

その成分は台の要素として載せられ、対での関係の項目が、二つの所属とその間の所属から改めて導入されます。

```agda
          where
          yS : CS.S
          yS = up y y∈M
          ry : Holds R yS xS
          ry = R-in yS xS y∈M x∈M y∈x
```

帰納法の仮定が `u` を `π y` と同定し、`π y = w` に沿って輸送すると、`w` が記録された値に属することが従います。後ろ向きの方向が主張するのはこれです。

```agda
          inner : Σ[ u ∈ CS.S ] Holds F yS u → ⟨ w ∈ˢ fst v ⟩
          inner (u , fu) =
            subst (λ t → ⟨ t ∈ˢ fst v ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁)
            where
            eu : fst u ≡ C.π y
```

等式 `eu` は、成分 `y` での帰納の仮定です。表の `y` での値は `y` の崩壊に等しい、というものです。分解が携える等式と合成すれば、項目の値は `w` と同一視され、後ろ向きの方向が置こうとしていたのはまさにこれです。

```agda
            eu = IH y y∈x (snd yS) y∈M u (hc yS u fu .fst) (hc yS u fu .snd)
```

台の要素の基礎集合に帰納を適用すると、制限された構造で同じ一意性の主張が得られます。得られる決定補題は、崩壊の論理式が `M` の要素で成立するなら、その値はその要素の崩壊に等しいことを述べます。

```agda
  value-val : (F : CS.S) → Correct F R → (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → (v : CS.S)
            → Complete F R x → ValueIs F R x v → fst v ≡ C.π (fst x)
  value-val F hc x = value-val′ F hc (fst x) (snd x)
  piFo-val : (q : CS.S) → ⟨ fst q ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩
           → fst v ≡ C.π (fst q)
```

証明は、切り詰められた存在を二つの h-集合の等しさという命題へ消去し、外向きの読み出しが手渡す正しい表に、今証明した一意性を適用します。次の構成では、`L` の与えられた要素の内側にある要素を台から切り出します。

```agda
  piFo-val q mq v h = PT.rec (setIsSet (fst v) (C.π (fst q)))
    (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv })
    (piFo-out v q h)
  module Cut (K : CS.S) where
```

切り出しの論理式はただ一つの原子論理式です。自由な枠が定数 `K` の要素であることを表します。スライスが収めるのは、これを満たす要素だけです。

```agda
    cutFo : Formula CS.S 1
    cutFo = var i0 ∈̇ con K
```

分離を `Mʟ` に適用することで、スライスも `L` の要素として得られ、単なる要素の類では終わりません。このため、スライスを内部再帰の定義域として使えます。

```agda
    opaque
      cut : CS.S
      cut = hasSeparationL Mʟ cutFo .fst .fst
```

所属の仕様は、スライスへの所属を、台への所属と切り出しの論理式の充足とを合わせたものとして同定します。後者はほどけば、`K` の基礎の集合の中にあることにほかなりません。

```agda
      cut-mem : (y : CS.S) → (y CS.∈ˢ cut) ≡ ((y CS.∈ˢ Mʟ) ⊓ ((y ∷ []) ⊨ cutFo))
      cut-mem = hasSeparationL Mʟ cutFo .fst .snd
```

内向きの方向は、`M` への所属と `K` の基礎集合への所属を組み合わせ、載せた要素をスライスに入れます。

```agda
      cut-in : (y : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst K ⟩ → ⟨ y CS.∈ˢ cut ⟩
      cut-in y my yK = subst ⟨_⟩ (sym (cut-mem y)) (my , yK)
```

外向きの方向は、同じ仕様を二つの成分へ読み戻します。台の要素 `q` が段階 `δ` で「良い」とは、その段階に属するとき、崩壊の構成可能な表示と `q` における崩壊の論理式の両方が得られることです。

```agda
      cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst K ⟩
      cut-out y h = subst ⟨_⟩ (cut-mem y) h
  Good : S → S → Type (ℓ-suc ℓ)
  Good δ q = ⟨ q ∈ˢ M ⟩ → ⟨ q ∈ˢ Lset δ ⟩
           → Σ[ qL ∈ ⟨ isL (C.π q) ⟩ ] ((mq : ⟨ q ∈ˢ M ⟩)
```

「良いこと」の第二成分は、構成可能性の証明によって崩壊を `𝒮ʟ` の要素として包み、その値と選んだ `M` の要素の表示について崩壊の論理式が成立することを述べます。

```agda
                → ⟨ ((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo ⟩)
```

「良いこと」は命題です。台への所属も、段階への所属も、構成可能性も充足も、それぞれ命題だからです。ここが大切です。段階の分解が返すのは、単に存在するだけの証人ですが、命題である「良いこと」なら、証人を選ぶことなく消費できるのです。

```agda
  isPropGood : (δ q : S) → isProp (Good δ q)
  isPropGood δ q = isPropΠ2 λ _ _ → isPropΣ (snd (isL (C.π q)))
    λ qL → isPropΠ λ mq → snd (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo)
```

順序数段階 `δ'` を固定し、`M` と `Lset δ'` の両方に属する各 `q` が「良い」と仮定します。これら先行する崩壊値を組み合わせて、次の入力での値を作ります。

```agda
  module Step (δ' : S) (oδ' : IsOrd δ')
              (IH : (q : S) → Good δ' q) where
```

スライスは、段階 `Lset δ'` で切り出されます。その段階がすでに収めている台の要素です。段階は `L` の集合なので、スライスは分離によって `L` の要素になり、これこそ帰納の仮定が語る定義域です。

```agda
    module Sl = Cut (LsetS δ' oδ') using ( cut; cut-in; cut-out )
```

段階は推移的です。したがって、段階の要素の要素も段階の内側にあり、この事実が後で表の条件をより小さい入力へ制限します。帰納の仮定により、スライスの要素の崩壊は `𝒮ʟ` の要素として得られ、その構成可能性の証明が「良いこと」の第一成分です。

```agda
    Lδ'-trans : {x y : S} → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ Lset δ' ⟩ → ⟨ y ∈ˢ Lset δ' ⟩
    Lδ'-trans {x} {y} = layer-trans (Lset-layer δ') {x = x} {y = y}
    πʟ : (y : CS.S) → ⟨ y CS.∈ˢ Sl.cut ⟩ → CS.S
    πʟ y hy = C.π (fst y) , IH (fst y) (Sl.cut-out y hy .fst) (Sl.cut-out y hy .snd) .fst
```

崩壊の論理式が、その崩壊と要素の対の上で成立するのも、同じ帰納の仮定によります。「良いこと」の第二成分はちょうど、この対での論理式の充足であり、要素とその基礎の集合の同定に沿って運ばれます。

```agda
    πʟ-graph : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩)
             → ⟨ (πʟ y hy ∷ y ∷ []) ⊨ piFo ⟩
    πʟ-graph y hy =
      subst (λ y' → ⟨ (πʟ y hy ∷ y' ∷ []) ⊨ piFo ⟩) (S≡ refl)
        (IH (fst y) my (Sl.cut-out y hy .snd) .snd my)
```

この同定には、スライスの仕様から読み出した要素の台への所属を使います。基礎集合は変わっておらず、構成可能性の証明は命題なので、この同一視に沿った輸送は一意に定まります。

```agda
      where
      my : ⟨ fst y ∈ˢ M ⟩
      my = Sl.cut-out y hy .fst
```

スライス上の崩壊値は、スライスを定義域、`piFo` をグラフの論理式とする内部再帰をなします。構成可能性によって各値は `𝒮ʟ` の要素となるので、グラフの項目は `𝒮ʟ` の要素の対です。

```agda
    private
      Rπ : Recursion
      Rπ = record
        { dom = Sl.cut ; graph = piFo
        ; funct = λ y hy → (πʟ y hy , πʟ-graph y hy)
```

関数性が成立するのは、崩壊の論理式が台のすべての要素でその値を決めるからです。同じ対で論理式を満たすほかの値はどれもそれと等しく、決定の補題がそれを読み出します。対応する `𝒮ʟ` の要素の等しさは、構成可能性の証明が命題値であることから従います。

```agda
            , λ { (v , h) → Σ≡Prop (λ w → snd ((w ∷ y ∷ []) ⊨ piFo))
                (sym (S≡ (piFo-val y (Sl.cut-out y hy .fst) v h))) } }
```

`L` のグラフの再帰が表を集めます。台の要素の対からなる集合で、その項目はスライス上の崩壊の記録にほかなりません。

```agda
      module T = RecursionGraph Rπ using ( F; F-in; pair-out )
```

集められた集合が、この段階での表です。`L` の要素であり、スライスの各要素と、その構成可能な崩壊とを対にします。

```agda
    Tab : CS.S
    Tab = T.F
```

表の内向きの読み出しは、その項目を示します。スライスの各要素で、要素とその崩壊の対が記録されます。

```agda
    Tab-in : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩) → Holds Tab y (πʟ y hy)
    Tab-in = T.F-in
```

外向きの読み出しは、項目をスライスの要素と、その基礎集合の崩壊に等しい値へ分解します。内向きの読み出しと合わせて、表が記録するのは崩壊そのものであり、歪みがないことが分かります。

```agda
    Tab-pair : (x v : CS.S) → Holds Tab x v
             → ⟨ x CS.∈ˢ Sl.cut ⟩ × (fst v ≡ C.π (fst x))
    Tab-pair = T.pair-out
```

引数 `x` が閉じているとは、`x` の要素であり、かつ `M` に属するものがすべて段階スライスに入ることです。この条件は引数ごとに課されます。ここでは `M` の推移性を仮定していません。

```agda
    Closed : CS.S → Type (ℓ-suc ℓ)
    Closed x = (y : S) (y∈x : ⟨ y ∈ˢ fst x ⟩) (y∈M : ⟨ y ∈ˢ M ⟩)
             → ⟨ up y y∈M CS.∈ˢ Sl.cut ⟩
```

スライスの要素は段階の推移性によって閉じています。その要素であり、かつ `M` に属するものは段階内にとどまるので、スライスに属します。

```agda
    slice-closed : (x : CS.S) → ⟨ x CS.∈ˢ Sl.cut ⟩ → Closed x
    slice-closed x hx y y∈x y∈M =
      Sl.cut-in (up y y∈M) y∈M (Lδ'-trans {x = fst x} {y = y} y∈x (Sl.cut-out x hx .snd))
```

閉じた入力に対する表の完備さとは、関係する各要素での表自身の項目の切り詰められた存在です。閉じていることがその要素をスライスの中へ置き、表がそこに崩壊を記録します。関係の項目は分解されて、その要素を名指します。

```agda
    complete-of : (x : CS.S) → Closed x → Complete Tab R x
    complete-of x cl y ry = ∣ πʟ y' hy' , subst (λ w → ⟨ pr w (C.π (fst y)) ∈ˢ fst Tab ⟩) refl (Tab-in y' hy') ∣₁
      where
      ro = R-out y x ry
      y' : CS.S
```

その要素は台の要素として載せられ、閉じていることが、載せられた要素をスライスの中へ置きます。これは、表が崩壊を記録したときの仮定そのものです。

```agda
      y' = up (fst y) (ro .fst)
      hy' : ⟨ y' CS.∈ˢ Sl.cut ⟩
      hy' = cl (fst y) (ro .snd .snd) (ro .fst)
```

閉じた入力に対して、値の条項は崩壊そのものについて成立します。証明には二方向あります。崩壊値の要素はどれも関係する要素から来ており、入力と関係する要素はどれも、表によって崩壊値の中へ運ばれます。

```agda
    valueIs-of : (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → Closed x → (v : CS.S) → fst v ≡ C.π (fst x)
               → ValueIs Tab R x v
    valueIs-of x mx cl v ev w = fwd , bwd
      where
      fwd : ⟨ fst w ∈ˢ fst v ⟩ → Src Tab R x w
```

前向きでは、候補の値 `v` の要素 `w` を、崩壊の読み出しによって台の中の入力の成分へ分解します。その成分の崩壊は `w` に等しくなります。分解は切り詰められた存在であり、消去の対象は命題です。

```agda
      fwd w∈ = PT.map read (π-mem-out (fst x) (fst w) (subst (λ t → ⟨ fst w ∈ˢ t ⟩) ev w∈))
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ fst x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ fst w))
             → Σ[ y ∈ CS.S ] (Holds R y x × Holds Tab y w)
        read (y , (y∈x , y∈M , e)) = up y y∈M
```

その成分を台の要素へ持ち上げます。入力への所属から関係の項目が得られ、表の項目はその崩壊と `w` の等式に沿って輸送されます。この二つを合わせると、必要な `Src Tab R x w` の証人になります。

```agda
          , ( R-in (up y y∈M) x y∈M mx y∈x
            , subst (λ t → ⟨ pr y t ∈ˢ fst Tab ⟩) e (Tab-in (up y y∈M) (cl y y∈x y∈M)) )
```

後ろ向き：`w` のソースの項目は、表の値が `w` であるような関係する要素を名指します。対の読み出しが項目を所属と等式に分け、崩壊の読み出しが `w` を第一成分の崩壊の中に置き、二つの等式がそれを記録された値へ運び戻します。

```agda
      bwd : Src Tab R x w → ⟨ fst w ∈ˢ fst v ⟩
      bwd = PT.rec (snd (fst w ∈ˢ fst v)) (λ { (y , (ry , ty)) →
        subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev)
          (C.π∈-fwd (fst x) (fst y) (R-out y x ry .snd .snd) (R-out y x ry .fst)) })
```

それぞれの項目での表の正しさは、その項目が名指すスライスの要素での二つの条項から組み立てられます。対の読み出しが、スライスへの所属と台への所属を与えます。

```agda
    Tab-correct : Correct Tab R
    Tab-correct x v hxv = complete-of x cl , valueIs-of x mx cl v (Tab-pair x v hxv .snd)
      where
      hx : ⟨ x CS.∈ˢ Sl.cut ⟩
      hx = Tab-pair x v hxv .fst
```

台への所属と閉じていることが仮定を完成させ、ステップのモジュールは、その要素がすべてより前の段階の下にあるような台の入力 `q` でパラメータづけられます。これは `Lset δ'` の定義可能冪集合の要素に必要な状況であり、ここでは閉じていることが `q⊆` から従います。

```agda
      mx : ⟨ fst x ∈ˢ M ⟩
      mx = Sl.cut-out x hx .fst
      cl : Closed x
      cl = slice-closed x hx
    module At (q : S) (mq : ⟨ q ∈ˢ M ⟩) (q⊆ : (y : S) → ⟨ y ∈ˢ q ⟩ → ⟨ y ∈ˢ Lset δ' ⟩) where
```

入力は台の要素として載せられ、環境の枠としても、対の第二成分としても働けるようになります。

```agda
      qS : CS.S
      qS = up q mq
```

載せた入力の閉じていることは仮定から成立します。台の中のその要素はすべてより前の段階の下にあり、スライスが受け入れます。そして台の中の入力の要素が、それ自身のスライスとして切り出されます。崩壊の値はこの定義域の上で計算されます。

```agda
      cl : Closed qS
      cl y y∈q y∈M = Sl.cut-in (up y y∈M) y∈M (q⊆ y y∈q)
      module Mq = Cut qS using ( cut; cut-in; cut-out )
```

`q` の崩壊値は、内部の再帰として作られます。定義域は台の中の `q` の要素のスライス、グラフは崩壊の論理式です。したがって、この関数的グラフは `L` における置換の仮定を満たします。

```agda
      private
        valR : Recursion
        valR = record
          { dom   = Mq.cut
          ; graph = piFo
```

関数性は `mereFunct` を通して組み立てられます。各入力で、一意な値が「単に存在する」ことからです。証人 `wit` は、そのような値と、その充足と一意性とを、切り詰めの内側で産出します。台の要素での崩壊の論理式の一意性が命題だからです。

```agda
          ; funct = λ y hy → mereFunct piFo y (wit y hy) }
          where
          wit : (y : CS.S) (hy : ⟨ y CS.∈ˢ Mq.cut ⟩)
              → ∥ Σ[ v ∈ CS.S ] (⟨ (v ∷ y ∷ []) ⊨ piFo ⟩
                                × ((v' : CS.S) → ⟨ (v' ∷ y ∷ []) ⊨ piFo ⟩ → v' ≡ v)) ∥₁
```

証人は大域的な崩壊値 `C.π (fst y)` であり、帰納の仮定によって構成可能なものとして表示されます。段階スライス上の表が `piFo` の証明を与え、`piFo-val` が一意性を与えます。

```agda
          wit y hy = ∣ πʟ y hy'
            , ( πʟ-graph y hy'
              , λ v' hv' → S≡ (piFo-val y my v' hv') ) ∣₁
            where
            my : ⟨ fst y ∈ˢ M ⟩
```

`y` の台への所属は `q` のスライスから来ます。仮定により `q` の各要素は `Lset δ'` に入るので、そのうち台に属する要素はすべて段階スライスに入ります。

```agda
            my = Mq.cut-out y hy .fst
            hy' : ⟨ y CS.∈ˢ Sl.cut ⟩
            hy' = Sl.cut-in y my (q⊆ (fst y) (Mq.cut-out y hy .snd))
```

置換はこの再帰の値を `L` の要素として集めます。その要素はちょうど、`q` の要素であり、かつ `M` に属するものの構成可能な崩壊値です。

```agda
        module Vq = Of valR using ( table; table-in; table-out )
```

表の基礎の集合は、`q` の崩壊と一致します。要素ごとの同値を通して外延性で証明されます。前向き：表の要素は、台の中の `q` のある要素 `y` での値であり、消去の対象は「`w` が `q` の崩壊に属する」という命題です。

```agda
      val≡π : fst Vq.table ≡ C.π q
      val≡π = extensionalV {a = fst Vq.table} {b = C.π q} (λ w → ⇔toPath (fwd w) (bwd w))
        where
        fwd : (w : S) → ⟨ w ∈ˢ fst Vq.table ⟩ → ⟨ w ∈ˢ C.π q ⟩
        fwd w hw = PT.rec (snd (w ∈ˢ C.π q))
```

外向きの読み出しが要素 `y` とその値を名指し、決定の補題がその値を `y` の崩壊と同一視し、崩壊の読み出しが `y` の崩壊を `q` の崩壊の中へ置きます。輸送がこの二つを合成します。

```agda
          (λ { (y , (hy , h)) →
             subst (λ t → ⟨ t ∈ˢ C.π q ⟩)
               (sym (piFo-val y (Mq.cut-out y hy .fst) wS h))
               (C.π∈-fwd q (fst y) (Mq.cut-out y hy .snd) (Mq.cut-out y hy .fst)) })
          (Vq.table-out wS hw)
```

`w` は構成可能な値集合 `Vq.table` に属するので、`L` の推移性から `w` の構成可能性が得られ、`𝒮ʟ` の要素として表示できます。

```agda
          where
          wS : CS.S
          wS = w , isL-trans {x = fst Vq.table} {y = w} hw (snd Vq.table)
```

後ろ向き：`q` の崩壊の要素は、台の中の `q` の成分へと分解され、その成分の崩壊がそれと等しくなります。これは、表が項目を記録する形そのものです。

```agda
        bwd : (w : S) → ⟨ w ∈ˢ C.π q ⟩ → ⟨ w ∈ˢ fst Vq.table ⟩
        bwd w hw = PT.rec (snd (w ∈ˢ fst Vq.table)) read (π-mem-out q w hw)
          where
          read : Σ[ y ∈ S ] (⟨ y ∈ˢ q ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst Vq.table ⟩
          read (y , (y∈q , y∈M , e)) =
```

等式が `w` を成分の崩壊へ運び、表の内向きの読み出しが、載せた成分での項目を作ります。そこに記録されるのはまさにその崩壊です。

```agda
            subst (λ t → ⟨ t ∈ˢ fst Vq.table ⟩) e
              (Vq.table-in yS (πʟ yS hy') hy (πʟ-graph yS hy'))
            where
            yS : CS.S
            yS = up y y∈M
```

載せた成分は、台への所属によって `q` のスライスの中にあり、また「`q` の要素はより前の段階の下にある」という仮定によって、段階のスライスの中にもあります。

```agda
            hy : ⟨ yS CS.∈ˢ Mq.cut ⟩
            hy = Mq.cut-in yS y∈M y∈q
            hy' : ⟨ yS CS.∈ˢ Sl.cut ⟩
            hy' = Sl.cut-in yS y∈M (q⊆ y y∈q)
```

`q` の崩壊は構成可能です。それは表の基礎の集合に等しく、表は `L` の要素なので、構成可能性がこの等式に沿って運ばれます。これが `q` での「良いこと」の最初の条項です。

```agda
      πq-isL : ⟨ isL (C.π q) ⟩
      πq-isL = subst (λ t → ⟨ isL t ⟩) val≡π (snd Vq.table)
```

「良いこと」の第二の条項は、崩壊と要素の対の上で崩壊の論理式が成立することです。表の正しさ、閉じた入力での完備さ、そして値を崩壊と同定する値の条項です。二つの条項がそろえば、段階の帰納を述べられます。すべての順序数での「良いこと」です。

帰納は、階層の所属に沿って走り、各ステップで、段階への所属の分解を消費します。

```agda
      good : (mq' : ⟨ q ∈ˢ M ⟩) → ⟨ ((C.π q , πq-isL) ∷ up q mq' ∷ []) ⊨ piFo ⟩
      good mq' = subst (λ q' → ⟨ ((C.π q , πq-isL) ∷ q' ∷ []) ⊨ piFo ⟩) (S≡ refl)
        (piFo-in (C.π q , πq-isL) qS Tab Tab-correct (complete-of qS cl)
          (valueIs-of qS mq cl (C.π q , πq-isL) refl))
  good-at : (δ : S) → IsOrd δ → (q : S) → Good δ q
```

`δ` での「良いこと」を証明するには、段階 `Lset δ` への `q` の所属を分解します。`q` は、より前の段階 `δ'` の定義可能冪集合の中にある、と。分解は「良いこと」へ消去されます。「良いこと」が命題だからです。

```agda
  good-at = ∈-induction {P = λ δ → IsOrd δ → (q : S) → Good δ q} go
    where
    go : (δ : S) → ((δ' : S) → ⟨ δ' ∈ˢ δ ⟩ → IsOrd δ' → (q : S) → Good δ' q)
       → IsOrd δ → (q : S) → Good δ q
    go δ IH oδ q mq q∈Lδ = PT.rec (isPropGood δ q) read (Lset-out δ q q∈Lδ) mq q∈Lδ
```

分解は、`δ` の下のより前の段階 `δ'` と、その定義可能冪集合への `q` の所属を名指します。`δ'` より下での「良いこと」を使うと、ステップの構成から `q` での「良いこと」が得られます。定義可能冪集合の条項はさらに、`q` のすべての要素が段階 `Lset δ'` の中にあると言います。これが、ステップが消費する閉じていることの仮定です。

```agda
      where
      read : Σ[ δ' ∈ S ] (⟨ δ' ∈ˢ δ ⟩ × ⟨ q ∈ˢ 𝒟ₒ (Lset δ') ⟩) → Good δ q
      read (δ' , (δ'∈δ , q∈𝒟)) _ _ = A.πq-isL , A.good
        where
        oδ' : IsOrd δ'
```

`δ' ∈ δ` から `δ'` の順序数性が得られます。`δ'` より下で帰納の仮定を使い、`q` のすべての要素が `Lset δ'` に属するという定義可能冪集合の事実を合わせると、`q` での「良いこと」が得られ、`good-at` の所属帰納が閉じます。また `M` 自身が `L` に属するので、その構成可能性の証明から `M` を含む段階が得られ、その段階の推移性によって `M` の各要素も段階内に入ります。

```agda
        oδ' = mem-ord {A = δ} oδ δ' δ'∈δ
        module A = Step.At δ' oδ' (IH δ' δ'∈δ oδ') q mq (λ y y∈q → 𝒟ₒ∋⊆ (Lset δ') q q∈𝒟 y y∈q)
          using ( πq-isL; good )
  π-isL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL (C.π y) ⟩
  π-isL y y∈M = PT.rec (snd (isL (C.π y)))
```

証明 `Mʟ` から構成可能な台 `M` を含む段階を取り、その段階での「良いこと」から `M` の各要素の崩壊が構成可能であることを得ます。続く主張は、崩壊像全体 `C.πX` の要素について同じ議論を始め、やはり切り詰められた表示を構成可能性へ消去します。

```agda
    (λ { (α , (oα , M∈Lα)) →
       good-at α oα y y∈M (layer-trans (Lset-layer α) {x = M} {y = y} y∈M M∈Lα) .fst })
    (snd Mʟ)
  πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩
  πX-isL x x∈πX = PT.rec (snd (isL x))
```

`πX-isL` の主張は要素についてのものです。

```agda
    (λ { (y , (y∈M , e)) → subst (λ w → ⟨ isL w ⟩) e (π-isL y y∈M) })
    (C.πX-member x x∈πX)
```

## Skolem 包を ω 反復として表す

崩壊像の各要素は台のどこかの要素の崩壊であり、だから構成可能です。これは、崩壊像が `L` に含まれると言っているだけです。像そのものが `L` の要素であるとは主張していません。前半が終わり、後半は新しいパラメータで始まります。要素の後者で閉じた段階 `lam` と、その要素がすべて段階の中にある始点 `X` です。

```agda
module Telescope (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
```

空集合も段階の中にあり、包の機構がこれらのデータの上で開かれます。包の台 `M`、包が段階に含まれること、そして始点のすべての要素が包の要素であることです。

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ
    using ( ∅∈Lsetα; hull-member; X⊆M; Hull⊆L )
  open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ public
```

包の符号は、`X` の要素に対する基底名か、無定数公式とそのパラメータの符号を保存する `wit k ψ cs` です。部分符号を評価した後、証人が存在するかどうかに応じて、最小の証人または廃棄値をその値とします。

```agda
    using ( Code; base; wit; val; vals; search; Sat; Hull; val-wit )
  open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ using ( inHull; _⊨₀_ )
```

小さな台 `SL` は、すべてが型づけられる、段階の要素を集めます。集合 `Z` から取ったパラメータのベクトルとは、各成分が `Z` の基礎の集合に属することです。ステップの探索はそのようなベクトルだけにわたります。

```agda
  SL : Type (ℓ-suc ℓ)
  SL = HullStage.ASt.SL lam ordλ succλ X X⊆L ∅∈λ
  From : {k : ℕ} → CS.S → Vec SL k → Type (ℓ-suc ℓ)
  From {k} Z vs = (i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ fst Z ⟩
  Searched : CS.S → S → Type (ℓ-suc ℓ)
```

探索にはアリティ `k+1` の無定数公式を使います。`Z` から取ったベクトルが `k` 個のパラメータ変数に値を与え、残る変数には候補となる証人を割り当てます。`Sat` はそのような証人の存在を表します。

```agda
  Searched Z z = Σ[ k ∈ ℕ ] Σ[ ψ ∈ Formula (⊥* {ℓ}) (suc k) ] Σ[ vs ∈ Vec SL k ]
                 Σ[ w ∈ Sat k ψ vs ] (From Z vs × (z ≡ fst (search k ψ vs w)))
  Reads : CS.S → S → Type (ℓ-suc ℓ)
  Reads Z z = ⟨ z ∈ˢ fst Z ⟩ ⊎ ((z ≡ ∅) ⊎ Searched Z z)
```

この構造は、演算 `Φ`、二変数公式 `ΦFo`、そして任意の `Z` について二つの変数に `Φ Z` と `Z` を割り当てた環境がその公式を満たすという証明を含みます。

```agda
  record StepPack : Type (ℓ-suc (ℓ-suc ℓ)) where
    field
      Φ       : CS.S → CS.S
      ΦFo     : Formula CS.S 2
      defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩
```

残りのフィールドがステップを確定させます。論理式を満たす集合はどれもステップの集合であり、要素は増え、廃棄値はつねにあり、現在の集合から取ったパラメータでのすべての探索に、最小の証人が加わります。

```agda
      only    : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
      grows   : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ fst (Φ Z) ⟩
      junk    : (Z : CS.S) → ⟨ ∅ ∈ˢ fst (Φ Z) ⟩
      least   : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
              → From Z vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ fst (Φ Z) ⟩
```

外向きのフィールドは、現在の集合が段階の下にあるとき、ステップの要素をホスト側で読みます。ステップの要素は、古い要素、廃棄値、探索の値のいずれかです。使い尽くしの証明が使うのはこの読み出しです。

```agda
      out     : (Z : CS.S) → ((z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
              → (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → ∥ Reads Z z ∥₁
```

反復のモジュールは、始点の構成可能性と、まとめられたステップを受け取ります。どちらも必要です。内部の再帰は `L` の要素からはじまり、ステップが論理式とその条項を供給するからです。

```agda
  module HullIter (X-isL : ⟨ isL X ⟩) (P : StepPack) where
    open StepPack P
```

始点は台の要素として提示されます。集合とその構成可能性の組であり、内部の再帰が消費するのはこの形です。

```agda
    Xʟ : CS.S
    Xʟ = X , X-isL
```

内部の ω 再帰が反復を作り、その閉包の機構が成長のフィールドを持ち運びます。それぞれの反復は前のものを含みます。反復はモデルの集合であり、反復の合併が `L` の要素になるのはこのためです。

```agda
    module It = Iterate Xʟ ΦFo Φ defines only
      using ( it; module Closure; iterUnion; iterUnion-in; iterUnion-out; iter; iter-in; iter-out; ω-num; Num )
    module Cl = It.Closure (λ Z z → grows Z (fst z)) using ( it-up )
```

反復の各段階は `hullStep n` と名づけられます。始点に対するステップの `n` 回目の適用です。

```agda
    hullStep : ℕ → CS.S
    hullStep = It.it
```

反復はその定義の等式に支配されます。ステップを `n+1` 回適用して得られるものは、`n` 番目の反復に一段階の閉包 `Φ` を適用したものちょうどです。この等式は `refl` で成立します。内部の ω 再帰は、後者の段階を計算するときにステップの演算を直接呼ぶので、輸送は何も要りません。これが、この構成のもっとも裸の算術です。この構成のそれぞれの層は、前の層の、ただ一つの定義可能なステップの下での閉包です。

```agda
    hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ Φ (hullStep n)
    hullStep-suc n = refl
```

反復はその添字とともに増えます。`n` が `n'` を超えなければ、`n` 番目の反復が集めたものはすべて、`n'` 番目の反復も集めます。ステップの成長のフィールドを差のぶんだけ繰り返し適用し、そのたびに古い要素は保たれます。数の等式が計数を運び、要素の構成可能性もそれとともに運ばれます。その要素は構成可能な反復に属するからです。この単調性により、早い段階で集められたものは、その後も収められたままになります。

```agda
    hullStep-≤ : (n n' : ℕ) → n ≤ n' → (z : S)
               → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ fst (hullStep n') ⟩
    hullStep-≤ n n' (k , e) z h =
      subst (λ m → ⟨ z ∈ˢ fst (hullStep m) ⟩) e (Cl.it-up n k (z , zL) h)
      where
```

反復の単調性は成長のフィールドから従います。前の反復の要素は、それ以降のすべての反復の要素であり、構成可能性も運ばれます。包の符号の深さは再帰で割り当てられます。base の符号の深さは零です。

証人の符号は、その符号のベクトルより一つ深い。その値は、パラメータの値の一歩あとの段階で計算されるからです。

```agda
      zL : ⟨ isL z ⟩
      zL = isL-trans {x = fst (hullStep n)} {y = z} h (snd (hullStep n))
    mutual
      depth : Code → ℕ
      depth (base m) = 0
```

証人の構成子は、その子の符号のベクトルの深さに一を加えます。

```agda
      depth (wit k ψ cs) = suc (depths cs)
```

符号のベクトルの深さは、項目の深さの最大値です。ベクトルは、すべての項目が手に入れば使えます。

```agda
      depths : {m : ℕ} → Vec Code m → ℕ
      depths [] = 0
      depths (c ∷ cs) = max (depth c) (depths cs)
```

補助は、決定可能な選言の一方が不可能なときの、場合分けの振る舞いを記録します。充足が空なら、計算された値は廃棄の分岐であり、もう一方の分岐が何と言おうと変わりません。

```agda
    private
      stuck-r : {A : Type (ℓ-suc ℓ)} (na : A → Empty.⊥)
                (f : A → SL) (g : (A → Empty.⊥) → SL) (s : A ⊎ (A → Empty.⊥))
              → Sum.rec f g s ≡ g na
      stuck-r na f g (inl a) = Empty.rec (na a)
```

反駁の分岐は、不可能な関数の関数外延性で証明されます。区別するような要素は存在しないからです。

```agda
      stuck-r na f g (inr h) = cong g (funExt (λ a → Empty.rec (na a)))
```

包から合併へ、前半：すべての包の符号の値は、その深さで添字づけられた反復に用意されます。base の符号は始点の要素を名指し、それは零番目の反復にあります。

```agda
    mutual
      hullStep-in : (c : Code) → ⟨ fst (val c) ∈ˢ fst (hullStep (depth c)) ⟩
      hullStep-in (base m) = member X m
      hullStep-in (wit k ψ cs) = go (lem (Sat k ψ (vals cs) , squash₁))
        where
```

証人符号について、その探索が充足可能かどうかで場合分けします。その深さはパラメータ符号ベクトルの深さより一つ大きく、後続段階の等式により、その深さの反復は `Φ` をもう一度適用した反復と同一視されます。

```agda
        n : ℕ
        n = depths cs
        go : (s : Sat k ψ (vals cs) ⊎ (Sat k ψ (vals cs) → Empty.⊥))
           → ⟨ fst (Sum.rec (search k ψ (vals cs)) (λ _ → (∅ , HSH.∅∈Lsetα)) s)
                ∈ˢ fst (hullStep (suc n)) ⟩
```

探索が充足されていれば、ステップの最小の証人の条項が、次の反復で探索された値を加えます。そのパラメータはベクトルの深さによって手に入ります。探索が充足されなければ、加える証人はなく、ステップは代わりに廃棄値を保ちます。

```agda
        go (inl w) = least (hullStep n) k ψ (vals cs) (vals-in cs) w
        go (inr h) = junk (hullStep n)
```

符号のベクトルのパラメータは、項目の深さの最大値で手に入ります。各項目の値はそれぞれの深さで現れ、単調性がそれを、ベクトルを消費するより後の反復へ運びます。

```agda
      vals-in : {m : ℕ} (cs : Vec Code m) → From (hullStep (depths cs)) (vals cs)
      vals-in (c ∷ cs) zero =
        hullStep-≤ (depth c) (max (depth c) (depths cs)) left-≤-max (fst (val c)) (hullStep-in c)
      vals-in (c ∷ cs) (suc i) =
        hullStep-≤ (depths cs) (max (depth c) (depths cs)) right-≤-max
```

この選択はパラメータベクトルについて再帰します。空ベクトルでは空の符号ベクトルの値ベクトルが条件を満たします。空でない場合は、先頭の包への所属からその符号を得て、尾部の符号を再帰的に得ます。

```agda
          (fst (lookup i (vals cs))) (vals-in cs i)
    private
      choose : {k : ℕ} (vs : Vec SL k)
             → ((i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ Hull ⟩)
             → ∥ Σ[ cs ∈ Vec Code k ] (vals cs ≡ vs) ∥₁
```

帰納のステップは、先頭を包の要素として符号化し、尾を帰納的に符号化します。値の等式は成分ごとに組み立てられ、台の等しさは基礎の集合の等しさへ帰着します。

```agda
      choose [] h = ∣ [] , refl ∣₁
      choose (v ∷ vs) h = PT.rec squash₁ (λ { (c , ec) → PT.map
        (λ { (cs , ecs) → (c ∷ cs)
           , cong₂ _∷_ (Σ≡Prop (λ z → snd (z ∈ˢ Lset lam)) ec) ecs })
        (choose vs (λ i → h (suc i))) })
```

符号ベクトル `cs` に対し、`val-wit` は `wit k ψ cs` の値を探索が返す最小の証人と同一視します。すべての符号の値は包に属するので、探索値も包に属します。

```agda
        (HSH.hull-member (fst v) (h zero))
      search-val : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k) (vs : Vec SL k)
                 → vals cs ≡ vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ Hull ⟩
      search-val k ψ cs vs e w =
        J (λ vs' e' → (w' : Sat k ψ vs') → ⟨ fst (search k ψ vs' w') ∈ˢ Hull ⟩)
```

パスの帰納が、パラメータのベクトルの同定に沿って主張を運び、証人の符号は包の内側で判定されます。

```agda
          (λ w' → subst (λ z → ⟨ fst z ∈ˢ Hull ⟩) (val-wit k ψ cs w') (inHull (wit k ψ cs)))
          e w
```

符号 `wit 0 ⊥̇ []` には充足する証人がないため、その値は失敗側の分岐を通って `∅` になります。すべての符号の値は包に属するので、廃棄値も包に属します。

```agda
      junk∈Hull : ⟨ ∅ ∈ˢ Hull ⟩
      junk∈Hull = subst (λ z → ⟨ fst z ∈ˢ Hull ⟩)
        (stuck-r no (search 0 ⊥̇ []) (λ _ → (∅ , HSH.∅∈Lsetα)) (lem (Sat 0 ⊥̇ [] , squash₁)))
        (inHull (wit 0 ⊥̇ []))
        where
```

偽を満たす環境はありません。そのような充足の証明を展開すると、空型の要素が得られてしまいます。

```agda
        no : Sat 0 ⊥̇ [] → Empty.⊥
        no = PT.rec Empty.isProp⊥ (λ { (a , h) → Empty.rec* h })
```

合併から包へ、後半：すべての反復のすべての要素が包の中にあります。反復の添字についての帰納です。基底の場合は始点であり、その要素は包の章によって包の要素です。

```agda
    hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Hull ⟩
    hullStep⊆Hull zero z h = HSH.X⊆M z h
    hullStep⊆Hull (suc n) z h = PT.rec (snd (z ∈ˢ Hull)) read
      (out (hullStep n) (λ z' hz' → HSH.Hull⊆L z' (hullStep⊆Hull n z' hz')) z h)
      where
```

ステップの場合は、外向きの条項を通して、後者の反復の要素を読みます。それは古い要素であり、帰納の仮定によってすでに包の中にあります。廃棄値でもあり、すでに包の中にあります。あるいは探索された値で、つぎに扱われます。

```agda
      read : Reads (hullStep n) z → ⟨ z ∈ˢ Hull ⟩
      read (inl h') = hullStep⊆Hull n z h'
      read (inr (inl e)) = subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e) junk∈Hull
      read (inr (inr (k , ψ , vs , w , from , e))) =
        subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e)
```

探索された値は、そのパラメータの符号のベクトルと対応づけられ、各パラメータは帰納の仮定によって包の要素です。だから探索は `search-val` によって包の中にあり、等式がその所属を `z` へ運びます。反復の合併が、包を提示する `L` の要素として名づけられます。

```agda
          (PT.rec (snd (fst (search k ψ vs w) ∈ˢ Hull))
            (λ { (cs , ecs) → search-val k ψ cs vs ecs w })
            (choose vs (λ i → hullStep⊆Hull n (fst (lookup i vs)) (from i))))
    hullL : CS.S
    hullL = It.iterUnion
```

`L` の要素としての包は、反復の合併であり、その所属の記述は、要素がちょうど包の要素であると言います。前向き：合併の要素はある反復に属し、だから包の中にあります。

```agda
    hullL-spec : fst hullL ≡ Hull
    hullL-spec = extensionalV {a = fst hullL} {b = Hull} (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : S) → ⟨ z ∈ˢ fst hullL ⟩ → ⟨ z ∈ˢ Hull ⟩
      fwd z h = PT.rec (snd (z ∈ˢ Hull))
```

反復の添字は、合併の外向きの読み出しに消費され、要素の構成可能性は合併から運ばれます。合併そのものが、構成によって構成可能なのです。

```agda
        (λ { (n , hn) → hullStep⊆Hull n z hn })
        (It.iterUnion-out (z , isL-trans {x = fst hullL} {y = z} h (snd hullL)) h)
```

後ろ向き：包の要素はある符号に名指され、その値は、符号の深さで添字づけられた反復に現れます。合併の内向きの読み出しがそれを受け入れます。

```agda
      bwd : (z : S) → ⟨ z ∈ˢ Hull ⟩ → ⟨ z ∈ˢ fst hullL ⟩
      bwd z h = PT.rec (snd (z ∈ˢ fst hullL))
        (λ { (c , ec) → It.iterUnion-in (depth c) zS
               (subst (λ t → ⟨ t ∈ˢ fst (hullStep (depth c)) ⟩) ec (hullStep-in c)) })
        (HSH.hull-member z h)
```

名指された要素は台の中へ載せられます。その構成可能性は、包が段階に含まれることから従い、段階の要素としての提示が証明書を供給します。

```agda
        where
        zS : CS.S
        zS = z , Lset→isL lam ordλ z (HSH.Hull⊆L z h)
```

基礎の集合の等しさが、合併の構成可能性を包の上へ運びます。包は `L` の要素です。本章の前半はこれで完全に清算され、第二のモジュールは、今消費された定義可能なステップを作ります。

ステップは段階の内側で作られ、その定数は段階の対象を名指します。`lam` の構成可能性は、`lam` が順序数であることから来ます。

```agda
    M-isL : ⟨ isL HS.M ⟩
    M-isL = subst (λ t → ⟨ isL t ⟩) hullL-spec (snd hullL)
  module Build where
```

階層の順序数は構成可能であり、これが段階を `L` の内側に固定します。

```agda
    λ-isL : ⟨ isL lam ⟩
    λ-isL = isL-ord lam ordλ
```

`A` は `Lset lam` をその構成可能性の証明とともにモデルの要素として表します。充足グラフと段階上の公式の符号化は、これを段階のパラメータとして用います。

```agda
    A : CS.S
    A = LsetS lam ordλ
```

段階の上の充足のグラフは、すべての符号の充足集合を、二つの読み出しとともに一度に供給します。そして段階の上の定義可能性が、論理式の定数を段階の要素として解釈します。

```agda
    module SM = SatGraph A using ( pairs; pairs-in; pairs-out; valOf; valOf≡ )
    module DA = DefOf (Lset lam) using ( ι; _⊨ᵐ_; 𝒮M )
```

空のアルファベットでの符号の集合は、無定数の論理式の符号を集めます。そのような論理式は自由変数をもつことがあります。欠けているのは定数であり、自由変数に値を与えるのは、探索のパラメータ環境です。

```agda
    C₀ : CS.S
    C₀ = AllCodes ∅ʟ
```

段階の内部の整列順序は、モデルの要素として提示されます。最小の証人を比較するための関係です。

```agda
    Rel : CS.S
    Rel = relL lam λ-isL ordλ
```

小さな台の上の狭義の整列順序は、その関係から読まれ、比較は台の要素の上で述べられます。構成可能な順序対の第二成分もまた構成可能であり、これが、のちの名前のパラメータに必要になります。

```agda
    wL : SWO SL
    wL = orderAt lam ordλ
    relOf-at : SL → SL → Type (ℓ-suc ℓ)
    relOf-at = relOf wL
    pr-snd-isL : (a b : V ℓ) → ⟨ isL (pr a b) ⟩ → ⟨ isL b ⟩
```

証明は、順序対を一元集合を通して二度剥がします。対への所属は第二成分を「一元集合と対」の入れ子の中に置き、それぞれの剥離が、推移性によって構成可能性を保ちます。

```agda
    pr-snd-isL a b h =
      isL-trans {x = ⁅ a , b ⁆} {y = b} (subst ⟨_⟩ (sym (pair-spec a b b)) ∣ inr refl ∣₁)
        (isL-trans {x = pr a b} {y = ⁅ a , b ⁆}
          (subst ⟨_⟩ (sym (pair-spec ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆)) ∣ inr refl ∣₁) h)
```

数項は台の要素として提示されます。有限の順序数とその構成可能性であり、証人の論理式のキーの条項がこれを量化します。

```agda
    nn : ℕ → CS.S
    nn k = # k , numL k
```

定数のアルファベットは空なので、段階の台への解釈 `ε′` は一意です。これにより、何も選択せずに無定数公式を段階の言語へ付け替えられます。

```agda
    ε′ : ⊥* {ℓ} → ⟪ Lset lam ⟫
    ε′ = Empty.rec*
    sat-bridge : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k)
               → (δ ⊨₀ χ) ≡ (δ DA.⊨ᵐ mapFo ε′ χ)
    sat-bridge k χ δ =
```

この橋は合成です。空のアルファベットの環境は、解釈すべきものがないため、自明に一致します。そして改名の定理が、改名された論理式の外側の充足と、段階の内側の充足とを同一視します。

```agda
        cong (λ κ → FOL.Semantics.At._⊨_ DA.𝒮M (⊥* {ℓ}) κ δ χ)
          (funExt (λ b → Empty.rec* b))
      ∙ sym (⊨-map DA.𝒮M ε′ DA.ι χ δ)
    opaque
      keyOf : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
```

無定数の論理式の、段階でのキーとは、改名された形の、段階の符号の集合でのキーです。一度だけ名づけられ、以後の主張はその構成を開かずに参照できます。

```agda
      keyOf k χ = keyS A (mapFo ε′ χ)
```

そのキーは、段階での符号の集合に属します。改名された論理式の符号は、段階のアルファベットの上の符号であり、符号の集合はそれらをすべて含みます。

```agda
      keyOf∈ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ keyOf k χ CS.∈ˢ AllCodes A ⟩
      keyOf∈ k χ = key∈AllCodes A (mapFo ε′ χ)
```

`keyOf` は不透明ですが、補題 `keyOf≡` が `keyS A (mapFo ε′ χ)` との正確な等式を公開します。以後の証明は、封印された定義を展開せずにこの等式を使えます。

```agda
      keyOf≡ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → keyOf k χ ≡ keyS A (mapFo ε′ χ)
      keyOf≡ k χ = refl
```

封印されたキーの基礎の集合が計算されます。それは、アリティの数項と、改名された論理式の符号との順序対です。証明は、論理式の二つの改名を合成します。空のアルファベットを経て、段階の埋め込みへ続くものです。改名の定理が、結果を極限段階が記録する符号と同一視します。

```agda
      keyOf-fst : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
                → fst (keyOf k χ) ≡ pr (# k) (fst (limitCode χ))
      keyOf-fst k χ = cong (pr (# k)) (cong VCode.⌜_⌝
        ( mapFo-comp ε′ ⟪ Lset lam ⟫↪ χ
        ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b)) ))
```

各無パラメータ論理式に対し、`Tof` は充足のグラフがその論理式の封印されたキーで選ぶ充足集合です。この固定した集合が、段階全体でその論理式の充足関係を表します。

```agda
    Tof : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
    Tof k χ = SM.valOf (keyOf k χ) (keyOf∈ k χ)
```

キーとその充足集合との順序対は、充足のグラフに属します。さらに、キーと同じ基礎集合をもつ台の要素は同じ充足集合を選びます。構成可能性の証明は命題なので、基礎集合の等しさが台での等しさへ持ち上がり、したがって選ばれた値も等しくなります。

```agda
    Tof-pair : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
             → ⟨ pr (fst (keyOf k χ)) (fst (Tof k χ)) ∈ˢ fst SM.pairs ⟩
    Tof-pair k χ = SM.pairs-in (keyOf k χ) (keyOf∈ k χ)
    valOf-same : (x : CS.S) (m : ⟨ x CS.∈ˢ AllCodes A ⟩) (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
               → fst x ≡ fst (keyOf k χ) → SM.valOf x m ≡ Tof k χ
```

証明は、基礎の集合の等式の上のパス帰納で進みます。符号集合への所属の命題性が、所属の証明の違いを吸収します。大切なのは基礎の集合だけなので、輸送はそのほかの何ものにも触れません。

```agda
    valOf-same x m k χ e =
      J (λ x' e' → (m' : ⟨ x' CS.∈ˢ AllCodes A ⟩) → SM.valOf x m ≡ SM.valOf x' m')
        (λ m' → cong (SM.valOf x) (snd (x CS.∈ˢ AllCodes A) m m'))
        (S≡ {x = x} {y = keyOf k χ} e) (keyOf∈ k χ)
    sat-at : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k) (z : CS.S)
```

充足集合への所属が、ここで段階自身の充足として計算されます。この橋は三つの同定を合成します。封印された名前は、その作られたキーと一致すること。キーでの値は、一様な充足の定理によって外側の充足として読めること。そして改名された論理式の外側の充足が、改名の橋によって段階の内側の充足に等しいことです。

```agda
           → fst z ≡ graph A δ → (z CS.∈ˢ Tof k χ) ≡ (δ ⊨₀ χ)
    sat-at k χ δ z qz =
        cong (z CS.∈ˢ_) (SM.valOf≡ (keyOf k χ) (keyOf∈ k χ))
      ∙ val-sat A (mapFo ε′ χ) (keyOf k χ) (keyOf∈ k χ) (cong fst (keyOf≡ k χ)) δ z qz
      ∙ sym (sat-bridge k χ δ)
```

キーの認識式は、枠 `s` の値がこの段階の符号集合に属し、ある符号との間で、枠 `a` にある数項の後者とその符号との順序対になっている、と述べます。したがって、枠 `a` が `# k` を含むとき、これはアリティ `k+1` の無パラメータ論理式のキーを認識します。ここで無パラメータとは定数域が空であるという意味で、論理式は自由変数をもちえます。

```agda
    opaque
      keyIn : ∀ {n} → Fin n → Fin n → Formula CS.S n
      keyIn s a = (var s ∈̇ con C₀)
                ∧̇ ∃̇ ( sucAtL (suc a) zero
                     ∧̇ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) )
```

読み出しは、変数の環境の上で、固定したアリティ `k` に対して述べられます。その数項は枠 `a` に名指されています。アリティをはじめに固定するからこそ、二つの読み出しは、符号の中を探すのではなく、符号についての等式になるのです。

```agda
    module KeyIn {n : ℕ} (s a : Fin n) (γ : CS.S ^ n) (k : ℕ)
                 (qa : fst (lookup a γ) ≡ # k) where
```

論理式は、その自分の枠の上で計算のために開かれます。読み出しが、定義の連言と存在量化子を通り抜けなければならないからです。

```agda
      opaque
        unfolding keyIn
```

導入は、三つのデータから充足を作ります。`s` の符号集合への所属、階層の要素 `c`、そして `s` を「後者の数項と `c` の対」と同定する等式です。数項、後者の条項、対の条項が、この順で満たされます。

```agda
        keyIn-in : ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩ → (c : V ℓ)
                 → fst (lookup s γ) ≡ pr (# (suc k)) c → ⟨ γ ⊨ keyIn s a ⟩
        keyIn-in h c q = h , ∣ numAt , ( hsuc , ∣ cS , hpr ∣₁ ) ∣₁
          where
          numAt : CS.S
```

数項は台の要素として提示され、符号 `c` も台の要素へ持ち上げられます。`s` をその順序対と同定する等式と `s` の構成可能性から、`pr-snd-isL` は順序対の第二成分 `c` の構成可能性を取り出します。

```agda
          numAt = nn (suc k)
          cS : CS.S
          cS = c , pr-snd-isL (# (suc k)) c
                     (subst (λ u → ⟨ isL u ⟩) q (isL-trans h (snd C₀)))
          hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
```

後者の条項は、枠 `a` の数項の等式から、対の条項は `s` の等式から、それぞれその符号化の演算子の妥当性を通して運ばれます。この二つの輸送こそ、ホストの等式を充足へ変えるものです。

```agda
          hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
            (cong sucV (sym qa))
          hpr : ⟨ (cS ∷ numAt ∷ γ) ⊨ prAtL (suc (suc s)) (suc zero) zero ⟩
          hpr = subst ⟨_⟩
            (sym (prAtL-adequate (suc (suc s)) (suc zero) zero (cS ∷ numAt ∷ γ))) q
```

消去は、二つのデータを取り戻します。`s` の符号集合への所属と、「`s` は後者の数項とある符号の対である」という切り詰められた主張です。論理式の存在の連鎖が、一歩ずつほどかれます。

```agda
        keyIn-out : ⟨ γ ⊨ keyIn s a ⟩
                  → ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩
                  × ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
        keyIn-out (h , hk) = h , PT.rec squash₁ atNum hk
          where
```

中間の束縛子は、後者の枠の数項を名指し、後者の符号化の妥当性が、その充足を基礎の集合の等式へ変換します。

```agda
          atNum : Σ[ z ∈ CS.S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                                × ⟨ (z ∷ γ) ⊨ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) ⟩ )
                → ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
          atNum (z , (hs , hc)) = PT.map
            (λ { (c , hp) → fst c
```

内側の存在量化子が、対の条項の充足をもつ符号 `c` を与えます。妥当性がそれを順序対の等式へ運び、数項とその後者の同定と合成します。取り戻された等式は、求めていた切り詰められた主張そのものです。

```agda
               , ( subst ⟨_⟩ (prAtL-adequate (suc (suc s)) (suc zero) zero (c ∷ z ∷ γ)) hp
                 ∙ cong (λ u → pr u (fst c)) (qz ∙ cong sucV qa) ) })
            hc
            where
            qz : fst z ≡ sucV (fst (lookup a γ))
```

七つの枠の環境がここで組み立てられます。充足の表、拡張された環境、パラメータの環境、キー、数項、証人、そして現在の集合。本体が読む順のままです。

```agda
            qz = subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs
    Env : CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S ^ 7
    Env T e' e s k w Z = T ∷ e' ∷ e ∷ s ∷ k ∷ w ∷ Z ∷ []
```

極小性の部分の論理式は、段階のアルファベットの上で量化します。こう言います。パラメータの環境がある段階の要素で拡張され、符号化された論理式を満たすなら、そのような要素で、段階の整列順序において証人の前に立つものはありません。定数 `A` で界されているので、量化は宇宙ではなく段階の上を走ります。

```agda
    opaque
      minFo : Formula CS.S 7
      minFo = ∀̇∈ (con A)
        ( (∃̇ ( consAtL i0 i1 i4 ∧̇ (var i0 ∈̇ var i2) )) ⇒̇ ¬̇ (appC Rel i0 i6) )
```

本体の連言項は、順にこう言います。数項は内部の `ωʟ` の中にある。`s` はアリティが一つ大きいキーである。パラメータの環境が、現在の集合の上のベクトルを符号化する。拡張された環境が、それを証人で拡張する、と。

```agda
      bodyFo : Formula CS.S 7
      bodyFo = (var i4 ∈̇ con ωʟ)
            ∧̇ ( keyIn i3 i4
            ∧̇ ( envOverAt i2 i4 i6
            ∧̇ ( consAtL i1 i5 i2
```

残りの連言項はこう言います。キーと表の対が充足のグラフの中にある。拡張された環境が表の中にある。証人が段階の中にある。そして極小性が成立します。連言項は全部で八つです。段階は証人と極小性で比較する候補を制限し、符号化の連言項は、この記録を充足表へ結びつける補助対象を与えます。

```agda
            ∧̇ ( appC SM.pairs i3 i0
            ∧̇ ( (var i1 ∈̇ var i0)
            ∧̇ ( (var i5 ∈̇ con A)
            ∧̇ minFo ))))))
```

七つの対象 `T,e',e,s,k,w,Z` を固定します。それらからなる環境では、本体は具体的な命題となり、八つの連言項を個別に取り出すことも、逆に組み立てることもできます。

```agda
    module BodyRd (T e' e s k w Z : CS.S) where
```

七つの枠の環境が記録され、ホスト側の極小性は、パラメータの環境を提示する族に相対的に述べられます。より小さい段階の要素による拡張が、充足の表の中に落ち、かつ整列順序で証人の前に立つ、ということはありません。

```agda
      γ₇ : CS.S ^ 7
      γ₇ = Env T e' e s k w Z
      Min : {m : ℕ} (g : Fin m → V ℓ) → Type (ℓ-suc ℓ)
      Min g = (w' : CS.S) → ⟨ fst w' ∈ˢ fst A ⟩ → (e'' : CS.S)
            → fst e'' ≡ env (cons (fst w') g) → ⟨ fst e'' ∈ˢ fst T ⟩
```

この条項は空型で終わります。極小性は反駁であり、反例のデータ、つまりより小さい拡張とその対への所属が、ちょうど不可能でなければならないのです。

```agda
            → ⟨ pr (fst w') (fst w) ∈ˢ fst Rel ⟩ → Empty.⊥
```

本体は入れ子の連言なので、八つの条件はそれぞれ射影によって読み出せます。逆に、八条件の証明を組み合わせれば、本体の充足を得られます。

```agda
      opaque
        unfolding bodyFo
```

最初の読み出しは数項の条項を射影します。内部の `ωʟ` への所属から自然数 `n` を復元でき、キーの条項と合わせると、`s` がアリティ `n+1` のキーであり、その一枠が証人に割り当てられていると分かります。

```agda
        b-num : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst k ∈ˢ fst ωʟ ⟩
        b-num h = h .fst
```

第二の射影はキーの条項です。論理式は `s` と `k` の枠で、`s` が認識されたキーであり、そのアリティが数項 `k` より一つ大きいことを述べます。

```agda
        b-key : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩
        b-key h = h .snd .fst
```

第三の読み出しは、環境の条項を射影します。パラメータの環境が、記録された枠で、現在の集合の上のベクトルを符号化します。

```agda
        b-env : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
        b-env h = h .snd .snd .fst
```

第四の読み出しは拡張の等式を述べます。cons の符号化の妥当性に沿って運ばれたもので、拡張された環境は、パラメータの環境を証人で拡張したものです。

```agda
        b-cons : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g
               → ⟨ γ₇ ⊨ bodyFo ⟩ → fst e' ≡ env (cons (fst w) g)
        b-cons g hE h =
          subst ⟨_⟩ (consAtL-adequate i1 i5 i2 γ₇ g hE) (h .snd .snd .snd .fst)
```

第五の読み出しは、キーと表の対のグラフへの所属を述べます。適用の符号化の妥当性に沿って運ばれたものです。

```agda
        b-tab : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩
        b-tab h = subst ⟨_⟩ (appC-adequate SM.pairs i3 i0 γ₇) (h .snd .snd .snd .snd .fst)
```

第六の読み出しは、拡張された環境の充足の表への所属です。証人がパラメータで符号化された論理式を満たす、という事実です。

```agda
        b-mem : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst e' ∈ˢ fst T ⟩
        b-mem h = h .snd .snd .snd .snd .snd .fst
```

第七の射影は、証人が段階 `A` に属することを述べます。したがって、証人と、それと比較される候補はすべて同じ段階を動きます。

```agda
        b-stage : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst w ∈ˢ fst A ⟩
        b-stage h = h .snd .snd .snd .snd .snd .snd .fst
```

第八の読み出しは、反駁の形で読まれる極小性の条項です。より小さい候補が充足する拡張をもてば、有界の量化子と矛盾します。関係の項目は、適用の妥当性を通して輸送されたうえでです。

```agda
        b-min : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g → ⟨ γ₇ ⊨ bodyFo ⟩ → Min g
        b-min g hE h w' hw' e'' qe hm hr =
          lower (h .snd .snd .snd .snd .snd .snd .snd w' hw' ∣ e'' , (hc , hm) ∣₁
            (subst ⟨_⟩ (sym (appC-adequate Rel i0 i6 (w' ∷ γ₇))) hr))
          where
```

候補の拡張の cons の条項は、そのホストの等式から運ばれます。内側の存在量化子での拡張の符号化と、ちょうど鏡の関係です。

```agda
          hc : ⟨ (e'' ∷ w' ∷ γ₇) ⊨ consAtL i0 i1 i4 ⟩
          hc = subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE)) qe
```

充填の読み出しは、八つの成分から本体の充足を組み立てます。数項の条項、キーの条項、環境の条項、拡張の等式、グラフへの所属、表への所属、段階への所属、そして極小性です。

```agda
        b-fill : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g
               → ⟨ fst k ∈ˢ fst ωʟ ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
               → fst e' ≡ env (cons (fst w) g) → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩
               → ⟨ fst e' ∈ˢ fst T ⟩ → ⟨ fst w ∈ˢ fst A ⟩ → Min g
               → ⟨ γ₇ ⊨ bodyFo ⟩
```

五つの連言項はそのまま挿入されます。拡張の等式とグラフの項目は、`consAtL` と `appC` の妥当性の等式を逆向きに用いて充足へ戻され、極小性は最後の条項で与えられます。

```agda
        b-fill g hE c1 c2 c3 c4 c5 c6 c7 mn =
          c1 , c2 , c3
          , subst ⟨_⟩ (sym (consAtL-adequate i1 i5 i2 γ₇ g hE)) c4
          , subst ⟨_⟩ (sym (appC-adequate SM.pairs i3 i0 γ₇)) c5
          , c6 , c7
```

極小性の充填は、切り詰められた反例を空型へ消去することで行われます。反例は二つの妥当性の等式を通して運ばれ、反駁に手渡されます。だから充填に要るのは矛盾だけで、構成ではありません。

```agda
          , λ w' hw' hex hr → lift (PT.rec Empty.isProp⊥
              (λ { (e'' , (hc , hm)) → mn w' hw' e''
                     (subst ⟨_⟩ (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE) hc) hm
                     (subst ⟨_⟩ (appC-adequate Rel i0 i6 (w' ∷ γ₇)) hr) })
              hex)
```

証人の論理式は、本体を五重の存在量化で包みます。対象ごとに一つです。充足の表、拡張された環境、パラメータの環境、キー、そして数項。この論理式の `w` と `Z` での充足が言うのは、`Z` の上の `w` での最小の証人の完全な記録が存在するということです。

```agda
    opaque
      witFo : Formula CS.S 2
      witFo = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ bodyFo))))
```

内向きの読み出しは、五つの対象と本体の充足を、五つの束縛子を通して注入します。一回の注入が一つの対象を、その枠へ運びます。

```agda
      witFo-in : (w Z T e' e s k : CS.S) → ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩
               → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
      witFo-in w Z T e' e s k h = ∣ k , ∣ s , ∣ e , ∣ e' , ∣ T , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
```

外向きの読み出しは、束縛の順に五つの切り詰められた存在を消去します。最内層では `PT.map` が、復元した対象を表示された依存対へ並べ替えるだけで、本体の充足そのものは輸送しません。

```agda
      witFo-out : (w Z : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
                → ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] Σ[ k ∈ CS.S ]
                     ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩ ∥₁
      witFo-out w Z = PT.rec squash₁ (λ { (k , hk) → PT.rec squash₁ (λ { (s , hs) →
        PT.rec squash₁ (λ { (e , he) → PT.rec squash₁ (λ { (e' , he') → PT.map
```

`witFo` をほどくと、充足表・拡張環境・パラメータ環境・キー・数項が得られ、それらからなる環境が本体を満たします。

```agda
          (λ { (T , hT) → T , e' , e , s , k , hT }) he' }) he }) hs }) hk })
```

## 固定したキーと環境における最小の証人の関係

`e` と `s` を固定すると、`LeastWitness Z e s z` は残る充足表・拡張環境・数項の切り詰められた存在を保持します。

```agda
    LeastWitness : CS.S → CS.S → CS.S → CS.S → Type (ℓ-suc ℓ)
    LeastWitness Z e s z =
      ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
          ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩ ∥₁
```

六つの周囲の変数を保ったまま充足表・拡張環境・数項を束縛するため、本体を七枠から九枠へ改名します。写像は七つの実質的な成分を `T,e',e,s,k,z,Z` の位置へ置きます。

```agda
    private
      ρ₉ : Fin 7 → Fin 9
      ρ₉ zero = i0
      ρ₉ (suc zero) = i1
      ρ₉ (suc (suc zero)) = i4
```

残る四つの場合は、キー `s`、数項 `k`、候補 `z`、現在の集合 `Z` を配置します。末尾の `p,q` は読まれないので、充足はその値に依存しません。

```agda
      ρ₉ (suc (suc (suc zero))) = i5
      ρ₉ (suc (suc (suc (suc zero)))) = i2
      ρ₉ (suc (suc (suc (suc (suc zero))))) = i6
      ρ₉ (suc (suc (suc (suc (suc (suc zero)))))) = i3
```

`Γ₉` がこの配置を示し、元の七つの枠の環境との各一致は、定義上の反射性で成り立ちます。

```agda
      Γ₉ : (T e' k Z e s z p q : CS.S) → CS.S ^ 9
      Γ₉ T e' k Z e s z p q = T ∷ e' ∷ k ∷ Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []
```

一致はこう言います。改名されたそれぞれの枠で、二つの環境は同じ台の要素を載せている、と。最初の三つは反射性で証明され、改名された位置ごとに一つです。

```agda
      ag₉ : (T e' k Z e s z p q : CS.S)
          → Ren.Agrees ρ₉ (Γ₉ T e' k Z e s z p q) (Env T e' e s k z Z)
      ag₉ T e' k Z e s z p q zero = refl
      ag₉ T e' k Z e s z p q (suc zero) = refl
      ag₉ T e' k Z e s z p q (suc (suc zero)) = refl
```

残りの四つの一致も同じく反射性で、枠ごとに一つです。どの一致も計算であり、これが、改名を充足の内側で使える理由です。

```agda
      ag₉ T e' k Z e s z p q (suc (suc (suc zero))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc zero)))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc zero))))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc (suc zero)))))) = refl
```

改名された本体は、本体の論理式を枠の対応に沿って押し出したもので、九つの枠の上にありながら、言うことは以前と同じです。

```agda
      body₉ : Formula CS.S 9
      body₉ = renameFo ρ₉ bodyFo
```

読みの等式はこう言います。九つの枠の環境で改名された本体を充足することは、七つの枠の環境で本体を充足することと、同じ命題です。

```agda
      body₉-read : (T e' k Z e s z p q : CS.S)
                 → ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩
                 ≡ ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩
      body₉-read T e' k Z e s z p q =
        cong ⟨_⟩ (Ren.⊨-rename ρ₉ bodyFo (Γ₉ T e' k Z e s z p q)
```

証明は、枠の一致を引数に改名の定理を適用し、充足の括弧の下で輸送するものです。

```agda
                    (Env T e' e s k z Z) (ag₉ T e' k Z e s z p q))
```

最小の証人の論理式は、改名された本体の上に、さらに三つの存在量化を包みます。数項、拡張された環境、充足の表です。六つの枠の環境での充足が言うのは、候補の、現在の集合・キー・パラメータの環境における最小の証人の記録が存在するということです。

```agda
    opaque
      leastWitnessFo : Formula CS.S 6
      leastWitnessFo = ∃̇ (∃̇ (∃̇ body₉))
```

内向きの読み出しは、切り詰められた最小の証人のデータを消去して三つの対象を注入し、本体の充足を、改名された本体の読みの等式に沿って運びます。

```agda
      leastWitness-in : (Z e s z p q : CS.S) → LeastWitness Z e s z
                      → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
      leastWitness-in Z e s z p q = PT.rec (snd ((Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo))
        (λ { (T , e' , k , h) →
          ∣ k , ∣ e' , ∣ T , transport (sym (body₉-read T e' k Z e s z p q)) h ∣₁ ∣₁ ∣₁ })
```

外向きの読み出しは、三重の入れ子の存在量化を順に消去し、そのつど切り詰められた続きの中へ消去します。だから論理式の充足は、再び最小の証人の記録になります。

```agda
      leastWitness-out : (Z e s z p q : CS.S)
                       → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
                       → LeastWitness Z e s z
      leastWitness-out Z e s z p q = PT.rec squash₁ at₁
        where
```

最も内側の消去は、名指された充足表・拡張環境・数項から最小の証人のデータを組み立て直し、本体の充足を読み出しの等式に沿って輸送します。外側の二つの消去は、この構成に必要な束縛された対象を与えます。

```agda
        at₃ : (k e' : CS.S) → Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩
            → LeastWitness Z e s z
        at₃ k e' (T , h) = ∣ T , e' , k , transport (body₉-read T e' k Z e s z p q) h ∣₁
        at₂ : (k : CS.S) → Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁
            → LeastWitness Z e s z
```

ここには二重の切り詰めが残っている。外側は延長された環境 `e'` を、内側は表 `T` を隠している。二回の除去でそれらを順に取り出すと、`at₃` が改名された本体の証明を `LeastWitness` へ戻す。

```agda
        at₂ k (e' , h) = PT.rec squash₁ (at₃ k e') h
        at₁ : Σ[ k ∈ CS.S ] ∥ Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ]
                ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁ ∥₁
            → LeastWitness Z e s z
        at₁ (k , h) = PT.rec squash₁ (at₂ k) h
```

数項のスロットには内部の `ω` の要素が収められており、`decode-num` がそれを解読します。切り詰められた自然数 `n` と、その項目を周囲の数項 `# n` と同一視する等式が得られるのです。解読は、内部の付番と証人のデータの自然数の管理とを結ぶ橋です。

```agda
    private
      decode-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
      decode-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
        (subst ⟨_⟩ (ω-specL q) h)
```

`LeastWitnessData` は最小証人の背後にある実際のデータです。自然数 `n`、`Z` の提示への `n` 個の添字の割り当て `g`、`e` がそれらの値を名指す環境であることの等式、そして `s` を `Lset ω` に置く段階の所属です。

```agda
    LeastWitnessData : CS.S → CS.S → CS.S → Type (ℓ-suc ℓ)
    LeastWitnessData Z e s =
      Σ[ n ∈ ℕ ] Σ[ g ∈ (Fin n → ⟪ fst Z ⟫) ]
        ((fst e ≡ env (λ i → ⟪ fst Z ⟫↪ (g i))) × (⟨ fst s ∈ Lset ω ⟩))
```

定理 `leastWitness-data` は、論理式の水準の最小証人から、命題的切り詰めのもとで、自然数のアリティ、`Z` 上で添字付けられたパラメータ環境、そしてキーが `Lset ω` に属する証明が得られることを述べる。

```agda
    opaque
      leastWitness-data : (Z e s z : CS.S) → LeastWitness Z e s z
                        → ∥ LeastWitnessData Z e s ∥₁
      leastWitness-data Z e s z = PT.rec squash₁ body
        where
```

変換の本体は、体の充足を消費します。それを表 `T`、拡張 `e'`、鍵 `k`、そして体の証明へ分解し、鍵の数項の項目がまず解読されます。

```agda
        body : Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
                 ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩
             → ∥ LeastWitnessData Z e s ∥₁
        body (T , e' , k , hb) = PT.map at (decode-num k (BodyRd.b-num T e' e s k z Z hb))
          where
```

数項 `n` と鍵を名指す等式が揃うと、データが組み上がります。長さ `n`、復元された割り当て `g`、環境の復元の等式、そして `s` の段階の所属です。七項目の文脈には一度名前が与えられ、復元が各スロットを参照できるようにします。

```agda
          at : Σ[ n ∈ ℕ ] (fst k ≡ # n) → LeastWitnessData Z e s
          at (n , qk) = n , R.g , R.recovers , s∈Lω
            where
            γ : CS.S ^ 7
            γ = Env T e' e s k z Z
```

環境の節は `Z` の添字の割り当て `g` を復元し、`e` がそれらの値のグラフであることを示す。一方、キーの節は `s` がコードであり、後続アリティの数項と論理式コードとの順序対であることを述べる。

```agda
            module R = Recover Z n γ i2 i4 i6 qk refl (BodyRd.b-env T e' e s k z Z hb)
              using ( g; recovers )
            kr : ⟨ fst s ∈ fst C₀ ⟩ × ∥ Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) ∥₁
            kr = KeyIn.keyIn-out i3 i4 γ n qk (BodyRd.b-key T e' e s k z Z hb)
            s∈Lω : ⟨ fst s ∈ Lset ω ⟩
```

鍵の値の段階の所属がデータの最後の部分です。これは対の等式から証明されます。鍵の第二成分 `c` はコードであり、コードは極限の段階で既に構成可能です。

```agda
            s∈Lω = PT.rec (snd (fst s ∈ Lset ω)) read (kr .snd)
              where
              read : Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) → ⟨ fst s ∈ Lset ω ⟩
              read (c , qs) = PT.rec (snd (fst s ∈ Lset ω))
                (λ { (χ , qc) → subst (λ w → ⟨ w ∈ Lset ω ⟩) (sym qs)
```

したがって鍵の二つの成分はどちらも `Lset ω` に住みます。後続の数項は数項の所属によって極限に属し、極限の段階の要素の順序対はやはり極限にとどまります。対の等式に沿って輸送すれば `s` は `Lset ω` に入り、`LeastWitnessData` が完成します。

```agda
                       (pr∈limit (# (suc n)) c (numeral∈limit (suc n))
                         (subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym qc) (snd (limitCode χ)))) })
                (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ fst C₀ ⟩) qs (kr .fst)))
```

証人の論理式の外向きの読みがここで組み上がります。`(z, Z)` での `witFo` の充足は、表、拡張、鍵、そして体の証明へ展開され、体の証明は切り詰められた `LeastWitness` へ変換されます。Skolem の節の充足を消費するのはこの形です。

```agda
      witFo-leastWitness : (z Z : CS.S) → ⟨ (z ∷ Z ∷ []) ⊨ witFo ⟩
                         → ∥ Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] LeastWitness Z e s z ∥₁
      witFo-leastWitness z Z h = PT.map
        (λ { (T , e' , e , s , k , hb) → e , s , ∣ T , e' , k , hb ∣₁ })
        (witFo-out z Z h)
```

二つの証人を比較するため、本体の八つの節のうち、数項、環境、延長、表、所属、段階、最小性の七つを保持する。ここではキーの節は必要ない。二つの証人はすでに `s` を共有しており、そのキーに対応する値の一意性によって二つの表が同定されるからである。

```agda
    private
      module WitnessBody (z T e' e s k Z : CS.S)
        (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩) where
        module Rd = BodyRd T e' e s k z Z
          using ( b-num; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
```

保持した二つの節から、延長された環境が表に属することと、証人が `Lset lam` に属することが直ちに得られる。キーの数項を `# n` と同定すると、環境の節はさらに `Z` の添字からなる `n` 組を復元する。

```agda
        h6 = Rd.b-mem hb
        h7 = Rd.b-stage hb
        module AtNum (n : ℕ) (qk : fst k ≡ # n) where
          module R = Recover Z n (Env T e' e s k z Z) i2 i4 i6 qk refl (Rd.b-env hb)
            using ( g; recovers )
```

復元された添字は `Z` の提示を通して周囲の値を名指し、復元の等式は、拡張環境が名指すのはまさにこれらの周囲の値であり、その順序は添字の並びどおりであることを言います。

```agda
          g′ : Fin n → V ℓ
          g′ i = ⟪ fst Z ⟫↪ (R.g i)
          hE : fst e ≡ env g′
          hE = R.recovers
```

一意性を示すため、同じ `Z`、パラメータ環境 `e`、論理式のキー `s` をもつ二つの本体の証人を取る。最初の証人のアリティの数項を解読すると、復元されるパラメータ列の共通の長さ `n` が定まる。

```agda
      module WitnessUnique (Z e s z T e' k : CS.S)
        (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩)
        (z' T₂ e'₂ k₂ : CS.S)
        (hb₂ : ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩)
        (n : ℕ) (qk : fst k ≡ # n) where
```

段階の節によって `z` と `z'` は `Lset lam` の要素となるので、その段階の整列順序で比較できる。また、最初の証人の解読から、二つの本体が共有するパラメータ列が得られる。

```agda
        module A₁ = WitnessBody z T e' e s k Z hb
        module A₂ = WitnessBody z' T₂ e'₂ e s k₂ Z hb₂
        module N = A₁.AtNum n qk
        zS : SL
        zS = fst z , A₁.h7
```

二番目の要素も同様にまとめられます。拡張の等式は、それぞれの体の環境が、みずからの証明された要素を加えた拡張であることを言います。`e'` は復元された値の前に `z` を加えたものを名指し、`e'₂` も同じ仕方で `z'` を名指します。

```agda
        z'S : SL
        z'S = fst z' , A₂.h7
        e'≡ : fst e' ≡ env (cons (fst z) N.g′)
        e'≡ = A₁.Rd.b-cons N.g′ N.hE hb
        e'₂≡ : fst e'₂ ≡ env (cons (fst z') N.g′)
```

ついで、二つの表のスロットが一致することが示されます。どちらの体も、鍵 `s` とみずからの表の対が表の族の対に属すると主張し、コードの名指しの単射性が、同じ鍵と対にされた二つの表を等しく強制します。

```agda
        e'₂≡ = A₂.Rd.b-cons N.g′ N.hE hb₂
        T≡ : fst T ≡ fst T₂
        T≡ =
          let p = SM.pairs-out s T (A₁.Rd.b-tab hb)
              q = SM.pairs-out s T₂ (A₂.Rd.b-tab hb₂)
```

表の等式は、二つの表の節の外向きの読みから組み立てられます。各表は鍵が名指す値であり、コードの名指しの単射性が二つの鍵のコードの添字を同一視します。ついで `not-below` が準備されます。より真に小さい構成可能な要素がみずからの体の証人をもち、その拡張が相手の表の内側にあることはあり得ません。

```agda
          in snd p ∙ cong (λ m → fst (SM.valOf s m))
            (snd (fst s ∈ fst (AllCodes A)) (fst p) (fst q)) ∙ sym (snd q)
        not-below : (a b : CS.S) (ha : ⟨ fst a ∈ fst A ⟩) (hb' : ⟨ fst b ∈ fst A ⟩)
                    (Ta e'a ka : CS.S) (hba : ⟨ Env Ta e'a e s ka a Z ⊨ bodyFo ⟩)
                    (e'b : CS.S) → fst e'b ≡ env (cons (fst b) N.g′) → ⟨ fst e'b ∈ fst Ta ⟩
```

構成可能な候補が一方の証人より真に下にあり、その延長された環境が同じ表に属するなら、最小性の節から矛盾が得られる。段階の整列順序が、その節に必要な内部の比較関係を与える。

```agda
                  → relOf wL (fst b , hb') (fst a , ha) → Empty.⊥
        not-below a b ha hb' Ta e'a ka hba e'b qe hm b<a =
          BodyRd.b-min Ta e'a e s ka a Z N.g′ N.hE hba b hb' e'b qe hm
            (relL-fill lam λ-isL ordλ (fst b , hb') (fst a , ha) b<a)
        result : fst z ≡ fst z'
```

結果は、まとめられた二つの証人の上の内部の整列順序の三分法から従います。`z` が `z'` より下なら、より小さい `z` が `z'` の体の記録する最小性と矛盾します。共有された表は表の等式を通して供給されます。

```agda
        result = go (SWO.tri∙ wL zS z'S)
          where
          go : Tri∙ (relOf wL zS z'S) (zS ≡ z'S) (relOf wL z'S zS) → fst z ≡ fst z'
          go (tri-lt h) = Empty.rec (not-below z' z A₂.h7 A₁.h7 T₂ e'₂ k₂ hb₂ e' e'≡
                        (subst (λ t → ⟨ fst e' ∈ t ⟩) T≡ A₁.h6) h)
```

まとめられた二つの証人が等しければ、その基礎にある集合も等しい。残る狭義順序の場合は対称であり、`z'` が `z` より下なら `z` の最小性に矛盾する。

```agda
          go (tri-eq q) = cong fst q
          go (tri-gt h) = Empty.rec (not-below z z' A₁.h7 A₂.h7 T e' k hb e'₂ e'₂≡
                        (subst (λ t → ⟨ fst e'₂ ∈ t ⟩) (sym T≡) A₂.h6) h)
```

最小証人の一意性が組み上がります。同じ `Z`、`e`、`s` に対する二つの証人は、等しい基底要素をもちます。二つの切り詰めは一緒に消費され、目標は h-集合における等式です。

```agda
    opaque
      leastWitness-unique : (Z e s z z' : CS.S) → LeastWitness Z e s z
                          → LeastWitness Z e s z' → fst z ≡ fst z'
      leastWitness-unique Z e s z z' = PT.rec2 (setIsSet (fst z) (fst z')) inner
        where
```

内側の補題は、展開された二つの体の証人を受け取ります。候補の要素 `z` と `z'` のそれぞれに対する表、拡張、鍵、そして体の充足です。

```agda
        inner : (Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
                   ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩)
              → (Σ[ T₂ ∈ CS.S ] Σ[ e'₂ ∈ CS.S ] Σ[ k₂ ∈ CS.S ]
                   ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩)
              → fst z ≡ fst z'
```

最初のキーを数項へ解読すると、先の一意性の議論をそのアリティで行える。同じ解読原理を `ω-num` として記録する。内部の `ω` の各要素は、命題的切り詰めのもとで、ある周囲の数項 `# n` である。

```agda
        inner (T , e' , k , hb) (T₂ , e'₂ , k₂ , hb₂) =
          PT.rec (setIsSet (fst z) (fst z'))
            (λ { (n , qk) → WitnessUnique.result Z e s z T e' k hb z' T₂ e'₂ k₂ hb₂ n qk })
            (decode-num k (BodyRd.b-num T e' e s k z Z hb))
    ω-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
```

解読は、内部の `ω` の要素を数項の等式とともに自然数へ写します。そして `vecOf` は `Fin k` の上の関数を、構成可能な要素の長さ `k` のベクトル、すなわち充足の節が消費する形へ変えます。

```agda
    ω-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
      (subst ⟨_⟩ (ω-specL q) h)
    vecOf : {k : ℕ} → (Fin k → SL) → Vec SL k
    vecOf {zero} f = []
    vecOf {suc k} f = f zero ∷ vecOf (λ i → f (suc i))
```

`vecOf f` の各成分を参照すると `f` が復元される。ここで、集合 `Z`、アリティ `k`、一つの証人変数と `k` 個のパラメータ変数をもつ論理式 `χ`、`Z` から取ったパラメータベクトル `vs`、そして `χ` が `vs` で証人をもつことの証拠を固定する。

```agda
    lookup-vecOf : {k : ℕ} (f : Fin k → SL) (i : Fin k) → lookup i (vecOf f) ≡ f i
    lookup-vecOf {suc k} f zero = refl
    lookup-vecOf {suc k} f (suc i) = lookup-vecOf (λ j → f (suc j)) i
    module Least (Z : CS.S) (k : ℕ) (χ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
                 (from : From Z vs) (w₀ : Sat k χ vs) where
```

最小化される述語は、要素 `a` について、拡張された環境 `(a ∷ vs)` が `χ` を充足することを述べます。これは命題としてまとめられるため、整列順序の最小性の述語として働けます。

```agda
      P : SL → hProp (ℓ-suc ℓ)
      P a = (a ∷ vs) ⊨₀ χ
```

最小証人 `a` は、この述語と非空の記録に対して、`L` の内部の整列順序に沿う最小要素の探索によって選ばれます。

```agda
      a : SL
      a = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .fst
```

その最小性のデータは丸ごと保持されます。`a` は述語を満たし、整列順序のより小さい要素は述語を満たしません。

```agda
      a-least : IsLeast wL P a
      a-least = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .snd
```

選ばれた証人 `a` は `Lset lam` に属するので構成可能であり、構成可能な台の要素 `aS` とみなせる。各パラメータ位置について、`g` はそのパラメータを名指す添字を `Z` の表示から選ぶ。

```agda
      aS : CS.S
      aS = fst a , Lset→isL lam ordλ (fst a) (snd a)
      g : Ix Z k
      g i = fiber (fst Z) (from i) .fst
```

名指しの等式は、各パラメータの添字が提示するのはまさにそのパラメータであることを言います。埋め込まれた添字は、`L` の要素としてそのパラメータに等しいのです。

```agda
      g-val : (i : Fin k) → ⟪ fst Z ⟫↪ (g i) ≡ fst (lookup i vs)
      g-val i = fiber (fst Z) (from i) .snd
```

パラメータの周囲の値は `g′` に集められ、スロットごとに一つです。これによりパラメータの環境は、内部と周囲の両方で記述できます。

```agda
      g′ : Fin k → V ℓ
      g′ i = ⟪ fst Z ⟫↪ (g i)
```

パラメータの環境 `e` は、これらの値の `Z` の上の内部のグラフであり、`ext b` は候補 `b` の拡張環境です。パラメータの前に `b` を加えたものです。

```agda
      e : CS.S
      e = envS Z g
      ext : SL → CS.S
      ext b = envFor A (b ∷ vs)
```

拡張のグラフの等式は、その基底集合が、候補 `b` を周囲のパラメータの値の前に加えたグラフであることを言います。拡張の二つの読みは項目ごとに同一視されます。

```agda
      ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′)
      ext-graph b = envFor-graph A (b ∷ vs)
        ∙ cong env (funExt (λ { zero → refl ; (suc i) → sym (g-val i) }))
```

拡張は、アリティ `suc k` における `χ` の充足の表に属するのは、拡張された環境が `χ` を充足するとき、かつそのときに限ります。ここでの表はこの論理式だけのための表であり、この等式によって、表への所属を充足と読み替えられるのです。

```agda
      ext-sat : (b : SL) → (ext b CS.∈ˢ Tof (suc k) χ) ≡ ((b ∷ vs) ⊨₀ χ)
      ext-sat b = sat-at (suc k) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs))
```

鍵 `sS` は論理式とそのアリティを名指します。表の族が `χ` の表を索引するための対です。

```agda
      sS : CS.S
      sS = keyOf (suc k) χ
```

表 `T` はアリティ `suc k` における `χ` の充足の表であり、充足する拡張が集められる集合です。

```agda
      T : CS.S
      T = Tof (suc k) χ
```

七項目の環境 `γ₇` が全体の絵を組み上げます。表、最小証人による拡張、パラメータの環境、鍵、アリティの数項、まとめられた証人、そして基礎集合 `Z` です。

```agda
      γ₇ : CS.S ^ 7
      γ₇ = Env T (ext a) e sS (nn k) aS Z
```

第一の節は、アリティの数項が内部の `ω` に属することを記録します。環境の長さは自然数だからです。

```agda
      c1 : ⟨ γ₇ ⊨ (var i4 ∈̇ con ωʟ) ⟩
      c1 = #∈ω k
```

鍵の節は、鍵がコードの集合に属し、後続の数項と `χ` のコードの対であることを述べます。このコードは自由コードであり、自由コードは `ω` の極限の段階に住みます。

```agda
      c2 : ⟨ γ₇ ⊨ keyIn i3 i4 ⟩
      c2 = KeyIn.keyIn-in i3 i4 γ₇ k refl
        (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) (sym (keyOf-fst (suc k) χ)) (freeCode-in (suc k) χ))
        (fst (limitCode χ)) (keyOf-fst (suc k) χ)
```

環境の節は、パラメータの環境が `Z` の上の長さ `nn k`、値 `g′` の環境であることを述べます。これは `e` の環境の補題から七項目の文脈へ輸送されます。

```agda
      c3 : ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
      c3 = envOverAt-transport (Z ∷ nn k ∷ e ∷ []) γ₇ i2 i1 i0 i2 i4 i6 refl refl refl
             (envOver Z g)
```

拡張の等式は、最小証人による拡張が、パラメータの値の前に証人を加えたグラフであることを繰り返します。

```agda
      c4 : fst (ext a) ≡ env (cons (fst a) g′)
      c4 = ext-graph a
```

鍵と表の対は、表の族の対に属します。表がみずからの鍵によって索引されるのはこの仕組みです。

```agda
      c5 : ⟨ pr (fst sS) (fst T) ∈ˢ fst SM.pairs ⟩
      c5 = Tof-pair (suc k) χ
```

最小証人による拡張は表に属します。表の所属の等式がそれを `χ` の充足として読み、最小性のデータがまさにその充足を供給するのです。

```agda
      c6 : ⟨ fst (ext a) ∈ˢ fst T ⟩
      c6 = transport (sym (cong ⟨_⟩ (ext-sat a))) (a-least .fst)
```

最小証人は段階 `Lset lam` に属する。内部表示 `A = LsetS lam ordλ` では、これはまさに `a` がもつ所属の証明である。

```agda
      c7 : ⟨ fst aS ∈ˢ fst A ⟩
      c7 = snd a
```

最小性の節は、延長された環境が表に属するような `Lset lam` の各候補 `w'` を排除する。そのまとめられた形が選ばれた証人より真に下にあることはできない。これはまさに `a` の最小性である。

```agda
      c8 : BodyRd.Min T (ext a) e sS (nn k) aS Z g′
      c8 w' w'∈ e'' q hm hr = a-least .snd w'S sat lt'
        where
        w'S : SL
        w'S = fst w' , w'∈
```

より小さい候補と `a` の間の内部の関係は、構成可能な要素に制限した周囲の整列順序から満たされ、候補は `χ` を充足します。その拡張が表に属することを、拡張の等式を通して充足として読むのです。

```agda
        lt' : relOf-at w'S a
        lt' = relL-rep lam λ-isL ordλ w'S a hr
        sat : ⟨ (w'S ∷ vs) ⊨₀ χ ⟩
        sat = transport (cong ⟨_⟩ (ext-sat w'S))
                (subst (λ t → ⟨ t ∈ˢ fst T ⟩) (q ∙ sym (ext-graph w'S)) hm)
```

八つの節を合わせると、`witFo` が `(aS, Z)` で成り立つ。すなわち `a` は、選んだパラメータにおける `χ` の最小証人であり、この事実は構成可能な構造の内部だけで表されている。次に、`Z` の各要素が `Lset lam` に属すると仮定し、同じ本体のデータを周囲で読む。

```agda
      least : ⟨ (aS ∷ Z ∷ []) ⊨ witFo ⟩
      least = witFo-in aS Z T (ext a) e sS (nn k)
        (BodyRd.b-fill T (ext a) e sS (nn k) aS Z g′ refl c1 c2 c3 c4 c5 c6 c7 c8)
    module Out (Z : CS.S) (Z⊆ : (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
               (w T e' e s k : CS.S) (h : ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩) where
```

本体の証人は八つの事実を与える。アリティの数項、キーの形、復元されたパラメータ環境、延長の等式、添字付けられた表、表への所属、段階への所属、そして最小性である。これらを周囲で読むと、コードが表す意味論的な探索を復元できる。

```agda
      module Rd = BodyRd T e' e s k w Z
        using ( b-num; b-key; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
```

段階の節は、証人となる集合 `w` が `Lset lam` に属することを示す。`w` とこの証明を組にすると、段階の台の対応する要素 `wS` が得られる。

```agda
      wS : SL
      wS = fst w , Rd.b-stage h
```

解読されたキーのアリティ成分は内部の `ω` に属する。したがって命題的切り詰めのもとで、ある数項 `# n` に等しい。この `n` を固定すれば、通常の自然数のアリティでキーを分析できる。

```agda
      module AtNum (n : ℕ) (qk : fst k ≡ # n) where
```

この場合の最初の事実は、鍵のスロット成分 `s` がそれ自体コード、すなわち `C₀` の要素であることを言います。これは鍵の逆読みから従います。鍵はアリティの数項とコードの順序対であり、対を分解すればコードが現れます。

```agda
        s∈ : ⟨ fst s ∈ˢ fst C₀ ⟩
        s∈ = KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .fst
```

アリティを `n` と同定すると、環境の節から関数 `g : Fin n → ⟪ fst Z ⟫` が復元され、符号化されたパラメータ環境が、それらの添字の名指す値のグラフであることが示される。

```agda
        module R = Recover Z n (Env T e' e s k w Z) i2 i4 i6 qk refl (Rd.b-env h) using ( g; recovers )
```

復元された環境は、始集合の索引の列です。各索引はその提示の埋め込みによって周囲の要素として実現され、底の集合のベクトル `g′` が得られます。

```agda
        g′ : Fin n → V ℓ
        g′ i = ⟪ fst Z ⟫↪ (R.g i)
```

ベクトル `vs` は、同じ要素を構成可能な台の項目として集め、それぞれに構成可能性の証明を対にします。

```agda
        vs : Vec SL n
        vs = vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i)))
```

各位置 `i` について、`lookup i vs` の第一成分は `g′ i` である。したがって `vs` と `g′` は同じパラメータ列を、一方は段階の台の要素として、他方は周囲の集合として表す。

```agda
        vs-val : (i : Fin n) → fst (lookup i vs) ≡ g′ i
        vs-val i = cong fst (lookup-vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i))) i)
```

復元された環境は、実際に始集合から来ています。`vs` の各項目は、集合として読めば `Z` の要素です。これが `From Z vs` の記録です。

```agda
        from : From Z vs
        from i = subst (λ u → ⟨ u ∈ˢ fst Z ⟩) (sym (vs-val i)) (member (fst Z) (R.g i))
```

復元の等式は、元の環境成分 `e` を `env g′`、すなわち復元された周囲の値から作られるグラフと同定する。

```agda
        hE : fst e ≡ env g′
        hE = R.recovers
```

証人のスロットは、復元された環境を一項目だけ延ばすことで他の候補と比較されます。`ext b` は `b` を `vs` の前に置いた環境です。

```agda
        ext : SL → CS.S
        ext b = envFor A (b ∷ vs)
```

この延長の底の環境は、`b` の底の集合と `g′` の cons として計算され、延長された環境のグラフの記述は項目ごとに一致します。

```agda
        ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′)
        ext-graph b = envFor-graph A (b ∷ vs)
          ∙ cong env (funExt (λ { zero → refl ; (suc i) → vs-val i }))
```

鍵自身の環境成分は `ext wS` と同一視されます。復元された環境を証人のスロットで延ばしたものが、まさに鍵が記録していたものです。

```agda
        e'≡ : fst e' ≡ fst (ext wS)
        e'≡ = Rd.b-cons g′ hE h ∙ sym (ext-graph wS)
```

ここでコード成分から解読された論理式 `χ` を取り、`s` をその正準なキー `keyOf (suc n) χ` と同定する。これで環境、論理式、キーはすべて同じ充足の問いを表す。

```agda
        module AtCode (χ : Formula (⊥* {ℓ}) (suc n)) (qs : fst s ≡ fst (keyOf (suc n) χ)) where
```

述語 `P b` は、`b` を復元された環境の前に置けば `χ` を充足することを言います。これが、最小の証人の探索が最小化する性質です。

```agda
          P : SL → hProp (ℓ-suc ℓ)
          P b = (b ∷ vs) ⊨₀ χ
```

`χ` の充足表への所属は `P b` と一致します。`ext b` の環境が `b ∷ vs` のグラフとして計算されるからです。これが、充足の符号化された読みと意味論的な読みを切り替えます。

```agda
          ext-sat : (b : SL) → ⟨ ext b CS.∈ˢ Tof (suc n) χ ⟩ ≡ ⟨ P b ⟩
          ext-sat b = cong ⟨_⟩ (sat-at (suc n) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs)))
```

鍵の表の成分は、アリティを上げた `χ` の充足表と同一視されます。両成分が解読されれば、鍵の要素を意味論的に読めます。

```agda
          module AtTable (qT : fst T ≡ fst (Tof (suc n) χ)) where
```

証人のスロットは、復元された論理式を充足します。鍵に記録された所属が、環境と表の同一視に沿って運ばれ、延長された環境のもとでの `χ` の充足になります。

```agda
            sat : ⟨ P wS ⟩
            sat = transport (ext-sat wS)
              (subst2 (λ u t → ⟨ u ∈ˢ t ⟩) e'≡ qT (Rd.b-mem h))
```

最小性は、`χ` を充足して `wS` より真に下にある段階の要素 `b` が存在しないことを述べる。`χ` の充足は `ext b` が復元された表に属することへ読み替えられ、段階の整列順序は本体の最小性の節が要求する内部関係へ変換される。

```agda
            min : (b : SL) → ⟨ P b ⟩ → relOf-at b wS → Empty.⊥
            min b pb lt = Rd.b-min g′ hE h bS (snd b) (ext b) (ext-graph b) hm
              (relL-fill lam λ-isL ordλ b wS lt)
              where
              bS : CS.S
```

より小さい候補は構成可能な要素 `bS` として包まれ、その延長された環境が表の中にあることが示されます。これこそ、鍵の最小性が反証する所属です。

```agda
              bS = fst b , Lset→isL lam ordλ (fst b) (snd b)
              hm : ⟨ fst (ext b) ∈ˢ fst T ⟩
              hm = subst (λ t → ⟨ fst (ext b) ∈ˢ t ⟩) (sym qT) (transport (sym (ext-sat b)) pb)
```

二つの事実は、復元された環境のもとでの `χ` の充足可能性の証人へと合成されます。証人のスロットとその充足が、`Sat` へと切り詰められるのです。

```agda
            w₀ : Sat n χ vs
            w₀ = ∣ wS , sat ∣₁
```

復元されたアリティ `n`、論理式 `χ`、パラメータベクトル `vs`、証人 `w₀` が意味論的な探索をなす。最小要素の一意性により、その結果 `search n χ vs w₀` は元の証人集合 `w` と同定される。一方、表の節から、復元された表が `χ` の充足表であることの証明が始まる。

```agda
            searched : Searched Z (fst w)
            searched = n , χ , vs , w₀ , (from , sym (cong (λ q → fst (fst q))
              (isPropLeastOf wL P (leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀) (wS , (sat , min)))))
          table : ∥ Searched Z (fst w) ∥₁
          table = ∣ AtTable.searched
```

表の節は `T` の基礎にある集合を、キー `s` に対応する値として表す。`s` はすでに、アリティ `suc n` における `χ` の正準なキーと同定されているので、そのキーにおける値の一意性から `fst T ≡ fst (Tof (suc n) χ)` が得られる。

```agda
            (snd p ∙ cong fst (valOf-same s (fst p) (suc n) χ qs)) ∣₁
            where
            p : Σ[ m ∈ ⟨ s CS.∈ˢ AllCodes A ⟩ ] (fst T ≡ fst (SM.valOf s m))
            p = SM.pairs-out s T (Rd.b-tab h)
```

コード成分 `s` を解読するため、`freeCode-out` は、その自由コードがこの成分である論理式 `χ` を与える。スロットの等式、解読されたコードの等式、`keyOf` の計算の等式を順に合成すると、`s` は `χ` の正準なキーと同定される。

```agda
        code : ∥ Searched Z (fst w) ∥₁
        code = PT.rec squash₁
          (λ { (c , qc) → PT.rec squash₁
            (λ { (χ , ec) → AtCode.table χ
                   (qc ∙ cong (pr (# (suc n))) ec ∙ sym (keyOf-fst (suc n) χ)) })
```

キーの等式が、符号化されたスロットと解読された論理式を結ぶ最後の関係を与える。したがってこの数項の場合には、切り詰められた `Searched Z (fst w)` が得られる。証人集合は、`Z` から復元したパラメータによる最小証人探索の結果にほかならない。

```agda
            (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) qc s∈)) })
          (KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .snd)
```

各本体の証人に記録されたアリティは内部の `ω` に属するので、数項の解読により、先の分析から各証人について切り詰められた意味論的探索が得られる。分出の上界には `Bnd Z = Z ∪ A` を取り、`A` は `Lset lam` の内部表示である。

```agda
      searched : ∥ Searched Z (fst w) ∥₁
      searched = PT.rec squash₁ (λ { (n , qk) → AtNum.code n qk }) (ω-num k (Rd.b-num h))
    Bnd : CS.S → CS.S
    Bnd Z = cupʟ Z A
```

`Z` の要素は、和の左の包含によって上界の中に入ります。

```agda
    bnd-Z : (Z z : CS.S) → ⟨ fst z ∈ˢ fst Z ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩
    bnd-Z Z z = cupʟ-inl Z A (fst z)
```

`Lset lam` の各要素は右側の包含によって `Bnd Z` に入る。一段階の閉包条件には三つの場合がある。`Z` の既存の要素、証人がないときに使う空集合、または基礎 `Z` とともに `witFo` を充足する集合 `w` である。

```agda
    bnd-L : (Z z : CS.S) → ⟨ fst z ∈ˢ Lset lam ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩
    bnd-L Z z = cupʟ-inr Z A (fst z)
    Body : CS.S → CS.S → Type (ℓ-suc ℓ)
    Body Z w = ⟨ fst w ∈ˢ fst Z ⟩ ⊎ ((fst w ≡ ∅) ⊎ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩)
```

第三の場合、`witFo` に符号化された段階の節が `w ∈ Lset lam` を直接示す。したがって新たに加えられる最小証人はすべて固定した段階の内部にとどまる。

```agda
    wit-L : (Z w : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ → ⟨ fst w ∈ˢ Lset lam ⟩
    wit-L Z w hw = PT.rec (snd (fst w ∈ˢ Lset lam))
      (λ { (T , e' , e , s , k , h) → BodyRd.b-stage T e' e s k w Z h })
      (witFo-out w Z hw)
    opaque
```

分出の論理式は、構成可能な構造の内部で三つの場合を表す。`Z` への所属、空集合との等しさ、または改名された `witFo` の充足である。改名は、その二つの自由変数を存在量化で作られた位置に配置する。

```agda
      sepFo : CS.S → Formula CS.S 1
      sepFo Z = (var i0 ∈̇ con Z)
              ∨̇ ( (var i0 ≐ con ∅ʟ)
                ∨̇ ∃̇ ( (var i0 ≐ con Z) ∧̇ renameFo ρs witFo ) )
```

この改名は環境の二つの成分を交換するだけである。したがって、改名された `witFo` を `(Z'', w)` で評価した真理値は、元の `witFo` を `(w, Z'')` で評価した真理値に等しい。

```agda
      private
        rs : (Z'' w : CS.S)
           → ⟨ (Z'' ∷ w ∷ []) ⊨ renameFo ρs witFo ⟩ ≡ ⟨ (w ∷ Z'' ∷ []) ⊨ witFo ⟩
        rs Z'' w = cong ⟨_⟩ (Ren.⊨-rename ρs witFo (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ []) (ags Z'' w))
```

分出の論理式の充足は、本体の三つの切り詰められた場合に分解されます。`Z` への所属、空集合との等号、あるいは、その証人が定義域を指認する存在の場合です。

```agda
      sep-out : (Z w : CS.S) → ⟨ (w ∷ []) ⊨ sepFo Z ⟩ → ∥ Body Z w ∥₁
      sep-out Z w = PT.rec squash₁ (λ
        { (inl hz) → ∣ inl hz ∣₁
        ; (inr h') → PT.rec squash₁ (λ
          { (inl e) → ∣ inr (inl e) ∣₁
```

存在の場合、その証人 `Z''` は固定したパラメータ `Z` に等しい。この等しさに沿って移送し、さらに改名のパスに沿って移送すると、`witFo` が `(w, Z)` で成り立つことが得られる。

```agda
          ; (inr hw) → PT.map (λ { (Z'' , (eZ , hr)) → inr (inr
              (subst (λ u → ⟨ (w ∷ u ∷ []) ⊨ witFo ⟩) (S≡ {x = Z''} {y = Z} eZ)
                (transport (rs Z'' w) hr))) }) hw }) h' })
```

逆に、本体の三つの場合はそれぞれ、分出の論理式の対応する充足を産み、必要なところで名前の付け替えを包み直します。

```agda
      sep-in : (Z w : CS.S) → Body Z w → ⟨ (w ∷ []) ⊨ sepFo Z ⟩
      sep-in Z w (inl hz) = ∣ inl hz ∣₁
      sep-in Z w (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁
      sep-in Z w (inr (inr hw)) = ∣ inr ∣ inr ∣ Z , (refl , transport (sym (rs Z w)) hw) ∣₁ ∣₁ ∣₁
```

`L` の内部で分出を行い、`Bnd Z` から `sepFo Z` を充足する集合だけを選ぶ。その構成可能集合を `Φ Z` とする。その所属のパスは、`Φ Z` への所属を、上界への所属と論理式の充足との組に同定する。

```agda
    opaque
      Φ : CS.S → CS.S
      Φ Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .fst
```

所属の仕様は次のように読めます。`w` が `Φ Z` に属するのは、`w` が上界 `Bnd Z` に属し、分出の論理式を満たすとき、そのときに限ります。

```agda
      Φ-mem : (Z w : CS.S) → (w CS.∈ˢ Φ Z) ≡ ((w CS.∈ˢ Bnd Z) ⊓ ((w ∷ []) ⊨ sepFo Z))
      Φ-mem Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .snd
```

本体のどの場合も `Φ Z` に着地します。所属の場合は上界を通って入り、証明は、各選言支から産み出される上界への所属を、分出の充足とともに包みます。

```agda
    Φ-in : (Z w : CS.S) → Body Z w → ⟨ fst w ∈ˢ fst (Φ Z) ⟩
    Φ-in Z w b = subst ⟨_⟩ (sym (Φ-mem Z w)) (bnd b , sep-in Z w b)
      where
      bnd : Body Z w → ⟨ w CS.∈ˢ Bnd Z ⟩
      bnd (inl hz) = bnd-Z Z w hz
```

空集合の場合は `∅ ∈ Lset lam` によって上界に属する。証人の場合も、`witFo` の段階の節がその値の `Lset lam` への所属を示すので、上界に属する。

```agda
      bnd (inr (inl e)) = bnd-L Z w (subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym e) HSH.∅∈Lsetα)
      bnd (inr (inr hw)) = bnd-L Z w (wit-L Z w hw)
```

逆に、`Φ Z` への所属からは、所属の仕様と分出の読みを通して、切り詰められた本体の場合が得られます。同値の論理式のために、本体は三つの枠の並びへ書き直されます。

```agda
    Φ-out : (Z w : CS.S) → ⟨ fst w ∈ˢ fst (Φ Z) ⟩ → ∥ Body Z w ∥₁
    Φ-out Z w h = sep-out Z w (subst ⟨_⟩ (Φ-mem Z w) h .snd)
    opaque
      bodyF : Formula CS.S 3
      bodyF = (var i0 ∈̇ var i2) ∨̇ ((var i0 ≐ con ∅ʟ) ∨̇ renameFo ρf witFo)
```

グラフの論理式 `ΦFo` は新しい集合 `w` を全称量化し、`w ∈ Z'` と三つの場合からなる条件 `Body Z w` の間の二つの含意を述べる。したがって `(Z', Z)` が `ΦFo` を充足するのは、`Z'` と `Φ Z` が同じ要素をもつとき、かつそのときに限る。

```agda
      ΦFo : Formula CS.S 2
      ΦFo = ∀̇ ( ((var i0 ∈̇ var i1) ⇒̇ bodyF) ∧̇ (bodyF ⇒̇ (var i0 ∈̇ var i1)) )
```

グラフのための改名の同値は、前のものと同じように証明されます。改名は環境を入れ替え、充足はその入れ替えに沿って運ばれます。

```agda
      private
        rf : (w Z' Z : CS.S)
           → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ renameFo ρf witFo ⟩ ≡ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
        rf w Z' Z = cong ⟨_⟩ (Ren.⊨-rename ρf witFo (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ []) (agf w Z' Z))
```

本体は、三つの枠の並びの下で双方向に移ります。`Z` への所属は直接であり、残りの選言支は切り詰めの上で写されます。

```agda
        bodyF-out : (w Z' Z : CS.S) → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩ → ∥ Body Z w ∥₁
        bodyF-out w Z' Z = PT.rec squash₁ (λ
          { (inl hz) → ∣ inl hz ∣₁
          ; (inr h') → PT.map (λ
            { (inl e) → inr (inl e)
```

証人の場合、改名のパスは三変数の論理式の充足を `(w, Z)` における `witFo` の充足へ戻し、グラフの本体から `Body Z w` への順方向の含意を完成させる。

```agda
            ; (inr hw) → inr (inr (transport (rf w Z' Z) hw)) }) h' })
```

逆方向は、三つの場合を三つの枠の読みに組み立て、Witnessの選言支を改名に対して運びます。

```agda
        bodyF-in : (w Z' Z : CS.S) → Body Z w → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩
        bodyF-in w Z' Z (inl hz) = ∣ inl hz ∣₁
        bodyF-in w Z' Z (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁
        bodyF-in w Z' Z (inr (inr hw)) = ∣ inr ∣ inr (transport (sym (rf w Z' Z)) hw) ∣₁ ∣₁
```

続いて、定義可能性の条項が証明されます。対 `(Φ Z, Z)` はグラフの論理式を充足します。同値のそれぞれの向きは、対応する所属の向きと本体の転送の合成です。

```agda
      Φ-defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩
      Φ-defines Z w =
          (λ h → PT.rec (snd ((w ∷ Φ Z ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in w (Φ Z) Z) (Φ-out Z w h))
        , (λ h → PT.rec (snd (fst w ∈ˢ fst (Φ Z))) (Φ-in Z w) (bodyF-out w (Φ Z) Z h))
```

グラフの一意性は、構成可能な構造の外延性によって証明されます。`Z` との対がグラフの論理式を充足する任意の `Z'` のすべての要素は本体を満たし、`Φ-in` がそれを `Φ Z` の中に置きます。

```agda
      Φ-only : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
      Φ-only Z Z' h = extensionalL (λ v → ⇔toPath (fwd v) (bwd v))
        where
        fwd : (v : CS.S) → ⟨ fst v ∈ˢ fst Z' ⟩ → ⟨ fst v ∈ˢ fst (Φ Z) ⟩
        fwd v hv = PT.rec (snd (fst v ∈ˢ fst (Φ Z))) (Φ-in Z v) (bodyF-out v Z' Z (h v .fst hv))
```

外延性の議論の逆方向は、`Φ Z` の各要素を切り詰められた本体の場合として読み、その要素のもとでグラフの論理式を適用します。

```agda
        bwd : (v : CS.S) → ⟨ fst v ∈ˢ fst (Φ Z) ⟩ → ⟨ fst v ∈ˢ fst Z' ⟩
        bwd v hv = h v .snd
          (PT.rec (snd ((v ∷ Z' ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in v Z' Z) (Φ-out Z v hv))
```

これで定義可能な一段階の演算 `Φ` が得られた。論理式 `ΦFo` がそのグラフを特徴づけ、外延性により、そのグラフ条件を満たす任意の集合は `Φ Z` に等しい。

```agda
    pack : StepPack
    pack = record
      { Φ       = Φ
      ; ΦFo     = ΦFo
      ; defines = Φ-defines
```

この一段階は `Z` の既存の各要素を含み、常に空集合を含み、さらに `Z` の要素をパラメータとする充足可能な各論理式の最小証人を含む。逆に、その要素はこの三つの場合からしか生じないので、`Φ` は求める一段階の閉包にほかならない。

```agda
      ; only    = Φ-only
      ; grows   = λ Z z hz → Φ-in Z (z , isL-trans {x = fst Z} {y = z} hz (snd Z)) (inl hz)
      ; junk    = λ Z → Φ-in Z ∅ʟ (inr (inl refl))
      ; least   = λ Z k χ vs from w₀ →
                    Φ-in Z (Least.aS Z k χ vs from w₀) (inr (inr (Least.least Z k χ vs from w₀)))
```

`Z` の各要素が `Lset lam` に属すると仮定する。`z ∈ Φ Z` なら、所属の特徴づけから三つの可能性が得られる。`z` がすでに `Z` に属する場合、`z = ∅` の場合、または `witFo` が `(z, Z)` で成り立つ場合である。第三の場合、本体を解読すると、`Z` の要素をパラメータとし、結果が `z` である意味論的探索が復元される。

```agda
      ; out     = λ Z Z⊆ z hz → PT.rec squash₁ (λ
          { (inl h') → ∣ inl h' ∣₁
          ; (inr (inl e)) → ∣ inr (inl e) ∣₁
          ; (inr (inr hw)) → PT.rec squash₁
              (λ { (T , e' , e , s , k , hb) →
```

証人の場合、`z ∈ Φ Z` からまず `z` の構成可能性が得られ、`z` を構成可能な台の要素として読める。解読された本体はさらに `Searched Z z` を示し、`z` を復元された論理式とパラメータが定める最小証人探索と同定する。

```agda
                 PT.map (λ sr → inr (inr sr)) (Out.searched Z Z⊆ (zS Z z hz) T e' e s k hb) })
              (witFo-out (zS Z z hz) Z hw) })
          (Φ-out Z (zS Z z hz) hz) }
      where
      zS : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → CS.S
```

`Φ Z` は構成可能であり、構成可能性は推移的なので、`Φ Z` の各要素 `z` も構成可能である。

```agda
      zS Z z hz = z , isL-trans {x = fst (Φ Z)} {y = z} hz (snd (Φ Z))
```

## 凝縮に必要な構成可能性の前提を与える

これにより先の解読に必要な台の要素が得られ、定義可能な一段階の閉包の構成が完成する。

```agda
module Discharge (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
```

包 `M` 自身が構成可能であると仮定します。これにより `M` を構成可能な台として扱えるので、包が推移的であると仮定せずに、先の崩壊の議論を適用できます。

```agda
  (M-isL : ⟨ isL (HullStage.M lam ordλ succλ X X⊆L ∅∈λ) ⟩) where
```

`M` を構成可能な台とみなすと、その崩壊像 `πX` が得られます。この像の各要素は `M` のある要素の崩壊値であり、構成可能な台についての定理から、そのような値は `L` に属します。

```agda
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
  module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX )
  module P = PiIn (HS.M , M-isL) using ( πX-isL )
```

したがって、すべての `x ∈ πX` は構成可能です。ここで、`X` から `Lset λ` の内部で生成される包に戻ります。`λ` は後続について閉じた順序数であり、`X` の各要素はこの段階に属すると仮定します。

```agda
  pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩
  pixL = P.πX-isL
module Condense′ (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
```

さらに、`∅ ∈ λ`、`X` から生成される包の枠組みの初等性、`λ` が強化された十分な段階であること、および `X` 自身の構成可能性を仮定します。最後の仮定は内部の有限反復の始点を与え、初等性と強化された十分性は凝縮の議論に必要な仮定を与えます。

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  where
```

この構成は三つの部分からなります。コードが初期要素と後の探索で選ばれる値を指し、探索に証人がない場合は空集合を値とします。一つの定義可能な演算 `Φ` が一段の閉包を行い、`Φ` を有限回反復して合併を取ることで、後に Skolem 包と同一視される構成可能集合を作ります。

```agda
  module T = Telescope lam ordλ succλ X X⊆L ∅∈λ using ( Code; val; Reads; module StepPack )
  module TB = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ using ( pack; Φ )
  module HI = Telescope.HullIter lam ordλ succλ X X⊆L ∅∈λ X-isL TB.pack
    using ( hullL; hullL-spec; hullStep; hullStep-suc; hullStep-in; hullStep⊆Hull; depth; M-isL )
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
```

有限な閉包段階の合併は、すでに構成可能宇宙の要素 `hullL` になっています。次の等式により、その台集合が周囲で定義された包 `M` にほかならないことを示します。これが、先に崩壊像を扱う際に仮定した包全体の構成可能性を与えます。

```agda
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX )
  module D = Discharge lam ordλ succλ X X⊆L ∅∈λ HI.M-isL using ( pixL )
  hullL : CS.S
  hullL = HI.hullL
```

`hullL` の台集合はちょうど `M` です。したがって、Skolem 包の周囲での特徴づけと、反復から得た構成可能集合は同じ要素を記述し、`hullL` はさらに構成可能性の証明も備えています。

```agda
  hullL-spec : fst hullL ≡ HS.M
  hullL-spec = HI.hullL-spec
```

殻の閉包の段階は自然数で添字づけられます。`hullStep n` は閉包の段階を `n` 回適用して到達する層です。

```agda
  hullStep : ℕ → CS.S
  hullStep = HI.hullStep
```

後続の添字では、次の段階は現在の段階に `Φ` を作用させたものです。この演算は現在の要素を保ち、空集合を加え、さらにパラメータがすでに現れている各符号化された探索について最小証人を加えます。

```agda
  hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ TB.Φ (hullStep n)
  hullStep-suc = HI.hullStep-suc
```

各コードには有限の深さがあり、それが指す値はその深さの閉包段階に属します。包の各要素は何らかのコードで表されるので、その要素を含む有限段階が得られますが、要素ごとに正準的なコードを選ぶわけではありません。

```agda
  hullStep-in : (c : T.Code) → ⟨ fst (T.val c) ∈ˢ fst (hullStep (HI.depth c)) ⟩
  hullStep-in = HI.hullStep-in
```

逆に、各有限閉包段階のすべての要素は `M` に属します。包の要素の符号による特徴づけと合わせると、これにより段階の合併と Skolem 包がまったく同じ要素をもつことが分かります。

```agda
  hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ HS.M ⟩
  hullStep⊆Hull = HI.hullStep⊆Hull
```

段階の合併は構成可能です。殻の段階 `M` は `L` の要素です。これが本章が証明を目指した二つの所属の事実のうちの一つです。

```agda
  M-isL : ⟨ isL HS.M ⟩
  M-isL = HI.M-isL
```

第二の事実は処理を通して従います。殻の段階 `M` の崩壊 `πX` のすべての値が構成可能なのは、台 `M` が構成可能だからです。

```agda
  pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩
  pixL = D.pixL
```

凝縮により、崩壊像がちょうど `Lset β` となる順序数 `β` が得られます。これにより、先の要素ごとの構成可能性は、像全体を構成可能階層の一つの段階と同一視する主張へ強められます。結論が主張するのはこの等式と `β` の順序数性であり、`β` と `λ` の間の比較までは含みません。

```agda
  condenses′ : Σ[ β ∈ S ] (IsOrd β × (HSC.πX ≡ Lset β))
  condenses′ = Condense.condenses lam ordλ succλ X X⊆L ∅∈λ elem sup D.pixL
```