---
title: "無限順序数の下で有限列をコード化する"
module: L.GCH.FiniteSequenceCoding
lang: ja
site: "Bedrock"
description: "無限順序数の下で有限列をコード化する"
stage: "GCH の証明"
reading_order: 114
canonical: https://bedrock.institute/ja/L.GCH.FiniteSequenceCoding.html
html: L.GCH.FiniteSequenceCoding.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/FiniteSequenceCoding.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Full, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Coding.Environment, L.Coding.EnvironmentSet, L.Recursion, L.Cardinal, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.CardinalSquareLaw]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.FiniteSequenceCoding.md, https://bedrock.institute/zh/L.GCH.FiniteSequenceCoding.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 無限順序数の下で有限列をコード化する

有限なパラメータ列を数えるには、その列を集める集合が `L` の内部に存在しなければなりません。本章ではまず、構成可能集合上のすべての有限列を一つの構成可能集合に集めます。次に無限順序数 `α` に対し、`α × α` から `α` への内部の符号化された単射を用いて列を項ごとに畳み込み、最後に長さをタグとして付け、列の集合から `α` への内部単射を示します。この結論は上界だけを与えます。`α` のすべての要素を覆うことも、`α` 全体で定義された復号写像を与えることもありません。

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

この構成で用いる古典性は、明示された排中律の仮定だけから来ます。とくに、命題的に切り詰められた証人は、一意性によって証人型そのものが命題になる場合を除いて、切り詰められたままです。列の表現や単射のグラフを任意に選ぶための選択原理は用いません。

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

宇宙レベル `ℓ` と、レベル `ℓ-suc ℓ` における排中律を固定します。以下の分出から最後に用いる平方律まで、すべての構成はこの一つの名づけられた仮定に相対的であり、最終的な列の上界もまったく同じ仮定をもちます。

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

以下では、同じ対象について二つの記述を行き来します。対象言語の水準では、等号、連言、有界および非有界の量化によって、`L` の内部の列のグラフと再帰の軌跡を記述します。ホストの水準では、提示によって集合の要素を小さな添字として扱い、正則性は後で平方律を支える整礎的な議論に用いられます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
```

符号化は、二つの剛直な集合符号の族に依存します。順序対の符号の単射性により、対の符号の等しさから二つの座標を復元でき、フォン・ノイマン数項は自然数とその順序を `ω` の内部で忠実に記録します。構成可能性の推移性により、構成可能な順序数の各要素も `L` にとどまるので、これらの周囲の符号を構成可能モデルの要素として使えます。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd )
open import L.Ordinal {ℓ} using ( #∈ω; ∈#-elim )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
```

ここで用いる集合論的グラフは、`L` の内部の一階推論から読めなければなりません。分出によって正確な部分集合を作り、対、グラフの適用、定義域、環境についての妥当性が、各対象言語の節を底集合間の意図された関係と同一視します。この橋によって、後でホスト側の再帰的な畳み込みを内部の定義可能なグラフへ移せます。

```agda
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOver-sv; envOver-dom; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate )
open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract )
open import L.Coding.Environment {ℓ} using ( lookup-spec )
```

有限列は、数項をちょうど定義域とする環境のグラフとして表します。各固定長について、環境集合の構成はそのようなグラフだけを集め、要素から表現を読み戻す向きは命題的に切り詰められています。それでも、グラフの論理式の出力が一意なら、再帰の仕組みは実際の値を与えます。さらに、符号化された単射の合成によって、得られた上界を構成可能集合の間で移せます。

```agda
open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envOver; envSet; envSet-in; envSet-out; module Recover )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct; smallDom )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
open import L.InjectionComposition {ℓ} lem using ( injl-trans )
```

最後の数え上げでは、与えられた無限順序数がすでに基数であると仮定する必要はありません。まず基数代表へ移り、そこで平方律を用いて対を圧縮し、もとの順序数へ合成して戻します。本章は、その対の圧縮から有限列の定義可能な単射を構成します。

```agda
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.CardinalSquareLaw {ℓ} lem
  using ( prodL; prodL-in; Goal; module Step; prod-inj; no-fin; ω⊆ )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
```

長さは自然数、位置は `Fin n` の要素、内部の定義域の標識は数項として表します。この三つの見方の間を移るには、`toℕ i < n` のような順序の事実と、`n` 未満の自然数から有限添字を作り直す逆変換が必要です。付随する所属の証明は命題なので、依存対の等しさはデータの成分によって決まります。

```agda
open import Cubical.Data.Nat.Order
  using ( _<_; ≤-refl; ≤-suc; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-split; zero-≤ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
open import Cubical.Data.Sigma using ( Σ≡Prop )
```

単射性の証明では、後続数未満の添字について、前の数未満である場合と最後の添字である場合を繰り返し分けます。命題外延性は二つの所属の含意を集合の等しさへ変え、累積階層はこの議論を行う集合とその標準的な提示を与えます。

```agda
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```

フォン・ノイマン数項とその後続演算は、有限な長さを内部集合 `ω` と結び付けます。不可能な有限上界は空型で表します。整礎帰納法が現れるのは、後で平方律から対の圧縮を構成するときだけであり、与えられた有限列を畳み込む初等的な再帰には用いません。

```agda
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV; #_ )
import Cubical.Induction.WellFounded as WF
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

命題的切り詰めは、ある表現が存在することを記録しつつ、どの表現が与えられたかを意図的に忘れます。その除去則を使うのは、集合の所属や等しさのように、目標自身が命題である場合だけです。この制限により、長さ、割り当て、内部グラフを暗黙に選ぶことなく、存在と単射性を証明できます。

```agda
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

周囲の水準では、所属は命題値です。切り詰められた証人を所属の主張へ除去するとき、この点が効きます。データは何も選ばれず、所属が成り立つという事実だけが残ります。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

周囲の累積階層上の命題値構造を `SV` と書きます。これは、順序対の符号、数項、集合論的グラフを構成可能な対象として見る前に比較するための、外側の所属概念を与えます。

```agda
module SV = hPropStructure 𝒮ᵥ using ()
```

構成可能構造 `SL` の台を `S` と書きます。`S` の要素は、周囲の集合と、それが `L` に属すことの証拠からなります。したがって、内部単射で用いる列の集合、グラフ、順序数には、いずれも実際の構成可能な代表があります。

```agda
module SL = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
open SL using ( S )
```

`S` の定数を含む論理式は構成可能構造で評価され、その原子的な内容は周囲の集合へ射影して読むこともできます。`L` の推移性により二つの読み方が一致するので、対象言語のグラフ条件から、畳み込みで用いる周囲の所属の等式を得られます。

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

数項 `nn k` は、周囲のフォン・ノイマン数項とその構成可能性の証明をまとめたものです。数項は有限環境の正確な定義域を示し、零の数項は畳み込みの初期累積値と `ext` の範囲外での無意味な既定値にもなり、長さの数項は完了した畳み込みにタグを付けます。これらの役割によって、有限添字を構成可能モデルの内部で扱えます。

```agda
nn : ℕ → S
nn k = # k , numL k
```

## 集合上のすべての有限列を集める

`A` の上の列とは、ホストの水準では、有限順序数から `A` の提示への関数です。小さな索引型は、長さとそのような関数の対を集めます。これはホストの水準の概念であり、集合で符号化された対応物は、この後で定義されます。

```agda
SeqIx : S → Type ℓ
SeqIx A = Σ[ n ∈ ℕ ] Ix A n
```

小さな定義域の原理は、`A` の上のすべての有限長の環境グラフを含む、一つの構成可能な集合を与えます。これは共通の容器にすぎません。正確な集合は後の分出で刻まれ、この容器がちょうどその像であるとは主張しません。

```agda
private
  amb : (A : S) → S
  amb A = smallDom (SeqIx A) (λ p → envS A (snd p)) .fst
```

特定の長さ `n` と割り当て `g` に対し、グラフ `envS A g` は共通の容器に属します。この包含が分出による所属の外側の半分を与え、定義論理式が有限環境であるという正確な条件を与えます。

```agda
  amb-in : (A : S) (p : SeqIx A) → ⟨ fst (envS A (snd p)) ∈ˢ fst (amb A) ⟩
  amb-in A = smallDom (SeqIx A) (λ p → envS A (snd p)) .snd
```

この一変数論理式は、候補 `x` が `A` 上の環境のグラフであり、その定義域が内部の `ω` のある要素であることを述べます。したがって、有界な証人について最初に分かるのは `ω` に属すことだけです。そこから実際の自然数の長さを復元するのは後の段階であり、その結果も命題的に切り詰められています。

```agda
seqFo : S → Formula S 1
seqFo A = ∃̇∈ (con ωʟ) (∃̇ ( (var zero ≐ con A)
                        ∧̇ envOverAt (suc (suc zero)) (suc zero) zero ))
```

ここで分出を用いて、共通の容器に含まれる余分な要素を除きます。得られる集合 `seqL A` は、容器の要素のうち有限環境の記述を満たすものをちょうど含みます。定義を不透明に保つことは正規化にだけ影響し、数学的内容は続く所属の等式によって完全に定まります。

```agda
opaque
  seqL : S → S
  seqL A = hasSeparationL (amb A) (seqFo A) .fst .fst
```

ある要素が `seqL A` に属すのは、それが共通の容器に属し、かつ `seqFo A` を満たすとき、そしてそのときに限ります。容器は集合としての大きさを保証し、論理式は正確さを保証します。どちらか一方だけでは、すべての有限列の集合を特徴づけられません。

```agda
  seqL-spec : (A x : S) → (x SL.∈ˢ seqL A)
            ≡ ((x SL.∈ˢ amb A) ⊓ ((x ∷ []) ⊨ seqFo A))
  seqL-spec A = hasSeparationL (amb A) (seqFo A) .fst .snd
```

長さ `n` の環境集合のすべての要素は `seqL A` に属します。証明は、その要素の切り詰められた提示を読み、その後に分出された集合の中へ導入します。

