---
title: "名前の比較を表す論理式"
module: L.Choice.NameComparison
lang: ja
site: "Bedrock"
description: "名前の比較を表す論理式"
stage: "正準整列順序と選択公理"
reading_order: 77
canonical: https://bedrock.institute/ja/L.Choice.NameComparison.html
html: L.Choice.NameComparison.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/NameComparison.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.Satisfaction, L.Coding.SatisfactionTable, L.Coding.SlotClosure, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.SatisfactionGraph, L.Coding.EnvironmentTower, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.PinnedRecursion, L.Choice.CanonicalNames, L.Choice.FiniteStageOrders, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.NameComparison.md, https://bedrock.institute/zh/L.Choice.NameComparison.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 名前の比較を表す論理式

同じ定義可能な部分集合が複数の名前をもつことがあります。メタ言語における名前は、アリティ `k`、`suc k` 個の変数位置をもつ無パラメータ論理式、そして台から取った `k` 個のパラメータのベクトルから成ります。名前の指示対象は、この三つのデータから導かれます。余分な一つの変数が候補となる要素を表し、残りの変数がパラメータベクトルを受け取ります。したがって、指示対象は名前の第四の成分ではありません。

このデータを `L` の内部で表すために、本章はパラメータベクトルを有限な環境グラフで表し、論理式の評価を充足関係グラフで表します。正しい論理式キーにおいて、`satGraphAt` はそのキーを、論理式を満たす環境全体の集合に関係づけます。その出力は、まさにこの充足環境の集合です。`NameAt` はアリティ、無パラメータ論理式の符号、パラメータ環境を、それらから導かれる指示対象に結び付けます。後で競合する名前を量化するとき、それらは同じ指示対象をもたなければなりません。

名前は辞書式に比較されます。まず極限段階の順序で論理式の符号を比較し、次にアリティを比較し、最後に台上の与えられた順序でパラメータベクトルを比較します。論理式 `≺At` はこの三つの場合を表します。`LeastNameAt` は、同じ指示対象をもち、現在の名前より小さい名前がないことを述べるだけです。最小名を実際に選ぶのは、先に構成された `CanonicalNames.leastName` です。`StepAt` は二つの最小名を局所的に量化して比較します。本章で証明する妥当性は、ちょうど `≺At` とメタ言語の関係 `_≺ₙ_` との対応までです。`NameAt`、`LeastNameAt`、`StepAt` の完全な妥当性は後続の展開で証明されます。

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

基礎となる言語は、宇宙レベル、有限添字、ベクトル、命題値の主張を与えます。古典的推論は、明示された一つの仮定 `LEM (ℓ-suc ℓ)` を通して入ります。そのレベルは、以下で使う充足関係の構成と整列順序を扱うのに十分です。この仮定を明示しておくことで、性質を述べるだけの記述と、証人を実際に選ぶ先行の構成とを区別できます。

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

宇宙レベル `ℓ` と、必要な一段高いレベルでの排中律を固定します。これは本章が引き継ぐ古典論理のインターフェースです。以下の論理式構成子は構文を組み立てるだけですが、そこで用いる自然数対象、充足関係グラフ、極限段階の符号順序、正準名の理論は、いずれも同じ仮定のもとで構成されています。したがって、このモジュールはこれらの意味論的依存関係を記録しますが、改めて選択を行うことはありません。`LeastNameAt` は最小性を表し、最小名を選ぶ構成は引き続き `CanonicalNames.leastName` です。

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

対象言語は所属と等号を述べ、命題を組み合わせ、台全体または一つの集合の上で量化できます。その意味論は命題値の構造で読み取られます。定数の写像は、後で必要となる三つの表示を結び付けます。すなわち、本当にパラメータをもたない論理式、空のアルファベット上の論理式、構成可能な台上で解釈された同じ構文です。これらの写像は論理式の構造を保つので、無パラメータ骨格の符号を内部で認識できるようになります。

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

論理式の符号、順序対、数項は、それ自身が累積階層の集合です。構成可能部分構造は論理式を読む台を与え、推移性は構成可能な符号集合への所属から、その成分に必要な構成可能性を与えます。対の符号化と数項の符号化の単射性によって、後に等しいキーからアリティと骨格符号を復元できます。各 `Lset` 段階は極限段階の符号順序の舞台となります。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset )
open import L.Ordinal {ℓ} using ( ∈#-elim; #∈#-elim )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ; extensionalL )
```

アリティは内部の自然数集合に属する数項で表し、パラメータベクトルは有限環境のグラフで表します。対象言語の論理式は、順序対、適用、定義域を調べ、候補となる要素を環境に追加し、外延的に部分集合を定義できます。ある台上の論理式に対して、`Sat` はその論理式を満たす環境全体の集合です。後で充足関係グラフから復元する意味論的な値は、この集合です。

```agda
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro; envOverAt )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in-both; numL; sucAtL; sucAtL-adequate; consAtL )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
```

充足関係はすでに表として構成されており、各項目は部分式のキーと、再帰的に定まる充足環境の集合を対にしています。スロットの閉性と全性により、再帰で必要となるすべての正しいキーに項目が与えられ、充足関係の橋渡しが論理式の定数を選ばれた台の要素として同定します。したがって本章では、充足関係の再帰を再実行せずに、キーに保存された集合値を読み取れます。

```agda
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.CodeSet {ℓ} lem
```

各台について、`AllCodes` はその台上の正しい論理式キーをちょうど集め、その二方向の読みは所属と元の論理式を結び付けます。統一充足関係の橋渡しは、関係を表す論理式 `satGraphAt B x y` を支えます。`x` がスロット `B` の台上の正しいキーであるとき、`y` は対応する充足環境の集合です。`GraphWitAt` と二つのグラフの読みは、この集合値の関係を新しい再帰なしに示します。

```agda
  using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge )
open import L.Coding.SatisfactionGraph {ℓ} lem using
  ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
  ; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )
```

環境の塔とタグ付き再帰データは、充足関係グラフの読みが各構文要素について成り立つことを保証します。この内部の仕組みに対し、正準名の理論は名前比較の基準となるメタ言語の対象を与えます。メタ言語の `Name` が保存するのは、アリティ、無パラメータ論理式、パラメータベクトルです。`limitCode` は論理式から第一の比較キーを導き、指示対象は充足関係から別に導かれます。後のスロット論理式も、この区別を保たなければなりません。

```agda
open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )
```

名前の符号は極限段階の要素であり、`limitOrder` によって比較されます。第三のキーは、台上に与えられた任意の狭義整列順序から来ます。正準名の理論は、これらと自然数のアリティをすでに `_≺ₙ_` にまとめ、その関係の整礎性を証明し、`leastName` で用いています。本章では二つの非数値的な順序を、表示法則を伴う関係スロットによって受け取ります。したがって、どちらの順序も再構成せず、それらによる比較を記述します。

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
```

自然数の順序が第二の比較キーを与えます。アリティが数項で表されるとき、一方の数項が他方に所属することは狭義の不等号を表します。有限添字は、パラメータベクトルの成分と、二つのベクトルが最初に異なる位置を指定します。後の妥当性の議論では、共通の長さに関する帰納法により、この最初の相違による記述が `_≺ₙ_` で使われる再帰的なベクトル順序と一致することを証明します。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
```

証明データは辞書式順序の形に従います。依存対は位置とその証拠を運び、直和は符号、アリティ、パラメータの三つの場合を分けます。先行するキーの等しさにより、依存する論理式とベクトルを共通のアリティへ輸送してから、次のキーを比較できます。空の型は、定数をもたない論理式に必要な定数解釈を一意に与えます。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2 )
```

存在式と選言式の充足意味論は命題的に切り詰められています。証人が存在することは保ちますが、どの証人が与えられたかは忘れます。そのため、論理式の符号や名前比較を外向きに読むと、結論にも切り詰められた存在が残り、消去先は命題に限られます。ここで使われるのは命題的切り詰めであり、命題のリサイズではありません。累積階層は集合値の所属関係と、その読みの後で必要となる外延的な等しさの原理を与えます。

```agda
open import Cubical.Foundations.Transport using ( constSubstCommSlice )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

階層集合の小さな要素は周囲の階層へ埋め込まれ、その埋め込みの単射性によって、後に表現されたパラメータの等しさから台の中での等しさを復元できます。空集合は空のアルファベットとして働きます。定数がないので、そこから出る写像は一意に定まり、無パラメータ論理式は必要な付け替えの下で同じ符号を保ちます。フォン・ノイマン数項 `# k`、その後者、そして `ω` が、環境の定義域と名前比較に使う内部のアリティを与えます。

```agda
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω; sucV )
```

以下の論理式は構成可能宇宙で解釈されます。`hPropStructure 𝒮ʟ` を開くことで、その台 `S` が定まります。台の要素は、周囲の宇宙にある集合と、それが構成可能であるという証拠の組です。また、この構造の命題値をとる等号関係と所属関係もスコープに入ります。したがって自由変数と定数は構成可能集合の中を動き、証明で等号や所属の証拠が必要なときには、`⟨_⟩` がその命題の基礎型を取り出します。

```agda
open hPropStructure 𝒮ʟ
```

同じ構文には、互いに両立する二つの読み方があります。この絶対性の実例は、周囲の宇宙の構造 `𝒮ᵥ` から出発し、それを推移的クラス `isL` に制限します。外側の読みでは構成可能集合をその基礎にある周囲の集合として扱い、内側の読みでは定数がそれを名指す構成可能集合を表し、制限された構造が等号と所属を解釈します。本章では内側の充足関係を `⊨` と書きます。したがって `γ : S ^ n` に対する判断 `γ ⊨ F` は、有限環境 `γ` のもとで `F` が `L` の内部に成り立つことを意味します。これは、`L` 自身が名前を識別して比較する論理式に必要な読み方です。

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

これらの論理式は、環境内の位置によって先に与えられたデータを参照します。新しい束縛子の下では、もとの位置は新たに束縛された値を越えなければなりません。二つの束縛子の下では、位置 `i` は `suc (suc i)` になります。`sh2` はこの移動を表す略記です。`FreeAt` が後続のアリティとその符号鍵を束縛してから骨格と空のアルファベットの符号集合を参照するとき、また表示の条件が候補要素と拡張環境を束縛してからもとのパラメータ環境を参照するときに使われます。

```agda
private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)
```

表示の条件の内部では、四つの値が環境に加わった後で初めて、骨格と台の符号集合を参照します。その四つは、候補要素 `z`、拡張環境 `c`、その定義域 `k`、そして考察中の鍵です。したがって、もとの位置を四回持ち上げる必要があります。`sh4` はまさにこの移動を行い、その鍵が台の符号集合に属することと、`k` と骨格から作られる対に等しいことの両方を述べられるようにします。

```agda
  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))
```

さらに一つの存在量化子が鍵に対応する値 `v` を束縛するため、`satGraphAt` を用いる時点では台が五つ先の位置にあります。ここで `v` は符号化された論理式を充足する環境全体の集合であり、真理値ではありません。続く所属原子は、拡張環境がその集合に属するかを問います。同じ移動は `LexAt` にも現れます。一つの添字、その位置で二つの環境から得られる値、より前の添字、そして両者の一致を証す共通の値を順に束縛すると、もとのパラメータ環境はやはり五つ先にあります。`sh5` は両方の論理式に共通する添字計算を記録します。

```agda
  sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n)))))
  sh5 i = suc (suc (suc (suc (suc i))))
```

## 空のアルファベットでも同じ符号

空のアルファベットは、空集合の要素の小さな表示 `⟪ ∅ ⟫` です。もし `m` がその記号の一つなら、埋め込み `⟪ ∅ ⟫↪` によって周囲の集合が得られ、表示の法則はそれが `∅` に属すると述べます。定理 `∅-empty` はまさにそのような証拠を否定するので、`noAlpha m` が従います。したがって、このアルファベット上の論理式は定数の節を含めません。これは無パラメータ論理式の一つの構文的表示です。メタ言語の名前が用いる空の定数域 `⊥*` と比較するには、この二つの空型を結び付ければ十分です。

```agda
private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)
```

`Fo∅ n` は、`n` 個の変数位置を使える空のアルファベット上の論理式の族 `Formula ⟪ ∅ ⟫ n` を表す略記です。定数を含まないことは、論理式に別の述語を課すのではなく、定数記号の型そのものから従います。メタ言語の名前は、これに対応する族 `Formula ⊥* n` を使います。より正確には、`Name` が格納するのはアリティ、この族に属して変数位置を一つ余分にもつ無パラメータ論理式、そしてそのアリティのパラメータ列です。表示はこの三つから導かれるものであり、別の格納成分ではありません。

```agda
  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫
```

写像 `ε` は、空のアルファベット `⟪ ∅ ⟫` から空の定数域 `⊥*` への移行を与えます。仮に始域の記号 `m` が与えられれば、`noAlpha m` が矛盾を導き、空型の消去によって必要な終域の値が得られます。したがって `mapFo ε` は `⟪ ∅ ⟫` 上の論理式を `⊥*` 上の論理式へ改名します。逆向きには、`embed` を `⊥*` から `⟪ ∅ ⟫` への改名として特殊化できます。もともと定数の出現がないので、どちらの操作も定数の出現を変えません。そこで改名の合成則から、空のアルファベットによる特徴付けに必要な論理式の符号の等式が得られます。

```agda
  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = Empty.rec (noAlpha m)
```

モデルの内部で無パラメータ論理式のコードを認識するには、まず「定数を持たない」ことの二つの表し方を結び付ける必要があります。`⟪ ∅ ⟫` 上の論理式`ψ` では、定数域は空集合の要素の型です。一方、`mapFo ε ψ` は同じ構文を空型`⊥*` の上で表します。空集合の要素を仮定すれば矛盾が得られるため、写像 `ε`を定義できます。したがって、`ψ` を直接宇宙へ読む経路と、`ε` に沿って改名してから宇宙へ埋め込む経路の違いは、空型から出る写像の違いだけです。関数外延性がそれらの写像を同一視し、`mapFo-comp` が改名の合成を同一視します。このように `sameCode` は、まず得られる宇宙上の論理式そのものの等式を証明します。後でこの等式にコード化写像を適用すれば、対応するコードの等式が得られます。

```agda
  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m)))
             ∙ sym (mapFo-comp ε Empty.rec* ψ)
```

逆向きの比較は、無パラメータ論理式 `χ : Formula ⊥* n` から始まります。まず `χ` を `⟪ ∅ ⟫` 上の論理式へ埋め込み、そのアルファベットから宇宙への包含写像に沿って改名することも、初めから宇宙上の論理式へ埋め込むこともできます。`mapFo-comp` によれば、前者は `⊥*` からの一回の改名です。`⊥*`からの任意の二つの関数は等しいので、この改名は直接の埋め込みで使われるものと一致します。`sameCode'` の等式は、`AllCodes ∅ʟ` が埋め込まれた論理式に与えるキーを、`χ` の通常の宇宙上の論理式コードからなるキーへ移すのに必要な向きを持っています。

```agda
  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))
```

