The sweep and MAIN, at the concrete program

DescriptiveComplexity.Draw.Data.reaches_sweep takes the per-address evaluation as four hypothesis families – the run itself (hspine) and three facts about the state it ends in – beside the two cover equations of the tape and control families. All six are now theorems about the branched evaluation, and this file feeds them in (DescriptiveComplexity.Draw.Data.reaches_sweepB); then it does the same one scale up, defining the stage families the machine iterates and feeding DescriptiveComplexity.Draw.Data.reaches_main (DescriptiveComplexity.Draw.Data.reaches_mainB), after which the only hypotheses left about the run are semantic – which stage converges.

Two joints are crossed here. The evaluation layer is stated at an arbitrary program and names the phases OuterPh (EvalPh dt.nv dt.PMF), which is DescriptiveComplexity.Draw.Data.PF up to unfolding – hence the @[reducible] on PF and PEF, without which instance search does not connect the two spellings. And the program's zero/one are its own arguments only up to unfolding, so the program is named once (DescriptiveComplexity.Draw.Data.progOf, reducible) and pinned explicitly wherever a pack's type mentions them.

@[reducible]

noncomputable def DescriptiveComplexity.Draw.Data.progOf {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] (hzo : zero ≠ one) [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) : Prog A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.CtlIx dt.SlotIx dt.KIx dt.dd

The reduction's own machine: the program at the packs DescriptiveComplexity.Draw.Data.varArgsOf computes. Reducible, so that its zero and one are its arguments for unification and its rules are the tower's by rfl.

Equations

• dt.progOf zero one hzo hpl = dt.prog zero one hzo (fun (w : dt.VarIx) => dt.varArgsOf zero one w) hpl

theorem DescriptiveComplexity.Draw.Data.reaches_sweepB {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hmir₀ : st₀.mir = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hbot₀ : st₀.bot = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) {s₀ s₁ : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hs₀ : WMSetLe WMLe s₀ s₁) (hs₁ : WMSetLt WMLe s₁ (wmSeg gbot)) (hltp₀ : ∀ (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ w → WMSetLt WMLe w s₁ → ¬st₀.ltp w) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (dt.sweepFSG (dt.stEndB (wmSegFile hlin) hord mV semAt) (dt.fsEndB (wmSegFile hlin) hord mV semAt) hlin st₀ f₀ s₀)), head := Sum.inl s₀, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (dt.sweepSWG (dt.stEndB (wmSegFile hlin) hord mV semAt) (dt.fsEndB (wmSegFile hlin) hord mV semAt) hlin st₀ f₀ s₀)) (dt.sweepSWG (dt.stEndB (wmSegFile hlin) hord mV semAt) (dt.fsEndB (wmSegFile hlin) hord mV semAt) hlin st₀ f₀ s₀).val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (dt.sweepFSG (dt.stEndB (wmSegFile hlin) hord mV semAt) (dt.fsEndB (wmSegFile hlin) hord mV semAt) hlin st₀ f₀ s₁)), head := Sum.inl s₁, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (dt.sweepSWG (dt.stEndB (wmSegFile hlin) hord mV semAt) (dt.fsEndB (wmSegFile hlin) hord mV semAt) hlin st₀ f₀ s₁)) (dt.sweepSWG (dt.stEndB (wmSegFile hlin) hord mV semAt) (dt.fsEndB (wmSegFile hlin) hord mV semAt) hlin st₀ f₀ s₁).val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) }

One whole sweep of the evaluation, at the concrete program: from the first address of the stretch to the last, one branched evaluation and one advance per address, the tape and control families the sweep's own. Every hypothesis DescriptiveComplexity.Draw.Data.reaches_sweep asks about the evaluation is discharged here; what is left to the caller is the geometry of the stretch and the end marker's position.

The stage families

DescriptiveComplexity.Draw.Data.reaches_main asks for the sweep and the top address's evaluation per stage, beside the two equations that say how one stage's exit becomes the next one's entry. Those equations are what the families below are defined by, so they hold by rfl; and the four registers the stages must keep – the marker, the mirror, the bottom and end marks – ride, because the sweep, the spine, and the copy-back all leave them alone (atSt, offSt and copySt write wk and old, nothing else).

noncomputable def DescriptiveComplexity.Draw.Data.stageEnd {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f : dt.CtlIx → A) : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF

The state one stage's top-address evaluation ends in – what its convergence test reads.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.stageEndFs {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f : dt.CtlIx → A) : dt.CtlIx → A

