The object language over the model

诸读式写的是关于层级的事，而那座桥把它们运进模型。本章把桥走一遍，并陈述一条被引用的读式在彼岸说的是什么。

有一处小小的皱褶。读式的含义当初是按「变元在层级环境中的取值」陈述的；而在彼岸，环境装的是模型的元素，那个层级环境是取底集得来的。在投影后的环境中查表就是把查表的结果投影，这是一次两行的归纳，之后被引用的读式所说的，恰是原读式关于诸底集所说的。

第一条过河的读式是此后一切所由构造的那条：有序对。它之上不再需要新的论证，因为那座桥是通用的，而诸读式自身的刻画早已证过一次。

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

open import Base.Prelude
open import Base.Truth

module L.Coding.Model {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇
        ; ∀̇_; ∀̇∈; ∃̇_; ∃̇∈ )
open import FOL.Manipulation.Relabelling using ( mapTm; mapFo )
import FOL.Absoluteness
import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import V.Model {ℓ} using ( pair-singleton )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import FOL.Manipulation.Bounding using ( BoundedFo )
open import L.Absoluteness {ℓ} using ( InL; liftFo; transferFo )
open import L.Coding.Base {ℓ}
  using ( prAt; Δ₀-prAt; prAt-adequate; sglConAt; pairConAt; tagAt )
open import L.Coding.Environment {ℓ}
  using ( sucAt; Δ₀-sucAt; sucAt-adequate; consAt; Δ₀-consAt; consAt-adequate
        ; env; cons; shiftPairAt )
open import L.Axioms.Numerals {ℓ}
  using ( numeralL; numeralL-fst; pairʟ; pairʟ-fst; sucʟ; sucʟ-fst )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Vec using ( map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ using ( S )

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

在投影后的环境中查表

两行，也是这次过河所付的全部记账。

lookup-fst : ∀ {n} (i : Fin n) (γ : S ^ n)
           → lookup i (map fst γ) ≡ fst (lookup i γ)
lookup-fst zero    (x ∷ γ) = refl
lookup-fst (suc i) (x ∷ γ) = lookup-fst i γ

有序对

被引用的读式就是原读式沿桥抬升，而抬升什么也不索取：该读式不点名任何常元，故没有东西需要可构造，合格性证书是空的。

它的含义分三步。桥把「在模型中满足」等同于「在层级中、于投影后的环境处满足」；读式自家的刻画说出那是什么；诸查表被投影。出来的正是消费方想要的陈述：一个变元的取值，是另两个变元取值的 Kuratowski 对，作为集合而言。

private
  PairIs : V ℓ → V ℓ → Ω
  PairIs a p = (a ≡ p) , setIsSet a p

prAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
prAtL q u v = liftFo (prAt q u v) _

prAtL-adequate : ∀ {n} (q u v : Fin n) (γ : S ^ n)
  → (γ ⊨ prAtL q u v)
  ≡ PairIs (fst (lookup q γ)) (pr (fst (lookup u γ)) (fst (lookup v γ)))
prAtL-adequate q u v γ =
    transferFo (prAt q u v) _ (Δ₀-prAt q u v) γ
  ∙ prAt-adequate q u v (map fst γ)
  ∙ cong₂ PairIs (lookup-fst q γ)
      (cong₂ pr (lookup-fst u γ) (lookup-fst v γ))

取值

对象语言里的函数是有序对之集，故凡用到函数的地方，所问的唯一一件事就是某个给定的对是否属于它。那是在该函数上的一个有界存在，里面装着对读式，而它的含义是那个 Kuratowski 对的隶属关系。

反向是模型出力之处，值得留意。要满足那个存在量词，必须拿出一个模型的元素，其底集是那个对；而假设只给了一个集合。它可构造，因为它属于某个可构造之物，而这个类传递。全部论证仅此而已，而同一步将在此后每个「见证必须造在模型之内、而非仅在层级之内」的地方重现。

appAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
appAt f x y = ∃̇∈ (var f) (prAtL zero (suc x) (suc y))

appAt-adequate : ∀ {n} (f x y : Fin n) (γ : S ^ n)
  → (γ ⊨ appAt f x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (lookup f γ))
appAt-adequate f x y γ = ⇔toPath fwd bwd
  where
  a = fst (lookup x γ)
  b = fst (lookup y γ)
  F = lookup f γ

  read : (z : S) → ⟨ (z ∷ γ) ⊨ prAtL zero (suc x) (suc y) ⟩ → fst z ≡ pr a b
  read z h = subst ⟨_⟩ (prAtL-adequate zero (suc x) (suc y) (z ∷ γ)) h

  fwd : ⟨ γ ⊨ appAt f x y ⟩ → ⟨ pr a b ∈ fst F ⟩
  fwd = PT.rec (snd (pr a b ∈ fst F))
    (λ { (z , (z∈F , h)) → subst (λ w → ⟨ w ∈ fst F ⟩) (read z h) z∈F })

  bwd : ⟨ pr a b ∈ fst F ⟩ → ⟨ γ ⊨ appAt f x y ⟩
  bwd h = ∣ zS , (h , subst ⟨_⟩
      (sym (prAtL-adequate zero (suc x) (suc y) (zS ∷ γ))) refl) ∣₁
    where
    zS : S
    zS = pr a b , isL-trans {x = fst F} {y = pr a b} h (F .snd)

单值性

作为函数的另一半：一个对的第一分量决定它的第二分量。三个无界量词 (此处不费分文)，加上面那条读式的两次应用。

陈述为两个方向而非一条道路，因为消费方就是这么用的，也因为把右侧造成一个命题只会把同一句话说得更长。读出来的那个方向才要紧：从对象语言的断言，得到「记在同一自变量下的两个取值相等」的一份真凭实据。

svAt : ∀ {n} → Fin n → Formula S n
svAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero)
  ⇒̇ (appAt (suc (suc (suc f))) (suc (suc zero)) zero
  ⇒̇ (var (suc zero) ≐ var zero)))))

