可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

给定公式 φ，本章构造 satTable φ；其中每个条目把一个子公式键与其递归定义的满足关系值配对，并证明键唯一确定旁边记录的值。

递归的答案，装配起来。给定元语言的一条公式，这是「键与其处取值」之对构成的有穷集，公式自己一对、每条子公式各一对；造法与子公式闭包完全相同，理由也相同：元语言可以把自己已经造好的东西点名。

此处的一切按构造都是模型的元素。键是数码与码之对，而码取自模型自己的那套编码，故不携带可构造性证书，也不必去证。这是编码那一章的第二次实例化买下的东西，而本章正是花掉它的那一章。

递归真正向这张表索取的是另一个方向：任何被记录在某个键处的取值，就是那个键处的那个取值。正是在这里码等式必须单射，也正是在这里「碰巧在一个键处记了两样东西」的表根本不是一个函数。

open import Cubical.Foundations.Prelude using ( J )

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

open hPropView 𝒮ʟ using ( S )

键与条目

keyʟ φ 把 φ 的元数与其编码配对，ent φ 再把该键与 Sat B φ 配对。对条目与键分别应用同一棵子公式树，便得到 satTable φ 及其索引槽位 slot φ。

一个键是元数与码的对，而那正是内部递归每条子句所读的形状。一个条目是键与取值的对。

两者所处的形状相同，故只写一次，且写在别处。tree 就是闭包那一章的那次递归：它为每条子公式收集一样东西，而那样东西是什么是它的参数。给它条目，得到那张表；给它键，得到表所索引的那个槽。递归两者都要，且要它们逐个构造子地一致，故两者出自同一次递归而非两次。

keyʟ : ∀ {n} → Formula S n → S
keyʟ {n} φ = prʟ (numeralL n) LCode.⌜ φ ⌝

module _ (B : S) where

ent : ∀ {n} → Formula S n → S
ent φ = prʟ (keyʟ φ) (Sat B φ)

satTable : ∀ {n} → Formula S n → S
satTable = tree ent

slot : ∀ {n} → Formula S n → S
slot = tree keyʟ

反演满足关系表与槽位

四条反演引理都是 tree-inv 的实例：属于满足关系表或槽位会识别出贡献该元素的子公式，而 slot-ent 与 ent-slot 在条目及其键之间转换。

每个元素都是被收集之物之一。那正是闭包那一章所证的求逆，且它在那里是对着两个收集同时陈述的，故下面四条读式是它的四次实例化，此处不跑归纳。

module Parts (f : ∀ {m} → Formula S m → S) where

open TreeParts f public

satTable-inv : ∀ {n} (φ : Formula S n) (x : V ℓ)
             → ⟨ x ∈ (satTable φ) .fst ⟩ → Of ent ent φ x
satTable-inv = tree-inv ent ent

slot-inv : ∀ {n} (φ : Formula S n) (x : V ℓ)
         → ⟨ x ∈ (slot φ) .fst ⟩ → Of keyʟ keyʟ φ x
slot-inv = tree-inv keyʟ keyʟ

slot-ent : ∀ {n} (φ : Formula S n) (x : V ℓ)
         → ⟨ x ∈ (slot φ) .fst ⟩ → Of keyʟ ent φ x
slot-ent = tree-inv keyʟ ent

ent-slot : ∀ {n} (φ : Formula S n) (x : V ℓ)
         → ⟨ x ∈ (satTable φ) .fst ⟩ → Of ent keyʟ φ x
ent-slot = tree-inv ent keyʟ

键处取值的唯一性

若两个满足关系表条目具有相同的「元数与公式编码」键，配对及公式编码的单射性便等同它们的公式。因此 key-determines 证明两个条目携带相同的满足关系值。

两条键相同的公式取值相同，而码等式的单射性正是用在这里。诸元数由键的数码那一半得出相等，码等式由另一半得出；随后前者由道路归纳消掉，好让后者在单一元数处使用，而那也是它唯一为真的地方。

