名字比较的公式

同一个可定义子集可能有许多名字。在元语言中，一个名字由三份数据组成：元数 k、具有 suc k 个变元位的无参公式，以及取自载体的 k 个参数所成的向量。名字的指称由这三份数据派生：多出的那个变元表示待判断的元素，其余变元接收参数向量。因此，指称不是名字的第四个分量。

为了在 L 内表达这些数据，本章把参数向量表示为有穷环境图，并用满足关系图表示公式的读取。在真实的公式键处，satGraphAt 把该键关联到所有满足该公式的环境所成的集合。因此，它的输出恰是这个满足环境集。NameAt 把元数、无参公式码和参数环境与派生的指称联系起来；后文量化竞争名字时，它们都要具有同一个指称。

名字按字典序比较：先由极限层上的序比较公式码，再比较元数，最后依载体上给定的序比较参数向量。公式 ≺At 表达这三种情形。LeastNameAt 只陈述当前名字没有同指称而更小的名字；真正选出最小名字的是前文的 CanonicalNames.leastName。StepAt 在局部量化两条最小名字并比较它们。本章完成的充分性恰好止于 ≺At 与元语言关系 _≺ₙ_ 的对应；NameAt、LeastNameAt 与 StepAt 的完整充分性由后续发展给出。

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

底层语言供给宇宙层级、有穷指标、向量与取值为命题的陈述。经典推理只经一个显式假设 LEM (ℓ-suc ℓ) 进入；它的层级足以承载下文使用的满足关系构造与良序。保留这个显式假设，有助于区分「只陈述一项性质」与「真正选出一个见证」这两类步骤。

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

现在固定宇宙层级 ℓ，并在所需的更高层级上假设排中律。这是本章沿用的经典逻辑接口。下面的公式构造器只组合语法，但它们使用的自然数对象、满足关系图、极限层码序和典范名字理论都在同一假设下构造。因此，本模块如实记录这些语义依赖，而不再次作选择。LeastNameAt 表达最小性；实际选出最小名字的构造仍是 CanonicalNames.leastName。

module L.Choice.NameComparison {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

对象语言能够陈述隶属与相等，组合命题，并在整个载体或某个集合上量化；它的语义在取值为命题的结构中读取。常元映射连接后文所需的三种呈现：真正的无参公式、空字母表上的公式，以及在可构造载体上解释的同一语法。这些映射保持公式结构，因此后文可以在内部辨认一个无参骨架的码。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed )

公式码、有序对与数码本身都是累积层级中的集合。可构造子结构提供读取这些公式的载体；传递性则使码集中的隶属事实能够供给其分量所需的可构造性。配对编码与数码编码的单射性将在后文从相等的键中恢复元数与骨架码。诸 Lset 层为极限层码序提供背景。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset )
open import L.Ordinal {ℓ} using ( ∈#-elim; #∈#-elim )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ; extensionalL )

元数由内部自然数集中的数码表示，参数向量则由有穷环境的图表示。对象语言公式能够检查有序对、应用与定义域，把一个待判断的元素加入环境，并以外延方式定义子集。对于载体上的一条公式，Sat 是所有满足该公式的环境所成的集合。后文从满足关系图恢复的正是这个集合值。

open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro; envOverAt )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in-both; numL; sucAtL; sucAtL-adequate; consAtL )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )

满足关系已经被组织成一张表，其中每个条目把子公式键与递归确定的满足环境集配成一对。槽位闭包与全性保证递归所需的每个真实键都有条目，满足关系桥则把公式中的常元认作所选载体的元素。因此，本章可以读取某个键处已经存下的集合值，而无须重新运行满足关系递归。

open import L.Coding.SatisfactionTable {ℓ} lem
  using ( slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.CodeSet {ℓ} lem

对每个载体，AllCodes 恰好收集该载体上所有真实的公式键；它的两个方向把成员关系与相应公式联系起来。统一满足关系桥由此支持关系公式 satGraphAt B x y：当 x 是槽位 B 所持载体上的真实键时，y 就是相应的满足环境集。GraphWitAt 与两条图读式揭示这项集合值关系，而无须启动新的递归。

  using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge )
open import L.Coding.SatisfactionGraph {ℓ} lem using
  ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
  ; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )

环境塔与带标签的递归数据证明满足关系图的读法对每种语法构造都成立。与这套内部机制相对照，典范名字理论供给名字比较所遵循的元语言标准。元语言的 Name 存储元数、无参公式与参数向量；limitCode 从公式派生第一个比较键，而指称则另由满足关系派生。后文的槽位公式必须保持这一区分。

open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )

名字的码是极限层的成员，并由 limitOrder 比较。第三个键来自载体上任意给定的严格良序。典范命名理论已经把这两项与自然数元数组合成 _≺ₙ_，证明该关系良基，并在 leastName 中使用它。本章让两个非数值的序经带有表示律的关系槽位出现，因而只描述它们所决定的比较，而不重新构造其中任何一个序。

open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )

自然数序供给第二个比较键：当元数表示为数码时，一个数码隶属于另一个数码正好表达严格小于。有穷指标用于定位参数向量的分量，以及两个向量最早出现差异的位置。后文的充分性论证对共同长度作归纳，证明这种「首次相异」描述与 _≺ₙ_ 所用的递归向量序一致。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )

证明数据遵循字典序的形状。依值对携带某个位置及其证据，余积则区分码、元数与参数三种情形。前面诸键的相等性允许把依值公式与向量运输到共同元数，再比较下一个键。空类型给出无常元公式所需的唯一常元解释。

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2 )

存在式与析取式的满足语义带有命题截断：它保留「见证存在」，却忘掉给出的是哪个见证。因此，从公式码或名字比较向外读取时，结论仍是经过命题截断的存在性，而消去也只进入命题。这里发生的是命题截断；命题降级并未在此出现。累积层级则供给集合值的隶属关系，以及这些读式之后所需的外延相等原则。

open import Cubical.Foundations.Transport using ( constSubstCommSlice )
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

层级集合的小成员能够嵌入外围层级；该嵌入的单射性将在后文把已表示参数的相等恢复为载体中的相等。空集充当空字母表：它没有常元，因此从它出发的映射唯一确定，无参公式在所需的重标记下保持同一个码。冯·诺伊曼数码 # k、它们的后继与 ω 则提供环境定义域和名字比较所用的内部元数。

  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω; sucV )

下文的公式都解释在可构造宇宙中。打开 hPropStructure 𝒮ʟ 便固定了它们的载体 S：载体的一个元素是环境宇宙中的一个集合，连同它可构造的证据。这个操作也把该结构中取命题值的等词与隶属关系带入作用域。因此，自由变元与常元都在可构造集合中取值；证明需要使用某条等词或隶属命题的证据时，⟨_⟩ 则取出该命题的底层类型。

open hPropStructure 𝒮ʟ

同一套句法有两种彼此相容的读法。这个绝对性实例从环境宇宙结构 𝒮ᵥ 出发，把它限制到传递类 isL。在外层读法中，一个可构造集合经其底层的环境集合来读取；在内层读法中，常元指称为它命名的那个可构造集合，而等词与隶属由限制后的结构解释。本章把内层满足关系改名为 ⊨。因此，对 γ : S ^ n，判断 γ ⊨ F 表示公式 F 在 L 内部、有限环境 γ 下成立。这正是 L 自身识别并比较名字时所需的读法。

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

