---
title: "Reading and validating the satisfaction clauses"
module: L.Coding.SatisfactionClauseSemantics
lang: en
site: "Bedrock"
description: "Reading and validating the satisfaction clauses"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 65
canonical: https://bedrock.institute/en/L.Coding.SatisfactionClauseSemantics.html
html: L.Coding.SatisfactionClauseSemantics.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionClauseSemantics.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Environment, L.Coding.EnvironmentSet, L.Coding.Model, L.Coding.Expressions, L.Axioms.Basic, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.Coding.SatisfactionClauses, FOL.Manipulation.ConstantMapping, L.Coding.Satisfaction, L.Coding.SatisfactionBridge]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.SatisfactionClauseSemantics.md, https://bedrock.institute/ja/L.Coding.SatisfactionClauseSemantics.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
The specification `tableAt` combines two domain conditions, `total` and `onC`, with ten constructor clauses. How does one constructor clause become a step in the semantic recursion? This chapter first reads each clause as an exact extensional condition on a candidate value set, then proves the same condition for the recursively constructed set `SatW`. Extensionality can identify the two values once the surrounding argument also supplies the matching code, its subvalues, and a table entry. The local bridges alone do not prove that a whole table is functional or uniquely determined.

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

The argument takes excluded middle at level `ℓ-suc ℓ` as an explicit parameter. Decoding witnesses will nevertheless remain merely existent when their type has been propositionally truncated; the classical hypothesis does not turn those witnesses into chosen data.

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

All subsequent constructions are relative to the fixed hypothesis `lem`. This keeps the logical cost visible when the local clause readers are later imported into the global soundness and completeness proofs.

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

Two languages meet in this proof. The internal formulas describe coded tables inside `L`; the external formulas are interpreted recursively in the structure presented by `W`. The bridge must respect each formula constructor, including bounded quantifiers whose bounds are term values in the current environment.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; con; _∈̇_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∃̇∈; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

A finite environment is represented internally by its graph of ordered pairs `(i,v)`. Pair injectivity recovers an index and its value, while `lookup-spec` states that the canonical graph contains exactly the pair belonging to each host-level slot. Membership in `envSet W n` later says, merely, that a set is the graph of some length-`n` assignment into `W`.

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.Model {ℓ} using ( prAtL; container )
```

The internal clauses can inspect pair components only through bounded formulas. A `container` supplies one constructible set containing both components, so the pair readers can bind them without an unbounded search. The analogous `consAtL` reader connects the graph of `x ∷ δ` with the graph of `δ`, which is the semantic step needed for quantifiers.

```agda
open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Coding.Quantification {ℓ} using
```

Three kinds of finite index must remain distinct. A natural `n` is a formula arity, `# n` is its set-theoretic numeral inside a code, and `Fin m` selects a slot of a host-level vector of length `m`. The names `i0` through `i19` and the shift `sh` only manage the last of these: when a binder adds a value at the head, every older slot is shifted past it.

```agda
  ( i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh
  ; pr-out; pr-in; down; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in
  ; fillSnd; fillBoth; useSnd; useBoth )
```

The common table frame has a fixed nested shape. An environment-tower entry codes `(ar,F)`, a formula key codes `(ar,p)`, its payload codes `(tag,r)`, and a table entry codes `(c,yc)`. The readers below repeatedly peel these pairs so that a constructor relation can speak about the candidate value `yc` over the environment set `F`.

```agda
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.Coding.SatisfactionClauses {ℓ}
  using ( extB; fstAll; subAt; subSucAt; tmIs; module Rel; module Clause )
```