もう一つ、依存型に由来する問題があります。アリティは論理式の型の一部なので、等式 `e : i ≡ j` は `ψ : Fo∅ i` を `subst Fo∅ e ψ : Fo∅ j` へ移します。しかし、この移動の後もキーに入る論理式コードは同じでなければなりません。論理式を読み、コード化する関数の終域は固定された宇宙 `V ℓ` であり、アリティの添字には依存しません。したがって、一般の置換計算 `constSubstCommSlice` により、論理式を輸送してもコードは変わりません。`codeShift` はこの等式を、輸送後の論理式のコードから元のコードへ向かう形で記録し、復号の議論で行うアリティの調整に備えます。

```agda
  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift e ψ = sym (constSubstCommSlice
    Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)
```

これで、コード集合との橋の直接な向きを証明できます。無パラメータな `k` 項論理式 `χ` を `⟪ ∅ ⟫` 上へ埋め込むと、その論理式のキーは`key∈AllCodes` により `AllCodes ∅ʟ` に属します。このキーは、数項 `# k` と、埋め込まれた論理式を空のアルファベットを通して読んだコードとの対です。`sameCode'` はその論理式を `χ` の宇宙への直接の埋め込みと同一視し、後者のコードはちょうど `fst (limitCode χ)` です。この等式に沿って所属の証明を輸送すると `freeCode-in` が得られます。すなわち、コード集合はすべての無パラメータ論理式について、アリティとコードからなるキーを含みます。

```agda
freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))
```

逆向きでは、`pr (# k) c` が `AllCodes ∅ʟ` に属すると仮定します。除去定理`AllCodes-out` は、要素を命題的切り詰めの下でのみ復号し、入力には `S` の要素、すなわち集合とその構成可能性の証明を要求します。必要な入力の台集合はすでに `pr (# k) c` なので、残るのはその構成可能性の証明です。それが得られれば、`PT.map read` は切り詰められた各復号データを、求める `k` 項の無パラメータなデータへ変換します。この操作が命題的切り詰めを取り除くことはありません。

```agda
freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩
             → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁
freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩
```

不足していた証明書は、構成可能性の推移性から得られます。`AllCodes ∅ʟ .snd` はコード集合が構成可能であることを述べ、`h` はキーがその集合に属することを述べます。したがって`isL-trans h (AllCodes ∅ʟ .snd)` により、キー自身の構成可能性が証明されます。この証明書を `pr (# k) c` と組にすれば、`AllCodes-out` が要求する `S` の要素が得られます。ここでは新たな復号も選択も行われません。

```agda
  cL = isL-trans h (AllCodes ∅ʟ .snd)
```

命題的切り詰めの内部で、`AllCodes-out` はアリティ `n`、論理式`ψ : Fo∅ n`、そして与えられたキーが `ψ` のキーであることを示す等式を与えます。局所関数 `read` は、そのような各データを、要求されたアリティ`k` の無パラメータ論理式と、`c` がそのコードに等しいことの証明へ変換します。まず `ψ` を `ψ' : Fo∅ k` へ輸送し、次に、現れ得ない定数を `ε` に沿って改名します。したがって構成される証人は `mapFo ε ψ'` です。対の等式は、輸送に必要なアリティの等式と、返される依存対に必要なコードの等式をともに与えます。

```agda
  read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ))
       → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ))
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k
```

キーの等式の二つの成分が構成を完成させます。第一成分の型は `# k ≡ # n`です。数項の単射性と対称性から `e : n ≡ k` が得られ、`ψ` はそれに沿って`ψ'` へ輸送されます。第二成分は、`c` が元の `ψ` から得られる宇宙上の論理式コードに等しいことを述べます。`codeShift` により、そのコードは輸送後の `ψ'` のコードと一致します。さらに `sameCode` により、後者は`embed (mapFo ε ψ')` のコードと一致します。これらの等式を合成すると、証人と組にすべき証明がちょうど得られます。`read` は `PT.map` を通してのみ使われるため、`freeCode-out` の結論は、そのような無パラメータ論理式が命題的切り詰めの下で存在するということだけです。コード集合から論理式を選び出してはいません。

```agda
    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')
```

## 無パラメータ性を一つの原子で述べる

符号集合では、論理式はアリティと骨格からなるキーのもとに格納されます。このことを一つの所属原子で表すため、`FreeAt` はまずアリティ位置の値の後続を束縛し、次にその後続と骨格との対を束縛して、最後にその対が符号集合位置に属するかを問います。したがってメタ言語の記法では `∃[ z ] ∃[ y ]` という形をもち、`z` が後続アリティ、`y` がキーです。各シフトは、一つまたは二つの束縛子の下から元のどの位置を参照するかを正確に記録します。この段階で論理式が述べるのは `C₀` に置かれた集合への所属だけです。その位置を空のアルファベットの符号集合と同定して初めて、無パラメータ性という意味が得られます。

```agda
FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )
```

最初の一対の読みは、任意の環境 `γ` に対して成り立ちます。外側から与えられる等式 `qa` は、アリティ位置の値を数項 `# k` と同定します。これは意味論的な読みの仮定であり、`FreeAt` の内部にある別の節ではありません。骨格位置と符号集合位置はまだ任意なので、これらの補題は特定の符号集合を選ぶ前に、二つの束縛子の論理的内容だけを取り出しています。

```agda
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) where
```

順方向の構成では、意図したキー `pr (# (suc k)) (fst (lookup s γ))` がすでに `C₀` 位置の集合に属すると仮定します。このキーから `FreeAt` が要求する二つの存在証人が得られます。最初は数項 `# (suc k)`、次はそれと骨格との対です。残るのは、これらの証人がそれぞれ後続と対の記述を満たすことの確認だけであり、最後の原子は仮定した所属そのものです。

```agda
  FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
    where
    numAt : S
```

内部言語の存在証人は `S` の要素なので、その台となる集合には構成可能性の証明が伴わなければなりません。第一の証人 `numAt` には、すべての数項が `L` に属することからこの証明が得られます。第二の証人 `keyAt` については、所属の仮定がキーを `C₀` 位置の構成可能集合に入れ、`L` の推移性がキー自身の構成可能性を与えます。これらの証明は数項とキーを束縛値として使えるようにするものであり、`FreeAt` に新たな数学的条件を加えるものではありません。

```agda
    numAt = # (suc k) , numL (suc k)
    keyAt : S
    keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd)
    hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
    hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
```

二つの補助論理式に対する妥当性の等式が、必要な確認を行います。`hsuc` では、等式 `qa` によってアリティ位置の値を `# k` に置き換え、その数項の後続が `# (suc k)` であることを使います。`hpr` では、`prAtL` の妥当性により、充足関係は二つの成分位置が指定する順序対との等しさに帰着します。`keyAt` はまさにその対として定義されています。こうして二つの意味論的事実が、選んだ証人を最後の所属原子へ結び付けます。

```agda
      (cong sucV (sym qa))
    hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
    hpr = subst ⟨_⟩
      (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl
```

逆方向の読みは、`FreeAt` の充足関係から所属を取り出します。存在論理式の充足関係は証人を命題的切り詰めの内側でしか与えないため、証明は外側の切り詰めを目標の所属命題へ消去します。外側の存在量化の一つの代表は、後続の証人と内側の存在論理式の充足関係を含みます。後者にはそれ自身の命題的切り詰めが残っており、次にもう一度消去されます。

```agda
  FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
  FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                            ∈ fst (lookup C₀ γ))) atNum
    where
```

二回の切り詰め消去は同じ終域をもつので、証明はそれを `Target` と名付けます。その内容は、意図したキーが `C₀` 位置の集合に属することです。集合への所属は命題値なので、この型は命題です。この事実こそ各切り詰め消去を使うための根拠であり、存在証人から特定の代表を選んでいるわけではありません。

```agda
    Target : Type (ℓ-suc ℓ)
    Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
```

分岐 `atKey` は、内側の存在量化の一つの代表を扱います。外側の証人 `z` と、`z` がアリティ値の後続であるという等式を受け取り、さらに内側の証人 `y` と二つの事実を受け取ります。その二つは、`y` が対の論理式を満たすことと、その台となる集合が `C₀` 位置の集合に属することです。内側の存在量化は命題的に切り詰められていますが、この消去分岐の内部では、その代表を用いて命題 `Target` を証明できます。

```agda
    atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ))
          → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                       × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ )
          → Target
    atKey z qz (y , (hp , hy)) =
```

`prAtL` の妥当性は、`y` の台となる集合を、第一成分が `z` の台となる集合、第二成分が骨格である対と同定します。`z` に関する等式に続けて `qa` を用いると、その第一成分は `# (suc k)` と同定されます。したがって `y` は意図したキーです。与えられた `y` の所属をこの等式に沿って移送すれば、`pr (# (suc k)) (fst (lookup s γ))` の所属、すなわち `Target` が得られます。

```agda
      subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
         ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy
```

外側の消去分岐 `atNum` は、一つの代表 `z` と二つの証拠を受け取ります。第一の証拠は `z` が後続の論理式を満たすことを述べ、第二の `hk` は、まだ命題的に切り詰められた内側の存在論理式の充足関係です。したがって `atNum` はキーの第一成分を定める情報をすでにもつ一方、内側の証人は `Target` へ消去できる段階まで切り詰めの中に保ちます。

```agda
    atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                       × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                       ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
          → Target
    atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
```

`sucAtL` の妥当性は、第一の証拠を `atKey` が必要とする等式へ読み替えます。すなわち、`z` はアリティ位置の値の後続です。そこで証明は `hk` を命題 `Target` へ消去し、各代表に `atKey` を適用します。`FreeAt-out` にすでに組み込まれた外側の消去と合わせて、これで二層の存在量化が処理され、命題的切り詰めの境界も保たれます。

```agda
                                         ∈ fst (lookup C₀ γ)))
      (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk
```

続く二つの読みでは、それまで任意だった二つの位置を具体化します。等式 `q₀` は `C₀` 位置の集合を `AllCodes ∅ʟ` と同定します。その要素は空のアルファベット上の論理式のキーです。また `qa` は、アリティ値を再び `# k` と同定します。これらの仮定のもとで、`FreeAt-in` と `FreeAt-out` が特徴付けた所属を、アリティ `suc k` の無パラメータ論理式についての具体的な主張へ変換できます。

```agda
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ))
         (qa : fst (lookup a γ) ≡ # k) where
```

`FreeAt` の充足関係から出発すると、`FreeAt-out` はキーが現在 `C₀` 位置に置かれた集合に属することを与えます。`q₀` に沿って移送すると、この所属は `AllCodes ∅ʟ` への所属になります。先に証明した復号補題 `freeCode-out` は、アリティ `suc k` の無パラメータ論理式 `χ` で、その極限段階の符号が骨格位置の値であるものを、命題的切り詰めのもとで返します。これが一つの所属原子の外向きの意味論的な読みです。

```agda
  codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
               → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                     (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁
  codeFree-out h = freeCode-out (suc k) (fst (lookup s γ))
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀
```

ここでアリティが `suc k` なのは、定義可能な部分集合の名前に使う論理式が、`k` 個のパラメータ位置に加えて、候補要素のための変数位置を一つ必要とするからです。`codeFree-out` が与える論理式の証人は、命題的に切り詰められたままです。`FreeAt-out` は所属が命題であるため自身の束縛された証人を局所的に消去できますが、最後の復号段階で `freeCode-out` が切り詰められた論理式の証人を与えます。したがって結論は、そのような論理式の存在だけを述べ、特定の一つを選びません。

```agda
      (FreeAt-out C₀ s a γ k qa h))
```

逆に `codeFree-in` は、アリティ `suc k` の具体的な無パラメータ論理式 `χ` と、その極限段階の符号を骨格位置の値と同定する等式から始めます。補題 `freeCode-in` は対応するキーを `AllCodes ∅ʟ` に入れます。次に符号の等式と `q₀` の逆向きに沿って移送すると、その所属は実際の骨格位置と符号集合位置に移ります。最後に `FreeAt-in` が、得られた所属を二つの存在証人とともにまとめます。この方向では `χ` 自身が入力として与えられているため、命題的に切り詰められた論理式の証人を作る必要はありません。

```agda
  codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
              → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  codeFree-in χ q = FreeAt-in C₀ s a γ k qa
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀)
      (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)
```

アリティのスロットと空のアルファベットの符号集合のスロットを同定すれば、`codeFree-out` と `codeFree-in` がそろって `FreeAt` の意図した読みを与えます。外向きには、骨格が `suc k` 個の変数をもつ無パラメータ論理式の符号であることが、命題的切り詰めのもとで得られます。内向きには具体的な論理式が初めから与えられているので、そのような切り詰めは要りません。これで名前の論理式を認識できました。次の問いは、その有限なパラメータ環境が数 `k` をどのように記録するかです。

```agda
        (freeCode-in (suc k) χ)))
```

## 列の長さを読む

まず、集合として符号化されたグラフへの任意の所属を特徴づけます。`g` が `Fin k` で添字づけられ、`pr x y` が `env g` に属するなら、`x ≡ # (toℕ i)` かつ `y ≡ g i` となる添字 `i` が単に存在します。階層の集合への所属が記録するのは、生成元となる項目の単なる存在だけなので、結果は命題的切り詰めのもとに留まります。したがって `memberOf` は可能な添字を明らかにしますが、その一つを選び出しはしません。

```agda
private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = PT.map
    (λ { (li , e) → lower li
```

所属の証人は、グラフに格納された項目と問い合わせた順序対との等式を含みます。順序対の構成子の単射性により、この一つの等式は二つの成分の等式に分かれます。証人では格納された項目が先に書かれているため、両方の成分のパスを逆向きにして、`memberOf` が必要とする向きにします。すなわち、`x` と `y` から、それぞれ数項の鍵と `g` の与える値へ向かう等式です。

```agda
       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })
```

逆に、指定された各添字は一つの項目を与えます。`i : Fin k` に対して、順序対 `pr (# (toℕ i)) (g i)` は `env g` に属します。持ち上げられた添字が所属の証人となり、項目の等式は反射性です。こうして `memberOf` と `entryOf`は、この有限グラフの第一成分を認識するために必要な二つの向きを与えます。

```agda
  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁
```

定義域の順向きの包含は、`pr x (fst y)` がグラフに入るようなモデルの元`y` が単に存在することから始まります。目標は所属命題 `x ∈ # k` なので、外側の命題的切り詰めをこの目標へ消去できます。代表 `y` を一つ固定した後は、グラフへの所属から添字を復元し、その数項が `# k` に属することを示せば十分です。

```agda
  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))
```

具体的な添字 `i` に対して、定義域が必要とするのは第一成分の等式だけです。`toℕ i < k` なので、数項に関する補題 `#mono` は `# (toℕ i)` を `# k` に入れます。さらに `x ≡ # (toℕ i)` に沿って輸送すれば、`x` もそこに属します。第二成分の等式はグラフの値を同定しますが、この包含には不要です。補助関数`atEntry` は値 `y` を固定してから、残る切り詰められた添字の情報を消去します。