这些公式用环境中的位置指向先前给定的数据。每进入一层新的约束，原有位置都必须越过新绑定的取值；经过两层约束后，位置 i 因而变成 suc (suc i)。缩写 sh2 记录的正是这次移动。FreeAt 先绑定后继元数及其码键，再读取骨架与空字母表码集时会用到它；指称条件先绑定候选元素及其扩展环境，再读取原参数环境时也会用到它。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

在指称条件内部，须等四个取值进入环境之后，才会读取骨架与载体的码集。这四个取值依次是候选元素 z、扩展环境 c、它的定义域 k，以及正在考察的键。因此，原来的位置必须连续提升四次。sh4 恰好执行这次移位，使公式既能要求该键属于载体的码集，也能要求它等于由 k 与骨架组成的对。

  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

再有一层存在量词绑定与该键相配的取值 v，所以调用 satGraphAt 时，载体的位置已隔着五个新取值。这里的 v 是满足被编码公式的诸环境所成的集合，并不是真值；紧接着的隶属原子询问扩展环境是否属于这个集合。同一档移位还出现在 LexAt 中：依次绑定一个序号、两个环境在该处的取值、一个更早的序号，以及见证两边相符的共同取值后，原参数环境也恰好隔着五个位置。sh5 统一记录了两处的下标计算。

  sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n)))))
  sh5 i = suc (suc (suc (suc (suc i))))

同一个码，落在空字母表上

空字母表是空集成员的小表示 ⟪ ∅ ⟫。如果 m 是其中一个符号，那么嵌入 ⟪ ∅ ⟫↪ 会给出一个环境集合，而表示定律会断言这个集合属于 ∅。定理 ∅-empty 恰好排除了这种证据，由此得到 noAlpha m。所以，这个字母表上的公式不可能含有常元节点。它们给出了无参公式的一种句法呈现；要把它与元层面名字所用的空常元域 ⊥* 联系起来，只须关联这两个空类型。

private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)

Fo∅ n 是公式族 Formula ⟪ ∅ ⟫ n 的简称，也就是空字母表上具有 n 个可用变元位置的公式。它们不含常元，这是由常元符号的类型保证的，并非另有一个作用于公式的谓词。元层面名字使用与之平行的公式族 Formula ⊥* n。更确切地说，一个 Name 存储元数、在这个公式族中多出一个变元位置的无参公式，以及具有该元数的参数向量；指称由这三份数据派生，并不是另一个存储分量。

  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫

映射 ε 把空字母表 ⟪ ∅ ⟫ 送到空常元域 ⊥*。给定一个假想的源符号 m，noAlpha m 导出矛盾，再由空型消去得到所需的目标。因此，mapFo ε 把 ⟪ ∅ ⟫ 上的公式改名为 ⊥* 上的公式；反方向则可把 embed 特化为从 ⊥* 到 ⟪ ∅ ⟫ 的改名。两种操作都不会改变任何常元出现，因为本来就没有常元。改名的复合法则因而给出空字母表刻画所需的精确公式码等式。

  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = Empty.rec (noAlpha m)

要在模型内部识别无参公式的码，首先必须联系「没有常元」的两种表示。以⟪ ∅ ⟫ 为常元域的公式 ψ，其常元来自空集的成员；而 mapFo ε ψ 把同一份语法表示在空类型 ⊥* 上。若假定空集有一个成员便会得到矛盾，所以映射 ε得以定义。于是，直接把 ψ 读入宇宙，与先沿 ε 改名再嵌入宇宙，两者的差别只在于从空类型出发的映射。函数外延性判定这些映射相等，mapFo-comp 再判定复合改名相等。因此，sameCode 首先证明所得宇宙公式本身相等；稍后对这条等式施用编码映射，便得到相应码的等式。

  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m)))
             ∙ sym (mapFo-comp ε Empty.rec* ψ)

反向的比较从无参公式 χ : Formula ⊥* n 出发。可以先把它嵌入以 ⟪ ∅ ⟫为常元域的公式，再沿该字母表到宇宙的包含映射改名；也可以把它直接嵌入宇宙上的公式。由 mapFo-comp，第一条路线就是一次从 ⊥* 出发的改名；而从 ⊥*出发的任意两个函数都相等，所以这次改名正是直接嵌入所用的改名。sameCode'给出的等式方向，恰好能把 AllCodes ∅ʟ 赋予嵌入公式的键，转换成 χ 通常的宇宙公式码所组成的键。

  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))

这里还有一个依值类型问题。元数属于公式类型的一部分，所以等式 e : i ≡ j会把 ψ : Fo∅ i 移到 subst Fo∅ e ψ : Fo∅ j。然而完成这次迁移后，键中的公式码应当保持不变。读取并编码公式的函数以固定的宇宙 V ℓ 为值域，而该值域不依赖元数索引。因此，一般的替换计算 constSubstCommSlice 表明，沿元数等式迁移公式不会改变其码。codeShift 把这条等式排成从迁移后公式的码指回原公式之码的方向，以便解码论证随后调整元数。

  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift e ψ = sym (constSubstCommSlice
    Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)

现在可以证明码集桥接中较直接的一向。对任意无参 k 元公式 χ，先把它嵌入 ⟪ ∅ ⟫ 上，所得公式的键由 key∈AllCodes 属于 AllCodes ∅ʟ。这个键由数码 # k 与「经空字母表读入所得的嵌入公式之码」组成。等式 sameCode' 把该公式等同于 χ 直接嵌入宇宙所得的公式，而后者的码正是 fst (limitCode χ)。沿这条等式迁移隶属证明，便得到 freeCode-in：码集包含每条无参公式的「元数与码」之键。

freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))

反向则设 pr (# k) c 属于 AllCodes ∅ʟ。消去定理 AllCodes-out 只在命题截断下解码一个成员，而且它接收的是 S 的元素，也就是一个集合连同其可构造性证明。所需输入的底层集合已经是 pr (# k) c，还须补上它的可构造性证明。完成这一步以后，PT.map read 会把命题截断中的每一份可能解码载荷变成所需的 k 元无参载荷，始终不消去命题截断。

freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩
             → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁
freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩

这张缺少的证书来自可构造性的传递性。AllCodes ∅ʟ .snd 说明码集可构造，h则说明该键属于码集，故 isL-trans h (AllCodes ∅ʟ .snd) 证明键本身可构造。把这张证书与 pr (# k) c 配对，就得到 AllCodes-out 所要求的 S 元素；此处没有额外的解码，也没有发生选择。

  cL = isL-trans h (AllCodes ∅ʟ .snd)

在命题截断内部，AllCodes-out 给出一个元数 n、一条公式 ψ : Fo∅ n，以及一条说明「给定的键就是 ψ 的键」的等式。局部函数 read 把每份这样的载荷变成所需元数 k 处的一条无参公式，并附上 c 等于其码的证明。它先把 ψ 迁移为 ψ' : Fo∅ k，再沿 ε 改名其不可能出现的常元。因此，所构造的见证是 mapFo ε ψ'。有序对的等式同时给出迁移所需的元数等式，以及返回依值对时所需的码等式。

  read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ))
       → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ))
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k

键等式的两个分量完成这一构造。第一分量的类型是 # k ≡ # n；数码的单射性再配合对称性，给出 e : n ≡ k，公式 ψ 沿它迁移为 ψ'。第二分量说明 c等于从原公式 ψ 得到的宇宙公式码。由 codeShift，该码等于迁移后 ψ' 的码；再由 sameCode，后者等于 embed (mapFo ε ψ') 的码。复合这些等式，恰好得到与见证配对的证明。由于 read 只通过 PT.map 使用，freeCode-out 的结论只是在命题截断下存在这样一条无参公式，并未从码集中选择出一条公式。

    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')

