---
title: "部分符号で閉じた領域上で再帰を固定する"
module: L.Coding.PinnedRecursion
lang: ja
site: "Bedrock"
description: "部分符号で閉じた添字集合に固定された再帰"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 66
canonical: https://bedrock.institute/ja/L.Coding.PinnedRecursion.html
html: L.Coding.PinnedRecursion.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/PinnedRecursion.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Closure, L.Coding.EnvironmentSet, L.Coding.CodeConstructibility, L.Coding.CodeSet, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.SatisfactionTable, L.Coding.Quantification, L.Coding.EnvironmentTower, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.Coding.SatisfactionClauses, L.Coding.SatisfactionClauseSemantics]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.PinnedRecursion.md, https://bedrock.institute/zh/L.Coding.PinnedRecursion.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 部分符号で閉じた領域上で再帰を固定する

階層の符号からなる添字集合を固定し、認識された各構成子の形が要求する直下の論理式部分符号について閉じていると仮定します。さらに、台のスロット、タグの各スロット、環境の塔が標準的な意味をもち、表が完全な表仕様を満たすと仮定します。すると本章の前半は局所的な一意性を示します。既知の論理式のキーがその添字集合に属し、そのキーで表項目が与えられていれば、その項目の基礎集合は再帰的に定義された充足関係集合に等しくなります。後半は閉性を用いず、台、タグ、環境の塔、値の一致、復号、全域性、領域について明示された仮定から表の各節を組み立てます。どちらの向きも、大域的に選ばれた充足関係関数を与えるものではありません。

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

議論は、明示的に与えた排中律の実例に相対して進みます。古典論理は、導入済みの充足関係集合、環境集合、表の構成を支えますが、命題的切り詰めを取り除くわけではありません。復号された論理式や子論理式の表の値は、存在だけが分かる場合があります。

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

モジュールは宇宙レベルを固定し、古典的な仮定に名前を与えます。以下の各定理は、どのレベルの排中律の実例を消費するかを正確に記録します。

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

構造再帰は論理式文法の十個の構成子、すなわち所属と等号の原子論理式、連言、選言、含意、偽、二つの非有界量化子、`∀[]-syntax`、`∃[]-syntax` に沿って進みます。定数の付け替えにより、同じ構文木をまず台の要素からなるアルファベット上で読み、次に構成可能な台の上で読むことができ、構成子の形は変わりません。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇∈; ∀̇∈; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
```

論理式キーは、アリティと構文符号を集合論的な順序対で組み合わせたものです。この構成には、累積階層で直接行うものと、構成可能性の証明を伴って `L` の内部で行うものがあります。対、数項、論理式符号についての射影定理により、両者の基礎にある階層集合が一致することを示します。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.Model {ℓ} using ( module LCode; prʟ-fst; codeBridge )
```

閉性条件は、論理式の充足関係がもつ再帰的依存関係に正確に従います。二項結合子では同じアリティの二つの子論理式が、非有界量化子では後続アリティの本体が必要です。`∀[]-syntax` と `∃[]-syntax` では、後続アリティの論理式本体だけが必要です。後二者がもつ項の符号は節の内部で評価され、閉じた領域への所属を要求されません。

```agda
open import L.Coding.Expressions {ℓ} using ( consAtL )
open import L.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSuccAt; succSndAt; binSameClosed-out; unSuccClosed-out; binSuccClosed-out )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.CodeConstructibility {ℓ} using ( sglʟ; cupʟ; tree; tree-inv )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; AllCodes-out; keyS; codeS )
```

論理式 `ψ` に対し、`Sat` は再帰的に定義された、充足する環境の標準的な集合を与えます。一方、充足関係の表は符号化されたキーと値の対を格納します。定理は、そこに与えられた値を `Sat ψ` と比較します。表の全域性が子論理式の値を与えるのは命題的切り詰めのもとだけなので、その値を等式の証明には使えても、再利用可能な選択関数にはできません。

```agda
open import L.Coding.Satisfaction {ℓ} lem using
  ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.SatisfactionTable {ℓ} lem using
  ( keyʟ; slot; satTable; entry-out; inSlot; ent-slot ) renaming ( total to slotTotal )
```

零から九までのタグが十個の構成子の節を選びます。環境塔は各自然数アリティ `n` に対し、数項 `# n` と長さ `n` の符号化された環境集合との対を記録します。この二種類の座標により、節は構文上の構成子と、その充足関係集合を特徴づけるアリティの両方を認識できます。

```agda
open import L.Coding.Quantification {ℓ} using
  ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; sh; i0; i1; i2; i3; i4; i7; i8
  ; fstS; sndS; bigAnd-in; bigAnd-out )
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt; module TowerRead )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
```

表の仕様には三つの数学的な部分があります。領域の各キーには何らかの値があり、各表項目は領域に属するキーと値の対であり、十個の構成子はそれぞれの意味論的な節を満たします。節の意味論は最後の部分を外延に関する事実として読みます。候補の値と標準的な再帰値が環境集合上で同じ外延をもてば、外延性により両者の基礎となる階層集合が同一視されます。

```agda
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.Coding.SatisfactionClauses {ℓ} using ( tmIs; tableAt; module Clause; module Rel )
open import L.Coding.SatisfactionClauseSemantics {ℓ} lem using
  ( extB-out; extB-in; ExtFact; ext-unique; module Frame; module RelRead; module Bridge )
open import Cubical.Data.Nat using ( _+_ )
```

節の環境は有限ベクトルであり、枠を拡張すると以前の座標はすべてずれます。参照と移送によって、それらの座標を対応させ続けます。命題的切り詰めの内側に隠れた証人を消去する先は命題値の目標に限られます。固定の証明では基礎となる階層集合の等式へ、節を埋める証明では固定された対象言語の節の充足へ消去します。これらの消去から、再利用可能な値、復号結果、枠のデータが取り出されることはありません。

```agda
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

命題的切り詰めは、証人が存在することを保ちつつ、それがどの証人であったかを忘れます。したがって、その消去先は命題値でなければなりません。階層における所属は命題値であり、階層 `V` は h-集合なので、その二つの集合の等式も命題です。このため、以下で用いる消去の正当な行き先になります。

```agda
open PT using ( ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )
```

構成子タグは `Fin 10` の要素として格納されますが、構文符号では通常の自然数の数項を使います。写像 `toℕ` は上界の証明を忘れ、符号化された対に現れる数項の自然数を取り出します。元の上界により、現れうるタグは零から九までに限られます。

```agda
open import Cubical.Data.FinData using ( toℕ )
```

`L` 上の一階構造の台を `S` と書きます。`S` の要素は、基礎となる階層集合と、その構成可能性の証明からなります。本章の結論の多くは第一射影だけを比較します。充足関係に必要な数学的内容は、表される集合の等しさだからです。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

対象言語の節は、`L` が担う一階構造で解釈されます。したがって `γ ⊨ φ` は、その構造の有限環境 `γ` が論理式 `φ` を充足することを意味します。後の橋渡し補題は、この内部的な充足の主張を、外部で定義された集合 `SatW ψ` への所属と比較します。

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

## 鍵、タグ、復号された論理式を対応させる

まず、論理式のキーへの二つの経路を比較します。外側の経路は、アルファベットの記号を階層へ埋め込み、周囲の数項と対にします。内側の経路は、定数を構成可能な集合として付け替え、論理式を `L` の内部で符号化し、内部の数項と対にします。

```agda
module _ (A : S) where
  keyBridge : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n)
            → fst (keyS A ψ) ≡ fst (keyʟ (mapFo (asConst A) ψ))
  keyBridge {n} ψ =
      cong (pr (# n))
```

証明はまず構文符号の成分をそろえます。定数を付け替えてから外部の符号を取ることは、付け替えた論理式の内部符号を射影することと一致します。次にアリティの数項をそろえ、最後に内部の順序対を射影します。得られるパスは二つのキーの第一射影を結ぶものであり、付随する構成可能性の証明が定義的に同じだとは主張しません。

```agda
        ( cong (λ χ → VCode.⌜ χ ⌝) (sym (mapFo-comp (asConst A) fst ψ))
        ∙ sym (codeBridge (mapFo (asConst A) ψ)) )
    ∙ cong (λ w → pr w (fst LCode.⌜ mapFo (asConst A) ψ ⌝))
        (sym (numeralL-fst n))
    ∙ sym (prʟ-fst (numeralL n) LCode.⌜ mapFo (asConst A) ψ ⌝)
```

一致のモジュールは、一つの台 `W` に対して述べられます。そのアルファベットが、形を照合する項と論理式の構文を供給します。

```agda
module Match (W : S) where
  open Alphabet W
```

`MatchN` は、タグで索引づけられた形状の記録の族です。タグ 0 と 1 では、アトムの二つの項とその符号化された対を名指し、タグ 2 から 4 では、二項結合子の直接の部分論理式とその符号化された対を名指します。この族は、すでに知られている論理式で索引づけられるので、任意の集合の解析器ではありません。

```agda
  MatchN : ∀ {n} → ℕ → Formula Ab n → V ℓ → Type (ℓ-suc ℓ)
  MatchN {n} 0 ψ r = Σ[ t ∈ Term Ab n ] Σ[ u ∈ Term Ab n ] ((ψ ≡ t ∈̇ u) × (r ≡ pr (ct t) (ct u)))
  MatchN {n} 1 ψ r = Σ[ t ∈ Term Ab n ] Σ[ u ∈ Term Ab n ] ((ψ ≡ t ≐ u) × (r ≡ pr (ct t) (ct u)))
  MatchN {n} 2 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ∧̇ b) × (r ≡ pr (cd a) (cd b)))
  MatchN {n} 3 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ∨̇ b) × (r ≡ pr (cd a) (cd b)))
```

タグ四から八も同じ形の表を続けます。タグ四は含意と二つの論理式符号を、タグ五は数項零をペイロードとする偽を記録します。タグ六と七は二つの非有界量化子の後続アリティの本体を記録し、タグ八は `∀[]-syntax` の現在のアリティにおける項符号と後続アリティの本体を記録します。

```agda
  MatchN {n} 4 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ⇒̇ b) × (r ≡ pr (cd a) (cd b)))
  MatchN 5 ψ r = (ψ ≡ ⊥̇) × (r ≡ # 0)
  MatchN {n} 6 ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇ a) × (r ≡ cd a))
  MatchN {n} 7 ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇ a) × (r ≡ cd a))
  MatchN {n} 8 ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇∈ t a) × (r ≡ pr (ct t) (cd a)))
```

タグ九は `∃[]-syntax` に対応するペイロード、すなわち現在のアリティの項符号と後続アリティの論理式符号との対をもちます。この補助族は十以上の自然数タグでは空型です。したがって `MatchN` が記述するのは正確に十個の構成子形ですが、タグの等式に沿う移送を可能にするため、すべての自然数上で定義されています。

```agda
  MatchN {n} 9 ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇∈ t a) × (r ≡ pr (ct t) (cd a)))
  MatchN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ψ r = Empty.⊥*