The external environment is a finite vector, but the table stores a set-theoretic graph. Moving between them requires both host-level finite lookup and object-level pair membership. Products and coproducts then record the alternatives exposed by formula and term constructors without conflating those alternatives with the coded sets themselves.

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.Vec using ( _∷_; []; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
```

Most semantic comparisons are paths between propositions, obtained from implications in both directions. Propositional truncation is equally essential: pair decompositions and decoded environments may be used inside a proposition, while no global choice of their witnesses is produced.

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

All codes live in the cumulative hierarchy. Ordered-pair codes and the numerals `# n` are therefore actual sets, and their injectivity lets later proofs recover arities, tags, and payloads from equations between codes. The h-set structure of the hierarchy ensures that these recovered equalities are proposition-valued.

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

The internal assignments range over the constructible carrier `S`, but their equations and memberships concern the underlying sets selected by `fst`. Bounded absoluteness supplies the interpretation of internal formulas in this carrier. Every reader therefore ends with a concrete statement about projected sets, ready to be compared with the external recursion.

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

## Reading the shared frame

The central type records an extensional fact about a set `y`: every member of `y` belongs to `F` and satisfies the property, and conversely every member of `F` satisfying the property belongs to `y`. A value set is described by such a fact rather than by a chosen enumeration.

```agda
ExtFact : (y F : V ℓ) (P : S → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ)
ExtFact y F P = ((z : S) → ⟨ fst z ∈ y ⟩ → ⟨ fst z ∈ F ⟩ × P z)
              × ((z : S) → ⟨ fst z ∈ F ⟩ → P z → ⟨ fst z ∈ y ⟩)
```

The extensional set builder is read definitionally: satisfaction of the builder is literally the pair of the two membership directions, with the property evaluated in the environment extended by the bound variable.

```agda
module _ {j : ℕ} (y F : Fin j) (φ : Formula S (1 + j)) (δ : S ^ j) where
  extB-out : ⟨ δ ⊨ extB y F φ ⟩ → ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩)
  extB-out h = h
```

Filling is likewise definitional: an extensional fact is exactly satisfaction of the builder.

```agda
  extB-in : ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩) → ⟨ δ ⊨ extB y F φ ⟩
  extB-in h = h
```

Suppose `y` and `y'` satisfy the same extension condition over `F`: among the elements of `F`, membership in either set is characterized by the property `P`. Extensionality reduces equality of their underlying sets to two membership conversions. In the first direction, a member of `y` passes through the outward half of its extension fact and then through the inward half for `y'`.

```agda
ext-unique : (y y' F : S) (P : S → Type (ℓ-suc ℓ))
           → ExtFact (fst y) (fst F) P → ExtFact (fst y') (fst F) P → fst y ≡ fst y'
ext-unique y y' F P (o1 , i1') (o2 , i2') =
  cong fst (extensionalL {a = y} {b = y'} (λ z → ⇔toPath
    (λ hz → i2' z (o1 z hz .fst) (o1 z hz .snd))
```

The backward conversion closes the biconditional: a member of the right-hand side is first recognized as a member of `F` satisfying the property, and the second half of the extensional fact then returns its membership in `y`. Composing the two conversions gives the equality of the underlying sets of `y` and `y'`; what is identified is the underlying set, not any chosen coding evidence.

```agda
    (λ hz → i1' z (o2 z hz .fst) (o2 z hz .snd))))
```

To use a subformula value, fix a table slot `T`, an arity slot `ar`, a payload slot `a`, and a body that expects four new entries. The reader will expose a matching table pair `(c₁,ya)` and place, in front of the old environment, the value `ya`, its key `c₁`, a container for the pair components, and a constructible representative of the table entry itself.

```agda
module _ {j : ℕ} (T ar a : Fin j) (body : Formula S (4 + j)) (δ : S ^ j) where
  private
    Tv = fst (lookup T δ)
    TS = lookup T δ
    A = fst (lookup ar δ)
```

Write `A` for the projected arity and `Av` for the projected payload. The matching condition for the subkey is then the single equation `fst c₁ ≡ pr A Av`, which keeps the coded key separate from the host-level slots that supplied its two components.

```agda
    Av = fst (lookup a δ)
```

If `subAt` holds, every table entry whose underlying pair is `(c₁,ya)` and whose key satisfies `c₁=(A,Av)` yields the body. The body is evaluated at `ya ∷ c₁ ∷ s ∷ e' ∷ δ`, where `e'` represents that table entry and `s` is only a container exposing the two pair components. Neither auxiliary object is an additional semantic value.

```agda
  subAt-out : ⟨ δ ⊨ subAt T ar a body ⟩ → (c₁ ya : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩)
            → fst c₁ ≡ pr A Av
            → ⟨ (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
                 ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩
  subAt-out h c₁ ya m e =
```

The proof first applies the table-bounded universal to the concrete representative `e'` of `(c₁,ya)`. The pair reader then supplies the two components `c₁` and `ya`; finally `pr-in` turns the equation `c₁=(A,Av)` into the antecedent required by the internal implication. What remains is exactly the requested body at the four-slot extension.

```agda
    useBoth i0 (down TS (pr (fst c₁) (fst ya)) m ∷ δ) c₁ ya refl (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body)
      (h (down TS (pr (fst c₁) (fst ya)) m) m)
      (pr-in i1 (sh 4 ar) (sh 4 a)
        (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
           ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) e)
```

Filling is the converse: given a proof of the body for every matching table entry with its own container, the bounded universal over table entries holds. Note what this reader does not do: it does not select one entry, and it does not assert that the value `ya` is unique; it quantifies over all matching entries.

```agda
  subAt-in : ((c₁ ya s e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A Av
              → ⟨ (ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
           → ⟨ δ ⊨ subAt T ar a body ⟩
  subAt-in g e' e'∈ = bothAll-in i0 (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body) (e' ∷ δ)
    (λ c₁ ya s s∈ c₁∈ ya∈ e hp → g c₁ ya s e' e'∈ e (pr-out i1 (sh 4 ar) (sh 4 a) (ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp))
```

The second subclause reader is stated for the raised-arity shape: its body is extended by six slots, because the subformula of a quantified formula is read at the raised arity.

```agda
module _ {j : ℕ} (T ar a : Fin j) (body : Formula S (6 + j)) (δ : S ^ j) where
  private
    Tv = fst (lookup T δ)
    TS = lookup T δ
    A = fst (lookup ar δ)
```

The arity value of the outer formula is named, and the raised one is recovered separately inside the proof.

```agda
    Av = fst (lookup a δ)
```

The raised reader uses a table entry at a key `(ar',Av)` together with the equation `fst ar' ≡ sucV A`. Its body is evaluated at `ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ`: the two containers `s'` and `s` merely make the components of the raised key and the table entry available to bounded formulas.

```agda
  subSucAt-out : ⟨ δ ⊨ subSucAt T ar a body ⟩ → (c₁ ya ar' : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩)
               → (e : fst c₁ ≡ pr (fst ar') Av) → fst ar' ≡ sucV A
               → ⟨ (ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ ya ∷ c₁
                    ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
                    ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩
```

Starting from the given table entry, the proof first obtains the four-slot statement `h4` by decomposing `(c₁,ya)`. It then supplies the candidate first component `ar'` to `fstAll`, proves `c₁=(ar',Av)` with `pr-in`, and proves `ar'=suc A` with `suc-in`. These two equations are precisely the guards needed before the body may be used.

```agda
  subSucAt-out h c₁ ya ar' m e es =
    (h4 (container c₁ ar' (lookup a δ) e .fst) (container c₁ ar' (lookup a δ) e .snd .fst)
        ar' (container c₁ ar' (lookup a δ) e .snd .snd .fst)
        (pr-in (sh 2 i1) i0 (sh 2 (sh 4 a)) δ6 e))
      (suc-in (sh 6 ar) i0 δ6 es)
```

The local name `e'S` is a constructible representative of the particular table entry `(c₁,ya)`, obtained from its membership in `T`. The environment `δ4` then places `ya`, `c₁`, a container for their pair, and `e'S` before `δ`; it does not contain a presentation of the whole table.

```agda
    where
    e'S = down TS (pr (fst c₁) (fst ya)) m
    δ4 : S ^ (4 + j)
    δ4 = ya ∷ c₁ ∷ container e'S c₁ ya refl .fst ∷ e'S ∷ δ
    δ6 : S ^ (6 + j)
```

Applying `useBoth` to the chosen table entry removes the outer table quantifier and the pair decomposition in one step. The result `h4` is the remaining `fstAll` statement at `δ4`; it still requires a candidate first component of `c₁` and the equations identifying that component with the successor arity.

```agda
    δ6 = ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ δ4
    h4 : ⟨ δ4 ⊨ fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body) ⟩
    h4 = useBoth i0 (e'S ∷ δ) c₁ ya refl (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)) (h e'S m)
```

For the converse direction, it is enough to prove the body uniformly for every possible table-entry decomposition and every possible first-component decomposition of its key. The two equations in the hypothesis ensure that only entries at `(suc A,Av)` matter; no particular entry or raised arity is selected globally.

```agda
  subSucAt-in : ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
                 → fst c₁ ≡ pr (fst ar') Av → fst ar' ≡ sucV A
                 → ⟨ (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
              → ⟨ δ ⊨ subSucAt T ar a body ⟩
  subSucAt-in g e' e'∈ = bothAll-in i0 (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)) (e' ∷ δ)
```

The introduction proof receives the components exposed by the two universal pair readers. It uses `pr-out` to recover the equation `c₁=(ar',Av)` and `suc-out` to recover `ar'=suc A`, then passes those equations, the table memberships, and the six-slot environment to the uniform hypothesis `g`.

```agda
    (λ c₁ ya s s∈ c₁∈ ya∈ e s' s'∈ ar' ar'∈ hp hs →
      g c₁ ya ar' s s' e' e'∈ e
        (pr-out (sh 2 i1) i0 (sh 2 (sh 4 a)) (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp)
        (suc-out (sh 6 ar) i0 (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hs))
```

`TmIsV t z v` records the two possible term-code shapes, under propositional truncation. Either `t=(#0,v)`, the constant case, or there merely exists an index `i` with `t=(#1,i)` and the graph entry `(i,v)` belonging to `z`, the variable case. For an arbitrary relation `z`, this statement contains no functionality or uniqueness claim.

```agda
TmIsV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
TmIsV t z v = ∥ (t ≡ pr (# 0) v) ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# 1) i) × ⟨ pr i v ∈ z ⟩)) ∥₁
```

The local reader is parameterized by five host-level slots: the term code, the environment graph, its proposed value, and the two tag numerals. The hypotheses `q0` and `q1` identify the last two slots with `#0` and `#1`; the local names `Tv` and `Z` project the term code and graph to the hierarchy where the coding equations live.

```agda
module _ {j : ℕ} (t z v N0 N1 : Fin j) (δ : S ^ j)
  (q0 : fst (lookup N0 δ) ≡ # 0) (q1 : fst (lookup N1 δ) ≡ # 1) where
  private
    Tv = fst (lookup t δ)
    Z = fst (lookup z δ)
```

The remaining projections name the proposed value `Vv` and the actual set stored in the tag-one slot, `N1v`. The proof must carry equations through `q1` because the internal formula refers to `N1v`, whereas `TmIsV` states its variable branch with the canonical numeral `#1`.

```agda
    Vv = fst (lookup v δ)
    N1v = fst (lookup N1 δ)
```

The inner bounded existential ranges over entries `q` of the graph `z`, not over indices themselves. Its pair atom asserts `q=(i,v)`, where the index `i` was already recovered as the second component of the term code. Thus the internal formula says that the graph contains the entry pairing that fixed index with the proposed value.

```agda
    inner : Formula S (2 + j)
    inner = ∃̇∈ (var (sh 2 z)) (prAtL i0 i1 (sh 3 v))
```

`Inner i s` repackages the semantics of that bounded existential. It merely supplies a graph entry `q`, a proof that `q∈Z`, and satisfaction of the atom saying `q=(i,Vv)` at `q ∷ i ∷ s ∷ δ`. The slot `s` is the container used to expose the components of the term code.

```agda
    Inner : (i s : S) → Type (ℓ-suc ℓ)
    Inner i s = ∥ Σ[ q ∈ S ] (⟨ fst q ∈ Z ⟩ × ⟨ (q ∷ i ∷ s ∷ δ) ⊨ prAtL i0 i1 (sh 3 v) ⟩) ∥₁
```

`Outer` packages the whole variable branch read from `sndEx`: there merely exist a payload representative `i` and a container `s` such that `Tv=pr N1v (fst i)` and the inner bounded existential holds at `i ∷ s ∷ δ`. The equation identifies the term code with the tag-one pair; it does not identify `i` with the tag.

```agda
    Outer : Type (ℓ-suc ℓ)
    Outer = ∥ Σ[ i ∈ S ] Σ[ s ∈ S ] ((Tv ≡ pr N1v (fst i)) × ⟨ (i ∷ s ∷ δ) ⊨ inner ⟩) ∥₁
```

From an inner witness `q`, `pr-out` gives `fst q=pr (fst i) Vv`; transporting the known membership `q∈Z` along this equation yields the required graph membership of `(i,Vv)`. In parallel, `q1` changes the outer equation from the actual tag slot `N1v` to `#1`. These are exactly the two fields of the variable branch of `TmIsV`.

```agda
    viaQ : (i s : S) → Tv ≡ pr N1v (fst i) → Inner i s → TmIsV Tv Z Vv
    viaQ i s e = PT.map
      (λ { (q , (q∈ , hp)) → inr (fst i , ( e ∙ cong (λ a → pr a (fst i)) q1
         , subst (λ u → ⟨ u ∈ Z ⟩) (pr-out i0 i1 (sh 3 v) (q ∷ i ∷ s ∷ δ) hp) q∈ )) })
```

`viaI` eliminates the merely existing outer decomposition into `TmIsV`. This elimination is allowed because `TmIsV` is itself propositionally truncated, so the construction transforms each local pair decomposition without choosing one decomposition for later use.

```agda
    viaI : Outer → TmIsV Tv Z Vv
    viaI = PT.rec squash₁ (λ { (i , s , (e , hq)) → viaQ i s e hq })
```

The object formula `tmIs` is a disjunction of two code shapes. In the constant branch, `pr-out` reads `Tv=pr(q0,Vv)` and the equation `q0=#0` converts it to the first branch of `TmIsV`. In the variable branch, `sndEx-out` produces `Outer`, which `viaI` converts to the graph-membership branch.

```agda
    cases : ⟨ δ ⊨ prAtL t N0 v ⟩ ⊎ ⟨ δ ⊨ sndEx t N1 inner ⟩ → TmIsV Tv Z Vv
    cases (inl h) = ∣ inl (pr-out t N0 v δ h ∙ cong (λ a → pr a Vv) q0) ∣₁
    cases (inr h) = viaI (sndEx-out t N1 inner δ h)
```

The public elimination `tmIs-out` performs that case analysis under the outer disjunction's propositional truncation. Its conclusion concerns one proposed value `Vv`; it does not show that two proposed values agree. If `Z` is an arbitrary multivalued relation, the same variable code may satisfy `tmIs` at more than one value.

```agda
  tmIs-out : ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ → TmIsV Tv Z Vv
  tmIs-out h = PT.rec squash₁ cases h
```

For the converse, `build` turns either concrete code shape back into satisfaction of `tmIs`. The constant equation is converted by `pr-in`. In the variable case, the proof must represent the payload index and the graph entry as elements of `S`, then rebuild the nested bounded existentials of `sndEx`.

```agda
  private
    build : (Tv ≡ pr (# 0) Vv) ⊎ (Σ[ i ∈ V ℓ ] ((Tv ≡ pr (# 1) i) × ⟨ pr i Vv ∈ Z ⟩))
          → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
    build (inl e) = ∣ inl (pr-in t N0 v δ (e ∙ cong (λ a → pr a Vv) (sym q0))) ∣₁
    build (inr (i , (e , hp))) = ∣ inr (fillSnd t δ (lookup N1 δ) iS e' inner hq N1 refl) ∣₁
```

`iS` is the constructible representative of the payload `i`, recovered as the second component of the pair equation `Tv=(#1,i)`. The term `qS` is the constructible representative of the graph entry `(i,Vv)`, obtained from its membership in `Z`. These are witnesses inside `S`, not new semantic indices or values.

```agda
      where
      iS : S
      iS = sndS (lookup t δ) (# 1) i e
      qS : S
      qS = down (lookup z δ) (pr i Vv) hp
```

The equation `e'` rewrites the canonical tag equation into the actual tag-one slot required by `sndEx`. The auxiliary environment `δ3` places the graph entry `qS`, the payload representative `iS`, and the container for the outer term-code pair before `δ`. The remaining goal `hq` is exactly the inner bounded existential at `iS ∷ container ∷ δ`.

```agda
      e' : Tv ≡ pr N1v (fst iS)
      e' = e ∙ cong (λ a → pr a i) (sym q1)
      δ3 : S ^ (3 + j)
      δ3 = qS ∷ iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ
      hq : ⟨ (iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ) ⊨ inner ⟩
```

To prove `hq`, choose `qS` from the graph. Its membership is the given fact `hp`, and `pr-in` proves by reflexivity that its underlying set is the pair of `iS` and `Vv`. This supplies exactly the graph entry demanded by the variable branch.

```agda
      hq = ∣ qS , (hp , pr-in i0 i1 (sh 3 v) δ3 refl) ∣₁
```

Finally, `tmIs-in` eliminates the propositional truncation in `TmIsV` into the proposition expressing satisfaction of `tmIs`, applying `build` to either branch. Together with `tmIs-out`, this gives both semantic directions while preserving the absence of any global choice or uniqueness claim.

```agda
  tmIs-in : TmIsV Tv Z Vv → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
  tmIs-in = PT.rec (snd (δ ⊨ tmIs t z v N0 N1)) build
```

`Frame` fixes the host-level slots for the table `T`, carrier `w`, code domain `C`, and environment tower `E`, together with the ten tag slots `N` and the surrounding assignment `γ`. The hypothesis `Tags γ N` identifies each tag slot with its numeral, allowing a clause selected by `k : Fin 10` to be read as the relation `relN (toℕ k)`.

```agda
module Frame {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
    Ev = fst (lookup E γ)
```

The frame is peeled by a sequence of bounded universals. At the innermost stage, `inner9 k` ranges over every table entry and uses `sndAll` to expose a value `yc` whenever that entry has first component `c`; the resulting twelve-slot environment is where `relN (toℕ k)` must hold. This is a universal condition on matching entries, not an existential search for one value.

```agda
    module Cl = Clause T w C E N
    module R = Rel T w N
    inner9 : Fin 10 → Formula S (9 + m)
    inner9 k = ∀̇∈ (var (sh 9 T)) (sndAll i0 i5 (R.relN (toℕ k)))
    inner7 : Fin 10 → Formula S (7 + m)
```

The preceding stages expose the nested key. `inner4 k` ranges over every `c∈C` whose first component is the current arity `ar`, obtaining its payload `p`; `inner7 k` then requires `p` to have the tag stored at `N k` and exposes its residual data `r`. Each pair decomposition adds its components and a container at the head, so the shifts preserve access to the older frame slots.

```agda
    inner7 k = sndAll i0 (sh 7 (N k)) (inner9 k)
    inner4 : Fin 10 → Formula S (4 + m)
    inner4 k = ∀̇∈ (var (sh 4 C)) (sndAll i0 i2 (inner7 k))
```

For one clause instance, `At` fixes a tower pair `(ar,F)`, a formula key `c=(ar,p)`, a tagged payload `p=(N k,r)`, and a table pair `(c,yc)`. The memberships `q∈` and `e∈` concern the projected pairs in `E` and `T`; the module does not itself prove that `c∈C`, decode `r`, or show that the table value is unique.

```agda
  module At (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩)
            (ec : fst c ≡ pr (fst ar) (fst p)) (k : Fin 10)
            (ep : fst p ≡ pr (fst (lookup (N k) γ)) (fst r))
            (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩) where
    qS eS : S
```

`qS` and `eS` lift the two projected pair memberships back to elements of the constructible carrier. Their underlying sets are definitionally `pr (fst ar) (fst F)` and `pr (fst c) (fst yc)`, respectively. They serve only as representatives to which the bounded pair readers can be applied when the twelve-slot environment is assembled.

```agda
    qS = down (lookup E γ) (pr (fst ar) (fst F)) q∈
    eS = down (lookup T γ) (pr (fst c) (fst yc)) e∈
```

The frame begins with an actual tower member `qS` whose underlying pair is `(ar,F)`. The four new slots record `F`, `ar`, a witness for the pair decomposition, and `qS`; the next three record the payload `p`, a witness that `c=(ar,p)`, and the code `c`. Thus the successive environments retain both the mathematical data and the bounded witnesses by which the object-language clause obtained them.

```agda
    δ4 : S ^ (4 + m)
    δ4 = F ∷ ar ∷ container qS ar F refl .fst ∷ qS ∷ γ
    δ7 : S ^ (7 + m)
    δ7 = p ∷ container c ar p ec .fst ∷ c ∷ δ4
    δ9 : S ^ (9 + m)
```

The twelve-slot environment completes the nesting. At the front is the candidate value `yc`, followed by a container exposing the components of the table pair `(c,yc)` and the actual table member `eS` whose underlying set is that pair; the nine earlier objects follow. This is the environment at which the relation body is read.

```agda
    δ9 = r ∷ container p (lookup (N k) γ) r ep .fst ∷ δ7
    δ12 : S ^ (12 + m)
    δ12 = yc ∷ container eS c yc refl .fst ∷ eS ∷ δ9
```

The outward reading starts from satisfaction of clause `k` and fixes all data matching one instance of its frame: `ar` and `F` from a tower pair, a code `c=(ar,p)` in `C`, a tagged payload `p=(#k,r)`, and a candidate value `yc` with `(c,yc)` in `T`. It then returns satisfaction of `relN (toℕ k)` at the corresponding twelve-slot environment. The table hypothesis here is membership of the pair `(c,yc)`; the representative table member and its container are constructed locally.

```agda
  clause-out : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩
             → (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩) → ⟨ fst c ∈ Cv ⟩
             → (ec : fst c ≡ pr (fst ar) (fst p)) → (ep : fst p ≡ pr (# (toℕ k)) (fst r))
             → (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩)
             → ⟨ At.δ12 ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈ ⊨ R.relN (toℕ k) ⟩
```

With the matching data fixed, the module `A` gives one coherent realization of all twelve frame slots. The first elimination opens the tower pair, and the final `useSnd` opens the actual table member as `(c,yc)`. Between them, the proof must still pass through the code and tag layers; naming `h4` before those steps makes explicit that the conclusion follows by successively specializing the single outer clause, rather than by assuming the constructor relation separately.

```agda
  clause-out k h ar F c p r yc q∈ c∈ ec ep e∈ =
    useSnd i0 (A.eS ∷ A.δ9) c yc refl (R.relN (toℕ k)) i5 refl (h9 A.eS e∈)
    where
    module A = At ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈
    h4 : ⟨ A.δ4 ⊨ inner4 k ⟩
```

The three intermediate judgments mark the three semantic layers of the common frame. At `δ4`, `h4` has opened the tower entry `(ar,F)` and is ready to range over codes in `C`; at `δ7`, `h7` has also decomposed `c=(ar,p)`; at `δ9`, `h9` has identified `p` as the tag-`k` payload `r` and is ready to inspect entries of `T`. The final elimination then decomposes the chosen table member as `(c,yc)` and reaches the constructor relation.

```agda
    h4 = useBoth i0 (A.qS ∷ γ) ar F refl (inner4 k) (h A.qS q∈)
    h7 : ⟨ A.δ7 ⊨ inner7 k ⟩
    h7 = useSnd i0 (c ∷ A.δ4) ar p ec (inner7 k) i2 refl (h4 c c∈)
    h9 : ⟨ A.δ9 ⊨ inner9 k ⟩
    h9 = useSnd i0 A.δ7 (lookup (N k) γ) r (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) (inner9 k) (sh 7 (N k)) refl h7
```

For the converse direction, suppose the constructor relation can be proved from every complete matching frame. Such a frame consists of a tower member `q=(ar,F)`, a code `c=(ar,p)` in `C`, a tag decomposition `p=(#k,r)`, and a table member `e=(c,yc)`, together with the four pair witnesses `s`, `s1`, `s2`, and `s3`. Proving the relation in the displayed environment for all this data is exactly the premise needed to reconstruct clause `k`.

```agda
  clause-in : (k : Fin 10)
            → ((q ar F s c p s1 r s2 e yc s3 : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F)
               → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (fst ar) (fst p) → fst p ≡ pr (# (toℕ k)) (fst r)
               → ⟨ fst e ∈ Tv ⟩ → fst e ≡ pr (fst c) (fst yc)
               → ⟨ (yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) ⊨ R.relN (toℕ k) ⟩)
```

The proof rebuilds the universally quantified frame in its logical order. It handles an arbitrary `q` in `E` together with every exposed decomposition `q=(ar,F)`, then an arbitrary `c` in `C` together with every matching decomposition `c=(ar,p)`. It next identifies the tag and payload of `p`, and finally handles an arbitrary `e` in `T` together with every decomposition `e=(c,yc)`. Each bounded introduction places its new value at the head of the environment, while the accompanying `s`-variables retain the pair-decomposition witnesses required by the formulas.

```agda
            → ⟨ γ ⊨ Cl.clause k ⟩
  clause-in k g q q∈ = bothAll-in i0 (inner4 k) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ eq c c∈ →
    sndAll-in i0 i2 (inner7 k) (c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ p s1 s1∈ p∈ ec →
      sndAll-in i0 (sh 7 (N k)) (inner9 k) (p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ r s2 s2∈ r∈ ep e e∈ →
        sndAll-in i0 i5 (R.relN (toℕ k)) (e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ yc s3 s3∈ yc∈ ee →
```

Before the host-level rule `g` is applied, the payload equation is composed with `tg k`, replacing the set stored in the tag slot by the canonical numeral `#k`. The rule therefore receives exactly the equation `p=(#k,r)` appearing in the outward reading. Thus `clause-in` and `clause-out` give the two directions between clause `k` and its relation at every matching frame.

```agda
          g q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec (ep ∙ cong (λ a → pr a (fst r)) (tg k)) e∈ ee))))
```

Totality is read outward as truncated existence: for each member of the code domain, the totality clause guarantees that some table entry with that first component exists, and the truncated decomposition of the table entry recovers the value `yc`.

```agda
  total-out : ⟨ γ ⊨ Cl.total ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
  total-out h c c∈ = PT.rec squash₁
    (λ { (e , (e∈ , hs)) → PT.map
      (λ { (yc , s , (ee , _)) → yc , subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈ })
      (sndEx-out i0 i1 ⊤̇ (e ∷ c ∷ γ) hs) })
```

For a fixed `c∈C`, applying the standing hypothesis `h` yields, under propositional truncation, a table member `e` together with its membership in `T` and a decomposition statement. The reader `sndEx-out` decomposes `e` as `(c,yc)`, and transporting the membership of `e` along that equation proves `(c,yc)∈T`. Both decompositions remain hidden by the truncation, so the result supplies existence without selecting a canonical value.

```agda
    (h c c∈)
```

Conversely, assume that every `c` in `C` has, propositionally truncated, a value `yc` with `(c,yc)` in `T`. The membership proof is turned by `down` into an element `e : S` of `T` whose underlying set is that pair; `fillSnd` supplies the bounded witnesses that decompose `e` back into `c` and `yc`. The remaining body is truth, so this data constructs the totality clause without choosing a value globally and without asserting uniqueness.

```agda
  total-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁) → ⟨ γ ⊨ Cl.total ⟩
  total-in g c c∈ = PT.map
    (λ { (yc , m) → down (lookup T γ) (pr (fst c) (fst yc)) m
       , ( m , fillSnd i0 (down (lookup T γ) (pr (fst c) (fst yc)) m ∷ c ∷ γ) c yc refl ⊤̇ (λ b → b) i1 refl ) })
    (g c c∈)
```

The on-domain condition starts with an arbitrary element `e` of `T`, rather than with a pair already chosen in advance. Its outward reading recovers, under propositional truncation, objects `c` and `yc` such that `e=(c,yc)` and `c` belongs to `C`. Thus every member of the table has a code from the stated domain as its first component, but the result says neither that the decomposition is selected canonically nor that a code has only one value.

```agda
  onC-out : ⟨ γ ⊨ Cl.onC ⟩ → (e : S) → ⟨ fst e ∈ Tv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
  onC-out h e e∈ = PT.map (λ { (c , yc , s , (ee , c∈)) → c , yc , (ee , c∈) })
    (bothEx-out i0 (var i1 ∈̇ var (sh 4 C)) (e ∷ γ) (h e e∈))
```

The converse asks for precisely that truncated decomposition of every member of `T` and inserts it into the two bounded existentials of `onC`. Together the two readings identify `onC` with the claim that the first projection of every table member lies in `C`. Combined with totality this fixes the table's domain projection, but it still does not make the table single-valued.

```agda
  onC-in : ((e : S) → ⟨ fst e ∈ Tv ⟩ → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁)
         → ⟨ γ ⊨ Cl.onC ⟩
  onC-in g e e∈ = PT.rec (snd ((e ∷ γ) ⊨ bothEx i0 (var i1 ∈̇ var (sh 4 C))))
    (λ { (c , yc , (ee , c∈)) → fillBoth i0 (e ∷ γ) c yc ee (var i1 ∈̇ var (sh 4 C)) c∈ })
    (g e e∈)
```

## Reading the constructor relations

The constructor readers work over a frame `δ` with twelve slots added in front of the original `m`-environment. The original slots `T` and `w`, and the ten numeral slots `N`, therefore live beyond this prefix, while the frame itself places the candidate value `yc` at `i0` and the constructor payload `r` at `i3`. Fixing these positions lets every relation reader use the same outer frame, regardless of the constructor being read.

```agda
module RelRead {m : ℕ} (T w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (12 + m)) where
  private
    module R = Rel T w N
    yc = lookup i0 δ
    r = lookup i3 δ
```

The remaining local names identify the environment-set slot `F` and the arity slot `ar`. They project the underlying table set `Tv`, the arity value `A`, and the constructor payload `Rv` once, so the relation readers can state their hypotheses directly in the cumulative hierarchy.

```agda
    F = lookup i8 δ
    ar = lookup i9 δ
    Tv = fst (lookup (sh 12 T) δ)
    A = fst ar
    Rv = fst r
```

For any further local environment `env`, `Ext env φ` states the exact extension property for the outer table value `yc`. An element `z` belongs to `yc` exactly when it belongs to the arity-appropriate environment set `F` and the formula `φ` holds after `z` is placed in the new head slot of `env`. The old slots of `env` are consequently read one position later inside `φ`.

```agda
  Ext : ∀ {k} (env : S ^ k) (φ : Formula S (1 + k)) → Type (ℓ-suc ℓ)
  Ext env φ = ExtFact (fst yc) (fst F) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)
```

For a binary connective, the payload `r` must decompose as the two child codes `a` and `b`. The keys `c₁=(A,a)` and `c₂=(A,b)` must have table values `ya` and `yb`. From these hypotheses, `bin-out` returns five auxiliary witnesses under propositional truncation: one container for `r=(a,b)`, and for each child both an actual member of `T` and a container witnessing its decomposition. The mathematical conclusion is an `Ext` fact for the outer value `yc`, whose body tests membership in `ya` and `yb` using the connective `op`.

```agda
  bin-out : (op : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.binRel op ⟩
          → (a b c₁ ya c₂ yb : S) → Rv ≡ pr (fst a) (fst b)
          → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr A (fst a)
          → ⟨ pr (fst c₂) (fst yb) ∈ Tv ⟩ → fst c₂ ≡ pr A (fst b)
          → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ e₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
```

The five witnesses are packaged only because the object-language bounded quantifiers hide the pair decompositions. After the payload has been opened, the first `subAt-out` reads the value at the left child key and the second reads the value at the right child key. The innermost `extB` then yields the exact extension of `yc`; it does not assert that either child value was uniquely selected by the table.

```agda
              Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op) ∥₁
  bin-out op h a b c₁ ya c₂ yb er m₁ e₁ m₂ e₂ =
    ∣ container r a b er .fst , container e₁S c₁ ya refl .fst , e₁S , container e₂S c₂ yb refl .fst , e₂S ,
      subAt-out (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)) δ19
        (subAt-out (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op))) δ15
```

The first step is to open the payload equation `r=(a,b)` inside the twelve-slot frame. This contributes the pair container and produces `δ15`, the old frame prefixed by `b`, `a`, and that container. The two nested subvalue readings then proceed from left to right, so their hidden table witnesses remain inside the outer propositional truncation.

```agda
          (useBoth i3 δ a b er (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)))) h)
          c₁ ya m₁ e₁)
        c₂ yb m₂ e₂ ∣₁
    where
    δ15 : S ^ (15 + m)
```

The membership proof for `(c₁,ya)` does not itself supply an element of the structure `S`; `down` realizes it as `e₁S : S`, an actual member of `T` with that underlying pair. The environment `δ19` then prefixes `ya`, `c₁`, their pair container, and `e₁S` to `δ15`. These four slots are exactly the frame expected by the first `subAt` reading.

```agda
    δ15 = b ∷ a ∷ container r a b er .fst ∷ δ
    e₁S : S
    e₁S = down (lookup (sh 15 T) δ15) (pr (fst c₁) (fst ya)) m₁
    δ19 : S ^ (19 + m)
    δ19 = ya ∷ c₁ ∷ container e₁S c₁ ya refl .fst ∷ e₁S ∷ δ15
```

The same construction realizes the second membership proof as `e₂S : S`, an actual table member with underlying pair `(c₂,yb)`. The second `subAt-out` supplies its accompanying pair container when it extends `δ19`. Hence both child values are available to `binBody`, while neither membership proof has been turned into a global choice from the table.

```agda
    e₂S : S
    e₂S = down (lookup (sh 19 T) δ19) (pr (fst c₂) (fst yb)) m₂
```

The converse begins with a rule for every possible decomposition of the binary frame. Besides the child codes and values, the rule receives the payload container, the two actual table members, their pair containers, and the equations proving that their keys are `(A,a)` and `(A,b)`. Its conclusion must be the `Ext` fact for the outer value `yc` in the environment obtained by adding these eleven objects to the original twelve-slot frame.

```agda
  bin-in : (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
         → ((a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ : S) → Rv ≡ pr (fst a) (fst b)
            → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A (fst a)
            → ⟨ fst e₂ ∈ Tv ⟩ → fst e₂ ≡ pr (fst c₂) (fst yb) → fst c₂ ≡ pr A (fst b)
            → Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op))
```

The proof introduces the two argument quantifiers and the relation container, then opens the two nested subAt clauses for the left and right table entries, each introducing its code, value, and pair equation.

```agda
         → ⟨ δ ⊨ R.binRel op ⟩
  bin-in op g = bothAll-in i3 (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)))) δ
    (λ a b s s∈ a∈ b∈ er →
      subAt-in (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op))) (b ∷ a ∷ s ∷ δ)
        (λ c₁ ya s₁ e₁ e₁∈ ee₁ e₁' →
```

At the innermost level, the host-side rule receives all eleven objects and produces the extension fact, which is transported into the innermost subAt clause. The nesting of introductions mirrors the nesting of the quantified clause.

```agda
          subAt-in (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)) (ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ)
            (λ c₂ yb s₂ e₂ e₂∈ ee₂ e₂' →
              g a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂')))
```

For an unbounded quantifier, the payload `r` is the child formula code. A matching child key has the form `c₁=(ar',r)`, where `ar'` is the successor of the outer arity `A`, and `(c₁,ya)` belongs to the table. From these data, `qu-out` returns three hidden witnesses and an `Ext` fact for the outer value `yc`. In that extension fact, `ya` supplies the child satisfaction set used by the quantified body; `ya` itself is not the set being characterized.

```agda
  qu-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → ⟨ δ ⊨ R.quRel q ⟩
         → (c₁ ya ar' : S) → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A
         → ∥ Σ[ s ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ] Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q) ∥₁
  qu-out q h c₁ ya ar' mem e es =
    ∣ container e'S c₁ ya refl .fst , container c₁ ar' r e .fst , e'S
```

The three witnesses have distinct roles. `e'S` is an actual member of `T` realizing the pair `(c₁,ya)`; one container witnesses that pair, and the other witnesses `c₁=(ar',r)`. The general successor-arity reader already knows how to combine these witnesses with `ar'=suc A` and then expose the innermost extension fact.

```agda
    , subSucAt-out (sh 12 T) i9 i3 (extB i6 i14 (R.quBody q)) δ h c₁ ya ar' mem e es ∣₁
    where
    e'S : S
    e'S = down (lookup (sh 12 T) δ) (pr (fst c₁) (fst ya)) mem
```

Conversely, suppose every actual table member `e'=(c₁,ya)` whose key satisfies `c₁=(ar',r)` and `ar'=suc A` yields the required `Ext` fact, for every choice of the two pair containers. This universal premise is strong enough to rebuild the bounded structure of `quRel`. It concerns all matching entries and does not presume that the child value `ya` is unique.

```agda
  qu-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
           → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A
           → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q))
        → ⟨ δ ⊨ R.quRel q ⟩
```

No additional payload decomposition is needed for an unbounded quantifier: its payload `r` already is the child formula code. Consequently the general converse for a successor-arity subvalue has exactly the premise and conclusion required by `quRel`. Applying it once reconstructs the whole relation while preserving the universal reading over all matching table entries.

```agda
  qu-in q g = subSucAt-in (sh 12 T) i9 i3 (extB i6 i14 (R.quBody q)) δ g
```

The bounded-quantifier payload has two syntactic components: the bound term code `t` and the child formula code `a`, so `r=(t,a)`. The child key is `c₁=(ar',a)` at successor arity, and its table value is `ya`. The four truncated witnesses record the payload pair, the child table member, and the two relevant pair decompositions. The resulting `Ext` fact characterizes the outer value `yc`; inside its body, the term code is evaluated and its value bounds the quantification.

```agda
  bq-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
         → (c : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.bqRel q c ⟩
         → (t a c₁ ya ar' : S) → Rv ≡ pr (fst t) (fst a)
         → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
         → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ]
```

The proof packages exactly four witnesses: a container for `r=(t,a)`, a container and an actual table member for `(c₁,ya)`, and a container for `c₁=(ar',a)`. After `useBoth` opens the payload, `subSucAt-out` reads the child value at successor arity. The environment supplied to `Ext` adds nine local slots to the twelve-slot frame, and `Ext` itself places the candidate encoded environment `z` in one further head slot, matching the arity of `bqBody`.

```agda
             Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c) ∥₁
  bq-out q c h t a c₁ ya ar' er mem e es =
    ∣ container r t a er .fst , container e'S c₁ ya refl .fst , container c₁ ar' a e .fst , e'S ,
      subSucAt-out (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c)) δ15
        (useBoth i3 δ t a er (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c))) h)
```

Opening the payload extends the original frame by three slots: the child formula code `a`, the bound term code `t`, and a container witnessing `r=(t,a)`. This is the environment `δ15`. The notation records a fifteen-slot prefix over the original `m`-environment because `δ` already contained the twelve common frame slots.

```agda
        c₁ ya ar' mem e es ∣₁
    where
    δ15 : S ^ (15 + m)
    δ15 = a ∷ t ∷ container r t a er .fst ∷ δ
    e'S : S
```

The hypothesis `mem` is membership of the underlying pair `(c₁,ya)` in the table set. Applying `down` at the shifted table slot realizes that proof as `e'S : S`, an actual table element with the required underlying set. This realization is local to the proof; it does not choose a child value from totality.

```agda
    e'S = down (lookup (sh 15 T) δ15) (pr (fst c₁) (fst ya)) mem
```

The converse premise ranges over nine objects because it must accept every realization of the payload and child-table decompositions. Here `s₁` is a pair container for the table member, while `s'` is a container for the successor-arity child key; neither is the semantic witness bound by the quantified formula. Given the membership and pair equations, the premise supplies the `Ext` fact for `yc` and thereby determines the bounded relation locally.

```agda
  bq-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → (c : ∀ {j} → Formula S j → Formula S j → Formula S j)
        → ((t a s c₁ ya ar' s₁ s' e' : S) → Rv ≡ pr (fst t) (fst a)
           → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
           → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
```

To rebuild `bqRel`, `bothAll-in` first handles every decomposition `r=(t,a)` of the constructor payload. At that extended environment, `subSucAt-in` handles every table entry for the child key `(suc A,a)`. The supplied rule then proves the exact extension condition for `yc`; the semantic bound value itself is quantified later inside `bqBody`, where `tmIs` relates it to the term code `t`.

```agda
           → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c))
        → ⟨ δ ⊨ R.bqRel q c ⟩
  bq-in q c g = bothAll-in i3 (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c))) δ
    (λ t a s s∈ t∈ a∈ er →
      subSucAt-in (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c)) (a ∷ t ∷ s ∷ δ)
```

At the innermost stage all structural obligations have become explicit: the payload is `(t,a)`, the child table member is `(c₁,ya)`, its key is `(ar',a)`, and `ar'` is the successor of `A`. These are exactly the hypotheses of the assumed rule `g`, so its extension fact closes the successor-arity subvalue clause. No assertion about the uniqueness of `ya` is used in this reconstruction.

```agda
        (λ c₁ ya ar' s₁ s' e' e'∈ ee e es → g t a s c₁ ya ar' s₁ s' e' er e'∈ ee e es))
```

For an atomic formula, `t` and `u` are the two term codes stored in the payload, not their semantic values. Opening `r=(t,u)` contributes one pair container and leaves an `Ext` fact for the outer table value `yc`. The formula `atomBody` evaluated there will separately quantify candidate values of the two terms, verify them with `tmIs`, and apply the chosen atomic relation.

```agda
  atom-out : (rel : Formula S (18 + m)) → ⟨ δ ⊨ R.atomRel rel ⟩
           → (t u : S) → Rv ≡ pr (fst t) (fst u)
           → ∥ Σ[ s ∈ S ] Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel) ∥₁
  atom-out rel h t u er = ∣ container r t u er .fst , useBoth i3 δ t u er (extB i3 i11 (R.atomBody rel)) h ∣₁
```

Conversely, assume the extension condition can be proved for every decomposition of the payload into term codes `t` and `u` and every accompanying pair container. The bounded-universal introduction reconstructs that payload decomposition and hence the atomic relation. The later existential choices of actual term values remain inside `atomBody`; they are not parameters of `atom-in`.

```agda
  atom-in : (rel : Formula S (18 + m))
          → ((t u s : S) → Rv ≡ pr (fst t) (fst u) → Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel))
          → ⟨ δ ⊨ R.atomRel rel ⟩
  atom-in rel g = bothAll-in i3 (extB i3 i11 (R.atomBody rel)) δ (λ t u s s∈ t∈ u∈ er → g t u s er)
```

## Bridging clauses to semantic satisfaction

The relation readings are complete: each constructor's clause has been converted into its extension fact, and each extension fact into its clause. The chapter now turns to the bridge that connects these object-language relations to the meta-level satisfaction semantics.

```agda
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat; Sat-mem; cond )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
import L.Coding.SatisfactionBridge {ℓ} lem as Semantic
open import Cubical.Data.Nat using ( znots; snotz )
```

The bridge module is parameterized by a set `W` of the hierarchy whose members form the constant alphabet of the internal language. The definability and semantic modules are opened at `W`, so that formulas over the alphabet `Ab` can be interpreted in the small model carried by `W`.

```agda
module Bridge (W : S) where
  open Alphabet W
  private
    module DB = Semantic.DB W
    module Sem = Semantic.SemB W
```

The small model's satisfaction judgment is renamed to `⊨ᴮ` and its term valuation to `⟦_⟧ᴮ`, so the bridge can distinguish them from the ambient-hierarchy satisfaction `⊨` used earlier in the chapter.

```agda
    open Sem.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```

The meta-level meaning of a formula `ψ` at a meta-level environment `δ` is the satisfaction of the constant-relabeled formula in the small model carried by `W`. This is the target semantics that the bridges will relate to the object-language table entries.

```agda
    Meaning : ∀ {n} → Formula Ab n → DB.SM ^ n → hProp (ℓ-suc ℓ)
    Meaning ψ δ = δ ⊨ᴮ mapFo DB.ι ψ
```

The underlying set `Wv` is the carrier over which the small-model quantifiers range. Keeping it separate from the presentation `W : S` matters in the later bridges: object-language membership uses the set `Wv`, while constructibility evidence remains in the second component of `W`. Thus the bridges quantify over members of the fixed model, not over every constructible set.

```agda
  private
    Wv = fst W
```

The map `toS` relabels every constant of a formula over the alphabet `Ab` into the corresponding constant of the structure `S`, producing a formula over `S` that can be judged by the ambient satisfaction.

```agda
  toS : ∀ {n} → Formula Ab n → Formula S n
  toS = mapFo (asConst W)
```

The constructible satisfaction set `SatW ψ` collects the coded environments that satisfy the relabeled formula. It is an element of `L`, being the output of the internal recursion that defines satisfaction.

```agda
  SatW : ∀ {n} → Formula Ab n → S
  SatW ψ = Sat W (toS ψ)
```

The outward reading of membership in `SatW ψ` follows from the membership specification of the internal satisfaction: a member of `SatW ψ` is a coded environment that lies in the environment set at the correct arity and satisfies the relabeled formula's condition.

```agda
  Sat-out : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩
          → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩
  Sat-out ψ z h = subst ⟨_⟩ (Sat-mem W (toS ψ) z) h
```

The inward direction starts from membership in the correct environment set together with the recursive condition, transports that pair backward along `Sat-mem`, and obtains membership in `SatW ψ`. Thus `Sat-out` and `Sat-in` are exactly the two transports supplied by the membership specification; they require no additional semantic hypothesis.

```agda
  Sat-in : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩
         → ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩
  Sat-in ψ z hz hc = subst ⟨_⟩ (sym (Sat-mem W (toS ψ) z)) (hz , hc)
```

The lemma `extension-path` turns a pointwise path of truth values into an exact extension theorem for `SatW ψ`. For each encoded environment `z`, its premise identifies the recursive condition `cond W (toS ψ)` with the target proposition `P z`. Using the two directions of `Sat-mem`, the conclusion says that the members of `SatW ψ` are exactly the members of `envSet W n` satisfying `P`; it neither decodes `z` nor chooses a representative environment vector.

```agda
  private
    extension-path : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
                   → ((z : S) → ((z ∷ []) ⊨ cond W (toS ψ)) ≡ P z)
                   → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)
    extension-path ψ P e =
```

The outward direction reads the two components of membership in `SatW ψ` through `Sat-out` and transports the condition along the pointwise equality. The inward direction transports the property back and applies `Sat-in`. Both directions use only the pointwise equality, not any choice of representatives.

```agda
        (λ z hz → Sat-out ψ z hz .fst , subst ⟨_⟩ (e z) (Sat-out ψ z hz .snd))
      , (λ z hz hp → Sat-in ψ z hz (subst ⟨_⟩ (sym (e z)) hp))
```

For falsity, the target property has no inhabitants for any `z`. If `z` belonged to `SatW ⊥̇`, `Sat-out` would expose the impossible satisfaction of falsity; conversely, an assumed proof of that impossible property eliminates the candidate immediately. The remaining component merely records that every hypothetical member would have the correct arity, so `botBridge` gives the empty extension inside `envSet W n`.

```agda
  botBridge : (n : ℕ) {k : ℕ} (env : S ^ k)
            → ExtFact (fst (SatW (⊥̇ {n = n}))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ ⊥̇ ⟩)
  botBridge n env = (λ z hz → Sat-out ⊥̇ z hz .fst , Sat-out ⊥̇ z hz .snd) , (λ z hz b → Empty.rec* b)
```

Assume slots `ya` and `yb` of `env` contain the underlying satisfaction sets of `a` and `b`. The conjunction bridge then characterizes `SatW (a ∧̇ b)` as the encoded environments `z` belonging to both child sets. Since `z` is prepended before the body is evaluated, the old slots are addressed as `suc ya` and `suc yb`, while `i0` names `z`; this shift is exactly the host `Fin` boundary recorded in the displayed formula.

```agda
  andBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
            → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
            → ExtFact (fst (SatW (a ∧̇ b))) (fst (envSet W n))
                (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)) ⟩)
  andBridge a b env ya yb qa qb = extension-path (a ∧̇ b)
```

For conjunction, the pointwise path compares two descriptions of the same candidate environment `z`. The recursive condition says that `z` belongs to both `SatW a` and `SatW b`; transporting those two memberships along `qa` and `qb` gives exactly the two object-language membership atoms in the clause body. No child environment is decoded at this step.

```agda
    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⊓ (fst z ∈ sym qb i))
```

The disjunction bridge gives an exact extension description. An environment belongs to `SatW (a ∨̇ b)` exactly when it lies in `envSet W n` and, after being placed at the head of the clause environment, satisfies the object-language disjunction saying that it belongs to the value of `a` or to the value of `b`.

```agda
  orBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
           → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
           → ExtFact (fst (SatW (a ∨̇ b))) (fst (envSet W n))
               (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)) ⟩)
  orBridge a b env ya yb qa qb = extension-path (a ∨̇ b)
```

The pointwise comparison for disjunction transports membership of the same `z` along the two slot equations. Its two alternatives are membership in `SatW a` and membership in `SatW b`; the object-language disjunction records precisely that alternative, without producing an additional environment witness.

```agda
    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⊔ (fst z ∈ sym qb i))
```

The implication bridge likewise characterizes `SatW (a ⇒̇ b)` inside the environment set. At a candidate environment `z`, its clause body says that membership of `z` in the value of the antecedent entails membership of that same `z` in the value of the consequent.

```agda
  impBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
            → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
            → ExtFact (fst (SatW (a ⇒̇ b))) (fst (envSet W n))
                (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)) ⟩)
  impBridge a b env ya yb qa qb = extension-path (a ⇒̇ b)
```

The required path is pointwise: `qa` and `qb` rename the antecedent and consequent value slots as `SatW a` and `SatW b`. Transporting along those equations turns the object-language implication into the recursive condition for implication, with no change of environment.

```agda
    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⇒ (fst z ∈ sym qb i))
```

Both unbounded quantifier bodies range first over the carrier named by `wi`. The existential body asks for some carrier member `x`, while the universal body treats every such `x`; in either case an inner bounded existential chooses an entry of the child value and requires it to be the graph obtained by consing `x` onto the old environment.

```agda
  quEx quAll : ∀ {k} → Fin k → Fin k → Formula S (1 + k)
  quEx wi yai = ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
  quAll wi yai = ∀̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
```

The lemma `direct-extension` isolates the argument shared by the quantifier and atom bridges. Once `z` is identified with the graph of a vector `δ`, it asks for maps in both directions between `Meaning ψ δ` and the proposed clause property `P z`; from them it proves that `SatW ψ` is exactly the part of `envSet W n` satisfying `P`. Recovery of `δ` remains truncated throughout.

```agda
  private
    direct-extension : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
      → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning ψ δ ⟩ → ⟨ P z ⟩)
      → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ P z ⟩ → ⟨ Meaning ψ δ ⟩)
      → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)
```

For the outward half, `Sat-out` first supplies membership of `z` in the environment set. The truncated recovery theorem then gives a vector `δ` and an equation identifying `z` with its graph; inside the proposition `P z`, `Sat-small-spec` changes the original membership in `SatW ψ` into `Meaning ψ δ`, and the forward hypothesis finishes the argument.

```agda
    direct-extension {n} ψ P f b = out , inn
      where
      out : (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩ → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ P z ⟩
      out z hz = Sat-out ψ z hz .fst , PT.rec (snd (P z))
        (λ { (δ , q) → f δ z q (subst ⟨_⟩ (Semantic.Sat-small-spec W ψ δ z q) hz) })
```

For the inward half, membership in the environment set again yields only a truncated pair `δ , q`. The backward hypothesis sends `P z` to `Meaning ψ δ`, and the inverse direction of `Sat-small-spec` returns membership in `SatW ψ`. This elimination is valid because the membership goal is a proposition, so no global choice of a decoding vector is made.

```agda
        (Semantic.envSet-vectors W z (Sat-out ψ z hz .fst))
      inn : (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩ → ⟨ P z ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩
      inn z hz hp = PT.rec (snd (fst z ∈ fst (SatW ψ)))
        (λ { (δ , q) → subst ⟨_⟩ (sym (Semantic.Sat-small-spec W ψ δ z q)) (b δ z q hp) })
        (Semantic.envSet-vectors W z hz)
```

The lemma `child` aligns the encoded and semantic views of one bound variable. If the old coded environment is the graph of `δ` and the named child value is `SatW a`, then saying that some member of that child value is the graph obtained by consing `x` onto the old environment is propositionally equal to `Meaning a (x ∷ δ)`.

```agda
    child : ∀ {n k} (a : Formula Ab (suc n)) (δ : DB.SM ^ n) (x : DB.SM)
      (γ : S ^ k) (zi yai : Fin k) → fst (lookup zi γ) ≡ Semantic.graph W δ
      → fst (lookup yai γ) ≡ fst (SatW a)
      → ((Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)))
        ≡ Meaning a (x ∷ δ)
```

The proof is a pair of implications joined by `⇔toPath`. The outward direction consumes the truncated witness of the bounded existential: an entry of the child value together with evidence from `consAtL` that this entry is the graph obtained by consing `x` onto the old environment.

```agda
    child a δ x γ zi yai qz qa = ⇔toPath out inn
      where
      out : ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
          → ⟨ Meaning a (x ∷ δ) ⟩
      out = PT.rec (snd (Meaning a (x ∷ δ))) (λ { (e , he , hc) →
```

In the outward direction, the bounded existential is eliminated into the proposition `Meaning a (x ∷ δ)`. The cons clause and the equation for the old graph identify its witness `e` with the graph of `x ∷ δ`; after `qa` turns `e`'s membership into membership in `SatW a`, `Sat-small-spec` yields the desired semantic satisfaction.

```agda
        subst ⟨_⟩ (Semantic.Sat-small-spec W a (x ∷ δ) e
          (Semantic.consAtL-out W δ x (e ∷ Semantic.intoL W x ∷ γ) i0 i1 (sh 2 zi) qz refl hc))
          (subst (λ X → ⟨ fst e ∈ X ⟩) qa he) })
      inn : ⟨ Meaning a (x ∷ δ) ⟩
          → ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
```

The inward direction builds the canonical extension environment `envFor W (x ∷ δ)`. Reading the small-spec path backward turns the semantic satisfaction into membership of this environment in `SatW a`; `consAtL-in` then proves that the same environment has the required graph-extension relation to the old one.

```agda
      inn h = ∣ Semantic.envFor W (x ∷ δ)
        , subst (λ X → ⟨ fst (Semantic.envFor W (x ∷ δ)) ∈ X ⟩) (sym qa)
          (subst ⟨_⟩ (sym (Semantic.Sat-small-spec W a (x ∷ δ) (Semantic.envFor W (x ∷ δ))
            (Semantic.envFor-graph W (x ∷ δ)))) h)
        , Semantic.consAtL-in W δ x (Semantic.envFor W (x ∷ δ) ∷ Semantic.intoL W x ∷ γ)
```

The remaining arguments to `consAtL-in` supply the old graph equation `qz`, the reflexive identification of the new head `x`, and `envFor-graph` for the extended vector. These data close the inward witness and complete the equivalence.

```agda
            i0 i1 (sh 2 zi) qz refl (Semantic.envFor-graph W (x ∷ δ)) ∣₁
```

The existential bridge is the first quantifier result: membership in the internal value of `∃̇ a` over the environment set is the same as satisfying the bounded-existential shape `quEx` over the carrier, with the two slot equations naming the carrier and the child value.

```agda
  exBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : S ^ k) (wi yai : Fin k)
           → fst (lookup wi γ) ≡ Wv → fst (lookup yai γ) ≡ fst (SatW a)
           → ExtFact (fst (SatW (∃̇ a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ γ) ⊨ quEx wi yai ⟩)
  exBridge a γ wi yai qw qa = direct-extension (∃̇ a) (λ z → (z ∷ γ) ⊨ quEx wi yai)
    (λ δ z qz → PT.map (λ { (x , h) → Semantic.intoL W x
```

For the existential bridge, `direct-extension` leaves only the two translations supplied by `child`. From semantic satisfaction, a truncated model element `x` is embedded into `L` and becomes the outer bounded witness; conversely, an object-language witness in the named carrier is turned into an element of the restricted model and then read through `child`. Both transformations stay under propositional truncation.

```agda
      , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x)
      , subst ⟨_⟩ (sym (child a δ x (z ∷ γ) i0 (suc yai) qz qa)) h }))
    (λ δ z qz → PT.map (λ { (x , hx , h) → (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
      , subst ⟨_⟩ (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
        (z ∷ γ) i0 (suc yai) qz qa) h }))
```

The universal bridge states the same extensional fact for `∀̇ a`: the internal value contains an environment exactly when every carrier member, consed onto the environment, satisfies the child formula.

```agda
  allBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : S ^ k) (wi yai : Fin k)
            → fst (lookup wi γ) ≡ Wv → fst (lookup yai γ) ≡ fst (SatW a)
            → ExtFact (fst (SatW (∀̇ a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ γ) ⊨ quAll wi yai ⟩)
  allBridge a γ wi yai qw qa = direct-extension (∀̇ a) (λ z → (z ∷ γ) ⊨ quAll wi yai)
    (λ δ z qz h x hx → subst ⟨_⟩
```

In the forward map required by `direct-extension`, an arbitrary object-level member of the named carrier is converted to a restricted-model element, the semantic universal hypothesis is applied to it, and `child` is read from semantic satisfaction back to the encoded extension clause. In the reverse map, a restricted-model element is embedded into the carrier, the encoded universal is applied, and `child` is read outward to recover semantic satisfaction.

```agda
      (sym (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (z ∷ γ) i0 (suc yai) qz qa))
      (h (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)))
    (λ δ z qz h x → subst ⟨_⟩ (child a δ x (z ∷ γ) i0 (suc yai) qz qa)
      (h (Semantic.intoL W x) (subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x))))
```

The bounded quantifiers are stated in the object language with three nested bounded layers: the value of the bounding term, a member of the carrier inside it, and the extension entry, in the same order for both quantifiers.

```agda
  bqAll bqEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (1 + k)
  bqAll wi ti yai N0i N1i =
    ∀̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))
      ⇒̇ ∀̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ⇒̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
  bqEx wi ti yai N0i N1i =
```

The existential form conjoins the three layers; the universal form nests them as implications. The bounding term's value is read by its own term clause, and the innermost clause uses the same graph-extension equation as in the unbounded case.

```agda
    ∃̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))
      ∧̇ ∃̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ∧̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
```

The semantic value of a term is obtained by mapping each constant from the alphabet of members of `W` into the restricted model and then evaluating the resulting term at `δ`. Constants are interpreted by the embedding `DB.ι`, while variables are read directly from the corresponding positions of `δ`; set-coded numerals belong to the later representation of variable indices, not to this evaluation function.

```agda
  private
    value : ∀ {n} → Term Ab n → DB.SM ^ n → DB.SM
    value t δ = ⟦ mapTm DB.ι t ⟧ᴮ δ
```

For a constant term, `term-out` eliminates the truncated `TmIsV` evidence into an equality of sets. In the constant branch, injectivity of the pair code compares the second components and identifies the proposed value with the constant; the variable-shaped branch would equate the distinct tags `# 0` and `# 1` and is therefore impossible.

```agda
    term-out : ∀ {n} (t : Term Ab n) (δ : DB.SM ^ n) (z v : S)
      → fst z ≡ Semantic.graph W δ → TmIsV (ct t) (fst z) (fst v)
      → fst v ≡ fst (value t δ)
    term-out (con q) δ z v qz = PT.rec (setIsSet _ _)
      (λ { (inl e) → sym (pr-inj e .snd)
```

For a variable term, the constant-shaped branch is ruled out by the same tag distinction. In the variable-shaped branch, pair injectivity identifies the stored index with the numeral of `i`; the equation `qz` moves its membership into the canonical graph, and `lookup-spec` then says that the proposed value is exactly the `i`th entry of `δ`. The truncation is eliminated only into this propositional equality.

```agda
         ; (inr (i , e , _)) → Empty.rec (znots (#-inj′ {0} {1} (pr-inj e .fst))) })
    term-out (var i) δ z v qz = PT.rec (setIsSet _ _)
      (λ { (inl e) → Empty.rec (snotz (#-inj′ {1} {0} (pr-inj e .fst)))
         ; (inr (j , e , hp)) → subst ⟨_⟩ (lookup-spec (Semantic.values W δ) i (fst v))
             (subst2 (λ a E → ⟨ pr a (fst v) ∈ E ⟩) (sym (pr-inj e .snd)) qz hp) })
```

The converse lemma reconstructs `TmIsV` from the actual semantic value. For a constant, the supplied equality is reversed and transported through the pair constructor with tag `# 0`, producing the constant-shaped alternative under propositional truncation.

```agda
    term-in : ∀ {n} (t : Term Ab n) (δ : DB.SM ^ n) (z v : S)
      → fst z ≡ Semantic.graph W δ → fst v ≡ fst (value t δ)
      → TmIsV (ct t) (fst z) (fst v)
    term-in (con q) δ z v qz e = ∣ inl (cong (pr (# 0)) (sym e)) ∣₁
    term-in (var i) δ z v qz e = ∣ inr (# (toℕ i) , refl
```

For a variable, the witness uses the numeral `# (toℕ i)` as its stored index. The supplied equality identifies the proposed value with the `i`th semantic entry; `lookup-spec` turns that equality into membership of the corresponding pair in the canonical graph, and transport backward along `qz` places the pair in the given coded environment.

```agda
      , subst (λ E → ⟨ pr (# (toℕ i)) (fst v) ∈ E ⟩) (sym qz)
          (subst ⟨_⟩ (sym (lookup-spec (Semantic.values W δ) i (fst v))) e)) ∣₁
```

The bounded-quantifier module fixes the bounding term, the subformula, five slots, and five equations: the carrier, the term's coding, the subformula's value, and the two numeral slots, all read at a shared context.

```agda
  module BqBridge {n : ℕ} (t : Term Ab n) (a : Formula Ab (suc n)) {k : ℕ} (Γ : S ^ k)
    (wi ti yai N0i N1i : Fin k)
    (qw : fst (lookup wi Γ) ≡ Wv) (qt : fst (lookup ti Γ) ≡ ct t) (qa : fst (lookup yai Γ) ≡ fst (SatW a))
    (q0 : fst (lookup N0i Γ) ≡ # 0) (q1 : fst (lookup N1i Γ) ≡ # 1) where
```

The remaining proof must connect the object-language term clause used by the bounded quantifier with the semantic term value just established. The local lemmas keep that connection at the fixed slots and equations of `BqBridge`, so every later quantifier argument uses the same carrier, term code, child value, and numeral tags.

```agda
    private
```

If the object-language term clause holds at `v ∷ z ∷ Γ`, `tmIs-out` first reads it as `TmIsV` for the code occupying the term slot. Transport along `qt` then replaces that slot value by the actual code `ct t`, yielding the representation-level statement needed by `term-out`.

```agda
      tmOut : (z v : S) → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩
            → TmIsV (ct t) (fst z) (fst v)
      tmOut z v h = subst (λ u → TmIsV u (fst z) (fst v)) qt
        (tmIs-out (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1 h)
```

Conversely, a `TmIsV` statement for `ct t` is transported backward along `qt` and passed to `tmIs-in`. The result is precisely the object-language term clause at `v ∷ z ∷ Γ`, so the bridge can move between the coded clause and semantic term evaluation in either direction.

```agda
      tmIn' : (z v : S) → TmIsV (ct t) (fst z) (fst v)
            → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩
      tmIn' z v h = tmIs-in (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1
        (subst (λ u → TmIsV u (fst z) (fst v)) (sym qt) h)
```

For a semantic environment `δ`, `bound δ` is the value of the bounding term embedded back into `L`. It serves as the canonical witness for the outer value slot of the coded bounded quantifier, and its members are the elements over which the bounded formula ranges.

```agda
      bound : DB.SM ^ n → S
      bound δ = Semantic.intoL W (value t δ)
```

The bound belongs to the carrier: the value's second component is its membership in the carrier, transported along the carrier's naming equation.

```agda
      bound∈W : (δ : DB.SM ^ n) → ⟨ fst (bound δ) ∈ fst (lookup wi Γ) ⟩
      bound∈W δ = subst (λ X → ⟨ fst (value t δ) ∈ X ⟩)
        (sym qw) (snd (value t δ))
```

When `z` is the graph of `δ`, the underlying set of `bound δ` is definitionally the underlying set of the semantic value of `t`, so reflexivity supplies the equality required by `term-in`. The result is `TmIsV (ct t) (fst z) (fst (bound δ))`, certifying that the chosen bound represents the coded term's value at the encoded environment.

```agda
      bound-term : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ
                 → TmIsV (ct t) (fst z) (fst (bound δ))
      bound-term δ z qz = term-in t δ z (bound δ) qz refl
```

The representation-level certificate from `bound-term` is then converted by `tmIn'` into the object-language `tmIs` formula at the exact shifted slots used by the bounded-quantifier body. Thus the canonical semantic bound can be inserted into that body's outer quantified layer.

```agda
      bound-read : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ
                 → ⟨ (bound δ ∷ z ∷ Γ)
                     ⊨ tmIs (suc (suc ti)) i1 i0
                         (suc (suc N0i)) (suc (suc N1i)) ⟩
      bound-read δ z qz = tmIn' z (bound δ) (bound-term δ z qz)
```

For the forward half of the bounded universal bridge, consider an arbitrary candidate value `v` satisfying the term clause and an arbitrary carrier member `x` lying in `v`. The lemma `term-out` identifies the underlying set of `v` with the underlying set of the actual semantic value of `t`, so membership of `x` transports to the semantic bound. The universal semantic hypothesis gives the child's truth, and `child` converts it back to the encoded extension clause.

```agda
    allInBridge : ExtFact (fst (SatW (∀̇∈ t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i ⟩)
    allInBridge = direct-extension (∀̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i)
      (λ δ z qz h v hv ht x hx hxv → subst ⟨_⟩
        (sym (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
          (v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa))
```

For the reverse half, an arbitrary restricted-model element `x` lying in the semantic bound must satisfy the child. The coded universal is instantiated with the canonical value `bound δ`, using `bound∈W` and `bound-read`, and with the embedded element `intoL W x`, using its carrier membership and the assumed bound membership. Reading `child` outward then gives `Meaning a (x ∷ δ)`.

```agda
        (h (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
          (subst (λ V → ⟨ fst x ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv)))
      (λ δ z qz h x hx → subst ⟨_⟩
        (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)
        (h (bound δ) (bound∈W δ) (bound-read δ z qz)
```

The last argument is exactly the hypothesis that `x` lies in the semantic value of the bounding term. Supplying it completes the universal verifier for every such `x`, and hence completes the reverse implication required by `direct-extension`.

```agda
          (Semantic.intoL W x) (subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x)) hx))
```

The bounded existential bridge states the same extensional fact for `∃̇∈ t a`: membership in the internal value is equivalent, within the environment set, to satisfaction of the three-layer bounded-existential formula over the carrier.

```agda
    exInBridge : ExtFact (fst (SatW (∃̇∈ t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i ⟩)
    exInBridge = direct-extension (∃̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i)
      (λ δ z qz → PT.map (λ { (x , hx , h) → bound δ
        , bound∈W δ
        , bound-read δ z qz
```

From a semantic witness `x` for the bounded existential, the forward map chooses the canonical outer value `bound δ`, supplies its carrier membership and term certificate, and embeds `x` as the inner carrier witness. Its membership in the semantic bound is retained, while `child` read backward produces the required encoded extension witness. Every existential witness remains under propositional truncation.

```agda
        , ∣ Semantic.intoL W x , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x) , hx
            , subst ⟨_⟩ (sym (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)) h ∣₁ }))
      (λ δ z qz → PT.rec squash₁ (λ { (v , hv , ht , h) → PT.map
        (λ { (x , hx , hxv , hc) → (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
          , subst (λ V → ⟨ fst x ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv
```

In the reverse map, the outer truncated witness supplies a candidate term value `v`, and the inner one supplies a carrier member `x` lying in `v` together with an encoded child extension. Reading the term clause outward identifies the underlying set of `v` with the underlying set of the actual semantic bound. That equality transports `x`'s membership to the true bound, and `child` transports the encoded child evidence to semantic satisfaction.

```agda
          , subst ⟨_⟩ (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx)
              (v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa) hc }) h }))
```

The atomic body binds two values, not three: a carrier element `v` proposed as the value of `t`, and a carrier element `x` proposed as the value of `u`. It then conjoins the two `tmIs` clauses with the given relation formula `rel`, evaluated in the context `x ∷ v ∷ z ∷ Γ`; the coded environment `z` is already free, and `rel` is a formula rather than a bound entry.

```agda
  atomEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (3 + k) → Formula S (1 + k)
  atomEx wi ti ui N0i N1i rel =
    ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc wi)))
      (tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i)
        ∧̇ (tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ∧̇ rel)))
```

`AtomBridge` abstracts the common proof for membership and equality atoms. The terms `t` and `u` and the five slot equations determine how their codes and the tags `# 0`, `# 1` are read; the parameters `op`, `R`, and `rel` then specify the meta-level atom, its ambient binary relation, and the object-language formula that represents that relation.

```agda
  module AtomBridge {n : ℕ} (t u : Term Ab n) {k : ℕ} (Γ : S ^ k)
    (wi ti ui N0i N1i : Fin k)
    (qw : fst (lookup wi Γ) ≡ Wv) (qt : fst (lookup ti Γ) ≡ ct t) (qu : fst (lookup ui Γ) ≡ ct u)
    (q0 : fst (lookup N0i Γ) ≡ # 0) (q1 : fst (lookup N1i Γ) ≡ # 1)
    (op : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j)
```

The agreement hypothesis states the exact interface between `rel` and `R` at the three newly prepended entries. Satisfaction of `rel` in `x ∷ v ∷ z ∷ Γ` yields `R (fst v) (fst x)`, and a proof of that relation reconstructs satisfaction of `rel`. Thus the bridge may use an arbitrary representing formula only when both directions are supplied.

```agda
    (R : V ℓ → V ℓ → Type (ℓ-suc ℓ))
    (rel : Formula S (3 + k))
    (agree : (z v x : S) → (⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩ → R (fst v) (fst x))
                           × (R (fst v) (fst x) → ⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩))
    (cnd-out : (δ : DB.SM ^ n) → ⟨ Meaning (op t u) δ ⟩ → R (fst (value t δ)) (fst (value u δ)))
```

Two further hypotheses connect the chosen relation to the intended atomic semantics. The first sends `Meaning (op t u) δ` to `R` of the two evaluated term values, while the second reconstructs that meaning from the same relation. These hypotheses keep the generic bridge neutral between membership and equality.

```agda
    (cnd-in : (δ : DB.SM ^ n) → R (fst (value t δ)) (fst (value u δ)) → ⟨ Meaning (op t u) δ ⟩) where
```

The context `δ3 z v x = x ∷ v ∷ z ∷ Γ` places the proposed value of `u` at slot `i0`, the proposed value of `t` at `i1`, and the coded environment at `i2`. These are the three newly exposed entries used by the two term clauses and the relation interface; the inherited entries of `Γ` remain available to the generic formula `rel`. Only `x` and `v` are newly bound by `atomEx`, while `z` is already the free environment argument.

```agda
    private
      δ3 : (z v x : S) → S ^ (3 + k)
      δ3 z v x = x ∷ v ∷ z ∷ Γ
```

The two outward readers turn the object-language term clauses in `δ3 z v x` into `TmIsV` statements. Transport along `qt` makes the first statement concern the actual code `ct t` and proposed value `v`; transport along `qu` does the same for `ct u` and proposed value `x`. The coded environment remains the common argument `z`.

```agda
      tOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct t) (fst z) (fst v)
      tOut z v x h = subst (λ w → TmIsV w (fst z) (fst v)) qt
        (tmIs-out (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h)
      uOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct u) (fst z) (fst x)
      uOut z v x h = subst (λ w → TmIsV w (fst z) (fst x)) qu
```

The converse readers rebuild the two object-language term clauses from `TmIsV`. For `t`, the code is first transported backward along `qt` and then passed to `tmIs-in`; the declaration for `uIn` sets up the identical construction for `u` at its own value slot.

```agda
        (tmIs-out (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h)
      tIn : (z v x : S) → TmIsV (ct t) (fst z) (fst v) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩
      tIn z v x h = tmIs-in (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1
        (subst (λ w → TmIsV w (fst z) (fst v)) (sym qt) h)
      uIn : (z v x : S) → TmIsV (ct u) (fst z) (fst x) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩
```

For `u`, backward transport along `qu` changes `TmIsV (ct u) (fst z) (fst x)` into the code named by the caller's slot, and `tmIs-in` rebuilds the second object-language term clause. The bridge now has both read and write directions for each proposed term value.

```agda
      uIn z v x h = tmIs-in (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1
        (subst (λ w → TmIsV w (fst z) (fst x)) (sym qu) h)
```

The theorem `atomBridge` now asks `direct-extension` to compare the atomic semantic value with `atomEx` on every encoded environment. Its outward map must start from `Meaning (op t u) δ` and construct the two bounded value witnesses, their term clauses, and the relation formula in `x ∷ v ∷ z ∷ Γ`; the inward map will reverse the same data.

```agda
    atomBridge : ExtFact (fst (SatW (op t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩)
    atomBridge = direct-extension (op t u) (λ z → (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel) out inn
      where
      out : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning (op t u) δ ⟩
          → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩
```

The outward construction chooses the actual semantic values of `t` and `u`, embedded into `L`, as the two bounded witnesses. The second components of the restricted-model values prove their membership in the carrier; `term-in` followed by `tIn` and `uIn` supplies the two term clauses, and `cnd-out` followed by the reverse half of `agree` supplies the object-language relation. The nested witnesses are introduced under the two propositional truncations.

```agda
      out δ z qz h = ∣ v , subst (λ X → ⟨ fst v ∈ X ⟩) (sym qw) (snd (value t δ))
        , ∣ x , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd (value u δ))
          , tIn z v x (term-in t δ z v qz refl)
          , uIn z v x (term-in u δ z x qz refl)
          , agree z v x .snd (cnd-out δ h) ∣₁ ∣₁
```

The local names `v` and `x` are the embeddings into `L` of the evaluated terms `t` and `u`. They are canonical witnesses for the two value quantifiers of `atomEx`; the atomic code itself names the two term codes, while these witnesses supply their values at the particular environment `δ`.

```agda
        where
        v x : S
        v = Semantic.intoL W (value t δ)
        x = Semantic.intoL W (value u δ)
```

The reverse implication of `atomBridge` starts with a meta-level environment `δ`, a coded environment `z`, and an identification of `z` with the canonical graph of `δ`. Its remaining hypothesis says that `atomEx` holds at `z`. The outer propositionally truncated bounded existential supplies a candidate `v`, a proof `hv` that it lies in `W`, and an inner existential proof `h`. Since `Meaning (op t u) δ` is a proposition, `PT.rec` may eliminate this truncation, and then the inner one, into that target. At this point `v` is only a candidate for the value of `t`; the term-value record extracted from the inner witness will identify it with the actual semantic value.

```agda
      inn : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ
          → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩ → ⟨ Meaning (op t u) δ ⟩
      inn δ z qz = PT.rec (snd (Meaning (op t u) δ)) (λ { (v , hv , h) →
        PT.rec (snd (Meaning (op t u) δ)) (λ { (x , hx , ht , hu , hr) →
          cnd-in δ (subst2 R (term-out t δ z v qz (tOut z v x ht))
```

The inner witness supplies a second candidate `x`, its membership proof `hx : x ∈ W`, proofs `ht` and `hu` of the two term clauses, and a proof `hr` of the object-language relation. The proofs `hv` and `hx` record the bounds of the two existential quantifiers, but no further use of them is needed here. First, `agree z v x .fst` reads `hr` as `R (fst v) (fst x)`. Because `z` is the canonical graph of `δ`, `tOut` and `uOut` feed the two term-clause proofs to `term-out`, which identifies the underlying sets of `v` and `x` with those of the semantic values of `t` and `u`. Then `subst2` transports `R` along those identifications, and `cnd-in` turns the transported relation into `Meaning (op t u) δ`. This completes the atomic bridge. Downstream it is instantiated for membership and equality. In `SatSoundC`, subcode closure and structural recursion pin table entries to `SatW` by comparing extension facts; in `SatHoldsC`, decoding, prescribed table values, totality, and the stated domain let the same bridges fill all ten clauses. `SatisfactionDescription` supplies the code-domain and environment-tower facts, proves that the canonical graph `SatGraph.pairs W` satisfies `tableAt`, and packages `towerAt`, `codesAt`, and `tableAt` as `satAt`. Its `SatRead` module exposes two-way membership readers for the resulting table graph, code set, and environment tower.

```agda
            (term-out u δ z x qz (uOut z v x hu)) (agree z v x .fst hr)) }) h })
```

## Recap

The clause semantics is now tied to ordinary satisfaction in both directions. Environment graphs interpret variables, the recursive bridges handle the logical constructors, and the atomic bridge transports membership and equality through the values of their terms. The proof uses only the existence and extensional facts stated by the coded table; it does not assume that an arbitrary table relation is already functional.