无参性，说成一个原子

码集把一条公式存放在由其元数与骨架组成的键之下。为了用一个隶属原子表达此事，FreeAt 先绑定元数位置之取值的后继，再绑定这个后继与骨架组成的对，最后询问该对是否属于码集位置。因此，用元语言记号看，它具有 ∃[ z ] ∃[ y ] 的形状：z 是后继元数，y 是键。各次移位只记录穿过一层或两层绑定之后仍要读取哪个原位置。此时公式本身只描述对 C₀ 所给集合的隶属；待该位置被认作空字母表的码集后，它才得到无参性的含义。

FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )

第一对读式在任意环境 γ 上成立。外部等式 qa 把元数位置的取值认作数码 # k；它是语义读式的假设，并不是 FreeAt 内部的另一个子句。骨架位置与码集位置仍可任意取值，所以这些引理先单独说明两层绑定的逻辑内容，尚不指定所用的码集。

module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) where

正向构造从预期的键 pr (# (suc k)) (fst (lookup s γ)) 已属于 C₀ 位置上的集合这一假设出发。这个键恰好给出 FreeAt 所需的两个存在见证：先取数码 # (suc k)，再取它与骨架组成的对。余下工作只是核实这两个见证分别满足后继描述与配对描述；最末的原子正是起初假设的隶属。

  FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
    where
    numAt : S

内部语言的存在见证是 S 的元素，因此其底层集合必须连同一份可构造性证明给出。第一个见证 numAt 的证明来自每个数码都属于 L。对于第二个见证 keyAt，隶属假设把该键放进 C₀ 位置所持有的可构造集中，再由 L 的传递性得到键本身可构造。这两份证明只是使数码与键能够充当绑定取值，并未给 FreeAt 增添新的数学条件。

    numAt = # (suc k) , numL (suc k)
    keyAt : S
    keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd)
    hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
    hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))

两条辅助公式的充分性等式现在完成所需核实。对于 hsuc，等式 qa 把元数位置的取值换成 # k，而这个数码的后继就是 # (suc k)。对于 hpr，prAtL 的充分性把对该公式的满足化为「该取值等于两个分量位置所指定的有序对」；keyAt 的定义恰是这个对。因此，这两条语义事实把所选见证接到了最后那条隶属原子上。

      (cong sucV (sym qa))
    hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
    hpr = subst ⟨_⟩
      (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl

反向读式从对 FreeAt 的满足关系中恢复隶属。存在公式的满足关系只在命题截断内给出见证，所以证明把外层截断消去到目标隶属命题中。外层存在量词的一个代表包含后继见证，以及对内层存在公式的满足关系；后者仍有自己的一层命题截断，随后还要再消去一次。

  FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
  FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                            ∈ fst (lookup C₀ γ))) atNum
    where

两次截断消去具有同一个余域，所以证明把它命名为 Target：预期的键属于 C₀ 位置上的集合。该类型是命题，因为集合的隶属关系取命题值。正是这一事实允许两次使用截断消去；证明并没有从存在见证中选出一个特定代表。

    Target : Type (ℓ-suc ℓ)
    Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩

分支 atKey 处理内层存在量词的一个代表。它取得外层见证 z 以及「z 是元数取值之后继」的等式，还取得内层见证 y 和两条事实：y 满足配对公式，且其底层集合属于 C₀ 位置上的集合。内层存在量词原本带有命题截断，但在这个消去分支内部，可以使用其代表来证明命题 Target。

    atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ))
          → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                       × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ )
          → Target
    atKey z qz (y , (hp , hy)) =

prAtL 的充分性把 y 的底层集合认作一个对，其第一分量是 z 的底层集合，第二分量是骨架。先用关于 z 的等式，再接上 qa，便把第一分量认作 # (suc k)。因此，y 正是预期的键。沿此等式迁移已知的 y 的隶属，就得到 pr (# (suc k)) (fst (lookup s γ)) 的隶属，也就是 Target。

      subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
         ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy

外层消去分支 atNum 取得一个代表 z 和两份证据。第一份说 z 满足后继公式；第二份 hk 是仍带命题截断的内层存在公式之满足关系。因此，atNum 已能确定键的预期第一分量，同时把内层见证留到消去进 Target 时再使用。

    atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                       × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                       ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
          → Target
    atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))

sucAtL 的充分性把第一份证据解码成 atKey 所需的等式：z 是元数位置之取值的后继。随后，证明把 hk 消去到命题 Target，并对每个代表应用 atKey。连同 FreeAt-out 外层已有的消去，这恰好处理了两层存在量词，同时守住命题截断的边界。

                                         ∈ fst (lookup C₀ γ)))
      (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk

接下来的读式把此前任意的两个位置具体化。等式 q₀ 把 C₀ 位置上的集合认作 AllCodes ∅ʟ，其元素是空字母表上诸公式的键；qa 则再次把元数取值认作 # k。在这两项假设下，FreeAt-in 与 FreeAt-out 所刻画的隶属便能转换为关于元数为 suc k 的无参公式的实际陈述。

module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ))
         (qa : fst (lookup a γ) ≡ # k) where

从对 FreeAt 的满足关系出发，FreeAt-out 得到该键属于 C₀ 位置当前所持有的集合。沿 q₀ 迁移后，这条隶属落入 AllCodes ∅ʟ。先前的解码引理 freeCode-out 随即在命题截断内给出一条元数为 suc k 的无参公式 χ，其极限层码正是骨架位置的取值。这就是那个隶属原子的向外语义读式。

  codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
               → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                     (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁
  codeFree-out h = freeCode-out (suc k) (fst (lookup s γ))
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀

这里的元数是 suc k，因为定义子集所用的名字公式除了 k 个参数位置之外，还要留一个变元位置给候选元素。codeFree-out 中的公式见证仍处于命题截断内。FreeAt-out 可以把自己的绑定见证局部消去到隶属命题中，但最后的解码步骤 freeCode-out 又给出一个带命题截断的公式见证。因此，结论只断言这样的公式存在，并不从中选出一条公式。

      (FreeAt-out C₀ s a γ k qa h))

反过来，codeFree-in 从一条给定的元数为 suc k 的无参公式 χ 出发，并假设它的极限层码与骨架位置的取值相等。引理 freeCode-in 先把相应的键放入 AllCodes ∅ʟ；再沿码等式以及 q₀ 的反向迁移，便把这条隶属移到实际的骨架位置与码集位置。最后，FreeAt-in 用两个存在见证包装所得隶属。这个方向无须产生带命题截断的公式见证，因为 χ 本来就是输入数据。

  codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
              → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  codeFree-in χ q = FreeAt-in C₀ s a γ k qa
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀)
      (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)

一旦元数位置与空字母表码集位置得到确定，codeFree-out 与 codeFree-in 便共同给出 FreeAt 所承诺的读法。向外方向在命题截断内断言：骨架是一条具有 suc k 个变元的无参公式之码。向内方向从一条给定公式出发，因而不需要这样的截断。名字公式的识别至此完成；下一个问题是，它的有穷参数环境怎样记录数 k。

        (freeCode-in (suc k) χ)))

一个序列有多长

先刻画集合编码图中的任意隶属。若 g 以 Fin k 为索引，并且pr x y 属于 env g，那么仅仅存在一个索引 i，使x ≡ # (toℕ i) 且 y ≡ g i。结果仍处于命题截断内，因为层级集合中的隶属只记录某个生成条目的仅仅存在。因此，memberOf 揭示所有可能的索引，却不从中选择一个。

