充足関係表の Δ₀ 記述

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

外部の意味論的再帰は、すでに一様な充足関係表を構成しています。ここでの問いは、L で解釈される論理式が、候補の集合をその同じグラフとしてどのように認識できるかです。環境の塔、論理式の符号領域、表の二つの領域条件、および十個の再帰的な構成子の節を、後の論理式が量化できる一つの有界な記述にまとめます。

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

この構成は引き続き、レベル ℓ-suc ℓ における排中律を仮定します。この仮定は以下の符号化と充足関係の構成を支えますが、候補の表に新たな性質を付け加えるものではなく、明示的な仮定として保たれます。

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

宇宙レベル ℓ と、この一つの古典的仮定を固定します。構成可能集合から符号化された論理式の鍵まで、記述に使う対象はすべて対応するレベルにあり、結論にこれより強い古典的仮定は入りません。

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

最終的な記述は三つの論理式の連言として作られます。統語上の目標は Δ₀ の証拠、すなわち記述中のすべての量化子が有界であることです。この有界性によって、後で L の内部の充足関係と周囲の階層における充足関係を比較できます。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; _∧̇_ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∧ )
import FOL.Absoluteness

三種類の符号化データが互いに整合しなければなりません。論理式の鍵は正準集合 AllCodes W に属し、アリティ k は環境集合 envSet W k を指し、順序対は鍵とその意味論的な値をまとめます。AllCodes W の要素が論理式の鍵であることは命題的切り詰めのもとでしか得られず、後の復号もこの境界を保ちます。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; AllCodes-out; key∈AllCodes; keyS )

各々の実際の論理式の鍵について、意味論的再帰は充足集合 SatW ψ を作り、関数的な表は対応する値を記録します。有界な記述は、その再帰を内部でもう一度実行するのではありません。十個の局所的な構成子の節を並べ、構造的な議論によって、それらに従う候補の表が各々の実際の鍵で外部に定義された値へ固定されることを示します。

open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table; val-at )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module Match ) public
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SatHoldsC )
open import L.Coding.Quantification {ℓ} using ( f0; down )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )

構成子の節を読むには、まずその定義域を制御する必要があります。候補のコード領域は、実際の論理式の鍵をすべて含み、しかもそのような鍵だけを許さなければなりません。環境の塔は各自然数アリティを、その長さの環境と結び付けます。この二つの記述が、帰納に必要な部分論理式の鍵と環境をちょうど供給します。

open import L.Coding.CodeDomain {ℓ} using ( Tags; codesAt; Δ₀-codesAt )
open import L.Coding.CodeDomainAdequacy {ℓ} lem
  using ( module CodesSound; module CodesComplete; module CodesHolds )
open import L.Coding.EnvironmentTower {ℓ} lem
  using ( towerAt; Δ₀-towerAt; module Tower; module TowerRead; module TowerHolds )

残る対象は、一様な充足関係表のグラフです。その項目は、論理式の鍵と充足集合からなる符号化された対です。十個の有界な節は、第二成分が第一成分に符号化された構成子からどのように決まるかを記述し、実際のグラフがそれらの節の完全性の証人になります。

open import L.Coding.SatisfactionClauses {ℓ} using ( tableAt; Δ₀-tableAt )
open import L.Coding.SatisfactionClauseSemantics {ℓ} lem using ( module Frame; module Bridge )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )

解釈環境は構成可能集合の有限ベクトルであり、その添字が表、作業集合、コード領域、塔、数項タグを指定します。依存対は各読みが返す証人を表します。その証人が命題的切り詰めのもとにある場合、別の命題を証明するためにだけ使うことができ、大域的に選ばれたデータにはできません。

open import Cubical.Data.Vec using ( lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isPropΣ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )

自然数アリティは、累積階層の内部で数項 # k として表されます。したがって環境の塔の項目は、# k と envSet W k の順序対として符号化されます。等しさは常に階層の底の集合の間で述べられ、符号化定理もこのレベルで働きます。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )

