---
title: "读取并验证满足关系子句"
module: L.Coding.SatisfactionClauseSemantics
lang: zh
site: "Bedrock"
description: "读取并验证满足关系子句"
stage: "内部编码：表与统一满足关系"
reading_order: 65
canonical: https://bedrock.institute/zh/L.Coding.SatisfactionClauseSemantics.html
html: L.Coding.SatisfactionClauseSemantics.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionClauseSemantics.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Environment, L.Coding.EnvironmentSet, L.Coding.Model, L.Coding.Expressions, L.Axioms.Basic, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.Coding.SatisfactionClauses, FOL.Manipulation.ConstantMapping, L.Coding.Satisfaction, L.Coding.SatisfactionBridge]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SatisfactionClauseSemantics.md, https://bedrock.institute/ja/L.Coding.SatisfactionClauseSemantics.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
规格 `tableAt` 把两个定义域条件 `total`、`onC` 与十条构造子子句合在一起。一条构造子子句如何成为语义递归的一步？本章先把每条子句读成候选值集合的精确外延条件，再证明递归构造的集合 `SatW` 满足同一条件。当外围论证另外给出匹配的码、子值与表条目后，外延性便可把两个值同一视。这些局部桥接本身并不证明整张表单值或唯一确定。

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

论证把层级 `ℓ-suc ℓ` 上的排中律作为显式参数。解码见证的类型经过命题截断后，结论仍只保留其存在性；这个经典假设并不会把见证变成选定的数据。

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

下文所有构造都相对于固定的假设 `lem` 陈述。这样，局部子句读式随后被用于整体可靠性与完备性证明时，其逻辑代价仍然清楚可见。

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

这个证明连接两种语言。内部公式在 `L` 中描述被编码的表，外部公式则在 `W` 所呈现的结构中递归解释。桥接必须逐个保持公式构造子，其中有界量词的界由当前环境中的词项值给出。

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

有限环境在内部由有序对 `(i,v)` 构成的图表示。有序对的单射性可恢复索引及其值，而 `lookup-spec` 说明典范图恰好含有每个宿主层槽位对应的配对。随后，属于 `envSet W n` 只表示某集合是某个长度为 `n`、取值于 `W` 的赋值图。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.Model {ℓ} using ( prAtL; container )
```

内部子句只能借助有界公式检查有序对的分量。`container` 给出一个同时包含两个分量的可构造集合，使配对读式无需无界搜索便能绑定它们。类似地，`consAtL` 读式把 `x ∷ δ` 的图与 `δ` 的图联系起来，这正是处理量词所需的语义步骤。

```agda
open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Coding.Quantification {ℓ} using
```

这里必须区分三种有限索引。自然数 `n` 是公式的元数，`# n` 是码中表示该元数的集合论数码，而 `Fin m` 选择宿主层长度为 `m` 的向量槽位。名称 `i0` 至 `i19` 与移位 `sh` 只管理第三种索引：约束子在向量前端加入一个值时，所有旧槽位都要越过这个新槽位。

```agda
  ( i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh
  ; pr-out; pr-in; down; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in
  ; fillSnd; fillBoth; useSnd; useBoth )
```

共同表框架具有固定的嵌套形状。环境塔条目编码 `(ar,F)`，公式键编码 `(ar,p)`，其载荷又编码 `(tag,r)`，而表条目编码 `(c,yc)`。下文的读式反复拆开这些配对，使构造子关系能够陈述候选值 `yc` 在环境集 `F` 上的外延。

```agda
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.Coding.SatisfactionClauses {ℓ}
  using ( extB; fstAll; subAt; subSucAt; tmIs; module Rel; module Clause )
```

