One variable's machinery at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstVar read at a coarse file: the gates' leg and the matrix leg of one variable's machinery, the VAL loop's thread and the capstone runs. Everything below it is already at the file, so this is the last layer before the evaluation.

noncomputable def DescriptiveComplexity.Draw.Data.ixVarGatesCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP : ℕ) : ℕ

What the gates' leg of one variable's machinery is charged: the walk-back into the sequence, the gate sequence itself, and the walk-back at the verdict checkpoint.

Equations

• dt.ixVarGatesCost A vi w wP = 1 + ((dt.ixGateCost A w wP + 2) * dt.arOf vi + 1) + 1

theorem DescriptiveComplexity.Draw.Data.ixVarGates_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w wG wP : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (TestOf : Fin (dt.arOf vi) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixVarGatesCost A vi w wP) { state := Sum.inr (PR.stElt (emb (VarPh.gatesP (SeqPh.chk 0))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk1) (dt.ixGatesFs F PR.zero PR.one hhasP vi st v (fun (ℓ : Fin (dt.arOf vi)) => Sum.inl (Fin.castLE ⋯ ℓ)) ⋯ ⋯ ⋯ tOf (dt.varArgsOf PR.zero PR.one vi).enterBlockSt f₀ (dt.arOf vi))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The gates' leg of one variable's machinery: from the dispatch's landing one cell right of the marker, the walk-back, the whole gate sequence at a gated address, and the walk-back at the verdict checkpoint.

noncomputable def DescriptiveComplexity.Draw.Data.ixFailCtl {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hhasP : F.toLayout.HasName PR.zero) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (tOf : Fin (dt.arOf vi) → dt.X.Tag) (ℓ₀ : Fin (dt.arOf vi)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after a failing gate sequence: the fail store at the failing block's entry, the flag clear.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixVarGatesFail_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w wG wP : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (TestOf : Fin (dt.arOf vi) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf vi)) (hTestLt : ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < ↑ℓ₀ → ∀ (u : I), TestOf ℓ u) {u₀ : I} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixVarGatesCost A vi w wP) { state := Sum.inr (PR.stElt (emb (VarPh.gatesP (SeqPh.chk 0))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk1) (dt.ixFailCtl F hhasP vi st tOf ℓ₀ f₀)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) }

The gates' leg at a junk address: the walk-back, the passing prefix, the failing block, and the walk-back at the verdict checkpoint – the fail store applied, the flag clear.

theorem DescriptiveComplexity.Draw.Data.ixVarBg_back {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)] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hix : IsLinOrd F.le) {v : Univ A R P dt.KIx dt.dd → Prop} {gtop : I} (htop : ∀ (y : I), F.le y gtop) (stV : TapeSt dt A R P I) (hwkV : stV.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) : dt.VarBg F PR.zero PR.one v gtop (dt.ixBack F.toLayout PR.zero PR.one ⋯ stV) stV.val

The background bundle, discharged at a boundary state: the five slot equations DescriptiveComplexity.Draw.Data.var_run's kits read are definitional in DescriptiveComplexity.Draw.Data.back, given the marker and the order facts.

theorem DescriptiveComplexity.Draw.Data.ixVarMachineFail_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w wG wP : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (TestOf : Fin (dt.arOf vi) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf vi)) (hTestLt : ∀ (ℓ : Fin (dt.arOf vi)), ↑ℓ < ↑ℓ₀ → ∀ (u : I), TestOf ℓ u) {u₀ : I} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) {rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = dt.ixBack F.toLayout PR.zero PR.one ⋯ st r) (hupd : rest' v = Function.update (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v) (dt.varArgsOf PR.zero PR.one vi).newSlot PR.zero) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (1 + dt.ixVarGatesCost A vi w wP + 1) { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixFailCtl F hhasP vi st tOf ℓ₀ ((dt.varArgsOf PR.zero PR.one vi).enterSt f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val rest' st.val) (PR.syElt PR.blank) }