```agda
            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))
```

グラフへの所属に `memberOf` を適用すると、必要な添字の情報がちょうど得られますが、それはまだ命題的切り詰めのもとにあります。`x ∈ # k` は命題なので、`PT.rec` は各代表を `atIndex` に渡せます。これで添字を通常のデータとして取り出すことなく、順向きの包含が閉じます。

```agda
      (memberOf k g x (fst y) p)
```

逆向きの包含では `x ∈ # k` と仮定します。von Neumann 数項の消去により、ある自然数 `m < k` について `x ≡ # m` であることが、命題的切り詰めのもとで得られます。そのような `m` は `Fin k` の添字を定めます。結論もグラフの値の存在を命題的に切り詰めたものなので、`PT.map` はいずれかを選ぶことなく、各数項の証人を変換できます。仮定 `cg` は、その値をモデルの元として提示するために必要な構成可能性の証明を供給します。

```agda
  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩
  dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))
```

代表 `m < k` に対し、`i` を対応する有限添字とします。存在量化の証人はモデルの元 `(g i , cg i)`、すなわちその添字での値と構成可能性の証明です。グラフについての事実は `entryOf` から得られます。標準的な第一成分`# (toℕ i)` をもつ対が一つの項目だからです。この第一成分を `x` へ輸送すれば、`pr x (g i)` がグラフに属するという必要な所属が得られます。

```agda
              → Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k
```

変換 `fromℕ' k m p` は境界の証明 `p : m < k` から添字 `i` を作ります。その往復則 `toFromId'` は `toℕ i ≡ m` を証明します。`x ≡ # m` と、往復の等式を逆向きにして数項へ写したパスとを合成すると、`qi : x ≡ # (toℕ i)` が得られます。これは標準的な項目を問い合わせた第一成分へ移すためのパスそのものです。これで定義域の逆向きの包含も完成します。

```agda
      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))
```

これで、二つの集合レベルの包含を対象言語の定義域の論理式と対応させられます。環境 `γ`、族 `g : Fin k → V ℓ`、そしてスロット `e` の台集合を `env g` と同定する等式 `qe` を固定し、スロット `d` は定義域の候補として残します。各 `cg i` は `g i` が構成可能モデルの元であることを証明します。これは逆向きの包含が存在の証人を作るときに、まさに必要となる条件です。この文脈で、次の二つの補題が `domAt e d` を読み出し、また充填します。

```agda
module _ {n : ℕ} (e d : Fin n) (γ : S ^ n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : fst (lookup e γ) ≡ env g) where
```

`γ` が `domAt e d` を充足すると仮定します。スロット `d` の台集合が`# k` であることを示すため、`domAt-numeral` はモデルの元 `lookup d γ` と`(# k , numL k)` に `L` 内部の外延性を適用し、得られた等式を台集合へ射影します。したがって、構成可能な各試験要素 `x` について、定義域の候補への所属と数項への所属が同じ命題であることを示せば十分です。順向きの含意は、まず `domAt-in` によって定義域への所属を読み出します。

```agda
  domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k
  domAt-numeral h = cong fst (extensionalL {a = lookup d γ} {b = # k , numL k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ fst x ∈ # k ⟩
    fwd x hx = dom-into k g (fst x)
```

順向きの含意では、`domAt-in` がスロット `d` への所属を、`x` と対をなしてスロット `e` の集合に入る値の単なる存在へ変えます。`qe` に沿って輸送するとその項目は `env g` に入り、`dom-into` が `x ∈ # k` を与えます。逆に、`dom-from` は `x ∈ # k` を `env g` の項目の単なる存在へ変えます。定義域の候補への所属は命題なので、この切り詰めを消去できます。局所関数 `put` が、提示された各項目を処理します。

```agda
      (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe
        (domAt-in e d γ h x hx))
    bwd : (x : S) → ⟨ fst x ∈ # k ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup d γ))) put (dom-from k g cg (fst x) hx)
      where
```

提示された一つの項目について、`put` はその所属を `qe` の逆向きに沿ってスロット `e` に格納されたグラフへ戻し、`domAt-out` によって第一成分のスロット `d` への所属を得ます。こうして二つの含意は `⇔toPath` により、各 `x` で二つの所属命題の間のパスになります。外延性はそれらの点ごとのパスを、定義域の候補と `# k` との等式へ組み立てます。切り詰められたグラフの証人は所属を証明するためだけに用いられ、そこから値を選び出すことはありません。

```agda
      put : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ env g ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
      put (y , p) = domAt-out e d γ h x y
        (subst (λ u → ⟨ pr (fst x) (fst y) ∈ u ⟩) (sym qe) p)
    pt : (x : S) → (fst x ∈ fst (lookup d γ)) ≡ (fst x ∈ # k)
    pt x = ⇔toPath (fwd x) (bwd x)
```

逆向きは、スロット `d` の集合が実際に `# k` であるという等式から始まります。`domAt e d` を示すために、`domAt-intro` は定義域を規定する二つの含意を各要素について要求します。グラフに値が単に存在すれば `d` に属し、`d` に属すればグラフに値が単に存在する、という二つです。等式 `qe` と `qd`によって、これらはそれぞれ `dom-into` と `dom-from` に帰着します。したがって論理式の充填には、読み出しで用いた二つの集合レベルの包含を逆向きにして、そのまま用います。

```agda
  domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩
  domAt-fill qd = domAt-intro e d γ step
    where
    step : (x : S)
         → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩
```

定義域の論理式を充足させるには、各点で二つの含意を示せば十分です。まず、ある値と `fst x` の対がスロット `e` のグラフに属するとします。`qe` に沿って輸送すると、この項目は `env g` に入り、`dom-into` によって `fst x` が数項 `# k` に属することが分かります。さらに `qd` を逆向きに使って輸送すれば、スロット `d` の定義域候補への所属が得られます。

```agda
            → ⟨ fst x ∈ fst (lookup d γ) ⟩)
         × (⟨ fst x ∈ fst (lookup d γ) ⟩
            → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩)
    step x =
        (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)
```

逆向きの含意は、同じ道筋を反対にたどります。スロット `d` への所属を `qd` によって `# k` への所属へ移し、`dom-from` から、`fst x` と対をなして `env g` に入る値の単なる存在を得ます。最後に `qe` の逆向きに沿って、その項目をスロット `e` へ戻します。これで `domAt-fill` の二方向がそろい、有限グラフから特定の値を選び出す必要はありません。

```agda
          (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe hy)))
      , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) (sym qe)
          (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))
```

## 充足関係グラフが割り当てる値

次に、充足関係グラフが実際の論理式の鍵で何を割り当てるかを調べます。周囲の環境 `γ` を固定し、スロット `B` から台を、`x` と `y` から鍵と値の候補を受け取ります。略記 `Bs = lookup B γ` により、以下の証明はこの三つのスロットについて一様に述べられます。ここで扱う論理式の定数は、台集合 `fst Bs` の要素によって添字づけられます。

```agda
module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where
  private
    Bs : S
    Bs = lookup B γ
```

グラフの論理式は、十四個の束縛されたスロットを通して充足関係の再帰をまとめます。モデル言語の論理式 `φ` に対し、`fr φ` はそれらのスロットへ、台 `Bs`、その正準な充足関係表、子論理式の鍵からなるスロット、環境の塔、そして十個の構成子タグの数項を順に置き、その後ろに周囲の環境 `γ` を続けます。どの成分も、この台と論理式についてすでに構成された正準な対象です。

```agda
    fr : ∀ {m} (φ : Formula S m) → S ^ (14 + n)
    fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
```

この十個の数項は符号領域の添字ではなく、表の仕様にある零から九までの十個の構成子節を表すタグです。`tgs φ` は、`fr φ` の各タグ用スロットが対応する構成子の数項をもつことを記録します。この対応により、まとめられた表の論理式は各構文の形に適切な節を選べます。

```agda
    tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN
    tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
```

充足関係表には、各アリティに対応する正しい環境の族も必要です。`htow φ` は、すでに得られている塔の定理を `fr φ` の各成分に適用します。塔のスロットには `Tower.tower Bs`、台のスロットには `Bs`、零番のタグ用スロットには必要な数項が入っています。したがって拡張された環境で `towerAt` が成り立ち、ここで塔について新たな議論を行う必要はありません。

```agda
    htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩
    htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl
```

正準な表の定義域は、論理式の鍵からなるスロットと一致します。一方では表の項目から始め、`inSlot` によってその鍵を `slot Bs φ` に入れます。項目は命題的切り詰めのもとで得られるので、その消去先は所属命題です。他方では `total` を使い、スロット内の各鍵に表の値が単に存在することを示します。`domAt-intro` がこの二つの含意を `hdom φ` にまとめます。

```agda
    hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩
    hdom φ = domAt-intro Ti Ci (fr φ)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ)))
                 (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h)
           , (λ h → total Bs φ (fst z) h))
```

これで順方向の読みを正確に述べられます。`ψ` を、定数が `fst Bs` の要素である論理式とします。スロット `x` が実際の鍵 `keyS Bs ψ` をもち、スロット `y` がモデル言語へ移した論理式 `mapFo (asConst Bs) ψ` の充足集合をもつなら、`satGraphAt B x y` が成り立ちます。この値は論理式を充足する環境の集合であり、一つの真理値ではありません。`graphAt-value` は正準な再帰の証人を `graphAt-in` に与えて、この主張を示します。

```agda
  graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
                → fst (lookup x γ) ≡ fst (keyS Bs ψ)
                → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
                → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-value {m} ψ qx qy = graphAt-in B x y γ
```

存在の証人は `GraphWitAt` が要求する順に、五つの正準な成分から組み立てられます。数項の割り当て `numν`、塔、スロット、充足関係表、そして台です。証人全体は、グラフの論理式における存在量化の意味に合わせて命題的切り詰めで包まれます。残るのは、選んだ成分が台、タグ、塔、閉包、定義域、項目、表の仕様を満たすことの確認です。

```agda
    ∣ numν
    , (Tower.tower Bs
    , (slot Bs φ
    , (satTable Bs φ
    , (Bs
```

台についての等式は反射性です。続く三つの証明は、十個のタグ用スロットが所定の数項をもち、環境のスロットが `Bs` 上の塔であり、`slot Bs φ` が直下の子論理式をもつ構成子について閉じていることを示します。最後の性質により、再帰的な表の節は、複合論理式の鍵で直下の子論理式の鍵にある項目を参照できます。

```agda
    , (refl
    , (tgs φ
    , (htow φ
    , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
```

最後の三つの条件は、表の定義域、選んだ項目、そして構成子節の仕様を確定します。すでに示した `hdom φ` が定義域の論理式を与えます。表の項目については、`keyBridge Bs ψ` が台の言語の論理式と `φ` の鍵を結び、`qx` と `qy` が正準な項目をスロット `x` と `y` の鍵と値へ輸送します。最後に `SlotHolds.holds` が、同じ台、タグ、塔、スロット、表から、正準な表が `tableAt` を充足することを示します。これで組み立てた証人がグラフの論理式を確立します。

```agda
    , (hdom φ
    , (subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩)
         (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
    , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁
    where
```

ここで `φ` は `ψ` をモデル言語へ移したものです。`ψ` の定数は台集合の要素であり、`asConst Bs` はそれに、`S` の要素とみなすために必要な構成可能性の証明を添えます。`mapFo` はこの定数写像を論理式全体に適用します。上で別に用いた `keyBridge` により、翻訳前に直接符号化した鍵と、翻訳後にモデル内部で符号化した鍵の台集合が一致します。

```agda
    φ : Formula S m
    φ = mapFo (asConst Bs) ψ
```

逆方向では、`satGraphAt B x y` が成り立ち、スロット `x` が `ψ` の実際の鍵であると仮定します。`graphAt-out` が十四個の存在成分を与えるのは、命題的切り詰めのもとだけです。求める結論は累積階層 `V` における等式であり、`setIsSet` によってその等式型は命題です。したがって `PT.rec` は、グラフの証人を大域的に選ぶことなく、提示された各証人を局所的に調べられます。

```agda
  graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
               → fst (lookup x γ) ≡ fst (keyS Bs ψ)
               → ⟨ γ ⊨ satGraphAt B x y ⟩
               → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
  graphAt-only {m} ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)
```

一つのグラフの証人をほどくと、表の候補 `T`、符号領域 `C`、環境の塔 `E`、台 `b`、およびそれらの証明が得られます。ここで `C` が正準なスロットである必要はありません。必要なのは、`C` が子符号について閉じ、`T` がまとめられた表の節を充足し、実際の鍵が `C` に属することです。最後の所属は、提示された表の項目 `ha` に `domAt-out` を適用して得られます。この鍵の所属と同じ表の項目を `SatSoundC.pinned` に渡すと、`ψ` について表に記録された値が正準な充足集合に定まります。

```agda
    where
    read : GraphWitAt B x y γ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
    read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) =
      SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12
        ψ (subst (λ u → ⟨ u ∈ fst C ⟩) qx
```

固定の定理に必要な二つの前提は、初めは周囲の環境のスロット `x` で読まれます。`qx` に沿って輸送すると、`hd` と `ha` から得た定義域への所属は `keyS Bs ψ` が `C` に属するという所属になり、`ha` 自身は、その鍵とスロット `y` の値における `T` の項目になります。そこで固定の定理が必要な等式を返します。実際の論理式の鍵では、グラフが許すどの値も、翻訳された論理式の充足集合に一致します。

```agda
             (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha))
        (lookup y γ)
        (subst (λ u → ⟨ pr u (fst (lookup y γ)) ∈ fst T ⟩) qx ha)
```

## 名前をスロット上で記述する

表示を定める本体は、候補 `z` を一つずつ調べます。最初の連言 `z ∈ B` は、記述される集合を台の内部に制限します。次に環境 `c` を束縛し、`c` がパラメータ環境 `e` の先頭に `z` を加えて得られる符号化環境であることを要求します。この時点では `c` と `z` が周囲の割り当ての前に置かれているので、`e` への参照は二つの束縛子を越えて移されます。

```agda
DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero
```

残る三つの証人は、骨格をどのように解釈するかを定めます。まず `k` が拡張環境 `c` の定義域であることを要求します。次に `key` はスロット `C` の符号集合に属し、`k` と骨格の符号 `s` の対に等しくなければなりません。最後に `v` は、台 `B` の充足関係グラフがその鍵で許す値であり、末尾の所属は `c ∈ v` を述べます。`C` に台の実際の符号集合が入ると、これらの条件は、任意の鍵でグラフを参照するだけではなく、拡張環境が骨格を充足することを表します。

```agda
            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )
```

メタ言語の名前は、アリティ、無パラメータ論理式、パラメータベクトルからなります。`NameAt` はそれらをアリティのスロット `a`、骨格の符号のスロット `s`、環境のスロット `e` で表し、表示のスロット `d` にはそのデータから導かれる集合を記録します。最初の連言は、`a` の後続と `s` から作った対が空のアルファベットの符号集合に属することを確かめます。この後続は欠かせません。`a` 個のパラメータをもつ名前には、候補となる要素を置く変数がもう一つ必要だからです。次の連言は、`a` がモデルの自然数の集合に属することを要求します。