```agda
seqL-in : (A : S) (n : ℕ) (x : S)
        → ⟨ fst x ∈ˢ fst (envSet A n) ⟩ → ⟨ fst x ∈ˢ fst (seqL A) ⟩
seqL-in A n x hx = PT.rec (snd (fst x ∈ˢ fst (seqL A))) from (envSet-out A n x hx)
  where
  from : Σ[ g ∈ Ix A n ] (fst x ≡ fst (envS A g)) → ⟨ fst x ∈ˢ fst (seqL A) ⟩
```

その要素はグラフの形へ運ばれ、界定の記録によって容器の中にあります。そして、正準な項目によって記述が充足されます。

```agda
  from (g , e) = subst (λ w → ⟨ w ∈ˢ fst (seqL A) ⟩) (sym e) canonical
    where
    canonical : ⟨ fst (envS A g) ∈ˢ fst (seqL A) ⟩
    canonical = subst ⟨_⟩ (sym (seqL-spec A (envS A g)))
      ( amb-in A (n , g)
```

記述の証人は、長さの数項、内部の `ω` への所属、そして `A` の上の環境のグラフの関係からなり、すべて切り詰められた存在の中にまとめられます。

```agda
      , ∣ nn n , (#∈ω n , ∣ A , (refl , envOver A g) ∣₁) ∣₁ )
```

逆に、`seqL A` への所属から得られるのは、ある自然数の長さ `n` が存在し、その要素が `envSet A n` に属すという命題的に切り詰められた主張だけです。分出の等式のうち容器の成分を捨て、定義論理式から存在情報を読み取りますが、すべての要素に対して長さを一様に選ぶわけではありません。

```agda
seqL-out : (A x : S) → ⟨ fst x ∈ˢ fst (seqL A) ⟩
         → ∥ Σ[ n ∈ ℕ ] ⟨ fst x ∈ˢ fst (envSet A n) ⟩ ∥₁
seqL-out A x hx = PT.rec squash₁ step1 (subst ⟨_⟩ (seqL-spec A x) hx .snd)
  where
  step2 : (d : S) (k : ℕ) → # k ≡ fst d
```

切り詰められた証人の一つの分岐の中で、定義域の対象 `d` が数項 `# k` と、基礎の対象 `b` が `A` と同一視され、`x` が環境条件を満たすとします。これらの固定された証人に対して、復元過程は長さ `k` の割り当てを構成し、`x` をそのグラフと同一視します。外側の結果は再び切り詰められるので、この局所的な構成は大域的な復号写像を定めません。

```agda
        → Σ[ b ∈ S ] ((fst b ≡ fst A)
             × ⟨ (b ∷ d ∷ x ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩)
        → ∥ Σ[ n ∈ ℕ ] ⟨ fst x ∈ˢ fst (envSet A n) ⟩ ∥₁
  step2 d k q (b , eb , hov) =
    ∣ k , subst (λ w → ⟨ w ∈ˢ fst (envSet A k) ⟩) (sym R.recovers) (envSet-in A R.g) ∣₁
```

長さ `k` を固定すると、環境の各条件がそれぞれの項目を一意に定めます。正確な定義域が切り詰められた存在を与え、一価性が項目のファイバーを命題にし、値の制限が復元された値を `A` の提示に置きます。さらに、グラフのすべての要素が対の形をもつという条件も用い、外延性によって集合 `x` 全体を標準的な環境のグラフと同一視します。

```agda
    where
    module R = Recover A k (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero
                 (sym q) eb hov using ( g; recovers )
```

残りの段階は、定義域の `ω` への所属を消去します。`ω` の要素は、単に、ある数項です。

```agda
  step1 : Σ[ d ∈ S ] (⟨ fst d ∈ˢ ω ⟩
            × ∥ Σ[ b ∈ S ] ((fst b ≡ fst A)
                 × ⟨ (b ∷ d ∷ x ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩) ∥₁)
        → ∥ Σ[ n ∈ ℕ ] ⟨ fst x ∈ˢ fst (envSet A n) ⟩ ∥₁
  step1 (d , d∈ω , h) = PT.rec squash₁
```

数項が変換の一歩に渡され、読みの方向が完成します。強さに注意してください。長さと環境は切り詰めの中でだけ復元され、`seqL A` から割り当てへの大域的な復号器が作られるわけではありません。

```agda
    (λ { (k , q) → PT.rec squash₁ (step2 d (lower k) q) h }) d∈ω
```

## 有限列を一つの順序数コードへ畳み込む

符号化のモジュールは、対の関数のデータを固定します。引数は、順序数 `α`、`α` が `ω` に属さないこと、すなわちこの章が使う形での無限性の仮定、そして構成可能なグラフ `F` と、一価性・積の上の全域性・単射性という三つの節です。

```agda
module Code (α : S) (oα : IsOrd (fst α)) (α∉ω : ⟨ fst α ∈ˢ ω ⟩ → Empty.⊥)
            (F : S)
            (sv : ⟨ (F ∷ prodL α ∷ []) ⊨ svAt zero ⟩)
            (dm : ⟨ (F ∷ prodL α ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ij : ⟨ (F ∷ prodL α ∷ []) ⊨ injAt zero ⟩)
```

最後の仮定は、メタレベルの形での値域の条件です。グラフに記録されたすべての値は `α` に属します。四つの節合わせて、`F` が積 `α × α` から `α` への内部の符号化された単射であることを言います。

```agda
            (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                 → ⟨ fst y ∈ fst α ⟩) where
```

入力と値の台は、構成可能な集合と `α` への所属の対の型です。積の項目も、すべての値も、`α` の中になければなりません。

```agda
  M : Type (ℓ-suc ℓ)
  M = Σ[ v ∈ S ] ⟨ fst v ∈ˢ fst α ⟩
```

数項は台の要素になります。`α` が `ω` に属さないため、`α` の無限性がすべての数項を `α` の中に置くからです。これが、畳み込みにおける無限性の仮定の唯一の用途です。

```agda
  num : ℕ → M
  num k = nn k , ω⊆ (fst α) oα α∉ω (# k) (#∈ω k)
```

`α` の提示の索引も台の要素になります。構成可能性は `α` の所属に沿って運ばれ、所属は提示によって証明されます。

```agda
  up : ⟪ fst α ⟫ → M
  up m = (⟪ fst α ⟫↪ m , isL-trans (member (fst α) m) (snd α)) , member (fst α) m
```

一価性と正確な定義域の条件を合わせると、グラフ `F` を `prodL α` の要素上の実際のホスト関数として読めます。定義域への所属から最初に得られる出力は切り詰められていますが、可能な出力のファイバーは命題なので、その一意な値を取り出せます。等しい出力から入力の等しさを結論するには、別の仮定 `ij` がなお必要です。

```agda
  module E = Extract F (prodL α) sv dm using ( toFun; toFun-graph; toFun-inj )
```

台の二つの要素の符号化された対は積の中にあります。両方の座標が `α` の中にあり、対の演算がそれを `prodL α` への所属に変えるからです。

```agda
  opaque
    pairMem : (a u : M) → ⟨ fst (prʟ (fst a) (fst u)) ∈ˢ fst (prodL α) ⟩
    pairMem a u = subst (λ w → ⟨ w ∈ˢ fst (prodL α) ⟩) (sym (prʟ-fst (fst a) (fst u)))
                    (prodL-in α (fst a) (fst u) (snd a) (snd u))
```

`prodL α` に属すことが分かっている入力 `x` に対し、`val x` を `F` が `x` に記録する一意な出力と定めます。所属の証明も入力データに含めるのは、グラフが全域的であると要求されるのがちょうどこの積の上だけであり、すべての構成可能集合の上ではないからです。

```agda
  opaque
    val : (x : S) → ⟨ fst x ∈ˢ fst (prodL α) ⟩ → S
    val x mx = E.toFun (x , mx)
```

グラフの記録は、入力と値の順序対が `F` に属することを述べます。これが、後の同一視の補題が消費するデータです。

```agda
    val-graph : (x : S) (mx : ⟨ fst x ∈ˢ fst (prodL α) ⟩)
              → ⟨ pr (fst x) (fst (val x mx)) ∈ fst F ⟩
    val-graph x mx = E.toFun-graph (x , mx)
```

グラフは積の上で単射です。同じ値をもつ二つの点は、底の集合が等しくなります。抽出と合わせて、これが対の関数の単射の半分です。

```agda
    val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst (prodL α) ⟩)
              (x' : S) (mx' : ⟨ fst x' ∈ˢ fst (prodL α) ⟩)
            → fst (val x mx) ≡ fst (val x' mx') → fst x ≡ fst x'
    val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')
```

二項演算 `app a u` は、`a` と `u` の内部順序対におけるグラフ `F` の値を取ります。その値はグラフのファイバーから得られるので、すでに構成可能集合です。さらに値域の条件が、その値が `α` に属すことを証明します。したがって `app` は台 `M` 上で閉じています。

```agda
  opaque
    app : M → M → M
    app a u = val (prʟ (fst a) (fst u)) (pairMem a u)
            , ran (prʟ (fst a) (fst u)) (val (prʟ (fst a) (fst u)) (pairMem a u))
                (val-graph (prʟ (fst a) (fst u)) (pairMem a u))
```

値を取り出しても、内部グラフとのつながりは失われません。定理 `app-graph` は、`(a,u)` の周囲の対符号を入力とし、`app a u` を出力とする順序対が `F` に属すことを記録します。構成可能な対の射影等式が、二つの入力符号の間に必要な同一視を与えます。

```agda
    app-graph : (a u : M)
              → ⟨ pr (pr (fst (fst a)) (fst (fst u))) (fst (fst (app a u))) ∈ fst F ⟩
    app-graph a u = subst (λ w → ⟨ pr w (fst (fst (app a u))) ∈ fst F ⟩)
                      (prʟ-fst (fst a) (fst u))
                      (val-graph (prʟ (fst a) (fst u)) (pairMem a u))
```

二つの適用の出力が等しければ、まず `F` の単射性によって、それらの符号化された対入力が同一視されます。次に順序対符号の単射性が、この等しさを二つの第一座標の等しさと二つの第二座標の等しさへ分けます。したがって、`F` の逆関数を構成せずに、適用を一層ずつ剥がせます。