構成可能構造の台を S と書きます。S の要素は、階層の底の集合と、その構成可能性の証拠からなります。表の読みが比較するのは底の集合であり、付随する構成可能性の証拠の等しさは主張しません。

open hPropStructure 𝒮ʟ using ( S )

この章の論理式は L の内部で解釈され、有限環境は S に値を取ります。論理式の有界性によって後で周囲の階層と比較できますが、ここでの健全性の議論はまず、この内部の充足関係だけを用いて進みます。

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

有界な記述の健全性

健全性のために、候補集合 T、C、E、作業集合 W、十個の数項タグ、そしてそれらを読む環境を固定します。塔、コード領域、表の記述が成り立つことを個別に仮定し、作業集合のスロットだけを W と整合させます。三つの記述の仮定のどれも、残りの二つからは従いません。

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

候補の表、コード領域、環境の塔が表す底の集合を、それぞれ Tv、Cv、Ev と書きます。節の意味論は、これらの集合についての有界論理式を、構造的な議論に必要な周囲の所属と等しさへ結ぶ橋を与えます。

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

Ev の項目が、すでに n と F の符号化された対として表されているとします。塔を読むと、命題的切り詰めのもとでアリティ k と等式 n = # k が得られます。同時に得られる F = envSet W k を忘れると、候補の論理式の鍵を解析するためにちょうど必要なアリティの事実になります。逆向きの塔の読みは各々の実際のアリティの項目を Ev に入れるので、実際の鍵を Cv に入れることもできます。

    module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
    arity : (n F : S) → ⟨ pr (fst n) (fst F) ∈ Ev ⟩ → ∥ Σ[ k ∈ ℕ ] (fst n ≡ # k) ∥₁
    arity n F q∈ = PT.map (λ { (k , (qk , _)) → k , qk }) (TR.entry-out n F q∈)
    module CS = CodesSound C w E N γ W qw tg arity (hC .fst)
    module CC = CodesComplete C w E N γ W qw tg TR.entry-in (hC .snd)

仮定 hT は、全域性、領域条件、十個の構成子の節からなり、Frame はそれらの意味論的な読みを与えます。SatSoundC の固定の議論は、全域性と十個の節を、環境の塔に関する事実および候補の符号領域の閉性に組み合わせます。固定すべき表の要素は、すでに実際の論理式の鍵における対として与えられているため、この段階で領域条件は必要ありません。その条件は、後で任意の提示された表の対を読むときに使われます。

    module Fr = Frame T w C E N γ tg
    module SC = SatSoundC T w C E N γ W qw tg hE CS.closed hT

二つの領域条件は互いを補う形をしています。全域性は、Cv の各 c に対し、pr c y が Tv に属するような y が存在することを、命題的切り詰めのもとで与えます。領域条件は Tv の任意の要素 e から始め、再び命題的切り詰めのもとで、e を pr c y と分解し、c が Cv に属することを与えます。どちらも値や対の成分を大域的に選ばず、またどちら一方だけで表が一価の関係になるわけでもありません。

    hTot = hT .fst
    hOn = hT .snd .fst

コード領域の完全性によって論理式 a の実際の鍵を Cv に入れ、その鍵に全域性を適用します。結論は、ある値とその鍵との対が Tv に属することを単に述べ、証人は命題的切り詰めのもとに残ります。選ばれた値も復号関数も得られず、後では命題への消去にだけ使われます。

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

固定の述語は次を言います。値 y と ψ のキーの対が候補の表に属するならば、y の底の集合は ψ の再帰的な充足集合の底の集合と等しくなる。固定されるのは底の集合だけです。y の構成可能性の証明も、論理式そのものも、これでは固定されません。

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

証明は ψ の構造再帰によって進みます。Cv の閉性が直接の部分論理式の鍵を与え、全域性がその鍵での表の値を命題的切り詰めのもとでのみ与えます。再帰的な仮定はそれらの子の値を固定し、対応する構成子の節は意味論的再帰と同じ外延条件を与えます。そのため、外延性によって親の値が固定されます。CC.key-in ψ は、ψ の鍵でこの議論を始めるために必要な、候補の符号領域への所属を与えます。

  pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ
  pinned ψ = SC.pinned ψ (CC.key-in ψ)

候補のコード領域の各要素は正準なコード集合に属します。候補の鍵の読みからアリティ、論理式、鍵の等式が得られるのは、命題的切り詰めのもとだけです。目標である正準集合への所属は命題なので、そこへ証人を消去し、その等式に沿って所属を運べます。この議論は論理式を選びません。

  C-out : (c : S) → ⟨ fst c ∈ Cv ⟩ → ⟨ fst c ∈ fst (AllCodes W) ⟩
  C-out c c∈ = PT.rec (snd (fst c ∈ fst (AllCodes W)))
    (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ fst (AllCodes W) ⟩) (sym e) (key∈AllCodes W ψ) })
    (CS.key-out c c∈)