The control one stage's top-address evaluation ends in.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.stagePair {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) : ℕ → TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF × (dt.CtlIx → A)

The pair the machine enters each stage with: the reduction's own at stage zero, and at every later stage the previous stage's exit – its marker and mirror back at the empty address and its stage tracks copied back, which is reaches_main's hnextSt/hnextFs by construction.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.stagePair hpl hlin hord mV semAt ltpAddr st₀ f₀ 0 = (st₀, f₀)

noncomputable def DescriptiveComplexity.Draw.Data.stageSt {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (n : ℕ) : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF

The tape family of the stages – reaches_main's entrySt.

Equations

• DescriptiveComplexity.Draw.Data.stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n = (DescriptiveComplexity.Draw.Data.stagePair hpl hlin hord mV semAt ltpAddr st₀ f₀ n).1

noncomputable def DescriptiveComplexity.Draw.Data.stageFs {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.CtlIx → A

The control family of the stages – reaches_main's entryFs.

Equations

• DescriptiveComplexity.Draw.Data.stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n = (DescriptiveComplexity.Draw.Data.stagePair hpl hlin hord mV semAt ltpAddr st₀ f₀ n).2

theorem DescriptiveComplexity.Draw.Data.stageSt_succ {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (n : ℕ) : stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ (n + 1) = dt.copySt zero one hzo (fun (w : dt.VarIx) => dt.varArgsOf zero one w) (have __src := dt.atSt (dt.offSt (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n))) fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) ltpAddr

reaches_main's hnextSt – by construction.

theorem DescriptiveComplexity.Draw.Data.stageFs_succ {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (n : ℕ) : stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ (n + 1) = stageEndFs hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n)

reaches_main's hnextFs – by construction.

theorem DescriptiveComplexity.Draw.Data.stageEnd_ride {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) {β : Sort u_1} (F : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF → β) (hFmir : ∀ (X : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (m : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), F { mir := m, tgt := X.tgt, sav := X.sav, val := X.val, old := X.old, new := X.new, wk := X.wk, bot := X.bot, ltp := X.ltp } = F X) (hFa : ∀ (X : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), F (have __src := dt.atSt X u; { mir := u, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) = F X) (hFleg : ∀ (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (semT : dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (f : dt.CtlIx → A), F (dt.legStB (wmSegFile hlin) hord mV j st semT f) = F st) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f : dt.CtlIx → A) : F (stageEnd hpl hlin hord mV semAt ltpAddr st f) = F st

A register no leg and no advance writes rides a whole stage – the sweep by sweepSWG_ride, the top address's own evaluation by stEndB_ride.

theorem DescriptiveComplexity.Draw.Data.stageSt_fields {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hwk₀ : st₀.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hmir₀ : st₀.mir = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hbot₀ : st₀.bot = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hltp₀ : st₀.ltp = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (n : ℕ) : ((stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n).wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) ∧ ((stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n).mir = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) ∧ ((stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n).bot = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) ∧ (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n).ltp = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr

The four registers the stages must keep: the marker back at the empty address, the mirror with it, the bottom mark, and the end marker where the reduction planted it. The first two are rewritten by the copy-back's own itinerary, the last two ride.

The stage tracks, stage by stage

The dictionary invariant is what turns reaches_main's two remaining hypotheses into statements about DescriptiveComplexity.StepDef.partStage: a stage's old tracks hold that stage over the logical interval, its sweep writes the next stage into the new ones (sweep_new_trackOf), and the copy-back moves those into old. The restriction to the interval is not a convenience: outside it the tracks say nothing, an address there being able to read a stage all the same – a tuple's address with one non-argument cell added lies above the interval, non-argument tags being the most significant.

theorem DescriptiveComplexity.Draw.Data.old_trackOf_zero_of_blank {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.X.Map A)] {st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF} (hblank : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), ¬st.old iv s) (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) : st.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s

A blank tape is stage 0: the empty stage writes an empty track (trackOf_botAssign), so a tape whose stage tracks hold nothing holds stage 0 – everywhere, the interval included. This is stageSt_old's hold₀ at the initial configuration.

theorem DescriptiveComplexity.Draw.Data.stageSt_old {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hKin : ∀ (a : ιV) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hold₀ : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s ltpAddr → (st₀.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe (dt.stageTgtD zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv)) ltpAddr) (n : ℕ) (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) : WMSetLt WMLe s ltpAddr → ((stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n).old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) n) s)

A stage's tracks hold that stage of the iteration, over the logical interval: stage 0 is the initial tape, and each later one is the previous stage's sweep copied back.

theorem DescriptiveComplexity.Draw.Data.stageEnd_old_trackOf {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hKin : ∀ (a : ιV) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hold₀ : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s ltpAddr → (st₀.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe (dt.stageTgtD zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv)) ltpAddr) (n : ℕ) (iv : dt.d.B.ι) {s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hs : WMSetLt WMLe s ltpAddr) : (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) n) s

What the convergence test compares: at the end of a stage the old tracks still hold that stage.

theorem DescriptiveComplexity.Draw.Data.stageEnd_new_trackOf {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hKin : ∀ (a : ιV) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hold₀ : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s ltpAddr → (st₀.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe (dt.stageTgtD zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv)) ltpAddr) (n : ℕ) (iv : dt.d.B.ι) {s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hs : WMSetLt WMLe s ltpAddr) : (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).new iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) (n + 1)) s