```agda
    app-inj : (a u a' u' : M) → fst (fst (app a u)) ≡ fst (fst (app a' u'))
            → (fst (fst a) ≡ fst (fst a')) × (fst (fst u) ≡ fst (fst u'))
    app-inj a u a' u' e = pr-inj
      (sym (prʟ-fst (fst a) (fst u))
       ∙ val-inj (prʟ (fst a) (fst u)) (pairMem a u) (prʟ (fst a') (fst u')) (pairMem a' u') e
```

対入力の比較では、構成可能な対符号から周囲のクラトフスキー対符号へ移り、さらに戻ります。これらの輸送の後、対の単射性が `app-inj` に必要な二つの成分の等しさをちょうど与えます。付随する所属の証明を比較する必要はありません。

```agda
       ∙ prʟ-fst (fst a') (fst u'))
```

対になる一意性の事実は、グラフを順方向に用います。`F` が入力対 `(a,u)` にある値 `w` を記録しているなら、`w` はすでに取り出した値 `app a u` と等しくなければなりません。これはグラフの一価性であり、異なる入力の間の単射性とは独立です。

```agda
    app-uniq : (a u : M) (w : S)
             → ⟨ pr (pr (fst (fst a)) (fst (fst u))) (fst w) ∈ fst F ⟩
             → fst w ≡ fst (fst (app a u))
    app-uniq a u w h =
      svAt-out zero (F ∷ prodL α ∷ []) sv (prʟ (fst a) (fst u)) w (fst (app a u))
```

一価性を適用するため、まず与えられた所属を周囲の対符号から `val` が用いる構成可能な対へ輸送します。次に、それを抽出された値についての標準的な所属 `val-graph` と比較します。二つの項目は同じ入力をもつので、一価性の条件がそれらの出力を同一視します。

```agda
        (subst (λ z → ⟨ pr z (fst w) ∈ fst F ⟩) (sym (prʟ-fst (fst a) (fst u))) h)
        (val-graph (prʟ (fst a) (fst u)) (pairMem a u))
```

環境の読みは、数項の上の全域的な関数へ延長されます。列の範囲の外では数項のゼロを返します。この既定の値に数学的な意味はなく、後の使用はすべて、長さより下の索引でだけこの延長を読みます。

```agda
  ext : (n : ℕ) → (Fin n → ⟪ fst α ⟫) → ℕ → M
  ext zero    g k       = num zero
  ext (suc n) g zero    = up (g zero)
  ext (suc n) g (suc k) = ext n (λ i → g (suc i)) k
```

索引についての再帰により、長さより下のどの索引でも、延長は列のその項目をちょうど読み戻します。

```agda
  ext-at : (n : ℕ) (g : Fin n → ⟪ fst α ⟫) (i : Fin n) → ext n g (toℕ i) ≡ up (g i)
  ext-at (suc n) g zero    = refl
  ext-at (suc n) g (suc i) = ext-at n (λ j → g (suc j)) i
```

長さ `n` と列 `g` を固定すると、`chain n g k` は段階数 `k` についての再帰で定義されます。初期値は零の数項であり、`k<n` を満たす各段階では、対の関数を次の項 `g(k)` とそれまでの累積値に適用します。したがって `chain n g n` は列の `n` 個の項をちょうどすべて消費します。この範囲を越えた後の振る舞いは `ext` の無意味な既定値だけに依存し、列の符号の数学的内容には含まれません。

```agda
  chain : (n : ℕ) → (Fin n → ⟪ fst α ⟫) → ℕ → M
  chain n g zero    = num zero
  chain n g (suc k) = app (ext n g k) (chain n g k)
```

長さ `n` の列では、畳み込みは `vₙ = chain n g n` で終わります。その符号を `F(n,vₙ)` と定めます。最後の対の第一座標が長さの数項、第二座標が畳み込み値です。`n` と `g` が与えられれば、これは実際の値を与えます。`α` のすべての要素が符号であるとも、`α` 全体上の復号写像があるとも述べていません。

```agda
  code : (n : ℕ) → (Fin n → ⟪ fst α ⟫) → M
  code n g = app (num n) (chain n g n)
```

二つの畳み込みの鎖が `k` 段後に一致すると仮定すると、各位置 `j<k` の項も一致します。帰納は鎖を後ろ向きにたどります。段階 `k+1` での等しさを `F` の単射性で分けると、段階 `k` で用いた項の等しさと、一つ前の鎖の値の等しさが得られます。

```agda
  chain-inj : (n : ℕ) (g g' : Fin n → ⟪ fst α ⟫) (k : ℕ)
            → fst (fst (chain n g k)) ≡ fst (fst (chain n g' k))
            → (j : ℕ) → j < k → fst (fst (ext n g j)) ≡ fst (fst (ext n g' j))
  chain-inj n g g' zero    e j j<0  = Empty.rec (¬-<-zero j<0)
  chain-inj n g g' (suc k) e j j<sk = go (<-split j<sk)
```

後者段階では、`app-inj` がこの二つの等しさを与えます。`j=k` なら第一の等しさが求める項の等しさであり、`j<k` なら第二の等しさによって短い鎖へ帰納仮定を適用できます。これは既知の正しい二つの畳み込みの間の消去論法であり、`α` の任意の要素を列へ変える手続きではありません。

```agda
    where
    q = app-inj (ext n g k) (chain n g k) (ext n g' k) (chain n g' k) e
    go : (j < k) ⊎ (j ≡ k) → fst (fst (ext n g j)) ≡ fst (fst (ext n g' j))
    go (inl j<k) = chain-inj n g g' k (snd q) j j<k
    go (inr j≡k) = subst (λ j → fst (fst (ext n g j)) ≡ fst (fst (ext n g' j))) (sym j≡k) (fst q)
```

ここで長さのタグが役割を果たします。二つの符号が等しければ、外側の適用の単射性からまず長さの数項が等しく、したがって自然数としての長さも等しいことが分かります。共通の長さへ輸送した後、畳み込みを後ろ向きに消去すると各項が一致し、二つの環境グラフの底集合も等しくなります。ここで述べるのはこの向きだけです。

```agda
  code-inj : (n : ℕ) (g : Fin n → ⟪ fst α ⟫) (n' : ℕ) (g' : Fin n' → ⟪ fst α ⟫)
           → fst (fst (code n g)) ≡ fst (fst (code n' g'))
           → fst (envS α g) ≡ fst (envS α g')
  code-inj n g n' g' e = subst P (#-inj′ (fst q)) same g' (snd q)
    where
```

対になった結論 `q` は、符号の等式を数項座標の等しさと終端の畳み込み値の等しさに分けます。族 `P m` は、長さ `m` の列について残る主張を正確に記録します。これにより、数項の単射性に沿って第二の列とその畳み込みの等式をもとの長さ `n` へ輸送できます。

```agda
    q = app-inj (num n) (chain n g n) (num n') (chain n' g' n') e
    P : ℕ → Type (ℓ-suc ℓ)
    P m = (h : Fin m → ⟪ fst α ⟫)
        → fst (fst (chain n g n)) ≡ fst (fst (chain m h m))
        → fst (envS α g) ≡ fst (envS α h)
```

長さが一致すれば、環境グラフの等しさは関数外延性から従います。各有限添字 `i` について、`α` の提示における対応する二要素を比較します。提示の埋め込みの単射性により、その等しさは二つの鎖から得た底集合の等しさへ帰着します。

```agda
    same : P n
    same h e' = cong (λ (f : Fin n → ⟪ fst α ⟫) → fst (envS α f)) (funExt pt)
      where
      pt : (i : Fin n) → g i ≡ h i
      pt i = ↪-inj {a = fst α}
```

位置 `i` での比較では、まず `ext-at` によって全域関数 `ext n g` の有界位置での値を本来の項 `g i` と同一視します。`toℕ i<n` なので鎖の消去補題から二つの全域関数の値が等しいと分かり、もう一度 `ext-at` を用いて他方を `h i` と同一視します。この範囲外での `ext` の値には数学的な意味を持たせません。

```agda
        ( sym (cong (λ z → fst (fst z)) (ext-at n g i))
        ∙ chain-inj n g h n e' (toℕ i) (toℕ<n i)
        ∙ cong (λ z → fst (fst z)) (ext-at n h i) )
```

再帰の一回の遷移を意味論的に記述するため、添字対象 `i` を固定します。`StepAt s C i` は、`j` が `i` の後者であり、列のグラフが `s(i)=a`、軌跡が `C(i)=u` と `C(j)=w`、グラフ `F` が `F(a,u)=w` を与えるような対象 `j,a,u,w` を記録するだけです。このデータ全体は命題的に切り詰められています。

```agda
  StepAt : (s C i : S) → Type (ℓ-suc ℓ)
  StepAt s C i = ∥ Σ[ j ∈ S ] Σ[ a ∈ S ] Σ[ u ∈ S ] Σ[ w ∈ S ]
      ( (fst j ≡ sucV (fst i))
      × ⟨ pr (fst i) (fst a) ∈ fst s ⟩
      × ⟨ pr (fst i) (fst u) ∈ fst C ⟩
```

最後の所属の主張は、漸化式をグラフの事実として書いたものです。入力は順序対 `(a,u)`、出力は `w` です。したがって `StepAt` は、後の一階のステップ論理式が表すべきホスト側の意味であり、復号写像や大域的な軌跡の選択を加えるものではありません。

```agda
      × ⟨ pr (fst j) (fst w) ∈ fst C ⟩
      × ⟨ pr (pr (fst a) (fst u)) (fst w) ∈ fst F ⟩ ) ∥₁
```

`DomIs s n` は、`n` が列のグラフ `s` のちょうど定義域であることを述べます。各 `x∈n` には `(x,y)∈s` となる値 `y` があり、逆に `(x,y)∈s` なら第一座標 `x` は `n` に属します。値の存在は命題的切り詰めのもとでだけ保たれ、一意性が必要な箇所では別の環境条件を用います。