```agda
NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  FreeAt C₀ s a
  ∧̇ ( (var a ∈̇ con ωʟ)
```

第三の連言は、`e` が定義域をちょうど `a` とし、`B` に値をとる環境であることを要求します。これにより、パラメータベクトルが一つ前のスロットに記録されたアリティと結び付きます。最後の連言は `d` を外延的に特徴づけます。各候補について、`d` への所属は `DenoteBody` の充足と同値であり、その本体の最初の連言がすでに候補を `B` の中に制限しています。したがって `d` は名前の三つのデータから導かれるもので、メタ言語の名前に追加で保存される成分ではありません。

```agda
    ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )
```

`DenoteOf z` は、`DenoteBody` の四層の存在量化に対応するメタ言語の中身です。拡張環境 `c`、その定義域の候補 `k`、論理式の鍵、グラフの値 `v` と、それらを結ぶすべての条件を記録します。これらを一つの依存対にまとめることで、対象言語の論理式を組み立てるのに必要な証人を明示しながら、後の条件が先に選んだ値に依存することも保たれます。

```agda
module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where
  DenoteOf : (z : S) → Type (ℓ-suc ℓ)
  DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
```

この中身は意味の連鎖をそのままたどります。最初の二つの充足の証明は、`c` がもとの環境を拡張することと、`k` がその定義域であることを述べます。`C` を `AllCodes B` で具体化すると、`key` が `C` に属するという条件により、続くグラフの参照が実際の論理式の符号で行われることが保証されます。次の明示的な等式は、その鍵を `k` と `s` の対と同一視します。最後の二つの証明は、`v` がこの鍵でのグラフの値であり、`c` が `v` に属することを述べます。ここで `v` は充足する環境の集合であって、ブール値の真理値ではありません。

```agda
      × ( ⟨ fst key ∈ fst (lookup C γ) ⟩
        × ( (fst key ≡ pr (fst k) (fst (lookup s γ)))
          × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
            × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )
```

`DenoteBody-in` は、この明示的な中身を本体の充足へ変えます。台への所属は外側の連言として残り、証人 `c`、`k`、`key`、`v` は四つの存在量化子と同じ順序で導入されます。ほとんどの条件は、初めから充足の証明として述べられています。例外は `key` を定める等式です。対の論理式の妥当性を表すパスが、この集合論的な等式を `prAtL` の充足へ変換します。

```agda
  DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z
                → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
  DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp
```

対象言語の各存在量化子は命題的切り詰めによって解釈されるので、この構成は証明を閉じる前に四つの証人を一層ずつ切り詰めます。最後の行は、グラフの値から拡張環境まで、この四層を内側から順に閉じます。したがって得られる充足が記録するのは適切なデータの存在であり、切り詰められていない証人は、構成に用いた入力 `DenoteOf z` の側にだけ残ります。

```agda
      , ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁
```

`DenoteBody-out` は、逆向きに読むときにも同じ境界を保ちます。台への所属はすべての存在量化子の外側にあるので、直接取り出せます。しかし四つの証人は、入れ子になった命題的切り詰めの内側でしか現れません。切り詰めの消去先は毎回 `∥ DenoteOf z ∥₁` であり、これも命題です。そのため、各局所的な証人の組を変換することはできますが、一つの組を大域的に選ぶことはありません。

```agda
  DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
                 → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁
  DenoteBody-out z (hz , hc) = hz , PT.rec squash₁
    (λ { (c , (hc , hk)) → PT.rec squash₁
      (λ { (k , (hk , hkey)) → PT.rec squash₁
```

鍵の層では、本体は対の論理式の充足を与えますが、`DenoteOf` が要求するのは、復号された等式 `fst key ≡ pr (fst k) (fst (lookup s γ))` です。対の論理式の妥当性を表すパスを順方向に読むと、ちょうどこの等式が得られます。最も内側の写像は、証人 `v` とともにグラフの証明と所属の証明を保ち、外側の消去が中身全体を一つの命題的切り詰めの下で組み立て直します。

```agda
        (λ { (key , (hi , (hp , hv))) → PT.map
          (λ { (v , (hg , hm)) → c , (k , (key , (v , (hc , (hk , (hi
            , ( subst ⟨_⟩
                  (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp
              , (hg , hm) ))))))) }) hv }) hkey }) hk }) hc
```

`NameAt-in` は五つの入力を取ります。最初の三つは固定された連言を示します。すなわち、骨格が指定されたアリティで無パラメータであること、アリティがモデルの自然数の集合に属すること、パラメータのグラフが台の上の環境であることです。残る二つは、表示を特徴づけるための点ごとの二方向を与えます。一方は `z ∈ d` から `z ∈ B` と明示的な `DenoteOf z` を返し、他方は `z ∈ B` と明示的な `DenoteOf z` から `z ∈ d` を導きます。

```agda
module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where
  NameAt-in : ⟨ γ ⊨ FreeAt C₀ s a ⟩
            → ⟨ fst (lookup a γ) ∈ ω ⟩
            → ⟨ γ ⊨ envOverAt e a B ⟩
            → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
```

二つの方向は、どちらも候補ごとに述べられます。`extAt` が集合の等しさを点ごとの所属で表すからです。ここでは意図的に、切り詰められていない `DenoteOf z` を使います。この補題は導入規則なので、呼び出す側が本体の充足を組み立てるための具体的なデータを与えます。`NameAt` の任意の充足からそのデータを復元する仕事は別の妥当性の議論に属し、次章で得られる復元結果も命題的切り詰めの下に残ります。

```agda
               → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z)
            → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
               → ⟨ fst z ∈ fst (lookup d γ) ⟩)
            → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
  NameAt-in hf ha he into back =
```

証明は、この二方向を `extAt` の導入規則へ渡します。`z ∈ d` からは、一方の入力が台への所属と中身を与え、`DenoteBody-in` がそれらを本体の充足へ変換します。逆に、本体の充足は `DenoteBody-out` によって、台への所属と命題的に切り詰められた中身として読まれます。目標の `z ∈ d` は命題なので、この切り詰めを消去してもう一方の入力を適用できます。こうして得た外延的な特徴づけを最初の三入力と組み合わせると、名前の論理式全体が充足されます。

```agda
    hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ
      (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd))
      (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ)))
                 (back z (DenoteBody-out B C s e γ z h .fst))
                 (DenoteBody-out B C s e γ z h .snd))))
```

## 再帰をもたない順序

続く比較の論理式はデータをまとまった束縛子で導入するため、周囲の割り当てへの参照を一様に移す必要があります。`sh3` は、周囲のスロットを三つの新しい束縛子の先へ移します。`LexAt` では、この三つに添字 `i` と、二つのパラメータ環境から `i` で読み出した値が入ります。その下でも、もとの二つの環境とパラメータ順序のスロットを参照できます。後の `LeastNameAt` でも同じ移動を使い、競合する名前の骨格、アリティ、環境を束縛した先へ周囲のスロットを運びます。

```agda
private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))
```

`sh6` は、対応する移動を六つの束縛子について行います。`StepBody` が二つの名前を束縛するときに使われ、各名前は骨格、アリティ、パラメータ環境によって表されます。そのため、完全に拡張された割り当てでは六つの新しい値がもとの割り当ての前に置かれますが、台、二つの順序関係、二つの符号集合、比較する二つの表示は周囲のスロットとして残ります。これらの移動は参照先を保つだけであり、順序の仮定を加えたり、それ自体で比較を行ったりはしません。

```agda
  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = suc (suc (suc (suc (suc (suc i)))))
```

パラメータの鍵は、二つのパラメータ環境が最初に異なる位置を求めます。`LexAt` はまず、アリティのスロットにある集合の元 `i` を束縛します。そのスロットにアリティの数項が入っていれば、その元はちょうど、それより小さい位置を表す数項です。したがって、この有界存在量化子だけで可能な添字をすべて動かせ、添字のための別の順序は必要ありません。

```agda
LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
LexAt P a e₁ e₂ =
  ∃̇∈ (var a) (
    ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero)
           ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero
```

`i` を選ぶと、続く二つの存在量化子が値 `u` と `v` を与え、`e₁(i)=u` と `e₂(i)=v` を述べます。第三の適用は、`u` と `v` の順序対がパラメータ関係 `P` に属すことを主張します。次の有界全称量化子は各 `j ∈ i` を調べ、それぞれについて、二つの環境グラフがともに `j` で取る値 `x` が単に存在することを要求します。したがって論理式の内容は、「この位置では厳密に小さく、それ以前の各位置では共通の値をもつ」です。共通の値から対応するパラメータの等しさを導けるのは、二つの環境を一価なグラフと同定した後です。後の妥当性証明では、グラフの参照に関する性質と台の埋め込みの単射性が、まさにこの含意を与えます。論理式そのものは再帰を行いません。

```agda
             ∧̇ ( appAt (sh3 P) (suc zero) zero
               ∧̇ ∀̇∈ (var (suc (suc zero))) (
                    ∃̇ ( appAt (sh5 e₁) (suc zero) zero
                      ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )
```

名前全体の比較は、骨格の符号、アリティ、パラメータ環境という三つの鍵を辞書式の優先順位で組み合わせます。第一の選言は、スロット `R` の関係を `s₁` と `s₂` に適用します。適用の妥当性により、これは二つの骨格の符号からなる順序対が `R` に属すという意味です。`R` をスロットのままにすることで、同じ論理式を異なる割り当てに使えます。後の妥当性定理では、極限段階の符号順序を表す関係がここに入ります。

```agda
≺At : ∀ {n} → Fin n → Fin n
    → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n
≺At R P s₁ a₁ e₁ s₂ a₂ e₂ =
      appAt R s₁ s₂
  ∨̇ ( (var s₂ ≐ var s₁)
```

第二の選言は、骨格の符号が等しい場合を扱います。まず等しさを `s₂ = s₁` の向きで記録し、その後に残る二つの辞書式の場合を並べます。両方のアリティのスロットが数項なら、`a₁ ∈ a₂` は第一のアリティが小さいことを意味します。もう一つの分岐は `a₂ = a₁` を要求し、`LexAt P a₁ e₁ e₂` が最初に異なるパラメータで比較を決めます。`s₂ = s₁` と `a₂ = a₁` という向きは、第二の名前の符号とパラメータベクトルを第一の名前のデータへ移す、後の輸送の向きに合っています。

```agda
    ∧̇ ( (var a₁ ∈̇ var a₂)
      ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )
```

`LexAt` の読みを繰り返し使える形で証明するため、一致を述べる存在量化子の下にある本体を取り出して名前を付けます。先行する位置 `j` で、`Body` は同じ値 `x` が二つの適用をともに満たすこと、すなわち二つの環境グラフがともに `j` で値 `x` をもつことを要求します。拡張された割り当てには `x`、`j`、`v`、`u`、`i` の五項が新しく並ぶので、周囲の環境スロットへの参照は五つの束縛子を越えて移されます。

```agda
module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where
  private
    Body : Formula S (suc (suc (suc (suc (suc n)))))
    Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero
```

`i`、`u`、`v` を固定すると、`Inner i u v` は最初の三つの存在束縛子の後に残る本体を記録します。最初の二成分は、グラフ `e₁` と `e₂` がそれぞれ対 `(i,u)` と `(i,v)` を含むことを述べます。第三の成分は、対 `(u,v)` が関係 `P` に属すことを述べます。これらはまだ `appAt` の充足を表す主張です。二つの表示を明示的に結べるように、解読後の所属の形は別に記録します。

```agda
    Inner : (i u v : S) → Type (ℓ-suc ℓ)
    Inner i u v =
      ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩
      × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩
        × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩
```

`Inner` の第四成分は、`i` より下での一致です。`i` に属するモデルの各要素 `j` に対し、一つの `x` が `Body` を満たすという意味論上の存在式 `∃[ x ∶ S ]` を与えます。この存在式は命題的切り詰めです。`j` で共通の値が存在することは保ちますが、選ばれた値をデータとして外へ出しません。したがって有界全称量化子は、各 `j ∈ i` に対して、そのように切り詰められた存在を一つ与える関数として読まれます。

```agda
          × ((j : S) → ⟨ fst j ∈ fst i ⟩
             → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩) ) )
```

`Agrees i` は、二つの適用を解読した形で同じ一致を述べます。各 `j ∈ i` について、`j` と `x` の底にある集合から作った対がグラフ `e₁` と `e₂` の両方に属すような元 `x : S` が単に存在します。`i` がアリティの数項なら、その元はちょうど先行する位置を表します。この定義が記録するのは共通のグラフ値だけです。対応するメタレベルのパラメータの等しさは、既知の環境グラフと台の埋め込みの単射性から後で導かれます。

```agda
  Agrees : (i : S) → Type (ℓ-suc ℓ)
  Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩
           → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                          × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁
```

`Differs` は、最初の相違を示す証人を解読した完全な形でまとめます。添字 `i`、値 `u` と `v`、アリティのスロットにある集合への `i` の所属、対 `(i,u)` と `(i,v)` のグラフへの所属、その位置での厳密なパラメータ比較、そして `Agrees i` が含まれます。アリティのスロットが数項で、二つのグラフのスロットがそのアリティのパラメータ環境なら、これらは辞書式の最初の相違に必要なデータそのものです。

```agda
  Differs : Type (ℓ-suc ℓ)
  Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ]
    ( ⟨ fst i ∈ fst (lookup a γ) ⟩
    × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩
      × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩
```

厳密な比較のフィールドは、`≺At` の符号の場合と同じ関係の形を取ります。`u` と `v` の底にある値から作った順序対が、スロット `P` の集合に属すという形です。最後の `Agrees i` は、それ以前の各位置で共通の値があることを記録します。意図した一価な環境グラフについては、これが、それ以前のパラメータに相違がないことを保証します。こうして `Differs` は、最初の相違を示す証人の数学的内容を、それを表す対象言語の束縛構造から分けて記録します。

```agda
        × ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )
```

写像 `pack` が変換するのは、`Inner` の一致の成分だけです。最初の三成分は、この局所的な変換には使いません。`j ∈ i` を固定すると、意味論上の存在式の証人 `x` には、`appAt` を充足する二つの証明が伴います。それぞれに `appAt-adequate` を適用すれば、同じ証人 `x` を保ったまま、`Agrees` が要求する二つのグラフ所属が得られます。

```agda
  private
    pack : (i u v : S) → Inner i u v → Agrees i
    pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩
```

この変換は、すでにある命題的切り詰めの内部で行われます。`PT.map` は、可能な各証人と二つの適用の証明を、同じ証人と二つの所属の証明へ写します。目標も切り詰められた存在なので、代表を取り出す必要はなく、選択原理も使いません。各点で写すだけで、すべての先行する位置について `Agrees i` に必要な結論が得られます。

```agda
               (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁
           , subst ⟨_⟩
               (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) })
      (hj j hj')
```

