The spine's legs at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawInstEval read at a coarse file: one variable's machinery per spine position, the legs' controls and states, and the legs' runs with their costs.

The legs are generic in the outer phase: what they read of it is the evaluation's own phases, embedded by ep, and the machineries' rules – never the spine's, whose rule shape the space-bounded and the clocked programs do not share. The fold of these legs is DescriptiveComplexity.Problems.Wide.NexSpine.

noncomputable def DescriptiveComplexity.Draw.Data.ixPostVarSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (v : Univ A R P dt.KIx dt.dd → Prop) (st : TapeSt dt A R P I) (m : I → Prop) (i : dt.d.B.ι) (b : Prop) : TapeSt dt A R P I

The tape state after one spine position: the round state at the final VAL content, the variable's new track set at the marker to the machinery's verdict.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixBack_postVarSt_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) (v : Univ A R P dt.KIx dt.dd → Prop) {zero one : A} {st : TapeSt dt A R P I} {m : I → Prop} {i : dt.d.B.ι} {b : Prop} (r : Univ A R P dt.KIx dt.dd → Prop) (hr : r ≠ v) : dt.ixBack F.toLayout zero one ⋯ (dt.ixPostVarSt v st m i b) r = dt.ixBack F.toLayout zero one ⋯ (dt.ixRoundSt st m) r

Off the marker, the post state's background is the round state's.

theorem DescriptiveComplexity.Draw.Data.ixBack_postVarSt_v {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) (v : Univ A R P dt.KIx dt.dd → Prop) {zero one : A} {st : TapeSt dt A R P I} {m : I → Prop} {i : dt.d.B.ι} {b : Prop} : dt.ixBack F.toLayout zero one ⋯ (dt.ixPostVarSt v st m i b) v = Function.update (dt.ixBack F.toLayout zero one ⋯ (dt.ixRoundSt st m) v) (Slot.new i) (bitVal zero one b)

At the marker, the post state's background is the round state's with the variable's stage slot updated to the verdict bit.

One position's leg

noncomputable def DescriptiveComplexity.Draw.Data.ixLegCtl {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixRoundSt st (mV a)) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after one position's leg: the machinery's exit fold – DescriptiveComplexity.Draw.Data.ixVarMachine_reachesIn's final control, at the position's variable.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixLegCtlT {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after one position's leg, threaded – the twin of DescriptiveComplexity.Draw.Data.ixLegCtl, with the VAL loop's rounds run at the states the thread produces for them.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixLegStT {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The tape state after one position's leg, threaded: the VAL loop's exit state – the entry state's SAV and TARGET normalized if any of its rounds ran a stage atom – with the variable's new track written at the marker.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixLegStT_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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀).mir = st.mir ∧ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀).wk = st.wk ∧ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀).bot = st.bot ∧ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀).old = st.old ∧ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀).ltp = st.ltp ∧ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀).val = mV aT

What a leg leaves alone: the machinery writes its own two scratch registers and its stage bit, so the mirror, the marker, the bottom and end marks and the stage dictionary all ride – which is what carries the next position's pack and, one scale up, the sweep's own invariants.

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

What one leg of the evaluation's spine is charged: the walk-back, the whole machinery of the position's variable, and the written exit. Uniform over the positions – the largest of the variables' costs – so the spine's fold is a single width.

Equations

• dt.ixLegCost A w wP wR wK n = (1 + Finset.univ.sup fun (j : Fin dt.nv) => dt.ixVarCost A (dt.varAt j) w wP wR wK n) + 1

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

What the output's leg is charged: the same shape at the output's own machinery, which is the none variable's.

Equations

• dt.ixOutLegCost A w wP wR wK n = 1 + dt.ixVarCost A none w wP wR wK n + 1

The costs, factored

The clock compares a product: a width and a number of rounds, each bounded on its own (nexTotal_lt_two_pow). So each cost above, which is «once plus a round's cost per VAL content», is rewritten here as «a width times the rounds and one more» – the width is the sum of the two parts, and nothing about the program is used but the shape of the definitions.

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

A variable's machinery, as one width: what it pays once and what it pays per VAL round, added.

Equations

• dt.ixVarCD A vi w wP wR wK = 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)

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

The width of a leg of the spine: the largest variable's, and the leg's own two steps.

Equations

• dt.ixLegWidth A w wP wR wK = 4 + Finset.univ.sup fun (j : Fin dt.nv) => dt.ixVarCD A (dt.varAt j) w wP wR wK

