構成可能階層の Δ₀ 記述

module PinsRead {m : ℕ} (N : Fin  → Fin m) (γ : Vec S m) where

タグの節の読みは、まず最初の枠が空であることを示す。要素をもたないのである。

pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N
pins-out (h0 , hs) = go
  where
  q0 : (lookup (N f0) γ) .fst ≡ # 
  q0 = extensionalV (λ y → ⇔toPath

空であることは、両方向の外延性の議論である。最初の枠のどんな要素も偽の節と矛盾し、そもそも空集合には要素がない。

    (λ y∈ → ⊥*-rec (h0 (down (lookup (N f0) γ) y y∈) y∈))
    (λ y∈ → ⊥₀-rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))))

補助補題 up は数項の鎖を一つ進める。スロット i が # k を表し、sucAtL i j が成り立つなら、その健全な読みはスロット j を sucV (# k)、したがって数項 # (suc k) と同定する。

  up : (i j : Fin m) (k : ℕ) → ⟨ γ ⊨ sucAtL i j ⟩ → (lookup i γ) .fst ≡ # k
     → (lookup j γ) .fst ≡ # (suc k)
  up i j k h q = suc-out i j γ h ∙ cong sucV q

零についての等式から始め、最初の五つの後続の節によって q1 から q5 が順に得られる。したがって f1 から f5 が名付けるスロットは、それぞれ数項一から五と同定される。

  q1 = up (N f0) (N f1)  (hs .fst) q0
  q2 = up (N f1) (N f2)  (hs .snd .fst) q1
  q3 = up (N f2) (N f3)  (hs .snd .snd .fst) q2
  q4 = up (N f3) (N f4)  (hs .snd .snd .snd .fst) q3
  q5 = up (N f4) (N f5)  (hs .snd .snd .snd .snd .fst) q4