`unpack` は、もとの論理式を充足するために必要な逆向きの変換を与えます。`Agrees i` と位置 `j ∈ i` から、切り詰められた共通値の証人を受け取ります。それぞれの代表 `x` をそのまま保ち、二つのグラフ所属を `Body` にある二つの適用の充足へ戻します。

```agda
    unpack : (i u v : S) → Agrees i
           → (j : S) → ⟨ fst j ∈ fst i ⟩
           → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩
    unpack i u v hj j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
```

ここでは同じ妥当性のパスを逆向きに使います。各所属の証明を `appAt-adequate` の対称なパスに沿って輸送すると、`Body` の対応する連言が得られます。ここでも `PT.map` によって構成全体が切り詰められた存在の内部に留まるため、`unpack` は共通の値を大域的に選ぶことなく、必要な意味論上の存在を証明できます。

```agda
         , ( subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁
           , subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) })
      (hj j hj')
```

`LexAt-in` は、`Differs` にある明示的なデータから始めます。添字 `i` と値 `u`、`v` は、有界存在量化子と、それに続く二つの存在量化子の証人になり、`hi` が `i` が限界内にあることを証明します。拡張された割り当て `γ₃ = v ∷ u ∷ i ∷ γ` では、最初の二つのグラフ所属を `appAt-adequate` に沿って逆向きに輸送し、`e₁(i)=u` と `e₂(i)=v` を表す二つの適用を充足させます。残る関係と一致のフィールドも同じ連言構造に入り、有界全称の成分は `unpack` が与えます。

```agda
  LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩
  LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj)))))))
    = ∣ i , (hi , ∣ u , ∣ v
    , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁
      , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂
```

`Differs` の最後の二つの成分が導入の証明を完成させます。`(u,v)` が `P`に属すという証明を `appAt-adequate` に沿って逆向きに輸送すると、第三の適用についての充足関係の証明になり、`unpack` は `i` より前での一致を有界全称量化子の意味論的な形へ変えます。割り当て`γ₃ = v ∷ u ∷ i ∷ γ` は三つの束縛の順序を明示しており、周囲の構成子が`v`、`u`、`i` の存在量化子を内側から順に閉じます。

```agda
        , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp
          , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁
    where
    γ₃ : S ^ (suc (suc (suc n)))
    γ₃ = v ∷ u ∷ i ∷ γ
```

`LexAt` を外向きに読むときは、その存在量化子が設けた証人の境界を保たなければなりません。そのため `LexAt-out` の行き先は命題 `∥ Differs ∥₁` であり、外側の切り詰めはこの行き先の中へだけ消去されます。局所関数 `atValue` が実際の数学的な復号を担います。各消去の局所的な範囲で、具体的な `i`、`u`、`v`、境界の証明、残りの充足関係のデータが得られれば、切り詰められていない`Differs` の記録を作れます。その記録を局所的な範囲の外へ選び出すことはありません。

```agda
  LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁
  LexAt-out = PT.rec squash₁ atIndex
    where
    atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs
    atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v
```

`atValue` の前半は、添字と二つのグラフ参照を復元します。境界の証明 `hi`は、すでに `Differs` が要求する形です。二つの妥当性のパスを順方向に読むと、適用についての充足関係は、`(i,u)` の `e₁` への所属と `(i,v)` の `e₂` への所属にそれぞれ変わります。したがって二つの値は、論理式がそれらを見つけた同じ添字に結び付いたままです。

```agda
      , ( hi
        , ( subst ⟨_⟩
              (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁
          , ( subst ⟨_⟩
                (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂
```

第三の適用も同じように復号され、`(u,v)` がパラメータ関係 `P` に属すことが得られます。関数 `pack` は、有界な範囲で適用の形を取っていた一致を`Agrees i` が要求する二つのグラフ所属へ翻訳し、最後の成分を与えます。これらのデータは `atValue` の内部で明示的な `Differs` の記録をなしますが、周囲の消去が最終的に保つのはその命題的切り詰めだけです。

```agda
            , ( subst ⟨_⟩
                  (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp
              , pack i u v h ) ) ) ) ))
```

最も内側の存在量化子は、第二の値 `v` と `Inner i u v` を与えますが、両者を使えるのはその切り詰めの内部だけです。処理関数 `atSecond` は、局所的に得られた各組 `(v,h)` から `atValue` で `Differs` を作り、ただちに`∥ Differs ∥₁` へ入れます。これは命題的切り詰めに許された消去そのものです。証人は命題を証明するために使われますが、結果から外へ現れることはありません。

```agda
    atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
             → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁
    atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁
```

一つ外の層で、`atFirst` は具体的な第一の値 `u` と、第二の値の存在を切り詰めたものを受け取ります。その内側の切り詰めを `atSecond` で消去すると、行き先は再び `∥ Differs ∥₁` です。したがって、第一の値から完成した最初の相違の記録へ進むあいだも、大域的に使える `v` を取り出す必要はありません。

```agda
    atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
            → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁
    atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h
```

最後に `atIndex` は、添字 `i`、それがアリティより小さいことを示す `hi`、そして `u` から始まる残りを切り詰めたものを受け取ります。その残りを`atFirst` で消去すれば、外向きの読みは完成します。三つの処理関数は合わせて、`i`、`u`、`v` という存在量化子の入れ子をたどり、どの消去も同じ命題を行き先とします。したがって `LexAt-out` が示すのは、最初の相違の記録が単に存在することだけであり、その添字や値を選ぶことではありません。

```agda
    atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩
                         × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ )
            → ∥ Differs ∥₁
    atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h
```

## 比較と順序族の一ステップを読む

メタレベルの中身 `Below` は、三つの比較の鍵を `≺At` と同じ優先順位で並べます。外側の直和は、骨格の符号からなる順序対 `(s₁,s₂)` がスロット `R` の関係に属すか、または符号が等しく、後の鍵が比較を決めることを表します。この直和の要素は、どの枝に入るかを明示してその証拠を運びますが、任意のスロットの値について枝を判定できると主張する定義ではありません。この区別が必要なのは、対象言語の選言が命題的切り詰めによって解釈されるからです。

```agda
module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where
  Below : Type (ℓ-suc ℓ)
  Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩
        ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
```

骨格の符号が等しい場合、内側の直和はまずアリティの比較 `a₁ ∈ a₂` を提示します。二つのスロットがアリティの数項を含むとき、この所属は第一のアリティのほうが小さいことを意味します。アリティも等しければ、`Differs` がパラメータの鍵について最初の相違の証拠を与えます。二つの等しさは意図的に `s₂ = s₁` と`a₂ = a₁` の向きに置かれ、後で第二の名前のデータを第一の名前の型へ輸送する向きに合っています。

```agda
            ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
              × Differs P a₁ e₁ e₂ γ ) ) )
```

`≺At-in` は、明示的な `Below` のデータを比較の論理式の充足関係へ翻訳します。符号の枝では、関係への所属を `appAt-adequate` に沿って逆向きに輸送し、外側の左の選言として導入します。アリティの枝では、符号の等しさとともに外側の右の選言へ入り、アリティの所属を内側の左の選言へ入れます。ここで行うのは導入だけです。与えられた枝の証拠を、対象言語の各選言に伴う切り詰められた意味へ包みます。

```agda
  ≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
  ≺At-in (inl h) =
    ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁
  ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁
  ≺At-in (inr (q , inr (q' , h))) =
```

パラメータの枝は、二つの選言の右側を順に進みます。符号とアリティの等しさをそれぞれの右の枝へ運び、与えられた `Differs` の記録を `LexAt-in` に渡します。こうして、すでに復号された最初の相違のデータがパラメータの節の充足関係になります。したがって `Below` の三つの場合はすべて、枝を探索したり存在証人を取り出したりせずに `≺At` へ導入できます。

```agda
    ∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁
```

逆向きの読みの行き先は、必然的に弱い `∥ Below ∥₁` です。外側の対象言語の選言についての充足関係自体が切り詰められているため、`PT.rec` が枝を調べられるのは、この命題を構成する局所的な範囲に限られます。局所関数 `outer` は符号の場合と符号が等しい場合を分けます。後者では等しさ `s₂ = s₁` を保ち、まだ分類されていない内側の選言を `inner` に渡します。

```agda
  ≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁
  ≺At-out = PT.rec squash₁ outer
    where
    inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
```

符号の等しさが与えられると、`inner` は残る二つの鍵を読みます。アリティの所属が得られれば、ただちに `Below` の中間の場合になります。もう一方の中身には、アリティの等しさ `a₂ = a₁` と `LexAt` の充足関係があり、復号すべきものは最初の相違の成分だけです。関数の型は、二つの場合に共通する符号の等しさを固定したまま、これらの選択肢を明示しています。

```agda
          ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
            × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ )
          → ∥ Below ∥₁
    inner q (inl h) = ∣ inr (q , inl h) ∣₁
    inner q (inr (q' , h)) =
```

パラメータの場合、`LexAt-out` が与えるのは `∥ Differs ∥₁` だけであり、存在の意味論が要求する境界を正確に保っています。`PT.map` は、その中で局所的に表された各 `Differs` の記録を `Below` の第三の場合へ写し、すでに得られた符号とアリティの等しさを付け加えます。結果は一つの命題的切り詰めの下に留まるので、この変換は存在を存在へ移すだけで、最初の相違の証人を選ぶことはありません。

```agda
      PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)
```

`outer` の型は、最初の比較の鍵で生じる意味論的な分岐をそのまま表します。左側は関係 `R` を二つの骨格のスロットへ適用した論理式の充足関係であり、右側は等しさ`s₂ = s₁` と、残る「アリティまたはパラメータ」の選言の充足関係を保ちます。左側を復号すれば `Below` の符号の場合が得られ、内側の選言の消去には `inner` を使います。この二段階の読みは `≺At` の入れ子に対応し、最終結果を`∥ Below ∥₁` に留めるので、どちらの選言も選ばれた枝として外へ出ません。

```agda
    outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩
          ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
            × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂)
                    ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ )
          → ∥ Below ∥₁
```

最後の二つの節で、比較を外向きに読む仕事が完了します。符号の場合には、`appAt-adequate` が関係の適用についての充足関係を、骨格の二つの符号からなる順序対が `R` に属すという主張へ変換し、`Below` の第一の場合を与えます。符号が等しい場合には、内側の対象言語の選言がなお命題的切り詰めの下にあるため、それを消去できる行き先は `∥ Below ∥₁` だけです。したがって三つの比較の鍵のどの場合も読み戻せますが、切り詰めの外で、どの鍵が比較を決めたかを取り出すことはありません。

```agda
    outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁
    outer (inr (q , h)) = PT.rec squash₁ (inner q) h
```

二つの最小の名前を比較する記述には、本体の中に六つの新しいスロットが必要です。ここでは最初の三つの添字を定めます。`s6a`、`a6a`、`e6a` はそれぞれ、第一の名前の骨格の符号、アリティの数項、パラメータ環境を指します。六つの束縛子をすべて通過した後では、これらは de Bruijn 添字の第五、第四、第三の位置にあります。位置に名前を付けておけば、後の最小性と比較の論理式を読みやすく保ちながら、束縛位置の計算を一か所に集められます。

```agda
private
  s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n))))))
  s6a = suc (suc (suc (suc (suc zero))))
  a6a = suc (suc (suc (suc zero)))
  e6a = suc (suc (suc zero))
```

残る添字 `s6b`、`a6b`、`e6b` は第二、第一、第零の位置を指し、そこに第二の名前のデータが置かれます。この反転は de Bruijn 表現に伴う通常の現象です。証人は `s₁,a₁,e₁,s₂,a₂,e₂` の順に束縛されますが、新しい証人はそのたびに環境の先頭へ加えられます。したがって、すべての束縛を加えた環境は `e₂ ∷ a₂ ∷ s₂ ∷ e₁ ∷ a₁ ∷ s₁ ∷ γ` となり、六つの添字が意図した二つの三つ組を正確に選びます。

```agda
  s6b = suc (suc zero)
  a6b = suc zero
  e6b = zero
```

最小の名前は、すでに `s`、`a`、`e` のスロットを占める名前のデータが満たす性質として表されます。第一の連言は、そのデータが `NameAt` を満たし、したがって `d` を表示することを要求します。第二の連言は、競合する骨格の符号、アリティの数項、パラメータ環境を全称量化します。三つの全称量化子は競合する三つ組を第二、第一、第零の位置に置き、`sh3` は台、二つの符号集合、表示 `d` への参照を元のスロットに保ちます。

```agda
LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n
            → Fin n → Fin n → Fin n → Fin n → Formula S n
LeastNameAt R P B C C₀ s a e d =
  NameAt B C C₀ s a e d
  ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)
```

含意の前件は、同じ `d` を表示する競合する名前だけに対象を限ります。別の集合を表示する名前は、この最小性には関係しません。後件は `≺At competitor current` を否定するので、`d` のどの競合する名前も、三つの鍵による順序で現在の名前に狭義に先行しません。この論理式は最小性を述べるだけです。名前を探索することも、命題的切り詰めを消去して一つを選ぶこともありません。明示的な最小の名前の構成はメタ言語の命名理論に属し、そこで排中律の仮定を用います。

```agda
                      (suc (suc zero)) (suc zero) zero (sh3 d)
             ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                        (sh3 s) (sh3 a) (sh3 e)) )))
```

存在量化子を繰り返し消去するときには、証人を大域的に選ぶことなく、その証人が携える性質を変換する必要があります。補助関数 `exists-map` は、まさにこの操作を表します。各 `B x` から単に `C x` が得られるなら、対 `(x , B x)` が単に存在することから、対 `(x , C x)` が単に存在することが従います。外側の `PT.rec` は元の命題的切り詰めを別の命題的切り詰められた型へ消去し、内側の `PT.map` は同じ `x` を保ったまま第二成分を変換します。結果が `A` の特定の証人を外へ示すことはありません。

```agda
private
  exists-map : {A : Type (ℓ-suc ℓ)} {B C : A → Type (ℓ-suc ℓ)}
             → ((x : A) → B x → ∥ C x ∥₁)
             → ∥ Σ A B ∥₁ → ∥ Σ A C ∥₁
  exists-map f = PT.rec squash₁ (λ { (x , h) → PT.map (x ,_) (f x h) })
```

演算子 `∃₆` は、任意の本体の外側で六つの対象言語の変数を順に束縛します。これは二つの名前に必要な二組の三つ組を与えるために使われますが、演算子自体は名前、最小性、順序のいずれにも言及しません。この束縛の枠を独立させることで、自由な位置が六つ多い任意の論理式について、意味論的な導入と消去の読みを一度だけ与えられます。証人に課される数学的条件は、後で `StepBody` が与えます。

```agda
∃₆ : ∀ {n} → Formula S (suc (suc (suc (suc (suc (suc n)))))) → Formula S n
∃₆ φ = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ φ)))))
```