```

輸送の補助は、一致の記録をタグとペイロードの間で変換します。対の単射性が符号化された対の等式をタグとペイロードの成分に分け、数項の単射性がタグの索引を運び、一致の記録がその両方に沿って置き換えられます。

```agda
  private
    at : ∀ {n} (ψ : Formula Ab n) (j k : ℕ) (r : V ℓ) → pr (# j) (cd ψ) ≡ pr (# j) (cd ψ)
       → MatchN j ψ r → (r' : V ℓ) → pr (# j) r ≡ pr (# k) r' → MatchN k ψ r'
    at ψ j k r _ mj r' e =
      subst2 (λ i x → MatchN i ψ x) (#-inj′ (pr-inj e .fst)) (pr-inj e .snd) mj
```

タグの読み手 `matchAt` は、任意の集合を復号するものではありません。すでに与えられた論理式から始まり、その論理式のコードがタグ付きの対と等しいことを述べ、一致の記録を返します。論理式についての場合分けがその固有のタグを露わにし、輸送の補助がそれを与えられたタグに付け替えます。

```agda
  matchAt : ∀ {n} (ψ : Formula Ab n) (k : ℕ) (r : V ℓ) → cd ψ ≡ pr (# k) r → MatchN k ψ r
  matchAt (t ∈̇ u) k r e = at (t ∈̇ u) 0 k _ refl (t , u , (refl , refl)) r e
  matchAt (t ≐ u) k r e = at (t ≐ u) 1 k _ refl (t , u , (refl , refl)) r e
  matchAt (a ∧̇ b) k r e = at (a ∧̇ b) 2 k _ refl (a , b , (refl , refl)) r e
  matchAt (a ∨̇ b) k r e = at (a ∨̇ b) 3 k _ refl (a , b , (refl , refl)) r e
```

残りの各式も探索は行いません。各構造の場合で、既知の構成子が標準的なタグとペイロードを直接与えます。含意は二つの子論理式符号を、偽は零を、二つの非有界量化子はそれぞれ本体の符号を、`∀[]-syntax` は項と本体の符号を与えます。その後、同じ移送補助が、これらの標準的なデータを入力の等式が指定するタグとペイロードに合わせます。

```agda
  matchAt (a ⇒̇ b) k r e = at (a ⇒̇ b) 4 k _ refl (a , b , (refl , refl)) r e
  matchAt ⊥̇ k r e = at ⊥̇ 5 k _ refl (refl , refl) r e
  matchAt (∃̇ a) k r e = at (∃̇ a) 6 k _ refl (a , (refl , refl)) r e
  matchAt (∀̇ a) k r e = at (∀̇ a) 7 k _ refl (a , (refl , refl)) r e
  matchAt (∀̇∈ t a) k r e = at (∀̇∈ t a) 8 k _ refl (t , a , (refl , refl)) r e
```

`∃[]-syntax` の標準的なタグは九であり、ペイロードは境界を表す項の符号と後続アリティの本体符号との対です。この最後の構造分岐により、`matchAt` はすべての論理式構成子を扱います。その結論は依然として、入力としてすでに与えられた論理式の形を記述するだけです。

```agda
  matchAt (∃̇∈ t a) k r e = at (∃̇∈ t a) 9 k _ refl (t , a , (refl , refl)) r e
```

いま `c` が標準的な符号集合に属し、アリティの数項 `# n` とペイロード `z` の対として表示されているとします。`AllCodes W` への所属からは、命題的切り詰めのもとで、あるアリティ `n₁`、そのアリティの論理式 `ψ₁`、そして `c` とそのキーとの等式が得られます。残る仕事は `n₁` を指定された `n` と一致させることです。

```agda
  decodeAll : (c : S) → ⟨ fst c ∈ fst (AllCodes W) ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z
            → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
  decodeAll c c∈ n z e = PT.map
    (λ { (n₁ , ψ₁ , e₁) →
      let q = pr-inj (sym e₁ ∙ e)
```

対符号化の単射性により、二つのアリティ数項と二つのペイロードがそれぞれ等しくなり、数項の単射性からパス `n₁ ≡ n` が得られます。この依存パスに沿って `ψ₁` を移送し、`cd-subst` でその符号を補正すると、アリティが正確に `n` で符号が `z` である論理式を得ます。結果は命題的切り詰めされたままなので、選ばれた復号器も、復号された論理式の一意性も与えません。

```agda
          nq = #-inj′ (q .fst)
      in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) })
    (AllCodes-out W c c∈)
```

## 部分符号で閉じた領域上の一意性

健全性の議論は、任意に与えた符号領域 `C` に局所化されています。候補となる表 `T` に加え、格納された台が `W` であること、十個のタグ位置が正しい数項をもつこと、環境の位置が正しい塔であること、`C` が必要な直下の論理式部分符号について閉じていること、そして `T` がまとめられた表の仕様を満たすことを仮定します。これらの仮定は、すべての論理式キーが `C` に属するとは述べません。

```agda
module SatSoundC {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (hcl : ⟨ γ ⊨ closedAt C ⟩)
  (hT : ⟨ γ ⊨ tableAt T w C E N ⟩) where
  open Alphabet W
```

表、符号領域、環境塔の各位置に格納された基礎階層集合を、それぞれ `Tv`、`Cv`、`Ev` と書きます。原子論理式では `Cv` における再帰的な参照は不要です。その項符号は原子論理式の橋渡しによって直接解釈されます。再帰呼出しが生じるのは、構成子が直下の子論理式をもつ場合だけです。

```agda
  open Bridge W
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
    Ev = fst (lookup E γ)
```

台 `W` の基礎階層集合を `Wv` と書きます。量化子の橋渡しはこの集合を量化の範囲として用い、原子論理式の橋渡しは同じ台が定めるアルファベット上で項の符号を解釈します。証明は値を階層集合として比較するので、固定の結論は第一射影の等式であり、`S` にある証明付きレコード全体の等式ではありません。

```agda
    Wv = fst W
```

環境塔は論理式のアリティに対応する行を与え、節の枠はその行を論理式キー、タグ付き符号、候補となる表の値と組み合わせます。この枠で構成子の節を読むと、候補の値をその要素によって特徴づける意味論的関係が現れます。

```agda
    module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
    module Fr = Frame T w C E N γ tg
    module Cl = Clause T w C E N
    module R = Rel T w N
```

まとめられた仮定 `hT` は、全域性、表項目のキーが `C` 上にあるという主張、十個の構成子の節の連言からなります。固定の証明は、全域性から子論理式の表項目を得て、構成子の節から値を特徴づけます。対象となる候補の表項目は命題に直接与えられているため、領域についての主張 `hOn` は包から取り出されますが、この一意性の議論では使われません。

```agda
    hTot = hT .fst
    hOn = hT .snd .fst
    hTen = hT .snd .snd
```

十個の構成子の節は、`Fin 10` で添字づけられた一つの有限連言として格納されています。読み手 `bigAnd-out` はこれを族 `cl k` に変えるので、各構造の場合は、ほかの九個の節を変更せずに、その構成子タグが指定する節だけを選べます。

```agda
    cl : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩
    cl = bigAnd-out γ 9 Cl.clause hTen
```

場合のモジュールは、一つの帰納の一歩のデータをまとめます。論理式、そのタグ、そのペイロードの集合、コードとペイロードの等式、コードの定義域の中でのキーの所属、候補の表の項目、そして項目の所属です。塔の読みが、論理式のアリティのための正準な塔の項目を供給します。

```agda
    module Case {n : ℕ} (ψ : Formula Ab n) (k : Fin 10) (rS : S)
      (ep : cd ψ ≡ pr (# (toℕ k)) (fst rS)) (c∈ : ⟨ fst (keyS W ψ) ∈ Cv ⟩)
      (y : S) (mem : ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩) where
      q∈ : ⟨ pr (# n) (fst (envSet W n)) ∈ Ev ⟩
      q∈ = TR.entry-in n
```

論理式符号は初め標準的な数項 `# k` を用いて書かれています。タグの等式によってこの数項を位置 `N k` に格納された値へ書き換えると、得られた等式は節の入力形式に合います。その後、枠 `δ12` は周囲の環境の前に十二個の座標を加えます。そこにはアリティの行、論理式キーと符号、ペイロード、候補の値が含まれます。

```agda
      ep' : fst (codeS W ψ) ≡ pr (fst (lookup (N k) γ)) (fst rS)
      ep' = ep ∙ cong (λ a → pr a (fst rS)) (sym (tg k))
      δ12 : S ^ (12 + m)
      δ12 = Fr.At.δ12 (nn n) (envSet W n) (keyS W ψ) (codeS W ψ) rS y q∈ refl k ep' mem
      rel : ⟨ δ12 ⊨ R.relN (toℕ k) ⟩
```

選んだ節をこの具体的な枠に適用すると、タグで添字づけられた関係 `relN k` の充足が得られます。次に関係の読み手を `δ12` に固定します。後の構成子別の読み手はこの同じ枠を拡張し、`rel` を原子論理式、二項結合子、量化子に適した外延の事実へ分解します。

```agda
      rel = Fr.clause-out k (cl k) (nn n) (envSet W n) (keyS W ψ) (codeS W ψ) rS y q∈ c∈ refl ep mem
      module RR = RelRead T w N δ12
```

子論理式のキーが `Cv` に属するなら、表の全域性から得られるのは、値 `ya` とそのキーにおける表項目との対を命題的切り詰めしたものだけです。したがって `sub` が証明するのは単なる存在であり、値を選ぶことではありません。各再帰の場合は、この証人を階層集合の等式へ直接消去し、h-集合構造によってその行き先が命題になります。

```agda
    sub : ∀ {n} (a : Formula Ab n) → ⟨ fst (keyS W a) ∈ Cv ⟩
        → ∥ Σ[ ya ∈ S ] ⟨ pr (fst (keyS W a)) (fst ya) ∈ Tv ⟩ ∥₁
    sub a a∈ = Fr.total-out hTot (keyS W a) a∈
```

中心的な述語は条件つきです。`ψ` のキーがコードの定義域にあれば、そのキーのもとで記録されたすべての表の値 `y` の底の集合は、`ψ` の再帰的な充足集合の底の集合と同じです。この条件つきの形が正直な形です。定義域の外のキーについては何も主張しません。

```agda
  Pinned : ∀ {n} (ψ : Formula Ab n) → Type (ℓ-suc ℓ)
  Pinned ψ = ⟨ fst (keyS W ψ) ∈ Cv ⟩
           → (y : S) → ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ → fst y ≡ fst (SatW ψ)
```

`Pinned` の証明は、与えられた論理式についての構造再帰として組み立てられます。再帰呼出しは、構文の構成子が直接与える子論理式にだけ行われます。`C` の要素についての再帰でも、任意の符号についての整礎再帰でもなく、論理式キーと同定されていない符号に値を定義する試みでもありません。

```agda
  private
```

符号化された論理式のペイロードの集合は、コードの等式から、対の射影によって復元されます。

```agda
    payS : ∀ {n} (ψ : Formula Ab n) (k : ℕ) (r : V ℓ) → cd ψ ≡ pr (# k) r → S
    payS ψ k r e = sndS (codeS W ψ) (# k) r e
```

三つの二項結合子は同じ再帰パターンを共有します。各パラメータは、構成子、タグとペイロードの等式、対応する対象言語の関係、意味論的な橋渡しを指定します。この橋渡しは、拡張された環境の二つの座標が二つの子論理式の標準的な充足関係集合に等しいという等式を仮定し、そこから複合論理式の標準値についての外延の事実を作ります。

```agda
    binCase : ∀ {n} (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
              (opA : Formula Ab n → Formula Ab n → Formula Ab n) (k : Fin 10)
              (a b : Formula Ab n) (code : cd (opA a b) ≡ pr (# (toℕ k)) (pr (cd a) (cd b)))
              (relIs : R.relN (toℕ k) ≡ R.binRel op)
              (bridge : ∀ {j} (env : S ^ j) (ya yb : Fin j)
```

橋渡しは、指定された座標に二つの子の値を含む環境について述べられます。別の閉性の読み手が、複合キーの `Cv` への所属から、同じアリティの二つの子キーの所属を取り出します。これにより、全域性がどの子表項目を与えても、再帰仮定によってそれぞれを `SatW a` と `SatW b` に同定できます。

```agda
                      → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
                      → ExtFact (fst (SatW (opA a b))) (fst (envSet W n))
                          (λ z → ⟨ (z ∷ env) ⊨ op (var i0 ∈̇ var (suc ya)) (var i0 ∈̇ var (suc yb)) ⟩))
            → (cl2 : ⟨ fst (keyS W (opA a b)) ∈ Cv ⟩
                   → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩)
```

複合論理式が固定されることを示すため、命題的切り詰めされた左の値、右の値、二項関係の証人を順に消去します。どの消去も、最終的には等式 `fst y ≡ fst (SatW (opA a b))` を目標とします。`V` は h-集合なのでこの等式は命題であり、消去によって子の値や枠のデータの恒久的な選択が残ることはありません。

```agda
            → Pinned a → Pinned b → Pinned (opA a b)
    binCase {n} op opA k a b code relIs bridge cl2 ia ib c∈ y mem =
      PT.rec (setIsSet _ _) (λ { (ya , ma) → PT.rec (setIsSet _ _) (λ { (yb , mb) →
        PT.rec (setIsSet _ _)
          (λ { (s , s₁ , e₁ , s₂ , e₂ , ext) →
```

二項関係の読み手は、二つの子論理式の符号、キー、値、および補助的な証人によって共通の節の枠を拡張します。この拡張環境では、節が候補 `y` の外延の事実を与え、橋渡しが `SatW (opA a b)` の対応する外延の事実を与えます。定理 `ext-unique` はこの二つの事実に集合の外延性を適用し、両者の基礎集合を等しくします。

```agda
            let env = yb ∷ keyS W b ∷ s₂ ∷ e₂ ∷ ya ∷ keyS W a ∷ s₁ ∷ e₁ ∷ codeS W b ∷ codeS W a ∷ s ∷ K.δ12
                P : S → Type (ℓ-suc ℓ)
                P z = ⟨ (z ∷ env) ⊨ R.binBody op ⟩
            in ext-unique y (SatW (opA a b)) (envSet W n) P ext
                 (bridge env i4 i0 (ia (cl2 c∈ .fst) ya ma) (ib (cl2 c∈ .snd) yb mb)) })
```

関係の読みは、節からタグの同一視を通して得られ、部分の値は表の全域性から、まず左の部分、次に右の部分の順で得られます。

```agda
          (K.RR.bin-out op (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel)
             (codeS W a) (codeS W b) (keyS W a) ya (keyS W b) yb refl ma refl mb refl) })
        (sub b (cl2 c∈ .snd)) })
        (sub a (cl2 c∈ .fst))
      where
```

局所モジュール `K` は、複合論理式そのもの、その構成子タグ、対になった子論理式符号のペイロードの構成可能な表現、複合キーの領域への所属、候補の表項目を記録します。これにより、二項の場合の議論全体に一つの具体的な節の枠が固定され、再帰仮定は二つの直下の子論理式だけに関わります。

```agda
      module K = Case (opA a b) k (payS (opA a b) (toℕ k) (pr (cd a) (cd b)) code) code c∈ y mem
```

二つの非有界量化子も一つの再帰の場合を共有します。本体は後続アリティをもち、ペイロードはその本体の符号だけです。意味論的な橋渡しは、固定された台の座標と、本体の表の値の座標を受け取ります。その値を `SatW a` と同定すると、橋渡しは `envSet W n` 上で量化された論理式の標準的な充足関係集合を特徴づけます。

```agda
    quCase : ∀ {n} (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
             (qA : Formula Ab (suc n) → Formula Ab n) (k : Fin 10)
             (a : Formula Ab (suc n)) (code : cd (qA a) ≡ pr (# (toℕ k)) (cd a))
             (relIs : R.relN (toℕ k) ≡ R.quRel q)
             (bridge : ∀ {j} (env : S ^ j) (wi yai : Fin j)
```

台の座標は元の周囲の環境に残り、枠を拡張した後は添字のずらしによって参照されます。子論理式の値は、関係の証人が新しく露わにする座標です。閉性から後続アリティの本体キーの所属が得られ、再帰仮定はそのキーにおけるすべての表項目を、本体の標準的な充足関係集合に同定します。これにより橋渡しは、対象言語の量化子を `Wv` 上の量化に正確に対応させます。

```agda
                     → fst (lookup wi env) ≡ Wv → fst (lookup yai env) ≡ fst (SatW a)
                     → ExtFact (fst (SatW (qA a))) (fst (envSet W n))
                         (λ z → ⟨ (z ∷ env) ⊨ q (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) ⟩))
           → (cl1 : ⟨ fst (keyS W (qA a)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩)
           → Pinned a → Pinned (qA a)
```

証明はまず命題的切り詰めされた本体の値を消去し、次に量化子関係の読み取りから得た命題的切り詰めされた証人を消去します。その証人は、後続の数項、本体キー、その値、補助座標によって共通の節の枠を拡張します。どちらの消去も、候補の値と標準的な量化された充足関係集合との等式を目標とするため、本体の値が大域的に選ばれることはありません。

```agda
    quCase {n} q qA k a code relIs bridge cl1 ia c∈ y mem =
      PT.rec (setIsSet _ _) (λ { (ya , ma) →
        PT.rec (setIsSet _ _)
          (λ { (s , s' , e' , ext) →
            let env = nn (suc n) ∷ s' ∷ ya ∷ keyS W a ∷ s ∷ e' ∷ K.δ12
```

拡張環境において、関係の節は候補の表の値 `y` に関する外延の事実を与えます。再帰仮定が橋渡しに必要な等式を与え、橋渡しは、ずらされた台の座標における等式を使って、`SatW (qA a)` に対応する外延の事実を与えます。最後に `ext-unique` の集合外延性が二つの基礎集合を同定します。

```agda
                P : S → Type (ℓ-suc ℓ)
                P z = ⟨ (z ∷ env) ⊨ R.quBody q ⟩
            in ext-unique y (SatW (qA a)) (envSet W n) P ext (bridge env (sh 18 w) i2 qw (ia (cl1 c∈) ya ma)) })
          (K.RR.qu-out q (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) (keyS W a) ya (nn (suc n)) ma refl refl) })
        (sub a (cl1 c∈))
```

ここで `K` が具体化されるのは、量化された論理式 `qA a` であり、その本体 `a` ではありません。ペイロードの表現は本体の符号から作られますが、領域への所属と候補の表項目は量化された論理式のキーに属します。本体は、後続アリティにある唯一の再帰的な子論理式として別に現れます。

```agda
      where
      module K = Case (qA a) k (payS (qA a) (toℕ k) (cd a) code) code c∈ y mem
```

有界量化子の構成子符号には二つのペイロード成分があります。境界を与える項の符号と、アリティが一つ大きい本体論理式の符号です。そこでこの場合の補題は、構成子のタグとペイロードの等式、対応する関係の節、五つのスロットで固定して表した意味論的本体、その本体に対する外延の橋、そして後で実際に必要となる唯一の閉性の含意を仮定します。その含意は、複合論理式の鍵が領域に属すれば本体の鍵も領域に属すというものです。項の符号について領域の閉性は仮定しません。

```agda
    bqCase : ∀ {n} (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
             (c : ∀ {j} → Formula S j → Formula S j → Formula S j)
             (qA : Term Ab n → Formula Ab (suc n) → Formula Ab n) (k : Fin 10)
             (t : Term Ab n) (a : Formula Ab (suc n)) (code : cd (qA t a) ≡ pr (# (toℕ k)) (pr (ct t) (cd a)))
             (relIs : R.relN (toℕ k) ≡ R.bqRel q c)
```

本体の等式は、有界量化子の本体が五つのずらした枠でどのように綴られるかを記録します。これにより、橋を、呼び出し側の正確な枠の添字に依存しない固定された論理式の形で述べられます。

```agda
             (body : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S (1 + j))
             (bodyIs : ∀ {j} (wi ti yai N0i N1i : Fin j)
                     → body wi ti yai N0i N1i
                     ≡ q (var (suc wi)) (c (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)))
                         (q (var (suc (suc wi))) (c (var i0 ∈̇ var i1) (∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3))))))
```

この橋は、有界論理式について再帰的に定めた充足集合を、符号化された環境上で五つのスロットをもつ意味論的本体が記述する外延と対応させます。ここでは量化子と結合子がまだパラメータなので、同じ主張が有界全称の場合と有界存在の場合の両方を扱います。したがって、すべての場合にある要素の存在を主張していると読んではいけません。証明では、この外延事実を表の節から読み取った外延事実と比較します。

```agda
             (bridge : ∀ {j} (env : S ^ j) (wi ti yai N0i N1i : Fin j)
                     → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup yai env) ≡ fst (SatW a)
                     → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1
                     → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ body wi ti yai N0i N1i ⟩))
           → (cl1 : ⟨ fst (keyS W (qA t a)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩)
```

複合論理式の鍵が領域に属すことから本体の鍵が領域に属すことが従い、さらに本体の鍵にある表の値がすでに固定されていると仮定します。このとき、複合論理式の鍵に与えられた任意の表の値も固定されます。全域性が与える本体の値は単に存在するだけであり、有界量化子の節の読み出しもその証人を命題的切り詰めの内側に置きます。結論は階層の基礎集合どうしの等式であり命題なので、ここではその両方を消去できます。一方、複合論理式の表の値は結論の前提として直接与えられており、全域性から得るものでも、切り詰めの内側にあるものでもありません。

```agda
           → Pinned a → Pinned (qA t a)
    bqCase {n} q c qA k t a code relIs body bodyIs bridge cl1 ia c∈ y mem =
      PT.rec (setIsSet _ _) (λ { (ya , ma) →
        PT.rec (setIsSet _ _)
          (λ { (s , s₁ , s' , e' , ext) →
```

節の証人を読み取った後、証明は後続アリティ、本体の表の値と鍵、本体の符号、そして境界を与える項の符号を含む拡張環境を組み立てます。その同じ環境で、`ext-unique` は二つの外延事実を比較します。一方は候補となる表の値を特徴づける節の外延事実であり、他方は再帰的な充足集合を特徴づける橋の外延事実です。本体の等式に沿って運ぶことで、両者に現れる述語が一致します。

```agda
            let env = nn (suc n) ∷ s' ∷ ya ∷ keyS W a ∷ s₁ ∷ e' ∷ codeS W a ∷ tS ∷ s ∷ K.δ12
                P : S → Type (ℓ-suc ℓ)
                P z = ⟨ (z ∷ env) ⊨ R.bqBody q c ⟩
            in ext-unique y (SatW (qA t a)) (envSet W n) P ext
                 (subst (λ φ → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))
```

まず閉性から本体の鍵が領域に属すことを得て、次に帰納仮定によって、全域性から得た本体の表の値を再帰的な充足集合と同定します。この同定と、台、項の符号、二つのタグに関する等式を合わせると、橋の仮定がすべて満たされます。有界量化子の節を外向きに読むと、四つの補助的な対象と一つの外延事実が得られますが、それらはこの局所的な比較にだけ使われます。

```agda
                    (bodyIs (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)))
                    (bridge env (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)) qw refl (ia (cl1 c∈) ya ma) (tg f0) (tg f1))) })
          (K.RR.bq-out q c (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) tS (codeS W a) (keyS W a) ya (nn (suc n)) refl ma refl refl) })
        (sub a (cl1 c∈))
      where
```

名づけられた三つの成分がこの場合を支えます。台の要素として提示されたペイロード、項の符号を載せる第一の射影、そして、合成キーでの表の項目をもつ十二の枠のフレームを供給する場合のモジュールです。

```agda
      rS : S
      rS = payS (qA t a) (toℕ k) (pr (ct t) (cd a)) code
      tS : S
      tS = fstS rS (ct t) (cd a) refl
      module K = Case (qA t a) k rS code c∈ y mem
```

原子論理式には論理式としての子がないので、この場合には閉性の含意も再帰仮定も要りません。構成子のペイロードは二つの項の符号の対です。残りの仮定は、対応する原子関係の節を同定し、台の等式、二つの項の符号の等式、二つのタグの等式から、原子論理式の再帰的な充足集合についての外延事実を与える橋を用意します。

```agda
    atomCase : ∀ {n} (opA : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j) (k : Fin 10)
               (t u : Term Ab n) (code : cd (opA t u) ≡ pr (# (toℕ k)) (pr (ct t) (ct u)))
               (rel : Formula S (18 + m))
               (relIs : R.relN (toℕ k) ≡ R.atomRel rel)
               (bridge : ∀ (env : S ^ (15 + m)) (wi ti ui N0i N1i : Fin (15 + m))
```

橋のパラメータは原子論理式の外延事実を述べます。充足関係集合には、項の値が対象言語の関係を満たす環境がちょうど含まれます。結論は、この原子論理式のキーが領域に属し、表項目が与えられていれば、その論理式が固定されることを述べます。

```agda
                       → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup ui env) ≡ ct u
                       → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1
                       → ExtFact (fst (SatW (opA t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ atomEx wi ti ui N0i N1i rel ⟩))
             → Pinned (opA t u)
    atomCase {n} opA k t u code rel relIs bridge c∈ y mem =
```

原子の節からは、補助的な集合と候補となる表の値についての外延事実が、単なる存在として得られます。その集合と二つの項の符号から作った環境では、原子の橋が再帰的な充足値について第二の外延事実を与えます。累積階層の等式は命題なので、節の隠された証人を消去でき、`ext-unique` によって二つの基礎集合が同定されます。

```agda
      PT.rec (setIsSet _ _)
        (λ { (s , ext) →
          let env = uS ∷ tS ∷ s ∷ K.δ12
              P : S → Type (ℓ-suc ℓ)
              P z = ⟨ (z ∷ env) ⊨ R.atomBody rel ⟩
```

橋は、拡張された環境で、二つのタグの等式と台の等式とともに適用され、原子の本体の外延の事実を作ります。原子の関係の外向きの読み出しが、中間の集合を供給します。

```agda
          in ext-unique y (SatW (opA t u)) (envSet W n) P ext
               (bridge env (sh 15 w) i1 i0 (sh 15 (N f0)) (sh 15 (N f1)) qw refl refl (tg f0) (tg f1)) })
        (K.RR.atom-out rel (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) tS uS refl)
      where
      rS : S
```

名づけられた三つの成分が原子の場合を支えます。台の要素としてのペイロード、その第一と第二の射影としての二つの項の符号、そして十二の枠のフレームを供給する場合のモジュールです。

```agda
      rS = payS (opA t u) (toℕ k) (pr (ct t) (ct u)) code
      tS uS : S
      tS = fstS rS (ct t) (ct u) refl
      uS = sndS rS (ct t) (ct u) refl
      module K = Case (opA t u) k rS code c∈ y mem
```

この所属原子では、表示された環境における充足は、二つの基礎集合の間の所属命題と定義上同じです。したがって `memAgree` の二つの向きはいずれも恒等写像です。これは原子の橋がこの箇所で必要とする局所的な一致であり、ほかの関係記号については何も主張しません。

```agda
    memAgree : ∀ {j} (env : S ^ j) (z v x : S)
             → (⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ∈̇ var i0 ⟩ → ⟨ fst v ∈ fst x ⟩) × (⟨ fst v ∈ fst x ⟩ → ⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ∈̇ var i0 ⟩)
    memAgree env z v x = (λ h → h) , (λ h → h)
```

等号の一致は、等号の原子についても同じことを言います。対象言語の等号は、基礎の集合の同一性です。

```agda
    eqAgree : ∀ {j} (env : S ^ j) (z v x : S)
            → (⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ≐ var i0 ⟩ → fst v ≡ fst x) × ((fst v ≡ fst x) → ⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ≐ var i0 ⟩)
    eqAgree env z v x = (λ h → h) , (λ h → h)
```

二項の結合子のための閉じの補題は、形の充足から下向きの閉じを読み出します。合成キーが領域にあれば、両方の成分キーも領域にある、というものです。証明は、二項の閉じの消去を一度適用するだけです。

```agda
    clSame : (n k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
           → (ψ a b : Formula Ab n) → cd ψ ≡ pr (# k) (pr (cd a) (cd b))
           → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩
    clSame n k h ψ a b e c∈ =
      binSameClosed-out C k γ h (keyS W ψ) (nn n) (codeS W a) (codeS W b) c∈ (cong (pr (# n)) e)
```

次の形の二項閉性補題では、形の証明を受け取る前に二つの子論理式を固定します。結論は変わりません。ペイロードがその二つの論理式の符号の対である鍵が領域に属すれば、両方の子の鍵も領域に属します。この引数順序により、構造再帰の各分岐は共通の閉性の事実を自分の二つの子に特殊化できます。

```agda
    clBin : (n k : ℕ) (a b : Formula Ab n)
          → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
          → (ψ : Formula Ab n) → cd ψ ≡ pr (# k) (pr (cd a) (cd b))
          → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩
    clBin n k a b h ψ e = clSame n k h ψ a b e
```

非有界量化子では、閉性は構成子のペイロードに含まれる唯一の論理式成分だけをたどります。したがって、アリティ `n` の量化された論理式の鍵が領域に属すれば、後続アリティにある本体の鍵も領域に属します。この主張は、ここで提示された構成子符号に局所的なものであり、領域の任意の要素を復号するものではありません。

```agda
    clQu : (n k : ℕ) (a : Formula Ab (suc n)) (ψ : Formula Ab n)
         → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → cd ψ ≡ pr (# k) (cd a)
         → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩
    clQu n k a ψ h e c∈ =
      unSuccClosed-out C k γ h (keyS W ψ) (nn n) (codeS W a) c∈ (cong (pr (# n)) e)
```

有界量化子のペイロードでは、第一成分が項の符号、第二成分が本体論理式の符号です。閉性の条件がたどるのは第二成分だけであり、複合論理式の鍵が領域に属すことから、後続アリティにある本体の鍵が領域に属すことを導きます。境界を与える項の符号について、領域への所属は意図的に何も結論しません。

```agda
    clBq : (n k : ℕ) (t : Term Ab n) (a : Formula Ab (suc n)) (ψ : Formula Ab n)
         → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → cd ψ ≡ pr (# k) (pr (ct t) (cd a))
         → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩
    clBq n k t a ψ h e c∈ =
      binSuccClosed-out C k γ h (keyS W ψ) (nn n) tS (codeS W a) c∈ (cong (pr (# n)) e)
```

名づけられた二つの成分が、有界量化子のための閉じを支えます。台の要素として提示されたペイロードと、項の符号を載せるその第一の射影です。

```agda
      where
      pS : S
      pS = sndS (codeS W ψ) (# k) (pr (ct t) (cd a)) e
      tS : S
      tS = fstS pS (ct t) (cd a) refl
```

釘づけの述語は、論理式の構造についての構造再帰で証明されます。所属の原子は、所属の関係に対する恒等の一致とともに原子の場合を適用し、下位の論理式の仮定を一切消費しません。

```agda
  pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ
  pinned (t ∈̇ u) = atomCase _∈̇_ f0 t u refl (var i1 ∈̇ var i0) refl
    (λ env wi ti ui N0i N1i qw' qt qu q0 q1 →
      AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _∈̇_ (λ v x → ⟨ v ∈ x ⟩)
        (var i1 ∈̇ var i0) (memAgree env) (λ δ h → h) (λ δ h → h))
```

等号の原子は、等号に対する恒等の一致とともに原子の場合を適用します。連言の場合は、連言の橋とタグ二での二項の閉じとともに二項の場合を適用し、二つの下位の論理式の釘づけの仮定を消費します。

```agda
  pinned (t ≐ u) = atomCase _≐_ f1 t u refl (var i1 ≐ var i0) refl
    (λ env wi ti ui N0i N1i qw' qt qu q0 q1 →
      AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _≐_ (λ v x → v ≡ x)
        (var i1 ≐ var i0) (eqAgree env) (λ δ h → h) (λ δ h → h))
  pinned {n} (a ∧̇ b) = binCase _∧̇_ _∧̇_ f2 a b refl refl (andBridge a b) (clBin n 2 a b (hcl .fst) (a ∧̇ b) refl) (pinned a) (pinned b)
```

選言と含意は、それぞれのタグで同じ二項のパターンに従います。偽には下位の論理式がなく、その一意性は、偽の条項の外向きの読み出しと偽の橋から直接証明されます。両方が合わせて空の外延を作るからです。

```agda
  pinned {n} (a ∨̇ b) = binCase _∨̇_ _∨̇_ f3 a b refl refl (orBridge a b) (clBin n 3 a b (hcl .snd .fst) (a ∨̇ b) refl) (pinned a) (pinned b)
  pinned {n} (a ⇒̇ b) = binCase _⇒̇_ _⇒̇_ f4 a b refl refl (impBridge a b) (clBin n 4 a b (hcl .snd .snd .fst) (a ⇒̇ b) refl) (pinned a) (pinned b)
  pinned {n} ⊥̇ c∈ y mem = ext-unique y (SatW ⊥̇) (envSet W n) (λ z → ⟨ (z ∷ K.δ12) ⊨ ⊥̇ ⟩) (extB-out i0 i8 ⊥̇ K.δ12 K.rel) (botBridge n K.δ12)
    where
    module K = Case ⊥̇ f5 (nn 0) refl c∈ y mem
```

二つの非有界量化子の分岐は、それぞれ存在の橋と全称の橋を使います。閉性によって量化された論理式の鍵から後続アリティの本体の鍵へ領域への所属を移し、再帰仮定によって橋が必要とする本体の値を固定します。有界全称の分岐も同じ局所的な形を取りますが、その構成子符号には項の符号も含まれます。この分岐は全称の `∀[]-syntax` の橋を用いて有界の場合を適用し、閉性はここでも本体だけをたどります。

```agda
  pinned {n} (∃̇ a) = quCase ∃̇∈ ∃̇_ f6 a refl refl (exBridge a) (clQu n 6 a (∃̇ a) (hcl .snd .snd .snd .fst) refl) (pinned a)
  pinned {n} (∀̇ a) = quCase ∀̇∈ ∀̇_ f7 a refl refl (allBridge a) (clQu n 7 a (∀̇ a) (hcl .snd .snd .snd .snd .fst) refl) (pinned a)
  pinned {n} (∀̇∈ t a) = bqCase ∀̇∈ _⇒̇_ ∀̇∈ f8 t a refl refl bqAll (λ _ _ _ _ _ → refl)
    (λ env wi ti yai N0i N1i qw' qt qa q0 q1 → BqBridge.allInBridge t a env wi ti yai N0i N1i qw' qt qa q0 q1)
    (clBq n 8 t a (∀̇∈ t a) (hcl .snd .snd .snd .snd .snd .fst) refl) (pinned a)
```

有界存在の分岐は、存在の `∃[]-syntax` の橋を用いて有界の場合を適用します。対応する閉性の成分が与えるのは、後続アリティにある本体の鍵の領域への所属だけであり、その後で再帰仮定が本体の表の値を固定します。境界を与える項は橋の中で評価され、別の再帰部分問題にはなりません。

```agda
  pinned {n} (∃̇∈ t a) = bqCase ∃̇∈ _∧̇_ ∃̇∈ f9 t a refl refl bqEx (λ _ _ _ _ _ → refl)
    (λ env wi ti yai N0i N1i qw' qt qa q0 q1 → BqBridge.exInBridge t a env wi ti yai N0i N1i qw' qt qa q0 q1)
    (clBq n 9 t a (∃̇∈ t a) (hcl .snd .snd .snd .snd .snd .snd) refl) (pinned a)
```

## すべての充足関係の節を満たす

ここから逆向きの接続を証明します。節から再帰的な値を取り出すのではなく、表に表示された値がすでに再帰的に定めた充足集合と一致すると仮定し、その一致を使って各節を検証します。作業集合 `W` は、この向きで一貫して使うアルファベット、充足の橋、構成子符号の照合を定めます。

```agda
module _ (W : S) where
  open Alphabet W
  open Bridge W
  open Match W
```

一つの環境の中で、表、台、論理式符号の領域、環境の塔の各スロットを固定し、十個の数項タグと塔の仕様を与えます。中心となる仮定 `val≡` は条件付きです。既知の論理式の鍵と、その鍵にある与えられた表の要素に対して、その要素の基礎の値を論理式の再帰的な充足集合と同定します。すべての鍵が表されるとは主張せず、表の要素を選ぶこともしません。

```agda
  module SatHoldsC {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
    (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
    (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩)
    (val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ)
          → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩ → fst yc ≡ fst (SatW ψ))
```

さらに三つの仮定は、命題的切り詰めの下でのみ存在を与えます。領域の要素がアリティ符号とペイロードの対として提示されると、指定されたそのアリティの論理式へ単に復号できるだけです。全域性は各領域の鍵にある何らかの表の値を単に与え、表の各要素も、鍵が領域に属す鍵と値の対へ単に分解されます。これらの仮定はいずれも、再利用できる復号関数や値の選択関数を定めません。

```agda
    (decode : (c : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → (n : ℕ) (z : V ℓ)
            → fst c ≡ pr (# n) z → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁)
    (tot : (c : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩
         → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩ ∥₁)
    (onc : (e : S) → ⟨ fst e ∈ fst (lookup T γ) ⟩
```

最後の仮定は領域条件を完成させます。表に表示された各要素は、指定された符号領域に `c` が属すような対 `(c,yc)` として、単に存在するものとして同定されます。したがって全域性は鍵から値への向きを制御し、この条件は表の要素から領域の鍵へ戻る向きを制御します。略記 `Tv` と `Cv` は、これらの局所的な主張で使う表と領域の基礎集合を名づけるだけです。

```agda
         → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ fst (lookup C γ) ⟩) ∥₁)
    where
    private
      Tv = fst (lookup T γ)
      Cv = fst (lookup C γ)
```

さらに、環境の塔の基礎集合と台を名づけます。枠、節、関係の読み出しは、同じ格納データを三つの尺度で表します。十二個の対象からなる共通の枠、表の最上位の条件、そして構成子ごとの関係です。これらは固定された環境の局所的な見方であり、新しい数学的仮定ではありません。

```agda
      Ev = fst (lookup E γ)
      Wv = fst W
      module Fr = Frame T w C E N γ tg
      module Cl = Clause T w C E N
      module R = Rel T w N
```

`Arity ar F` は、ある自然数 `n` が単に存在し、`ar` が `n` の数項であり、`F` が対応する符号化環境の集合 `envSet W n` であることを述べます。証人 `n` は命題的切り詰めの内側に留まるので、この型は命題値の証明に必要なアリティ情報を記録するだけで、後の計算に使うアリティを選びません。

```agda
      Arity : (ar F : S) → Type (ℓ-suc ℓ)
      Arity ar F = ∥ Σ[ n ∈ ℕ ] ((fst ar ≡ # n) × (fst F ≡ fst (envSet W n))) ∥₁
```

このアリティの証拠を得るには、環境の塔の要素 `q` を対 `(ar,F)` として提示します。すると塔の仕様に、台の等式と零タグの等式を合わせることで、その対から、単に存在する自然数アリティとその正準な環境集合を読み取れます。

```agda
      arity : (q ar F : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F) → Arity ar F
      module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
```

対の等式によって、`q` の所属証明を表示された対 `(ar,F)` へ運びます。続いて塔の要素に関する定理が、命題的切り詰めの内側にあるまま `Arity ar F` を返します。この段階で取り出すのは現在の要素に必要な局所的アリティ証拠だけであり、塔の符号化に対する大域的な逆関数は定めません。

```agda
      arity q ar F q∈ eq = TR.entry-out ar F (subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈)
```

表に対する第一の最上位条件は、指定された論理式符号の領域上での全域性です。仮定 `tot` はすでにその意味内容を正確に与えており、各値は単に存在するだけです。そこで枠の補題は、この仮定を対象言語の全域性の節が充足されることへ直接変換します。

```agda
      total : ⟨ γ ⊨ Cl.total ⟩
      total = Fr.total-in tot
```

第二の最上位条件は、表に表示された各要素が、指定された領域の鍵の上にあることを述べます。仮定 `onc` は基礎集合の水準でまさにこの条件を表すので、枠の補題によって対応する対象言語の節の充足へ変換できます。

```agda
      onC : ⟨ γ ⊨ Cl.onC ⟩
      onC = Fr.onC-in onc
```

各構成子の節は、同じ十二対象の配置について検証されます。最初のフィールド群はそれらの対象を記録します。すなわち、塔の要素とそのアリティおよび環境集合、論理式符号の領域の要素とその構成子ペイロード、表の要素とその値、そして対象言語の論理式が必要とする補助的な証人です。

```agda
      record Args (k : Fin 10) : Type (ℓ-suc ℓ) where
        field
          q ar F s c p s1 r s2 e yc s3 : S
          q∈ : ⟨ fst q ∈ Ev ⟩
          eq : fst q ≡ pr (fst ar) (fst F)
```

残りのフィールドは、それらの対象を一つの整合した枠にする関係を述べます。塔の要素がアリティと環境集合の対であること、論理式の符号が領域に属してアリティ、タグ、ペイロードへ分かれること、そして表の要素が表に属してその符号と候補値へ分かれることです。これらは局所的な表示の等式であり、一意性や大域的な復号を主張しません。

```agda
          c∈ : ⟨ fst c ∈ Cv ⟩
          ec : fst c ≡ pr (fst ar) (fst p)
          ep : fst p ≡ pr (# (toℕ k)) (fst r)
          e∈ : ⟨ fst e ∈ Tv ⟩
          ee : fst e ≡ pr (fst c) (fst yc)
```

一つのタグと、整合した十二対象の枠を固定すると、問題は一つの構成子の節を検証することに絞られます。この範囲で後に行う議論はすべて同じ対象と等式を使うので、そのタグのペイロードが必要な外延事実をどのように定めるかに集中できます。

```agda
      module Fill (k : Fin 10) (A : Args k) where
        open Args A
```

枠は、節の論理式が要求する正確な座標順に、十二個の対象 `yc`、`s3`、`e`、`r`、`s2`、`p`、`s1`、`c`、`F`、`ar`、`s`、`q` を元の環境 `γ` の前へ加えます。したがって、候補値、表項目、構成子のペイロード、論理式符号、環境集合、アリティ、塔の項目は四つの補助的な証人を間に挟みながら、節が用いる添字に正確に置かれます。

```agda
        frame : S ^ (12 + m)
        frame = yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ
```

この固定された枠では、タグに対応する関係の定理を、その意味論的な外延条件と対象言語の関係の節との間で双方向に使えます。充足を組み立てる証明が使うのは構成する向きです。復号されたペイロードとあらかじめ定められた子の値から正しい外延事実が得られれば、そのタグの関係の節が従います。

```agda
        module RR = RelRead T w N frame
```

それぞれの充填の場合の目標は、十二の枠のフレームで、与えられたタグに対する関係の条項の充足です。

```agda
        Goal : Type (ℓ-suc ℓ)
        Goal = ⟨ frame ⊨ R.relN (toℕ k) ⟩
```

この目標は命題値です。この構造における任意の論理式の充足が h-命題だからです。これが後で使う命題的切り詰めの正確な消去境界になります。単に復号されたアリティ、論理式、構成子の形は、この目標を証明するためには使えますが、再利用可能な計算データとして取り出すことはできません。

```agda
        isPropGoal : isProp Goal
        isPropGoal = snd (frame ⊨ R.relN (toℕ k))
```

移行の補題が重要なステップです。アリティの等式、環境集合の等式、論理式符号の等式 `fst p ≡ cd ψ`、そして `ψ` の充足関係集合についての外延事実が与えられると、枠にある表の値について対応する外延事実を作ります。この三つの等式は、枠のアリティ、環境集合、論理式符号の対象を、再帰的な充足関係集合が用いるデータにそろえます。

```agda
        transfer : (n : ℕ) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
                 → fst p ≡ cd ψ → {j : ℕ} (env : S ^ j) (φ : Formula S (1 + j))
                 → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)
                 → RR.Ext env φ
        transfer n ψ qa qF qp env φ ext =
```

まず枠の等式から、`c` が復号された論理式の正準な鍵であり、与えられた表の要素が `c` と `yc` の対であることを示します。すると値の一致の仮定により、`yc` の基礎集合が再帰的な充足集合と同定されます。最後に、その値の等式を逆向きに用い、さらに `F` を正準な環境集合と同定する等式に沿って運ぶことで、橋の外延事実を枠が要求する外延事実へ変換します。

```agda
          subst2 (λ Y F' → ExtFact Y F' (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))
            (sym (val≡ ψ c yc (ec ∙ cong₂ pr qa qp) (subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈))) (sym qF) ext
```

下位の値の補題は、同じアリティの子の項目に、値の一致の仮定を適用します。子の表の項目から充足集合を復元するのです。

```agda
        subVal : (n : ℕ) (a : Formula Ab n) (c₁ ya e₁ : S) → fst ar ≡ # n
               → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar) (cd a)
               → fst ya ≡ fst (SatW a)
        subVal n a c₁ ya e₁ qa e₁∈ ee₁ e₁' =
          val≡ a c₁ ya (e₁' ∙ cong (λ v → pr v (cd a)) qa) (subst (λ u → ⟨ u ∈ Tv ⟩) ee₁ e₁∈)
```

量化子の本体では、子の鍵は後続アリティにあります。追加の等式は、そのアリティ成分 `ar'` を親のアリティ成分のフォン・ノイマン後続と同定します。これを `ar = # n` と合成すると `suc n` の数項が得られます。したがって値の一致の仮定により、子の表の値を本体の再帰的な充足集合と同定できます。これはアリティの計算であり、構成可能階層の段階についての主張ではありません。

```agda
        subValS : (n : ℕ) (a : Formula Ab (suc n)) (c₁ ya e₁ ar' : S) → fst ar ≡ # n
                → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar') (cd a) → fst ar' ≡ sucV (fst ar)
                → fst ya ≡ fst (SatW a)
        subValS n a c₁ ya e₁ ar' qa e₁∈ ee₁ e₁' es =
          val≡ a c₁ ya (e₁' ∙ cong (λ v → pr v (cd a)) (es ∙ cong sucV qa)) (subst (λ u → ⟨ u ∈ Tv ⟩) ee₁ e₁∈)
```

データの型は、復号されたアリティ、環境の集合、論理式、そしてタグの照合を集めます。構成子の場合を振り分けるために必要なすべてです。

```agda
        Data : Type (ℓ-suc ℓ)
        Data = Σ[ n ∈ ℕ ] ((fst ar ≡ # n) × ((fst F ≡ fst (envSet W n))
                 × (Σ[ ψ ∈ Formula Ab n ] ((fst p ≡ cd ψ) × MatchN (toℕ k) ψ (fst r)))))
```

`data'` の証拠は、全体を通して命題的切り詰めの内側に留まります。まず塔の要素が、あるアリティとその環境集合を単に与えます。その各証人に対して、`decode` はそのアリティのある論理式を単に与え、`PT.map` が `matchAt` から得た構成子の形の証明を付け加えます。外側の消去先も再び切り詰められた型なので、アリティや論理式が大域的に選ばれることはありません。

```agda
        data' : ∥ Data ∥₁
        data' = PT.rec squash₁
          (λ { (n , (qa , qF)) → PT.map
            (λ { (ψ , qp) → n , (qa , qF , ψ , (qp , matchAt ψ (toℕ k) (fst r) (sym qp ∙ ep))) })
            (decode c c∈ n (fst p) (ec ∙ cong (λ v → pr v (fst p)) qa)) })
```

外側の命題的切り詰めの消去に渡す最後の引数は、提示された塔の要素から読み取った局所的な `Arity ar F` の証拠です。これは上の入れ子になった切り詰め付き復号を開始しますが、隠された自然数の証人をそれだけで外へ取り出すことはありません。

```agda
          (arity q ar F q∈ eq)
```

任意の二項構成子について、まず二つの子論理式の表の値を、それぞれの再帰的な充足集合と同定します。次に二項の橋は、二つの子充足集合への所属を対応する対象言語の結合子で組み合わせることにより、複合論理式の再帰的な充足集合を特徴づけます。この共通の議論を、連言、選言、含意にそれぞれ用います。

```agda
        module BinFill (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
          (opA : ∀ {j} → Formula Ab j → Formula Ab j → Formula Ab j)
          (bridge : ∀ {n} (a b : Formula Ab n) {j : ℕ} (env : S ^ j) (ya yb : Fin j)
                  → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
                  → ExtFact (fst (SatW (opA a b))) (fst (envSet W n))
```

橋の外延の事実は、二つの下位の充足集合の上の所属の原子に、二項の結合子を適用する論理式の上で述べられます。

```agda
                      (λ z → ⟨ (z ∷ env) ⊨ op (var i0 ∈̇ var (suc ya)) (var i0 ∈̇ var (suc yb)) ⟩)) where
```

ペイロードの等式は、枠のペイロードが二つの子論理式の符号の対であることを述べます。対の単射性から二つの成分の等式を別々に取り出し、`subVal` はそれらを使って、表された各子の値の底集合を再帰的に定義された値 `SatW` の底集合と同定します。

```agda
          go : (n : ℕ) (a b ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ opA a b → fst r ≡ pr (cd a) (cd b) → ⟨ frame ⊨ R.binRel op ⟩
          go n a b ψ qa qF qp qψ qr = RR.bin-in op (λ a' b' s' c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂' →
            let q' = pr-inj (sym er ∙ qr)
                ya≡ = subVal n a c₁ ya e₁ qa e₁∈ ee₁ (e₁' ∙ cong (pr (fst ar)) (q' .fst))
```

この二つの子の値の等式は、対応する表の項目と同じ拡張環境に置かれます。結合子の橋渡しは二項の節によって `SatW (opA a b)` を特徴づけ、`transfer` はその正準な値と環境集合を、枠にすでにある候補値と環境集合へ置き換えます。

```agda
                yb≡ = subVal n b c₂ yb e₂ qa e₂∈ ee₂ (e₂' ∙ cong (pr (fst ar)) (q' .snd))
                env = yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b' ∷ a' ∷ s' ∷ frame
            in transfer n (opA a b) qa qF (qp ∙ cong cd qψ) env (R.binBody op)
                 (bridge a b env i4 i0 ya≡ yb≡))
```

非有界量化された論理式では、再帰的な子論理式のアリティは後続になりますが、その意味論的な量化は台 `W` 上を動きます。そこで抽象的な構成子 `q'` は後で `∃[]-syntax` または `∀[]-syntax` に具体化され、`qA` はアルファベット上の対応する非有界構成子を表し、橋渡しはその再帰的な充足集合を台で有界化した節に結び付けます。

```agda
        module QuFill (q' : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
          (qA : ∀ {j} → Formula Ab (suc j) → Formula Ab j)
          (bridge : ∀ {n} (a : Formula Ab (suc n)) {j : ℕ} (env : S ^ j) (wi yai : Fin j)
                  → fst (lookup wi env) ≡ Wv → fst (lookup yai env) ≡ fst (SatW a)
                  → ExtFact (fst (SatW (qA a))) (fst (envSet W n))
```

この節は、候補となる符号化環境 `z` を判定します。外側の構成子は後で `∃[]-syntax` または `∀[]-syntax` に具体化され、台 `W` 上を量化します。その各要素について、内側の `∃[]-syntax` は、その要素を `z` に付け加えて得られる符号化環境が、子論理式を表す充足集合の要素として存在することを要求します。これは一回の量化を対象言語で記述したものであり、復号器でも、再利用可能な証人の選択でもありません。

```agda
                      (λ z → ⟨ (z ∷ env) ⊨ q' (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) ⟩)) where
```

復号された論理式のアリティは `n` ですが、その量化本体のアリティは `suc n` です。関係の読み取りが与える後続の等式により、`subValS` は本体の鍵をそのアリティへ書き換え、表された値を `SatW a` と同定できます。これで量化子の橋渡しは、節が必要とする再帰的な子の値をちょうど受け取れます。

```agda
          go : (n : ℕ) (a : Formula Ab (suc n)) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ qA a → fst r ≡ cd a → ⟨ frame ⊨ R.quRel q' ⟩
          go n a ψ qa qF qp qψ qr = RR.qu-in q' (λ c₁ ya ar' s' s'' e' e'∈ ee₁ e₁' es →
            let ya≡ = subValS n a c₁ ya e' ar' qa e'∈ ee₁ (e₁' ∙ cong (pr (fst ar')) qr) es
                env = ar' ∷ s'' ∷ ya ∷ c₁ ∷ s' ∷ e' ∷ frame
```

橋渡しはまず正準な値 `SatW (qA a)` に対する外延事実を与えます。次にアリティ、環境集合、論理式の符号の等式を使って、`transfer` がその事実を、この枠の表の候補値に必要な外延の主張へ変えます。これで非有界量化子の節が完成します。

```agda
            in transfer n (qA a) qa qF (qp ∙ cong cd qψ) env (R.quBody q')
                 (bridge a env (sh 18 w) i2 qw ya≡))
```

有界量化された論理式がもつ再帰的な子論理式は一つだけであり、境界項は意味論的な橋渡しの内部で評価されます。ここでは有界量化子、条件を組み合わせる結合子、アルファベット側の構成子、そして対象言語で書かれた節の本体を分けて与えます。そのため、項の符号を子論理式として扱うことなく、同じ議論を全称形と存在形の両方に使えます。

```agda
        module BqFill (q' : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
          (c' : ∀ {j} → Formula S j → Formula S j → Formula S j)
          (qA : ∀ {j} → Term Ab j → Formula Ab (suc j) → Formula Ab j)
          (body : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S (1 + j))
          (bodyIs : ∀ {j} (wi ti yai N0i N1i : Fin j)
```

等式 `bodyIs` は、一般の節の本体を三つの有界な層と同定します。最外層は境界項の候補値を `W` 上で量化し、`tmIs` がその候補を検証します。次の層はその値に属し、かつ `W` にも属する要素を量化し、最内層の `∃[]-syntax` は符号化された拡張環境が子論理式の充足集合に属することを要求します。この等式が記述するのは意味論的な節の本体であり、元の論理式の本体そのものではありません。

```agda
                  → body wi ti yai N0i N1i
                  ≡ q' (var (suc wi)) (c' (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)))
                      (q' (var (suc (suc wi))) (c' (var i0 ∈̇ var i1) (∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3))))))
          (bridge : ∀ {n} (t : Term Ab n) (a : Formula Ab (suc n)) {j : ℕ} (env : S ^ j) (wi ti yai N0i N1i : Fin j)
                  → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup yai env) ≡ fst (SatW a)
```

橋渡しは、同じ環境の中で台、境界項の符号、子論理式の再帰的な値、そして数項タグ `0` と `1` を位置づける五つの等式を仮定します。これらから有界な論理式の外延事実を証明します。したがって外延事実は橋渡しの結論であり、再帰的に入力されるのは子論理式の値だけです。

```agda
                  → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1
                  → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ body wi ti yai N0i N1i ⟩)) where
```

対の単射性は、有界量化子のペイロードを項の符号の成分と論理式の符号の成分に分けます。第一の等式は橋渡しの項を扱う部分へ渡され、第二の等式は後続アリティの等式とともに、唯一の子論理式の表された値を `subValS` が同定するために使われます。項の符号について再帰的に表を引く必要はありません。

```agda
          go : (n : ℕ) (t : Term Ab n) (a : Formula Ab (suc n)) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ qA t a → fst r ≡ pr (ct t) (cd a) → ⟨ frame ⊨ R.bqRel q' c' ⟩
          go n t a ψ qa qF qp qψ qr = RR.bq-in q' c' (λ t' a' s' c₁ ya ar' s₁ s'' e' er e'∈ ee₁ e₁' es →
            let q'' = pr-inj (sym er ∙ qr)
                ya≡ = subValS n a c₁ ya e' ar' qa e'∈ ee₁ (e₁' ∙ cong (pr (fst ar')) (q'' .snd)) es
```

具体的な橋渡しは、正準な有界量化子の本体について外延事実を証明します。`bodyIs` に沿って書き換えると、その事実は一般の関係の本体に置かれ、続いて `transfer` が正準な充足の値を表の項目に表された候補値へ置き換えます。

```agda
                env = ar' ∷ s'' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a' ∷ t' ∷ s' ∷ frame
            in transfer n (qA t a) qa qF (qp ∙ cong cd qψ) env (R.bqBody q' c')
                   (subst (λ φ → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))
                     (bodyIs (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)))
                     (bridge t a env (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)) qw (q'' .fst) ya≡ (tg f0) (tg f1))))
```

原子論理式は二つの項の符号をもちますが、再帰的な子論理式はもちません。そこで一般の橋渡しは二項の原子構成子と、拡大された環境における関係式によって添字づけられます。橋渡しは二つの項を直接評価し、対応する外延事実を証明します。

```agda
        module AtomFill (opA : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j) (rel : Formula S (18 + m))
          (bridge : ∀ {n} (t u : Term Ab n) (env : S ^ (15 + m)) (wi ti ui N0i N1i : Fin (15 + m))
                  → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup ui env) ≡ ct u
                  → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1
                  → ExtFact (fst (SatW (opA t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ atomEx wi ti ui N0i N1i rel ⟩)) where
```

ここでもペイロードの等式は対の等式であり、今度は二つの項の符号を分離します。得られた等式により、項の符号は原子の本体が要求する環境に置かれます。実際の項の値は、その本体の内部にある二つの `tmIs` の節によって量化され検証されるのであり、再帰的な表の参照から得られるのではありません。

```agda
          go : (n : ℕ) (t u : Term Ab n) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ opA t u → fst r ≡ pr (ct t) (ct u) → ⟨ frame ⊨ R.atomRel rel ⟩
          go n t u ψ qa qF qp qψ qr = RR.atom-in rel (λ t' u' s' er →
            let q' = pr-inj (sym er ∙ qr)
                env = u' ∷ t' ∷ s' ∷ frame
```

枠の先頭に加えられる三つの項目は、ペイロード中の二つの項の符号と、その対のコンテナです。二つの成分の等式が確立すると、原子の橋渡しが選ばれた関係によって正準な充足集合を特徴づけ、`transfer` がその特徴づけを表の候補値へ移します。

```agda
            in transfer n (opA t u) qa qF (qp ∙ cong cd qψ) env (R.atomBody rel)
                   (bridge t u env (sh 15 w) i1 i0 (sh 15 (N f0)) (sh 15 (N f1)) qw (q' .fst) (q' .snd) (tg f0) (tg f1)))
```

偽は項のデータも子論理式ももちません。その橋渡しは、再帰的な充足集合が `envSet W n` 上で空の外延をもつことを直接述べます。`transfer` がこの事実を表の候補値へ書き換え、関係の構成子が偽の節としてまとめます。

```agda
        botGo : (n : ℕ) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
              → fst p ≡ cd ψ → ψ ≡ ⊥̇ → ⟨ frame ⊨ R.botRel ⟩
        botGo n ψ qa qF qp qψ = extB-in i0 i8 ⊥̇ frame
          (transfer n ⊥̇ qa qF (qp ∙ cong cd qψ) frame ⊥̇ (botBridge n frame))
```

タグ `0` は所属の原子論理式に対応します。ここでの関係式は構成可能な構造における通常の所属をそのまま意味するので、一致の証明の両方向と、原子の意味を所属に結び付ける両方向はいずれも恒等写像です。それでも原子の場合の議論は、関係を適用する前に二つの項の符号とその値を検証します。

```agda
      fill : (k : Fin 10) (A : Args k) → Fill.Data k A → Fill.Goal k A
      fill f0 A (n , (qa , qF , ψ , (qp , (t , u , (qψ , qr))))) =
        Fill.AtomFill.go f0 A _∈̇_ (var i1 ∈̇ var i0)
          (λ t u env wi ti ui N0i N1i qw' qt qu q0 q1 →
            AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _∈̇_ (λ v x → ⟨ v ∈ x ⟩)
```

タグ `1` では同じ議論を等号について行います。対象言語の等号は階層の底集合の等しさとして解釈されるので、一致の写像と意味論的な変換写像にも、表示された恒等写像以外の輸送は要りません。

```agda
              (var i1 ∈̇ var i0) (λ z v x → (λ h → h) , (λ h → h)) (λ δ h → h) (λ δ h → h))
          n t u ψ qa qF qp qψ qr
      fill f1 A (n , (qa , qF , ψ , (qp , (t , u , (qψ , qr))))) =
        Fill.AtomFill.go f1 A _≐_ (var i1 ≐ var i0)
          (λ t u env wi ti ui N0i N1i qw' qt qu q0 q1 →
```

タグ `2`、`3`、`4` は、連言、選言、含意の橋渡しとともに共通の二項の議論を使います。タグ `5` は子論理式をもたない偽の場合です。この部分の振り分けは構成子の符号に正確に従い、再帰的な情報は二項結合子が必要とする二つの子の値だけに限られます。

```agda
            AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _≐_ (λ v x → v ≡ x)
              (var i1 ≐ var i0) (λ z v x → (λ h → h) , (λ h → h)) (λ δ h → h) (λ δ h → h))
          n t u ψ qa qF qp qψ qr
      fill f2 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f2 A _∧̇_ _∧̇_ andBridge n a b ψ qa qF qp qψ qr
      fill f3 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f3 A _∨̇_ _∨̇_ orBridge n a b ψ qa qF qp qψ qr
```

タグ `6` と `7` は、非有界の存在論理式と全称論理式を表します。それらの意味論的な節は `∃[]-syntax` と `∀[]-syntax` によって台 `W` 上を量化し、後続アリティにある再帰的な本体の値を使います。残る二つのタグから有界の場合が始まり、同じ有界構成子を連言または含意と組み合わせて、項が与える境界も表します。

```agda
      fill f4 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f4 A _⇒̇_ _⇒̇_ impBridge n a b ψ qa qF qp qψ qr
      fill f5 A (n , (qa , qF , ψ , (qp , (qψ , qr)))) = Fill.botGo f5 A n ψ qa qF qp qψ
      fill f6 A (n , (qa , qF , ψ , (qp , (a , (qψ , qr))))) = Fill.QuFill.go f6 A ∃̇∈ ∃̇_ exBridge n a ψ qa qF qp qψ qr
      fill f7 A (n , (qa , qF , ψ , (qp , (a , (qψ , qr))))) = Fill.QuFill.go f7 A ∀̇∈ ∀̇_ allBridge n a ψ qa qF qp qψ qr
      fill f8 A (n , (qa , qF , ψ , (qp , (t , a , (qψ , qr))))) =
```

有界全称では、正準な本体がすでに `BqFill` の要求する抽象的な形をもつため、`bodyIs` は反射律です。入れ子になった `∀[]-syntax` は、検証された境界項の各値と、その値に属する各台要素が、再帰的な子の集合に属する符号化環境へ至らなければならないことを表します。

```agda
        Fill.BqFill.go f8 A ∀̇∈ _⇒̇_ ∀̇∈ bqAll (λ _ _ _ _ _ → refl)
          (λ t a env wi ti yai N0i N1i qw' qt qa' q0 q1 → BqBridge.allInBridge t a env wi ti yai N0i N1i qw' qt qa' q0 q1)
          n t a ψ qa qF qp qψ qr
      fill f9 A (n , (qa , qF , ψ , (qp , (t , a , (qψ , qr))))) =
        Fill.BqFill.go f9 A ∃̇∈ _∧̇_ ∃̇∈ bqEx (λ _ _ _ _ _ → refl)
```

有界存在は、これと平行な三層の本体を `∃[]-syntax` で表し、項の値であるという条件、その値への所属、そして拡張環境の子集合への所属を連言で結びます。この本体も反射律によって一致し、タグ `9` で十個の構成子の場合がすべてそろいます。

```agda
          (λ t a env wi ti yai N0i N1i qw' qt qa' q0 q1 → BqBridge.exInBridge t a env wi ti yai N0i N1i qw' qt qa' q0 q1)
          n t a ψ qa qF qp qψ qr
```

一つの構成子の節を証明するため、まず十二個の対象と、それらの所属および対の等式を `Args k` に集め、一つの対応する枠を固定します。復号されたアリティ、論理式、構成子の形は `Fill.data'` の命題的切り詰めの内側にとどまります。元の仮定はそのいずれも選択していないからです。

```agda
      clause : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩
      clause k = Fr.clause-in k (λ q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec ep e∈ ee →
        let A : Args k
            A = record { q = q ; ar = ar ; F = F ; s = s ; c = c ; p = p ; s1 = s1 ; r = r ; s2 = s2 ; e = e ; yc = yc ; s3 = s3
                       ; q∈ = q∈ ; eq = eq ; c∈ = c∈ ; ec = ec ; ep = ep ; e∈ = e∈ ; ee = ee }
```

論理式の充足は命題なので、`Fill.Goal k A` は命題的に切り詰められたデータを除去できる行き先です。隠された各証人に対して `fill` は同じ節の目標を証明し、目標の命題性により、どのアリティ、論理式、分解が復号を証言したかには結果が依存しません。この除去から再利用可能な復号器や表の値の選択が取り出されることはありません。

```agda
        in PT.rec (Fill.isPropGoal k A) (fill k A) (Fill.data' k A))
```

十個の構成子の節を一つの有限連言にまとめます。この連言は完全な表仕様の `ten` 成分であり、全域性と領域条件は次の段階で別に加えます。

```agda
      ten : ⟨ γ ⊨ Cl.ten ⟩
      ten = bigAnd-in γ 9 Cl.clause clause
```

これで三つの部分が `tableAt` の定義をちょうど満たします。`total` は `C` の各符号について表の値が命題的に切り詰められて存在することを与え、`onC` は表の各要素の鍵が `C` に属することを述べ、`ten` はすべての構成子の節を与えます。これらは与えられた関係が表の仕様を満たすことを証明しますが、それが大域的に選ばれた関数であることも、ここで値が一意であることも主張しません。

```agda
    holds : ⟨ γ ⊨ tableAt T w C E N ⟩
    holds = total , (onC , ten)
```

## 一つの論理式のスロットへの特殊化

`W` を固定すると、結び付いた二つの見方が定まります。`Alphabet W` は、定数が `W` の要素を名指す論理式とその符号を与え、`Bridge W` はそれらの定数を構成可能な台で解釈し、再帰的な充足と対象言語の節を比較します。以下の特殊化では、一つの論理式が生成するスロットにこの二つの見方を同時に用います。

```agda
module _ (W : S) where
  open Alphabet W
  open Bridge W
```

`x` が `ψ` の生成するスロットに属するなら、命題的切り詰めの下で、あるアリティ `m` と論理式 `χ : Formula Ab m` が存在し、`x` は `keyS W χ` の底集合に等しくなります。この結論はそのような論理式の鍵の存在を保ちますが、論理式を選択せず、`χ` が `ψ` の部分論理式であることの明示的な証明も保持しません。

```agda
  slotAb : ∀ {n} (ψ : Formula Ab n) (x : V ℓ)
         → ⟨ x ∈ fst (slot W (toS ψ)) ⟩
         → ∥ Σ[ m ∈ ℕ ] Σ[ χ ∈ Formula Ab m ] (x ≡ fst (keyS W χ)) ∥₁
  slotAb ψ x h = PT.map
    (λ { (m , χ , e , _) → m , χ , (e ∙ sym (keyBridge W χ)) })
```

局所的な等式 `mapped ψ` は、まず具体的なスロットを `keyʟ (toS χ)` を集める一般の木へ書き換えます。次に `tree-inv` を適用すると、寄与した論理式 `χ` と、その内部の鍵との等式が命題的に切り詰められて得られます。この写像はその等式を保ち、`keyBridge` によって内部の鍵を `keyS W χ` に置き換えます。付随する部分木の包含証明は、定理の結論から意図的に捨てられます。

```agda
    (tree-inv key key ψ x (subst (λ y → ⟨ x ∈ fst y ⟩) (mapped ψ) h))
    where
    key : ∀ {n} → Formula Ab n → S
    key χ = keyʟ (toS χ)
```

等式 `mapped` は構造再帰で証明されます。`toS` は定数だけを変え、論理式の各構成子をそのまま保つからです。所属の原子論理式、等号の原子論理式、偽では二つの表示が定義上等しくなります。二項結合子では、スロットは論理式自身の鍵を含む一元集合と二つの子の木の合併からなるので、二つの再帰的な等式を同じ合併の下で組み合わせます。

```agda
    mapped : ∀ {n} (χ : Formula Ab n) → slot W (toS χ) ≡ tree key χ
    mapped (t ∈̇ u) = refl
    mapped (t ≐ u) = refl
    mapped ⊥̇ = refl
    mapped χ@(a ∧̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
```

連言、選言、含意はいずれも同じ二分木の形をもち、二つの再帰的な等式を使います。各非有界量化子がもつ論理式の本体は一つだけなので、根の一元集合を、再帰的に対応づけられた一つの子の木と合併します。束縛子の下でのアリティの変化は子論理式の型を変えますが、この合併の形は変えません。

```agda
    mapped χ@(a ∨̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
    mapped χ@(a ⇒̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
    mapped χ@(∃̇ a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
    mapped χ@(∀̇ a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
    mapped χ@(∀̇∈ t a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
```

有界全称と有界存在の場合も、子の木として加わるのは論理式の本体だけです。境界項は構成子のペイロードの一部であり、`slot` が集める子論理式の木ではありません。この最後の二つの再帰的な等式で、具体的なスロットと一般の鍵の木との比較が完成します。

```agda
    mapped χ@(∃̇∈ t a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
```

`SlotHolds` は、表、台、符号領域、環境の塔の位置をそれぞれ `T`、`w`、`C`、`E` とし、さらに十個のタグ位置 `N` をもつ環境で働きます。台、タグ、塔についての事実を仮定して基礎となる論理式 `ψ0` を固定し、等式 `qT` と `qC` は、`T` と `C` に格納された底集合だけを、`ψ0` が生成する正準な表とスロットに同定します。

```agda
  module SlotHolds {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
    (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
    (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) {n0 : ℕ} (ψ0 : Formula Ab n0)
    (qT : fst (lookup T γ) ≡ fst (satTable W (toS ψ0)))
    (qC : fst (lookup C γ) ≡ fst (slot W (toS ψ0))) where
```

ここで略記される底集合は二つだけです。`Tv` は表の位置 `T` に格納された関係であり、`Cv` は符号領域の位置 `C` に格納された集合です。続く四つの構成は、この二つの集合について必要となる値の一致、復号、全域性、領域条件の仮定を正確に与えます。

```agda
    private
      Tv = fst (lookup T γ)
      Cv = fst (lookup C γ)
```

`c` の底集合が論理式 `ψ` の鍵に等しく、`(c,yc)` が `Tv` に表されているとします。`keyBridge` と `qT` に沿って書き換えると、これは `ψ0` の生成する正準な表の項目になり、`entry-out` によって `fst yc ≡ fst (SatW ψ)` が得られます。この結論は正しい論理式の鍵において、すでに与えられた値を固定しますが、そのような項目の存在を主張するものではありません。

```agda
      val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ)
           → ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ → fst yc ≡ fst (SatW ψ)
      val≡ ψ c yc qc h = entry-out W (toS ψ0) (toS ψ) (fst yc)
        (subst2 (λ u v → ⟨ pr u (fst yc) ∈ v ⟩) (qc ∙ keyBridge W ψ) qT h)
```

復号は、所属 `c ∈ Cv` と、指定されたアリティ表示 `fst c ≡ pr (# n) z` の両方から始まります。所属を `qC` に沿って運ぶと、`slotAb` は、あるアリティの論理式でその鍵が `c` であるものを命題的切り詰めの下で与えます。残る仕事は、この隠されたアリティがちょうど `n` であり、その論理式の符号がちょうど `z` であることを示すことです。

```agda
      decode : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (z : V ℓ)
             → fst c ≡ pr (# n) z → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
      decode c c∈ n z e = PT.map
        (λ { (n₁ , ψ₁ , e₁) →
          let q = pr-inj (sym e₁ ∙ e)
```

`c` についての二つの等式から、対どうしの等式が得られます。対の単射性は数項の成分と論理式の符号の成分をそれぞれ比較し、数項の単射性から二つのアリティの等しさが従います。論理式はアリティで添字づけられているため、隠された論理式をその等式に沿って輸送しなければなりません。`cd-subst` はこの依存輸送に伴う符号の変化を処理し、符号が `z` である `Formula Ab n` の論理式を与えます。

```agda
              nq = #-inj′ (q .fst)
          in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) })
        (slotAb ψ0 (fst c) (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
```

各 `c ∈ Cv` について、`qC` による輸送で `c` を正準なスロットへ移すと、`slotTotal` は、`c` と対をなして正準な表に属する値 `y` を命題的切り詰めの下で与えます。さらに `qT` に沿ってその項目を `Tv` へ戻します。得られる全域性は存在だけを述べ、`Cv` 上の値関数を選択しません。

```agda
      tot : (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
      tot c c∈ = PT.map
        (λ { (y , h) → y , subst (λ u → ⟨ pr (fst c) (fst y) ∈ u ⟩) (sym qT) h })
        (slotTotal W (toS ψ0) (fst c) (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
```

`Tv` の要素 `e` について、等式 `qT` はまずその所属を正準な充足関係表へ移します。次に `ent-slot` は、命題的切り詰めの下で、アリティ `m`、論理式 `χ`、および `fst e` と `χ` が供給した正準な項目の底集合との等式を返します。この等式を `prʟ-fst` と合成すると、`fst e ≡ pr (fst (keyʟ χ)) (fst (Sat W χ))` が得られます。

```agda
      onc : (e : S) → ⟨ fst e ∈ Tv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
      onc e e∈ = PT.map
        (λ { (m , χ , (q , _)) →
          let ee = q ∙ prʟ-fst (keyʟ χ) (Sat W χ)
```

この切り詰められた証人の内部で `c = keyʟ χ`、`yc = Sat W χ` と取ります。先ほど得た等式が `e` の必要な分解を与えます。`e` の所属を正準な表へ運ぶと、`inSlot` によりその鍵が正準なスロットに属することが従い、`qC` がこの事実を `Cv` へ移します。こうして同じ命題的切り詰めの下で領域条件が得られますが、分解を大域的に選択することも、一価性を証明することもありません。

```agda
          in keyʟ χ , Sat W χ , (ee , subst (λ u → ⟨ fst (keyʟ χ) ∈ u ⟩) (sym qC)
               (inSlot W (toS ψ0) (fst (keyʟ χ)) (fst (Sat W χ))
                 (subst2 (λ u v → ⟨ u ∈ v ⟩) ee qT e∈))) })
        (ent-slot W (toS ψ0) (fst e) (subst (λ u → ⟨ fst e ∈ u ⟩) qT e∈))
```

ここで共通の台、タグ、環境の塔の仮定に、先ほど証明した値の一致、復号、全域性、領域上の分解という四つの事実を合わせます。これらが `SatHoldsC` の七つの仮定です。この向きで閉性が不要なのは、構成子の節を組み直す際に、関係の節が対応するすべての子論理式の表項目を全称的に提示し、`val≡` がその各項目にすでに与えられた子の値を直接固定するからです。復号器は現在の領域の符号を扱い、`tot` と `onc` は残る二つの最上位の表条件を確立します。ここでは、親の論理式キーの所属から子論理式キーの所属を導く段階はありません。

```agda
      module SH = SatHoldsC W T w C E N γ qw tg hE val≡ decode tot onc
```

したがって、`qC` と `qT` によって `ψ0` の生成するスロットと充足関係表に同定された対象は、`tableAt T w C E N` を満たします。この結論は具体的な表の仕様だけを述べます。スロットの閉性を証明せず、この仕様を満たすすべての表を正準な表と同定するものでもありません。後の利用箇所では、表された鍵での一意性が必要なときに `slotClosed` を別に加え、`SatSoundC.pinned` を適用します。

```agda
    holds : ⟨ γ ⊨ tableAt T w C E N ⟩
    holds = SH.holds
```

## まとめ

固定再帰は、外から与えられた表の仕様を正準な充足関係表についての定理へ変換し、逆に正準な表がその仕様を満たすことも示します。証明の数学的な役割は明確に分かれています。復号は論理式の符号を同定し、全域性は値の存在だけを与え、領域条件は表の各項目の由来を説明します。閉性が使われるのは、表された親の論理式キーから子のキーを回収しなければならない向きに限られます。