残り四つの後続の節が同じ鎖を続け、q6 から q9 を与える。これにより、スロット f6 から f9 は数項六から九と同定され、数項についての読みが完成する。

  q6 = up (N f5) (N f6)  (hs .snd .snd .snd .snd .snd .fst) q5
  q7 = up (N f6) (N f7)  (hs .snd .snd .snd .snd .snd .snd .fst) q6
  q8 = up (N f7) (N f8)  (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7
  q9 = up (N f8) (N f9)  (hs .snd .snd .snd .snd .snd .snd .snd .snd) q8

記録 Tags γ N は、Fin 10 の各要素について対応する数項の等式を要求する。最初の四つの場合は q0、q1、q2、q3 を返し、零から三までのタグに対応する。

  go : Tags γ N
  go zero = q0
  go (suc zero) = q1
  go (suc (suc zero)) = q2
  go (suc (suc (suc zero))) = q3

go の次の五つの場合は q4 から q8 を返す。入れ子の後続として書かれたこれらのパターンは、追加の算術的な議論なしに、タグ四から八を尽くす。

  go (suc (suc (suc (suc zero)))) = q4
  go (suc (suc (suc (suc (suc zero))))) = q5
  go (suc (suc (suc (suc (suc (suc zero)))))) = q6
  go (suc (suc (suc (suc (suc (suc (suc zero))))))) = q7
  go (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = q8

Fin 10 に残る唯一の場合は、零の九回目の後続であり、q9 を返す。これで場合分けは、Tags γ N が要求する十個すべての数項の等式を与える。

  go (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = q9

逆向きには、スロットがすでに Tags γ N を満たすとする。零のスロットの要素と仮定されたものは、タグの等式に沿って空集合の要素へ移されるため、存在できない。同じタグの等式が、九つの後続の節を埋めるためのデータも与える。

pins-in : Tags γ N → ⟨ γ ⊨ pins N ⟩
pins-in tg =
    (λ x x∈ → ⊥₀-rec (∅-empty (x .fst) (∈∈ₛ {a = x .fst} {b = ∅} .fst
                (subst (λ u → ⟨ x .fst ∈ u ⟩) (tg f0) x∈))))
  , ( st f0 f1 refl , ( st f1 f2 refl , ( st f2 f3 refl , ( st f3 f4 refl , ( st f4 f5 refl , ( st f5 f6 refl

各後続の節は、二つのタグのスロットを対応する数項の等式に沿って書き換えた後、後続論理式の内向きの読みを適用して再構成する。

  , ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl ))))))))
  where
  st : (j k : Fin ) → # (toℕ k) ≡ sucV (# (toℕ j)) → ⟨ γ ⊨ sucAtL (N j) (N k) ⟩
  st j k e = suc-in (N j) (N k) γ (tg k ∙ e ∙ cong sucV (sym (tg j)))

module DefInRead {k : ℕ} (w z : Fin k) (N : Fin  → Fin k) (body : Formula S ( + k))
  (δ : Vec S k) (tg : Tags δ N) where

private
  Wv = (lookup w δ) .fst
  Zv = (lookup z δ) .fst

四つの証人は T、C、E、d の順に束縛される。新しい束縛子は環境の先頭を拡張するため、本体は d ∷ E ∷ C ∷ T ∷ δ で評価される。したがって先頭の四つのスロットは、定義可能冪集合の値、環境の塔、符号集合、充足関係表をこの順に指す。

δ4 : (T C E d : S) → Vec S ( + k)
δ4 T C E d = d ∷ E ∷ C ∷ T ∷ δ

defIn を読むとき、四つの証人 T、C、E、d を囲む命題的切り詰めは保たれる。その結論が意図的に残すのは、d ∈ z、d = 𝒟ₒ Wv、そして拡張された環境で本体が成り立つことだけである。T、C、E が z に属する証明と、内部の充足および冪集合の記述の証明は、この弱い主張を導く途中で消費される。

defIn-out : ⟨ δ ⊨ defIn w z N body ⟩
          → ∥ Σ[ T ∶ S ] Σ[ C ∶ S ] Σ[ E ∶ S ] Σ[ d ∶ S ]
              (⟨ d .fst ∈ Zv ⟩ × ((d .fst ≡ 𝒟ₒ Wv) × ⟨ δ4 T C E d ⊨ body ⟩)) ∥₁
defIn-out = rec₁ squash₁ (λ { (T , (T∈ , h1)) → rec₁ squash₁ (λ { (C , (C∈ , h2)) →
  rec₁ squash₁ (λ { (E , (E∈ , h3)) → map₁ (λ { (d , (d∈ , (hs , (hd , hb)))) →

四重の切り詰めから証人を取り出した後、def-sound は充足の記述 hs と定義可能冪集合の記述 hd を組み合わせる。ここに残される唯一の等式は、その結論 d = 𝒟ₒ Wv であり、本体の証明はそのまま先へ渡される。

    T , C , E , d , ( d∈ , ( def-sound i0 (sh  w) i3 i2 i1 (shN  N) (δ4 T C E d) (lookup w δ) refl tg hs hd
                           , hb )) })
    h3 }) h2 }) h1 })

逆に、意味論的なデータから defIn を示すには、真正な証人を明示的に与える必要がある。w で表される構成可能な台 W、四つの集合とそれらが z に属する証明、真正な充足関係表、符号集合、環境の塔、定義可能冪集合とのそれぞれの同定、そして本体の証明を与える。したがってこの向きでは、外向きの読みが意図的に忘れるデータを仮定する。

defIn-in : (W : S) → Wv ≡ W .fst → (T C E d : S)
         → ⟨ T .fst ∈ Zv ⟩ → ⟨ C .fst ∈ Zv ⟩ → ⟨ E .fst ∈ Zv ⟩ → ⟨ d .fst ∈ Zv ⟩
         → T .fst ≡ (SatGraph.pairs W) .fst → C .fst ≡ (AllCodes W) .fst → E .fst ≡ (Tower.tower W) .fst
         → d .fst ≡ 𝒟ₒ (W .fst) → ⟨ δ4 T C E d ⊨ body ⟩ → ⟨ δ ⊨ defIn w z N body ⟩
defIn-in W qw T C E d T∈ C∈ E∈ d∈ qT qC qE qd hb =

内向きの読みでは、まず sat-complete が、真正な充足関係表、符号集合、環境の塔が satAt を満たすことを示す。次に def-complete が、その証明と与えられた d の等式を使って、定義可能冪集合の節を示す。与えられた本体の証明で連言が完成し、その後、四つの証人とそれぞれの所属証明が、入れ子の命題的切り詰めの中へ順に導入される。

  ∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs
    , ( def-complete i0 (sh  w) i3 i2 i1 (shN  N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁
  where
  hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh  w) i2 i1 (shN  N) ⟩
  hs = sat-complete i3 (sh  w) i2 i1 (shN  N) (δ4 T C E d) W qw qT qC qE tg

module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (tg : Tags γ N) where

private
  Vv = (lookup v γ) .fst
  Bv = (lookup b γ) .fst
  Fv = (lookup f γ) .fst

共通の上界の底集合を Zv と書く。これは、補助的な充足関係、符号、環境の塔、定義可能冪集合の証人をどこで見つけられるかを制御する。一段階から得たい等式には Zv は現れない。この上界は記述を可能にするが、得られる段階の値の一部にはならない。

  Zv = (lookup z γ) .fst

内向きの本体では、d は defIn が認識する定義可能冪集合であり、x は外側の v 上の有界全称量化子が導入した要素である。原子論理式の本体は x ∈ d を述べる。記録された値 w を Lset c と同定すれば、これはある c ∈ b に対する 𝒟ₒ (Lset c) への所属になる。

  intoBody : Formula S ( + m)
  intoBody = defIn i0 (sh  z) (shN  N) (var i8 ∈̇ var i0)

over の本体は定義可能冪集合の記述であり、その内側の論理式は、記述された集合のすべての要素が候補となる次の値に属することを述べる。これは合併の等式に必要な逆向きの包含を与える。

  overBody : Formula S ( + m)
  overBody = defIn i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v)))