本体 `φ` と環境 `γ` に対して、`Six` は六つの存在量化子を導入するための、切り詰められていないデータを記録します。それは六つの証人 `s₁,k₁,p₁,s₂,k₂,p₂` と、`φ` の充足関係です。`k` と `p` という文字は、後にそれぞれアリティの数項とパラメータ環境として使われることを先取りしています。この一般的な定義の段階では、いずれも台 `S` の要素にすぎません。束縛子は新しい証人を順に環境の先頭へ加えるため、充足関係の環境では順序が反転し、元の `γ` の前に `p₂,k₂,s₂,p₁,k₁,s₁` と並びます。

```agda
module _ {n : ℕ} (φ : Formula S (suc (suc (suc (suc (suc (suc n))))))) (γ : S ^ n)
         where
  Six : Type (ℓ-suc ℓ)
  Six = Σ[ s₁ ∈ S ] Σ[ k₁ ∈ S ] Σ[ p₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ k₂ ∈ S ] Σ[ p₂ ∈ S ]
          ⟨ (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) ⊨ φ ⟩
```

導入の読みは、六つの証人がすべて明示された `Six` の値から始まります。それらを束縛の順に六つの存在量化子へ渡し、残る充足関係の証明を、各存在量化子がもたらす命題的切り詰めの中へ一層ずつ包みます。証人は入力データとしてすでに与えられているので、探索も選択も必要ありません。入れ子になった構成子から、本体が見る環境が `Six` の定義に記された逆順になる理由も読み取れます。

```agda
  ∃₆-in : Six → ⟨ γ ⊨ ∃₆ φ ⟩
  ∃₆-in (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , h)))))) =
    ∣ s₁ , ∣ k₁ , ∣ p₁ , ∣ s₂ , ∣ k₂ , ∣ p₂ , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
```

外向きの読みは、六重の存在量化についての充足関係から始まり、切り詰めの外に現れた六つ組ではなく `∥ Six ∥₁` を行き先とします。`exists-map` を一度使うたびに存在量化子を一層通過し、その層で局所的に得られた証人を共通の命題的な行き先の内側に保ちます。この連鎖は `s₁`、`k₁`、`p₁`、`s₂`、`k₂` を順に扱います。最も内側では、`PT.map` が `p₂` と本体の充足関係の証明からなる対を、同じ最終的な切り詰められた中身へ送ります。

```agda
  ∃₆-out : ⟨ γ ⊨ ∃₆ φ ⟩ → ∥ Six ∥₁
  ∃₆-out = exists-map (λ s₁ →
    exists-map (λ k₁ →
      exists-map (λ p₁ →
        exists-map (λ s₂ →
```

五回目の `exists-map` の後では、最も内側の存在量化が最後の成分に必要な形をすでにもつため、恒等写像で十分です。`∃₆-in` と `∃₆-out` は合わせて、束縛の枠の意味論的内容を正しい非対称性のもとで表します。明示的な六つの証人のデータから論理式を導入できますが、論理式の充足関係から得られるのは、そのようなデータが単に存在することだけです。これで、六つの切り詰めを開き直すことなく、この一般的な結果を具体的な本体へ適用できます。

```agda
          exists-map (λ k₂ → PT.map (λ p → p))))))
```

具体的な本体は、六つの添字が選ぶ二組の三つ組に三つの条件を課します。第一の三つ組は `x` について `LeastNameAt` を満たし、第二の三つ組は `y` についてそれを満たさなければなりません。両者は同じ台と同じ二つの符号集合を使い、`R` と `P` が名前の比較に必要な二つの関係スロットを与えます。本体は六つの新しい証人を越えて外側の七つのスロットを読むため、それらへの参照はすべて `sh6` で移されます。

```agda
StepBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
         → Formula S (suc (suc (suc (suc (suc (suc n))))))
StepBody R P B C C₀ x y =
    LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x)
  ∧̇ ( LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y)
```

第三の条件は二組の三つ組を `≺At` で比較し、`x` の名前を `y` の名前より三つの鍵による名前順序で狭義に前へ置きます。したがって `StepBody` が述べるのは、同じ台の上で二つの最小の名前が与えられ、第一の名前が第二の名前に先行することです。`x` と `y` が生まれる段階の比較も、外側の再帰的な表も、表現された関係が整礎的であるという主張も含みません。それらは、この一ステップの記述を用いる、より大きな構成に属します。

```agda
    ∧̇ ≺At (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b )
```

`StepAt` は、六つの存在量化子で `StepBody` を閉じます。対象言語の論理式として主張するのは、`x` の最小の名前のデータ、`y` の最小の名前のデータ、そして前者を後者より前に置く比較が単に存在することです。この論理式が記述するのは、この一つの比較の場合です。それ自体が最小の名前を作ることも、周囲の段階についての再帰を実行することも、整礎性を証明することもありません。また、存在量化の意味論により、充足された `StepAt` を外向きに読む際には命題的切り詰めを保つ必要があります。

```agda
StepAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
StepAt R P B C C₀ x y = ∃₆ (StepBody R P B C C₀ x y)
```

スロットと環境を固定すると、`StepOf` は一般的な型 `Six` を `StepBody` に特殊化します。したがってその要素は、台の六つの明示的な要素と、それらが逆順に拡張された環境で二つの最小の名前の条件および名前の比較を満たすことの証明を含みます。この切り詰められていない中身に名前を付けることで、`StepAt` が表す命題との違いも明確になります。続く導入の読みは `StepOf` を直接使えますが、外向きの読みが返せるのは `∥ StepOf ∥₁` だけです。これが六つの束縛子をもつステップの論理式における証人の境界です。

```agda
module _ {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) where
  StepOf : Type (ℓ-suc ℓ)
  StepOf = Six (StepBody R P B C C₀ x y) γ
```

`StepOf` には六つの証人と本体の証明がすでに含まれているので、導入の向きは直ちに得られます。各証人を束縛の順に対応する存在量化子の下へ入れると、得られた割り当ては `StepAt` を満たします。ここでは与えられた二つの最小の名前の条件と比較の証明を使うだけで、名前そのものは構成しません。

```agda
  StepAt-in : StepOf → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
  StepAt-in = ∃₆-in (StepBody R P B C C₀ x y) γ
```

逆向きには、`StepAt` の充足関係から取り出せるのは `∥ StepOf ∥₁` までです。したがって、二つの最小の名前の論理式をそれぞれ満たす二組の三つ組と、第一の三つ組から第二の三つ組への比較の論理式の充足とは、単に存在するにとどまります。命題的切り詰めはこの存在を保ちながら六つの具体的な証人を隠し、存在量化の意味論にちょうど対応します。

```agda
  StepAt-out : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ StepOf ∥₁
  StepAt-out = ∃₆-out (StepBody R P B C C₀ x y) γ
```

## メタ言語が構成した名前との対応

論理式を意図したメタレベルの関係と比較するため、構成可能集合 `A` と、その台 `⟪ A ⟫` 上の狭義整列順序 `w` を固定します。`A` 上の名前の各パラメータはこの台から取られるので、`w` がパラメータ列の比較に必要な順序を正確に与えます。以下の妥当性はこれらのデータに相対的であり、その台にこのような順序を備えた任意の構成可能集合に適用できます。

```agda
module Adequacy (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where
  private
    module NM = Naming A w
```

ここで命名の構成から、型 `Name` と照合すべき比較が得られます。アリティが `k` の名前は、`suc k` 個の変数位置をもつ無パラメータ論理式と、ちょうど `k` 個のパラメータからなるベクトルを含みます。論理式の符号はその論理式から導かれ、`_≺ₙ_` はまず符号、次にアリティ、最後にパラメータ列を比較します。`w` の関係を `_≺ₚ_` と書き換えるのは、ここでの役割がパラメータ順序であることを示すためです。

```agda
  open NM using ( Name; arity; params; codeOf; _≺ᵥ_; _≺ₙ_ )
  open SWO w using () renaming ( _<∙_ to _≺ₚ_ )
```

再帰的に定義されたベクトル順序と比較するため、最初の相違を明示する関係 `Lex` を置きます。同じ長さの二つのベクトルについて、`Lex p q` は添字 `i` を選び、その位置で `p` の成分が `_≺ₚ_` により `q` の成分に先行し、すべての `j<i` では両成分が等しいことを要求します。対象言語の一致を表す論理式とは異なり、このメタレベルの関係は成分の等しさを直接述べられるため、共通のグラフ値を仲介させる必要がありません。

```agda
  Lex : ∀ {k} → Vec ⟪ A ⟫ k → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ)
  Lex {k} p q = Σ[ i ∈ Fin k ]
    ( (lookup i p ≺ₚ lookup i q)
    × ((j : Fin k) → toℕ j < toℕ i → lookup j p ≡ lookup j q) )
```

`Lex` から再帰的なベクトル順序への向きは、最初の相違の位置に従います。添字が零なら、先頭どうしの狭義の比較がそのまま `_≺ᵥ_` の第一の場合です。添字が後続なら、それより下での一致から二つの先頭が等しいことが分かり、同じ証人の添字を一つ下げると尾どうしの比較が得られます。これはベクトルについての構造的再帰であり、古典的原理を用いません。

```agda
  lex-vec : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Lex p q → p ≺ᵥ q
  lex-vec (x ∷ p) (y ∷ q) (zero  , (h , _)) = inl h
  lex-vec (x ∷ p) (y ∷ q) (suc i , (h , ag)) =
    inr (ag zero (suc-≤-suc zero-≤) , lex-vec p q (i , (h , λ j hj → ag (suc j) (suc-≤-suc hj))))
```

逆向きの写像は `_≺ᵥ_` の二つの場合に従います。二つの空ベクトルの間に順序の証明がある場合は不可能です。空でない二つのベクトルが先頭どうしの狭義の順序によって比較されているなら、添字零が `Lex` の証人になります。零より小さい添字はないので、一致の条件は空虚に成り立ちます。

```agda
  vec-lex : ∀ {k} (p q : Vec ⟪ A ⟫ k) → p ≺ᵥ q → Lex p q
  vec-lex []      []      h = Empty.rec* h
  vec-lex (x ∷ p) (y ∷ q) (inl h) = zero , (h , λ j hj → Empty.rec (¬-<-zero hj))
  vec-lex (x ∷ p) (y ∷ q) (inr (e , h)) = suc (vec-lex p q h .fst)
    , ( vec-lex p q h .snd .fst
```

残る場合には、先頭の等しさと、尾どうしの再帰的な順序が与えられます。尾に帰納法の仮定を適用して最初に異なる添字を得て、それを後続添字へ移せば、元のベクトルでの対応する位置になります。与えられた先頭の等しさが、移した添字より下にある最初の位置、すなわち位置零での一致を証明します。

```agda
      , step )
    where
    step : (j : Fin (suc _)) → toℕ j < suc (toℕ (vec-lex p q h .fst))
         → lookup j (x ∷ p) ≡ lookup j (y ∷ q)
    step zero    _  = e
```

移した添字より下にある残りの各位置では、数の不等式から両側の後続を一つずつ外すと、必要な主張は尾自身の一致へ帰着します。これで逆向きも完成します。したがって、明示的な最初の相違と再帰的なベクトル順序は同じ関係を表し、パラメータについての議論は比較を変えずに二つの表示を行き来できます。

```agda
    step (suc j) hj = vec-lex p q h .snd .snd j (pred-≤-pred hj)
```

## パラメータを双方向に読む

論理式の符号は、もう一つの既存の順序で比較されます。各 `codeOf t` は極限段階に属し、その上の狭義整列順序が `limitOrder` です。その関係を `_≺ˡ_` と書けば、パラメータの鍵 `_≺ₚ_` と並んで符号の鍵が明確になります。ここで新しい順序を定義するわけではありません。三つの鍵による名前の比較は、まさにこれら二つの順序のモデル内での表示を用います。

```agda
  open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )
```

パラメータは小さな台 `⟪ A ⟫` の要素なので、台となる集合と、それが `A` に属すことの証拠をともに含みます。写像 `ix` はこの所属の証拠を忘れ、`V` 内の台となる集合だけを残します。パラメータの値を環境グラフに入れるときも、パラメータ順序を表す関係の順序対に入れるときも、この標準的な埋め込み像を用います。

```agda
  ix : ⟪ A ⟫ → V ℓ
  ix m = ⟪ A ⟫↪ m
```

同じ台となる集合は、構成可能モデルの要素としても扱えます。`A` が構成可能であり、`ix m` が `A` に属すので、構成可能性の推移性から `ix m` も構成可能です。この集合と証明を組にすると `ixL m : S` が得られ、パラメータを対象言語の値として使うための形になります。

```agda
  ixL : ⟪ A ⟫ → S
  ixL m = ix m , isL-trans (∈∈ₛ {a = ix m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) pA
```

名前 `t` に対して、族 `pfam t` はそのパラメータベクトルを成分ごとに読みます。定義域は `Fin (arity t)` で、添字 `i` における値は、その位置に格納されたパラメータの台となる `V` の集合です。したがってアリティがこの族の定義域を定義上決め、グラフ `env (pfam t)` がそのパラメータベクトルのモデル内での環境表示を正確に与えます。

```agda
  pfam : (t : Name) → Fin (arity t) → V ℓ
  pfam t i = ix (lookup i (params t))
```

台の要素をその台となる集合へ移しても、要素を識別するための情報は失われません。標準写像 `⟪ A ⟫↪` は埋め込みなので、`ix u ≡ ix v` から `u ≡ v` が従います。この単射性はパラメータを逆向きに読む議論で欠かせません。二つの環境グラフが先行する添字で共通の値をもつとき、その台となる `V` の集合の等しさを、パラメータベクトルの対応する成分の等しさへ読み戻せます。

```agda
  ix-inj : (u v : ⟪ A ⟫) → ix u ≡ ix v → u ≡ v
  ix-inj u v = isEmbedding→Inj isEmb⟪ A ⟫↪ u v
```

最後に、モデル内の二つの関係集合がそれぞれ何を表すべきかを定めます。符号について、`Rrep` は `u` と `v` の順序対が `Rs` に属すことを `u ≺ˡ v` として読み、`Rfill` はこの比較からその所属を証明します。パラメータについても、`Prep` と `Pfill` が、二つの `ix` 像からなる順序対の `Ps` への所属と `u ≺ₚ v` の間の両方向を与えます。これら四つの表示則は仮定です。この仮定の下で、対応する表示をもつ任意の二つの構成可能な関係集合について三つの鍵の論理式は妥当になります。どちらの関係もここでは構成しません。

```agda
  module Keys (Rs Ps : S)
              (Rrep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩ → u ≺ˡ v)
              (Rfill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩)
              (Prep : (u v : ⟪ A ⟫) → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩ → u ≺ₚ v)
              (Pfill : (u v : ⟪ A ⟫) → u ≺ₚ v → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩)
```

四つの表示則を具体的なパラメータ比較に適用するため、二つの名前と、そのデータを対象言語で読むスロットを固定します。この局所的な議論を支える同一視は五つあります。パラメータ関係を定めるもの、第一のアリティを定めるもの、二つのアリティを等しくするもの、そして二つのパラメータ環境をそれぞれ定めるものです。これらの仮定のもとで、明示的な最初の相違 `Lex` とグラフによる記録 `Differs` を双方向に翻訳します。

