One round of the VAL loop, assembled

The composite DescriptiveComplexity.Draw.RoundPh slotted into the variable machinery's matrix parameter, run end to end: the inner gates – one gate block per quantified level of the variable's pack, at the Sum.inr blocks of the VAL register, each level's verdict conjoined into its polarity's flag and a failing level continuing – the branch checkpoint dispatching on the two flags, and the matrix pass on the passing branch only.

Two levels here. DescriptiveComplexity.Draw.Data.igateBlock_hStage_pos / _neg are one level's stage in the sequencer's shape – the mirrors of the outer DescriptiveComplexity.Draw.Data.gateBlock_hStage_pos/_neg at the igateArgs pack, the failing exit continuing to the next checkpoint. DescriptiveComplexity.Draw.Data.igFs is the concrete control thread over the levels – pass or fail decided classically by the level's file-test question DescriptiveComplexity.Draw.Data.igTest – DescriptiveComplexity.Draw.Data.igs_run its run, and DescriptiveComplexity.Draw.Data.round_run the whole round at the program's own rules: inner gates, branch, matrix or skip, ending at the fold checkpoint with DescriptiveComplexity.Draw.Data.roundCtl – the matrix thread applied to the gates' output at a passing round, the gates' output alone otherwise.

No semantic hypothesis survives: the pass/fail of a level and the branch of the checkpoint are decided classically inside the statements, which is what lets the round hypothesis of DescriptiveComplexity.Draw.Data.varMachine_run be discharged for every VAL content the loop enumerates.

