可定义幂集的 Δ₀ 描述

module _ {j : ℕ} (e N0 z : Fin j) (δ : Vec S j) (q0 : (lookup N0 δ) .fst ≡ # ) where

private
  E = (lookup e δ) .fst
  Z = (lookup z δ) .fst

读取单点子句得到「编码集合等于值的标准单点环境」。正向：编码集合的每个元素都是「数码零与值」的有序对，经配对原子的充分性搬运。

singleOf-out : ⟨ δ ⊨ singleOf e N0 z ⟩ → E ≡ envOne Z
singleOf-out (hall , hex) = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
  where
  fwd : (y : V ℓ) → ⟨ y ∈ E ⟩ → ⟨ y ∈ envOne Z ⟩
  fwd y hy = ∣ lift zero , sym (pr-out i0 (sh  N0) (sh  z) (down (lookup e δ) y hy ∷ δ) (hall (down (lookup e δ) y hy) hy)

证明反向包含时，从标准单条目环境的一个元素出发。存在合取支给出编码集合的某个元素；它的配对等式与已知的零标签一起，把这个元素认同为起初给定的元素。沿此等式搬运成员关系证明，便得到原元素属于编码集合。

                               ∙ cong (λ a → pr a Z) q0) ∣₁
  bwd : (y : V ℓ) → ⟨ y ∈ envOne Z ⟩ → ⟨ y ∈ E ⟩
  bwd y = rec₁ ((y ∈ E) .snd)
    (λ { (lift zero , qy) → rec₁ ((y ∈ E) .snd)
      (λ { (y' , (y'∈ , hy')) →

envOne Z 的元素是有序对 pr (# 0) Z。因此，把标签槽改写为数码零后，这个元素便与 singleOf 所要求的有序对认同；它并不与 Z 本身认同。

        subst (λ u → ⟨ u ∈ E ⟩)
          (pr-out i0 (sh  N0) (sh  z) (y' ∷ δ) hy' ∙ cong (λ a → pr a Z) q0 ∙ qy) y'∈ })
      hex
       ; (lift (suc ()) , _) })

反过来，假设编码集合等于标准单条目环境。该环境唯一的索引是零，所以每个元素都具有所需的有序对形式；其余后继索引情形由不可能性排除。典范的零号条目提供有界存在见证，沿所给等式搬运则提供它的成员关系证明。

singleOf-in : E ≡ envOne Z → ⟨ δ ⊨ singleOf e N0 z ⟩
singleOf-in q =
    (λ y hy → pr-in i0 (sh  N0) (sh  z) (y ∷ δ)
       (rec₁ (setIsSet (y .fst) (pr ((lookup N0 δ) .fst) Z))
         (λ { (lift zero , qy) → sym qy ∙ cong (λ a → pr a Z) (sym q0) ; (lift (suc ()) , _) })

该元素被命名，其成员关系被搬运，而存在见证把零数码与值配对，并逆着标签等式搬运。

         (subst (λ u → ⟨ y .fst ∈ u ⟩) q hy)))
  , ∣ yS , ( subst (λ u → ⟨ pr (# ) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁
           , pr-in i0 (sh  N0) (sh  z) (yS ∷ δ) (cong (λ a → pr a Z) (sym q0)) ) ∣₁
  where
  yS : S

被命名的元素是「零数码与值的对」在编码集合内的呈现。

  yS = down (lookup e δ) (pr (# ) Z) (subst (λ u → ⟨ pr (# ) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁)

module _ {j : ℕ} (x w y N0 : Fin j) (δ : Vec S j) (q0 : (lookup N0 δ) .fst ≡ # ) where

private
  X = (lookup x δ) .fst
  Wv = (lookup w δ) .fst
  Y = (lookup y δ) .fst

由于 Y 是可构造集合，单条目环境属于 Y 的任何证明都能转换为该环境的一个载体表示。正是这个呈现使 definesB 中的有界存在量词能够在 Y 的实际元素上取值。

  YS = lookup y δ

读取单点子句的存在量化，将其转换为标准单点环境在值中的成员关系：见证是值的元素，而单点子句把编码条目认同为该索引的标准环境。

  one-out : (z : S) → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh  y)) (singleOf i0 (sh  N0) i1) ⟩ → ⟨ envOne (z .fst) ∈ Y ⟩
  one-out z = rec₁ ((envOne (z .fst) ∈ Y) .snd)
    (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Y ⟩) (singleOf-out i0 (sh  N0) i1 (e ∷ z ∷ δ) q0 he) e∈ })

填充存在量化是反向：标准单点环境在值内被呈现，而单点子句在延拓环境处填充。

  one-in : (z : S) → ⟨ envOne (z .fst) ∈ Y ⟩ → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh  y)) (singleOf i0 (sh  N0) i1) ⟩
  one-in z h = ∣ down YS (envOne (z .fst)) h , (h , singleOf-in i0 (sh  N0) i1 (down YS (envOne (z .fst)) h ∷ z ∷ δ) q0 refl) ∣₁

读取可定义子集子句便得到切割关系的两个方向。第一个合取支对 X 的每个元素给出它属于 Wv，以及其单条目环境属于 Y；第二个合取支把这两个事实转换回该元素属于 X。

definesB-out : ⟨ δ ⊨ definesB x w y N0 ⟩ → Cuts X Wv Y
definesB-out (h1 , h2) = (λ z hz → h1 z hz .fst , one-out z (h1 z hz .snd)) , (λ z hw he → h2 z hw (one-in z he))

反过来，Cuts X Wv Y 的两个逐点方向填充对象语言中可定义子集子句的两个合取支。上面的私有转换恰在「有界的单条目见证」与「标准单条目环境属于 Y」之间往返。

definesB-in : Cuts X Wv Y → ⟨ δ ⊨ definesB x w y N0 ⟩
definesB-in (o , i) = (λ z hz → o z hz .fst , one-in z (o z hz .snd)) , (λ z hw he → i z hw (one-out z he))

module Read {m : ℕ} (v w T C : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (tg : Tags γ N) where

private
  Vv = (lookup v γ) .fst
  Wv = (lookup w γ) .fst
  Tv = (lookup T γ) .fst

码域的底层集与标签一背后的数码被命名，因为成员关系子句选取的码形如「标签一与第二分量」之对。

  Cv = (lookup C γ) .fst
  N1v = (lookup (N f1) γ) .fst

读取成员关系子句对拟议值的每个元素给出截断记录：码域中的一个码 (拆为标签一与某分量之对)、把该码与某值配对的表条目，以及该元素与该值之间的切割关系。记录在截断下存在；不选定任何码或值。

mem-out : ⟨ γ ⊨ memAt v w T C N ⟩ → (x : S) → ⟨ x .fst ∈ Vv ⟩
        → ∥ Σ[ c ∶ S ] Σ[ p ∶ S ] Σ[ y ∶ S ]
            (⟨ c .fst ∈ Cv ⟩ × ((c .fst ≡ pr (# ) (p .fst)) × (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × Cuts (x .fst) Wv (y .fst)))) ∥₁
mem-out h x x∈ = rec₁ squash₁
  (λ { (c , (c∈ , hc)) → rec₁ squash₁

读取成员关系子句时，先取得候选码域中具有键形状的元素 c，再取得把 c 与值 y 配对的表条目。配对规格把编码的第二分量转成结果中所示的语义等式，而标签等式把形式标签改写为真正的数码一。

    (λ { (p , s , (ec , he)) → rec₁ squash₁
      (λ { (e , (e∈ , hy)) → map₁
        (λ { (y , s' , (ee , hd)) →
          c , p , y , ( c∈ , ( ec ∙ cong (λ a → pr a (p .fst)) (tg f1)
                      , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈

最内层存在经 definesB-out 读取，产出该元素与表条目之值 y 之间的切割关系。

                        , definesB-out i6 (sh  w) i0 (sh  (N f0)) (y ∷ s' ∷ e ∷ p ∷ s ∷ c ∷ x ∷ γ) (tg f0) hd ) ) ) })
        (sndEx-out i0 i3 (definesB i6 (sh  w) i0 (sh  (N f0))) (e ∷ p ∷ s ∷ c ∷ x ∷ γ) hy) })
      he })
    (sndEx-out i0 (sh  (N f1)) (∃̇∈ (var (sh  T)) (sndEx i0 i3 (definesB i6 (sh  w) i0 (sh  (N f0))))) (c ∷ x ∷ γ) hc) })
  (h x x∈)

填充成员关系子句是反向构造：它收取为每个元素产出截断记录的函数，并组装子句的满足。

mem-in : ((x : S) → ⟨ x .fst ∈ Vv ⟩
          → ∥ Σ[ c ∶ S ] Σ[ p ∶ S ] Σ[ y ∶ S ]
              (⟨ c .fst ∈ Cv ⟩ × ((c .fst ≡ pr (# ) (p .fst)) × (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × Cuts (x .fst) Wv (y .fst)))) ∥₁)
       → ⟨ γ ⊨ memAt v w T C N ⟩
mem-in g x x∈ = map₁

反过来，设候选输出的每个元素都带有这样一个截断的语义记录。等式 c = pr (# 1) p 给出有界公式所需的元数一形状，而 pr(c,y) 属于表的证明为表条目提供一个有界表示。

  (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) →
    let ec' : c .fst ≡ pr N1v (p .fst)
        ec' = ec ∙ cong (λ a → pr a (p .fst)) (sym (tg f1))
        δ4 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ x ∷ γ
        eS = down (lookup T γ) (pr (c .fst) (y .fst)) e∈

随后组装七槽环境，并由 definesB-in 把切割关系转换回可定义子集子句。

        δ7 = y ∷ container eS c y refl .fst ∷ eS ∷ δ4
    in c , ( c∈ , fillSnd i0 (c ∷ x ∷ γ) (lookup (N f1) γ) p ec'
               (∃̇∈ (var (sh  T)) (sndEx i0 i3 (definesB i6 (sh  w) i0 (sh  (N f0)))))
               ∣ eS , ( e∈ , fillSnd i0 (eS ∷ δ4) c y refl (definesB i6 (sh  w) i0 (sh  (N f0)))
                            (definesB-in i6 (sh  w) i0 (sh  (N f0)) δ7 (tg f0) cuts) i3 refl ) ∣₁

键的形状、表条目与切出条件编码完毕后，外层有界量词把这个截断整体用于候选输出的原元素。因此，这个语义记录足以重建整个成员关系子句的满足。

               (sh  (N f1)) refl ) })
  (g x x∈)

读取覆盖子句：取一个可拆成「标签一与 p 之对」的码 c，则仅仅地给出 c 处的表值 y 以及被 y 切出的集合 x。

all-out : ⟨ γ ⊨ allAt v w T C N ⟩ → (c p : S) → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (# ) (p .fst)
        → ∥ Σ[ y ∶ S ] Σ[ x ∶ S ] (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × (⟨ x .fst ∈ Vv ⟩ × Cuts (x .fst) Wv (y .fst))) ∥₁
all-out h c p c∈ ec = rec₁ squash₁
  (λ { (e , (e∈ , hy)) → rec₁ squash₁
    (λ { (y , s' , (ee , hx)) → map₁

证明消去表条目与三槽存在量化，而可定义子句读取产出元素与表值之间的切割关系。

      (λ { (x , (x∈ , hd)) →
        y , x , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
                , ( x∈ , definesB-out i0 (sh  w) i1 (sh  (N f0)) (x ∷ y ∷ s' ∷ e ∷ δ3) (tg f0) hd ) ) })
      hx })
    (sndEx-out i0 i3 (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0)))) (e ∷ δ3) hy) })

为作反向构造，固定码域的元素 c，并考察它作为 pr (# 1) p 的任一呈现。语义覆盖假设随后在命题截断下给出一个表取值及由该取值切出的子集；这些见证填入该呈现所需的有界结论。

  (useSnd i0 (c ∷ γ) (lookup (N f1) γ) p ec'
    (∃̇∈ (var (sh  T)) (sndEx i0 i3 (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0))))))
    (sh  (N f1)) refl (h c c∈))
  where
  ec' : c .fst ≡ pr N1v (p .fst)

借助 Tags，使用形式标签的等式被转换为所需的元数一等式。辅助容器只负责让分量与码始终处于有界量词内；它们不会给语义见证增加任何选择或唯一性。

  ec' = ec ∙ cong (λ a → pr a (p .fst)) (sym (tg f1))
  δ3 : Vec S ( + m)
  δ3 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ γ

因此，填充覆盖子句时遍历候选码域中每个被呈现为元数一键形状的元素。对每个这样的呈现，语义假设在命题截断下给出表取值、候选输出中由它切出的元素及二者的成员关系。直到后文加入 satAt，这里都不声称这些元素是真正的公式键。

all-in : ((c p : S) → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (# ) (p .fst)
          → ∥ Σ[ y ∶ S ] Σ[ x ∶ S ] (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × (⟨ x .fst ∈ Vv ⟩ × Cuts (x .fst) Wv (y .fst))) ∥₁)
       → ⟨ γ ⊨ allAt v w T C N ⟩
all-in g c c∈ = sndAll-in' (λ p s s∈ p∈ ec →
  map₁ (λ { (y , x , (e∈ , (x∈ , cuts))) →

最内层的有界存在量词现在以切出的集合 x 为见证，并同时接收 x 属于取值集合的证明以及刚由 definesB 编码的 Cuts 证据。这便完成反向翻译：表条目及其所切子集的语义见证给出成员关系子句的满足，而所有存在数据仍保留在命题截断中。

    let eS = down (lookup T γ) (pr (c .fst) (y .fst)) e∈
        δ6 = y ∷ container eS c y refl .fst ∷ eS ∷ p ∷ s ∷ c ∷ γ
    in eS , ( e∈ , fillSnd i0 (eS ∷ p ∷ s ∷ c ∷ γ) c y refl (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0))))
                     ∣ x , (x∈ , definesB-in i0 (sh  w) i1 (sh  (N f0)) (x ∷ δ6) (tg f0) cuts) ∣₁ i3 refl ) })
    (g c p c∈ (ec ∙ cong (λ a → pr a (p .fst)) (tg f1))))

覆盖子句含有同样两层存在选择：满足关系表的一个取值，以及该取值从工作集中切出的子集。为二者合成后的向外读法命名，使下一个论证能把这对仅仅存在的见证作为一个命题值整体处理。

  where
  sndAll-in' = sndAll-in i0 (sh  (N f1))
    (∃̇∈ (var (sh  T)) (sndEx i0 i3 (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0)))))) (c ∷ γ)

module DefRead {m : ℕ} (v w T C E : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N) (hs : ⟨ γ ⊨ satAt T w C E N ⟩) where

open Alphabet W
open Match W

前面的两个读取器提供所需桥梁。SatRead 把描述中的码域和表与 W 上真正的码及满足取值对齐；Read 把 defAt 读成两个语义切出条件。随后 DefOf (W .fst) 把每条解码得到的元数一公式解释为 W 的一个子集。

private module SR = SatRead T w C E N γ W qw tg hs
private module RD = Read v w T C N γ tg
private module DA = DefOf (W .fst)
private
  Vv = (lookup v γ) .fst
  Wv = (lookup w γ) .fst

记表槽与码槽所指称的底层集合为 Tv 与 Cv。satAt 的作用正在于：如今可以在这些描述集合中的成员关系与真正满足关系表、码域中的成员关系之间来回转换。

  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst

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

  toS : Formula Ab  → Formula S 
  toS = mapFo (asConst W)

表取值引理说：在公式键处记录的取值等于改名后公式的显式满足集合。证明复合表的外向投影与一致满足的取值认同。

  valOf : (ψ : Formula Ab ) (c y : S) → c .fst ≡ (keyS W ψ) .fst → ⟨ pr (c .fst) (y .fst) ∈ Tv ⟩
        → y .fst ≡ (Sat W (toS ψ)) .fst
  valOf ψ c y qc h = SR.T-out c y h .snd ∙ cong (λ p → p .fst) (val-at W W ψ c (SR.T-out c y h .fst) qc)

核心桥梁逐条处理公式。若 Cuts 说明 x 恰由 W 中那些其单变元环境属于 ψ 的满足集合的元素组成，那么 x 就等于这个特定的可定义子集 DA.defSet ψ。外延性通过两个成员关系方向证明此等式。

  cut≡ : (ψ : Formula Ab ) (x : S) → Cuts (x .fst) Wv ((Sat W (toS ψ)) .fst) → DA.defSet ψ ≡ x .fst
  cut≡ ψ x (o , i) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
    where
    fwd : (z : V ℓ) → ⟨ z ∈ DA.defSet ψ ⟩ → ⟨ z ∈ x .fst ⟩
    fwd z = rec₁ ((z ∈ x .fst) .snd)

第一个方向中，属于 DA.defSet ψ 的证明在命题截断下给出 W 中元素的一个表示。满足桥梁把该表示的单变元环境放入 ψ 的满足集合，于是 Cuts 的向内一半把所表示的集合放入 x。

      (λ { ((q , hq) , e) →
        i (down W z (subst (λ u → ⟨ u ∈ W .fst ⟩) e (ι∈ q)))
          (subst (λ u → ⟨ z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ W .fst ⟩) e (ι∈ q)))
          (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) e
            (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁)) })

另一个方向从 z ∈ x 出发。Cuts 的向外一半同时给出 z ∈ W 以及其单变元环境属于满足集合。∈-asFiber 把第一项转换为 W 的呈现中的一个实际索引，并给出回到 z 的路径。

    bwd : (z : V ℓ) → ⟨ z ∈ x .fst ⟩ → ⟨ z ∈ DA.defSet ψ ⟩
    bwd z hz =
      let zS = down x z hz
          zW = subst (λ u → ⟨ z ∈ u ⟩) qw (o zS hz .fst)
          fib = ∈-asFiber {a = z} {b = W .fst} zW

沿该呈现路径运输环境成员关系，再反向应用 defSet-Sat，便证明对应表示属于 DA.defSet ψ；沿同一路径运回后得到 z ∈ DA.defSet ψ，从而完成外延等式。

      in subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
           (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
             (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) (sym (fib .snd)) (o zS hz .snd)))

反过来，设已知 DA.defSet ψ 等于 x。为重建 Cuts，先取 x 的一个元素，把它改写为 DA.defSet ψ 的元素，再展开可定义子集的成员关系。由此同时得到它作为 W 中元素的表示，以及相应单变元环境属于满足集合的证明。

  cuts-of : (ψ : Formula Ab ) (x : S) → DA.defSet ψ ≡ x .fst → Cuts (x .fst) Wv ((Sat W (toS ψ)) .fst)
  cuts-of ψ x e = o , i
    where
    o : (z : S) → ⟨ z .fst ∈ x .fst ⟩ → ⟨ z .fst ∈ Wv ⟩ × ⟨ envOne (z .fst) ∈ (Sat W (toS ψ)) .fst ⟩
    o z hz = rec₁ (isProp× ((z .fst ∈ Wv) .snd) ((envOne (z .fst) ∈ (Sat W (toS ψ)) .fst) .snd))

展开这一成员关系，得到 W 中的一个表示，并经 defSet-Sat 得到其单变元环境属于所需满足集合。表示与原元素之间的等式把这两个结论都运输回 x 的该元素。

      (λ { ((q , hq) , eq) →
          subst (λ u → ⟨ z .fst ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ W .fst ⟩) eq (ι∈ q))
        , subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) eq (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁) })
      (subst (λ u → ⟨ z .fst ∈ u ⟩) (sym e) hz)
    i : (z : S) → ⟨ z .fst ∈ Wv ⟩ → ⟨ envOne (z .fst) ∈ (Sat W (toS ψ)) .fst ⟩ → ⟨ z .fst ∈ x .fst ⟩

为证明 Cuts 的向内一半，从 W 中一个已呈现的元素出发，并假定其单变元环境满足 ψ。满足桥梁把它转成属于 DA.defSet ψ，再由假定的等式 DA.defSet ψ = x .fst 把该元素放入 x。

    i z hw he =
      let fib = ∈-asFiber {a = z .fst} {b = W .fst} (subst (λ u → ⟨ z .fst ∈ u ⟩) qw hw)
      in subst (λ u → ⟨ z .fst ∈ u ⟩) e
           (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
             (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))

最后的运输只是在所选元素表示与其底层集合之间作对齐。因此，cut≡ 与 cuts-of 合起来把 ψ 的 Cuts 谓词同「等于单个可定义子集 DA.defSet ψ」对应起来；两个方向都没有断言定义公式唯一。

               (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) (sym (fib .snd)) he)))

现在可以准确陈述可靠性。在工作集槽与 W 已对齐、数码标签正确且 satAt 已校准码集和满足关系表的背景下，defAt 的满足迫使取值槽恰等于 𝒟ₒ (W .fst)。这里的 𝒟ₒ 收集由允许取 W 中参数的一阶公式定义出的 W 的子集，并非完整的内部幂集。

def-sound : ⟨ γ ⊨ defAt v w T C N ⟩ → Vv ≡ 𝒟ₒ (W .fst)
def-sound hd = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
  where
  hm = defAt-out v w T C N γ hd .fst
  ha = defAt-out v w T C N γ hd .snd

对正向包含，成员关系子句在命题截断下给出一个具有键形状的码、一个满足关系表条目，以及描述该条目所切子集的条件。satAt 把候选码域同真正码域对齐后，decodeAll 仅仅给出一条元数一公式，其编码具有所需的第二分量。表取值引理再把该条目的取值认同为这条公式的满足集合。

  fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ 𝒟ₒ (W .fst) ⟩
  fwd x hx = rec₁ ((x ∈ 𝒟ₒ (W .fst)) .snd)
    (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → rec₁ ((x ∈ 𝒟ₒ (W .fst)) .snd)
      (λ { (ψ , qp) →
        𝒟ₒ-intro (W .fst) x ∣ ψ , cut≡ ψ xS

Cuts 事实沿表取值认同被运至解码公式的满足集，而可定义幂集引入把切片集合放进 𝒟ₒ。截断的公式解码被消耗到命题值的引入中。

          (subst (λ u → Cuts x Wv u) (valOf ψ c y (ec ∙ cong (pr (# )) qp) e∈) cuts) ∣₁ })
      (decodeAll c (SR.C-out c c∈)  (p .fst) ec) })
    (RD.mem-out hm xS hx)
    where
    xS : S

取值槽被呈现为载体元素，以供成员关系子句向外方向读取。

    xS = down (lookup v γ) x hx

对反向包含，属于 𝒟ₒ (W .fst) 只给出命题截断下的一条公式 ψ 及等式 DA.defSet ψ = x。在消去到成员关系命题的过程中，defAt 的覆盖部分针对由这个临时见证 ψ 构造的键，给出一个表取值以及取值槽中的集合 x'。

  bwd : (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (W .fst) ⟩ → ⟨ x ∈ Vv ⟩
  bwd x hx = rec₁ ((x ∈ Vv) .snd)
    (λ { (ψ , e) → rec₁ ((x ∈ Vv) .snd)
      (λ { (y , x' , (e∈ , (x'∈ , cuts))) →
        subst (λ u → ⟨ u ∈ Vv ⟩)

切片等式沿表取值认同运输以恢复切片集的底层集合，运输把它放进取值槽。

          (sym (cut≡ ψ x' (subst (λ u → Cuts (x' .fst) Wv u) (valOf ψ (keyS W ψ) y refl e∈) cuts)) ∙ e)
          x'∈ })
      (RD.all-out ha (keyS W ψ) (sndS (keyS W ψ) (# ) (cd ψ) refl) (SR.C-in (keyS W ψ) (key∈AllCodes W ψ)) refl) })
    (𝒟ₒ-inv (W .fst) x hx)

完备性把同一等价关系反向使用。在仍假定工作集已对齐、标签正确且 satAt 成立时，取值槽与 𝒟ₒ (W .fst) 的相等足以构造 defAt 的满足。两个合取项分别说明：列出的每个集合都有定义公式，而每条元数一公式所定义的子集都会出现。

def-complete : Vv ≡ 𝒟ₒ (W .fst) → ⟨ γ ⊨ defAt v w T C N ⟩
def-complete qv = defAt-in v w T C N γ mem all
  where

每条公式的表条目从已定义的递归表中选取，后者同时保证表中的成员关系与显式满足集的认同。

  entry : (ψ : Formula Ab ) → Σ[ y ∶ S ] (⟨ pr ((keyS W ψ) .fst) (y .fst) ∈ Tv ⟩ × (y .fst ≡ (Sat W (toS ψ)) .fst))
  entry ψ = Table.val W W (keyS W ψ) (key∈AllCodes W ψ)
          , ( SR.T-in (keyS W ψ) (key∈AllCodes W ψ)
            , cong (λ p → p .fst) (val-at W W ψ (keyS W ψ) (key∈AllCodes W ψ) refl) )

对成员关系合取项，先把取值槽的元素运输到 𝒟ₒ (W .fst)，再由 𝒟ₒ-inv 展开。定义公式只在命题截断下存在。在该截断内部，证明组装它的公式键、相应表条目和所需的 Cuts 证据；整个过程没有全局选取定义公式，也没有把某条公式保留为规范数据。

  mem : ⟨ γ ⊨ memAt v w T C N ⟩
  mem = RD.mem-in (λ x x∈ → map₁
    (λ { (ψ , e) →
      keyS W ψ , sndS (keyS W ψ) (# ) (cd ψ) refl , entry ψ .fst
      , ( SR.C-in (keyS W ψ) (key∈AllCodes W ψ)

所用表取值是递归满足关系表已为该公式键确定的取值。沿它与显式满足集合的等式运输 cuts-of，便得到切出证据。这个临时公式见证始终留在 map₁ 内，因此所得成员关系见证仍受命题截断。

        , ( refl
          , ( entry ψ .snd .fst
            , subst (λ u → Cuts (x .fst) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ x e) ) ) ) })
    (𝒟ₒ-inv (W .fst) (x .fst) (subst (λ u → ⟨ x .fst ∈ u ⟩) qv x∈)))

覆盖合取项对码域中每个元数一的键证明，对分解被显式名指。

  all : ⟨ γ ⊨ allAt v w T C N ⟩
  all = RD.all-in (λ c p c∈ ec → map₁
    (λ { (ψ , qp) →
      let qc : c .fst ≡ (keyS W ψ) .fst
          qc = ec ∙ cong (pr (# )) qp

对给定的元数一键，解码仅仅给出一条公式 ψ，其编码是该键的第二分量。由引入规则，可定义子集 DA.defSet ψ 属于 𝒟ₒ (W .fst)；再沿假定的等式运输，便得到它属于取值槽。解码并未选出唯一或规范的公式。

          xS : S
          xS = down (lookup v γ) (DA.defSet ψ)
                 (subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (W .fst) (DA.defSet ψ) ∣ ψ , refl ∣₁))
      in entry ψ .fst , xS
       , ( subst (λ u → ⟨ pr u ((entry ψ .fst) .fst) ∈ Tv ⟩) (sym qc) (entry ψ .snd .fst)

满足关系表给出解码公式键所对应的取值，而 cuts-of 证明该取值从工作集中切出的恰是 DA.defSet ψ。连同刚得到的成员关系，这些数据满足覆盖子句。由于 decodeAll 的结果受命题截断，且只被消去到这个命题值子句中，构造只记录存在性，并不保留解码所得的公式。

         , ( subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (W .fst) (DA.defSet ψ) ∣ ψ , refl ∣₁)
           , subst (λ u → Cuts (DA.defSet ψ) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ xS refl) ) ) })
    (decodeAll c (SR.C-out c c∈)  (p .fst) ec))