```agda
              where
```

最初の四つの同一視が、比較に共通する枠組みを定めます。スロット `P` は関係集合 `Ps` を持ち、スロット `a₁` は `t₁` のアリティの数項を持ちます。また `qk : arity t₂ ≡ arity t₁` によって、二つのパラメータベクトルを同じ長さで比較できます。最後に `e₁` は `pfam t₁` のグラフを持ち、その各添字での値は第一の名前の対応するパラメータの埋め込み像です。`qk` は自然数としての二つのアリティの等しさであり、対象言語のスロットを同定する式ではありません。

```agda
    module _ {n : ℕ} (P a₁ e₁ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name)
             (qP : fst (lookup P γ) ≡ fst Ps)
             (qa : fst (lookup a₁ γ) ≡ # (arity t₁))
             (qk : arity t₂ ≡ arity t₁)
             (q₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
```

第五の同一視により、第二の環境も同じ定義域を持ちます。まず `params t₂` を `qk` に沿って長さ `arity t₂` から長さ `arity t₁` へ輸送し、次に輸送後の各成分を `V` へ埋め込んで、そのグラフを取ります。これで、どちらの環境も `Fin (arity t₁)` の添字で参照できます。続いて導入する局所的な族は輸送前後の成分に名前を付けるもので、まず第一のベクトルを読む `pr₁` を定めます。

```agda
             (q₂ : fst (lookup e₂ γ)
                 ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) qk (params t₂)))))
             where
      private
        pr₁ : Fin (arity t₁) → ⟪ A ⟫
```

共通の長さの添字 `i` において、`pr₁ i` は `t₁` のパラメータベクトルのその成分です。これは小さな台 `⟪ A ⟫` の要素のままであり、環境グラフやモデル内の順序対へ入れるときにだけ埋め込み `ix` を施します。この二つの水準を分けておくことで、パラメータ順序を台の要素そのものに適用できます。

```agda
        pr₁ i = lookup i (params t₁)
```

もう一方の族 `pr₂` は、輸送された `t₂` のベクトルを読みます。定義域は `pr₁` と同じですが、その値は第二の名前に属する台の要素です。したがって、共通の各添字で `pr₁ i ≺ₚ pr₂ i` と `pr₁ j ≡ pr₂ j` を型の合う形で述べられます。これらがそれぞれ、`Lex` の求める狭義の比較と、それ以前での一致です。

```agda
        pr₂ : Fin (arity t₁) → ⟪ A ⟫
        pr₂ i = lookup i (subst (Vec ⟪ A ⟫) qk (params t₂))
```

これで第一のグラフを特定の添字で読めます。鍵が `# (toℕ i)`、値が `fst u` である対がスロット `e₁` の集合に属すとします。この所属を `q₁` に沿って輸送すると `env (pfam t₁)` への所属になり、`lookup-spec` が第二成分をそのグラフの当該位置における唯一の値と同一視します。その値は `ix (pr₁ i)` なので、`at₁` は等式 `fst u ≡ ix (pr₁ i)` を復元します。

```agda
        at₁ : (i : Fin (arity t₁)) (u : S)
            → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₁ γ) ⟩ → fst u ≡ ix (pr₁ i)
        at₁ i u h = subst ⟨_⟩ (lookup-spec (pfam t₁) i (fst u))
          (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₁ h)
```

第二のグラフも、`pfam t₁` の代わりに輸送後の族を用いて同じように読めます。鍵 `# (toℕ i)` の対の所属をまず `q₂` に沿って輸送すると、`lookup-spec` によって `fst u ≡ ix (pr₂ i)` が得られます。したがって `at₁` と `at₂` は、ここで必要な一価性の帰結を与えます。有効な添字で見つかった値を、そこで表される特定のパラメータ成分と正確に同一視するのです。

```agda
        at₂ : (i : Fin (arity t₁)) (u : S)
            → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₂ γ) ⟩ → fst u ≡ ix (pr₂ i)
        at₂ i u h = subst ⟨_⟩ (lookup-spec (λ j → ix (pr₂ j)) i (fst u))
          (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₂ h)
```

`lookup-spec` を逆向きに使うと、第一のグラフの標準的な項目が得られます。反射律により `ix (pr₁ i)` は `pfam t₁` が `i` で指定する値です。この参照の等式を逆向きに読むと、その等しさは `env (pfam t₁)` への所属になります。さらに `q₁` の逆向きに輸送すれば、同じ順序対がスロット `e₁` に実際に格納された集合へ入ります。これが証人 `put₁ i` です。

```agda
        put₁ : (i : Fin (arity t₁))
             → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ fst (lookup e₁ γ) ⟩
        put₁ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ z ⟩) (sym q₁)
          (subst ⟨_⟩ (sym (lookup-spec (pfam t₁) i (ix (pr₁ i)))) refl)
```

証人 `put₂ i` も、輸送後の第二の族とスロット `e₂` について同じように構成されます。これで四つの補題は、二つの名前のグラフ参照を両方向から扱えます。`at₁` と `at₂` は候補として与えられた値を同定し、`put₁` と `put₂` はグラフが指定する値を実際に示します。順方向の翻訳では後の二つから `Differs` を作り、逆方向の翻訳では前の二つから `Lex` を復元します。

```agda
        put₂ : (i : Fin (arity t₁))
             → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ fst (lookup e₂ γ) ⟩
        put₂ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ z ⟩) (sym q₂)
          (subst ⟨_⟩ (sym (lookup-spec (λ j → ix (pr₂ j)) i (ix (pr₂ i)))) refl)
```

`Lex` が使う添字は有限な自然数ですが、`Differs` が携える添字は構成可能モデルの要素でなければなりません。補助定義 `numAt` はこの小さな隔たりを越え、von Neumann 数項 `# m` とその構成可能性の証明 `numL m` を組にします。ただし、これだけで数項があるアリティより下にあると主張するわけではありません。その所属は、有限添字に備わる境界から別に与えます。

```agda
        numAt : (m : ℕ) → S
        numAt m = # m , numL m
```

順方向の翻訳では、`Lex` の要素から有限添字 `i`、その位置での狭義の比較 `hlt`、およびそれ以前の各添字での等しさ `agree` が得られます。`Differs` の記録にはまずモデルの要素 `numAt (toℕ i)` を置き、続いて二つの値 `ixL (pr₁ i)` と `ixL (pr₂ i)` を置きます。有限添字はその長さより小さいので、`#mono` は `toℕ<n i` を、その添字の数項がアリティの数項に属すという証明へ変えます。これを `qa` に沿って輸送すれば、アリティのスロットへの所属が得られます。

```agda
      lex-fill : Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂))
               → Differs P a₁ e₁ e₂ γ
      lex-fill (i , (hlt , agree)) = numAt (toℕ i)
        , ( ixL (pr₁ i) , ( ixL (pr₂ i)
        , ( subst (λ z → ⟨ # (toℕ i) ∈ z ⟩) (sym qa)
```

続く成分は、相違する添字で何が起きるかを証明します。証人 `put₁ i` と `put₂ i` は、二つの埋め込まれたパラメータ値をそれぞれの環境グラフに入れます。表示則 `Pfill` は `hlt : pr₁ i ≺ₚ pr₂ i` を、それらの順序対が `Ps` に属すという事実へ変えます。さらに `qP` の逆向きに輸送すると、その所属はスロット `P` が持つ関係集合への所属になります。したがって `Differs` の三つの所属成分は、二つの参照とパラメータの狭義の比較を正確に表します。

```agda
              (#mono (toℕ i) (arity t₁) (toℕ<n i))
          , ( put₁ i
            , ( put₂ i
              , ( subst (λ z → ⟨ pr (ix (pr₁ i)) (ix (pr₂ i)) ∈ z ⟩) (sym qP)
                    (Pfill (pr₁ i) (pr₂ i) hlt)
```

残るのは、選んだ添字より前で `Agrees` を構成することです。モデルの要素 `j` と `fst j ∈ # (toℕ i)` が与えられると、数項の消去定理は、ある `m < toℕ i` について `fst j` が `# m` に等しいことを命題的切り詰めの中で示します。この結果に局所的な構成 `step` を写せば、その先行位置で二つのグラフに共通する値が得られます。切り詰めは保たれており、数項への所属から復元された特定の自然数が `Agrees` の求める命題の外へ現れることはありません。

```agda
                , agrees ) ) ) ) ) )
        where
        agrees : Agrees P a₁ e₁ e₂ γ (numAt (toℕ i))
        agrees j hj = PT.map step (∈#-elim (toℕ i) (fst j) hj)
          where
```

関数 `step` は、共通の値という主張を正確に述べます。`m < toℕ i` と `fst j` を `# m` に同一視する等式から、鍵 `fst j` と値 `fst x` の対が両方の環境グラフに属すようなモデルの要素 `x` を返さなければなりません。ここで与える値は、対応する有限添字における第一の族の成分であり、`ixL (pr₁ jx)` としてまとめられます。第一のグラフについては、`put₁ jx` が標準的な数項の鍵で必要な所属をすでに与えています。その鍵の二つの表示を結ぶ等式に沿って輸送すれば、鍵を `fst j` に書き換えられます。

```agda
          step : Σ[ m ∈ ℕ ] ((m < toℕ i) × (fst j ≡ # m))
               → Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                            × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
          step (m , (hm , qj)) = ixL (pr₁ jx)
            , ( subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₁ γ) ⟩)
```

第二のグラフでは、先行添字についての仮定 `agree` が `pr₁ jx` と `pr₂ jx` を同一視します。この等しさの逆向きに `put₂ jx` を輸送すると、その値を `ix (pr₂ jx)` から共通の値 `ix (pr₁ jx)` へ書き換えられます。さらに先ほどと同じように鍵を輸送すれば、`fst j` での所属が得られます。したがって `i` より前のすべての位置で、二つのグラフはまったく同じ値を含みます。これで `step` の一つの結果が完成し、ひいては `Differs` の `Agrees` 成分が得られます。

```agda
                  (sym qjx) (put₁ jx)
              , subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₂ γ) ⟩) (sym qjx)
                  (subst (λ y → ⟨ pr (# (toℕ jx)) (ix y) ∈ fst (lookup e₂ γ) ⟩)
                    (sym (agree jx (subst (_< toℕ i) (sym qm) hm))) (put₂ jx)) )
            where
```

残る同一視は、共通の項目の鍵に関するものです。`m < toℕ i` と、`i` 自身が`arity t₁` より小さいことから、推移性によって `m` は正当な要素`jx : Fin (arity t₁)` を定めます。`jx` を自然数へ戻すと `m` が得られ、その往復を経路`qm` が記録します。この経路により、二つのグラフへの所属をそれぞれの標準的な数項の鍵で書けます。

```agda
            jx : Fin (arity t₁)
            jx = fromℕ' (arity t₁) m (<-trans hm (toℕ<n i))
            qm : toℕ jx ≡ m
            qm = toFromId' (arity t₁) m (<-trans hm (toℕ<n i))
            qjx : fst j ≡ # (toℕ jx)
```

等式 `qj` はもとのモデル内の鍵を `# m` と同一視し、`qm` は `m` を `jx` の表す自然数と同一視します。両者を合成すると`qjx : fst j ≡ # (toℕ jx)` が得られます。これは先ほど用いた鍵の書き換えそのもので、二つのグラフの標準的な項目を、ともに`j` が名指す位置へ輸送します。これで `Agrees` の構成が終わり、順方向の橋 `lex-fill` も完成します。

```agda
            qjx = qj ∙ cong #_ (sym qm)
```

逆向きの橋は `Differs` の記録から出発し、明示的な最初の相違を復元します。記録された添字 `i` はアリティの数項に属しますが、数項への所属についての消去定理が対応する小さい自然数を復元するのは、命題的切り詰めの中だけです。そのため `lex-read` は `Lex` の命題的切り詰めを返します。数項の消去は選ばれた自然数を隠したままにし、`PT.map` がその切り詰めを外さずに残りの明示的な構成を行います。

```agda
      lex-read : Differs P a₁ e₁ e₂ γ
               → ∥ Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂)) ∥₁
      lex-read (i , (u , (v , (hi , (h₁ , (h₂ , (hp , ag))))))) =
        PT.map atIndex (∈#-elim (arity t₁) (fst i)
          (subst (λ z → ⟨ fst i ∈ z ⟩) qa hi))
```

写像された構成の内部では、隠されていた証人を具体的な自然数 `m` として使えます。同時に`m < arity t₁` と、モデル内の添字を `# m` と同一視する等式も得られます。関数 `atIndex` はここで`Lex` そのものを構成します。対応する有限添字を選び、その位置での狭義の比較と、それより小さいすべての添字での一致という、最初の相違の二条件を証明します。

```agda
        where
        atIndex : Σ[ m ∈ ℕ ] ((m < arity t₁) × (fst i ≡ # m))
                → Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂))
        atIndex (m , (hm , qi)) = ι , (below , agrees)
          where
```

`m` の境界から `ι : Fin (arity t₁)` が得られます。順方向と同様に、数項との往復によって`# m` についての等式は `qι : fst i ≡ # (toℕ ι)` へ書き換えられます。したがって、第一の環境に記録された所属を`ι` の標準的な鍵で読めます。参照の補題 `at₁` は、記録された値 `fst u` を第一のパラメータの埋め込み像`ix (pr₁ ι)` と同一視します。

```agda
          ι : Fin (arity t₁)
          ι = fromℕ' (arity t₁) m hm
          qι : fst i ≡ # (toℕ ι)
          qι = qi ∙ cong #_ (sym (toFromId' (arity t₁) m hm))
          qu : fst u ≡ ix (pr₁ ι)
```

第二のグラフに `at₂` を適用すると、同様に `fst v ≡ ix (pr₂ ι)` が得られます。`Differs` の関係原子は、記録された二つの値の順序対がスロット`P` の集合に属すと述べます。その集合を `Ps` に、二つの値を対応するパラメータの埋め込み像に書き換えると、表示則`Prep` がこの原子を、必要な狭義の比較 `pr₁ ι ≺ₚ pr₂ ι` として読みます。

```agda
          qu = at₁ ι u (subst (λ z → ⟨ pr z (fst u) ∈ fst (lookup e₁ γ) ⟩) qι h₁)
          qv : fst v ≡ ix (pr₂ ι)
          qv = at₂ ι v (subst (λ z → ⟨ pr z (fst v) ∈ fst (lookup e₂ γ) ⟩) qι h₂)
          below : pr₁ ι ≺ₚ pr₂ ι
          below = Prep (pr₁ ι) (pr₂ ι)
```

以上の輸送によって `below` と名づけられた証明が完成します。残るのは `ι` より前での一致の復元です。`toℕ j < toℕ ι` を満たす任意の `j` に対して、有界な節 `ag` は、その位置で両方の環境グラフに値として現れる一つのモデル要素を、単に存在するものとして与えます。求める二つのパラメータの埋め込み像の等しさは命題なので、この命題的切り詰めをそこへ直接消去できます。