module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds : S → S → Type (ℓ-suc ℓ)
    Holds x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at : (x y y' : S)
       → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero))
       ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero)
                  (y' ∷ y ∷ x ∷ γ)

    at' : (x y y' : S)
        → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) zero)
        ≡ (pr (fst x) (fst y') ∈ fst (lookup f γ))
    at' x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) zero
                   (y' ∷ y ∷ x ∷ γ)

  svAt-out : ⟨ γ ⊨ svAt f ⟩
           → (x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y'
  svAt-out h x y y' p q = h x y y'
    (subst ⟨_⟩ (sym (at x y y')) p) (subst ⟨_⟩ (sym (at' x y y')) q)

  svAt-in : ((x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y')
          → ⟨ γ ⊨ svAt f ⟩
  svAt-in h x y y' p q = h x y y'
    (subst ⟨_⟩ (at x y y') p) (subst ⟨_⟩ (at' x y y') q)

定义域

落在定义域中就是有取值：在上面那条读式上作一个无界存在。定义域本身则是恰以那些东西为成员的集合，用两条蕴含说出，因为对象语言没有自带的双条件，而把它摊开来写比添一个更短。

两者各自只用一个方向，而被取出的也只有那两个方向。一个握着表的消费方，要么问「这个自变量有条目，故它在定义域中」，要么问「这个自变量在定义域中，故它有条目」；没有谁想要那句陈述本身作为命题。

那两条都是消去，而名字没有说出这一点：domAt-in 朝「有条目」拆，domAt-out 朝「在定义域中」拆。引入 (那才是「必须满足这句陈述」的一张表所要的) 来得晚，于是取了第三个名字，而没有占用它们中的任何一个。

inDomAt : ∀ {n} → Fin n → Fin n → Formula S n
inDomAt f x = ∃̇ (appAt (suc f) (suc x) zero)

inDomAt-adequate : ∀ {n} (f x : Fin n) (γ : S ^ n)
  → (γ ⊨ inDomAt f x)
  ≡ (∃[ y ∶ S ] (pr (fst (lookup x γ)) (fst y) ∈ fst (lookup f γ)))
inDomAt-adequate f x γ =
  cong (⋁ S) (funExt (λ y → appAt-adequate (suc f) (suc x) zero (y ∷ γ)))

domAt : ∀ {n} → Fin n → Fin n → Formula S n
domAt f d = ∀̇ ( (inDomAt (suc f) zero ⇒̇ (var zero ∈̇ var (suc d)))
             ∧̇ ((var zero ∈̇ var (suc d)) ⇒̇ inDomAt (suc f) zero) )

module _ {n : ℕ} (f d : Fin n) (γ : S ^ n) where
  private
    step : (x : S)
         → ((x ∷ γ) ⊨ inDomAt (suc f) zero)
         ≡ (∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)))
    step x = inDomAt-adequate (suc f) zero (x ∷ γ)

  domAt-out : ⟨ γ ⊨ domAt f d ⟩ → (x y : S)
            → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
            → ⟨ fst x ∈ fst (lookup d γ) ⟩
  domAt-out h x y p = h x .fst (subst ⟨_⟩ (sym (step x)) ∣ y , p ∣₁)

  domAt-in : ⟨ γ ⊨ domAt f d ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩
           → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁
  domAt-in h x m = subst ⟨_⟩ (step x) (h x .snd m)

  domAt-intro : ((x : S)
                 → (⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩
                    → ⟨ fst x ∈ fst (lookup d γ) ⟩)
                 × (⟨ fst x ∈ fst (lookup d γ) ⟩
                    → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩))
              → ⟨ γ ⊨ domAt f d ⟩
  domAt-intro g x = (λ h → g x .fst (subst ⟨_⟩ (step x) h))
                  , (λ m → subst ⟨_⟩ (sym (step x)) (g x .snd m))

模型之内的对

每个码都由配对造出，故下面每个构造都需要「L 两元素的有序对仍是 L 的元素」。确实如此，用模型自己的配对三次即可，而数码那一章的投影等式说：沿底层集合读出来就把层级的对还了回来。单点集是两分量相等的对，这是层级供给的那一条小小恒等式。

prʟ : S → S → S
prʟ a b = pairʟ (pairʟ a a) (pairʟ a b)

prʟ-fst : (a b : S) → fst (prʟ a b) ≡ pr (fst a) (fst b)
prʟ-fst a b =
    pairʟ-fst (pairʟ a a) (pairʟ a b)
  ∙ cong₂ ⁅_,_⁆ (pairʟ-fst a a ∙ pair-singleton (fst a)) (pairʟ-fst a b)

编码，在模型处

对与诸数码是单射的，而这就是编码那一章向一个结构索取的全部，故对象语言可以编码进 L 自身。由此得到两件事，而两件都是想要的。一个码按构造就是模型的元素，没有可构造性证书要扛、也没有要证。而码等式在该元数处是单射的，由那一章自己的定理给出，而这正是「以码为索引的表」所需要的：两处不同子公式的出现不可共用一个键，否则表就多值，而它的存在性会垮。

那座桥说两套编码一致：把模型的一个码沿底层集合读出来，得到的是层级为那条换名后的公式所给的码。十二条子句加两条，每条都是「架在下面那条之上」的一条标签等式。正是它使本章那些写在层级一侧的读式，能施于造在模型一侧的诸码。

prʟ-inj : {a b c d : S} → prʟ a b ≡ prʟ c d → (a ≡ c) × (b ≡ d)
prʟ-inj {a} {b} {c} {d} e =
    Σ≡Prop (λ v → snd (isL v)) (pr-inj q .fst)
  , Σ≡Prop (λ v → snd (isL v)) (pr-inj q .snd)
  where
  q : pr (fst a) (fst b) ≡ pr (fst c) (fst d)
  q = sym (prʟ-fst a b) ∙ cong fst e ∙ prʟ-fst c d

numeralL-inj : {j k : ℕ} → numeralL j ≡ numeralL k → j ≡ k
numeralL-inj {j} {k} e =
  #-inj′ (sym (numeralL-fst j) ∙ cong fst e ∙ numeralL-fst k)

module LCode = FOL.Coding {ℓ-suc ℓ} 𝒮ʟ prʟ prʟ-inj numeralL numeralL-inj

tagBridge : (k : ℕ) (x : S) → fst (LCode.mkTag k x) ≡ VCode.mkTag k (fst x)
tagBridge k x = prʟ-fst (numeralL k) x ∙ cong₂ pr (numeralL-fst k) refl

codeBridgeTm : ∀ {n} (t : Term S n) → fst LCode.⌜ t ⌝ᵗ ≡ VCode.⌜ mapTm fst t ⌝ᵗ
codeBridgeTm (con c) = tagBridge  c
codeBridgeTm (var i) =
  tagBridge  (numeralL (toℕ i)) ∙ cong (VCode.mkTag ) (numeralL-fst (toℕ i))

codeBridge : ∀ {n} (φ : Formula S n) → fst LCode.⌜ φ ⌝ ≡ VCode.⌜ mapFo fst φ ⌝
codeBridge (t ∈̇ u) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (t ≐ u) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (a ∧̇ b) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ∨̇ b) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ⇒̇ b) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (¬̇ a)   = tagBridge  _ ∙ cong (VCode.mkTag ) (codeBridge a)
codeBridge ⊤̇       = tagBridge  _ ∙ cong (VCode.mkTag ) (numeralL-fst )
codeBridge ⊥̇       = tagBridge  _ ∙ cong (VCode.mkTag ) (numeralL-fst )
codeBridge (∃̇ a)   = tagBridge  _ ∙ cong (VCode.mkTag ) (codeBridge a)
codeBridge (∀̇ a)   = tagBridge  _ ∙ cong (VCode.mkTag ) (codeBridge a)
codeBridge (∀̇∈ t a) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
codeBridge (∃̇∈ t a) = tagBridge  _ ∙ cong (VCode.mkTag )
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))

环境

一个环境是取值落在给定集合中的函数，故「某集合之上的环境」是四者的合取：单值、定义域为给定者、取值落在该落的地方，以及由诸对构成。

第四条容易漏掉，而漏掉是致命的。另外三条谈的全是某集合中的诸对，对「不是对的成员」只字未提，故没有它，一个集合可以携带任意多的垃圾而仍然合格。若那条谓词只被检验，这不费分文；但「以成员描述集合」的那个框架断言双向，于是满足它的取值就得包含每一个带垃圾的集合：那是真类，是没有集合能兑现的假设。这一合取项把每个成员钉成「索引与取值之对」，从而使环境成为一个积的子集，而它们的全体成为一个集合。

只给出四个投影，因为消费方想要的仅此而已。某个特定集合是否就是给定长度的全体环境之集，是另一个问题，而且更难；这里说的只是「单个东西是一个环境」是什么意思。

valuesInAt : ∀ {n} → Fin n → Fin n → Formula S n
valuesInAt f B = ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero
                     ⇒̇ (var zero ∈̇ var (suc (suc B))) ))

valuesInAt-out : ∀ {n} (f B : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ valuesInAt f B ⟩ → (x y : S)
               → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
               → ⟨ fst y ∈ fst (lookup B γ) ⟩
valuesInAt-out f B γ h x y p = h x y
  (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ))) p)

pairsInAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
pairsInAt e d B =
  ∀̇∈ (var e) (∃̇∈ (var (suc d)) (∃̇∈ (var (suc (suc B)))
    (prAtL (suc (suc zero)) (suc zero) zero)))

pairsIn-out : ∀ {n} (e d B : Fin n) (γ : S ^ n) → ⟨ γ ⊨ pairsInAt e d B ⟩
            → (s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
            → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                  (⟨ fst u ∈ fst (lookup d γ) ⟩
                   × (⟨ fst v ∈ fst (lookup B γ) ⟩
                      × (fst s ≡ pr (fst u) (fst v)))))) ∥₁