The whole machinery at a junk address: entry, the failing gates, and the verdict checkpoint's clear flag routing straight to the exit with the stage slot erased – the VAL loop never entered.

noncomputable def DescriptiveComplexity.Draw.Data.ixUngatedCtl {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hhasP : F.toLayout.HasName PR.zero) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (tOf : Fin (dt.arOf vi) → dt.X.Tag) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after a completed but failing gate sequence: the whole gates' thread – every block's file test passed and every block's machinery ran – with the flag clear because some block encoded no point.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixVarMachineUngated_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (w wG wP : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (TestOf : Fin (dt.arOf vi) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf vi)), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), TestOf ℓ u) (ℓ₀ : Fin (dt.arOf vi)) (hbad : ¬((∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ₀) ∧ ExpExpansion.DomHolds (tOf ℓ₀, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))))))) (f₀ : dt.CtlIx → A) {rest' : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hoff : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), r ≠ v → rest' r = dt.ixBack F.toLayout PR.zero PR.one ⋯ st r) (hupd : rest' v = Function.update (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v) (dt.varArgsOf PR.zero PR.one vi).newSlot PR.zero) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (1 + dt.ixVarGatesCost A vi w wP + 1) { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (dt.ixUngatedCtl F hhasP vi st tOf ((dt.varArgsOf PR.zero PR.one vi).enterSt f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val rest' st.val) (PR.syElt PR.blank) }

The whole machinery at a shaped but ungated address: every block passes its file test – the total dispatch carries each block's machinery through – but some block encodes no point, its witness not one-hot at the dispatched tag or its domain sentence failing. The gates complete with the flag clear, and the verdict checkpoint routes straight to the exit with the stage slot erased – the VAL loop never entered. The third landing an arbitrary address makes, beside the gated and the shape-failing ones.

The whole variable machinery, run

noncomputable def DescriptiveComplexity.Draw.Data.ixVarCost {L : FirstOrder.Language} (dt : Data L) (A : Type) (vi : dt.VarIx) (w wP wR wK n : ℕ) : ℕ

What one variable's machinery is charged: the gates' leg, one round, the three sweeps of the entry and the exhaustion test, and then one round and two sweeps per VAL content the loop enumerates.

Equations

• dt.ixVarCost A vi w wP wR wK n = dt.ixVarGatesCost A vi w wP + dt.ixRoundCost A vi w wP wR wK + 3 * wP + 6 + (2 * wP + dt.ixRoundCost A vi w wP wR wK + 3) * n

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (m : I → Prop) : TapeSt dt A R P I

The state of one VAL-loop round: the entry state with the round's VAL content.

Equations

• dt.ixRoundSt st m = { mir := st.mir, tgt := st.tgt, sav := st.sav, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

theorem DescriptiveComplexity.Draw.Data.ixIGPassP_roundSt {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] {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (zero one : A) (vi : dt.VarIx) (st st' : TapeSt dt A R P I) (m : I → Prop) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP F zero one vi (dt.ixRoundSt st m) ℓ ↔ dt.ixIGPassP F zero one vi (dt.ixRoundSt st' m) ℓ

Two round states at the same register ask the same pass.

theorem DescriptiveComplexity.Draw.Data.ixRoundSt_val {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} (stV : TapeSt dt A R P I) : dt.ixRoundSt stV stV.val = stV

A state written with the register it already holds is itself.

theorem DescriptiveComplexity.Draw.Data.ixBack_roundSt_off {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)] {I : Type} (F : LaidFile dt A R P I) (st : TapeSt dt A R P I) {zero one : A} (m₁ m₂ : I → Prop) (r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx) (hs : s ≠ Slot.val) : dt.ixBack F.toLayout zero one ⋯ (dt.ixRoundSt st m₁) r s = dt.ixBack F.toLayout zero one ⋯ (dt.ixRoundSt st m₂) r s

Two round states' backgrounds agree off the VAL slot.

noncomputable def DescriptiveComplexity.Draw.Data.ixValCarry {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)] {I : Type} (F : LaidFile dt A R P I) (m : I → Prop) : Option I

The carry of a VAL round at a coarse file: the greatest register the mark is clear at, every register above it set – what the increment's landing phase names. A file need not have one (an empty file has none), so this is an Option; at the elementwise file it is always some.

Equations

• dt.ixValCarry F m = if h : ∃ (u : I), ¬m u ∧ ∀ (w : I), DescriptiveComplexity.WMLt F.le u w → m w then some h.choose else none

noncomputable def DescriptiveComplexity.Draw.Data.ixCarryBlk {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)] {I : Type} (F : LaidFile dt A R P I) (m : I → Prop) : Option dt.KIx

The block the carry lies in: what a round's store is indexed by.

Equations

• dt.ixCarryBlk F m = (dt.ixValCarry F m).bind F.blk

theorem DescriptiveComplexity.Draw.Data.ixValCarry_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)] {I : Type} (F : LaidFile dt A R P I) (hix : IsLinOrd F.le) {m : I → Prop} {u₀ : I} (h1 : ¬m u₀) (h2 : ∀ (w : I), WMLt F.le u₀ w → m w) : dt.ixValCarry F m = some u₀