theorem DescriptiveComplexity.Draw.Data.ixVarCost_le_mul {L : FirstOrder.Language} (dt : Data L) {A : Type} (vi : dt.VarIx) (w wP wR wK n : ℕ) : dt.ixVarCost A vi w wP wR wK n ≤ dt.ixVarCD A vi w wP wR wK * (n + 1)

A variable's whole cost is its width times the rounds and one more.

theorem DescriptiveComplexity.Draw.Data.ixLegCost_le_mul {L : FirstOrder.Language} (dt : Data L) {A : Type} (w wP wR wK n : ℕ) : dt.ixLegCost A w wP wR wK n + 2 ≤ dt.ixLegWidth A w wP wR wK * (n + 1)

A leg's whole cost, and its dispatch, is its width times the rounds and one more.

theorem DescriptiveComplexity.Draw.Data.ixSpineCost_le_mul {L : FirstOrder.Language} (dt : Data L) {A : Type} (w wP wR wK n : ℕ) : (dt.ixLegCost A w wP wR wK n + 2) * dt.nv ≤ dt.ixLegWidth A w wP wR wK * dt.nv * (n + 1)

The spine's whole cost, factored: a width – the leg's, times the number of positions – and the number of VAL rounds and one more. This is the shape the clock compares (nexTotal_lt_two_pow), so what an instantiation owes is a bound on each factor separately.

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

The width of the whole clocked evaluation: the spine's width times its positions, the output machinery's own, and the four steps that join them – the dispatch into the spine, the dispatch into the output's leg and the two the legs themselves pay. This is the first factor the clock compares.

Equations

• dt.ixEvalWidth A w wP wR wK = dt.ixLegWidth A w wP wR wK * dt.nv + dt.ixVarCD A none w wP wR wK + 4

theorem DescriptiveComplexity.Draw.Data.ixEvalCost_le_mul {L : FirstOrder.Language} (dt : Data L) {A : Type} (w wP wR wK n : ℕ) : 1 + (dt.ixLegCost A w wP wR wK n + 2) * dt.nv + 1 + dt.ixOutLegCost A w wP wR wK n ≤ dt.ixEvalWidth A w wP wR wK * (n + 1)

The clocked evaluation's whole cost, factored: one width times the VAL rounds and one more. This is what DescriptiveComplexity.Draw.Data.nexProg_wideAccept_legs asks of the evaluation leg – the run's count is exactly the left-hand side.

theorem DescriptiveComplexity.Draw.Data.ixVarLeg_run_thread_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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)) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v 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) {ι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) (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (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 (dt.varAt j)) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (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 ℓ) (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 (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (hDom : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixLegCtlT F hinj hhasP heltP mV j st tOf semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixLegStT F hinj hhasP heltP mV j st tOf semT f₀)) (mV aT)) (PR.syElt PR.blank) }

One spine position's leg – threaded: the leg without the boundary hypotheses hsav/htgt, which the sweep cannot supply at more than one address. The leg ends in DescriptiveComplexity.Draw.Data.ixLegStT, the machinery's own exit state with the stage bit written at the marker.

theorem DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (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) (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) {ιV : Type} (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (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 (dt.varAt j)) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf (dt.varAt j))) (hTestLt : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ↑ℓ < ↑ℓ₀ → ∀ (u : I), TestOf ℓ u) {u₀ : I} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixFailCtl F hhasP (dt.varAt j) st tOf ℓ₀ ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).enterSt f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixPostVarSt v st st.val (dt.varList.get j) False)) st.val) (PR.syElt PR.blank) }

One spine position's leg at a junk address: the walk-back, the machinery's failing gates, and the erased stage slot at the marker – the verdict False, the VAL register untouched.

theorem DescriptiveComplexity.Draw.Data.ixVarLegUngated_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') (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) (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) {ιV : Type} (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (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 (dt.varAt j)) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), TestOf ℓ u) (ℓ₀ : Fin (dt.arOf (dt.varAt j))) (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) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixUngatedCtl F hhasP (dt.varAt j) st tOf ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).enterSt f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixPostVarSt v st st.val (dt.varList.get j) False)) st.val) (PR.syElt PR.blank) }