逆に、正準なコード集合の各要素は Cv に属します。正準集合への所属は、命題的切り詰めのもとで論理式の鍵としての表示を与え、コード領域の完全性がその鍵を候補領域に入れます。ここでも証人は所属を証明するためだけに使われ、復号器の定義には使われません。

  C-in : (c : S) → ⟨ fst c ∈ fst (AllCodes W) ⟩ → ⟨ fst c ∈ Cv ⟩
  C-in c c∈ = PT.rec (snd (fst c ∈ Cv))
    (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ Cv ⟩) (sym e) (CC.key-in ψ) })
    (AllCodes-out W c c∈)

塔の外向きの読みが扱うのは、すでに pr n F として表された項目です。命題的切り詰めのもとで自然数 k が得られ、n = # k かつ F = envSet W k となります。k を大域的に選ぶことも、この補題だけで Ev の任意の要素に符号化された対としての表示を与えることもありません。

  E-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ Ev ⟩
        → ∥ Σ[ k ∈ ℕ ] ((fst n ≡ # k) × (fst F ≡ fst (envSet W k))) ∥₁
  E-out = TR.entry-out

塔の内向きの読みは、命題的切り詰めを伴わずに補完的な事実を与えます。与えられた各自然数 k について、標準的な項目 pr (# k) (envSet W k) は Ev に属します。前の読みと合わせて標準的な符号化項目を双方向に制御しますが、塔の任意の要素ごとにアリティを選ぶとは主張しません。

  E-in : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩
  E-in = TR.entry-in

表の読みは、健全性の方向の中心です。それは、x と y の順序対としてすでに提示された要素に対してだけ述べられます。候補の表の任意の要素は、この補題の範囲ではありません。

  T-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ Tv ⟩
        → Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst y ≡ fst (Table.val W W x mx))
  T-out x y h = PT.rec (isPropΣ (snd (fst x ∈ fst (AllCodes W))) (λ mx → setIsSet _ _))
    (λ { (c , yc , (ee , c∈)) → PT.rec (isPropΣ (snd (fst x ∈ fst (AllCodes W))) (λ mx → setIsSet _ _))
      (λ { (k , ψ , e) →

対の等式は両辺の第一成分に分解され、コードの等式が、記録されたキーを、復号されたある論理式のキーと同一視します。その論理式のキーが正準なコード集合に属することは、輸送によって従います。

        let q = pr-inj ee
            qx : fst x ≡ fst (keyS W ψ)
            qx = q .fst ∙ e
            mx : ⟨ fst x ∈ fst (AllCodes W) ⟩
            mx = subst (λ u → ⟨ u ∈ fst (AllCodes W) ⟩) (sym qx) (key∈AllCodes W ψ)

固定によって記録された値を再帰的な充足集合と同一視し、val-at によってその集合を同じ鍵における関数的な表の値と同一視します。結論は、正準なコード集合への所属と底の集合の等しさからなります。結論自体は命題的切り詰められていませんが、依存対全体が命題なので、命題的切り詰められた復号から得られます。これは計算的な復号ではありません。

        in mx , ( pinned ψ y (subst (λ u → ⟨ u ∈ Tv ⟩) (cong (λ a → pr a (fst y)) qx) h)
                ∙ sym (cong fst (val-at W W ψ x mx qx)) ) })
      (CS.key-out c c∈) })
    (Fr.onC-out hOn (down (lookup T γ) (pr (fst x) (fst y)) h) h)

表の逆向きの読みでは、指定された正準コード x から始めます。AllCodes W への所属により、命題的切り詰めのもとで、鍵が x である論理式 ψ が得られます。次に全域性から、再び命題的切り詰めのもとで、その論理式の鍵に記録された候補の値が得られます。

  T-in : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ pr (fst x) (fst (Table.val W W x mx)) ∈ Tv ⟩
  T-in x mx = PT.rec (snd (pr (fst x) (fst (Table.val W W x mx)) ∈ Tv))
    (λ { (k , ψ , e) → PT.rec (snd (pr (fst x) (fst (Table.val W W x mx)) ∈ Tv))
      (λ { (y , my) →
        subst (λ u → ⟨ u ∈ Tv ⟩)

候補の値は、再帰的な充足の集合に固定され、値の補題がそれを関数的な表の値と整列させます。そして所属が、順序対の等式に沿って運ばれます。どちらの消去も、命題である表の所属に着地します。

          (cong₂ pr (sym e) (pinned ψ y my ∙ sym (cong fst (val-at W W ψ x mx e))))
          my })
      (sub ψ) })
    (AllCodes-out W x mx)

完全性と二つの読み方

完全性は任意の候補ではなく、具体的な意味論的対象から始めます。環境の四つのスロットは、それぞれ W、実際のグラフ SatGraph.pairs W、正準なコード集合 AllCodes W、実際の塔 Tower.tower W と整合し、十個のタグも固定されます。これらの整合は仮定であり、有界な節から得られる結論ではありません。

module SatHolds {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qT : fst (lookup T γ) ≡ fst (SatGraph.pairs W))
  (qC : fst (lookup C γ) ≡ fst (AllCodes W)) (qE : fst (lookup E γ) ≡ fst (Tower.tower W))
  (tg : Tags γ N) where
  open Alphabet W

表と符号領域のスロットにある基礎集合を Tv と Cv と書きます。同定 qT と qC は、それらの所属事実をそれぞれ実際のグラフと正準な符号集合へ運びます。したがって、すでに対の形で提示された表の要素はグラフの読みによって扱えますが、符号の復号は命題的切り詰めのもとでのみ得られます。以下の等式はすべて、引き続き階層の基礎集合を比較します。

  open Bridge W
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)

論理式のキーと同一視された符号のもとでの表の値は、その論理式の再帰的な充足の集合と等しくなります。証明は、本物の充足のグラフから対を読み出し、提示されたキーと論理式のキーの同一視に沿って第二成分を運び、値の補題で締めくくります。

    val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ)
         → ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ → fst yc ≡ fst (SatW ψ)
    val≡ ψ c yc qc h =
      let p = SatGraph.pairs-out W c yc (subst (λ u → ⟨ pr (fst c) (fst yc) ∈ u ⟩) qT h)
      in p .snd ∙ cong fst (SatGraph.valOf≡ W c (p .fst)) ∙ cong fst (val-at W W ψ c (p .fst) qc)