The carry is unique, so the chosen one is the hypothesis's.

noncomputable def DescriptiveComplexity.Draw.Data.ixRoundFX {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (q : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The exit control of one VAL round, at an entry control: the inner gates' thread over the round's register, then – at a passing round only, both flags set – the matrix thread on its output.

Equations

• DescriptiveComplexity.Draw.Data.ixRoundFX F hinj hhasP heltP vi st v mV semOf q a = dt.ixRoundCtl F hinj hhasP heltP ⋯ vi (dt.ixRoundSt st (mV a)) v (semOf a) q

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFM {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) : ιV → dt.CtlIx → A

The VAL loop's entry-control thread: the fold's start at the cleared register, each round the matrix pass folded and stored at the carry's block.

Equations

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

The fold invariant of the VAL loop

theorem DescriptiveComplexity.Draw.Data.ixReadAcc_varFM {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hix : IsLinOrd F.le) (hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1) (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) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : I) => False) (hUse : ∀ (a : ιV) (u : I), mV a u → Use u) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (fG : dt.CtlIx → A) {Ps : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop} (hleaf : ∀ (a : ιV), roundLeaf vi (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) a) ↔ Ps (ixBlk (argIn dt.ko) (ixAddr elt (mV a)))) (a : ιV) (j : ℕ) (hj : j < dt.ki) : dt.readAcc PR.one (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) j ↔ accCVal (dt.polOf vi) Ps (WMSetLe tupLeLex) j (ixBlk (argIn dt.ko) (ixAddr elt (mV a)))

The VAL loop maintains the fold's contributions: at every round of the enumeration, the accumulator vector of the control thread reads the accCVal contributions of the inner quantifier prefix at the blocks of the register's address – the invariant that turns the machinery's exit verdict into the prefix's value.

theorem DescriptiveComplexity.Draw.Data.ixAccVerdict_varFM {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hix : IsLinOrd F.le) (hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1) (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) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : I) => False) (hUse : ∀ (a : ιV) (u : I), mV a u → Use u) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u) (fG : dt.CtlIx → A) {Ps : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop} (hleaf : ∀ (a : ιV), roundLeaf vi (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) a) ↔ Ps (ixBlk (argIn dt.ko) (ixAddr elt (mV a)))) : dt.accVerdict PR.one (dt.polOf vi) ((dt.varArgsOf PR.zero PR.one vi).postFold (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG aT) aT) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT)) v)) ↔ altQuantFrom (dt.polOf vi) Ps 0 (ixBlk (argIn dt.ko) (ixAddr elt (mV aT)))

The machinery's verdict is the inner prefix's value: at the exhausted register – every inner block full – the exit fold's bit is the alternating quantifier prefix over the inner blocks, applied to the matrix's value.