```agda
  DomIs : (s n : S) → Type (ℓ-suc ℓ)
  DomIs s n = (x : S)
    → (⟨ fst x ∈ fst n ⟩ → ∥ Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst s ⟩ ∥₁)
    × ((y : S) → ⟨ pr (fst x) (fst y) ∈ fst s ⟩ → ⟨ fst x ∈ fst n ⟩)
```

`EnvC m C` は、`C` が `α` に値を取り、ちょうど `m` を定義域とする環境であることを述べます。`envOverAt` には、一価性、定義域の条件、すべての値が `α` に属すこと、そして `C` の各要素が順序対であることが含まれます。ここで `m` は列の長さの後者になるので、軌跡は `0` から `n` までの位置をもちます。

```agda
  EnvC : (m C : S) → Type (ℓ-suc ℓ)
  EnvC m C = ⟨ (α ∷ m ∷ C ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩
```

完全な意味論的証人は、数項 `n∈ω`、その後者 `m`、軌跡の環境 `C` から始まります。`s` の定義域が `n`、`C` の定義域が `m` で値が `α` に属し、軌跡が `C(0)=0` から始まることを要求します。各 `i∈n` について一つの遷移を与え、最後に `C(n)` の値を `n` と対にすると `y` になることを記録します。この証人は命題的に切り詰められています。

```agda
  Wit : (y s : S) → Type (ℓ-suc ℓ)
  Wit y s = ∥ Σ[ n ∈ S ] Σ[ m ∈ S ] Σ[ C ∈ S ]
      ( ⟨ fst n ∈ ω ⟩
      × (fst m ≡ sucV (fst n))
      × DomIs s n
```

最後の成分は、軌跡の終端値と長さのタグを分けて記録します。ある `v` について `(n,v)∈C` かつ `F(n,v)=y` を与えます。遷移の条件が `v` を `n` 回の畳み込み後の値として決定し、最後の `F` の適用が長さを記録するため、長さの異なる列が同じ符号をもつことはありません。

```agda
      × EnvC m C
      × ⟨ pr (# zero) (# zero) ∈ fst C ⟩
      × ((i : S) → ⟨ fst i ∈ fst n ⟩ → StepAt s C i)
      × ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                     × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁ ) ∥₁
```

量化子を入れ子にすると、それまで使えた各変数の de Bruijn 位置がずれます。略記 `i0,i1,…` はこれらの位置を一様に表し、`i0` が直前に束縛された変数、後者を一回取るごとに一つ外側の変数を指します。この記法により、以下の論理式は各出現がどの対象を指すかを保ったまま有限軌跡の等式を述べられます。

```agda
  private
    i0 : ∀ {k} → Fin (suc k)
    i0 = zero
    i1 : ∀ {k} → Fin (suc (suc k))
    i1 = suc i0
```

`i0` から `i4` までの名前は、現在の添字、その後者、一回の漸化段階で導入される近くの値など、軌跡論理式の浅い部分を扱います。長さについて多相的なので、さらに束縛子を加えた後も同じ位置名を再利用できます。

```agda
    i2 : ∀ {k} → Fin (suc (suc (suc k)))
    i2 = suc i1
    i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
    i3 = suc i2
    i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
```

次の位置は、いくつかの存在証人を導入した後にも、軌跡の環境ともとの自由変数へ届きます。そのため同じ論理式の中で、古い軌跡値、新しい軌跡値、両者を結ぶ列の項を同時に指せます。

```agda
    i4 = suc i3
    i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
    i5 = suc i4
    i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
    i6 = suc i5
```

ステップ論理式は全部で五つの証人を導入します。後者添字 `j`、値 `a,u,w`、そして `(a,u)` の対の符号です。五つの束縛子の内側では、もとの列変数は位置 `i12` まで移ります。この深い添字は束縛の深さから生じるもので、新たな数学的仮定ではありません。

```agda
    i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
    i7 = suc i6
    i8 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))
    i8 = suc i7
    i12 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))))))
```

具体的に、`i12` は `i8` からさらに四回後者を取った位置です。位置名を固定したので、以下の定義では後者構成子を一段ずつ数えず、各変数の数学的役割を追えます。

```agda
    i12 = suc (suc (suc (suc i8)))
```

論理式 `stepFo` は `StepAt` の対象言語での表現です。まず `j` を選び、それが現在の添字 `i` の後者であると述べます。次に列の値 `a`、古い軌跡値 `u`、新しい軌跡値 `w`、順序対 `(a,u)` の符号を選びます。

```agda
  opaque
    private
      stepFo : Formula S 8
      stepFo = ∃̇ (
            sucAtL i1 i0
```

内側の四つの存在量化子は `a,u,w` とその対の符号を束縛します。最初の三つの適用条件はそれぞれ `s(i)=a`、`C(i)=u`、`C(j)=w` を述べ、対の条件は補助符号を `(a,u)` と同一視します。これらが論理式の中心にある一つの漸化条件を準備します。

```agda
         ∧̇ (∃̇ (∃̇ (∃̇ (∃̇ (
              appAt i12 i5 i3
           ∧̇ appAt i8 i5 i2
           ∧̇ appAt i8 i4 i1
           ∧̇ prAtL i0 i3 i2
```

最も内側の連言項は、漸化式を表すグラフの事実です。補助的な入力符号に `F` を適用すると、新しい値 `w` が得られると述べます。その直前の対の条件が、この補助符号を順序対 `(a,u)` と同一視します。二つの条件を合わせて、対象言語で畳み込みの等式 `F(a,u)=w` を表します。

```agda
           ∧̇ appC F i0 i1 ))))))
```

最終長の論理式はこう言います。符号化された環境の数項の枠に値があり、数項とその値に符号化された対を適用すると出力になる、と。

```agda
      finFo : Formula S 7
      finFo = ∃̇ (∃̇ (
            appAt i4 i6 i1
         ∧̇ prAtL i0 i6 i1
         ∧̇ appC F i0 i7 ))
```

本体は軌跡の条件を述べる前に、二つの補助パラメータを明示的に保ちます。`b` を固定したアルファベット `α`、`z` を零の数項と同一視し、続いて `m` が選んだ長さ `n` の後者であると述べます。これらの等式により、後の一般的な環境と適用の論理式を `α` と `0` に特殊化できます。

```agda
      body : Formula S 7
      body =
          (var i1 ≐ con α)
       ∧̇ (var i0 ≐ con (nn zero))
       ∧̇ sucAtL i4 i3
```

残りの連言項は、定義域の条件、環境の上の条件、零の項目の等式、`n` 未満のすべての遷移、そして最終長の条件を課します。現在名前の付いている対象について、これらは `C` が符号化された対を通して初期の零から出力へ至る有限な軌跡であることを述べます。その後で `fo` の外側の量化子が、そのような長さと軌跡の存在を主張します。

```agda
       ∧̇ domAt i6 i4
       ∧̇ envOverAt i2 i3 i1
       ∧̇ appAt i2 i0 i0
       ∧̇ ∀̇∈ (var i4) stepFo
       ∧̇ finFo
```

完全なグラフの論理式は、`ωʟ` の上の有界量化子で数項を束縛し、つづいて入れ子の存在量化子で四つの補助の対象を束縛して、出力と列の上の二つの枠の論理式を作ります。

```agda
    fo : Formula S 2
    fo = ∃̇∈ (con ωʟ) (∃̇ (∃̇ (∃̇ (∃̇ body))))
```

環境 `e7` は、`stepFo` と `finFo` の内側の量化子へ入る前に利用できる七つの対象を含みます。de Bruijn 順では `z,b,C,m,n,y,s` であり、位置零は補助的な零、もとの出力と列は最も外側の二位置にあります。後の束縛子はこの環境の先頭を拡張します。

```agda
    private
      e7 : S → S → S → S → S → S → S → S ^ 7
      e7 y s n m C b z = z ∷ b ∷ C ∷ m ∷ n ∷ y ∷ s ∷ []
```

`stepFo` を外向きに読むため、その命題的に切り詰められた証人を命題 `StepAt s C i` へ除去します。これにより `j,a,u,w` と補助的な対の符号、さらに後者条件、三つのグラフ適用条件、対の条件、`F` の適用条件が得られます。補助的な対の符号は、その等式を使った後には残りません。

```agda
      stepOut : (y s n m C b z i : S)
              → ⟨ (i ∷ e7 y s n m C b z) ⊨ stepFo ⟩ → StepAt s C i
      stepOut y s n m C b z i = PT.rec squash₁ (λ { (j , (ej , ha)) →
        PT.rec squash₁ (λ { (a , hu) → PT.rec squash₁ (λ { (u , hw) →
        PT.rec squash₁ (λ { (w , hp) → PT.rec squash₁ (λ { (p , (h1 , (h2 , (h3 , (h4 , h5))))) →
```

各妥当性の等式は、一つの充足判断を意図された等式またはグラフ所属へ輸送します。得られた事実は `j` を `i` の後者と同一視し、`s` から `a`、`C` から `u,w` を読み取ります。最後の `F` に関するグラフの事実と合わせると、ちょうど `StepAt` が要求する意味論的な形になります。

```agda
          let γ = p ∷ w ∷ u ∷ a ∷ j ∷ i ∷ e7 y s n m C b z in
          ∣ j , a , u , w
          , ( subst ⟨_⟩ (sucAtL-adequate i1 i0 (j ∷ i ∷ e7 y s n m C b z)) ej
            , subst ⟨_⟩ (appAt-adequate i12 i5 i3 γ) h1
            , subst ⟨_⟩ (appAt-adequate i8 i5 i2 γ) h2
```

対についての妥当性の等式は、補助対象を順序対 `(a,u)` と同一視します。その等式に沿って `F` の適用の事実を輸送すると、漸化式を表す所属 `((a,u),w)∈F` が得られます。これで一階のステップ論理式から一回の意味論的遷移への外向きの読み取りが完了します。