一段階の読み補題は、Bv より下の各対の行が正しい値をもつこと (Values) と、Bv より下の各添字に正準な行があること (Entries) を別々に仮定する。ちょうどこの二つの仮定のもとで、stepAt の二つの部分が反対向きの所属の含意を与え、外延性から Vv = Lset Bv が得られる。これらの仮定が制約するのは関係する対の行だけであり、候補表の無関係な要素を排除するものではない。

step-out : ⟨ γ ⊨ stepAt v b f z N ⟩ → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → Vv ≡ Lset Bv
step-out (hi , ho) vals ents = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
  where
  fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ Lset Bv ⟩
  fwd x x∈ = rec₁ ((x ∈ Lset Bv) .snd) (λ { (c , (c∈ , h1)) → rec₁ ((x ∈ Lset Bv) .snd)

前向きの包含では、intoAt が段階の添字 c ∈ Bv、表の対の行 (c,w)、そして x を含む定義可能冪集合の値 d を与える。仮定 Values は w を Lset c と同定するので、d = 𝒟ₒ (Lset c) である。段階への内向きの規則 Lset-in が、この寄与から x を Lset Bv へ運ぶ。

    (λ { (q , (q∈ , h2)) → rec₁ ((x ∈ Lset Bv) .snd) (λ { (w , s , (eq , h3)) →
      rec₁ ((x ∈ Lset Bv) .snd) (λ { (T , C , E , d , (d∈ , (qd , hx))) →
        Lset-in Bv (c .fst) x c∈
          (subst (λ u → ⟨ x ∈ u ⟩)
            (qd ∙ cong 𝒟ₒ (vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) eq q∈))) hx) })

入れ子の存在形を読む各段階で、命題的切り詰めは保たれる。まず sndEx-out が、対の形をした表の項目から第二成分 w が単に存在することを復元し、次に defIn-out が、補助データと、d を w の定義可能冪集合と同定する等式が単に存在することを復元する。各切り詰めは、所属命題 x ∈ Lset Bv へ直接除去される。

      (DefInRead.defIn-out i0 (sh  z) (shN  N) (var i8 ∈̇ var i0) (w ∷ s ∷ q ∷ c ∷ xS ∷ γ) tg h3) })
      (sndEx-out i0 i1 intoBody (q ∷ c ∷ xS ∷ γ) h2) })
    h1 })
    (hi xS x∈)
    where

証明は周囲の要素 x ∈ Vv から始まるが、論理式は構成可能な台 S の上で解釈される。演算 down はこの所属証明を使って x を台の要素 xS として提示する。xS を環境の先頭に置くと、新しく束縛されたスロットは同じ底集合 x を表す。

    xS : S
    xS = down (lookup v γ) x x∈