pairsIn-out e d B γ h s s∈ = PT.rec squash₁
  (λ { (u , (u∈ , hv)) → PT.map
    (λ { (v , (v∈ , hp)) → u , (v , (u∈ , (v∈ , subst ⟨_⟩
      (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ)) hp))) })
    hv })
  (h s s∈)

pairsIn-in : ∀ {n} (e d B : Fin n) (γ : S ^ n)
           → ((s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
              → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                    (⟨ fst u ∈ fst (lookup d γ) ⟩
                     × (⟨ fst v ∈ fst (lookup B γ) ⟩
                        × (fst s ≡ pr (fst u) (fst v)))))) ∥₁)
           → ⟨ γ ⊨ pairsInAt e d B ⟩
pairsIn-in e d B γ k s s∈ = PT.map
  (λ { (u , (v , (u∈ , (v∈ , eq)))) → u , (u∈ , ∣ v , (v∈ , subst ⟨_⟩
    (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ))) eq) ∣₁) })
  (k s s∈)

envOverAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envOverAt e d B =
  svAt e ∧̇ (domAt e d ∧̇ (valuesInAt e B ∧̇ pairsInAt e d B))

module _ {n : ℕ} (e d B : Fin n) (γ : S ^ n) (h : ⟨ γ ⊨ envOverAt e d B ⟩) where
  envOver-sv     : ⟨ γ ⊨ svAt e ⟩
  envOver-sv     = h .fst
  envOver-dom    : ⟨ γ ⊨ domAt e d ⟩
  envOver-dom    = h .snd .fst
  envOver-values : ⟨ γ ⊨ valuesInAt e B ⟩
  envOver-values = h .snd .snd .fst
  envOver-pairs  : ⟨ γ ⊨ pairsInAt e d B ⟩
  envOver-pairs  = h .snd .snd .snd

