可构造层级的 Δ₀ 描述

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 运输，便得到 y 属于拟议取值。

         (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，并沿同一传递性论证限制到 c 以下。因此，层级规格提供表条目，而 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∈)))