step-out の逆向きの包含は、実際の段階 Lset Bv の要素を候補の値 Vv に入れる。これは Lset Bv の切り詰められた段階分解を消去し、x がその定義可能冪集合に属するような、より前の段階 δ についての主張へ帰着させる。

  bwd : (x : V ℓ) → ⟨ x ∈ Lset Bv ⟩ → ⟨ x ∈ Vv ⟩
  bwd x x∈ = rec₁ ((x ∈ Vv) .snd) put (Lset-out Bv x x∈)
    where
    put : Σ[ δ ∶ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ Vv ⟩
    put (δ , (δ∈ , xD)) = rec₁ ((x ∈ Vv) .snd)

Lset-out がより前の添字 δ を示すと、完全性が正準な表の項目 (δ, Lset δ) を与える。over の節をこの項目に適用し、さらに defIn-out がそこで有界化された集合 d を 𝒟ₒ (Lset δ) と同一視する。したがって、その全称な本体は与えられた x を候補の値 Vv に入れる。この向きで使うのは Entries が与える正準な項目であり、Values への別の訴えは要らない。

      (λ { (T , C , E , d , (d∈ , (qd , hsub))) →
        hsub (down d x (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD)) (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD) })
      (DefInRead.defIn-out i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v)))
        (w ∷ container q c w refl .fst ∷ q ∷ c ∷ γ) tg
        (useSnd i0 (q ∷ c ∷ γ) c w refl overBody i1 refl (ho c δ∈ q (ents c δ∈))))

名づけられる二つの対象は、符号化された引数と符号化された対である。どちらも、所属の証明を下降して台の要素として提示される。

      where
      c : S
      c = down (lookup b γ) δ δ∈
      q : S
      q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)

行の値 w は、対の提示から読まれ、本体の充足が消費する成分である。

      w : S
      w = sndS q δ (Lset δ) refl

ステップの条項の内向きの方向には、五つの仮定が要る。界の順序数性、提案された値と界での段階の同定、界での表の正しさと完備さ、そして界の各要素のための補助の証人を証人の界の中に置く供給関数である。証明は二つの連言項に分かれる。

step-in : (ob : IsOrd Bv) → Vv ≡ Lset Bv → Values (lookup f γ) Bv → Entries (lookup f γ) Bv
        → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
        → ⟨ γ ⊨ stepAt v b f z N ⟩
step-in ob vq vals ents sup = into , over
  where

into の連言項は、提案された値の要素 x から外向きに読まれる。界での段階の切り詰められた分解が、より前の順序数と定義可能冪集合への所属を名指し、存在の導入がそれを二つの有界量化子に満たす。

  into : ⟨ γ ⊨ intoAt v b f z N ⟩
  into x x∈ = rec₁ squash₁ put (Lset-out Bv (x .fst) (subst (λ u → ⟨ x .fst ∈ u ⟩) vq x∈))
    where
    put : Σ[ δ ∶ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x .fst ∈ 𝒟ₒ (Lset δ) ⟩)
        → ⟨ (x ∷ γ) ⊨ ∃̇∈ (var (sh  b)) (∃̇∈ (var (sh  f)) (sndEx i0 i1 intoBody)) ⟩

入れ子になった有界存在量化子は、命題的切り詰めからデータを取り出すことなく満たされる。証明は δ を台の要素 c として提示し、Entries によって正準な対を q として提示し、fillSnd で対の分解を与える。残る本体が hb である。充足は命題なので、各構成子は ∃[]-syntax に組み込まれた命題的切り詰めを保つ。

    put (δ , (δ∈ , xD)) =
      ∣ c , ( δ∈ , ∣ q , ( ents c δ∈ , fillSnd i0 (q ∷ c ∷ x ∷ γ) c w refl intoBody hb i1 refl ) ∣₁ ) ∣₁
      where
      oδ : IsOrd δ
      oδ = mem-ord {A = Bv} ob δ δ∈

三つの台の要素は、それぞれ異なる根拠から得られる。所属 δ ∈ Bv はより前の添字を c として提示し、正準な対が表に属するという証明はその対を q として提示し、δ の順序数性によって LsetS は段階 Lset δ を w として提示できる。有界な証人を組み立てる際には、これらの由来を区別することが大切である。

      c : S
      c = down (lookup b γ) δ δ∈
      q : S
      q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
      w : S