private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = PT.map
    (λ { (li , e) → lower li

隶属见证携带一条等式，把图中存放的条目与所查询的有序对联系起来。有序对构造子的单射性把这一条等式拆成两个分量各自的等式。见证中的等式先写存入的条目，故两个分量的路径都要反向，才能得到 memberOf 所需的方向：从 x、y 分别指向数码键与 g 给出的取值。

       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })

反过来，每个给定索引都产生一个条目。对 i : Fin k，有序对pr (# (toℕ i)) (g i) 属于 env g；提升后的索引就是隶属见证，而条目等式由自反性给出。因此，memberOf 与 entryOf 提供识别这个有穷图之横坐标所需的两个方向。

  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁

定义域的正向包含从如下仅仅存在出发：存在一个模型元素 y，使pr x (fst y) 位于图中。目标是隶属命题 x ∈ # k，所以外层命题截断可以消去到这个目标中。固定其中一个代表 y 后，只须从图的隶属中恢复一个索引，并证明该索引的数码属于 # k。

  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))

对一个明确的索引 i，定义域只用到第一分量的等式。由于toℕ i < k，数码引理 #mono 给出 # (toℕ i) 属于 # k；再沿x ≡ # (toℕ i) 迁移，便得到 x 属于 # k。第二分量的等式识别图中的取值，却与这一包含无关。辅助函数 atEntry 先固定取值 y，然后才消去余下的截断索引信息。

            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))

对图的隶属应用 memberOf，恰好得到所需的索引信息，但它仍在命题截断内。由于 x ∈ # k 是命题，PT.rec 可以把每个代表交给 atIndex。正向包含由此完成，整个过程没有把某个索引提取成普通数据。

      (memberOf k g x (fst y) p)

反向包含设 x ∈ # k。冯·诺伊曼数码的消去表明，在命题截断内，存在一个自然数 m < k，使 x ≡ # m。这样的 m 决定 Fin k 中的一个索引。结论本身也是「图中有取值」的命题截断存在，所以 PT.map 可以逐一变换数码见证，而无须选择其中一个。假设 cg 随后提供把该取值呈现为模型元素所需的可构造性证明。

  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩
  dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))

对一个代表 m < k，令 i 为相应的有穷索引。存在量词的见证是模型元素(g i , cg i)，即该索引处的取值及其可构造性证明。图中的事实来自entryOf：以标准第一分量 # (toℕ i) 为键的有序对是一个条目。把这个第一分量迁移为 x，便得到所需的 pr x (g i) 属于图。

              → Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k

转换 fromℕ' k m p 把界限证明 p : m < k 化为索引 i。其往返律toFromId' 证明 toℕ i ≡ m。把 x ≡ # m 与这条往返等式之反向在数码下的像复合起来，便得到 qi : x ≡ # (toℕ i)；这正是把标准条目搬到所查询第一分量所需的路径。定义域的反向包含至此完成。

      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))

现在可以把这两个集合层面的包含与对象语言的定义域公式对应起来。固定环境γ、族 g : Fin k → V ℓ，以及等式 qe；后者把 e 位置的底集认作env g，而 d 位置仍是候选定义域。每个 cg i 都证明 g i 是可构造模型的元素，这正是反向包含构造存在见证时所需的条件。在这个语境中，接下来的两个引理分别读出与填充 domAt e d。

module _ {n : ℕ} (e d : Fin n) (γ : S ^ n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : fst (lookup e γ) ≡ env g) where

设 γ 满足 domAt e d。为了证明 d 位置的底集就是 # k，domAt-numeral 对模型元素 lookup d γ 与 (# k , numL k) 应用 L 内部的外延性，再把所得等式投影到底集。因此，只须对每个可构造的测试元素 x 证明：属于候选定义域与属于该数码是同一个命题。正向蕴含先用 domAt-in 读取定义域隶属。

  domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k
  domAt-numeral h = cong fst (extensionalL {a = lookup d γ} {b = # k , numL k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ fst x ∈ # k ⟩
    fwd x hx = dom-into k g (fst x)

在正向蕴含中，domAt-in 把 d 位置中的隶属化为如下仅仅存在：某个取值与x 配成的对位于 e 位置的集合中。沿 qe 迁移后，该条目落入 env g，dom-into 随即给出 x ∈ # k。反过来，dom-from 把 x ∈ # k 化为env g 中某个条目的仅仅存在。由于属于候选定义域是命题，可以消去这一截断；局部函数 put 处理每个呈现出来的条目。

      (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe
        (domAt-in e d γ h x hx))
    bwd : (x : S) → ⟨ fst x ∈ # k ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup d γ))) put (dom-from k g cg (fst x) hx)
      where

对一个呈现出来的条目，put 先沿 qe 的反向把其隶属搬回 e 位置所存的图，再由 domAt-out 得到它的第一分量属于 d 位置。于是，两条蕴含经⇔toPath 在每个 x 处形成两条隶属命题之间的路径；外延性把这些逐点路径组装成候选定义域与 # k 的相等。截断的图见证只用于证明隶属，并未从中选择任何取值。

      put : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ env g ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
      put (y , p) = domAt-out e d γ h x y
        (subst (λ u → ⟨ pr (fst x) (fst y) ∈ u ⟩) (sym qe) p)
    pt : (x : S) → (fst x ∈ fst (lookup d γ)) ≡ (fst x ∈ # k)
    pt x = ⇔toPath (fwd x) (bwd x)

反向从一条等式开始，它断言 d 位置的集合确实是 # k。为了证明domAt e d，domAt-intro 要求对每个元素给出定义域的两条蕴含：图中仅仅存在一个取值蕴含该元素属于 d，而属于 d 又蕴含图中仅仅存在一个取值。等式 qe 与 qd 分别把这两项化为 dom-into 与 dom-from。因此，填充公式使用的仍是读出公式时那两个集合层面的包含，只是方向相反。

  domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩
  domAt-fill qd = domAt-intro e d γ step
    where
    step : (x : S)
         → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩

为了填充定义域公式，只须证明逐点的两个蕴含。先设某个取值与 fst x 配成的对属于位置 e 所存的图。沿 qe 搬运后，这个条目属于 env g，于是 dom-into 证明 fst x 属于数码 # k。再沿 qd 的反向搬运，便得到它属于位置 d 所存的候选定义域。

            → ⟨ fst x ∈ fst (lookup d γ) ⟩)
         × (⟨ fst x ∈ fst (lookup d γ) ⟩
            → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩)
    step x =
        (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)

反向蕴含沿同一路径倒行。先用 qd 把位置 d 中的隶属搬到 # k 中；dom-from 随后在命题截断内给出一个取值，使它与 fst x 配成的对属于 env g；最后沿 qe 的反向把该条目送回位置 e。两个方向由此完成 domAt-fill，过程中没有从有穷图中选出一个取值。

          (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe hy)))
      , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) (sym qe)
          (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))

满足关系的图所指派的取值

现在考察满足关系图在真实公式键处指派什么。固定周围环境 γ：位置 B 给出载体，x 与 y 则给出候选键和候选取值。缩写 Bs = lookup B γ 使随后证明对这三个位置保持统一。因此，以下公式的常元由底集 fst Bs 的成员索引。

module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where
  private
    Bs : S
    Bs = lookup B γ