private
  same : ∀ {n} (ψ χ : Formula S n)
       → (LCode.⌜ ψ ⌝) .fst ≡ (LCode.⌜ χ ⌝) .fst → Sat B ψ ≡ Sat B χ
  same ψ χ e =
    cong (Sat B) (LCode.⌜⌝-inj ψ χ (Σ≡Prop (λ v → (isL v) .snd) e))

  cross : ∀ {n m} (ψ : Formula S n) (χ : Formula S m) → n ≡ m
        → (LCode.⌜ ψ ⌝) .fst ≡ (LCode.⌜ χ ⌝) .fst → Sat B ψ ≡ Sat B χ
  cross {n} ψ χ p = J
    (λ m' p' → (χ' : Formula S m')
             → (LCode.⌜ ψ ⌝) .fst ≡ (LCode.⌜ χ' ⌝) .fst → Sat B ψ ≡ Sat B χ')
    (same ψ) p χ

total : ∀ {n} (φ : Formula S n) (x : V ℓ) → ⟨ x ∈ (slot φ) .fst ⟩
      → ∥ (Σ[ y ∶ S ] ⟨ pr x (y .fst) ∈ (satTable φ) .fst ⟩) ∥₁
total φ x h = map₁
  (λ { (m , χ , (q , incl)) → Sat B χ
     , subst (λ w → ⟨ pr w ((Sat B χ) .fst) ∈ (satTable φ) .fst ⟩) (sym q)
         (incl (pr ((keyʟ χ) .fst) ((Sat B χ) .fst))
           (subst (λ w → ⟨ w ∈ (tree ent χ) .fst ⟩)
             (prʟ-fst (keyʟ χ) (Sat B χ)) (Parts.self ent χ))) })
  (slot-ent φ x h)

inSlot : ∀ {n} (φ : Formula S n) (x y : V ℓ)
       → ⟨ pr x y ∈ (satTable φ) .fst ⟩ → ⟨ x ∈ (slot φ) .fst ⟩
inSlot φ x y h = rec₁ ((x ∈ (slot φ) .fst) .snd)
  (λ { (m , χ , (q , incl)) →
    subst (λ w → ⟨ w ∈ (slot φ) .fst ⟩)
      (sym (pr-inj (q ∙ prʟ-fst (keyʟ χ) (Sat B χ)) .fst))
      (incl ((keyʟ χ) .fst) (Parts.self keyʟ χ)) })
  (ent-slot φ (pr x y) h)

key-determines : ∀ {n m} (ψ : Formula S n) (χ : Formula S m)
               → (keyʟ ψ) .fst ≡ (keyʟ χ) .fst → Sat B ψ ≡ Sat B χ
key-determines {n} {m} ψ χ e = cross ψ χ
  (#-inj′ (sym (numeralL-fst n) ∙ pr-inj q .fst ∙ numeralL-fst m))
  (pr-inj q .snd)
  where
  q : pr ((numeralL n) .fst) ((LCode.⌜ ψ ⌝) .fst)
    ≡ pr ((numeralL m) .fst) ((LCode.⌜ χ ⌝) .fst)
  q = sym (prʟ-fst (numeralL n) LCode.⌜ ψ ⌝)
    ∙ e ∙ prʟ-fst (numeralL m) LCode.⌜ χ ⌝

entry-out : ∀ {n m} (φ : Formula S n) (ψ : Formula S m) (y : V ℓ)
          → ⟨ pr ((keyʟ ψ) .fst) y ∈ (satTable φ) .fst ⟩
          → y ≡ (Sat B ψ) .fst
entry-out φ ψ y h = rec₁ (setIsSet y ((Sat B ψ) .fst))
  (λ { (m , χ , (q , _)) →
    let r = pr-inj (q ∙ prʟ-fst (keyʟ χ) (Sat B χ)) in
    r .snd ∙ cong (λ p → p .fst) (sym (key-determines ψ χ (r .fst))) })
  (satTable-inv φ (pr ((keyʟ ψ) .fst) y) h)

entry-in : ∀ {n} (φ : Formula S n)
         → ⟨ pr ((keyʟ φ) .fst) ((Sat B φ) .fst) ∈ (satTable φ) .fst ⟩
entry-in φ = subst (λ w → ⟨ w ∈ (satTable φ) .fst ⟩)
  (prʟ-fst (keyʟ φ) (Sat B φ)) (Parts.self ent φ)

构造子标签确定的子键

对于公式编码带有指定构造子标签的键，最后的分类讨论识别其槽位中的直接子公式键。二元、一元与量词构造子分别给出递归子句所需的、元数经过相应调整的键。

子句所作的那次分派，是十次验证之前的最后一步。一条子句在某个标签处陈述，收到一个那种形状的键；由上面那次求逆恢复出该键所命名的公式，随后其构造子必须与那个标签一致。这一步使用编码一章已有的装置，只导出而不重造：构造子可从标签还原，故「带某个标签的公式是什么形状」可以从标签算出来，而那条标签等式处理的正是公式自身的情形。

一条引理同时用于全部十条子句，它给出三件信息：那条公式的构造子是什么、被读出的元数就是它的元数、被读出的载荷就是它的载荷。

keyʟ-shape : ∀ {m} (ψ : Formula S m) (k : ℕ) (ar p : V ℓ)
           → (keyʟ ψ) .fst ≡ pr ar (pr (# k) p)
           → LCode.Match k ψ
           × ((# m ≡ ar) × ((LCode.payOf ψ) .fst ≡ p))
keyʟ-shape {m} ψ k ar p e =
    subst (λ j → LCode.Match j ψ) tag≡ (LCode.matches ψ)
  , ( sym (numeralL-fst m) ∙ pr-inj e' .fst
    , pr-inj inner .snd )
  where
  e' : pr ((numeralL m) .fst) ((LCode.⌜ ψ ⌝) .fst) ≡ pr ar (pr (# k) p)
  e' = sym (prʟ-fst (numeralL m) LCode.⌜ ψ ⌝) ∙ e

  inner : pr ((numeralL (LCode.tagOf ψ)) .fst) ((LCode.payOf ψ) .fst)
        ≡ pr (# k) p
  inner = sym (prʟ-fst (numeralL (LCode.tagOf ψ)) (LCode.payOf ψ))
        ∙ sym (cong (λ p → p .fst) (LCode.shape ψ))
        ∙ pr-inj e' .snd

  tag≡ : LCode.tagOf ψ ≡ k
  tag≡ = #-inj′ (sym (numeralL-fst (LCode.tagOf ψ)) ∙ pr-inj inner .fst)