The leaf, discharged

theorem DescriptiveComplexity.Draw.Data.ixPostLeaf_roundFX {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} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {ιV : Type} (mV : ιV → I → Prop) [LinearOrder (dt.X.Map A)] (σ : dt.d.B.Assignment (dt.X.Map A)) (a : ιV) (wa : Fin (dt.nOf vi) → dt.X.Map A) (hENCa : ∀ (j : Fin (dt.nOf vi)), wmBlk (ixAddr elt (dt.lvSet (dt.ixRoundSt st (mV a)) vi j)) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly PR.zero PR.one (wa j)) (hOlda : ∀ (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf vi)), (dt.ixRoundSt st (mV a)).old i (ixAddr elt (dt.ixStageTgt F hhasP vi ts (have __src := dt.ixRoundSt st (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (dt.d.B.arity i))) ↔ σ i fun (k : Fin (dt.d.B.arity i)) => wa (ts k)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (q : dt.CtlIx → A) : dt.postLeaf PR.one vi (dt.ixMatFs F PR.zero PR.one hhasP vi (dt.ixRoundSt st (mV a)) v (dt.varArgsOf PR.zero PR.one vi).enterAtomSt (fun (b : Fin (dt.natOf vi)) => dt.ixMkKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) wa hENCa (dt.kindOf vi b)) q (dt.natOf vi)) ↔ qfValue (dt.matOf vi) fun (atm : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf vi)) => (matAtom? atm).elim False (MatAtom.holds σ wa)

A round's leaf is the matrix's realization: with the round's semantic pack built by ixMkKindSem from the encoded valuation, the fold's leaf after the matrix pass is the quantifier-free matrix's value at that valuation – the concrete form of the invariant's hleaf hypothesis.

theorem DescriptiveComplexity.Draw.Data.ixAccVerdict_varFM_qfValue {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} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hix : IsLinOrd F.le) (hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1) (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) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} (hlin : IsLinOrd WMLe) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) [LinearOrder (dt.X.Map A)] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : I) => False) (hUse : ∀ (a : ιV) (u : I), mV a u → Use u) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) (wOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → Fin (dt.nOf vi) → dt.X.Map A) (hENC : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) (j : Fin (dt.nOf vi)), wmBlk (ixAddr elt (dt.lvSet (dt.ixRoundSt st (mV a)) vi j)) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly PR.zero PR.one (wOf a hp j)) (hOld : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf vi)), (dt.ixRoundSt st (mV a)).old i (ixAddr elt (dt.ixStageTgt F hhasP vi ts (have __src := dt.ixRoundSt st (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (dt.d.B.arity i))) ↔ σ i fun (k : Fin (dt.d.B.arity i)) => wOf a hp (ts k)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) {Ps : (Fin dt.ki → (Fin dt.dd → A) → Prop) → Prop} (hsem : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) (b : Fin (dt.natOf vi)), semOf a hp b = dt.ixMkKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) (wOf a hp) ⋯ (dt.kindOf vi b)) (fG : dt.CtlIx → A) {Ex Al : ιV → Prop} (hEx : ∀ (a : ιV), dt.ctlBit PR.one (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) a) dt.existGateC ↔ Ex a) (hAll : ∀ (a : ιV), dt.ctlBit PR.one (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) a) dt.allGateC ↔ Al a) (hPass : ∀ (a : ιV), Ex a → Al a → ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) (hPsPass : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ), Ex a ∧ (Al a → qfValue (dt.matOf vi) fun (atm : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf vi)) => (matAtom? atm).elim False (MatAtom.holds σ (wOf a hp))) ↔ Ps (ixBlk (argIn dt.ko) (ixAddr elt (mV a)))) (hPsFail : ∀ (a : ιV), ¬(Ex a ∧ Al a) → (Ex a ↔ Ps (ixBlk (argIn dt.ko) (ixAddr elt (mV a))))) : dt.accVerdict PR.one (dt.polOf vi) ((dt.varArgsOf PR.zero PR.one vi).postFold (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG aT) aT) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT)) v)) ↔ altQuantFrom (dt.polOf vi) Ps 0 (ixBlk (argIn dt.ko) (ixAddr elt (mV aT)))