```agda
            , subst ⟨_⟩ (appAt-adequate i8 i4 i1 γ) h3
            , subst (λ q → ⟨ pr q (fst w) ∈ fst F ⟩)
                (subst ⟨_⟩ (prAtL-adequate i0 i3 i2 γ) h4)
                (subst ⟨_⟩ (appC-adequate F i0 i1 γ) h5) ) ∣₁ }) hp }) hw }) hu }) ha })
```

`finFo` を外向きに読むと、まず軌跡の終端値 `v` と補助対象 `q` が得られます。三つの条件は `C(n)=v`、`q=(n,v)`、`F(q)=y` を述べます。目標は命題的に切り詰められているので、二つの存在証人を除去し、`Wit` に必要な `v` と二つのグラフの事実だけを残せます。

```agda
      finOut : (y s n m C b z : S) → ⟨ e7 y s n m C b z ⊨ finFo ⟩
             → ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                            × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁
      finOut y s n m C b z = PT.rec squash₁ (λ { (v , hq) →
        PT.rec squash₁ (λ { (q , (h1 , (h2 , h3))) →
```

妥当性により、三つの条件は `C(n)=v` と `F(q)=y` を表す所属、および等式 `q=(n,v)` へ移されます。最後の等式に沿って `F` への所属を輸送し、`q` を `(n,v)` で置き換えると、グラフの形で `F(n,v)=y` が得られます。

```agda
          let γ = q ∷ v ∷ e7 y s n m C b z in
          ∣ v , ( subst ⟨_⟩ (appAt-adequate i4 i6 i1 γ) h1
                , subst (λ r → ⟨ pr r (fst y) ∈ fst F ⟩)
                    (subst ⟨_⟩ (prAtL-adequate i0 i6 i1 γ) h2)
                    (subst ⟨_⟩ (appC-adequate F i0 i7 γ) h3) ) ∣₁ }) hq })
```

本体には八つの連言項があります。最初の二つは補助対象を `b=α`、`z=0` と同一視し、残る六つは `m=n+1`、`s` の正確な定義域、`C` の環境条件、`C(0)=0`、`n` 未満のすべての遷移、最後の長さ付きの値を述べます。別に与えられた `n∈ω` と合わせると、これらが `Wit y s` を構成します。

```agda
      bodyOut : (y s n m C b z : S) → ⟨ fst n ∈ ω ⟩
              → ⟨ e7 y s n m C b z ⊨ body ⟩ → Wit y s
      bodyOut y s n m C b z n∈ω (eb , (ez , (em , (hd , (hE , (h0 , (hS , hF))))))) =
        ∣ n , m , C
        , ( n∈ω
```

後者論理式の妥当性の等式から `m=n+1` が得られ、`domAt` の二つの読み方から `s` の正確な定義域について両方向の所属が得られます。さらに `b=α` を用い、環境の論理式を補助的な基礎集合 `b` から固定した `α` へ輸送します。軌跡全体の等しさは必要ありません。

```agda
          , subst ⟨_⟩ (sucAtL-adequate i4 i3 (e7 y s n m C b z)) em
          , (λ x → domAt-in i6 i4 (e7 y s n m C b z) hd x
                 , domAt-out i6 i4 (e7 y s n m C b z) hd x)
          , envOverAt-transport (e7 y s n m C b z) (α ∷ m ∷ C ∷ [])
              i2 i3 i1 (suc (suc zero)) (suc zero) zero refl refl eb hE
```

等式 `z=0` によって、本体の条件 `C(z)=z` は初期条件 `C(0)=0` へ移されます。有界全称の条件は `stepOut` によって各点で読まれ、`finOut` がタグ付きの終端値を与えます。これらが命題的に切り詰められた証人の残りの成分です。

```agda
          , subst (λ w → ⟨ pr w w ∈ fst C ⟩) ez
              (subst ⟨_⟩ (appAt-adequate i2 i0 i0 (e7 y s n m C b z)) h0)
          , (λ i i∈n → stepOut y s n m C b z i (hS i i∈n))
          , finOut y s n m C b z hF ) ∣₁
```

完全な論理式の外向きの読み出しは、五重の入れ子の存在量化子を一つずつ消去し、それぞれを本体の読み出しに渡して、完全な証人が組み立てられるまで続けます。

```agda
    fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
    fo-out y s = PT.rec squash₁ (λ { (n , (n∈ω , hm)) →
      PT.rec squash₁ (λ { (m , hC) → PT.rec squash₁ (λ { (C , hb) →
      PT.rec squash₁ (λ { (b , hz) → PT.rec squash₁ (λ { (z , hbody) →
        bodyOut y s n m C b z n∈ω hbody }) hz }) hb }) hC }) hm })
```

逆向きの構成は、命題的に切り詰められた一つの `StepAt` 証人を `stepFo` の充足へ写すことから始まります。代表 `j,a,u,w` に対し、その対の符号と四つの値で環境を拡張します。続く条件が、後者と各グラフに関する主張を対象言語の形で組み立て直します。

```agda
    private
      stepIn : (y s n m C i : S) → StepAt s C i
             → ⟨ (i ∷ e7 y s n m C α (nn zero)) ⊨ stepFo ⟩
      stepIn y s n m C i = PT.map (λ { (j , a , u , w , (ej , ha , hu , hw , hF)) →
        let γ = prʟ a u ∷ w ∷ u ∷ a ∷ j ∷ i ∷ e7 y s n m C α (nn zero) in
```

各証人は `stepFo` が束縛する順序で導入されます。後者と適用に関する妥当性の等式を逆向きに用い、意味論的事実 `j=i+1`、`s(i)=a`、`C(i)=u`、`C(j)=w` を対応する充足判断へ移します。既にある証人を導入するだけで、命題的切り詰めから選択するのではないため、入れ子の切り詰めは保たれます。

```agda
        j , ( subst ⟨_⟩ (sym (sucAtL-adequate i1 i0 (j ∷ i ∷ e7 y s n m C α (nn zero)))) ej
            , ∣ a , ∣ u , ∣ w , ∣ prʟ a u
            , ( subst ⟨_⟩ (sym (appAt-adequate i12 i5 i3 γ)) ha
              , ( subst ⟨_⟩ (sym (appAt-adequate i8 i5 i2 γ)) hu
              , ( subst ⟨_⟩ (sym (appAt-adequate i8 i4 i1 γ)) hw
```

標準的な構成可能な対 `prʟ a u` が、補助的な対変数の証人になります。対についての妥当性がその底集合を `(a,u)` と同一視し、所属 `((a,u),w)∈F` を輸送すると、必要な対象言語の適用条件が得られます。これで一回の遷移の内向きの読み取りが完了します。

```agda
              , ( subst ⟨_⟩ (sym (prAtL-adequate i0 i3 i2 γ)) (prʟ-fst a u)
                , subst ⟨_⟩ (sym (appC-adequate F i0 i1 γ))
                    (subst (λ q → ⟨ pr q (fst w) ∈ fst F ⟩) (sym (prʟ-fst a u)) hF) )))) ∣₁ ∣₁ ∣₁ ∣₁ ) })
```

`finFo` の内向きの読み取りは、`C(n)=v` かつ `F(n,v)=y` を満たす、命題的に切り詰められた終端値 `v` から始まります。この証人を `finFo` の二つの存在量化子へ写します。一つは `v`、もう一つは順序対 `(n,v)` の明示的な符号を束縛します。

```agda
      finIn : (y s n m C : S)
            → ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                           × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁
            → ⟨ e7 y s n m C α (nn zero) ⊨ finFo ⟩
      finIn y s n m C = PT.map (λ { (v , (hv , hy)) →
```

環境を `v` と標準的な対 `prʟ n v` で拡張します。適用の妥当性を逆向きに用いて `C(n)=v` を表し、対の妥当性を逆向きに用いて対の証人を同一視し、定数グラフ `F` への適用の妥当性を逆向きに用いて `F(n,v)=y` を表します。

```agda
        let γ = prʟ n v ∷ v ∷ e7 y s n m C α (nn zero) in
        v , ∣ prʟ n v
            , ( subst ⟨_⟩ (sym (appAt-adequate i4 i6 i1 γ)) hv
              , ( subst ⟨_⟩ (sym (prAtL-adequate i0 i6 i1 γ)) (prʟ-fst n v)
                , subst ⟨_⟩ (sym (appC-adequate F i0 i7 γ))
```

最後の輸送は、周囲の順序対 `(n,v)` を入力とするグラフ所属を、構成可能な代表 `prʟ n v` を用いた充足へ移します。したがって、命題的切り詰めが既に保持する証人以外を選ぶことなく、終端条件が再構成されます。

```agda
                    (subst (λ q → ⟨ pr q (fst y) ∈ fst F ⟩) (sym (prʟ-fst n v)) hy) )) ∣₁ })
```

本体を再構成するため、六つの実質的な軌跡条件を仮定します。すなわち `m=n+1`、`s` の正確な定義域、`C` の環境条件、初期値、すべての有界な遷移、タグ付きの終端値です。本体に残る二つの連言項は固定された同一視 `b=α` と `z=0` であり、追加の仮定を必要としません。

```agda
      bodyIn : (y s n m C : S) → fst m ≡ sucV (fst n) → DomIs s n → EnvC m C
             → ⟨ pr (# zero) (# zero) ∈ fst C ⟩
             → ((i : S) → ⟨ fst i ∈ fst n ⟩ → StepAt s C i)
             → ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                            × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁
```

選んだ七対象の環境では、二つの補助項目は定義上そのまま `α` と `0` です。したがって本体の最初の二つの連言項は反射律で証明されます。残りの証明は、与えられた六つの意味論的条件を残る六つの対象言語の連言項へ移します。

```agda
             → ⟨ e7 y s n m C α (nn zero) ⊨ body ⟩
      bodyIn y s n m C em hd hE h0 hS hF =
        let γ = e7 y s n m C α (nn zero) in
          refl
        , ( refl
```

後者についての妥当性を逆向きに用いると、`m=n+1` を表す連言項が得られます。`domAt` の導入方向は `DomIs` の二方向を組み合わせます。グラフ値の存在が命題的に切り詰められているため一方では命題への除去を用い、他方はもともと直接の含意です。続いて環境条件を選ばれた変数位置へ輸送します。