图公式通过十四个受界位置封装满足关系递归。对模型语言公式 φ，fr φ 在这些位置依次放入载体 Bs、它的典范满足关系表、由子公式键组成的槽、环境塔以及十个构造子标签的数码，随后接上周围环境 γ。每个分量都是此前已经为该载体与公式构造好的典范对象。

    fr : ∀ {m} (φ : Formula S m) → S ^ ( + n)
    fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ

这十个数码并不为码域编制索引，而是标记表规格中从零到九的十条构造子子句。tgs φ 记录 fr φ 中每个指定的标签位置都含有与其构造子相应的数码。凭借这份对齐，打包后的表公式才能为每种语法形状选中正确子句。

    tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN
    tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ

满足关系表还需要为每个元数配备正确的环境族。htow φ 把既有的塔定理应用于 fr φ 的各分量：塔位置的取值是 Tower.tower Bs，载体位置是 Bs，零号标签位置则含有所需数码。因此，towerAt 在扩展环境中成立，此处无须重新证明关于塔的论证。

    htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩
    htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl

典范表的定义域恰是公式键所成的槽。一个方向从表条目出发，用 inSlot 证明其键属于 slot Bs φ；由于条目是在命题截断下取得的，这次消去落入隶属命题。另一个方向用 total 证明槽中的每个键都仅仅存在一个表取值。domAt-intro 把这两个蕴含组合成 hdom φ。

    hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩
    hdom φ = domAt-intro Ti Ci (fr φ)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ)))
                 (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h)
           , (λ h → total Bs φ (fst z) h))

现在可以准确陈述正向读式。设 ψ 的常元取自 fst Bs 的成员。若位置 x 含有它的真实键 keyS Bs ψ，位置 y 含有翻译后的模型语言公式 mapFo (asConst Bs) ψ 的满足集合，那么 satGraphAt B x y 成立。这里的取值是满足该公式的环境所成的集合，并非单个真值。graphAt-value 向 graphAt-in 提供典范递归见证，从而证明这一结论。

  graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
                → fst (lookup x γ) ≡ fst (keyS Bs ψ)
                → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
                → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-value {m} ψ qx qy = graphAt-in B x y γ

存在见证按 GraphWitAt 所需的次序由五个典范分量装配：数码指派 numν、塔、槽、满足关系表与载体。随后把整份见证包入命题截断，以配合图公式中存在量词的语义。余下任务是证明这些选定分量满足载体、标签、塔、闭包、定义域、条目与表规格的要求。

    ∣ numν
    , (Tower.tower Bs
    , (slot Bs φ
    , (satTable Bs φ
    , (Bs

载体等式由自反性给出。接下来的三份证明分别断言：十个标签位置含有预定数码，环境位置确实是 Bs 上的塔，并且 slot Bs φ 对带有直接子公式的构造子闭合。最后一项保证递归表在复合公式键处施用子句时，能够查阅直接子公式键处的表条目。

    , (refl
    , (tgs φ
    , (htow φ
    , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)

最后三项要求分别确定表的定义域、选定条目与子句规格。先前证明的 hdom φ 给出定义域公式。对表条目，keyBridge Bs ψ 关联载体语言公式与 φ 的键，而 qx、qy 把典范条目搬到位置 x、y 所存的键和值上。最后，SlotHolds.holds 从同一载体、标签、塔、槽与表证明该典范表满足 tableAt。装配好的见证因而证明图公式成立。

    , (hdom φ
    , (subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩)
         (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
    , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁
    where

这里的 φ 是 ψ 在模型语言中的版本。ψ 的一个常元是底层载体的成员；asConst Bs 为它配上作为 S 中元素所需的可构造性证明，mapFo 再把这个常元映射施于整条公式。上文另行使用的 keyBridge 保证：翻译前直接编码与翻译后在模型内部编码所得的底层键相同。

    φ : Formula S m
    φ = mapFo (asConst Bs) ψ

反向读式设 satGraphAt B x y 成立，且位置 x 是 ψ 的真实键。graphAt-out 只能在命题截断内给出十四个存在分量。所求结论是累积层级 V 中的一条相等，而 setIsSet 说明这种相等所成的类型是命题。因此，PT.rec 可以在局部逐一考察呈现出的图见证，而不从中作全局选择。

  graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
               → fst (lookup x γ) ≡ fst (keyS Bs ψ)
               → ⟨ γ ⊨ satGraphAt B x y ⟩
               → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
  graphAt-only {m} ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)

拆开一个图见证，可得候选表 T、码域 C、环境塔 E、载体 b 及其全部证明。这里的 C 不必是典范槽；关键在于它对子码闭合，T 满足打包后的表子句，而且真实键属于 C。最后一项由表条目 ha 经 domAt-out 得到。把这份键隶属与同一个表条目交给 SatSoundC.pinned，便可将 ψ 在表中记录的取值确定为典范满足集合。

    where
    read : GraphWitAt B x y γ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
    read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) =
      SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12
        ψ (subst (λ u → ⟨ u ∈ fst C ⟩) qx

钉定定理所需的两个前提起初都在周围环境的位置 x 处读取。沿 qx 搬运，一方面把由 hd 与 ha 得到的定义域隶属化为 keyS Bs ψ 属于 C，另一方面把 ha 本身化为 T 在该键与位置 y 所存取值处的条目。钉定定理随即交回所需相等：在真实公式键处，图所容许的任何取值都等于翻译后公式的满足集合。

             (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha))
        (lookup y γ)
        (subst (λ u → ⟨ pr u (fst (lookup y γ)) ∈ fst T ⟩) qx ha)

名字，描述在诸位上

指称公式体一次检验一个候选元素 z。首个合取项 z ∈ B 把所描述的集合限制在载体之内。随后公式体绑定环境 c，并要求 c 是把 z 添到参数环境 e 前端所得的编码环境。此时 c 与 z 都位于周遭赋值之前，故对 e 的引用须穿过两层绑定。

DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero

其余三个见证决定如何解释骨架。首先要求 k 是扩展环境 c 的定义域；接着要求 key 属于位置 C 中的码集，并等于 k 与骨架码 s 组成的对；最后，v 是满足关系图在载体 B 与该键处容许的取值，末尾的隶属断言则是 c ∈ v。当 C 填入载体的真实码集时，这些条件表达的是扩展环境满足骨架，而非仅在任意键处查询图。

            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )

元语言名字由元数、无参公式与参数向量组成。NameAt 分别以元数位置 a、骨架码位置 s 与环境位置 e 表示这三项，并以指称位置 d 记录由它们导出的集合。第一个合取项检查由 a 的后继与 s 组成的对是否属于空字母表码集。这里的后继不可省略：具有 a 个参数的名字还需要一个变元来放置候选成员。下一个合取项要求 a 属于模型的自然数之集。

NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  FreeAt C₀ s a
  ∧̇ ( (var a ∈̇ con ωʟ)

第三个合取项要求 e 是定义域恰为 a、取值落在 B 中的环境，从而把参数向量与前一位置记录的元数联系起来。最后一个合取项以外延方式刻画 d：对每个候选元素，属于 d 当且仅当它满足 DenoteBody，而该公式体的首项已经把候选元素限制在 B 中。因此，d 是由名字的三项数据导出的，并非元语言名字额外存储的分量。

    ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )

DenoteOf z 是与 DenoteBody 四层存在量词相应的元语言载荷。它记录扩展环境 c、其候选定义域 k、一个公式键和图取值 v，并带上联系这些对象的全部条件。把这些数据放进一个依值元组，既显露出装配对象语言公式所需的见证，也保留了后续条件对先前选择的依赖。

module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where
  DenoteOf : (z : S) → Type (ℓ-suc ℓ)
  DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩

这份载荷严格沿着语义链展开。前两份满足证明分别断言 c 扩展旧环境，以及 k 是它的定义域。当 C 实例化为 AllCodes B 时，key 对 C 的隶属保证随后是在真实公式码处查询图。接着的显式等式把该键确定为 k 与 s 组成的对。末两份证明则断言 v 是图在该键处的取值，并且 c 属于 v。这里的 v 是满足该公式的环境之集，并非布尔真值。

      × ( ⟨ fst key ∈ fst (lookup C γ) ⟩
        × ( (fst key ≡ pr (fst k) (fst (lookup s γ)))
          × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
            × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )

DenoteBody-in 把这份显式载荷变成对公式体的满足。载体隶属保留为最外层合取项，而见证 c、k、key 与 v 按四层存在绑定的同一次序引入。多数条件本来就以满足证明陈述。例外是定义 key 的等式：配对公式的充分性路径把这条集合论等式转换为对 prAtL 的满足。

  DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z
                → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
  DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp

对象语言的每个存在量词都以命题截断解释，因此构造在结束证明前把四个见证逐层包入截断。最后一行从图取值向外直至扩展环境，依次闭合这四层。所得满足因而只记录适当数据存在；未截断的见证只保留在用来构造它的输入 DenoteOf z 中。

      , ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁

DenoteBody-out 在反向读取时保留同一边界。载体隶属位于所有存在量词之外，因此可以直接取得；四个见证则只能在嵌套的命题截断中显露。每次截断消去的目标都是 ∥ DenoteOf z ∥₁，仍为一个命题，故证明可以变换每一份局部见证，却不会从中全局选出一个元组。

  DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
                 → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁
  DenoteBody-out z (hz , hc) = hz , PT.rec squash₁
    (λ { (c , (hc , hk)) → PT.rec squash₁
      (λ { (k , (hk , hkey)) → PT.rec squash₁

在键这一层，公式体给出对配对公式的满足，而 DenoteOf 要求解码后的等式 fst key ≡ pr (fst k) (fst (lookup s γ))。沿配对公式的充分性路径正向读取，恰好得到这条等式。最内层的映射随后把图证明与隶属证明连同见证 v 一并保留，外围的消去再于一层命题截断之下重建整份载荷。

        (λ { (key , (hi , (hp , hv))) → PT.map
          (λ { (v , (hg , hm)) → c , (k , (key , (v , (hc , (hk , (hi
            , ( subst ⟨_⟩
                  (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp
              , (hg , hm) ))))))) }) hv }) hkey }) hk }) hc

NameAt-in 接受五份输入。前三份建立固定的合取项：骨架在给定元数处为无参公式，元数属于模型的自然数之集，参数图是载体上的环境。余下两份输入给出刻画指称所需的逐点双向蕴含。第一向从 z ∈ d 得到 z ∈ B 与一份显式的 DenoteOf z；反向则把 z ∈ B 和一份显式的 DenoteOf z 变成 z ∈ d。

module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where
  NameAt-in : ⟨ γ ⊨ FreeAt C₀ s a ⟩
            → ⟨ fst (lookup a γ) ∈ ω ⟩
            → ⟨ γ ⊨ envOverAt e a B ⟩
            → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩

两个方向都对每个候选元素分别陈述，因为 extAt 通过逐点隶属表达集合相等。它们有意使用未截断的 DenoteOf z：本引理是一条引入规则，调用方要提供可用来构造公式体满足的具体数据。从 NameAt 的任意满足中恢复这些数据属于另一项充分性论证；下一章给出的恢复结果仍保留在命题截断之下。

               → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z)
            → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
               → ⟨ fst z ∈ fst (lookup d γ) ⟩)
            → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
  NameAt-in hf ha he into back =

证明把这两个方向交给 extAt 的引入规则。由 z ∈ d，第一向给出载体隶属与载荷，DenoteBody-in 再把它们转换为对公式体的满足。反过来，DenoteBody-out 把公式体的满足读成载体隶属与经过命题截断的载荷。由于目标 z ∈ d 是命题，可以消去该截断并应用第二份输入。把所得外延刻画与前三份输入组合起来，便得到整条名字公式的满足。

    hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ
      (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd))
      (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ)))
                 (back z (DenoteBody-out B C s e γ z h .fst))
                 (DenoteBody-out B C s e γ z h .snd))))