ここで w は構成可能な台における実際の段階 Lset δ である。供給の仮定を δ に適用すると、その充足関係表、符号集合、環境の塔、後継段階がいずれも Zv に属するという証明が得られる。この四つの界とそれらを同定する等式により、defIn-in は残る課題を数学的事実 x ∈ 𝒟ₒ (Lset δ) に帰着させる。

      w = LsetS δ oδ
      s = sup δ oδ δ∈
      hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩
      hb = DefInRead.defIn-in i0 (sh  z) (shN  N) (var i8 ∈̇ var i0)
             (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) tg w refl

四つの有界な対象は、実際の充足関係表、符号集合、環境の塔、そして Lset (sucV δ) である。供給の仮定はそれぞれが Zv に属することを証明し、最初の三つは反射律によって記述が要求する構造と一致する。最後に Lset-suc δ が四つ目を 𝒟ₒ (Lset δ) と同一視するので、もとの x の所属を論理式の本体へ移せる。

             (SatGraph.pairs w) (AllCodes w) (Tower.tower w) (LsetS (sucV δ) (suc-ord oδ))
             (s .fst) (s .snd .fst) (s .snd .snd .fst) (s .snd .snd .snd) refl refl refl (Lset-suc δ)
             (subst (λ u → ⟨ x .fst ∈ u ⟩) (sym (Lset-suc δ)) xD)

over の連言を示すため、c ∈ Bv、表の要素 q、そして q を対 (c,w) として提示する仕方を固定する。すると正しさにより w は Lset c と同一視される。残る目標は y について一様である。すべての y ∈ 𝒟ₒ w が候補の値 Vv に属さなければならない。これは候補の値を Bv における段階と同一視するために必要な第二の包含である。

  over : ⟨ γ ⊨ overAt v b f z N ⟩
  over c c∈ q q∈ = sndAll-in i0 i1 overBody (q ∷ c ∷ γ) (λ w s s∈ w∈ e →
    let wq : w .fst ≡ Lset (c .fst)
        wq = vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) e q∈)
        oc : IsOrd (c .fst)

c の順序数性は界から受け継がれ、段階は台の要素として提示され、供給の関数が c で四つの証人を作る。

        oc = mem-ord {A = Bv} ob (c .fst) c∈
        W : S
        W = LsetS (c .fst) oc
        s' = sup (c .fst) oc c∈
    in DefInRead.defIn-in i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v)))

c における供給は、実際の充足関係表、符号集合、環境の塔、後継段階をすべて Zv の中に有界化するので、defIn-in は定義可能冪集合の記述を示せる。y がそこで記述された集合に属するとき、Lset-suc c によりこれは y ∈ 𝒟ₒ (Lset c) となり、さらに c ∈ Bv と Lset-in によって y ∈ Lset Bv が得られる。最後に Vv ≡ Lset Bv に沿って移せば、候補の値への所属が従う。

         (w ∷ s ∷ q ∷ c ∷ γ) tg W wq
         (SatGraph.pairs W) (AllCodes W) (Tower.tower W) (LsetS (sucV (c .fst)) (suc-ord oc))
         (s' .fst) (s' .snd .fst) (s' .snd .snd .fst) (s' .snd .snd .snd) refl refl refl (Lset-suc (c .fst))
         (λ y y∈d → subst (λ u → ⟨ y .fst ∈ u ⟩) (sym vq)
           (Lset-in Bv (c .fst) (y .fst) c∈ (subst (λ u → ⟨ y .fst ∈ u ⟩) (Lset-suc (c .fst)) y∈d))))

module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (tg : Tags γ N) where

private
  Fv = (lookup f γ) .fst
  Bv = (lookup b γ) .fst
  Zv = (lookup z γ) .fst

ステップの本体は、四つずらした枠でのステップの条項である。

  stepBody : Formula S ( + m)
  stepBody = stepAt i0 i1 (sh  f) (sh  z) (shN  N)

近似の条項の外向きの読み出しは、界での表の正しさと完備さを作る。述語 P は、それぞれの入力について証明すべきことを記録する。記録された値がその入力での段階であること。結果が正確に Values と Entries であることに注意してほしい。表が対でない要素や、界の外を第一成分とする項目を含まないとは述べていない。