```agda
        , ( subst ⟨_⟩ (sym (sucAtL-adequate i4 i3 γ)) em
        , ( domAt-intro i6 i4 γ (λ x →
              PT.rec (snd (fst x ∈ fst n)) (λ { (yy , p) → hd x .snd yy p })
            , hd x .fst)
        , ( envOverAt-transport (α ∷ m ∷ C ∷ []) γ
```

初期の所属 `C(0)=0` は、適用の妥当性を通して第六の連言項を与えます。`n` 未満の各遷移は `stepIn` によって内向きに送られ、`finIn` が最後のタグ付きの値の条件を再構成します。先の五つの事実と合わせて、有限軌跡の本体にある八つの連言項がすべて完成します。

```agda
              (suc (suc zero)) (suc zero) zero i2 i3 i1 refl refl refl hE
        , ( subst ⟨_⟩ (sym (appAt-adequate i2 i0 i0 γ)) h0
        , ( (λ i i∈n → stepIn y s n m C i (hS i i∈n))
        , finIn y s n m C hF ))))))
```

完全な論理式の内向きの読み出しは、切り詰められた証人を消去し、五つの対象を五重の入れ子の存在量化子を通して注入して、グラフの論理式の対象言語の充足を組み立てます。

```agda
    fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
    fo-in y s = PT.rec (snd ((y ∷ s ∷ []) ⊨ fo))
      (λ { (n , m , C , (n∈ω , em , hd , hE , h0 , hS , hF)) →
        ∣ n , ( n∈ω
              , ∣ m , ∣ C , ∣ α , ∣ nn zero
```

五つの証人は `n,m,C,α,0` です。最初のものは `ω` 上の有界存在量化子、残る四つは通常の存在量化子を通して導入されます。固定した `α` と `0` によって本体の最初の二等式は反射律で成り立ち、`bodyIn` が後者、定義域、環境、初期値、遷移、終端の条件を与えます。したがって `fo-in` は、切り詰められた証人から大域的に代表を選ぶことなく、完全な充足を再構成します。

```agda
              , bodyIn y s n m C em hd hE h0 hS hF ∣₁ ∣₁ ∣₁ ∣₁ ) ∣₁ })
```

次に、この意味論的論理式を実際の有限列に適用します。長さ `N`、割り当て `g : Fin N → α`、構成可能集合 `s`、そして `s` の底集合を環境グラフ `envS α g` と同一視する等式を固定します。以下では、この表現された列について論理式の出力が存在し一意であることを示します。

```agda
  module AtSeq (N : ℕ) (g : Fin N → ⟪ fst α ⟫) (s : S) (e : fst s ≡ fst (envS α g)) where
```

標準的な環境グラフについて一般的な環境論理式を使うには、基礎集合 `α`、長さの数項 `N`、`envS α g` の三対象で十分です。`δ` における de Bruijn 順では、グラフが位置二、数項が位置一、基礎集合が位置零に置かれます。

```agda
    private
      δ : S ^ 3
      δ = α ∷ nn N ∷ envS α g ∷ []
```

標準グラフ `envS α g` は、`α` に値を取り、`N` を定義域とする環境であることが既に分かっています。この環境の事実から定義域の条件を取り出すと、その正確な定義域が数項 `#N` であることが示されます。後でこの事実により、同じ列に対するどの別の証人も同じ有限長を使うことが強制されます。

```agda
      dom0 : ⟨ δ ⊨ domAt (suc (suc zero)) (suc zero) ⟩
      dom0 = envOver-dom (suc (suc zero)) (suc zero) zero δ (envOver α g)
```

環境の参照定理を使うには、まず割り当てを `V` の集合族として見ます。写像 `gV` は各有限添字を、表示要素 `g i` が名指す底集合へ送ります。`g i` は `α` の要素を表示しているので、これはその添字に記録される値そのものです。

```agda
      gV : Fin N → V ℓ
      gV i = ⟪ fst α ⟫↪ (g i)
```

`k < N` なら、正準な環境は、第一成分が数項 `# k`、第二成分が列の第 `k` 項である順序対を含みます。証明では `k` を `Fin N` の要素に直し、そこで参照の仕様を適用して、得られた所属を自然数の添字へ戻します。

```agda
      extMem : (k : ℕ) (p : k < N)
             → ⟨ pr (# k) (fst (fst (ext N g k))) ∈ fst (envS α g) ⟩
      extMem k p = subst (λ k → ⟨ pr (# k) (fst (fst (ext N g k))) ∈ fst (envS α g) ⟩)
        (toFromId' N k p)
        (subst ⟨_⟩ (sym (lookup-spec gV i (fst (fst (ext N g (toℕ i))))))
```

等式 `ext-at` は、全域化された参照 `ext N g (toℕ i)` を本来の項 `g i` と同一視します。続いて、有界な自然数と `Fin N` の間の往復等式により、添字と表示された値の両方が元の `k` に戻ります。

```agda
          (cong (λ z → fst (fst z)) (ext-at N g i)))
        where
        i : Fin N
        i = fromℕ' N k p
```

逆向きの参照は、各有効添字での単値性を表します。`k < N` のとき環境が `(# k,a)` を含むなら、`a` の底集合は実際の第 `k` 項の底集合に等しく、その添字に別の値を記録することはできません。

```agda
      s-uniq : (k : ℕ) (p : k < N) (a : S)
             → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩
             → fst a ≡ fst (fst (ext N g k))
      s-uniq k p a ha =
          subst ⟨_⟩ (lookup-spec gV i (fst a))
```

この同一視は、対応する `Fin N` の添字で行います。参照等式がまず `a` を決定し、`ext-at` が全域化された項を元の割り当ての項に戻し、変換の恒等式が結論を `k` へ運びます。

```agda
            (subst (λ k → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩) (sym (toFromId' N k p)) ha)
        ∙ sym (cong (λ z → fst (fst z)) (ext-at N g i))
        ∙ cong (λ k → fst (fst (ext N g k))) (toFromId' N k p)
        where
        i : Fin N
```

ここで `i = fromℕ' N k p` は、境界 `p : k < N` によって正当化される有限添字です。この境界を明示することが大切です。全域関数 `ext` は、この範囲の外では列としての意味をもちません。

```agda
        i = fromℕ' N k p
```

畳み込みには、初期値から `N` 個すべての項を処理した後の状態まで、`N + 1` 個の状態があります。各状態にはすでに `α` への所属証明があり、`fiber` はその所属を表示要素へ変えて、`Fin (suc N)` で添字づけられた割り当て `h` を作ります。

```agda
      h : Fin (suc N) → ⟪ fst α ⟫
      h i = fiber (fst α) (snd (chain N g (toℕ i))) .fst
```

族 `hV` は表示添字を忘れて、それらが名指す `V` の底集合へ戻ります。後で使うファイバー等式により、これらが `h` のもとになった畳み込み状態そのものであることが分かります。

```agda
      hV : Fin (suc N) → V ℓ
      hV i = ⟪ fst α ⟫↪ (h i)
```

この状態割り当ての環境グラフを `C` とします。その定義域の長さは `N + 1` で、`k` 番目には列の最初の `k` 項を処理した後の畳み込み状態が記録されます。`k = 0` の初期状態と `k = N` の最終状態も含まれます。

```agda
      C : S
      C = envS α h
```

各 `k < N + 1` に対し、`chainMem` は期待されるグラフ項 `(# k, chain N g k)` が `C` に属することを示します。元の列の場合と同様に、対応する `Fin (suc N)` の要素へ移り、環境の参照仕様を使います。

```agda
      chainMem : (k : ℕ) (p : k < suc N)
               → ⟨ pr (# k) (fst (fst (chain N g k))) ∈ fst C ⟩
      chainMem k p = subst (λ k → ⟨ pr (# k) (fst (fst (chain N g k))) ∈ fst C ⟩)
        (toFromId' (suc N) k p)
        (subst ⟨_⟩ (sym (lookup-spec hV i (fst (fst (chain N g (toℕ i))))))
```

ファイバー等式は `h i` が名指す値を実際の畳み込み状態と同一視し、`toFromId'` は元の自然数添字を復元します。この二つの同一視によってグラフへの所属が証明され、`N + 1` の外の添字については何も主張しません。

```agda
          (sym (fiber (fst α) (snd (chain N g (toℕ i))) .snd)))
        where
        i : Fin (suc N)
        i = fromℕ' (suc N) k p
```

固定した等式 `e : fst s ≡ fst (envS α g)` により、正準な環境についての事実を、表示される列 `s` に使えます。`inS` は `envS α g` の正準なグラフ項を `s` へ運びます。

```agda
      inS : (k : ℕ) (a : S) → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩ → ⟨ pr (# k) (fst a) ∈ fst s ⟩
      inS k a = subst (λ w → ⟨ pr (# k) (fst a) ∈ w ⟩) (sym e)
```

逆向きの輸送 `outS` は、`s` の任意のグラフ項を `envS α g` へ戻します。一意性の議論では、任意の証人となる連鎖が与える項を実際の割り当ての項と比較するために、この向きを使います。

```agda
      outS : (k : ℕ) (a : S) → ⟨ pr (# k) (fst a) ∈ fst s ⟩ → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩
      outS k a = subst (λ w → ⟨ pr (# k) (fst a) ∈ w ⟩) e
```

ここで正準な符号がグラフ論理式を満たすことを確かめます。証人には有限長の数項 `# N`、その後続 `#(N+1)`、状態環境 `C` を選びます。残りの成分は、`s` の定義域、`α` に値をとる状態列、零の初期状態、各遷移、最後の対グラフの適用を証明します。

```agda
    wit : Wit (fst (code N g)) s
    wit = ∣ nn N , nn (suc N) , C
          , ( #∈ω N
            , refl
            , domIs
```

最後の存在節は、状態 `chain N g N` によって証されます。この状態は `C` の添字 `N` に現れ、長さの数項とこの状態の対に `F` を適用すると `code N g` が得られます。存在の主張全体は命題的に切り詰められたままです。