コード領域の要素が pr (# n) z として表されているなら、それを AllCodes W へ運ぶことで、命題的切り詰めのもとで復号できます。すなわち、ペイロードが z である論理式 ψ : Formula Ab n が存在します。論理式は選ばれず、復号の一意性も得られないので、復号関数は定義されません。

    decode : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z
           → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
    decode c c∈ = Match.decodeAll W c (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈)

候補コード c は、正準なコード集合との整合によって、実際のグラフへの正しい入力になります。そのグラフの値から表の項目を得て、Tv と SatGraph.pairs W の整合に沿って運び戻します。得られる存在の主張は、全域性の節が要求する通り、命題的切り詰めのもとに残ります。

    tot : (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
    tot c c∈ =
      let mx = subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈
      in ∣ SatGraph.valOf W c mx , subst (λ u → ⟨ pr (fst c) (fst (SatGraph.valOf W c mx)) ∈ u ⟩) (sym qT) (SatGraph.pairs-in W c mx) ∣₁

実際のグラフは、任意の表の要素に必要な形も与えます。命題的切り詰めのもとで、その各要素は、あるコードとそのグラフの値からなる符号化された対であり、そのコードは Cv に属します。これは存在だけを述べる分解であり、各要素の成分を選ぶものではありません。

    onc : (e : S) → ⟨ fst e ∈ Tv ⟩
        → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
    onc e e∈ = PT.map
      (λ { (x , mx , ee) → x , SatGraph.valOf W x mx , (ee , subst (λ u → ⟨ fst x ∈ u ⟩) (sym qC) mx) })
      (SatGraph.pairs-shape W e (subst (λ u → ⟨ fst e ∈ u ⟩) qT e∈))

SatHoldsC.holds への入力は異なる役割を担います。実際の環境の塔が環境の行を与え、val≡ が実際の論理式の鍵での値を同定し、decode が形の定まった符号から論理式を命題的切り詰めのもとでのみ復号し、tot と onc が二つの領域条件を示します。構造的な議論は、続いて十個の構成子の節をすべて検証します。命題的に切り詰められたアリティ、論理式、分解を使うときは、対応する節が満たされるという命題にのみその証人を消去します。復号器や表の値の選択がその外へ出ることはありません。

  holds : ⟨ γ ⊨ tableAt T w C E N ⟩
  holds = SatHoldsC.holds W T w C E N γ qw tg
    (TowerHolds.holds E w (N f0) γ W qw qE (tg f0)) val≡ decode tot onc

封じられた論理式 satAt は、towerAt、codesAt、tableAt という三つの独立な記述をまとめます。塔の成分にはタグのスロット N f0 が渡され、Tags はそれを数項ゼロと同定します。符号領域と表の成分には、十個のスロットからなる族 N 全体が渡されます。この連言自体は、候補の対象と正準な環境の塔、符号集合、または充足関係グラフとの等しさを加えるものではありません。

opaque
  satAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
  satAt T w C E N = towerAt E w (N f0) ∧̇ (codesAt C w E N ∧̇ tableAt T w C E N)

後の議論では、satAt の三つの成分を繰り返し展開することなく、これを一つの有界述語として扱えます。Lévy 階層への所属などの統語的性質を確かめるときには、定義を限定された範囲で展開します。意味論的に使うときは、以下の射影と完全性の結果を通して扱います。不透明性はこの証明の境界を示すだけであり、モデル理論的な性質を加えるものではありません。

opaque
  unfolding satAt

証明 Δ₀-satAt は、有界部分が連言について閉じていることを使い、三つの成分の証明を組み合わせます。ここで得られるのは satAt の統語的な有界性だけであり、どの集合がこの論理式を満たすかはまだ述べません。意味論的な二つの方向は、後で SatRead と sat-complete が与えます。

  Δ₀-satAt : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) → Δ₀ (satAt T w C E N)
  Δ₀-satAt T w C E N = δ-∧ (Δ₀-towerAt E w (N f0)) (δ-∧ (Δ₀-codesAt C w E N) (Δ₀-tableAt T w C E N))

satAt の証明から、健全性に必要な三つの正確な仮定、すなわち環境の塔、コード領域、表の記述を取り出せます。この射影は意味論的な結論を加えず、候補の対象と正準な対象との等しさも与えません。

  satAt-out : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
            → ⟨ γ ⊨ satAt T w C E N ⟩
            → ⟨ γ ⊨ towerAt E w (N f0) ⟩ × (⟨ γ ⊨ codesAt C w E N ⟩ × ⟨ γ ⊨ tableAt T w C E N ⟩)
  satAt-out T w C E N γ h = h

逆に、三つの記述の証明を組み合わせれば satAt が得られます。この構成は連言そのものであり、各成分を個別に与える必要があります。表の節によって、欠けた塔やコード領域の節を補うことはできません。

  satAt-in : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
           → ⟨ γ ⊨ towerAt E w (N f0) ⟩ → ⟨ γ ⊨ codesAt C w E N ⟩ → ⟨ γ ⊨ tableAt T w C E N ⟩
           → ⟨ γ ⊨ satAt T w C E N ⟩
  satAt-in T w C E N γ hE hC hT = hE , (hC , hT)

SatRead は、satAt を満たす候補に対する健全性側の接続口です。作業集合のスロットが W と同定され、Tags が数項のスロットを整合させた後にのみ適用でき、上で証明した六つの正確な外向きと内向きの規則を公開します。それぞれの結論の形はそのまま保たれます。この接続口は、それらを候補集合と正準集合との一括した等しさに置き換えず、選ばれた復号結果や証人も取り出しません。

module SatRead {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (h : ⟨ γ ⊨ satAt T w C E N ⟩) where
  private
    module SS = SatSound T w C E N γ W qw tg
      (satAt-out T w C E N γ h .fst) (satAt-out T w C E N γ h .snd .fst) (satAt-out T w C E N γ h .snd .snd)

コードについては、二方向の読みが AllCodes W への所属を比較します。塔の項目については、標準的な対 pr (# k) (envSet W k) を読んだり挿入したりします。表の項目については、提示された対を正準コードにおける関数的な表の値と比較します。この三種類の結論を区別しておくことで、根拠のない強い一意性の主張を避けられます。

  open SS public using ( C-out; C-in; E-out; E-in; T-out; T-in )

逆向きの定理は、四つのスロットがすでに意図された対象、すなわち W、その充足関係のグラフ、完全なコード集合、環境の塔を表していると仮定します。さらに、正しい十個の数項タグも仮定します。これらの整合は完全性への入力であり、satAt から復元されるものではありません。

sat-complete : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
             → fst (lookup w γ) ≡ fst W
             → fst (lookup T γ) ≡ fst (SatGraph.pairs W)
             → fst (lookup C γ) ≡ fst (AllCodes W)
             → fst (lookup E γ) ≡ fst (Tower.tower W)

結論は、すでに整合された環境が satAt を満たすことの証明です。証明はまず、qw、qE、qC、整合されたタグを用いて、環境の塔と符号領域の成分を満たします。これらの同定は全体を通じて仮定のままです。この段階は、新しい塔、符号集合、グラフの存在証人を導入せず、satAt を満たす四つ組がすべて一意に正準であるとも主張しません。

             → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
sat-complete T w C E N γ W qw qT qC qE tg =
  satAt-in T w C E N γ
    (TowerHolds.holds E w (N f0) γ W qw qE (tg f0))
    (CodesHolds.holds C w E N γ W qw qC qE tg)

最後の行は SatHolds.holds を再利用して、表の連言項を与えます。上で証明したように、これが示すのは十個の節だけではなく、二つの領域条件と十個の構成子の節を含む tableAt 全体です。satAt-in がその結果を環境の塔と符号領域の連言項に組み合わせます。したがって sat-complete は、すでに整合された正準なデータを有界な記述に書き込む向きです。表の証明内部で用いる命題的に切り詰められた復号から、大域的な復号器や選ばれた値が外に取り出されることはありません。

    (SatHolds.holds T w C E N γ W qw qT qC qE tg)