外部环境是有限向量，表中保存的却是集合论的图。因此二者之间的转换同时需要宿主层的有限查找与对象层的配对隶属。积与余积记录公式构造子和词项构造子产生的不同情形，但不会把这些情形与被编码的集合混为一谈。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.Vec using ( _∷_; []; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
```

多数语义比较都是命题之间的路径，由两个方向的蕴涵得到。命题截断同样关键：配对分解与解码环境的见证可以在命题内部使用，但证明不会由此产生对这些见证的全局选择。

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

所有码都生活在累积层级中。因此，有序对码与数码 `# n` 都是真正的集合，而它们的单射性使后文能从码的等式恢复元数、标签与载荷。累积层级的 h-集合结构保证这些恢复出的等式都是命题值。

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

内部赋值取值于可构造载体 `S`，但其中的等式与隶属都是关于 `fst` 投影出的底层集合陈述的。有界绝对性给出内部公式在该载体中的解释。因此，每个读式最终都得到关于投影后集合的具体陈述，可以继续与外部递归比较。

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

## 读取共同框架

中心类型记录关于集合 `y` 的外延事实：`y` 的每个成员都属于 `F` 且满足该性质；反之，`F` 中满足该性质的每个元素都属于 `y`。值集合由这样的事实描述，而非由选定的枚举描述。

```agda
ExtFact : (y F : V ℓ) (P : S → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ)
ExtFact y F P = ((z : S) → ⟨ fst z ∈ y ⟩ → ⟨ fst z ∈ F ⟩ × P z)
              × ((z : S) → ⟨ fst z ∈ F ⟩ → P z → ⟨ fst z ∈ y ⟩)
```

外延集合构造子的读取是定义性的：构造子的满足字面上就是两个隶属方向的二元组，其中性质在由约束变元延拓后的环境中求值。

```agda
module _ {j : ℕ} (y F : Fin j) (φ : Formula S (1 + j)) (δ : S ^ j) where
  extB-out : ⟨ δ ⊨ extB y F φ ⟩ → ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩)
  extB-out h = h
```

填充同样是定义性的：外延事实恰是构造子的满足。

```agda
  extB-in : ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩) → ⟨ δ ⊨ extB y F φ ⟩
  extB-in h = h
```

假定 `y` 与 `y'` 在 `F` 上满足同一个外延条件：对 `F` 中的元素而言，属于任一集合都由性质 `P` 刻画。外延性把二者底层集合的相等化为两个隶属转换。正向转换先用 `y` 的外延事实向外读出成员满足的条件，再用 `y'` 的外延事实向内得到该成员属于 `y'`。

```agda
ext-unique : (y y' F : S) (P : S → Type (ℓ-suc ℓ))
           → ExtFact (fst y) (fst F) P → ExtFact (fst y') (fst F) P → fst y ≡ fst y'
ext-unique y y' F P (o1 , i1') (o2 , i2') =
  cong fst (extensionalL {a = y} {b = y'} (λ z → ⇔toPath
    (λ hz → i2' z (o1 z hz .fst) (o1 z hz .snd))
```

反向转换补全该双条件：右侧的成员先被认作 `F` 中满足该性质的元素，外延事实的另一半随即返回它在 `y` 中的隶属。两个转换复合起来，就得到 `y` 与 `y'` 的底层集合相等；被同一视的是底层集合，而不是任何选定的编码证据。

```agda
    (λ hz → i1' z (o2 z hz .fst) (o2 z hz .snd))))
```

要使用子公式的值，先固定表槽 `T`、元数槽 `ar`、载荷槽 `a`，以及需要四个新条目的主体。读式会揭示一条匹配的表对 `(c₁,ya)`，并在旧环境前依次放入值 `ya`、键 `c₁`、容纳配对分量的集合，以及表条目本身的可构造代表。

```agda
module _ {j : ℕ} (T ar a : Fin j) (body : Formula S (4 + j)) (δ : S ^ j) where
  private
    Tv = fst (lookup T δ)
    TS = lookup T δ
    A = fst (lookup ar δ)
```

记投影后的元数为 `A`，投影后的载荷为 `Av`。子键的匹配条件便是等式 `fst c₁ ≡ pr A Av`；这个写法清楚地区分了集合论编码的键与提供其两个分量的宿主层槽位。

```agda
    Av = fst (lookup a δ)
```

若 `subAt` 成立，则每条底层配对为 `(c₁,ya)` 且键满足 `c₁=(A,Av)` 的表条目都会推出主体。主体在 `ya ∷ c₁ ∷ s ∷ e' ∷ δ` 处求值，其中 `e'` 表示该表条目，`s` 只是用于暴露两个配对分量的容纳集合。二者都不是额外的语义值。

```agda
  subAt-out : ⟨ δ ⊨ subAt T ar a body ⟩ → (c₁ ya : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩)
            → fst c₁ ≡ pr A Av
            → ⟨ (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
                 ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩
  subAt-out h c₁ ya m e =
```

证明先把表上的有界全称用于 `(c₁,ya)` 的具体代表 `e'`。随后，配对读式给出两个分量 `c₁` 与 `ya`；最后，`pr-in` 把等式 `c₁=(A,Av)` 转成内部蕴涵所需的前件。余下的正是四槽扩展环境处的主体。

```agda
    useBoth i0 (down TS (pr (fst c₁) (fst ya)) m ∷ δ) c₁ ya refl (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body)
      (h (down TS (pr (fst c₁) (fst ya)) m) m)
      (pr-in i1 (sh 4 ar) (sh 4 a)
        (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
           ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) e)
```

填充是其反向：若对每个匹配的表条目连同其容器都能证明主体，则表条目上的有界全称成立。注意该读取器不做的事：它不选定某个条目，也不断言值 `ya` 唯一；它是对所有匹配条目量化。

```agda
  subAt-in : ((c₁ ya s e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A Av
              → ⟨ (ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
           → ⟨ δ ⊨ subAt T ar a body ⟩
  subAt-in g e' e'∈ = bothAll-in i0 (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body) (e' ∷ δ)
    (λ c₁ ya s s∈ c₁∈ ya∈ e hp → g c₁ ya s e' e'∈ e (pr-out i1 (sh 4 ar) (sh 4 a) (ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp))
```

第二条子子句读取针对抬升元数的形状陈述：其主体延拓六个槽位，因为量化公式的子公式要在抬升后的元数处读取。

```agda
module _ {j : ℕ} (T ar a : Fin j) (body : Formula S (6 + j)) (δ : S ^ j) where
  private
    Tv = fst (lookup T δ)
    TS = lookup T δ
    A = fst (lookup ar δ)
```

外层公式的元数值被命名，抬升后的元数则在证明内部单独恢复。

```agda
    Av = fst (lookup a δ)
```

抬升读式使用键为 `(ar',Av)` 的表条目，并要求等式 `fst ar' ≡ sucV A`。主体在 `ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ` 处求值；两个容纳集合 `s'` 与 `s` 只是让有界公式能够取得抬升键和表条目的分量。

```agda
  subSucAt-out : ⟨ δ ⊨ subSucAt T ar a body ⟩ → (c₁ ya ar' : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩)
               → (e : fst c₁ ≡ pr (fst ar') Av) → fst ar' ≡ sucV A
               → ⟨ (ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ ya ∷ c₁
                    ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
                    ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩
```

证明从给定表条目出发，先分解 `(c₁,ya)` 得到四槽陈述 `h4`。随后向 `fstAll` 提供候选第一分量 `ar'`，用 `pr-in` 证明 `c₁=(ar',Av)`，再用 `suc-in` 证明 `ar'=suc A`。主体可用之前所需的守卫恰好就是这两个等式。

```agda
  subSucAt-out h c₁ ya ar' m e es =
    (h4 (container c₁ ar' (lookup a δ) e .fst) (container c₁ ar' (lookup a δ) e .snd .fst)
        ar' (container c₁ ar' (lookup a δ) e .snd .snd .fst)
        (pr-in (sh 2 i1) i0 (sh 2 (sh 4 a)) δ6 e))
      (suc-in (sh 6 ar) i0 δ6 es)
```

局部名称 `e'S` 是特定表条目 `(c₁,ya)` 的可构造代表，由该配对属于 `T` 得到。环境 `δ4` 随后在 `δ` 前依次放入 `ya`、`c₁`、容纳其配对分量的集合与 `e'S`；其中并没有整张表的呈现。

```agda
    where
    e'S = down TS (pr (fst c₁) (fst ya)) m
    δ4 : S ^ (4 + j)
    δ4 = ya ∷ c₁ ∷ container e'S c₁ ya refl .fst ∷ e'S ∷ δ
    δ6 : S ^ (6 + j)
```

把 `useBoth` 用于选定的表条目，会一步消去表上的外层量化与配对分解。所得 `h4` 是 `δ4` 处余下的 `fstAll` 陈述；它仍需取得 `c₁` 的候选第一分量，并验证该分量就是后继元数。

```agda
    δ6 = ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ δ4
    h4 : ⟨ δ4 ⊨ fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body) ⟩
    h4 = useBoth i0 (e'S ∷ δ) c₁ ya refl (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)) (h e'S m)
```

反向证明只需对每一种可能的表条目分解以及其键的每一种可能第一分量分解，一致地证明主体。前提中的两个等式保证只有键为 `(suc A,Av)` 的条目相关；证明不会全局选定某个表条目或抬升元数。

```agda
  subSucAt-in : ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
                 → fst c₁ ≡ pr (fst ar') Av → fst ar' ≡ sucV A
                 → ⟨ (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
              → ⟨ δ ⊨ subSucAt T ar a body ⟩
  subSucAt-in g e' e'∈ = bothAll-in i0 (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)) (e' ∷ δ)
```

引入证明接收两层全称配对读式暴露出的分量。它用 `pr-out` 恢复等式 `c₁=(ar',Av)`，用 `suc-out` 恢复 `ar'=suc A`，再把这些等式、表隶属事实与六槽环境交给一致前提 `g`。

```agda
    (λ c₁ ya s s∈ c₁∈ ya∈ e s' s'∈ ar' ar'∈ hp hs →
      g c₁ ya ar' s s' e' e'∈ e
        (pr-out (sh 2 i1) i0 (sh 2 (sh 4 a)) (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp)
        (suc-out (sh 6 ar) i0 (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hs))
```

`TmIsV t z v` 在命题截断下记录词项码的两种可能形状。常元情形为 `t=(#0,v)`；变元情形则只说存在索引 `i`，使 `t=(#1,i)` 且图条目 `(i,v)` 属于 `z`。对于任意关系 `z`，这个陈述不包含单值性或唯一性结论。

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

局部读式由五个宿主层槽位参数化：词项码、环境图、候选值以及两个标签数码。前提 `q0` 与 `q1` 把最后两个槽分别认同为 `#0` 与 `#1`；局部名称 `Tv` 与 `Z` 则把词项码和图投影到编码等式所在的累积层级。

```agda
module _ {j : ℕ} (t z v N0 N1 : Fin j) (δ : S ^ j)
  (q0 : fst (lookup N0 δ) ≡ # 0) (q1 : fst (lookup N1 δ) ≡ # 1) where
  private
    Tv = fst (lookup t δ)
    Z = fst (lookup z δ)
```

其余两个投影分别命名候选值 `Vv` 与标签一槽中实际存放的集合 `N1v`。内部公式引用的是 `N1v`，而 `TmIsV` 的变元分支使用典范数码 `#1`，所以证明必须沿 `q1` 搬运等式。

```agda
    Vv = fst (lookup v δ)
    N1v = fst (lookup N1 δ)
```

内层有界存在遍历的是图 `z` 的条目 `q`，并非索引本身。其配对原子断言 `q=(i,v)`，其中索引 `i` 已经作为词项码的第二分量被恢复。因此，内部公式表示图中含有把这个固定索引与候选值配对的条目。

```agda
    inner : Formula S (2 + j)
    inner = ∃̇∈ (var (sh 2 z)) (prAtL i0 i1 (sh 3 v))
```

`Inner i s` 重新包装这个有界存在的语义。它只给出一个图条目 `q`、证明 `q∈Z`，以及配对原子 `q=(i,Vv)` 在 `q ∷ i ∷ s ∷ δ` 处成立的证据。槽位 `s` 是用于暴露词项码分量的容纳集合。

```agda
    Inner : (i s : S) → Type (ℓ-suc ℓ)
    Inner i s = ∥ Σ[ q ∈ S ] (⟨ fst q ∈ Z ⟩ × ⟨ (q ∷ i ∷ s ∷ δ) ⊨ prAtL i0 i1 (sh 3 v) ⟩) ∥₁
```

`Outer` 包装从 `sndEx` 读出的整个变元分支：只存在一个载荷代表 `i` 与一个容纳集合 `s`，使 `Tv=pr N1v (fst i)`，并且内层有界存在在 `i ∷ s ∷ δ` 处成立。这个等式把词项码认同为标签一配对，并没有把 `i` 与标签本身同一视。

```agda
    Outer : Type (ℓ-suc ℓ)
    Outer = ∥ Σ[ i ∈ S ] Σ[ s ∈ S ] ((Tv ≡ pr N1v (fst i)) × ⟨ (i ∷ s ∷ δ) ⊨ inner ⟩) ∥₁
```

从内层见证 `q` 出发，`pr-out` 给出 `fst q=pr (fst i) Vv`；沿该等式搬运已知的隶属 `q∈Z`，便得到所需的图条目 `(i,Vv)` 属于 `Z`。与此同时，`q1` 把外层等式中的实际标签槽 `N1v` 改写为 `#1`。这两部分恰好组成 `TmIsV` 的变元分支。

```agda
    viaQ : (i s : S) → Tv ≡ pr N1v (fst i) → Inner i s → TmIsV Tv Z Vv
    viaQ i s e = PT.map
      (λ { (q , (q∈ , hp)) → inr (fst i , ( e ∙ cong (λ a → pr a (fst i)) q1
         , subst (λ u → ⟨ u ∈ Z ⟩) (pr-out i0 i1 (sh 3 v) (q ∷ i ∷ s ∷ δ) hp) q∈ )) })
```

`viaI` 把只保留存在性的外层分解消去到 `TmIsV`。由于 `TmIsV` 本身也经过命题截断，这种消去只会逐个转换局部配对分解，不会选出一个分解供后文使用。

```agda
    viaI : Outer → TmIsV Tv Z Vv
    viaI = PT.rec squash₁ (λ { (i , s , (e , hq)) → viaQ i s e hq })
```

对象公式 `tmIs` 是两种码形状的析取。在常元分支中，`pr-out` 读出 `Tv=pr(q0,Vv)`，再由 `q0=#0` 把它化为 `TmIsV` 的第一分支。在变元分支中，`sndEx-out` 产生 `Outer`，随后由 `viaI` 转成图隶属分支。

```agda
    cases : ⟨ δ ⊨ prAtL t N0 v ⟩ ⊎ ⟨ δ ⊨ sndEx t N1 inner ⟩ → TmIsV Tv Z Vv
    cases (inl h) = ∣ inl (pr-out t N0 v δ h ∙ cong (λ a → pr a Vv) q0) ∣₁
    cases (inr h) = viaI (sndEx-out t N1 inner δ h)
```

公开消去式 `tmIs-out` 在外层析取的命题截断之下完成上述情形分析。其结论只涉及一个给定候选值 `Vv`，并不证明两个候选值相等。若 `Z` 是任意多值关系，同一个变元码可以在多个值处满足 `tmIs`。

```agda
  tmIs-out : ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ → TmIsV Tv Z Vv
  tmIs-out h = PT.rec squash₁ cases h
```

在反向证明中，`build` 把任一具体码形状重新构造成 `tmIs` 的满足。常元等式由 `pr-in` 转换；在变元情形中，证明先把载荷索引与图条目表示成 `S` 的元素，再重建 `sndEx` 的嵌套有界存在。

```agda
  private
    build : (Tv ≡ pr (# 0) Vv) ⊎ (Σ[ i ∈ V ℓ ] ((Tv ≡ pr (# 1) i) × ⟨ pr i Vv ∈ Z ⟩))
          → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
    build (inl e) = ∣ inl (pr-in t N0 v δ (e ∙ cong (λ a → pr a Vv) (sym q0))) ∣₁
    build (inr (i , (e , hp))) = ∣ inr (fillSnd t δ (lookup N1 δ) iS e' inner hq N1 refl) ∣₁
```

`iS` 是载荷 `i` 的可构造代表，由配对等式 `Tv=(#1,i)` 的第二分量恢复。`qS` 是图条目 `(i,Vv)` 的可构造代表，由该配对属于 `Z` 得到。它们都是 `S` 内的见证，并非新的语义索引或语义值。

```agda
      where
      iS : S
      iS = sndS (lookup t δ) (# 1) i e
      qS : S
      qS = down (lookup z δ) (pr i Vv) hp
```

等式 `e'` 把典范标签等式改写成 `sndEx` 所需的实际标签一槽。辅助环境 `δ3` 在 `δ` 前依次放入图条目 `qS`、载荷代表 `iS` 与外层词项码配对的容纳集合。余下的目标 `hq` 正是 `iS ∷ container ∷ δ` 处的内层有界存在。

```agda
      e' : Tv ≡ pr N1v (fst iS)
      e' = e ∙ cong (λ a → pr a i) (sym q1)
      δ3 : S ^ (3 + j)
      δ3 = qS ∷ iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ
      hq : ⟨ (iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ) ⊨ inner ⟩
```

为证明 `hq`，从图中选择 `qS`。其隶属事实就是给定的 `hp`，而 `pr-in` 以自反性证明其底层集合是 `iS` 与 `Vv` 的配对。这恰好给出变元分支所需的图条目。

```agda
      hq = ∣ qS , (hp , pr-in i0 i1 (sh 3 v) δ3 refl) ∣₁
```

最后，`tmIs-in` 把 `TmIsV` 中的命题截断消去到表示 `tmIs` 满足的命题，并对任一分支应用 `build`。它与 `tmIs-out` 合在一起给出两个语义方向，同时仍不引入全局选择或唯一性结论。

```agda
  tmIs-in : TmIsV Tv Z Vv → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
  tmIs-in = PT.rec (snd (δ ⊨ tmIs t z v N0 N1)) build
```

`Frame` 固定表 `T`、载体 `w`、码定义域 `C` 与环境塔 `E` 的宿主层槽位，并固定十个标签槽 `N` 和外围赋值 `γ`。前提 `Tags γ N` 把每个标签槽与相应数码同一视，使由 `k : Fin 10` 选出的子句能够读成关系 `relN (toℕ k)`。

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

框架通过一系列有界全称逐层拆开。在最内层，`inner9 k` 遍历每个表条目，并在该条目的第一分量为 `c` 时用 `sndAll` 暴露值 `yc`；所得十二槽环境正是 `relN (toℕ k)` 必须成立之处。这是对所有匹配条目的全称条件，并非寻找某个值的存在式。

```agda
    module Cl = Clause T w C E N
    module R = Rel T w N
    inner9 : Fin 10 → Formula S (9 + m)
    inner9 k = ∀̇∈ (var (sh 9 T)) (sndAll i0 i5 (R.relN (toℕ k)))
    inner7 : Fin 10 → Formula S (7 + m)
```

前两层负责暴露嵌套的键。`inner4 k` 遍历每个第一分量为当前元数 `ar` 的 `c∈C`，取得其载荷 `p`；`inner7 k` 随后要求 `p` 的标签等于 `N k` 槽中的数码，并暴露余下数据 `r`。每次配对分解都会在前端加入分量与容纳集合，因此必须用移位保持对旧框架槽位的访问。

```agda
    inner7 k = sndAll i0 (sh 7 (N k)) (inner9 k)
    inner4 : Fin 10 → Formula S (4 + m)
    inner4 k = ∀̇∈ (var (sh 4 C)) (sndAll i0 i2 (inner7 k))
```

对于一条子句实例，`At` 固定塔配对 `(ar,F)`、公式键 `c=(ar,p)`、带标签载荷 `p=(N k,r)` 与表配对 `(c,yc)`。隶属 `q∈` 和 `e∈` 分别涉及 `E` 与 `T` 中投影后的配对；该模块本身不证明 `c∈C`，不解码 `r`，也不证明表值唯一。

```agda
  module At (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩)
            (ec : fst c ≡ pr (fst ar) (fst p)) (k : Fin 10)
            (ep : fst p ≡ pr (fst (lookup (N k) γ)) (fst r))
            (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩) where
    qS eS : S
```

`qS` 与 `eS` 把两个投影后的配对隶属提升回可构造载体中的元素。它们的底层集合分别按定义为 `pr (fst ar) (fst F)` 与 `pr (fst c) (fst yc)`。二者只充当代表，使组装十二槽环境时能够应用有界配对读式。

```agda
    qS = down (lookup E γ) (pr (fst ar) (fst F)) q∈
    eS = down (lookup T γ) (pr (fst c) (fst yc)) e∈
```

框架从实际的塔成员 `qS` 开始，其底层配对是 `(ar,F)`。新增的四个槽位记录 `F`、`ar`、配对分解的见证与 `qS`；随后的三个槽位记录载荷 `p`、`c=(ar,p)` 的见证与代码 `c`。因此，逐层扩展的环境既保留数学数据，也保留对象语言子句取得这些数据时所用的有界见证。

```agda
    δ4 : S ^ (4 + m)
    δ4 = F ∷ ar ∷ container qS ar F refl .fst ∷ qS ∷ γ
    δ7 : S ^ (7 + m)
    δ7 = p ∷ container c ar p ec .fst ∷ c ∷ δ4
    δ9 : S ^ (9 + m)
```

十二槽环境完成这层嵌套。候选取值 `yc` 居首，随后是暴露表配对 `(c,yc)` 两个分量的容纳集合，以及底层集合正是该配对的实际表成员 `eS`；再后是先前九个对象。关系体就在这个环境中读取。

```agda
    δ9 = r ∷ container p (lookup (N k) γ) r ep .fst ∷ δ7
    δ12 : S ^ (12 + m)
    δ12 = yc ∷ container eS c yc refl .fst ∷ eS ∷ δ9
```

向外读式从第 `k` 条子句的满足出发，并固定该子句一个框架实例的全部匹配数据：来自塔配对的 `ar` 与 `F`、`C` 中的代码 `c=(ar,p)`、带标签的载荷 `p=(#k,r)`，以及满足 `(c,yc)` 属于 `T` 的候选取值 `yc`。随后，它返回相应十二槽环境处 `relN (toℕ k)` 的满足。这里的表前提是配对 `(c,yc)` 的隶属；实际表成员及其容纳集合都在局部构造。

```agda
  clause-out : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩
             → (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩) → ⟨ fst c ∈ Cv ⟩
             → (ec : fst c ≡ pr (fst ar) (fst p)) → (ep : fst p ≡ pr (# (toℕ k)) (fst r))
             → (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩)
             → ⟨ At.δ12 ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈ ⊨ R.relN (toℕ k) ⟩
```

匹配数据固定后，模块 `A` 为全部十二个框架槽给出一个彼此相容的实现。第一次消去打开塔配对，最后的 `useSnd` 把实际表成员打开为 `(c,yc)`；二者之间还必须经过代码层与标签层。先命名 `h4`，正是为了表明结论来自对同一条外层子句的逐次特化，而不是另行假定构造子关系。

```agda
  clause-out k h ar F c p r yc q∈ c∈ ec ep e∈ =
    useSnd i0 (A.eS ∷ A.δ9) c yc refl (R.relN (toℕ k)) i5 refl (h9 A.eS e∈)
    where
    module A = At ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈
    h4 : ⟨ A.δ4 ⊨ inner4 k ⟩
```

三条中间判断标出共同框架的三个语义层次。在 `δ4` 处，`h4` 已打开塔条目 `(ar,F)`，可以开始考察 `C` 中的代码；在 `δ7` 处，`h7` 还分解了 `c=(ar,p)`；在 `δ9` 处，`h9` 已把 `p` 识别为标签 `k` 的载荷 `r`，可以考察 `T` 中的条目。最后一次消去把所选表成员分解为 `(c,yc)`，由此抵达构造子关系。

```agda
    h4 = useBoth i0 (A.qS ∷ γ) ar F refl (inner4 k) (h A.qS q∈)
    h7 : ⟨ A.δ7 ⊨ inner7 k ⟩
    h7 = useSnd i0 (c ∷ A.δ4) ar p ec (inner7 k) i2 refl (h4 c c∈)
    h9 : ⟨ A.δ9 ⊨ inner9 k ⟩
    h9 = useSnd i0 A.δ7 (lookup (N k) γ) r (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) (inner9 k) (sh 7 (N k)) refl h7
```

反向构造假定：每个完整匹配的框架都能证明构造子关系。这样的框架包含塔成员 `q=(ar,F)`、`C` 中的代码 `c=(ar,p)`、标签分解 `p=(#k,r)`、表成员 `e=(c,yc)`，以及四个配对见证 `s`、`s1`、`s2` 与 `s3`。若对所有这些数据都能在所示环境中证明该关系，便恰好具备重建第 `k` 条子句所需的前提。

```agda
  clause-in : (k : Fin 10)
            → ((q ar F s c p s1 r s2 e yc s3 : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F)
               → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (fst ar) (fst p) → fst p ≡ pr (# (toℕ k)) (fst r)
               → ⟨ fst e ∈ Tv ⟩ → fst e ≡ pr (fst c) (fst yc)
               → ⟨ (yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) ⊨ R.relN (toℕ k) ⟩)
```

证明按逻辑次序重建这个全称量化的框架。它先处理 `E` 中任意的 `q` 以及每个被暴露出的分解 `q=(ar,F)`，再处理 `C` 中任意的 `c` 以及每个匹配的分解 `c=(ar,p)`；继而识别 `p` 的标签与载荷，最后处理 `T` 中任意的 `e` 以及每个分解 `e=(c,yc)`。每次有界引入都把新值放在环境头部，而相伴的 `s` 变量保留公式所需的配对分解见证。

```agda
            → ⟨ γ ⊨ Cl.clause k ⟩
  clause-in k g q q∈ = bothAll-in i0 (inner4 k) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ eq c c∈ →
    sndAll-in i0 i2 (inner7 k) (c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ p s1 s1∈ p∈ ec →
      sndAll-in i0 (sh 7 (N k)) (inner9 k) (p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ r s2 s2∈ r∈ ep e e∈ →
        sndAll-in i0 i5 (R.relN (toℕ k)) (e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ yc s3 s3∈ yc∈ ee →
```

调用宿主层规则 `g` 之前，证明把载荷等式与 `tg k` 复合，将标签槽中存放的集合改写为典范数码 `#k`。因此，规则收到的恰是向外读式中出现的等式 `p=(#k,r)`。这样，`clause-in` 与 `clause-out` 就在每个匹配框架上给出第 `k` 条子句与其关系之间的两个方向。

```agda
          g q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec (ep ∙ cong (λ a → pr a (fst r)) (tg k)) e∈ ee))))
```

全定义性向外读取为经过命题截断的存在陈述：对码定义域的每个成员，全定义性子句保证存在以该成员为第一分量的表条目，而表条目经过命题截断的分解会恢复取值 `yc`。

```agda
  total-out : ⟨ γ ⊨ Cl.total ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
  total-out h c c∈ = PT.rec squash₁
    (λ { (e , (e∈ , hs)) → PT.map
      (λ { (yc , s , (ee , _)) → yc , subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈ })
      (sndEx-out i0 i1 ⊤̇ (e ∷ c ∷ γ) hs) })
```

固定 `c∈C` 后，把既有假设 `h` 用于 `c`，便在命题截断下得到一个表成员 `e`、它属于 `T` 的证明以及一条分解陈述。读式 `sndEx-out` 再把 `e` 分解为 `(c,yc)`，并沿该等式搬运 `e` 的隶属证明，从而得到 `(c,yc)∈T`。两层分解都由命题截断隐藏，因此结论只给出存在性，并不选取典范取值。

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

反过来，假定对 `C` 中每个 `c`，都有一个经过命题截断的存在陈述，断言某个 `yc` 满足 `(c,yc)` 属于 `T`。`down` 把这条隶属证明实现为 `T` 的一个元素 `e : S`，其底层集合正是该配对；`fillSnd` 再给出把 `e` 分解回 `c` 与 `yc` 的有界见证。余下的主体为真，故这些数据足以构造全定义性子句，同时既不全局选择取值，也不主张唯一性。

```agda
  total-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁) → ⟨ γ ⊨ Cl.total ⟩
  total-in g c c∈ = PT.map
    (λ { (yc , m) → down (lookup T γ) (pr (fst c) (fst yc)) m
       , ( m , fillSnd i0 (down (lookup T γ) (pr (fst c) (fst yc)) m ∷ c ∷ γ) c yc refl ⊤̇ (λ b → b) i1 refl ) })
    (g c c∈)
```

定义域约束从 `T` 的任意元素 `e` 出发，而不是预先给定一个配对。其向外读法在命题截断下恢复 `c` 与 `yc`，满足 `e=(c,yc)` 且 `c` 属于 `C`。因此，表的每个成员都以给定定义域中的代码为第一分量；这个结论既不典范地选定分解，也不说明一个代码只有一个取值。

```agda
  onC-out : ⟨ γ ⊨ Cl.onC ⟩ → (e : S) → ⟨ fst e ∈ Tv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
  onC-out h e e∈ = PT.map (λ { (c , yc , s , (ee , c∈)) → c , yc , (ee , c∈) })
    (bothEx-out i0 (var i1 ∈̇ var (sh 4 C)) (e ∷ γ) (h e e∈))
```

反向读法恰好要求 `T` 的每个成员都具有上述经过命题截断的分解，再把该分解注入 `onC` 的两层有界存在量词。两条读法合起来把 `onC` 精确解释为「每个表成员的第一投影属于 `C`」。它与全定义性结合后确定表的定义域投影，但仍不使这张表成为单值关系。

```agda
  onC-in : ((e : S) → ⟨ fst e ∈ Tv ⟩ → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁)
         → ⟨ γ ⊨ Cl.onC ⟩
  onC-in g e e∈ = PT.rec (snd ((e ∷ γ) ⊨ bothEx i0 (var i1 ∈̇ var (sh 4 C))))
    (λ { (c , yc , (ee , c∈)) → fillBoth i0 (e ∷ γ) c yc ee (var i1 ∈̇ var (sh 4 C)) c∈ })
    (g e e∈)
```

## 读取构造子关系

构造子读式在一个框架 `δ` 上工作，它在原来的 `m` 槽环境前增加了十二个槽位。因此，原环境中的 `T`、`w` 与十个数码槽 `N` 都位于这段前缀之后；框架自身则把候选取值 `yc` 放在 `i0`，把构造子载荷 `r` 放在 `i3`。固定这些位置后，无论读取哪一种构造子，每条关系读式都能共用同一个外层框架。

```agda
module RelRead {m : ℕ} (T w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (12 + m)) where
  private
    module R = Rel T w N
    yc = lookup i0 δ
    r = lookup i3 δ
```

其余局部名称标出环境集槽 `F` 与元数槽 `ar`，并一次性投影出表的底层集合 `Tv`、元数值 `A` 与构造子载荷 `Rv`。这样，后续关系读式就能直接在累积层级中陈述前提。

```agda
    F = lookup i8 δ
    ar = lookup i9 δ
    Tv = fst (lookup (sh 12 T) δ)
    A = fst ar
    Rv = fst r
```

对任意进一步扩展的局部环境 `env`，`Ext env φ` 都陈述外层表取值 `yc` 的精确外延性质。元素 `z` 属于 `yc`，当且仅当它属于元数相应的环境集 `F`，并且把 `z` 放入 `env` 的新头槽后公式 `φ` 成立。因此，`env` 的原有槽位在 `φ` 内都向后移动一个位置读取。

```agda
  Ext : ∀ {k} (env : S ^ k) (φ : Formula S (1 + k)) → Type (ℓ-suc ℓ)
  Ext env φ = ExtFact (fst yc) (fst F) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)
```

对于二元联结词，载荷 `r` 必须分解为两个子公式码 `a` 与 `b`，而键 `c₁=(A,a)`、`c₂=(A,b)` 必须分别在表中具有取值 `ya`、`yb`。由这些假设，`bin-out` 在命题截断下返回五个辅助见证：一个见证 `r=(a,b)` 的容纳集合，以及每个子公式对应的一个 `T` 的实际成员和一个分解容纳集合。数学结论是关于外层取值 `yc` 的 `Ext` 事实，其主体以联结词 `op` 组合对 `ya` 与 `yb` 的隶属判断。

```agda
  bin-out : (op : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.binRel op ⟩
          → (a b c₁ ya c₂ yb : S) → Rv ≡ pr (fst a) (fst b)
          → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr A (fst a)
          → ⟨ pr (fst c₂) (fst yb) ∈ Tv ⟩ → fst c₂ ≡ pr A (fst b)
          → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ e₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
```

之所以打包这五个见证，只是因为对象语言的有界量词隐藏了各次配对分解。打开载荷后，第一次 `subAt-out` 读取左子公式键处的取值，第二次读取右子公式键处的取值；最内层的 `extB` 随即给出 `yc` 的精确外延。这个结论并不说明表为任一子公式键唯一选定了取值。

```agda
              Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op) ∥₁
  bin-out op h a b c₁ ya c₂ yb er m₁ e₁ m₂ e₂ =
    ∣ container r a b er .fst , container e₁S c₁ ya refl .fst , e₁S , container e₂S c₂ yb refl .fst , e₂S ,
      subAt-out (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)) δ19
        (subAt-out (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op))) δ15
```

第一步是在十二槽框架内打开载荷等式 `r=(a,b)`。这一步加入配对容纳集合，并产生 `δ15`，即在旧框架前依次加入 `b`、`a` 与该容纳集合。随后两层嵌套的子值读式从左到右进行，因而其中隐藏的表见证仍留在外层命题截断之内。

```agda
          (useBoth i3 δ a b er (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)))) h)
          c₁ ya m₁ e₁)
        c₂ yb m₂ e₂ ∣₁
    where
    δ15 : S ^ (15 + m)
```

关于 `(c₁,ya)` 的隶属证明本身并不直接给出结构 `S` 的元素；`down` 把它实现为 `e₁S : S`，即 `T` 中底层配对为 `(c₁,ya)` 的一个实际成员。环境 `δ19` 再把 `ya`、`c₁`、二者的配对容器与 `e₁S` 加到 `δ15` 前面。这四个槽位恰是第一次 `subAt` 读取所需的框架。

```agda
    δ15 = b ∷ a ∷ container r a b er .fst ∷ δ
    e₁S : S
    e₁S = down (lookup (sh 15 T) δ15) (pr (fst c₁) (fst ya)) m₁
    δ19 : S ^ (19 + m)
    δ19 = ya ∷ c₁ ∷ container e₁S c₁ ya refl .fst ∷ e₁S ∷ δ15
```

同一构造把第二条隶属证明实现为 `e₂S : S`，即底层配对为 `(c₂,yb)` 的实际表成员。第二次 `subAt-out` 在扩展 `δ19` 时会补上相应的配对容器。因此，`binBody` 可以同时读取两个子公式取值，而两条隶属证明都没有被提升为从表中进行的全局选择。

```agda
    e₂S : S
    e₂S = down (lookup (sh 19 T) δ19) (pr (fst c₂) (fst yb)) m₂
```

反向构造从一条适用于二元框架所有可能分解的规则开始。除子公式码与取值外，该规则还接收载荷容器、两个实际表成员、它们的配对容器，以及证明相应键分别为 `(A,a)`、`(A,b)` 的等式。它必须在原十二槽框架前加入这十一个对象所得的环境中，给出外层取值 `yc` 的 `Ext` 事实。

```agda
  bin-in : (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
         → ((a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ : S) → Rv ≡ pr (fst a) (fst b)
            → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A (fst a)
            → ⟨ fst e₂ ∈ Tv ⟩ → fst e₂ ≡ pr (fst c₂) (fst yb) → fst c₂ ≡ pr A (fst b)
            → Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op))
```

证明引入两个实参量词与关系容器，然后为左右两条表条目打开两层嵌套的 subAt 子句，各自引入其码、取值与对等式。

```agda
         → ⟨ δ ⊨ R.binRel op ⟩
  bin-in op g = bothAll-in i3 (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)))) δ
    (λ a b s s∈ a∈ b∈ er →
      subAt-in (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op))) (b ∷ a ∷ s ∷ δ)
        (λ c₁ ya s₁ e₁ e₁∈ ee₁ e₁' →
```

在最内层，宿主侧规则接收全部十一个对象并产出外延事实，该事实被运入最内层的 subAt 子句。引入的嵌套与量化子句的嵌套互为镜像。

```agda
          subAt-in (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)) (ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ)
            (λ c₂ yb s₂ e₂ e₂∈ ee₂ e₂' →
              g a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂')))
```

对无界量词而言，载荷 `r` 就是子公式码。匹配的子公式键形如 `c₁=(ar',r)`，其中 `ar'` 是外层元数 `A` 的后继，并且 `(c₁,ya)` 属于表。由这些数据，`qu-out` 返回三个隐藏见证，以及关于外层取值 `yc` 的 `Ext` 事实。在该外延事实中，`ya` 提供量化体所读取的子公式满足集；被刻画的集合并不是 `ya` 本身。

```agda
  qu-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → ⟨ δ ⊨ R.quRel q ⟩
         → (c₁ ya ar' : S) → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A
         → ∥ Σ[ s ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ] Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q) ∥₁
  qu-out q h c₁ ya ar' mem e es =
    ∣ container e'S c₁ ya refl .fst , container c₁ ar' r e .fst , e'S
```

三个见证各有不同作用。`e'S` 是 `T` 中实现配对 `(c₁,ya)` 的实际成员；一个容器见证该配对，另一个容器见证 `c₁=(ar',r)`。通用的后继元数读式已经能够把这些见证与 `ar'=suc A` 结合，再揭示最内层的外延事实。

```agda
    , subSucAt-out (sh 12 T) i9 i3 (extB i6 i14 (R.quBody q)) δ h c₁ ya ar' mem e es ∣₁
    where
    e'S : S
    e'S = down (lookup (sh 12 T) δ) (pr (fst c₁) (fst ya)) mem
```

反过来，假定每个实际表成员 `e'=(c₁,ya)`，只要其键满足 `c₁=(ar',r)` 与 `ar'=suc A`，就在任意两个配对容器下给出所需的 `Ext` 事实。这条全称前提足以重建 `quRel` 的有界结构；它考察所有匹配条目，并不预设子公式取值 `ya` 唯一。

```agda
  qu-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
           → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A
           → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q))
        → ⟨ δ ⊨ R.quRel q ⟩
```

无界量词不需要额外分解载荷，因为其载荷 `r` 本身就是子公式码。因此，后继元数子值的一般反向读式具有 `quRel` 恰好所需的前提与结论；应用一次便能重建整个关系，同时保留对所有匹配表条目的全称读取。

```agda
  qu-in q g = subSucAt-in (sh 12 T) i9 i3 (extB i6 i14 (R.quBody q)) δ g
```

有界量词的载荷有两个句法分量：界词项码 `t` 与子公式码 `a`，故 `r=(t,a)`。子公式键是在后继元数处的 `c₁=(ar',a)`，其表取值为 `ya`。四个见证在命题截断下打包在一起，记录载荷配对、子公式表成员与两个相关的配对分解。所得 `Ext` 事实刻画外层取值 `yc`；在其主体内部，词项码被求值，而所得词项值限制量化范围。

```agda
  bq-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
         → (c : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.bqRel q c ⟩
         → (t a c₁ ya ar' : S) → Rv ≡ pr (fst t) (fst a)
         → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
         → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ]
```

证明恰好打包四个见证：`r=(t,a)` 的容器、配对 `(c₁,ya)` 的容器与实际表成员，以及 `c₁=(ar',a)` 的容器。`useBoth` 打开载荷后，`subSucAt-out` 在后继元数处读取子公式取值。传给 `Ext` 的环境在十二槽框架前增加九个局部槽位，而 `Ext` 自身再把候选编码环境 `z` 放入一个新的头槽，恰与 `bqBody` 的元数吻合。

```agda
             Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c) ∥₁
  bq-out q c h t a c₁ ya ar' er mem e es =
    ∣ container r t a er .fst , container e'S c₁ ya refl .fst , container c₁ ar' a e .fst , e'S ,
      subSucAt-out (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c)) δ15
        (useBoth i3 δ t a er (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c))) h)
```

打开载荷会在原框架前增加三个槽位：子公式码 `a`、界词项码 `t`，以及见证 `r=(t,a)` 的容器。这便是环境 `δ15`。该记号表示原 `m` 槽环境前共有十五个槽位，因为 `δ` 已经包含十二个共同框架槽。

```agda
        c₁ ya ar' mem e es ∣₁
    where
    δ15 : S ^ (15 + m)
    δ15 = a ∷ t ∷ container r t a er .fst ∷ δ
    e'S : S
```

假设 `mem` 表示底层配对 `(c₁,ya)` 属于表集合。在移位后的表槽处应用 `down`，便把这条证明实现为 `e'S : S`，即具有所需底层集合的实际表元素。这个实现仅用于当前证明，并不是从全定义性中选择一个子公式取值。

```agda
    e'S = down (lookup (sh 15 T) δ15) (pr (fst c₁) (fst ya)) mem
```

反向前提量化九个对象，因为它必须接受载荷分解与子公式表分解的每一种实现。这里 `s₁` 是表成员的配对容器，`s'` 是后继元数子公式键的容器；二者都不是量化公式所约束的语义见证。在给定隶属证明与配对等式后，该前提提供关于 `yc` 的 `Ext` 事实，从而局部确定有界量词关系。

```agda
  bq-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → (c : ∀ {j} → Formula S j → Formula S j → Formula S j)
        → ((t a s c₁ ya ar' s₁ s' e' : S) → Rv ≡ pr (fst t) (fst a)
           → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
           → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
```

为重建 `bqRel`，`bothAll-in` 先处理构造子载荷的每个分解 `r=(t,a)`。在扩展后的环境中，`subSucAt-in` 再处理子公式键 `(suc A,a)` 的每个表条目。给定规则随后证明 `yc` 的精确外延条件；语义上的界值是在 `bqBody` 内部才被量化，并由 `tmIs` 把它与词项码 `t` 联系起来。

```agda
           → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c))
        → ⟨ δ ⊨ R.bqRel q c ⟩
  bq-in q c g = bothAll-in i3 (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c))) δ
    (λ t a s s∈ t∈ a∈ er →
      subSucAt-in (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c)) (a ∷ t ∷ s ∷ δ)
```

到最内层时，所有结构义务都已显式给出：载荷为 `(t,a)`，子公式表成员为 `(c₁,ya)`，其键为 `(ar',a)`，且 `ar'` 是 `A` 的后继。这些恰是规则 `g` 的假设，故它给出的外延事实可以闭合后继元数子值子句。此处的重建不使用任何关于 `ya` 唯一性的断言。

```agda
        (λ c₁ ya ar' s₁ s' e' e'∈ ee e es → g t a s c₁ ya ar' s₁ s' e' er e'∈ ee e es))
```

对原子公式而言，`t` 与 `u` 是载荷中存放的两个词项码，而不是它们的语义取值。打开 `r=(t,u)` 会加入一个配对容器，并留下关于外层表取值 `yc` 的 `Ext` 事实。在该环境中求值的 `atomBody` 会另行量化两个词项的候选取值，用 `tmIs` 验证它们，再应用选定的原子关系。

```agda
  atom-out : (rel : Formula S (18 + m)) → ⟨ δ ⊨ R.atomRel rel ⟩
           → (t u : S) → Rv ≡ pr (fst t) (fst u)
           → ∥ Σ[ s ∈ S ] Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel) ∥₁
  atom-out rel h t u er = ∣ container r t u er .fst , useBoth i3 δ t u er (extB i3 i11 (R.atomBody rel)) h ∣₁
```

反过来，假定对载荷分解为词项码 `t`、`u` 的每一种方式及每个相伴配对容器，都能证明所需的外延条件。有界全称引入据此重建载荷分解，从而构造原子关系。词项实际取值的存在选择仍位于 `atomBody` 内部，并不是 `atom-in` 的参数。

```agda
  atom-in : (rel : Formula S (18 + m))
          → ((t u s : S) → Rv ≡ pr (fst t) (fst u) → Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel))
          → ⟨ δ ⊨ R.atomRel rel ⟩
  atom-in rel g = bothAll-in i3 (extB i3 i11 (R.atomBody rel)) δ (λ t u s s∈ t∈ u∈ er → g t u s er)
```

## 从子句桥接到语义满足关系

关系读法完毕：每个构造子的子句已被转换为外延事实，每个外延事实也被转换为子句。本章随即转向把这些对象语言关系与元层满足语义相连接的桥。

```agda
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat; Sat-mem; cond )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
import L.Coding.SatisfactionBridge {ℓ} lem as Semantic
open import Cubical.Data.Nat using ( znots; snotz )
```

桥模块以层级的一个集合 `W` 为参数，其成员构成内部语言的常元字母表。可定义性与语义模块在 `W` 处打开，使字母表 `Ab` 上的公式能在 `W` 携带的小模型中解释。

```agda
module Bridge (W : S) where
  open Alphabet W
  private
    module DB = Semantic.DB W
    module Sem = Semantic.SemB W
```

小模型的满足判断被改名为 `⊨ᴮ`，其词项赋值被改名为 `⟦_⟧ᴮ`，使桥接论证能够把二者与本章先前使用的外围层级满足 `⊨` 区分开来。

```agda
    open Sem.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```

公式 `ψ` 在元层环境 `δ` 处的元层意义，是该公式经常元改名后在 `W` 携带的小模型中的满足。这正是各桥要将对象语言表条目与之关联的目标语义。

```agda
    Meaning : ∀ {n} → Formula Ab n → DB.SM ^ n → hProp (ℓ-suc ℓ)
    Meaning ψ δ = δ ⊨ᴮ mapFo DB.ι ψ
```

底层集合 `Wv` 是小模型量词的取值载体。把它与呈现 `W : S` 区分开来，对后续桥接很重要：对象语言的隶属使用集合 `Wv`，而可构造性证据保留在 `W` 的第二分量中。因此，各桥只对固定模型的成员量化，而不是对所有可构造集合量化。

```agda
  private
    Wv = fst W
```

映射 `toS` 把字母表 `Ab` 上公式的每个常元改名为结构 `S` 的相应常元，产出的 `S` 上公式可由环境满足判断。

```agda
  toS : ∀ {n} → Formula Ab n → Formula S n
  toS = mapFo (asConst W)
```

可构造满足集 `SatW ψ` 收集满足改名后公式的编码环境。它是 `L` 的元素，因为它是定义满足的内部递归的输出。

```agda
  SatW : ∀ {n} → Formula Ab n → S
  SatW ψ = Sat W (toS ψ)
```

`SatW ψ` 中隶属的向外读法来自内部满足的隶属规格：`SatW ψ` 的成员是一个编码环境，它属于正确元数的环境集，并满足改名后公式的条件。

```agda
  Sat-out : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩
          → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩
  Sat-out ψ z h = subst ⟨_⟩ (Sat-mem W (toS ψ) z) h
```

向内方向从「属于正确的环境集」与「满足递归条件」这两个事实出发，把它们沿 `Sat-mem` 反向搬运，从而得到属于 `SatW ψ`。因此，`Sat-out` 与 `Sat-in` 恰是隶属规格所给路径的两个搬运方向，不需要额外的语义假设。

```agda
  Sat-in : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩
         → ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩
  Sat-in ψ z hz hc = subst ⟨_⟩ (sym (Sat-mem W (toS ψ) z)) (hz , hc)
```

引理 `extension-path` 把逐点的真值路径转化为关于 `SatW ψ` 的精确外延定理。对每个编码环境 `z`，其前提把递归条件 `cond W (toS ψ)` 与目标命题 `P z` 识别起来。借助 `Sat-mem` 的两个方向，结论说明 `SatW ψ` 的成员恰是 `envSet W n` 中满足 `P` 的成员；这里既不解码 `z`，也不选择环境向量的代表。

```agda
  private
    extension-path : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
                   → ((z : S) → ((z ∷ []) ⊨ cond W (toS ψ)) ≡ P z)
                   → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)
    extension-path ψ P e =
```

向外方向经 `Sat-out` 读取 `SatW ψ` 中隶属的两个分量，并沿逐点等式运输条件。向内方向把性质运回并应用 `Sat-in`。两个方向都只使用逐点等式，不选取任何代表。

```agda
        (λ z hz → Sat-out ψ z hz .fst , subst ⟨_⟩ (e z) (Sat-out ψ z hz .snd))
      , (λ z hz hp → Sat-in ψ z hz (subst ⟨_⟩ (sym (e z)) hp))
```

对假式而言，目标性质对任何 `z` 都没有元素。若 `z` 属于 `SatW ⊥̇`，`Sat-out` 会给出不可能成立的假式满足；反过来，假定有这项不可能的性质，便可立即消去候选。剩余分量只记录每个假想成员都会具有正确元数，因此 `botBridge` 给出 `envSet W n` 内的空外延。

```agda
  botBridge : (n : ℕ) {k : ℕ} (env : S ^ k)
            → ExtFact (fst (SatW (⊥̇ {n = n}))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ ⊥̇ ⟩)
  botBridge n env = (λ z hz → Sat-out ⊥̇ z hz .fst , Sat-out ⊥̇ z hz .snd) , (λ z hz b → Empty.rec* b)
```

假定 `env` 的槽位 `ya` 与 `yb` 分别承载 `a`、`b` 的满足集之底层集合。合取桥于是把 `SatW (a ∧̇ b)` 刻画为同时属于两个子公式满足集的编码环境 `z`。由于求值主体前先把 `z` 加到环境头部，原槽位改由 `suc ya`、`suc yb` 读取，而 `i0` 指向 `z`；这次移位正是所示公式记录的宿主 `Fin` 边界。

```agda
  andBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
            → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
            → ExtFact (fst (SatW (a ∧̇ b))) (fst (envSet W n))
                (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)) ⟩)
  andBridge a b env ya yb qa qb = extension-path (a ∧̇ b)
```

对合取而言，这条逐点路径比较同一个候选环境 `z` 的两种描述。递归条件说 `z` 同时属于 `SatW a` 与 `SatW b`；沿 `qa` 和 `qb` 传输这两份隶属，恰好得到子句主体中的两条对象语言隶属原子。这一步不解码任何子环境。

```agda
    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⊓ (fst z ∈ sym qb i))
```

析取桥接给出一条精确的外延描述。一个环境属于 `SatW (a ∨̇ b)`，当且仅当它属于 `envSet W n`，并且把它放在子句环境首部后，满足对象语言析取：它属于 `a` 的值或属于 `b` 的值。

```agda
  orBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
           → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
           → ExtFact (fst (SatW (a ∨̇ b))) (fst (envSet W n))
               (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)) ⟩)
  orBridge a b env ya yb qa qb = extension-path (a ∨̇ b)
```

析取的逐点比较沿两条槽位等式传输同一个 `z` 的隶属。两种可能分别是 `z` 属于 `SatW a` 与 `z` 属于 `SatW b`；对象语言析取准确记录这一选择，并不产生额外的环境见证。

```agda
    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⊔ (fst z ∈ sym qb i))
```

蕴涵桥接同样在环境集合之内刻画 `SatW (a ⇒̇ b)`。对候选环境 `z`，子句主体说：若 `z` 属于前件的值，则同一个 `z` 属于后件的值。

```agda
  impBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
            → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
            → ExtFact (fst (SatW (a ⇒̇ b))) (fst (envSet W n))
                (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)) ⟩)
  impBridge a b env ya yb qa qb = extension-path (a ⇒̇ b)
```

这里所需的是逐点路径：`qa` 与 `qb` 分别把前件和后件的值槽指认为 `SatW a` 与 `SatW b`。沿这两条等式传输后，对象语言蕴涵就成为蕴涵的递归条件，环境本身没有改变。

```agda
    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⇒ (fst z ∈ sym qb i))
```

两种无界量词主体都先在 `wi` 指名的载体上量化。存在主体要求某个载体成员 `x`，全称主体则处理每个这样的 `x`；两者的内层都有一个有界存在，它从子公式的值中取一个条目，并要求该条目是把 `x` 添加到旧环境前端所得的图。

```agda
  quEx quAll : ∀ {k} → Fin k → Fin k → Formula S (1 + k)
  quEx wi yai = ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
  quAll wi yai = ∀̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
```

引理 `direct-extension` 抽出量词桥接与原子桥接共有的论证。一旦 `z` 被认作某个向量 `δ` 的图，它要求在 `Meaning ψ δ` 与拟议的子句性质 `P z` 之间给出两个方向的映射；由此证明 `SatW ψ` 恰是 `envSet W n` 中满足 `P` 的部分。对 `δ` 的恢复始终留在截断之内。

```agda
  private
    direct-extension : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
      → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning ψ δ ⟩ → ⟨ P z ⟩)
      → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ P z ⟩ → ⟨ Meaning ψ δ ⟩)
      → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)
```

在向外的一半中，`Sat-out` 先给出 `z` 属于环境集合。随后，截断的恢复定理给出向量 `δ` 以及把 `z` 认作其图的等式；在命题 `P z` 内，`Sat-small-spec` 把原来的 `z ∈ SatW ψ` 转成 `Meaning ψ δ`，再由前向假设完成论证。

```agda
    direct-extension {n} ψ P f b = out , inn
      where
      out : (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩ → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ P z ⟩
      out z hz = Sat-out ψ z hz .fst , PT.rec (snd (P z))
        (λ { (δ , q) → f δ z q (subst ⟨_⟩ (Semantic.Sat-small-spec W ψ δ z q) hz) })
```

在向内的一半中，属于环境集合仍只给出截断的 `δ , q`。反向假设把 `P z` 送到 `Meaning ψ δ`，再沿 `Sat-small-spec` 的逆向得到 `z ∈ SatW ψ`。由于目标隶属是命题，这次截断消去是合法的，也没有全局选取解码向量。

```agda
        (Semantic.envSet-vectors W z (Sat-out ψ z hz .fst))
      inn : (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩ → ⟨ P z ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩
      inn z hz hp = PT.rec (snd (fst z ∈ fst (SatW ψ)))
        (λ { (δ , q) → subst ⟨_⟩ (sym (Semantic.Sat-small-spec W ψ δ z q)) (b δ z q hp) })
        (Semantic.envSet-vectors W z hz)
```

引理 `child` 对齐一个约束变元的编码读法与语义读法。若旧编码环境是 `δ` 的图，且被指名的子公式值为 `SatW a`，那么「子公式值的某个成员是把 `x` 添加到旧环境前端所得的图」与 `Meaning a (x ∷ δ)` 命题相等。

```agda
    child : ∀ {n k} (a : Formula Ab (suc n)) (δ : DB.SM ^ n) (x : DB.SM)
      (γ : S ^ k) (zi yai : Fin k) → fst (lookup zi γ) ≡ Semantic.graph W δ
      → fst (lookup yai γ) ≡ fst (SatW a)
      → ((Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)))
        ≡ Meaning a (x ∷ δ)
```

证明是由 `⇔toPath` 连接的一对蕴涵。向外方向消去有界存在的截断见证：子公式值中的一个条目，以及 `consAtL` 给出的证据，说明该条目正是把 `x` 添加到旧环境前端所得的图。

```agda
    child a δ x γ zi yai qz qa = ⇔toPath out inn
      where
      out : ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
          → ⟨ Meaning a (x ∷ δ) ⟩
      out = PT.rec (snd (Meaning a (x ∷ δ))) (λ { (e , he , hc) →
```

在向外方向，有界存在被消去到命题 `Meaning a (x ∷ δ)` 中。序接子句连同旧图的等式，把见证 `e` 认作 `x ∷ δ` 的图；再由 `qa` 把 `e` 的隶属改写为属于 `SatW a`，`Sat-small-spec` 随即给出所需的语义满足。

```agda
        subst ⟨_⟩ (Semantic.Sat-small-spec W a (x ∷ δ) e
          (Semantic.consAtL-out W δ x (e ∷ Semantic.intoL W x ∷ γ) i0 i1 (sh 2 zi) qz refl hc))
          (subst (λ X → ⟨ fst e ∈ X ⟩) qa he) })
      inn : ⟨ Meaning a (x ∷ δ) ⟩
          → ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
```

向内方向构造典范扩展环境 `envFor W (x ∷ δ)`。反向读取 small-spec 路径，把语义满足转成该环境属于 `SatW a` 的证明；随后，`consAtL-in` 证明同一环境与旧环境之间满足所需的图扩展关系。

```agda
      inn h = ∣ Semantic.envFor W (x ∷ δ)
        , subst (λ X → ⟨ fst (Semantic.envFor W (x ∷ δ)) ∈ X ⟩) (sym qa)
          (subst ⟨_⟩ (sym (Semantic.Sat-small-spec W a (x ∷ δ) (Semantic.envFor W (x ∷ δ))
            (Semantic.envFor-graph W (x ∷ δ)))) h)
        , Semantic.consAtL-in W δ x (Semantic.envFor W (x ∷ δ) ∷ Semantic.intoL W x ∷ γ)
```

`consAtL-in` 的余下参数依次给出旧图等式 `qz`、新首项 `x` 的自反同一视，以及扩展向量的 `envFor-graph`。这些数据闭合向内见证，从而完成等价。

```agda
            i0 i1 (sh 2 zi) qz refl (Semantic.envFor-graph W (x ∷ δ)) ∣₁
```

存在桥接是量词的第一个结果：`∃̇ a` 的内部值在环境集上的隶属，与在载体上满足有界存在形状 `quEx` 是同一回事，其中两条槽位等式分别点名载体与子值。

```agda
  exBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : S ^ k) (wi yai : Fin k)
           → fst (lookup wi γ) ≡ Wv → fst (lookup yai γ) ≡ fst (SatW a)
           → ExtFact (fst (SatW (∃̇ a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ γ) ⊨ quEx wi yai ⟩)
  exBridge a γ wi yai qw qa = direct-extension (∃̇ a) (λ z → (z ∷ γ) ⊨ quEx wi yai)
    (λ δ z qz → PT.map (λ { (x , h) → Semantic.intoL W x
```

对存在桥接，`direct-extension` 之后只剩由 `child` 提供的两次转换。从语义满足出发，截断中的模型元素 `x` 被嵌入 `L`，成为外层有界见证；反过来，对象语言中属于被指名载体的见证被视为限制模型的元素，再经 `child` 读取。两次转换都始终处在命题截断之内。

```agda
      , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x)
      , subst ⟨_⟩ (sym (child a δ x (z ∷ γ) i0 (suc yai) qz qa)) h }))
    (λ δ z qz → PT.map (λ { (x , hx , h) → (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
      , subst ⟨_⟩ (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
        (z ∷ γ) i0 (suc yai) qz qa) h }))
```

全称桥接为 `∀̇ a` 陈述同样的外延事实：内部值包含一个环境，当且仅当载体的每个成员添加到该环境之后都满足子公式。

```agda
  allBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : S ^ k) (wi yai : Fin k)
            → fst (lookup wi γ) ≡ Wv → fst (lookup yai γ) ≡ fst (SatW a)
            → ExtFact (fst (SatW (∀̇ a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ γ) ⊨ quAll wi yai ⟩)
  allBridge a γ wi yai qw qa = direct-extension (∀̇ a) (λ z → (z ∷ γ) ⊨ quAll wi yai)
    (λ δ z qz h x hx → subst ⟨_⟩
```

在 `direct-extension` 所需的前向映射中，先把被指名载体的任意对象层成员变成限制模型的元素，对它施用语义全称假设，再从语义满足向编码扩展子句反向读取 `child`。在反向映射中，先把限制模型元素嵌入载体，施用编码全称，再向外读取 `child` 以恢复语义满足。

```agda
      (sym (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (z ∷ γ) i0 (suc yai) qz qa))
      (h (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)))
    (λ δ z qz h x → subst ⟨_⟩ (child a δ x (z ∷ γ) i0 (suc yai) qz qa)
      (h (Semantic.intoL W x) (subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x))))
```

有界量词的对象语言形状有三层嵌套的有界量化：界项的取值、其内落在载体中的成员、以及扩展条目，两个量词的次序相同。

```agda
  bqAll bqEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (1 + k)
  bqAll wi ti yai N0i N1i =
    ∀̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))
      ⇒̇ ∀̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ⇒̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
  bqEx wi ti yai N0i N1i =
```

存在形式把三层合取；全称形式以蕴涵嵌套它们。界项的取值由其自身的词项子句读取，而最内层子句使用与无界情形相同的图扩展等式。

```agda
    ∃̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))
      ∧̇ ∃̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ∧̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
```

词项的语义值这样得到：先把字母表中来自 `W` 的每个常元映入限制模型，再在 `δ` 处求值。常元由嵌入 `DB.ι` 解释，变元则直接从 `δ` 的相应位置读取；集合编码的数码用于随后表示变元索引，并不属于这里的求值函数。

```agda
  private
    value : ∀ {n} → Term Ab n → DB.SM ^ n → DB.SM
    value t δ = ⟦ mapTm DB.ι t ⟧ᴮ δ
```

对常元词项，`term-out` 把截断的 `TmIsV` 证据消去到集合等式中。在常元分支，对编码的单射性比较第二分量，从而把候选值认作该常元；变元形状的分支会迫使不同标签 `# 0` 与 `# 1` 相等，因而不可能。

```agda
    term-out : ∀ {n} (t : Term Ab n) (δ : DB.SM ^ n) (z v : S)
      → fst z ≡ Semantic.graph W δ → TmIsV (ct t) (fst z) (fst v)
      → fst v ≡ fst (value t δ)
    term-out (con q) δ z v qz = PT.rec (setIsSet _ _)
      (λ { (inl e) → sym (pr-inj e .snd)
```

对变元词项，常元形状的分支同样由标签互异而排除。在变元形状的分支，对编码的单射性把所存索引认作 `i` 的数码；等式 `qz` 把相应隶属移入典范图，`lookup-spec` 随即说明候选值恰是 `δ` 的第 `i` 个条目。截断只被消去到这条命题性等式中。

```agda
         ; (inr (i , e , _)) → Empty.rec (znots (#-inj′ {0} {1} (pr-inj e .fst))) })
    term-out (var i) δ z v qz = PT.rec (setIsSet _ _)
      (λ { (inl e) → Empty.rec (snotz (#-inj′ {1} {0} (pr-inj e .fst)))
         ; (inr (j , e , hp)) → subst ⟨_⟩ (lookup-spec (Semantic.values W δ) i (fst v))
             (subst2 (λ a E → ⟨ pr a (fst v) ∈ E ⟩) (sym (pr-inj e .snd)) qz hp) })
```

反向引理从真实语义值重建 `TmIsV`。对常元，把给定等式反向，并通过标签为 `# 0` 的对构造传输，就得到命题截断中的常元形状分支。

```agda
    term-in : ∀ {n} (t : Term Ab n) (δ : DB.SM ^ n) (z v : S)
      → fst z ≡ Semantic.graph W δ → fst v ≡ fst (value t δ)
      → TmIsV (ct t) (fst z) (fst v)
    term-in (con q) δ z v qz e = ∣ inl (cong (pr (# 0)) (sym e)) ∣₁
    term-in (var i) δ z v qz e = ∣ inr (# (toℕ i) , refl
```

对变元，见证以数码 `# (toℕ i)` 作为所存索引。给定等式把候选值认作第 `i` 个语义条目；`lookup-spec` 将这条等式转成相应的配对属于典范图的证明，再沿 `qz` 反向传输，把该配对放回给定的编码环境中。

```agda
      , subst (λ E → ⟨ pr (# (toℕ i)) (fst v) ∈ E ⟩) (sym qz)
          (subst ⟨_⟩ (sym (lookup-spec (Semantic.values W δ) i (fst v))) e)) ∣₁
```

有界量词模块固定界限词项、子公式、五个槽位与五条等式：载体、词项的编码、子公式的值，以及两个数码槽位，全部在同一语境上读取。

```agda
  module BqBridge {n : ℕ} (t : Term Ab n) (a : Formula Ab (suc n)) {k : ℕ} (Γ : S ^ k)
    (wi ti yai N0i N1i : Fin k)
    (qw : fst (lookup wi Γ) ≡ Wv) (qt : fst (lookup ti Γ) ≡ ct t) (qa : fst (lookup yai Γ) ≡ fst (SatW a))
    (q0 : fst (lookup N0i Γ) ≡ # 0) (q1 : fst (lookup N1i Γ) ≡ # 1) where
```

余下的证明要把有界量词所用的对象语言词项子句，与刚刚确立的语义词项值连接起来。以下局部引理把这条联系固定在 `BqBridge` 的槽位与等式上，使后续每个量词论证都使用同一个载体、词项码、子公式值和数码标签。

```agda
    private
```

若对象语言词项子句在 `v ∷ z ∷ Γ` 处成立，`tmIs-out` 先把它读成关于词项槽中代码的 `TmIsV`。再沿 `qt` 传输，把该槽值替换为真实代码 `ct t`，得到 `term-out` 所需的表示层陈述。

```agda
      tmOut : (z v : S) → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩
            → TmIsV (ct t) (fst z) (fst v)
      tmOut z v h = subst (λ u → TmIsV u (fst z) (fst v)) qt
        (tmIs-out (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1 h)
```

反过来，关于 `ct t` 的 `TmIsV` 陈述沿 `qt` 反向传输，再交给 `tmIs-in`。所得正是在 `v ∷ z ∷ Γ` 处的对象语言词项子句，因此桥接可在编码子句与语义词项求值之间双向移动。

```agda
      tmIn' : (z v : S) → TmIsV (ct t) (fst z) (fst v)
            → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩
      tmIn' z v h = tmIs-in (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1
        (subst (λ u → TmIsV u (fst z) (fst v)) (sym qt) h)
```

对语义环境 `δ`，`bound δ` 是界项取值重新嵌入 `L` 后所得的集合。它充当编码有界量词最外层取值槽的典范见证，而有界公式所量化的对象正是它的成员。

```agda
      bound : DB.SM ^ n → S
      bound δ = Semantic.intoL W (value t δ)
```

界属于载体：取值的第二分量是它在载体中的隶属，沿载体的命名等式传输。

```agda
      bound∈W : (δ : DB.SM ^ n) → ⟨ fst (bound δ) ∈ fst (lookup wi Γ) ⟩
      bound∈W δ = subst (λ X → ⟨ fst (value t δ) ∈ X ⟩)
        (sym qw) (snd (value t δ))
```

当 `z` 是 `δ` 的图时，`bound δ` 的底层集合按定义就是 `t` 的语义值之底层集合，因此自反性给出 `term-in` 所需的等式。所得 `TmIsV (ct t) (fst z) (fst (bound δ))` 认证所选的界表示编码词项在该编码环境处的取值。

```agda
      bound-term : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ
                 → TmIsV (ct t) (fst z) (fst (bound δ))
      bound-term δ z qz = term-in t δ z (bound δ) qz refl
```

随后，`bound-term` 给出的表示层证书由 `tmIn'` 转成对象语言的 `tmIs` 公式，并落在有界量词主体所用的精确移位槽位上。于是，典范语义界可以填入该主体的最外层量化。

```agda
      bound-read : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ
                 → ⟨ (bound δ ∷ z ∷ Γ)
                     ⊨ tmIs (suc (suc ti)) i1 i0
                         (suc (suc N0i)) (suc (suc N1i)) ⟩
      bound-read δ z qz = tmIn' z (bound δ) (bound-term δ z qz)
```

在有界全称桥接的前向一半中，任取满足词项子句的候选值 `v`，再任取既属于载体又属于 `v` 的成员 `x`。引理 `term-out` 把 `v` 的底层集合认同为 `t` 的真实语义值之底层集合，因此 `x` 的隶属可传输到语义界中。语义全称假设给出子公式的真值，再由 `child` 把它转回编码扩展子句。

```agda
    allInBridge : ExtFact (fst (SatW (∀̇∈ t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i ⟩)
    allInBridge = direct-extension (∀̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i)
      (λ δ z qz h v hv ht x hx hxv → subst ⟨_⟩
        (sym (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
          (v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa))
```

在反向一半中，要证明语义界内任意限制模型元素 `x` 满足子公式。把编码全称实例化于典范值 `bound δ`，所需条件由 `bound∈W` 与 `bound-read` 提供；再实例化于嵌入后的元素 `intoL W x`，使用它的载体隶属与假定的界内隶属。最后向外读取 `child`，得到 `Meaning a (x ∷ δ)`。

```agda
        (h (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
          (subst (λ V → ⟨ fst x ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv)))
      (λ δ z qz h x hx → subst ⟨_⟩
        (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)
        (h (bound δ) (bound∈W δ) (bound-read δ z qz)
```

最后一个参数恰是假设 `x` 属于界项的语义值。供给这份隶属后，便为每个这样的 `x` 完成全称验证者，也就完成了 `direct-extension` 所需的反向蕴涵。

```agda
          (Semantic.intoL W x) (subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x)) hx))
```

有界存在桥接为 `∃̇∈ t a` 陈述同样的外延事实：在环境集合内，属于内部值等价于满足载体上的三层有界存在公式。

```agda
    exInBridge : ExtFact (fst (SatW (∃̇∈ t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i ⟩)
    exInBridge = direct-extension (∃̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i)
      (λ δ z qz → PT.map (λ { (x , hx , h) → bound δ
        , bound∈W δ
        , bound-read δ z qz
```

从有界存在的语义见证 `x` 出发，前向映射选取典范外层值 `bound δ`，供给其载体隶属与词项证书，并把 `x` 嵌入为内层载体见证。`x` 属于语义界的证据得到保留，而反向读取 `child` 产生所需的编码扩展见证。所有存在见证始终留在命题截断之内。

```agda
        , ∣ Semantic.intoL W x , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x) , hx
            , subst ⟨_⟩ (sym (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)) h ∣₁ }))
      (λ δ z qz → PT.rec squash₁ (λ { (v , hv , ht , h) → PT.map
        (λ { (x , hx , hxv , hc) → (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
          , subst (λ V → ⟨ fst x ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv
```

在反向映射中，外层截断见证给出候选词项值 `v`，内层见证给出既属于载体又属于 `v` 的成员 `x`，以及编码的子公式扩展。向外读取词项子句，把 `v` 的底层集合认同为真实语义界的底层集合；沿该等式把 `x` 的隶属传输到真实界，再由 `child` 把编码的子公式证据转成语义满足。

```agda
          , subst ⟨_⟩ (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
              (v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa) hc }) h }))
```

原子主体只绑定两个值，而不是三个：载体元素 `v` 作为 `t` 的候选值，载体元素 `x` 作为 `u` 的候选值。随后，它把两条 `tmIs` 子句与给定关系公式 `rel` 合取，并在语境 `x ∷ v ∷ z ∷ Γ` 中求值；编码环境 `z` 原本就是自由参数，`rel` 是公式而非被绑定的条目。

```agda
  atomEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (3 + k) → Formula S (1 + k)
  atomEx wi ti ui N0i N1i rel =
    ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc wi)))
      (tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i)
        ∧̇ (tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ∧̇ rel)))
```

`AtomBridge` 抽出隶属原子与相等原子共有的证明。词项 `t`、`u` 及五条槽位等式决定如何读取它们的代码与标签 `# 0`、`# 1`；参数 `op`、`R`、`rel` 则分别指定元层原子、对应的外围二元关系，以及表示该关系的对象语言公式。

```agda
  module AtomBridge {n : ℕ} (t u : Term Ab n) {k : ℕ} (Γ : S ^ k)
    (wi ti ui N0i N1i : Fin k)
    (qw : fst (lookup wi Γ) ≡ Wv) (qt : fst (lookup ti Γ) ≡ ct t) (qu : fst (lookup ui Γ) ≡ ct u)
    (q0 : fst (lookup N0i Γ) ≡ # 0) (q1 : fst (lookup N1i Γ) ≡ # 1)
    (op : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j)
```

相符假设给出 `rel` 与 `R` 在新加入的三个条目处的精确接口。在 `x ∷ v ∷ z ∷ Γ` 中满足 `rel` 会得到 `R (fst v) (fst x)`，而该关系的一份证明又能重建 `rel` 的满足。因此，只有在两个方向均已给出时，桥接才可使用任意表示公式。

```agda
    (R : V ℓ → V ℓ → Type (ℓ-suc ℓ))
    (rel : Formula S (3 + k))
    (agree : (z v x : S) → (⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩ → R (fst v) (fst x))
                           × (R (fst v) (fst x) → ⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩))
    (cnd-out : (δ : DB.SM ^ n) → ⟨ Meaning (op t u) δ ⟩ → R (fst (value t δ)) (fst (value u δ)))
```

另外两条假设把所选关系连接到目标原子语义。第一条把 `Meaning (op t u) δ` 送到两个词项求值之间的 `R`，第二条则从同一关系重建该语义。正因如此，这条一般桥接可同时适用于隶属与相等。

```agda
    (cnd-in : (δ : DB.SM ^ n) → R (fst (value t δ)) (fst (value u δ)) → ⟨ Meaning (op t u) δ ⟩) where
```

语境 `δ3 z v x = x ∷ v ∷ z ∷ Γ` 把 `u` 的候选值放在槽位 `i0`，把 `t` 的候选值放在 `i1`，并把编码环境放在 `i2`。它们是两条词项子句与关系接口使用的三个新条目；一般公式 `rel` 仍可使用从 `Γ` 继承的条目。`atomEx` 只新绑定 `x` 与 `v`，而 `z` 原本就是自由的环境参数。

```agda
    private
      δ3 : (z v x : S) → S ^ (3 + k)
      δ3 z v x = x ∷ v ∷ z ∷ Γ
```

两条向外读式把 `δ3 z v x` 中的对象语言词项子句转成 `TmIsV` 陈述。沿 `qt` 传输后，第一条陈述涉及真实代码 `ct t` 与候选值 `v`；沿 `qu` 传输后，第二条同样涉及 `ct u` 与候选值 `x`。两者共享的编码环境始终是 `z`。

```agda
      tOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct t) (fst z) (fst v)
      tOut z v x h = subst (λ w → TmIsV w (fst z) (fst v)) qt
        (tmIs-out (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h)
      uOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct u) (fst z) (fst x)
      uOut z v x h = subst (λ w → TmIsV w (fst z) (fst x)) qu
```

反向读式从 `TmIsV` 重建两条对象语言词项子句。对 `t`，先沿 `qt` 反向传输代码，再把结果交给 `tmIs-in`；`uIn` 的声明则为 `u` 在自身取值槽处安排同样的构造。

```agda
        (tmIs-out (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h)
      tIn : (z v x : S) → TmIsV (ct t) (fst z) (fst v) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩
      tIn z v x h = tmIs-in (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1
        (subst (λ w → TmIsV w (fst z) (fst v)) (sym qt) h)
      uIn : (z v x : S) → TmIsV (ct u) (fst z) (fst x) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩
```

对 `u`，沿 `qu` 反向传输，把 `TmIsV (ct u) (fst z) (fst x)` 改写成关于调用者槽位所指代码的陈述，再由 `tmIs-in` 重建第二条对象语言词项子句。至此，桥接对两个候选词项值都具备读取与写入两个方向。

```agda
      uIn z v x h = tmIs-in (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1
        (subst (λ w → TmIsV w (fst z) (fst x)) (sym qu) h)
```

定理 `atomBridge` 现在让 `direct-extension` 在每个编码环境上比较原子的语义值与 `atomEx`。其前向映射必须从 `Meaning (op t u) δ` 出发，构造两个有界取值见证、相应词项子句，以及 `x ∷ v ∷ z ∷ Γ` 中的关系公式；反向映射则沿同一批数据返回。

```agda
    atomBridge : ExtFact (fst (SatW (op t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩)
    atomBridge = direct-extension (op t u) (λ z → (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel) out inn
      where
      out : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning (op t u) δ ⟩
          → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩
```

前向构造选取 `t` 与 `u` 的真实语义值嵌入 `L` 后的结果，作为两个有界见证。限制模型取值的第二分量证明它们属于载体；`term-in` 再接 `tIn` 与 `uIn`，给出两条词项子句；`cnd-out` 再接 `agree` 的反向一半，给出对象语言关系。两层见证分别被引入到两层命题截断之中。

```agda
      out δ z qz h = ∣ v , subst (λ X → ⟨ fst v ∈ X ⟩) (sym qw) (snd (value t δ))
        , ∣ x , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd (value u δ))
          , tIn z v x (term-in t δ z v qz refl)
          , uIn z v x (term-in u δ z x qz refl)
          , agree z v x .snd (cnd-out δ h) ∣₁ ∣₁
```

局部名称 `v` 与 `x` 分别是词项 `t`、`u` 的求值嵌入 `L` 后所得的元素。它们是 `atomEx` 两个取值量词的典范见证；原子码本身指名的是两个词项码，而这里的见证给出它们在特定环境 `δ` 处的取值。

```agda
        where
        v x : S
        v = Semantic.intoL W (value t δ)
        x = Semantic.intoL W (value u δ)
```

`atomBridge` 的反向蕴含从元层环境 `δ`、编码环境 `z` 以及 `z` 与 `δ` 的典范图之间的同一视出发。余下的假设断言 `atomEx` 在 `z` 处成立。外层命题截断的有界存在式给出候选值 `v`、它属于 `W` 的证明 `hv`，以及内层存在式的证明 `h`。由于 `Meaning (op t u) δ` 是命题，`PT.rec` 可以把这层命题截断消去到该目标中，随后也可如此消去内层命题截断。此时 `v` 还只是 `t` 的候选值；从内层见证取得的词项取值记录才会把它认同为真正的语义值。

```agda
      inn : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ
          → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩ → ⟨ Meaning (op t u) δ ⟩
      inn δ z qz = PT.rec (snd (Meaning (op t u) δ)) (λ { (v , hv , h) →
        PT.rec (snd (Meaning (op t u) δ)) (λ { (x , hx , ht , hu , hr) →
          cnd-in δ (subst2 R (term-out t δ z v qz (tOut z v x ht))
```

内层见证给出第二个候选值 `x`、其成员证明 `hx : x ∈ W`、两条词项子句的证明 `ht` 与 `hu`，以及对象语言关系的证明 `hr`。`hv` 与 `hx` 记录两个存在量词的界，但这里无需再使用它们。首先，`agree z v x .fst` 把 `hr` 读成 `R (fst v) (fst x)`。由于 `z` 是 `δ` 的典范图，`tOut` 与 `uOut` 把两条词项子句证明交给 `term-out`；所得等式分别把 `v`、`x` 的底层集合认同为 `t`、`u` 的语义值之底层集合。随后，`subst2` 沿这两条同一视搬运 `R`，最后 `cnd-in` 把搬运后的关系化为 `Meaning (op t u) δ`。原子桥至此完成。下游分别为隶属关系与相等关系实例化该桥。在 `SatSoundC` 中，对子码封闭与公式结构递归通过比较外延事实，把表项固定为 `SatW`；在 `SatHoldsC` 中，码的解码、给定的表值、全定义性与指定定义域使同一组桥能够填入全部十条子句。`SatisfactionDescription` 提供码域与环境塔的事实，证明典范图 `SatGraph.pairs W` 满足 `tableAt`，并把 `towerAt`、`codesAt` 与 `tableAt` 封装为 `satAt`。其中的 `SatRead` 模块为所得满足图、码集与环境塔给出双向隶属读式。

```agda
            (term-out u δ z x qz (uOut z v x hu)) (agree z v x .fst hr)) }) h })
```

## 回顾

各条子句的内部语义至此与通常的满足关系双向对应。环境图解释变元，递归桥接处理逻辑构造子，原子桥接则沿词项取值搬运隶属关系与相等关系。证明只使用编码表所陈述的存在事实与外延事实，并未假定任意表关系本身已经是函数。