那个序，不跑自己的递归

随后的比较公式成组绑定数据，因此对周遭赋值的引用须作统一移位。sh3 把一个周遭位置移过三层新绑定。在 LexAt 中，这三层分别存放序号 i 以及两个参数环境在 i 处的取值，使原有的两个环境位置与参数序位置仍可引用。稍后的 LeastNameAt 也使用同一移位，把周遭位置移过一个竞争名字的骨架、元数与环境。

private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))

sh6 相应地把引用移过六层绑定。StepBody 绑定两个名字时会使用它，每个名字都由骨架、元数与参数环境表示。完全扩展后的赋值因而把六个新取值置于原赋值之前，而载体、两个序关系、两个码集以及待比较的两个指称仍保留为周遭位置。这些移位只保持引用所指，不增添任何序假设，也不亲自执行比较。

  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = suc (suc (suc (suc (suc (suc i)))))

参数键要找两个参数环境首次相异的位置。LexAt 先绑定元数位置所持集合的一个成员 i。当该位置存放一个元数的数码时，它的成员恰是各个更小位置的数码；因此，这个有界存在量词已经遍历全部可能的序号，无须另行引入序号之序。

LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
LexAt P a e₁ e₂ =
  ∃̇∈ (var a) (
    ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero)
           ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero

选定 i 后，两层存在量词给出取值 u 与 v，使 e₁(i)=u、e₂(i)=v；第三次应用则断言 u 与 v 组成的有序对属于参数关系 P。随后的有界全称量词考察每个 j ∈ i，并对每个这样的 j 要求仅仅存在一个取值 x，使两张环境图在 j 处都取到 x。所以整条公式说的是「此处严格有序，而每个更早位置都有共同取值」。只有把两个环境认作单值图之后，共同取值才蕴涵相应参数相等；后面的充分性论证正是用图的查表性质与载体嵌入的单射性得到这一步。公式本身不执行递归。

             ∧̇ ( appAt (sh3 P) (suc zero) zero
               ∧̇ ∀̇∈ (var (suc (suc zero))) (
                    ∃̇ ( appAt (sh5 e₁) (suc zero) zero
                      ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )

完整的名字比较现在按字典序的优先次序组合三个键：骨架码、元数与参数环境。第一个析取支把关系位置 R 应用于 s₁ 与 s₂。由取值公式的充分性，这表示两个骨架码组成的有序对属于 R。把 R 保留为一个位置，使同一条公式可以通用于不同赋值；后面的充分性定理会在这里填入表示极限层码序的关系。

≺At : ∀ {n} → Fin n → Fin n
    → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n
≺At R P s₁ a₁ e₁ s₂ a₂ e₂ =
      appAt R s₁ s₂
  ∨̇ ( (var s₂ ≐ var s₁)

第二个析取支处理骨架码相等的情形。它先按 s₂ = s₁ 的方向记录等式，再给出余下两个字典序分支：若两个元数位置都存放数码，则 a₁ ∈ a₂ 表示第一元数更小；另一分支要求 a₂ = a₁，再由 LexAt P a₁ e₁ e₂ 在参数首次相异处决定次序。s₂ = s₁ 与 a₂ = a₁ 的方向正好配合后面的迁移，把第二个名字的码与参数向量移到第一个名字的数据上。

    ∧̇ ( (var a₁ ∈̇ var a₂)
      ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )

为了给 LexAt 证明一条可复用的读式，先单独命名相符存在量词之下的公式体。在先前位置 j 处，Body 要求同一个取值 x 满足两次应用，也就是让两张环境图在 j 处都含有取值 x。扩张赋值中新添的五项依次是 x、j、v、u、i，所以对周遭环境位置的引用都须穿过五层绑定。

module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where
  private
    Body : Formula S (suc (suc (suc (suc (suc n)))))
    Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero

固定 i、u、v 后，Inner i u v 记录前三层存在绑定之后剩下的公式体。前两个分量说图 e₁ 与 e₂ 分别含有对 (i,u) 与 (i,v)；第三个分量说对 (u,v) 属于关系 P。这些分量仍是关于 appAt 的满足关系陈述；稍后另行记录它们解码后的隶属形态，便可显式联系这两种呈现。

    Inner : (i u v : S) → Type (ℓ-suc ℓ)
    Inner i u v =
      ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩
      × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩
        × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩

Inner 的第四个分量是在 i 之下相符。对每个属于 i 的模型元素 j，它给出语义存在式 ∃[ x ∶ S ]，断言某个 x 满足 Body。这个存在式是命题截断：它保留「在 j 处有共同取值」这一事实，却不把选定的取值作为数据暴露出来。因此，有界全称量词被读成一个函数，为每个 j ∈ i 给出这样一份经过命题截断的存在。

          × ((j : S) → ⟨ fst j ∈ fst i ⟩
             → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩) ) )

Agrees i 以两次应用解码后的形态陈述同一项相符：对每个 j ∈ i，仅仅存在一个元素 x : S，使 j 与 x 的底集组成的对同时属于图 e₁ 与 e₂。当 i 是元数的数码时，它的成员恰好表示所有更早位置。这个定义只记录共同的图取值；相应元层参数的相等要到后面才从已知的环境图与载体嵌入的单射性导出。

  Agrees : (i : S) → Type (ℓ-suc ℓ)
  Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩
           → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                          × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁

Differs 汇集首次相异见证的完整解码形态。它包含序号 i、取值 u 与 v、i 对元数位置所持集合的隶属、对 (i,u) 与 (i,v) 的两份图隶属、该位置上的严格参数比较，以及 Agrees i。当元数位置存放数码，且两个图位置存放该元数的参数环境时，这些字段恰好组成字典序首次相异所需的数据。

  Differs : Type (ℓ-suc ℓ)
  Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ]
    ( ⟨ fst i ∈ fst (lookup a γ) ⟩
    × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩
      × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩

严格比较字段与 ≺At 的码分支采用相同的关系形态：u 与 v 的底层值组成的有序对属于位置 P 所持的集合。末尾的 Agrees i 记录每个更早位置上的共同取值；对预期的单值环境图而言，这便保证更早参数没有相异。因此，Differs 把首次相异见证的数学内容与表达它的对象语言绑定结构分开记录。

        × ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )

映射 pack 只把 Inner 的相符分量转换为 Agrees，前三个分量与这次局部转换无关。固定 j ∈ i 后，语义存在式的一个见证 x 带有两份对 appAt 的满足证明。分别应用 appAt-adequate，即可把它们变成 Agrees 所需的两份图隶属，同时保持同一个见证 x。

  private
    pack : (i u v : S) → Inner i u v → Agrees i
    pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩

这次转换在已有的命题截断之内完成。PT.map 把每个可能的见证及其两份应用证明，映成同一个见证及其两份隶属证明。由于目标仍是经过命题截断的存在，过程中既不取出任何代表，也不使用选择原理。逐点映射便足以对每个更早位置得到 Agrees i 所需的结论。

               (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁
           , subst ⟨_⟩
               (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) })
      (hj j hj')

unpack 给出满足原公式所需的反向转换。由 Agrees i 与一个位置 j ∈ i，它取得一份经过命题截断的共同取值见证。对其中每个可能的代表 x，它保留该见证，并把两份图隶属转换回 Body 中两次应用的满足证明。

    unpack : (i u v : S) → Agrees i
           → (j : S) → ⟨ fst j ∈ fst i ⟩
           → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩
    unpack i u v hj j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x

这里沿反方向使用同一些充分性路径。每份隶属证明都沿 appAt-adequate 的对称路径迁移，从而得到 Body 中相应的合取项。PT.map 再次使整个构造留在经过命题截断的存在之内，所以 unpack 无须在全局选定共同取值，便能证明所需的语义存在。

         , ( subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁
           , subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) })
      (hj j hj')

LexAt-in 从 Differs 中的明确数据出发。序号 i 与取值 u、v 分别成为有界存在量词及随后两层存在量词的见证，hi 则证明 i 确实落在界内。在扩张赋值 γ₃ = v ∷ u ∷ i ∷ γ 中，前两份图隶属沿 appAt-adequate 反向迁移，得到对 e₁(i)=u 与 e₂(i)=v 两次应用的满足证明。关系字段与相符字段随后进入同一个合取结构，其中有界全称分量由 unpack 给出。

  LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩
  LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj)))))))
    = ∣ i , (hi , ∣ u , ∣ v
    , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁
      , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂

Differs 的最后两个字段完成引入证明。对 (u,v) 属于 P 的证明沿appAt-adequate 反向迁移，成为对第三次应用的满足关系证明；unpack 则把i 以下的相符变成有界全称量词所需的语义形态。赋值γ₃ = v ∷ u ∷ i ∷ γ 明确记录三层绑定的次序，外围的构造子再由内向外依次闭合 v、u 与 i 的存在量词。

        , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp
          , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁
    where
    γ₃ : S ^ (suc (suc (suc n)))
    γ₃ = v ∷ u ∷ i ∷ γ

从 LexAt 向外读取时，必须保留其存在量词所设下的见证边界。因此，LexAt-out 的目标是命题 ∥ Differs ∥₁，并且只把外层截断消去到这个目标中。局部函数 atValue 承担实际的数学解码：一旦在各次消去的局部范围内取得具体的i、u、v、界限证明和余下的满足关系数据，它便构造一份未截断的Differs 记录。这样的记录不会被选出到这些局部范围之外。

  LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁
  LexAt-out = PT.rec squash₁ atIndex
    where
    atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs
    atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v

atValue 的前半段恢复序号与两次图查取。界限证明 hi 已经具有 Differs要求的形态。正向读取两条充分性路径，便把两次应用的满足关系分别变成(i,u) 对 e₁ 的隶属，以及 (i,v) 对 e₂ 的隶属。因此，两个取值仍与公式找到它们时的同一个序号相联系。

      , ( hi
        , ( subst ⟨_⟩
              (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁
          , ( subst ⟨_⟩
                (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂

第三次应用以同样方式解码，得到 (u,v) 对参数关系 P 的隶属。函数 pack把有界范围内以应用陈述的相符翻译成 Agrees i 所要求的两份图隶属，从而给出最后一个字段。这些数据在 atValue 内组成一份明确的 Differs 记录；外围的各次消去最终只保留它的命题截断。

            , ( subst ⟨_⟩
                  (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp
              , pack i u v h ) ) ) ) ))

最内层存在量词给出第二个取值 v 及 Inner i u v，但二者只在该存在量词的截断内部可用。处理函数 atSecond 对每一份局部可用的 (v,h) 调用 atValue构造 Differs，并立即把结果放入 ∥ Differs ∥₁。这正是命题截断所容许的消去：见证被用于证明一个命题，却不会由结果暴露出来。

    atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
             → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁
    atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁

向外一层，atFirst 取得具体的第一个取值 u，以及第二个取值之存在的截断。它用 atSecond 消去这层内部截断，而 atSecond 的结果仍是∥ Differs ∥₁。所以论证可以从第一个取值走到完整的首次相异记录，而始终无须取得一个全局可用的 v。

    atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
            → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁
    atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h

最后，atIndex 取得序号 i、证明它低于元数的 hi，以及从 u 开始的余项之截断。用 atFirst 消去这份余项，就完成了向外读取。三个处理函数合起来依i、u、v 的次序跟随存在量词的嵌套，而每次消去都有同一个命题目标。因此，LexAt-out 只证明首次相异记录仅仅存在，并未选择其中的序号或取值。

    atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩
                         × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ )
            → ∥ Differs ∥₁
    atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h

读那次比较，以及族的一步

元语言载荷 Below 依照 ≺At 的同一优先次序排列三个比较键。最外层的和类型表示：或者骨架码组成的有序对 (s₁,s₂) 属于位置 R 中的关系，或者两码相等，由后面的键决定。这个和类型的一个元素会明确指出所取分支并携带相应证据；定义本身并未断言对任意位置取值都能判定应取哪一支。这一区别很要紧，因为对象语言析取的语义带有命题截断。

module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where
  Below : Type (ℓ-suc ℓ)
  Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩
        ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩

在骨架码相等的前提下，内层和类型首先给出元数比较 a₁ ∈ a₂。当这两个位置存放元数的数码时，这条隶属表示第一元数较小。若两元数转而相等，则由Differs 给出参数键的首次相异证据。两条等式特意取 s₂ = s₁ 与a₂ = a₁ 的方向，以配合后文把第二个名字的数据迁移到第一个名字的类型中。

            ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
              × Differs P a₁ e₁ e₂ γ ) ) )