一条描述在任何「把同样三个集合放在它所看之处」的框架里读起来都一样。上面每条读式都只经一次查表的 fst 陈述，别无其他，故把那条描述从一个环境搬到另一个环境是四次搬运、不必动脑。十二条子句里有七条绑定自己的周遭集合，而这就是把「那个集合的成员就是诸环境」变回「关于某个构造真正造出的集合」的那句话的东西。

valuesInAt-in : ∀ {n} (f B : Fin n) (γ : S ^ n)
              → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
                 → ⟨ fst y ∈ fst (lookup B γ) ⟩)
              → ⟨ γ ⊨ valuesInAt f B ⟩
valuesInAt-in f B γ k x y hp = k x y
  (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ)) hp)

envOverAt-transport : ∀ {n n'} (γ : S ^ n) (γ' : S ^ n')
                      (e d B : Fin n) (e' d' B' : Fin n')
                    → fst (lookup e γ) ≡ fst (lookup e' γ')
                    → fst (lookup d γ) ≡ fst (lookup d' γ')
                    → fst (lookup B γ) ≡ fst (lookup B' γ')
                    → ⟨ γ ⊨ envOverAt e d B ⟩ → ⟨ γ' ⊨ envOverAt e' d' B' ⟩
envOverAt-transport γ γ' e d B e' d' B' qe qd qb h =
    svAt-in e' γ' (λ x y y' p q →
      svAt-out e γ (envOver-sv e d B γ h) x y y'
        (subst ⟨_⟩ (sym (at x y)) p) (subst ⟨_⟩ (sym (at x y')) q))
  , ( domAt-intro e' d' γ'
      (λ x → (λ m → subst (λ w → ⟨ fst x ∈ w ⟩) qd
                (PT.rec (snd (fst x ∈ fst (lookup d γ)))
                  (λ { (y , p) → domAt-out e d γ (envOver-dom e d B γ h) x y
                         (subst ⟨_⟩ (sym (at x y)) p) })
                  m))
            , (λ hx → PT.map (λ { (y , p) → y , subst ⟨_⟩ (at x y) p })
                (domAt-in e d γ (envOver-dom e d B γ h) x
                  (subst (λ w → ⟨ fst x ∈ w ⟩) (sym qd) hx))))
    , ( valuesInAt-in e' B' γ'
        (λ x y p → subst (λ w → ⟨ fst y ∈ w ⟩) qb
          (valuesInAt-out e B γ (envOver-values e d B γ h) x y
            (subst ⟨_⟩ (sym (at x y)) p)))
      , pairsIn-in e' d' B' γ'
        (λ s s∈ → PT.map
          (λ { (u , (v , (u∈ , (v∈ , eq)))) →
            u , (v , ( subst (λ w → ⟨ fst u ∈ w ⟩) qd u∈
                     , ( subst (λ w → ⟨ fst v ∈ w ⟩) qb v∈ , eq ) )) })
          (pairsIn-out e d B γ (envOver-pairs e d B γ h) s
            (subst (λ w → ⟨ fst s ∈ w ⟩) (sym qe) s∈))) ) )
  where
  at : (x y : S) → (pr (fst x) (fst y) ∈ fst (lookup e γ))
                 ≡ (pr (fst x) (fst y) ∈ fst (lookup e' γ'))
  at x y = cong (λ w → pr (fst x) (fst y) ∈ w) qe

标签

一个码把它的构造子作为数码放在一个对的第一分量里，故读一个码的形状，就是读一个第一分量为给定数码的对。那条读式本可以像别的一样被引用，但那样比直接写还贵：层级那边的版本把该数码作为层级的常元点名，于是桥会索取一份沿公式整个形状穿行的可构造性证书。

直接写走的是短路，也是桥那一章推荐的路。L 的数码本来就是模型的元素，故它在此处本来就是合法常元；一个无界存在说「有个东西等于它，而那个对由它造出」。无界不费分文，而下面两条读式原样复用对读式，什么也不必重推。

第二条是此后出力的那条。对象语言的每个二元构造子，其码都是同一个形状：标签施于两个子码之对，彼此只差标签是哪个数码。

tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = ∃̇ ((var zero ≐ con (numeralL k)) ∧̇ prAtL (suc s) zero (suc x))

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : S ^ n)
  → (γ ⊨ tagAtL s k x)
  ≡ PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))
tagAtL-adequate s k x γ = ⇔toPath fwd bwd
  where
  target = PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))

  fwd : ⟨ γ ⊨ tagAtL s k x ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (e , p)) →
      subst ⟨_⟩ (prAtL-adequate (suc s) zero (suc x) (z ∷ γ)) p
      ∙ cong (λ w → pr w (fst (lookup x γ))) (e ∙ numeralL-fst k) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ tagAtL s k x ⟩
  bwd q = ∣ numeralL k , (refl , subst ⟨_⟩
      (sym (prAtL-adequate (suc s) zero (suc x) (numeralL k ∷ γ)))
      (q ∙ cong (λ w → pr w (fst (lookup x γ))) (sym (numeralL-fst k)))) ∣₁

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b =
  ∃̇ (prAtL zero (suc a) (suc b) ∧̇ tagAtL (suc s) k zero)

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs (fst (lookup s γ))
      (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ))))