And the new tracks hold the next one: the stage's own sweep wrote them, and the top address's evaluation leaves every other cell alone.

theorem DescriptiveComplexity.Draw.Data.stageEnd_conv_iff {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hKin : ∀ (a : ιV) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hold₀ : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s ltpAddr → (st₀.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe (dt.stageTgtD zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv)) ltpAddr) (n : ℕ) : (∀ (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (iv : dt.d.B.ι), (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).old iv r ↔ (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).new iv r) ↔ ∀ (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (iv : dt.d.B.ι), trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) n) r ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) (n + 1)) r

The convergence test, semantically: a stage's test passes exactly when its stage and the next agree at every address of the logical interval – reaches_main's hconv/hnotconv as statements about DescriptiveComplexity.StepDef.partStage and nothing else.

theorem DescriptiveComplexity.Draw.Data.stageEnd_conv_of_eq {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hKin : ∀ (a : ιV) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hold₀ : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s ltpAddr → (st₀.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe (dt.stageTgtD zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv)) ltpAddr) {n : ℕ} (hN : dt.d.partStage (dt.X.Map A) n = dt.d.partStage (dt.X.Map A) (n + 1)) (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) : WMSetLt WMLe r ltpAddr → ∀ (iv : dt.d.B.ι), (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).old iv r ↔ (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).new iv r

reaches_main's hconv, from a stable stage: if the stage does not move, neither does its dictionary.

theorem DescriptiveComplexity.Draw.Data.stageEnd_not_conv_of_ne {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) [LinearOrder (dt.X.Map A)] (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hKin : ∀ (a : ιV) (t : Tag (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hold₀ : ∀ (iv : dt.d.B.ι) (s : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe s ltpAddr → (st₀.old iv s ↔ trackOf dt.ly zero one ⋯ (dt.d.partStage (dt.X.Map A) 0) s)) (hbelow : ∀ (j : Fin dt.nv) (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (dt.varAt j))) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe (dt.stageTgtD zero (dt.varAt j) iv ts (dt.roundSt st (mV a)) w (dt.d.B.arity iv)) ltpAddr) (hS : ∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A), WMSetLt WMLe (tupAddr dt.ly zero one ⋯ x) ltpAddr) {n : ℕ} (hN : dt.d.partStage (dt.X.Map A) n ≠ dt.d.partStage (dt.X.Map A) (n + 1)) : ¬∀ (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (iv : dt.d.B.ι), (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).old iv r ↔ (stageEnd hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr (stageSt hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV (fun (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (hg : dt.gatedAt (wmSegFile hlin) j st) => dt.gatedSem (wmSegFile hlin) hzo hlin mV j st hg) ltpAddr st₀ f₀ n)).new iv r

reaches_main's hnotconv, from a moving stage: the dictionary is faithful over an interval that carries every tuple's own address (assignment_ext_of_trackOf), so a stage that moves moves its tracks.

theorem DescriptiveComplexity.Draw.Data.reaches_mainB {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hneT : ∃ (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), ltpAddr x) {v₁ : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hiE : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) v₁) (hwk₀ : st₀.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hmir₀ : st₀.mir = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hbot₀ : st₀.bot = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hltp₀ : st₀.ltp = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) {N : ℕ} (hnotconv : ∀ n < N, ¬∀ (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n)).old i r ↔ (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n)).new i r) (hconv : ∀ (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ N) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ N)).old i r ↔ (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ N) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ N)).new i r) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) f₀), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st₀) st₀.val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.sub dt.smEntryOut)) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ (N + 1))), head := Sum.inl v₁, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (have __src := dt.atSt (dt.offSt (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ N) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ N))) fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (have __src := dt.atSt (dt.offSt (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ N) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ N))) fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }).val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) }