One spine position's leg at a shaped but ungated address: the walk-back, the whole gate sequence – every file test passing, the total dispatch carrying every block through – the clear flag at the verdict checkpoint, and the erased stage slot at the marker: the verdict False, the VAL register untouched. With DescriptiveComplexity.Draw.Data.ixVarLeg_run_thread_reachesIn and DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn this covers every address the sweep visits.

The output's leg

The out machinery is the same shape at vi := none, entered by the walk home after a passed convergence sweep, its exit the accepting phase. Its stage slot is the working-cell marker itself, so an accepting verdict's write is idempotent – the tape after the leg is the machinery's own end tape.

noncomputable def DescriptiveComplexity.Draw.Data.ixOutFM {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → I → Prop) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt st (mV a)) elt (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : ιV → dt.CtlIx → A

The VAL-loop thread of the output's leg, at the entry-wrapped control.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixOutCtl {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt st (mV a)) elt (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after the output's leg: the out machinery's exit fold.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixOutLeg_run {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (accPh : P) (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => ep (EvalPh.sub (Sum.inr p))) accPh 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)) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v 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) {ι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) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf none) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (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 none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (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 ℓ) (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 none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt st (mV a)) elt (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) (hacc : (dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl F hinj hhasP heltP mV st tOf semOf f₀)) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixOutLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub dt.smEntryOut)) 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 accPh (dt.ixOutCtl F hinj hhasP heltP mV st tOf semOf f₀)), 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) }

The output's leg: from the walk home's landing one cell right of the marker, back to it, through the out machinery, and – the verdict holding – out into the accepting phase, the marker rewritten with the value it already carries.

theorem DescriptiveComplexity.Draw.Data.ixOutLeg_run_any {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (accPh : P) (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => ep (EvalPh.sub (Sum.inr p))) accPh 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)) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v 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) {ι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) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf none) → I → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (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 none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (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 ℓ) (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 none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt st (mV a)) elt (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : I), TestOf ℓ u) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixOutLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub dt.smEntryOut)) 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 accPh (dt.ixOutCtl F hinj hhasP heltP mV st tOf semOf f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (fun (r : Univ A R P dt.KIx dt.dd → Prop) => if r = v then Function.update (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT)) v) (dt.varArgsOf PR.zero PR.one none).newSlot (bitVal PR.zero PR.one ((dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl F hinj hhasP heltP mV st tOf semOf f₀))) else dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT)) r) (mV aT)) (PR.syElt PR.blank) }

The output's leg, whatever the verdict: ixOutLeg_run with the verdict not assumed. The run is the same run – the exit fires either way – and what changes is only what it writes at the marker: the verdict's own bit. This is what a backward reading needs, where the verdict is what is being determined rather than assumed.