One variable's verdict, semantically: with each round's pack built by ixMkKindSem from an encoded valuation, the machinery's exit bit at the exhausted register is the alternating quantifier prefix over the inner blocks, applied to the quantifier-free matrix's realization. The remaining interface (hPs) is the well-definedness of the matrix's value as a function of the blocks alone – the encoding layer's obligation.

The threaded twins of the VAL loop's two threads

A round's exit state is its entry state unless the round's matrix ran a stage atom, which normalizes SAV and TARGET (DescriptiveComplexity.Draw.Data.ixRoundEndSt). Whether it ran at all is the gates' verdict, read off the control entering the round – so the two have to be iterated together, one pair per round, exactly as the spine's nodes are one scale up.

What is threaded is not the state but the two scratch registers (DescriptiveComplexity.Draw.Data.ixRoundEndSt_eq): every other register is the machinery's entry state's, definitionally. That is what keeps the semantic packs available – a pack reads the tape state through the levels' register sets, i.e., through the mirror and VAL alone, so one family indexed by the two registers serves every round, and it can actually be built, which a family over arbitrary states could not be.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.IxScratch {L : FirstOrder.Language} (_dt : Data L) (_A _R _P I : Type) : Type

The two registers one round of the VAL loop can change.

Equations

• _dt.IxScratch _A _R _P I = ((I → Prop) × (I → Prop))

noncomputable def DescriptiveComplexity.Draw.Data.ixVarRdSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} (st : TapeSt dt A R P I) (p : dt.IxScratch A R P I) (m : I → Prop) : TapeSt dt A R P I

The state a round is entered in: the machinery's entry state with the round's two scratch registers and the register it enumerates.

Equations

• DescriptiveComplexity.Draw.Data.ixVarRdSt st p m = { mir := st.mir, tgt := p.2, sav := p.1, val := m, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }

noncomputable def DescriptiveComplexity.Draw.Data.ixVarPairT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) : ιV → dt.IxScratch A R P I × (dt.CtlIx → A)

The VAL loop's thread: the two scratch registers beside the control, the fold's start at the cleared register, and at each cover the round's exit – the store taken against the background the round ends in.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixVarSTT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.IxScratch A R P I

The scratch family of the VAL loop.

Equations

• DescriptiveComplexity.Draw.Data.ixVarSTT F hinj hhasP heltP vi st v mV semT fG a = (DescriptiveComplexity.Draw.Data.ixVarPairT F hinj hhasP heltP vi st v mV semT fG a).1

noncomputable def DescriptiveComplexity.Draw.Data.ixVarStT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : TapeSt dt A R P I

The tape family of the VAL loop – the state each round is entered in.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFMT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The control family of the VAL loop, threaded – the twin of DescriptiveComplexity.Draw.Data.ixVarFM.

Equations

• DescriptiveComplexity.Draw.Data.ixVarFMT F hinj hhasP heltP vi st v mV semT fG a = (DescriptiveComplexity.Draw.Data.ixVarPairT F hinj hhasP heltP vi st v mV semT fG a).2