approx-out : ⟨ γ ⊨ approxAt f b z N ⟩ → IsOrd Bv → Values (lookup f γ) Bv × Entries (lookup f γ) Bv
approx-out (hd , hs) ob = vals , ents
  where
  P : V ℓ → Type (ℓ-suc ℓ)
  P c = ⟨ c ∈ Bv ⟩ → (w : S) → ⟨ pr c (w .fst) ∈ Fv ⟩ → w .fst ≡ Lset c

被覆の節は、各 c ∈ Bv に対して、第一成分が c である対を提示する表の要素が命題的に切り詰められた意味で存在すると述べる。その対を読むと値 w が現れ、もとの所属の証明は正準な記法 pr c w へ移される。結果は命題的に切り詰められたままなので、entryOf は後の命題的推論に存在を与えるが、値を大域的に選ぶことはない。

  entryOf : (c : S) → ⟨ c .fst ∈ Bv ⟩ → ∥ Σ[ w ∶ S ] ⟨ pr (c .fst) (w .fst) ∈ Fv ⟩ ∥₁
  entryOf c c∈ = rec₁ squash₁
    (λ { (q , (q∈ , h)) → map₁ (λ { (w , s , (e , _)) → w , subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ })
                            (sndEx-out i0 i1 ⊤̇ (q ∷ c ∷ γ) h) })
    (hd c c∈)

帰納段階では、c ∈ Bv を満たす任意の記録された対 (c,w) を検証する。その所属の証明から近似の第二の節が stepAt w c を与え、帰納の仮定が c より下の各入力での正しさを与える。さらに被覆の節がそこで対応する正準な項目を与える。したがって StepRead.step-out は、記録された値がちょうど Lset c であると結論できる。

  step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c
  step c IH c∈ w rec =
    StepRead.step-out i0 i1 (sh  f) (sh  z) (shN  N) env tg
      (useBoth i0 (q ∷ γ) cS w refl stepBody (hs q rec)) vals' ents'
    where

ここで関係する集合を構成可能な台の中に提示する。所属 c ∈ Bv から台の要素 cS が得られ、pr c (w .fst) が表に属するという仮定から q が得られる。値 w はすでに帰納述語へ渡された台の要素である。次の環境は、この三つの提示をステップの論理式が要求する枠に置く。

    cS : S
    cS = down (lookup b γ) c c∈
    q : S
    q = down (lookup f γ) (pr c (w .fst)) rec
    env : Vec S ( + m)

拡張された環境は、ステップの読み出しのための四つの枠を組み立てる。界の順序数性がより小さい入力を界の下に制限し、より小さい入力での正しさの読み出しは、帰納の仮定の制限である。

    env = w ∷ cS ∷ container q cS w refl .fst ∷ q ∷ γ
    in' : (y : S) → ⟨ y .fst ∈ c ⟩ → ⟨ y .fst ∈ Bv ⟩
    in' y y∈ = ob .fst {x = c} {y = y .fst} y∈ c∈
    vals' : Values (lookup f γ) c
    vals' y w' y∈ rec' = IH (y .fst) y∈ (in' y y∈) w' rec'

