---
title: "充足関係の節の読み取りと検証"
module: L.Coding.SatisfactionClauseSemantics
lang: ja
site: "Bedrock"
description: "充足関係の節の読み取りと検証"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 65
canonical: https://bedrock.institute/ja/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/zh/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)` を符号化します。以下の読み補題はこれらの対を順にほどき、構成子の関係が環境集合 `F` 上の候補値 `yc` の外延を述べられるようにします。

```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'` の外延条件の内向きの半分を適用します。

```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)` です。変数の場合は、`t=(#1,i)` かつグラフ要素 `(i,v)` が `z` に属する添字 `i` が単に存在します。任意の関係 `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 ∷ s ∷ δ` において対のアトム `q=(i,Vv)` が成り立つ証明だけです。スロット `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)` の所属が得られます。同時に `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∈
```

枠は、基礎の対が `(ar,F)` である塔の実際の要素 `qS` から始まります。新しい四つの枠には `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` について、`(c,yc)` が `T` に属するような値 `yc` が命題的に切り詰められて存在すると仮定します。`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` から出発します。その外向きの読み取りは、`e=(c,yc)` かつ `c` が `C` に属するような `c` と `yc` を、命題的切り詰めの下で復元します。したがって表の各要素の第一成分は指定された領域の符号ですが、分解の正準な選択も、一つの符号が値を一つしか持たないことも述べていません。

```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` に属するのは、`z` がアリティに対応する環境集合 `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` であり、その本体は `ya` と `yb` への所属を結合子 `op` で組み合わせます。

```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)` を開きます。これにより対のコンテナが加わり、古い枠の前に `b`、`a`、そのコンテナを置いた `δ15` が得られます。その後、入れ子になった二つの子の値の読み取りが左から右へ進むため、そこで隠される表の証人は外側の命題的切り詰めの内部に保たれます。

```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` はそれを、基礎の対が `(c₁,ya)` である `T` の実際の要素 `e₁S : S` として実現します。環境 `δ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
```

同じ構成により、二つ目の所属証明は、基礎の対が `(c₂,yb)` である実際の表の要素 `e₂S : S` として実現されます。二つ目の `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` は対 `(c₁,ya)` を実現する `T` の実際の要素で、一方のコンテナはその対を、もう一方は `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
```

逆に、鍵が `c₁=(ar',r)` と `ar'=suc A` を満たす実際の表の要素 `e'=(c₁,ya)` が、二つの対のコンテナのどの選び方に対しても必要な `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` の前提と正確に一致するため、`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 ψ` の要素が、`P` を満たす `envSet W n` の要素にちょうど一致すると述べます。ここでは `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` への所属と `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` で結ばれた一対の含意です。外向きの方向では、有界存在の切り詰められた証人を消去します。その証人は、子論理式の値に属する一つの項目と、その項目が `x` を古い環境の先頭に加えて得られるグラフであることを示す `consAtL` の証拠です。

```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` はここで、各符号化環境について原子の意味論的な値と `atomEx` を比較するよう `direct-extension` に求めます。その前向きの写像は `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 })
```

## まとめ

各節の内部意味論は、通常の充足関係と双方向に結びつきました。環境グラフが変数を解釈し、再帰的な橋渡しが論理構成子を扱い、原子式の橋渡しが項の値に沿って所属と等号を運びます。証明が用いるのは、符号化された表が述べる存在と外延性の事実だけであり、任意の表関係がすでに関数的であるとは仮定していません。