noncomputable def DescriptiveComplexity.Draw.Data.ixVarStE {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : TapeSt dt A R P I

The state one round ends in – the next round's entry state at a cover, and the loop's exit state at the top.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFXT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : dt.CtlIx → A

The exit control of one VAL round, threaded – the twin of DescriptiveComplexity.Draw.Data.ixRoundFX, at the state the round's atoms actually run at.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixVarStT_fields {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : (ixVarStT F hinj hhasP heltP vi st v mV semT fG a).wk = st.wk ∧ (ixVarStT F hinj hhasP heltP vi st v mV semT fG a).mir = st.mir ∧ (ixVarStT F hinj hhasP heltP vi st v mV semT fG a).bot = st.bot ∧ (ixVarStT F hinj hhasP heltP vi st v mV semT fG a).old = st.old ∧ (ixVarStT F hinj hhasP heltP vi st v mV semT fG a).val = mV a

The registers a round leaves alone ride the whole loop – by construction now, since only the two scratch ones are threaded.

theorem DescriptiveComplexity.Draw.Data.ixVarStE_val {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : (ixVarStE F hinj hhasP heltP vi st v mV semT fG a).val = mV a

A round leaves the register it was entered with.

theorem DescriptiveComplexity.Draw.Data.ixVarStE_new {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) : (ixVarStE F hinj hhasP heltP vi st v mV semT fG a).new = st.new

The VAL loop never touches a stage track: only the two scratch registers are threaded, so the new tracks the spine writes ride the whole loop.

theorem DescriptiveComplexity.Draw.Data.ixVarRdSt_varStE {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (fG : dt.CtlIx → A) (a : ιV) (m : I → Prop) : ixVarRdSt st ((ixVarStE F hinj hhasP heltP vi st v mV semT fG a).sav, (ixVarStE F hinj hhasP heltP vi st v mV semT fG a).tgt) m = dt.ixRoundSt (ixVarStE F hinj hhasP heltP vi st v mV semT fG a) m

A round's exit state is the next round's entry state, once the next round's register is written over it.

theorem DescriptiveComplexity.Draw.Data.ixVarSTT_bot {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (fG : dt.CtlIx → A) : ixVarSTT F hinj hhasP heltP vi st v mV semT fG a₀ = (st.sav, st.tgt)

The thread starts at the entry state.

theorem DescriptiveComplexity.Draw.Data.ixVarStT_bot {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (fG : dt.CtlIx → A) : ixVarStT F hinj hhasP heltP vi st v mV semT fG a₀ = dt.ixRoundSt st (mV a₀)

The thread starts at the entry state.

theorem DescriptiveComplexity.Draw.Data.ixVarFMT_bot {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) {a₀ : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (fG : dt.CtlIx → A) : ixVarFMT F hinj hhasP heltP vi st v mV semT fG a₀ = (dt.varArgsOf PR.zero PR.one vi).initSt fG (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st fun (x : I) => False) v)

The control thread starts at the fold's start.

theorem DescriptiveComplexity.Draw.Data.ixVarStT_covers {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) {a a' : ιV} (hlt : a < a') (hnb : ∀ (b : ιV), ¬(a < b ∧ b < a')) (fG : dt.CtlIx → A) : ixVarStT F hinj hhasP heltP vi st v mV semT fG a' = dt.ixRoundSt (ixVarStE F hinj hhasP heltP vi st v mV semT fG a) (mV a')

The tape's cover equation: the next round is entered in this round's exit state, its own register written over it.

theorem DescriptiveComplexity.Draw.Data.ixVarFMT_covers {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) {a a' : ιV} (hlt : a < a') (hnb : ∀ (b : ιV), ¬(a < b ∧ b < a')) (fG : dt.CtlIx → A) : ixVarFMT F hinj hhasP heltP vi st v mV semT fG a' = (dt.varArgsOf PR.zero PR.one vi).storeCarry (dt.ixCarryBlk F (mV a)) ((dt.varArgsOf PR.zero PR.one vi).postFold (ixVarFXT F hinj hhasP heltP vi st v mV semT fG a) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (ixVarStE F hinj hhasP heltP vi st v mV semT fG a) v)) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (ixVarStE F hinj hhasP heltP vi st v mV semT fG a) v)

The control's cover equation: the round's exit control, folded and stored at the block its increment carried.

The threaded loop is the unthreaded one

The VAL loop's rounds run at states that differ from the machinery's entry state in SAV and TARGET alone, and every control they compute is blind to that difference (DescriptiveComplexity.Draw.Data.ixRoundCtlT_eq_ixRoundCtl, DescriptiveComplexity.Draw.Data.ixRoundCtl_congr_scratch). What the threading can change is the semantic pack, since a family indexed by the scratch registers may pick different points at different registers; so the bridge is stated at a pack that is one unthreaded pack transported (ixSemCastT), which is what a reduction supplies (DescriptiveComplexity.Draw.Data.gatedSem, whose points are the address's blocks and nothing else).

theorem DescriptiveComplexity.Draw.Data.ixScratchEq_varRdSt {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} (st : TapeSt dt A R P I) (p : dt.IxScratch A R P I) (m : I → Prop) : dt.ScratchEq (ixVarRdSt st p m) (dt.ixRoundSt st m)

A round's entry state is the round state up to the two scratch registers.

noncomputable def DescriptiveComplexity.Draw.Data.ixSemCastT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) {ιV : Type} (mV : ιV → I → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (p : dt.IxScratch A R P I) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) (b : Fin (dt.natOf vi)) : dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)

One unthreaded pack, at every state a round reaches: the round's own state and the states its matrix threads all share the mirror and VAL of the round state, so ixKindSemCast carries the pack to each of them.

Equations

• DescriptiveComplexity.Draw.Data.ixSemCastT F vi st v mV sem₀ p a hp b = dt.ixKindSemCast PR.zero PR.one vi ⋯ ⋯ (dt.kindOf vi b) (sem₀ a ⋯ b)

theorem DescriptiveComplexity.Draw.Data.ixRoundCtlT_semCastT {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} (mV : ιV → I → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (hreg : ¬∃ (u : I), v = F.cell u) (p : dt.IxScratch A R P I) (a : ιV) (q : dt.CtlIx → A) : dt.ixRoundCtlT F hinj hhasP heltP ⋯ vi (ixVarRdSt st p (mV a)) v (ixSemCastT F vi st v mV sem₀ p a) q = ixRoundFX F hinj hhasP heltP vi st v mV sem₀ q a

One threaded round is the unthreaded round: a round's own state is the round state up to SAV and TARGET, its matrix threads those two further, and the pack rides along – three transports that compose to none.

theorem DescriptiveComplexity.Draw.Data.ixVarFXT_eq_roundFX {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (hreg : ¬∃ (u : I), v = F.cell u) (fG : dt.CtlIx → A) (a : ιV) : ixVarFXT F hinj hhasP heltP vi st v mV (ixSemCastT F vi st v mV sem₀) fG a = ixRoundFX F hinj hhasP heltP vi st v mV sem₀ (ixVarFMT F hinj hhasP heltP vi st v mV (ixSemCastT F vi st v mV sem₀) fG a) a

The threaded round of the VAL loop is the unthreaded one, at the state the loop's own thread produced.

theorem DescriptiveComplexity.Draw.Data.ixVarFMT_eq_varFM {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → I → Prop) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (hreg : ¬∃ (u : I), v = F.cell u) (fG : dt.CtlIx → A) (a : ιV) : ixVarFMT F hinj hhasP heltP vi st v mV (ixSemCastT F vi st v mV sem₀) fG a = ixVarFM F hinj hhasP heltP vi st v mV sem₀ fG a

The VAL loop's threaded control is its unthreaded control: round by round, ixVarFXT_eq_roundFX, the backgrounds agreeing because a round's exit state is the round state up to SAV and TARGET. This is the bridge between the control the machine's run produces and the control DescriptiveComplexity.Draw.Data.accVerdict_leafP reads.

noncomputable def DescriptiveComplexity.Draw.Data.ixVarFG {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] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) (hhasP : F.toLayout.HasName PR.zero) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) (st : TapeSt dt A R P I) (v : Univ A R P dt.KIx dt.dd → Prop) (tOf : Fin (dt.arOf vi) → dt.X.Tag) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control the gates leave, at the reduction's own budgets – what both forms of the machinery's run start their VAL loop from.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixVarMachine_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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) (st : TapeSt dt A R P I) {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (TestOf : Fin (dt.arOf vi) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → I → Prop) (hmV0 : mV a₀ = fun (x : I) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a')) (hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u) (hmir : st.mir = ixMark elt v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsav : st.sav = ixMark elt v) (htgt : st.tgt = ixMark elt v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b)) (hDom : ∀ (ℓ : Fin (dt.arOf vi)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hwitOf : ∀ (ℓ : Fin (dt.arOf vi)) (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixVarCost A vi w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk2) ((dt.varArgsOf PR.zero PR.one vi).postFold (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf (dt.ixGatesFs F PR.zero PR.one hhasP vi st v (fun (ℓ : Fin (dt.arOf vi)) => Sum.inl (Fin.castLE ⋯ ℓ)) ⋯ ⋯ ⋯ tOf (dt.varArgsOf PR.zero PR.one vi).enterBlockSt ((dt.varArgsOf PR.zero PR.one vi).enterSt f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)) (dt.arOf vi)) aT) aT) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT)) v))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT))) (mV aT)) (PR.syElt PR.blank) }

One variable's machinery, fully instantiated: from the entry checkpoint at the marker, through the gates at a gated address, the VAL clear and the rounds of matrix pass, exhaustion test and block-indexed increment, to the exit checkpoint – the fold spelled by the concrete threads, every leg the assembled runs of the layers below.

theorem DescriptiveComplexity.Draw.Data.ixVarMachine_run_thread_reachesIn {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} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) (hhasP : F.toLayout.HasName PR.zero) (heltP : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c)) (hsepP : F.toLayout.NameSep PR.zero ⋯) (hix : IsLinOrd F.le) {e₀ : Univ A R P dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe e₀ y) (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) (st : TapeSt dt A R P I) {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 : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, (∀ (x : Univ A R P dt.KIx dt.dd), r x → ∃ (i : dt.KIx), x.1 = Tag.arg i) → ∀ (u : I), WMSetLt WMLe r (F.cell u)) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) {Use : I → Prop} (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) (hvh : IxHolds elt Use v) (hxdUse : ∀ {iv : dt.d.B.ι} (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), Use (dt.ixStageXD F hhasP ℓ b)) (w wG wP wR wK : ℕ) (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hcostR : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), 2 * (wideRank (F.cell (F.toLayout.reg hhasP b c)) - wideRank v) + 2 ≤ w) (TestOf : Fin (dt.arOf vi) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir (F.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf vi) → dt.X.Tag) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → I → Prop) (hmV0 : mV a₀ = fun (x : I) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a')) (hTestT : ∀ (u : I), dt.InnerFull F.blk (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : I), ¬dt.InnerFull F.blk (mV a) u) (hmir : st.mir = ixMark elt v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixMatSt vi (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf vi b)) (hDom : ∀ (ℓ : Fin (dt.arOf vi)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hwitOf : ∀ (ℓ : Fin (dt.arOf vi)) (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf vi)) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixVarCost A vi w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (emb VarPh.vchk0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb VarPh.vchk2) ((dt.varArgsOf PR.zero PR.one vi).postFold (ixVarFXT F hinj hhasP heltP vi st v mV semT (ixVarFG F hhasP vi st v tOf f₀) aT) (dt.ixBack F.toLayout PR.zero PR.one ⋯ (ixVarStE F hinj hhasP heltP vi st v mV semT (ixVarFG F hhasP vi st v tOf f₀) aT) v))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (ixVarStE F hinj hhasP heltP vi st v mV semT (ixVarFG F hhasP vi st v tOf f₀) aT)) (mV aT)) (PR.syElt PR.blank) }

One variable's machinery, fully instantiated – threaded: as DescriptiveComplexity.Draw.Data.ixVarMachine_reachesIn with no boundary discipline assumed, so it applies at every address of a sweep and not only at the one whose SAV and TARGET the advance happens to have left behind. The rounds run at the states the thread produces, and the loop ends in DescriptiveComplexity.Draw.Data.ixVarStE at the top, which differs from the entry state in SAV and TARGET alone.