```agda
            , envOver α h
            , chainMem zero (suc-≤-suc zero-≤)
            , step
            , ∣ fst (chain N g N)
              , ( chainMem N ≤-refl , app-graph (num N) (chain N g N) ) ∣₁ ) ∣₁
```

`s` の定義域が `# N` であることを示すため、まず `# N` の添字を取ります。正準な環境はその添字で単に存在する値を与え、`e` に沿ってグラフへの所属を運ぶと、その順序対が `s` に属することが得られます。

```agda
      where
      domIs : DomIs s (nn N)
      domIs x =
          (λ m → PT.map (λ { (yy , p) → yy , subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) (sym e) p })
                   (domAt-in (suc (suc zero)) (suc zero) δ dom0 x m))
```

逆に、`s` が第一成分 `x` の順序対を含むなら、それを正準な環境へ戻します。その環境の既知の定義域から `x ∈ # N` が従い、定義域の特徴づけの両方向がそろいます。

```agda
        , (λ yy p → domAt-out (suc (suc zero)) (suc zero) δ dom0 x yy
                      (subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) e p))
```

集合論的な添字 `i ∈ # N` に数項の除去を使うと、その数項が `i` に等しい自然数 `k < N` が得られます。遷移の証人には、後続の数項、列の実際の第 `k` 項、`k` と `k+1` における畳み込み状態を選びます。

```agda
      step : (i : S) → ⟨ fst i ∈ # N ⟩ → StepAt s C i
      step i i∈N = PT.rec squash₁ (λ { (k , p , ei) →
        ∣ nn (suc k) , fst (ext N g k) , fst (chain N g k) , fst (chain N g (suc k))
        , ( cong sucV (sym ei)
          , subst (λ w → ⟨ pr w (fst (fst (ext N g k))) ∈ fst s ⟩) (sym ei)
```

必要な遷移の事実は、二つの正準な環境と畳み込みの定義式から得られます。列の項は `s` に属し、隣り合う二状態はともに `C` に属し、`app-graph` は項と旧状態の対を `F` が新状態へ送ることを記録します。輸送は `# k` を最初に与えられた添字 `i` へ戻すためだけに使われます。

```agda
              (inS k (fst (ext N g k)) (extMem k p))
          , subst (λ w → ⟨ pr w (fst (fst (chain N g k))) ∈ fst C ⟩) (sym ei)
              (chainMem k (≤-suc p))
          , chainMem (suc k) (suc-≤-suc p)
          , app-graph (ext N g k) (chain N g k) ) ∣₁ }) (∈#-elim N (fst i) i∈N)
```

存在だけでは、まだ `fo` は関数グラフになりません。定理 `only` は、`Wit y s` が認めるどの出力 `y` も、正準な符号と同じ底集合をもつことを示します。この等式は命題なので、命題的に切り詰められた証人を除去してから一意性の議論を進められます。

```agda
    only : (y : S) → Wit y s → fst y ≡ fst (fst (code N g))
    only y = PT.rec (setIsSet (fst y) (fst (fst (code N g))))
      (λ { (n , m , C' , (n∈ω , em , hd , hE , h0 , hS , hF)) →
        Only.final n m C' n∈ω em hd hE h0 hS hF })
      where
```

長さの対象を `n`、その後続を `m`、状態環境を `C'` とする任意の証人を固定します。仮定は、`s` の定義域が `n` であること、`C'` が長さ `m` で `α` に値をとる環境であること、初期項が零であること、`n` より下の各畳み込み段階に従うこと、終状態を `n` と対にすると `y` が得られることを述べます。

```agda
      module Only (n m C' : S) (n∈ω : ⟨ fst n ∈ ω ⟩) (em : fst m ≡ sucV (fst n))
                  (hd : DomIs s n) (hE : EnvC m C')
                  (h0 : ⟨ pr (# zero) (# zero) ∈ fst C' ⟩)
                  (hS : (i : S) → ⟨ fst i ∈ fst n ⟩ → StepAt s C' i)
                  (hF : ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C' ⟩
```

終端節 `hF` は、状態 `v` が単に存在し、それが `C'` の添字 `n` に記録され、`n` とともに `F` で `y` へ写されることを述べます。終状態を大域的に選ぶものではなく、後では出力の一意性を述べる集合の等式へだけ除去します。

```agda
                                     × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁)
                  where
```

証人の長さ `n` は、集合として正準な数項 `# N` に等しくなければなりません。どちらも同じ列 `s` の定義域を表し、`hd` は任意の証人から、`dom0` は選んだ表示 `s = envS α g` からその記述を与えます。外延性により、この等式は所属の二つの含意へ帰着します。

```agda
        n≡ : fst n ≡ # N
        n≡ = cong fst (extensionalL {a = n} {b = nn N} (λ x → ⇔toPath (fwd x) (bwd x)))
          where
          fwd : (x : S) → ⟨ fst x ∈ fst n ⟩ → ⟨ fst x ∈ # N ⟩
          fwd x x∈n = PT.rec (snd (fst x ∈ # N))
```

順方向では、`x ∈ n` と `hd` から、第一成分が `x` である順序対が `s` に単に存在することが得られます。その対を正準な環境へ運び、既知の定義域を読むと `x ∈ # N` が従います。

```agda
            (λ { (yy , p) → domAt-out (suc (suc zero)) (suc zero) δ dom0 x yy
                              (subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) e p) })
            (hd x .fst x∈n)
          bwd : (x : S) → ⟨ fst x ∈ # N ⟩ → ⟨ fst x ∈ fst n ⟩
          bwd x x∈N = PT.rec (snd (fst x ∈ fst n))
```

逆方向では、`x ∈ # N` から正準な環境の項が得られます。それを `s` へ運ぶと、`hd` の逆向きの部分から `x ∈ n` が従います。したがって、各列の表示を選ぶことなく、その定義域から長さを復元できます。

```agda
            (λ { (yy , p) → hd x .snd yy (subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) (sym e) p) })
            (domAt-in (suc (suc zero)) (suc zero) δ dom0 x x∈N)
```

`C'` は環境条件を満たすので単値です。したがって、`C'` に属する二つの順序対の第一成分が同じなら、第二成分の底集合は等しくなります。この事実を用いて、`C'` が記録する任意の状態を、畳み込み方程式が定める状態と比較します。

```agda
        svC : (x v v' : S) → ⟨ pr (fst x) (fst v) ∈ fst C' ⟩ → ⟨ pr (fst x) (fst v') ∈ fst C' ⟩
            → fst v ≡ fst v'
        svC = svAt-out (suc (suc zero)) (α ∷ m ∷ C' ∷ [])
                (envOver-sv (suc (suc zero)) (suc zero) zero (α ∷ m ∷ C' ∷ []) hE)
```

中心となる帰納命題は、各 `k < N + 1` について、`C'` が添字 `k` に記録するどの値も正準な畳み込み状態 `chain N g k` に等しいというものです。`k = 0` では、初期節と `C'` の単値性により、両方の値が零に定まります。

```agda
        entry : (k : ℕ) → k < suc N → (v : S)
              → ⟨ pr (# k) (fst v) ∈ fst C' ⟩ → fst v ≡ fst (fst (chain N g k))
        entry zero    p v hv = svC (nn zero) v (nn zero) hv h0
        entry (suc k) p v hv = PT.rec (setIsSet (fst v) (fst (fst (chain N g (suc k)))))
          (λ { (j , a , u , w , (ej , ha , hu , hw , hFw)) →
```

後続の場合、遷移の証人は列の項 `a`、旧状態 `u`、新状態 `w` を与えます。正準な列の参照によって `a` は第 `k` 入力に等しく、帰納法の仮定によって `u` は正準な旧状態に等しくなります。すると `F` の機能性から、`w` は正準な新状態に等しいと分かります。

```agda
            let ea : fst a ≡ fst (fst (ext N g k))
                ea = s-uniq k p' a (outS k a ha)
                eu : fst u ≡ fst (fst (chain N g k))
                eu = entry k (≤-suc p') u hu
                ew : fst w ≡ fst (fst (chain N g (suc k)))
```

後続添字の境界から `k < N` が得られるので、段階の節を使えます。この節は `w` を `C'` の後続添字に置きます。単値性がまず最初に与えられた値 `v` を `w` と同一視し、先の適用についての議論が `w` を `chain N g (suc k)` と同一視します。

```agda
                ew = app-uniq (ext N g k) (chain N g k) w
                       (subst (λ q → ⟨ pr q (fst w) ∈ fst F ⟩) (cong₂ pr ea eu) hFw)
            in svC (nn (suc k)) v w hv
                 (subst (λ z → ⟨ pr z (fst w) ∈ fst C' ⟩) ej hw) ∙ ew })
          (hS (nn k) (subst (λ z → ⟨ # k ∈ z ⟩) (sym n≡) (#mono k N p')))
```

前者の境界は帰納法に必要な小さな算術事実です。`suc k < suc N` から `k < N` を得ます。これにより、第 `k` 入力が実際の項であり、`k` での畳み込み段階が列の範囲内にあることが保証されます。

```agda
          where
          p' : k < N
          p' = pred-≤-pred p
```

残るのは、与えられた出力 `y` を決定することです。命題的に切り詰められた終端の証人を除去すると、証人の長さ `n` に記録された状態 `v` が得られます。底集合の等式 `n≡ : fst n ≡ # N` でこの所属を添字 `N` へ運ぶと、帰納法の結論が `v` を正準な最終畳み込み状態と同一視します。

```agda
        final : fst y ≡ fst (fst (code N g))
        final = PT.rec (setIsSet (fst y) (fst (fst (code N g))))
          (λ { (v , (hv , hy)) →
            let hv' : ⟨ pr (# N) (fst v) ∈ fst C' ⟩
                hv' = subst (λ z → ⟨ pr z (fst v) ∈ fst C' ⟩) n≡ hv
```

終端節はさらに、`F` が `fst n` と `fst v` からなる対を `y` の底集合 `fst y` へ写すことを述べます。これらの入力を `# N` と正準な最終状態に置き換えると、`F` の機能性から `fst y ≡ fst (fst (code N g))` が得られます。これはグラフ論理式を満たす出力の一意性だけを示し、`α` の任意の要素に対する復号関数を定義するものではありません。