tagPairAtL-adequate s k a b γ = ⇔toPath fwd bwd
  where
  A = fst (lookup a γ)
  B = fst (lookup b γ)
  target = PairIs (fst (lookup s γ)) (pr (# k) (pr A B))

  fwd : ⟨ γ ⊨ tagPairAtL s k a b ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , t)) →
      subst ⟨_⟩ (tagAtL-adequate (suc s) k zero (z ∷ γ)) t
      ∙ cong (pr (# k))
          (subst ⟨_⟩ (prAtL-adequate zero (suc a) (suc b) (z ∷ γ)) p) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ tagPairAtL s k a b ⟩
  bwd q = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc a) (suc b) (zS ∷ γ))) e
      , subst ⟨_⟩ (sym (tagAtL-adequate (suc s) k zero (zS ∷ γ)))
          (q ∙ cong (pr (# k)) (sym e)) ) ∣₁
    where
    zS : S
    zS = prʟ (lookup a γ) (lookup b γ)
    e : fst zS ≡ pr A B
    e = prʟ-fst (lookup a γ) (lookup b γ)

以外延给出集合

凡取值为集合的递归，其每一条子句说的都是同一句话：这个取值恰是满足某某条件的那些东西之集。把它一次写出来，条件留作参数，那就是一个量词之下的两条蕴含，而它的两种读法就是两个投影。什么也没有证，而这正是要点：此后一条递归子句的代价，只剩它的条件。

诸集合运算随即而来，每个一条条件那么长，且含义都已在手。一条子句其余的内容全在它的条件里说，而那正是某个特定递归的数学之所在。

extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : S ^ n) where
  extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
            → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
  extAt-out h = h .fst

  extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
           → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩
  extAt-in h = h .snd

  extAt-in-both : ((z : S) → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
                → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩)
                → ⟨ γ ⊨ extAt y φ ⟩
  extAt-in-both f g = f , g

private
  memb : ∀ {n} → Fin n → Formula S (suc n)
  memb a = var zero ∈̇ var (suc a)

interAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
interAt y a b = extAt y (memb a ∧̇ memb b)

unionAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
unionAt y a b = extAt y (memb a ∨̇ memb b)

diffAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
diffAt y a b = extAt y (memb a ∧̇ ¬̇ memb b)

sameAt : ∀ {n} → Fin n → Fin n → Formula S n
sameAt y a = extAt y (memb a)

emptyAt : ∀ {n} → Fin n → Formula S n
emptyAt y = extAt y ⊥̇

implAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
implAt y e a b = extAt y (memb e ∧̇ (memb a ⇒̇ memb b))

分两层读一个键

递归所遍历的诸码携带自己的元数：一个条目是「元数的数码」与「码本身」之对，而码本身又是「标签」与「载荷」之对。故一条子句的假设必须读两层，不是一层；而只读外层比不完整更糟。配对是单射的，于是一层的读式会悄悄把元数与构造子标签匹配起来，并把载荷自己的标签当作子码绑定：那条子句于是在除一个元数外的所有元数上空洞，而在那一个上是错的。Agda 不会报告这件事，因为那条读式仍然为真；它只是无法被供给。

两层由一个「对内层码作存在」读出，上面的对读式钉住外层，标签读式钉住内层。元数留作变元，好让子句能谈论它，而四个改变元数的构造子正需要这一点。

arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b =
  ∃̇ (prAtL (suc c) (suc ar) zero ∧̇ tagPairAtL zero k (suc a) (suc b))

arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ))
        (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ)))))