```agda
            (subst2 (λ y z → ⟨ pr y z ∈ fst Ps ⟩) qu qv
              (subst (λ z → ⟨ pr (fst u) (fst v) ∈ z ⟩) qP hp))
          agrees : (j : Fin (arity t₁)) → toℕ j < toℕ ι → pr₁ j ≡ pr₂ j
          agrees j hj = ix-inj (pr₁ j) (pr₂ j)
            (PT.rec (setIsSet (ix (pr₁ j)) (ix (pr₂ j))) same
```

`ag` を使うため、まず有限な不等式を `#mono` によって`# (toℕ j) ∈ # (toℕ ι)` という所属へ変え、さらに `qι` に沿って記録された境界へ輸送します。得られる切り詰められた証人は`same` が扱う形そのものです。すなわち、要素 `x` と、順序対 `(# (toℕ j), fst x)` がそれぞれの環境グラフに属すことの組です。したがって、切り詰めの内部には等しさを導くための情報がすべてありながら、具体的な証人は外へ出ません。

```agda
              (ag (numAt (toℕ j))
                (subst (λ z → ⟨ # (toℕ j) ∈ z ⟩) (sym qι) (#mono (toℕ j) (toℕ ι) hj))))
            where
            same : Σ[ x ∈ S ] ( ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₁ γ) ⟩
                              × ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
```

共通の値 `x` を一つ取ると、`at₁` は `fst x` を `ix (pr₁ j)` と同一視し、`at₂` は同じ集合を`ix (pr₂ j)` と同一視します。第一の経路を逆にして第二の経路と合成すれば、二つのパラメータの埋め込み像が等しいと分かります。`ix` の単射性はこの等しさを `pr₁ j ≡ pr₂ j` へ反映し、これは `Lex` が先行添字に要求する条件そのものです。これで逆向きの橋も完成します。

```agda
                 → ix (pr₁ j) ≡ ix (pr₂ j)
            same (x , (k₁ , k₂)) = sym (at₁ j x k₁) ∙ at₂ j x k₂
```

## 妥当性の両方向

`Keys` に与えられた四つの表示則のもとで、二つの関係スロットは、それぞれ論理式の符号上の `limitOrder` と台のパラメータ上の与えられた順序を表します。ここで証明した二方向は、同じ三つのキーを比較します。`order-in` は具体的な `t₁ ≺ₙ t₂` の証明から `≺At` の充足関係を導き、`order-out` はその充足関係から `∥ t₁ ≺ₙ t₂ ∥₁` だけを読み出します。外向きの証明には、選言と存在量化の充足関係から生じる命題的切り詰めが残ります。したがって、本章でここまでに得られたのは比較論理式 `≺At` 自体の妥当性であり、他の論理式についてこれより強い結果を証明したわけではありません。

残る仕事の境界は明確です。メタ言語の `Name` が保持するのは、アリティ、無パラメータ論理式、パラメータベクトルであり、指示対象はそれらから導かれます。モデル内部では、`NameAt` がそれらのデータと導出された指示対象のスロットを設け、`satGraphAt` が返す充足環境の集合を用いて指示対象を検査します。`LeastNameAt` は同じ指示対象をもつより小さな名前がないことを述べるだけで、名前を選択しません。充足関係からの証人の回収を含む `NameAt`、`LeastNameAt`、`StepAt` の完全な妥当性は `L.Choice.NameComparisonAdequacy` で扱われ、最小名の実際の選択は引き続き `CanonicalNames.leastName` が担います。

## まとめ

続く二つの経路帰納の補題は、三つの鍵による比較全体にある型の障害を取り除きます。第一の `envShift` は、アリティの等式`e : arity t ≡ k` を扱います。`params t` を `e` に沿って輸送し、成分を読んで環境グラフを作っても、もとの長さで`params t` を読んで作るグラフと等しくなります。`e` が反射経路なら主張は直ちに簡約され、経路帰納によって任意の等式の場合が従います。

```agda
    private
      envShift : (t : Name) {k : ℕ} (e : arity t ≡ k)
               → env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) e (params t))))
               ≡ env (pfam t)
      envShift t e = sym (constSubstCommSlice
```

この等式は、輸送後のベクトルのグラフから、もとのグラフ `env (pfam t)` へ向いています。この向きは最後の証明で役立ちます。第二の環境についての仮定は、まずそのスロットをもとのグラフと同一視します。そこに`envShift` の逆向きをつなぐと、同じスロットを第一の名前のアリティ上のグラフと同一視でき、最初の相違の橋が要求する形がちょうど得られます。

```agda
        (Vec ⟪ A ⟫) (V ℓ) (λ _ v → env (λ i → ix (lookup i v))) e (params t))
```

第二の補題 `vecShift` は、ベクトル順序について対応する簡約を行います。長さの等式に沿って `q` を輸送してから`p` と比較して得る命題は、もとのベクトルを比較する命題と同じです。ここでも等式の証明から新しい数学的場合は生じません。経路帰納によって反射経路の場合へ帰着します。したがって、アリティを同一視したとき、`envShift` と`vecShift` が環境グラフの表示とベクトルの比較を同期させます。

```agda
      vecShift : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i)
               → (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q)
      vecShift e p q = sym (constSubstCommSlice
        (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)
```

最後の比較は、任意の環境の任意のスロットで行います。二つのスロットには表示関係 `Rs` と `Ps` が入り、各名前についてさらに三つのスロットが、その論理式の符号、アリティの数項、パラメータのグラフを持ちます。八つの等式`qR`、`qP`、`qs₁`、`qs₂`、`qa₁`、`qa₂`、`qe₁`、`qe₂` が、これらの読みを二つの具体的な名前`t₁` と `t₂` に固定します。まさにこれらの仮定のもとで、内部の論理式を `_≺ₙ_` と照合できます。

```agda
    module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name)
             (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps)
             (qs₁ : fst (lookup s₁ γ) ≡ fst (codeOf t₁))
             (qs₂ : fst (lookup s₂ γ) ≡ fst (codeOf t₂))
             (qa₁ : fst (lookup a₁ γ) ≡ # (arity t₁))
```

最後の四つのスロット等式は、二つのアリティと二つの環境グラフを固定します。したがって、この定理は特定の座標を組み込んでいません。第二、第三の鍵を読むには、スロットの値の等しさを、名前が携える依存データの等しさへ持ち上げる必要があります。最初の補助関数 `codeSame` は符号の鍵を扱い、二つの骨格スロットの等しさから、型 `Limit` における等式 `codeOf t₂ ≡ codeOf t₁` を復元します。

```agda
             (qa₂ : fst (lookup a₂ γ) ≡ # (arity t₂))
             (qe₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
             (qe₂ : fst (lookup e₂ γ) ≡ env (pfam t₂)) where
      private
        codeSame : fst (lookup s₂ γ) ≡ fst (lookup s₁ γ) → codeOf t₂ ≡ codeOf t₁
```

`Limit` の要素は、台となる集合と、それが `Lset ω` に属すことの証拠からなります。その証拠は命題値なので、`Σ≡Prop` により、台となる集合の間の経路だけで完全な符号の間の経路が定まります。ここで必要な台の経路は`sym qs₂ ∙ q ∙ qs₁` です。第二の符号からそのスロットへ進み、記録された骨格の等式を渡って、第一の符号へ至ります。これにより、証明成分を別に比較する必要がないことと、得られる等式が名前順序の第二の分岐に必要な向きを持つことの両方が分かります。

```agda
        codeSame q = Σ≡Prop (λ x → snd (x ∈ Lset ω)) (sym qs₂ ∙ q ∙ qs₁)
```

逆向きの変換は `Limit` における等しさから始まります。ここで符号は、台となる集合と、それが極限段階に属することの証明から成ります。`fst` で射影すれば台となる符号集合の等しさが得られ、それを二つのスロットの同一視と合成すると、論理式の後二つの枝が要求する向き、すなわち第二の骨格スロットが第一の骨格スロットに等しいという形になります。

```agda
        codeBack : codeOf t₂ ≡ codeOf t₁ → fst (lookup s₂ γ) ≡ fst (lookup s₁ γ)
        codeBack ec = qs₂ ∙ cong fst ec ∙ sym qs₁
```

パラメータの枝では、第二の環境を第一の名前のアリティで読まなければなりません。`ek : arity t₂ ≡ arity t₁` が与えられると、経路帰納法により、`params t₂` のグラフは、そのベクトルを新しい長さへ輸送してから作ったグラフと同一視されます。このグラフの等しさを逆向きに読み、スロット `e₂` の同一視と合成すれば、最初の相違を扱う橋が要求する輸送後の環境が得られます。

```agda
        shiftEnv : (ek : arity t₂ ≡ arity t₁)
                 → fst (lookup e₂ γ)
                 ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) ek (params t₂))))
        shiftEnv ek = qe₂ ∙ sym (envShift t₂ ek)
```

順方向の定理は、一方の名前が他方に先行する三つの理由を順に扱います。符号の枝では、`Rfill` が二つの論理式符号の極限順序による狭義の比較を、それらの順序対が `Rs` に属するという事実へ変えます。`R`、`s₁`、`s₂` に関する同一視でこの所属を論理式の三つのスロットへ輸送し、`≺At-in` が得られた証人を `≺At` の第一の枝へ入れます。

```agda
      order-in : t₁ ≺ₙ t₂ → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
      order-in (inl h) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inl (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩)
                (sym qR)
                (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) (sym qs₁) (sym qs₂)
```

アリティの枝では、まず符号の等しさから `codeBack` を通じて二つの骨格スロットに必要な等しさを得ます。狭義の不等式 `arity t₁ < arity t₂` は、von Neumann 数項の法則 `#mono` によって所属 `# (arity t₁) ∈ # (arity t₂)` へ変わり、二つのアリティスロットの同一視がこの所属を論理式へ輸送します。したがって第二の鍵が比較に使われるのは、第一の鍵の等しさが示された後だけです。

```agda
                  (Rfill (codeOf t₁) (codeOf t₂) h))))
      order-in (inr (ec , inl h)) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inr (codeBack ec , inl
          (subst2 (λ y z → ⟨ y ∈ z ⟩) (sym qa₁) (sym qa₂)
            (#mono (arity t₁) (arity t₂) h))))
```

パラメータの枝は、符号とアリティがともに等しい場合から始まります。アリティの経路で第二のパラメータベクトルを第一のベクトルの長さへ輸送し、`vec-lex` によって再帰的なベクトル比較を明示的な最初の相違の添字へ変えます。続いて `lex-fill` は、この証人を `LexAt` の充足に用いる `Differs` のデータへ変えます。そこには添字、その位置での狭義の比較、それ以前の各位置での等しさが記録され、`shiftEnv` が輸送後の第二のグラフを同一視します。こうして、命題的切り詰めから証人を取り出すことなく、比較の証拠から `≺At` の第三の枝を直接構成できます。

```agda
      order-in (inr (ec , inr (ek , hv))) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inr (codeBack ec , inr (qa₂ ∙ cong #_ ek ∙ sym qa₁
          , lex-fill P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek)
              (vec-lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂))
                (transport (sym (vecShift ek (params t₁) (params t₂))) hv)))))
```

逆向きの定理は、対象言語の選言と存在量化が伴う命題的切り詰めを保ちます。したがって `≺At-out` が三つの場合を取り出すのは切り詰めの内側だけです。目標自身が命題 `∥ t₁ ≺ₙ t₂ ∥₁` なので、`PT.rec` はその中で場合分けできます。符号の枝では、各スロットの同一視によって論理式に記録された順序対の所属を `Rs` へ戻し、`Rrep` がそれを二つの実際の符号の極限順序による狭義の比較として読みます。これが名前比較の第一の枝を与えます。

```agda
      order-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ t₁ ≺ₙ t₂ ∥₁
      order-out h = PT.rec squash₁ read (≺At-out R P s₁ a₁ e₁ s₂ a₂ e₂ γ h)
        where
        read : Below R P s₁ a₁ e₁ s₂ a₂ e₂ γ → ∥ t₁ ≺ₙ t₂ ∥₁
        read (inl k) = ∣ inl (Rrep (codeOf t₁) (codeOf t₂)
```

アリティの場合、論理式はまず第二の骨格スロットが第一の骨格スロットに等しいと述べます。`codeSame` はこの台の等しさを、二つの符号の `Limit` における等しさへ持ち上げます。もう一つの前提は、アリティスロットの同一視で輸送すると、第一のアリティの数項が第二のアリティの数項に属するという事実になります。数項についての消去がこの所属を `arity t₁ < arity t₂` へ変えるので、第一の鍵の等しさと第二の鍵の狭義の比較から `_≺ₙ_` のアリティの枝が組み立てられます。

```agda
          (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) qs₁ qs₂
            (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩)
              qR k))) ∣₁
        read (inr (q , inl k)) = ∣ inr (codeSame q , inl
          (#∈#-elim (arity t₁) (arity t₂)
```

パラメータの場合には、まず共通の長さを復元する必要があります。論理式は第二のアリティスロットから第一のアリティスロットへの等しさを与えます。これを二つのスロットの同一視と合成すると、対応する von Neumann 数項が等しいと分かり、`#-inj′` によって `ek : arity t₂ ≡ arity t₁` が得られます。この経路で第二のベクトルの型を比較可能な形にそろえると、`lex-read` は二つの環境グラフに照らして `LexAt` の記録を解釈します。結果は、命題的切り詰めの内側に保たれた明示的な最初の相違 `Lex` であり、論理式の存在証人に関する境界を正確に保っています。

```agda
            (subst2 (λ y z → ⟨ y ∈ z ⟩) qa₁ qa₂ k))) ∣₁
        read (inr (q , inr (q' , dif))) = PT.map atLex
          (lex-read P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek) dif)
          where
          ek : arity t₂ ≡ arity t₁
```

その切り詰めの内側で、`atLex` が第三の場合を完成させます。帰納法 `lex-vec` は明示的な最初の相違を、第一のベクトルと輸送後の第二のベクトルとの再帰的なベクトル順序へ変え、`vecShift` が得られた命題からその輸送を取り除きます。これに `codeSame q` と復元したアリティの経路 `ek` を合わせると `_≺ₙ_` のパラメータの枝となり、`PT.map` は結果全体を切り詰めの内側に保ちます。したがって、二つの順序の表示則と各スロットの同一視のもとで、`order-in` は名前比較から `≺At` の充足を構成し、`order-out` は `∥ t₁ ≺ₙ t₂ ∥₁` だけを復元します。ここで証明されたのは比較論理式そのものの妥当性であり、`NameAt`、`LeastNameAt`、`StepAt` の対応する読みには、さらに別の議論が必要です。

```agda
          ek = #-inj′ (sym qa₂ ∙ q' ∙ qa₁)
          atLex : Lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) → t₁ ≺ₙ t₂
          atLex lx = inr (codeSame q , inr (ek
            , transport (vecShift ek (params t₁) (params t₂))
                (lex-vec (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) lx)))
```