```agda
                ev : fst v ≡ fst (fst (chain N g N))
                ev = entry N ≤-refl v hv'
            in app-uniq (num N) (chain N g N) y
                 (subst (λ q → ⟨ pr q (fst y) ∈ fst F ⟩) (cong₂ pr n≡ ev) hy) })
          hF
```

述語 `Mem s` は、`s` が `seqL α` に属するという意味です。したがって、以後の構成の対象は有限な `α` 値環境グラフに限られ、周囲の宇宙の任意の要素ではありません。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem s = ⟨ fst s ∈ˢ fst (seqL α) ⟩
```

`s` の表示とは、自然数の長さ `n`、割り当て `g : Ix α n`、`s` が `g` の環境グラフに等しいことが、単に存在するという内容です。命題的切り詰めによって、どの表示がデータを与えたかは意図的に忘れられ、長さや割り当てを大域的に選ぶことはありません。

```agda
  Rep : S → Type (ℓ-suc ℓ)
  Rep s = ∥ Σ[ n ∈ ℕ ] Σ[ g ∈ Ix α n ] (fst s ≡ fst (envS α g)) ∥₁
```

`s ∈ seqL α` から、`seqL-out` はまず、`s` が対応する環境集合に属するような有限長が単に存在することを与えます。その環境集合の逆向きの特徴づけから、割り当てと必要なグラフ等式が単に存在することが得られ、`Rep s` が成立します。

```agda
  rep : (s : S) → Mem s → Rep s
  rep s m = PT.rec squash₁
    (λ { (n , hn) → PT.map (λ { (g , e) → n , g , e }) (envSet-out α n s hn) })
    (seqL-out α s m)
```

これでグラフ論理式から `seqL α` 上の関数を得られます。具体的な各表示 `(n,g,e)` から、候補 `fst (code n g)` と、それが `s` 上のグラフのファイバーを一意に占めることの証明が得られます。切り詰められた表示を、この命題的に切り詰められた一意存在の主張へ写せば、`mereFunct` への入力になります。`mereFunct` は優先する表示を選ぶことなく、それを必要な可縮性へ変換します。

```agda
  R : Recursion
  R = record
    { dom   = seqL α
    ; graph = fo
    ; funct = λ s m → mereFunct fo s (PT.map (λ { (n , g , e) →
```

各表示について、`fo-in` は正準な符号がグラフのファイバーに属することを示します。別の `y'` も同じファイバーに属するなら、`fo-out` がその充足証明を証人へ変え、`AtSeq.only` が正準な符号と同一視します。構成可能性の証明は命題なので、底集合の等式から証明つき要素の等式が得られます。

```agda
        fst (code n g)
        , ( fo-in (fst (code n g)) s (AtSeq.wit n g s e)
          , λ y' h → Σ≡Prop (λ v → snd (isL v)) (AtSeq.only n g s e y' (fo-out y' s h)) ) })
        (rep s m)) }
```

定義可能な関数的関係についての一般定理から、一意な値を与える演算が得られます。ここでは関数値と、`fo` を満たすどの出力もその値に等しいという原理を取り出します。内部単射の構成に必要なのはこの二つです。

```agda
  module T = Of R using ( funct; val; val-uniq )
```

列の要素 `s` に対するこの一意な値を `fn s m` と定めます。記法には所属証明 `m` が含まれますが、所属は命題値なので、数学的な値は異なる証明の選び方に依存しません。

```agda
  fn : (s : S) → Mem s → S
  fn = T.val
```

`s` が長さ `n` の割り当て `g` で表示されるなら、`S` の要素としての符号値 `fst (code n g)` は `fo` を満たします。したがってグラフ値の一意性から `fn s m ≡ fst (code n g)` が得られます。この比較は与えられたどの表示についても成り立つので、優先する表示を選ぶ必要はありません。

```agda
  fn-code : (s : S) (m : Mem s) (n : ℕ) (g : Ix α n) → fst s ≡ fst (envS α g)
          → fn s m ≡ fst (code n g)
  fn-code s m n g e = T.val-uniq s m (fst (code n g)) (fo-in (fst (code n g)) s (AtSeq.wit n g s e))
```

`fn` の値は `α` の内部にとどまります。目標となる所属は命題なので、命題的に切り詰められた表示を除去できます。各代表 `(n,g)` については、`code n g` の第二成分が `α` への所属を証し、`fn-code` がその事実を `fn s m` へ運びます。

```agda
  into : (s : S) (m : Mem s) → ⟨ fst (fn s m) ∈ˢ fst α ⟩
  into s m = PT.rec (snd (fst (fn s m) ∈ˢ fst α))
    (λ { (n , g , e) → subst (λ w → ⟨ fst w ∈ˢ fst α ⟩) (sym (fn-code s m n g e)) (snd (code n g)) })
    (rep s m)
```

これらの事実から、`seqL α` から `α` への `DefinableMap` が得られます。このレコードは、ホスト側の関数と、その値が終域に属することの証明を一階論理式 `fo` とともに保持します。`defines` は選ばれた値が論理式を満たすことを示し、`only` は論理式を満たすどの出力もその値であることを示します。続いて単射性を証明すると、`Inj` の構成がこの定義可能性のデータを用いて、`L` の中に実際の関数グラフを作ります。

```agda
  D : DefinableMap
  D = record
    { dom = seqL α ; cod = α ; fn = fn ; into = into ; graph = fo
    ; defines = λ s m → T.funct s m .fst .snd
    ; only    = λ s m y h → sym (T.val-uniq s m y h) }
```

単射性を示すため、二つの列の要素が同じ `fn` の値をもつと仮定します。それぞれの表示は命題的に切り詰められていますが、求める底集合の等式も命題なので、両方の切り詰めを除去して任意の代表 `(n,g)` と `(n',g')` を比較できます。

```agda
  inj : (s : S) (m : Mem s) (s' : S) (m' : Mem s')
      → fst (fn s m) ≡ fst (fn s' m') → fst s ≡ fst s'
  inj s m s' m' e = PT.rec2 (setIsSet (fst s) (fst s'))
    (λ { (n , g , es) (n' , g' , es') →
        es
```

等式 `fn-code` により、二つの `fn` の値の等しさは二つの正準な符号の等しさへ変わります。先に示した `code-inj` から対応する環境グラフの等しさが得られ、二つの表示等式と合成すると `fst s ≡ fst s'` となります。これは正しい符号どうしを比較する証明であり、`α` 全体で定義された復号演算ではありません。

```agda
      ∙ code-inj n g n' g'
          (sym (cong fst (fn-code s m n g es)) ∙ e ∙ cong fst (fn-code s' m' n' g' es'))
      ∙ sym es' })
    (rep s m) (rep s' m')
```

定義可能な写像と先の単射性証明から、`seqL α` から `α` への内部単射が得られます。結論 `InjL` は、適切なグラフが `L` に存在するという命題的に切り詰められた主張です。この写像の全射性も、`α` の任意の要素を有限列として復号できることも主張しません。

```agda
  injL : InjL (seqL α) α
  injL = Inj.injL D inj
```

## 有限列を無限順序数へ単射する

最後の定理では、`α` 上の対の単射があらかじめ与えられているという一時的な仮定を取り除きます。内部単射 `prodL α ↪ α` を構成すると、その命題的に切り詰められたグラフの証人から、畳み込みに必要な単値性、正確な定義域、単射性、値域の事実が得られ、`L` の内部で `seqL α ↪ α` が従います。

```agda
seq-count :
    (α : SL.S) → IsOrd (fst α) → (⟨ fst α ∈ˢ ω ⟩ → Empty.⊥)
  → InjL (seqL α) α
seq-count α oα α∉ω = PT.rec squash₁
  (λ { (F , sv , dm , ij , ran) → Code.injL α oα α∉ω F sv dm ij ran }) pairing
```

対の単射を作るため、`cardOf α oα` が与える基数代表 `μ` を局所的にだけ取ります。この代表は命題的切り詰めのもとで得られますが、目標 `InjL (prodL α) α` も命題なので、大域的な選択をせず任意の代表について構成できます。

```agda
  where
  pairing : InjL (prodL α) α
  pairing = PT.rec squash₁ build (cardOf α oα)
    where
    build : Σ[ μ ∈ S ]
```

代表 `μ` は順序数であり内部の基数でもあり、`α` と `μ` の間には両方向の内部単射があります。`cardOf` は包含 `μ ⊆ α` も与えますが、この構成では使いません。二つの単射は濃度を両方向から比較しますが、`μ` と `α` を定義的に同一視するものではありません。

```agda
              ( IsOrd (fst μ) × IsCardinalL μ
              × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩)
              × InjL α μ × InjL μ α )
          → InjL (prodL α) α
    build (μ , oμ , cardμ , _ , α↪μ , μ↪α) =
```

必要な対の単射は、合成 `α² ↪ μ² ↪ μ ↪ α` です。最初の矢印は `α ↪ μ` を両座標に適用し、中央の矢印は無限な内部基数 `μ` に対する平方律で、最後の矢印が `α` へ戻します。したがって平方律は、任意の無限順序数に直接ではなく、基数代表に適用されます。

```agda
      injl-trans (prodL α) (prodL μ) α (prod-inj α μ α↪μ)
        (injl-trans (prodL μ) μ α
          (WF.WFI.induction regularityV {P = Goal} Step.result (fst μ) (snd μ) oμ cardμ μ∉ω)
          μ↪α)
      where
```

最後に、平方律が必要とする意味で `μ` が無限であることを示します。もし `μ ∈ ω` なら `μ` は有限順序数ですが、与えられた内部単射 `α ↪ μ` は無限順序数 `α` をそこへ単射することになります。`no-fin` は、`α` と `μ` の順序数性および `α` の無限性を用いてこれを排除します。

```agda
      μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
      μ∉ω h = no-fin α μ oα α∉ω oμ h α↪μ
```