arityTagPairAtL-adequate c ar k a b γ = ⇔toPath fwd bwd
  where
  N = fst (lookup ar γ)
  P = pr (fst (lookup a γ)) (fst (lookup b γ))
  target = PairIs (fst (lookup c γ)) (pr N (pr (# k) P))

  fwd : ⟨ γ ⊨ arityTagPairAtL c ar k a b ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , t)) →
      subst ⟨_⟩ (prAtL-adequate (suc c) (suc ar) zero (z ∷ γ)) p
      ∙ cong (pr N) (subst ⟨_⟩ (tagPairAtL-adequate zero k (suc a) (suc b) (z ∷ γ)) t) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ arityTagPairAtL c ar k a b ⟩
  bwd q = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate (suc c) (suc ar) zero (zS ∷ γ)))
          (q ∙ cong (pr N) (sym e))
      , subst ⟨_⟩ (sym (tagPairAtL-adequate zero k (suc a) (suc b) (zS ∷ γ))) e ) ∣₁
    where
    zS : S
    zS = prʟ (numeralL k) (prʟ (lookup a γ) (lookup b γ))
    e : fst zS ≡ pr (# k) P
    e = prʟ-fst (numeralL k) (prʟ (lookup a γ) (lookup b γ))
      ∙ cong₂ pr (numeralL-fst k) (prʟ-fst (lookup a γ) (lookup b γ))

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n
arityTagAtL c ar k a =
  ∃̇ (prAtL (suc c) (suc ar) zero ∧̇ tagAtL zero k (suc a))

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagAtL c ar k a)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ)) (pr (# k) (fst (lookup a γ))))
arityTagAtL-adequate c ar k a γ = ⇔toPath fwd bwd
  where
  N = fst (lookup ar γ)
  A = fst (lookup a γ)
  target = PairIs (fst (lookup c γ)) (pr N (pr (# k) A))

  fwd : ⟨ γ ⊨ arityTagAtL c ar k a ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , t)) →
      subst ⟨_⟩ (prAtL-adequate (suc c) (suc ar) zero (z ∷ γ)) p
      ∙ cong (pr N) (subst ⟨_⟩ (tagAtL-adequate zero k (suc a) (z ∷ γ)) t) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ arityTagAtL c ar k a ⟩
  bwd q = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate (suc c) (suc ar) zero (zS ∷ γ)))
          (q ∙ cong (pr N) (sym e))
      , subst ⟨_⟩ (sym (tagAtL-adequate zero k (suc a) (zS ∷ γ))) e ) ∣₁
    where
    zS : S
    zS = prʟ (numeralL k) (lookup a γ)
    e : fst zS ≡ pr (# k) A
    e = prʟ-fst (numeralL k) (lookup a γ) ∙ cong₂ pr (numeralL-fst k) refl

在表中查一个子码

诸框架绑定一个码的载荷，却从不在其上查表，因为载荷分量可能是词项码，而表在那里什么也没有。想要取值的关系于是必须自己造那个键：把元数与该分量配成对，再在那里读表。

那是对该键的一个存在量词，也是十二条关系中四条所由构造的部件。谈论下一元数处子公式的那两条，需要的是同一件事而元数加一，即此物再加一层。

subValAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
subValAt T ar a y =
  ∃̇ (prAtL zero (suc ar) (suc a) ∧̇ appAt (suc T) zero (suc y))

subValAt-adequate : ∀ {n} (T ar a y : Fin n) (γ : S ^ n)
  → (γ ⊨ subValAt T ar a y)
  ≡ (pr (pr (fst (lookup ar γ)) (fst (lookup a γ))) (fst (lookup y γ))
      ∈ fst (lookup T γ))
subValAt-adequate T ar a y γ = ⇔toPath fwd bwd
  where
  K = pr (fst (lookup ar γ)) (fst (lookup a γ))
  target = pr K (fst (lookup y γ)) ∈ fst (lookup T γ)

  fwd : ⟨ γ ⊨ subValAt T ar a y ⟩ → ⟨ target ⟩
  fwd = PT.rec (snd target)
    (λ { (z , (p , q)) →
      subst (λ w → ⟨ pr w (fst (lookup y γ)) ∈ fst (lookup T γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc ar) (suc a) (z ∷ γ)) p)
        (subst ⟨_⟩ (appAt-adequate (suc T) zero (suc y) (z ∷ γ)) q) })

  bwd : ⟨ target ⟩ → ⟨ γ ⊨ subValAt T ar a y ⟩
  bwd h = ∣ zS
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc ar) (suc a) (zS ∷ γ))) e
      , subst ⟨_⟩ (sym (appAt-adequate (suc T) zero (suc y) (zS ∷ γ)))
          (subst (λ w → ⟨ pr w (fst (lookup y γ)) ∈ fst (lookup T γ) ⟩) (sym e) h) ) ∣₁
    where
    zS : S
    zS = prʟ (lookup ar γ) (lookup a γ)
    e : fst zS ≡ K
    e = prʟ-fst (lookup ar γ) (lookup a γ)