MAIN, at the concrete program: from the first stage's entry at the empty address to the out machinery's entry, one sweep and one convergence test per stage, the stage families the reduction's own. Everything the machine does is now discharged; what is left of the theorem is semantic – which stage converges (hnotconv, hconv) – plus the geometry of the logical interval.

theorem DescriptiveComplexity.Draw.Data.transGen_stageB {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hTestT : ∀ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (semAt : (w : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) → (j : Fin dt.nv) → (st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → dt.gatedAt (wmSegFile hlin) j st → (p : dt.Scratch A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP (wmSegFile hlin) zero one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem zero one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) w ↑b) (dt.kindOf (dt.varAt j) b)) (st₀ : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF) (f₀ : dt.CtlIx → A) (ltpAddr : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hneT : ∃ (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), ltpAddr x) (hwk₀ : st₀.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hmir₀ : st₀.mir = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hbot₀ : st₀.bot = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hltp₀ : st₀.ltp = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (n : ℕ) (hnc : ¬∀ (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n)).old i r ↔ (stageEnd hpl hlin hord mV semAt ltpAddr (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n)).new i r) : Relation.TransGen (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ n)), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n)) (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ n).val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) (stageFs hpl hlin hord mV semAt ltpAddr st₀ f₀ (n + 1))), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ (n + 1))) (stageSt hpl hlin hord mV semAt ltpAddr st₀ f₀ (n + 1)).val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) }

One stage of MAIN, when its convergence test fails: from a stage's entry at the empty address to the next stage's, in at least one step. The strictness is the sweep's: it leaves the head at the end-marked address, which is not the empty one – and it is what DescriptiveComplexity.TMData.not_acceptsSpace_of_chain asks of a link, so that a diverging iteration keeps the machine off every halting configuration.

From the initial configuration to MAIN

DescriptiveComplexity.Draw.Data.reaches_startup stops one rule short of reaches_mainB: the mirror clear leaves the head on the marker at the empty address in clearMir1P .run, and two steps join that to the evaluation's first checkpoint – the exit rule, which steps right off the marker, and one stay step of the checkpoint, which walks back left onto it. The two presentations of the tape are one term (trackTape_val_eq_mir), so no conversion is needed beyond naming it.

theorem DescriptiveComplexity.Draw.Data.step_clearMir1_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) {v' : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) v') {fc : dt.CtlIx → A} {st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) (hreg : ¬∃ (u : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), (fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) = wmSeg u) : (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.clearMir1P TrackPh.run) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) fc), head := Sum.inl v', tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) }

The startup's exit: at the marker, the exit guard holds and the rule steps right into the evaluation's first checkpoint.

theorem DescriptiveComplexity.Draw.Data.step_chk0_back {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) {v' : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) v') {fc : dt.CtlIx → A} {st : TapeStD dt A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) : (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) fc), head := Sum.inl v', tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) }

The checkpoint walks back to the marker: off the marker the checkpoint's stay rule fires and moves left, which is the one step between the startup's exit and reaches_mainB's starting configuration.

theorem DescriptiveComplexity.Draw.Data.reaches_evalEntry {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [Fintype dt.SlotIx] [Finite A] [Finite dt.KIx] [Nonempty A] [L.IsRelational] [L.Structure A] {hzo : zero ≠ one} [LinearOrder (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [LinearOrder dt.PF] {hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)] [Finite (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w)] [Finite dt.PF] (hR : (dt.progOf zero one hzo hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd), WMLe gbot y) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt OuterPh.start fun (x : dt.CtlIx) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.emptySt) fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) } { state := Sum.inr ((dt.progOf zero one hzo hpl).stElt (OuterPh.evalP (EvalPh.chk 0)) fun (x : dt.CtlIx) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo fun (w : dt.VarIx) => dt.varArgsOf zero one w) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.progOf zero one hzo hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ dt.startupSt) dt.startupSt.val) ((dt.progOf zero one hzo hpl).syElt (dt.progOf zero one hzo hpl).blank) }

From the initial configuration to MAIN's starting configuration: the startup, its exit, and the walk back onto the marker. The state is DescriptiveComplexity.Draw.Data.startupSt – the bottom mark at the empty address, the end marker at the logical top, both registers home and every stage track still clear – which is what reaches_mainB asks of its st₀.