规格 tableAt 把两个定义域条件 total、onC 与十条构造子子句合在一起。一条构造子子句如何成为语义递归的一步？本章先把每条子句读成候选值集合的精确外延条件，再证明递归构造的集合 SatW 满足同一条件。当外围论证另外给出匹配的码、子值与表条目后，外延性便可把两个值同一视。这些局部桥接本身并不证明整张表单值或唯一确定。

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

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

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

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

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

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

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 的赋值图。

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 ∷ δ 的图与 δ 的图联系起来，这正是处理量词所需的语义步骤。

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 只管理第三种索引：约束子在向量前端加入一个值时，所有旧槽位都要越过这个新槽位。

  ( 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 上的外延。

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 )

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

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 )

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

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-集合结构保证这些恢复出的等式都是命题值。

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

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

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

读取共同框架

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

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 ⟩)

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

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

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

  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'。

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' 的底层集合相等；被同一视的是底层集合，而不是任何选定的编码证据。

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

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

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

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

    Av = fst (lookup a δ)

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

  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) 转成内部蕴涵所需的前件。余下的正是四槽扩展环境处的主体。

    useBoth i0 (down TS (pr (fst c₁) (fst ya)) m ∷ δ) c₁ ya refl (prAtL i1 (sh  ar) (sh  a) ⇒̇ body)
      (h (down TS (pr (fst c₁) (fst ya)) m) m)
      (pr-in i1 (sh  ar) (sh  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 唯一；它是对所有匹配条目量化。

  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  ar) (sh  a) ⇒̇ body) (e' ∷ δ)
    (λ c₁ ya s s∈ c₁∈ ya∈ e hp → g c₁ ya s e' e'∈ e (pr-out i1 (sh  ar) (sh  a) (ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp))

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

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

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

    Av = fst (lookup a δ)

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

  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。主体可用之前所需的守卫恰好就是这两个等式。

  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  i1) i0 (sh  (sh  a)) δ6 e))
      (suc-in (sh  ar) i0 δ6 es)

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

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

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

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

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

  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  a) (sucAtL (sh  ar) i0 ⇒̇ body)) (e' ∷ δ)

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

    (λ 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  i1) i0 (sh  (sh  a)) (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp)
        (suc-out (sh  ar) i0 (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hs))

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

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

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

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

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

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

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

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

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

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

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

    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 的变元分支。

    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  v) (q ∷ i ∷ s ∷ δ) hp) q∈ )) })

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

    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 转成图隶属分支。

    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。

  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 的嵌套有界存在。

  private
    build : (Tv ≡ pr (# ) Vv) ⊎ (Σ[ i ∈ V ℓ ] ((Tv ≡ pr (# ) 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 内的见证，并非新的语义索引或语义值。

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

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

      e' : Tv ≡ pr N1v (fst iS)
      e' = e ∙ cong (λ a → pr a i) (sym q1)
      δ3 : S ^ ( + 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 的配对。这恰好给出变元分支所需的图条目。

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

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

  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)。

module Frame {m : ℕ} (T w C E : Fin m) (N : Fin  → 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) 必须成立之处。这是对所有匹配条目的全称条件，并非寻找某个值的存在式。

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

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

    inner7 k = sndAll i0 (sh  (N k)) (inner9 k)
    inner4 : Fin  → Formula S ( + m)
    inner4 k = ∀̇∈ (var (sh  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，也不证明表值唯一。

  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 )
            (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)。二者只充当代表，使组装十二槽环境时能够应用有界配对读式。

    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。因此，逐层扩展的环境既保留数学数据，也保留对象语言子句取得这些数据时所用的有界见证。

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

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

    δ9 = r ∷ container p (lookup (N k) γ) r ep .fst ∷ δ7
    δ12 : S ^ ( + 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) 的隶属；实际表成员及其容纳集合都在局部构造。

  clause-out : (k : Fin ) → ⟨ γ ⊨ 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，正是为了表明结论来自对同一条外层子句的逐次特化，而不是另行假定构造子关系。

  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)，由此抵达构造子关系。

    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  (N k)) refl h7

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

  clause-in : (k : Fin )
            → ((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 变量保留公式所需的配对分解见证。

            → ⟨ γ ⊨ 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  (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 条子句与其关系之间的两个方向。

          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。

  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。两层分解都由命题截断隐藏，因此结论只给出存在性，并不选取典范取值。

    (h c c∈)

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

  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。因此，表的每个成员都以给定定义域中的代码为第一分量；这个结论既不典范地选定分解，也不说明一个代码只有一个取值。

  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  C)) (e ∷ γ) (h e e∈))

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

  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  C))))
    (λ { (c , yc , (ee , c∈)) → fillBoth i0 (e ∷ γ) c yc ee (var i1 ∈̇ var (sh  C)) c∈ })
    (g e e∈)

读取构造子关系

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

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

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

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

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

  Ext : ∀ {k} (env : S ^ k) (φ : Formula S ( + 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 的隶属判断。

  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 的精确外延。这个结论并不说明表为任一子公式键唯一选定了取值。

              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  T) i16 i4 (extB i11 i19 (R.binBody op)) δ19
        (subAt-out (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op))) δ15

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

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

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

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

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

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

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

  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 子句，各自引入其码、取值与对等式。

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

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

          subAt-in (sh  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 本身。

  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 结合，再揭示最内层的外延事实。

    , subSucAt-out (sh  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  T) δ) (pr (fst c₁) (fst ya)) mem

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

  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 恰好所需的前提与结论；应用一次便能重建整个关系，同时保留对所有匹配表条目的全称读取。

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

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

  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 的元数吻合。

             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  T) i12 i0 (extB i9 i17 (R.bqBody q c)) δ15
        (useBoth i3 δ t a er (subSucAt (sh  T) i12 i0 (extB i9 i17 (R.bqBody q c))) h)

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

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

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

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

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

  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 联系起来。

           → 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  T) i12 i0 (extB i9 i17 (R.bqBody q c))) δ
    (λ t a s s∈ t∈ a∈ er →
      subSucAt-in (sh  T) i12 i0 (extB i9 i17 (R.bqBody q c)) (a ∷ t ∷ s ∷ δ)

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

        (λ 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 验证它们，再应用选定的原子关系。

  atom-out : (rel : Formula S ( + 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 的参数。

  atom-in : (rel : Formula S ( + 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)

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

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

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 携带的小模型中解释。

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

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

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

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

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

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

  private
    Wv = fst W

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

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

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

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

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

  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 恰是隶属规格所给路径的两个搬运方向，不需要额外的语义假设。

  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，也不选择环境向量的代表。

  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。两个方向都只使用逐点等式，不选取任何代表。

        (λ 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 内的空外延。

  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 边界。

  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 传输这两份隶属，恰好得到子句主体中的两条对象语言隶属原子。这一步不解码任何子环境。

    (λ 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 的值。

  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；对象语言析取准确记录这一选择，并不产生额外的环境见证。

    (λ 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 属于后件的值。

  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。沿这两条等式传输后，对象语言蕴涵就成为蕴涵的递归条件，环境本身没有改变。

    (λ 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 添加到旧环境前端所得的图。

  quEx quAll : ∀ {k} → Fin k → Fin k → Formula S ( + 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 的部分。对 δ 的恢复始终留在截断之内。

  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 ⟩)