より小さい入力での完備さも同じ制限で復元される。より小さい入力ごとに、切り詰められた項目が消費され、帰納の仮定の値の等式が、正準な項目を所定の位置へ運ぶ。

    ents' : Entries (lookup f γ) c
    ents' y y∈ = rec₁ ((pr (y .fst) (Lset (y .fst)) ∈ Fv) .snd)
      (λ { (w' , rec') → subst (λ u → ⟨ pr (y .fst) u ∈ Fv ⟩) (IH (y .fst) y∈ (in' y y∈) w' rec') rec' })
      (entryOf y (in' y y∈))

Bv より下での正しさは、基礎にある入力 c に対する周囲の所属帰納によって得られる。述語 P c は c ∈ Bv を条件とする。この所属は定理を必要な界に制限すると同時に、Bv の順序数性を通じて、より小さい各入力に帰納の仮定を適用できるようにする。帰納の結論を任意の記録された値に適用すると Values が得られる。

  vals : Values (lookup f γ) Bv
  vals c w c∈ rec = ∈-induction {P = P} step (c .fst) c∈ w rec

界での完備さは、切り詰められた項目と、今証明した正しさを合成する。値の等式が、記録された項目を正準な項目へ運ぶ。

  ents : Entries (lookup f γ) Bv
  ents c c∈ = rec₁ ((pr (c .fst) (Lset (c .fst)) ∈ Fv) .snd)
    (λ { (w , rec) → subst (λ u → ⟨ pr (c .fst) u ∈ Fv ⟩) (vals c w c∈ rec) rec })
    (entryOf c c∈)

近似の条項の内向きの方向は、より強い意味論的な仮定からはじまる。表が界で階層を実現することである。この非対称は意図的なものである。外向きの方向が証明するのは二つの表の条件だけで、内向きの方向が消費するのは、階層の完全な仕様である。

approx-in : (ob : IsOrd Bv) → IsHier Bv (lookup f γ)
          → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
          → ⟨ γ ⊨ approxAt f b z N ⟩
approx-in ob sp sup = dom , steps
  where

階層の仕様の外向きの読み出しは、記録されたそれぞれの対について、入力が界の下にあり、値がそこの段階に等しいと言う。

  hout : (c w : S) → ⟨ pr (c .fst) (w .fst) ∈ Fv ⟩ → ⟨ c .fst ∈ Bv ⟩ × (w .fst ≡ Lset (c .fst))
  hout = hier-out Bv ob (lookup f γ) sp

内向きの読み出しは、界の下のすべての正準な対が記録されていると言う。

  hin : (c : S) → ⟨ c .fst ∈ Bv ⟩ → ⟨ pr (c .fst) (Lset (c .fst)) ∈ Fv ⟩
  hin = hier-in Bv ob (lookup f γ) sp

定義域の連言項は、界の下のそれぞれの入力で段階を提示し、正準な対を表の中へ注入することで証明される。

  dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh  f)) (sndEx i0 i1 ⊤̇)) ⟩
  dom c c∈ = ∣ q , ( hin c c∈ , fillSnd i0 (q ∷ c ∷ γ) c w refl ⊤̇ (λ z → z) i1 refl ) ∣₁
    where
    w : S
    w = LsetS (c .fst) (mem-ord {A = Bv} ob (c .fst) c∈)

正準な対は、所属の証明を下降して台の要素として提示される。

    q : S
    q = down (lookup f γ) (pr (c .fst) (Lset (c .fst))) (hin c c∈)

近似の第二の連言は、表の各要素 q と、q を対 (c,w) として提示する各方法について示す必要がある。そのような提示のもとでは、階層の厳密な仕様から c ∈ Bv と w ≡ Lset c の両方が得られ、c におけるステップの論理式を証明する準備が整う。ここでは、候補の表の任意の要素がそのような対の提示をもつとは主張していない。

  steps : ⟨ γ ⊨ ∀̇∈ (var f) (bothAll i0 stepBody) ⟩
  steps q q∈ = bothAll-in i0 stepBody (q ∷ γ) (λ c w s s∈ c∈s w∈s e →
    let rec : ⟨ pr (c .fst) (w .fst) ∈ Fv ⟩
        rec = subst (λ u → ⟨ u ∈ Fv ⟩) e q∈
        c∈ : ⟨ c .fst ∈ Bv ⟩

入力は、階層の外向きの読み出しによって界の下にあり、順序数性は受け継がれる。そして StepRead.step-in が、制限された正しさと完備さと、より小さい入力ごとの供給を含む、五つの仮定をすべて受け取る。

        c∈ = hout c w rec .fst
        oc : IsOrd (c .fst)
        oc = mem-ord {A = Bv} ob (c .fst) c∈
    in StepRead.step-in i0 i1 (sh  f) (sh  z) (shN  N) (w ∷ c ∷ s ∷ q ∷ γ) tg oc (hout c w rec .snd)
         (λ d w' d∈ rec' → hout d w' rec' .snd)

現在の入力 c より下での完全性は hier-in から得られる。順序数である界の推移性が d ∈ c ∈ Bv を d ∈ Bv に変え、そこで正準な項目の存在が分かる。補助的な界は別の根拠から来る。与えられた供給関数 sup を同じ推移性に沿って制限したものである。したがって、階層の仕様が表の項目を与え、sup が四つの有界な符号化対象を与える。

         (λ d d∈ → hin d (ob .fst {x = c .fst} {y = d .fst} d∈ c∈))
         (λ d od d∈ → sup d od (ob .fst {x = c .fst} {y = d} d∈ c∈)))