≺At-in 把一份明确的 Below 数据翻译成对比较公式的满足关系。在码分支中，关系隶属沿 appAt-adequate 反向迁移，并作为最外层的左析取支引入。在元数分支中，码等式随最外层右析取支进入，而元数隶属进入内层左析取支。这里所做的全是引入：已给出的分支证据被包装进各对象语言析取带命题截断的语义中。

  ≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
  ≺At-in (inl h) =
    ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁
  ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁
  ≺At-in (inr (q , inr (q' , h))) =

参数分支沿两层析取各自的右支进入。它把码等式与元数等式带入相应的右支，再把给定的 Differs 记录交给 LexAt-in。于是，前文已经解码的首次相异数据便成为参数子句的满足关系。这样，Below 的三个情形都能直接引入 ≺At，无需搜索分支，也无需从存在量词中取出见证。

    ∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁

反向读式的目标必然较弱：≺At-out 返回 ∥ Below ∥₁。最外层对象语言析取的满足关系本身带有截断，所以 PT.rec 只能在构造这个命题时局部查看其分支。局部函数 outer 把码分支与码相等分支分开；在后一情形中，它保留等式s₂ = s₁，并把尚未归类的内层析取交给 inner。

  ≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁
  ≺At-out = PT.rec squash₁ outer
    where
    inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩

在给定码等式后，inner 读取余下两个键。若取得元数隶属，便立即得到 Below的中间情形；否则，载荷包含元数等式 a₂ = a₁ 以及对 LexAt 的满足关系，只剩首次相异分量尚待解码。函数签名把这两个选项明确列出，同时固定二者共同使用的码等式。

          ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
            × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ )
          → ∥ Below ∥₁
    inner q (inl h) = ∣ inr (q , inl h) ∣₁
    inner q (inr (q' , h)) =

在参数分支中，LexAt-out 只给出 ∥ Differs ∥₁，恰好保留存在语义所要求的边界。PT.map 把其中每一份局部出现的 Differs 记录映到 Below 的第三种情形，并附上已经取得的码等式与元数等式。结果仍处于一层命题截断之下，因此这次转换只是把存在带到存在，从不要求选定一份首次相异见证。

      PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)

outer 的类型正是第一个比较键处的语义分支。左侧是关系 R 对两个骨架位置之应用的满足关系；右侧则保留等式 s₂ = s₁，并带有余下「元数或参数」析取的满足关系。解码左侧便得到 Below 的码分支，消去内层析取则调用 inner。这两阶段读取与 ≺At 的嵌套结构相互对应，并始终把最终结果留在 ∥ Below ∥₁ 中，不把任何一层析取变成被选定的分支。

    outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩
          ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
            × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂)
                    ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ )
          → ∥ Below ∥₁

最后两个分支完成对比较的向外读取。在码分支中，appAt-adequate 把关系应用的满足关系转换成「两个骨架码组成的有序对属于 R」，从而得到 Below 的第一种情形。在码相等的分支中，内层对象语言析取仍处于命题截断之下，因此只能将它消去到 ∥ Below ∥₁ 中。这样，三个比较键中的任一情形都能被读回，但在截断之外，公式不会显露究竟是哪一个键决定了比较。

    outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁
    outer (inr (q , h)) = PT.rec squash₁ (inner q) h

为了描述两个最小名字之间的比较，步进的公式体需要六个新槽位。这里先固定前三个索引：s6a、a6a 与 e6a 分别指向第一个名字的骨架码、元数数码与参数环境。进入全部六层绑定以后，这三项数据位于 de Bruijn 的第五、第四与第三位。为这些位置命名，使后面的最小性公式和比较公式保持可读，也把绑定位置的计算集中在一处。

private
  s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n))))))
  s6a = suc (suc (suc (suc (suc zero))))
  a6a = suc (suc (suc (suc zero)))
  e6a = suc (suc (suc zero))

余下的索引 s6b、a6b 与 e6b 指向第二、第一与第零位，第二个名字的数据将落在这里。这种反转来自 de Bruijn 表示的通常规律：见证按 s₁,a₁,e₁,s₂,a₂,e₂ 的次序绑定，而每个新见证都添加在环境的最前端。因此，完全扩张后的环境是 e₂ ∷ a₂ ∷ s₂ ∷ e₁ ∷ a₁ ∷ s₁ ∷ γ，六个索引恰好分别选中预定的两个三元组。

  s6b = suc (suc zero)
  a6b = suc zero
  e6b = zero

最小名字被表达为已经占据 s、a 与 e 三个槽位的一组名字数据所具有的性质。第一个合取项要求这组数据满足 NameAt，因而指称 d。第二个合取项全称量化一个竞争者的骨架码、元数数码与参数环境。三层全称量词把该竞争者放在第二、第一与第零位，而 sh3 使载体、两个码集以及指称 d 仍指向原来的槽位。

LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n
            → Fin n → Fin n → Fin n → Fin n → Formula S n
LeastNameAt R P B C C₀ s a e d =
  NameAt B C C₀ s a e d
  ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)

蕴涵的前件把范围限制在同样指称 d 的竞争名字上；指称其他集合的名字与这里的最小性无关。其后件否定 ≺At competitor current，所以 d 的任何竞争名字都不会在三键序中严格先于当前名字。这个公式只陈述最小性，既不搜索名字，也不通过消去命题截断来选出名字。明确的最小名字构造属于元语言中的命名理论，并使用其中的排中律假设。

                      (suc (suc zero)) (suc zero) zero (sh3 d)
             ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                        (sh3 s) (sh3 a) (sh3 e)) )))