One inner gate block, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.igateBlock_hStage_pos {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (b : Fin dt.ko ⊕ Fin dt.ki) (flag : dt.CtlIx) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) {emb : dt.GateBlockPh → P} (wellG : (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {failPh exitPh : P} {rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i), PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.igateArgs PR.zero PR.one b flag hc hn hrd) wellG setFail failPh exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : Univ A R P dt.KIx dt.dd → Prop) (hcompat : ∀ (u : Univ A R P dt.KIx dt.dd), wellG (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ Test u) (hTest : ∀ (u : Univ A R P dt.KIx dt.dd), Test u) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.igateArgs PR.zero PR.one b flag hc hn hrd).exitSt (dt.dspTagOf PR.zero PR.one (wmBlk st.val (Tag.arg (toLex b)))) (dt.igateFam RF PR.zero PR.one b st (dt.dspTagOf PR.zero PR.one (wmBlk st.val (Tag.arg (toLex b)))) flag hc hn hrd v (dt.igateTagFam RF PR.zero PR.one b st flag hc hn hrd v f (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup) (Fin.last (dt.domNr (dt.dspTagOf PR.zero PR.one (wmBlk st.val (Tag.arg (toLex b))))))) (dt.back RF.cell PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

A passing inner gate block, entered by a dispatch: the file test passes, the witness chain reads the VAL block, the branch dispatches – on the decoded tag or the default – the domain loop runs, and the conjoining exit lands at the next checkpoint.

The concrete thread over the levels

theorem DescriptiveComplexity.Draw.Data.domN {L : FirstOrder.Language} (dt : Data L) (t : dt.X.Tag) : (dt.domPk t).n ≤ dt.eDim

The domain-sentence depth budget, packaged.

theorem DescriptiveComplexity.Draw.Data.domRd {L : FirstOrder.Language} (dt : Data L) (t : dt.X.Tag) : dt.domNr t ≤ dt.nfDim

The domain-sentence read budget, packaged.

noncomputable def DescriptiveComplexity.Draw.Data.igBlk {L : FirstOrder.Language} (dt : Data L) (vi : dt.VarIx) (ℓ : Fin (dt.nIn vi)) : Fin dt.ko ⊕ Fin dt.ki

The inner block of a quantified level: the Sum.inr block the level's point occupies.

Equations

• dt.igBlk vi ℓ = Sum.inr ⟨dt.arOf vi + ↑ℓ, ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.igFlag {L : FirstOrder.Language} (dt : Data L) (vi : dt.VarIx) (ℓ : Fin (dt.nIn vi)) : dt.CtlIx

The polarity flag of a quantified level.

Equations

• dt.igFlag vi ℓ = if dt.polOf vi (dt.arOf vi + ↑ℓ) = true then dt.existGateC else dt.allGateC

noncomputable def DescriptiveComplexity.Draw.Data.igTest {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (zero one : A) (stV : TapeStD dt A R P) (b : Fin dt.ko ⊕ Fin dt.ki) (u : Univ A R P dt.KIx dt.dd) : Prop

The file-test question of an inner gate, semantically: every cell of the gated block that the round's register holds is encoding-shaped.

Equations

• dt.igTest RF zero one stV b u = dt.wellShapedIG zero one b (dt.back RF.cell zero one ⋯ stV (RF.cell u))

noncomputable def DescriptiveComplexity.Draw.Data.igFs {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control thread across one round's inner gates: each level's machinery entered through the pack's enterIGSt – the first level resetting the two flags – its conjoining exit the next level's input where the file test passes, the fail store where it does not.

Equations

• One or more equations did not get rendered due to their size.
• dt.igFs RF zero one vi stV v f₀ 0 = f₀

theorem DescriptiveComplexity.Draw.Data.igFs_congr_scratch {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeStD dt A R P} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (vi : dt.VarIx) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.igFs RF zero one vi stV v f₀ n = dt.igFs RF zero one vi stV' v f₀ n

The inner gates are blind to the two scratch registers: every level's test reads the VAL register (igTest_congr), its dispatched tag is that register's block value, and its two loops read their background at the working cell.

noncomputable def DescriptiveComplexity.Draw.Data.igPassP {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (stV : TapeStD dt A R P) (ℓ : Fin (dt.nIn vi)) : Prop

What one level's gate is worth: the file test passed, the block value's witness one-hot at the dispatched tag, and the domain condition there. By DescriptiveComplexity.Draw.Data.igVerdict_iff_isEnc this is IsEnc of the block value, once the encoding layer relates the test's marks to the true shapes.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.igPassP_congr {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (zero one : A) (vi : dt.VarIx) {st st' : TapeStD dt A R P} (hval : st.val = st'.val) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi st ℓ ↔ dt.igPassP RF zero one vi st' ℓ

A round's pass depends on the VAL register alone. Hence at a round state (DescriptiveComplexity.Draw.Data.roundSt, which sets VAL and keeps everything else) the pass is the same proposition at every position of the spine – so a position's hp is the entry state's, and kindSemCast may carry the pack it unlocks.

The rides: what the round's machinery never writes

The two-flag characterization

theorem DescriptiveComplexity.Draw.Data.roundPass_of_flags {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (h : dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) dt.existGateC ∧ dt.ctlBit one (dt.igFs RF zero one vi stV v f₀ (dt.nIn vi)) dt.allGateC) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi stV ℓ

The branch's guard delivers the pass: with both flags set after the inner gates' thread, every quantified level passed its gate – what unlocks the round's semantic pack.

noncomputable def DescriptiveComplexity.Draw.Data.roundCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one round leaves at the fold checkpoint: the matrix thread applied to the inner gates' output at a passing round – both flags set, the round's conditional semantic pack unlocked by DescriptiveComplexity.Draw.Data.roundPass_of_flags – and the gates' output alone at a skipping one. The pack must be conditional: a garbage round holds no encodings to build one from, and its matrix never runs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.roundEndSt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : TapeStD dt A R P

The state one round leaves: the matrix runs on the passing branch only, so the round's exit state is the matrix's threaded state there and the entry state at a skipping round.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.roundEndSt_eq {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : dt.roundEndSt RF zero one vi stV v f₀ = { mir := stV.mir, tgt := (dt.roundEndSt RF zero one vi stV v f₀).tgt, sav := (dt.roundEndSt RF zero one vi stV v f₀).sav, val := stV.val, old := stV.old, new := stV.new, wk := stV.wk, bot := stV.bot, ltp := stV.ltp }

A round's exit state is its entry state with the two scratch registers rewritten – the sharpening of DescriptiveComplexity.Draw.Data.roundEndSt_fields, and what lets the VAL loop thread those two registers rather than the whole state.

noncomputable def DescriptiveComplexity.Draw.Data.roundCtlT {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi stV v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one round leaves, threaded: as DescriptiveComplexity.Draw.Data.roundCtl, with the matrix's thread taken at the states its atoms run at.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.roundCtl_congr_scratch {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} {stV stV' : TapeStD dt A R P} (h : dt.ScratchEq stV stV') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (vi : dt.VarIx) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi stV (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.roundCtl RF hord hzo vi stV v sem f₀ = dt.roundCtl RF hord hzo vi stV' v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV' ℓ) (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem ⋯ a)) f₀

A round is blind to the two scratch registers: its gates by igFs_congr_scratch, its matrix by matFs_congr_scratch.

theorem DescriptiveComplexity.Draw.Data.roundCtlT_eq_roundCtl {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {v : Univ A R P dt.KIx dt.dd → Prop} (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (vi : dt.VarIx) (stV : TapeStD dt A R P) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem zero one vi (dt.matSt vi stV v ↑a) (dt.kindOf vi a)) (f₀ : dt.CtlIx → A) : dt.roundCtlT RF hord hzo vi stV v sem f₀ = dt.roundCtl RF hord hzo vi stV v (fun (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF zero one vi stV ℓ) (a : Fin (dt.natOf vi)) => dt.kindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi a) (sem hp a)) f₀

The threaded round is the unthreaded one: the gates decide the branch off the same registers, and on the passing branch the matrix threads SAV and TARGET alone (matFsT_eq_matFs). With this the control the run produces is the control the semantic capstone (DescriptiveComplexity.Draw.Data.accVerdict_leafP) is stated at.

The inner gates' run

theorem DescriptiveComplexity.Draw.Data.igs_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) {stV : TapeStD dt A R P} {emb : dt.IGatesPh vi → P} {exitPh : P} {rEmb : (i : dt.IGatesSite vi) → dt.IGatesSh vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.IGatesSite vi) (ρ : dt.IGatesSh vi i), PR.rules (rEmb i ρ) = dt.igatesRule PR.one vi emb (dt.varArgsOf PR.zero PR.one vi).argsIG (dt.varArgsOf PR.zero PR.one vi).wellIGOf (dt.varArgsOf PR.zero PR.one vi).setFailIGOf (dt.varArgsOf PR.zero PR.one vi).enterIGSt exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (SeqPh.chk 0)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.igFs RF PR.zero PR.one vi stV v f₀ (dt.nIn vi))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) }

The inner gates' run: from the checkpoint before the first level at the marker, through every level – the file test, and either the dispatch, domain loop and conjoining exit, or the continuing fail – to the round's branch checkpoint one cell to the marker's right, the two flags spelled by the thread.

The whole round, at the program's own rules

theorem DescriptiveComplexity.Draw.Data.round_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) {v : Univ A R P dt.KIx dt.dd → Prop} {emb : dt.VarPhF vi → P} {exitPh : P} {rEmb : (i : dt.VarSiteF vi) → dt.VarShF vi i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.VarSiteF vi) (ρ : dt.VarShF vi i), PR.rules (rEmb i ρ) = dt.varRuleF PR.zero PR.one vi (dt.varArgsOf PR.zero PR.one vi) emb exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (stV : TapeStD dt A R P) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirV : stV.mir = v) (hbotV : stV.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsavV : stV.sav = v) (htgtV : stV.tgt = v) (sem : (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi stV ℓ) → (a : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi stV (dt.kindOf vi a)) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (VarPh.matrixP (RoundPh.igP (SeqPh.chk 0)))) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.mchk1) (dt.roundCtl RF hord ⋯ vi stV v sem f)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ stV) stV.val) (PR.syElt PR.blank) }

One round of the VAL loop, run: from the dispatch's landing one cell right of the marker at the inner gates' first checkpoint, the walk-back, every quantified level's gate – pass or fail, the fail continuing – the branch checkpoint on the two flags, the matrix pass on the passing branch, and the walk-back at the fold checkpoint. No semantic hypothesis: the levels' outcomes and the branch are decided classically, so the round runs at every VAL content the loop enumerates.