一条子句的形状

对码的递归由子句陈述，而子句只有几种形状，不是十二种。一个二元构造子的子句说：对索引中每个以此标签架在这两个子码之上的码，以及表在这三者处所记录的取值，某某成立。除了那个「某某」，其余全是固定的，故只写一次，把那条关系留作参数，而三个二元构造子只差交给它的是哪条关系。

被绑定的有五样，按读者遇到的次序：那个码、它的元数、它的两个载荷分量、以及表在该码处记录的取值。诸载荷分量处的取值不被绑定，而这正是使该框架通用之处。一个联结词的载荷是一对公式码，它的子句确实要它们；但一个原子的载荷是一对词项码，表在那里根本没有条目，而有界量词的载荷则两者混杂。故框架只绑定每个构造子都有的东西，把查表留给那条关系，由它自行执行。

把子句读回来是沿诸读式的适足性作一串代换，而它按可靠性证明所消费的方向陈述：给定索引中一个那种形状的码与三个被记录的取值，那条关系成立。

module _ {n : ℕ} where
  private
    sh5 : Fin n → Fin ( + n)
    sh5 i = suc (suc (suc (suc (suc i))))

    c5 n5 a5 b5 yc5 : Fin ( + n)
    c5  = suc (suc (suc (suc zero)))
    n5  = suc (suc (suc zero))
    a5  = suc (suc zero)
    b5  = suc zero
    yc5 = zero

  binClauseAt : Fin n → Fin n → ℕ → Formula S ( + n) → Formula S n
  binClauseAt C T k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ (∀̇ (∀̇
      ( arityTagPairAtL c5 n5 k a5 b5
      ⇒̇ ( appAt (sh5 T) c5 yc5
      ⇒̇ rel ))))))

  binClause-out : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ binClauseAt C T k rel ⟩
    → (c ar a b yc : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
    → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
    → ⟨ (yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
  binClause-out C T k rel γ h c ar a b yc c∈ shape hc =
    h c c∈ ar a b yc
      (subst ⟨_⟩ (sym (arityTagPairAtL-adequate c5 n5 k a5 b5 δ)) shape)
      (subst ⟨_⟩ (sym (appAt-adequate (sh5 T) c5 yc5 δ)) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ b ∷ a ∷ ar ∷ c ∷ γ

每个框架也向另一个方向读，而另一个方向才是实例要用的。消去是为「手上握着一个码」的消费方把子句拆开；引入是为「必须满足它」的一张表把子句装起来。两个框架都以一个 λ 引入，因为模型上的有界全称就是成员上的函数，而蕴含就是读式证明上的函数，故两者是同样几次代换倒着跑。

  binClause-in : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a b yc : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
       → ⟨ (yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
    → ⟨ γ ⊨ binClauseAt C T k rel ⟩
  binClause-in C T k rel γ g c c∈ ar a b yc sh hc =
    g c ar a b yc c∈
      (subst ⟨_⟩ (arityTagPairAtL-adequate c5 n5 k a5 b5 δ) sh)
      (subst ⟨_⟩ (appAt-adequate (sh5 T) c5 yc5 δ) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ b ∷ a ∷ ar ∷ c ∷ γ

数一数有几种形状是值得的，因为它说出那十二条里真正存在多少，也因为数错很容易：这一段已经错过两次。

诸框架只区分一件事：载荷是一个对，还是单个分量。对框架覆盖两个原子、三个联结词与两个有界量词，共七个；单分量框架覆盖否定、两个无界量词、以及那两个常量，共五个，因为常量的载荷是一个数码，而框架并不在意某个分量究竟是什么。故是两个框架，其上有十二条关系。

诸框架不可区分的，是那些载荷分量究竟是什么。按那个分组得到的是五种关系、而非五个框架：词项对词项、公式对公式、词项对公式、单个公式、以及处于下一元数的单个公式。那才是十二条真正分开的地方，而它们分在诸关系里，也就是查表所在之处。

单分量框架就是少一个绑定的对框架，读回来的方式相同。

  private
    sh4 : Fin n → Fin ( + n)
    sh4 i = suc (suc (suc (suc i)))

    c4 n4 a4 yc4 : Fin ( + n)
    c4  = suc (suc (suc zero))
    n4  = suc (suc zero)
    a4  = suc zero
    yc4 = zero

  unClauseAt : Fin n → Fin n → ℕ → Formula S ( + n) → Formula S n
  unClauseAt C T k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ (∀̇
      ( arityTagAtL c4 n4 k a4
      ⇒̇ ( appAt (sh4 T) c4 yc4
      ⇒̇ rel )))))

  unClause-out : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ unClauseAt C T k rel ⟩
    → (c ar a yc : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
    → ⟨ (yc ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
  unClause-out C T k rel γ h c ar a yc c∈ shape hc =
    h c c∈ ar a yc
      (subst ⟨_⟩ (sym (arityTagAtL-adequate c4 n4 k a4 δ)) shape)
      (subst ⟨_⟩ (sym (appAt-adequate (sh4 T) c4 yc4 δ)) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ a ∷ ar ∷ c ∷ γ

  unClause-in : (C T : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a yc : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))
       → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
       → ⟨ (yc ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
    → ⟨ γ ⊨ unClauseAt C T k rel ⟩
  unClause-in C T k rel γ g c c∈ ar a yc sh hc =
    g c ar a yc c∈
      (subst ⟨_⟩ (arityTagAtL-adequate c4 n4 k a4 δ) sh)
      (subst ⟨_⟩ (appAt-adequate (sh4 T) c4 yc4 δ) hc)
    where
    δ : S ^ ( + n)
    δ = yc ∷ a ∷ ar ∷ c ∷ γ

正的联结词

十二条里有两条现在就能写，而它们正是不需要本章尚未拥有之物的那两条。合取与析取把某码处的取值与它两个子码处的取值以交与并相关联，元数相同，而这就是它们的全部内容。

共用的部分是一条关系，它绑定两个子取值，并以查表为它们设防；剩下的就是那个运算，它谈论该码处的取值与两个子取值，位于位置二、一、零。故一条命题子句在共用部分之上只有一行。

蕴含与否定要补集，因而要该码元数处的全体环境之集，而本章尚未为它命名。它们等着。这处分界并不随意：它恰是「真值随其部分单调」的联结词与「不单调」的联结词之间的分界。

module _ {n : ℕ} where
  private
    sh7 : Fin n → Fin ( + n)
    sh7 i = suc (suc (suc (suc (suc (suc (suc i))))))

  c7 ar7 a7 b7 yc7 ya7 yb7 : Fin ( + n)
  c7  = suc (suc (suc (suc (suc (suc zero)))))
  ar7 = suc (suc (suc (suc (suc zero))))
  a7  = suc (suc (suc (suc zero)))
  b7  = suc (suc (suc zero))
  yc7 = suc (suc zero)
  ya7 = suc zero
  yb7 = zero

  propRel : Fin n → Formula S ( + n) → Formula S ( + n)
  propRel T op =
    ∀̇ (∀̇ ( subValAt (sh7 T) ar7 a7 ya7
         ⇒̇ ( subValAt (sh7 T) ar7 b7 yb7
         ⇒̇ op )))

  propClauseAt : Fin n → Fin n → ℕ → Formula S ( + n) → Formula S n
  propClauseAt C T k op = binClauseAt C T k (propRel T op)

  propClause-out : (C T : Fin n) (k : ℕ) (op : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ propClauseAt C T k op ⟩
    → (c ar a b yc ya yb : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
    → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
    → ⟨ pr (pr (fst ar) (fst a)) (fst ya) ∈ fst (lookup T γ) ⟩
    → ⟨ pr (pr (fst ar) (fst b)) (fst yb) ∈ fst (lookup T γ) ⟩
    → ⟨ (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ op ⟩
  propClause-out C T k op γ h c ar a b yc ya yb c∈ shape hc ha hb =
    binClause-out C T k (propRel T op) γ h c ar a b yc c∈ shape hc ya yb
      (subst ⟨_⟩ (sym (subValAt-adequate (sh7 T) ar7 a7 ya7 δ)) ha)
      (subst ⟨_⟩ (sym (subValAt-adequate (sh7 T) ar7 b7 yb7 δ)) hb)
    where
    δ : S ^ ( + n)
    δ = yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ

  propClause-in : (C T : Fin n) (k : ℕ) (op : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a b yc ya yb : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩
       → ⟨ pr (pr (fst ar) (fst a)) (fst ya) ∈ fst (lookup T γ) ⟩
       → ⟨ pr (pr (fst ar) (fst b)) (fst yb) ∈ fst (lookup T γ) ⟩
       → ⟨ (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ) ⊨ op ⟩)
    → ⟨ γ ⊨ propClauseAt C T k op ⟩
  propClause-in C T k op γ g =
    binClause-in C T k (propRel T op) γ
      (λ c ar a b yc c∈ sh hc ya yb ha hb →
        g c ar a b yc ya yb c∈ sh hc
          (subst ⟨_⟩
            (subValAt-adequate (sh7 T) ar7 a7 ya7 (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ)) ha)
          (subst ⟨_⟩
            (subValAt-adequate (sh7 T) ar7 b7 yb7 (yb ∷ ya ∷ yc ∷ b ∷ a ∷ ar ∷ c ∷ γ)) hb))

  andClauseAt : Fin n → Fin n → Formula S n
  andClauseAt C T = propClauseAt C T  (interAt yc7 ya7 yb7)

  orClauseAt : Fin n → Fin n → Formula S n
  orClauseAt C T = propClauseAt C T  (unionAt yc7 ya7 yb7)