noncomputable def DescriptiveComplexity.Draw.Data.ixOutStE {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixMatSt none (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The state the output's leg ends at – threaded: the machinery's own exit state, the accepting write at the marker being idempotent.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixOutCtlT {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixMatSt none (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control after the output's leg – threaded: the out machinery's exit fold, at the states its own thread produces.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixOutStA {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (st : TapeSt dt A R P I) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semT : (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixMatSt none (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The state the output's leg leaves, whatever its verdict: the machinery's exit state with the marker rewritten by the accepting bit – so the marker survives a true verdict and is cleared by a false one, which is what makes a false output halt and reject.

Equations

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

Which leg a position takes

A position's machinery has three runs, by what its gates do: DescriptiveComplexity.Draw.Data.ixVarLeg_run_thread_reachesIn when every block is well shaped and the tags and the domain sentence agree, DescriptiveComplexity.Draw.Data.ixVarLegUngated_reachesIn when the blocks are well shaped but the verdict flag is cleared, and DescriptiveComplexity.Draw.Data.ixVarLegFail_reachesIn when a block fails the shape test – which is the one that needs a witness, and a least one, so that the blocks before it have run.

def DescriptiveComplexity.Draw.Data.ixShapeAt {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) (j : Fin dt.nv) (st : TapeSt dt A R P I) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I) : Prop

The shape test the gates run, at a position and a state: the per-cell question a block's TestKit asks, which is what tells the third leg from the other two.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixTagAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeSt dt A R P I) (ℓ : Fin (dt.arOf (dt.varAt j))) : dt.X.Tag

The tag a block's witness cells name, as the machine reads it – so htagOf is rfl at this choice.

Equations

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

def DescriptiveComplexity.Draw.Data.ixTagDomAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeSt dt A R P I) (ℓ : Fin (dt.arOf (dt.varAt j))) : Prop

The other half of a block's gate: its tag witnesses are one-hot at the tag they name, and the expansion's domain sentence holds of the point the block decodes. Together with DescriptiveComplexity.Draw.Data.ixShapeAt this is the gates' verdict.

Equations

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

def DescriptiveComplexity.Draw.Data.ixGatedAt {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] (j : Fin dt.nv) (st : TapeSt dt A R P I) : Prop

A position is gated when every block passes both halves.

Equations

• dt.ixGatedAt F j st = ((∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : I), dt.ixShapeAt F j st ℓ u) ∧ ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.ixTagDomAt j st ℓ)

noncomputable def DescriptiveComplexity.Draw.Data.ixLegStB {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : TapeSt dt A R P I

The state one position's leg leaves, whichever leg it takes: the machinery's own exit at a gated position, and the entry state with the stage bit erased at the two ungated ones – which agree on the tape and differ only in their control.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixLegCtlB {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

The control one position's leg leaves: the machinery's fold at a gated position, the ungated exit when the blocks are well shaped but a tag or the domain fails, and the failing gates' exit – at the least badly shaped block – otherwise.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixLegStB_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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).mir = st.mir ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).wk = st.wk ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).bot = st.bot ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).old = st.old ∧ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).ltp = st.ltp

What a leg leaves alone, whichever leg it takes: the ungated legs never enter the VAL loop, so they touch nothing but the stage bit, and the gated one is DescriptiveComplexity.Draw.Data.ixLegStT_fields. The val register is left out on purpose – it is the loop's top at a gated position and the entry state's at the other two.

noncomputable def DescriptiveComplexity.Draw.Data.ixLegBitB {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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : Prop

The stage bit one position writes, whichever leg it takes: the machinery's verdict at a gated position, False at the two ungated ones, which is what the stage dictionary holds where the blocks encode no point.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ixLegStB_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] {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (semT : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) (i' : dt.d.B.ι) (r : Univ A R P dt.KIx dt.dd → Prop) : (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).new i' r = if i' = dt.varList.get j ∧ r = v then dt.ixLegBitB F hinj hhasP heltP mV j st semT f₀ else st.new i' r

What a leg writes: its variable's cell at the marker, and nothing else – the same equation whichever leg it takes, since the VAL loop threads the two scratch registers alone (DescriptiveComplexity.Draw.Data.ixVarStE_new) and the ungated legs write the stage bit directly. This is the branched twin of DescriptiveComplexity.Draw.Data.new_postVarSt, and the only thing the spine's dictionary lemmas need of a leg.

theorem DescriptiveComplexity.Draw.Data.ixVarLegB_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] (ep : EvalPh dt.nv dt.PMF → 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] [Finite dt.KIx] {v v' : Univ A R P dt.KIx dt.dd → Prop} {rEmbM : (j : Fin dt.nv) → (i : dt.VarSiteF (dt.varAt j)) → dt.VarShF (dt.varAt j) i → R} (hrulesM : ∀ (j : Fin dt.nv) (i : dt.VarSiteF (dt.varAt j)) (ρ : dt.VarShF (dt.varAt j) i), PR.rules (rEmbM j i ρ) = dt.varRuleF PR.zero PR.one (dt.varAt j) (dt.varArgsOf PR.zero PR.one (dt.varAt j)) (fun (p : dt.VarPhF (dt.varAt j)) => ep (EvalPh.sub (Sum.inl ⟨j, p⟩))) (ep (EvalPh.chk j.succ)) 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)) (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v 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) {ι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) (j : Fin dt.nv) (st : TapeSt dt A R P I) (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (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 : dt.ixGatedAt F j st → (p : dt.IxScratch A R P I) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (dt.ixLegCost A w wP wR wK (Nat.card ιV)) { state := Sum.inr (PR.stElt (ep (EvalPh.sub (dt.smEntry j))) 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 (ep (EvalPh.chk j.succ)) (dt.ixLegCtlB F hinj hhasP heltP mV j st semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀)) (dt.ixLegStB F hinj hhasP heltP mV j st semT f₀).val) (PR.syElt PR.blank) }

One spine position's leg, whichever leg it takes: the three runs of the machinery under one statement, the case split on the gates made once and for all. This is what a sweep needs, since it visits junk addresses and gated ones alike.