The tag-branched machinery's run

The run theorem of DescriptiveComplexity.Draw.tagRule: the witness reads store the argument points' tags one-hot into the control, the branch checkpoint dispatches on the decoded tuple – its guard TagsAre holding at exactly one tag tuple – and that tuple's element loop runs to the shared exit phase by DescriptiveComplexity.Draw.elem_reachesIn.

The run comes with its cost (tag_reachesIn): the chain's reads at the trip width the caller fixes, the branch's dispatch and walk back, and the loop's own count. tag_run is it with the budget forgotten, at the width every trip has anyway.

As in the element loop's run, the machinery is entered at its first phase on the marker (the caller's dispatch steps right and DescriptiveComplexity.Draw.tag_back walks back down), and it leaves through the loop's exit dispatch one cell to the marker's right.

theorem DescriptiveComplexity.Draw.tag_back {A R P Q W K T : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {m : ℕ} {nrOf : T → ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : TagPh m T nrOf → P} {rdTrackT : Fin m → W} {MatchT : Fin m → (Q → A) → (W → A) → Prop} {setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A} {TagsAre : T → (Q → A) → Prop} {rdTrackE : (τ : T) → Fin (nrOf τ) → W} {MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop} {setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A} {IsMaxEl : T → (Q → A) → Prop} {exitPh : P} {rEmb : (i : TagSite m T nrOf) → TagSh m T nrOf i → R} (hlin : IsLinOrd WMLe) {v v' : Univ A R P K dd → Prop} (hvi : WMIncr WMLe v v') {rest : (Univ A R P K dd → Prop) → W → A} (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) {t₀ : W} {m₀ : I → Prop} (hwkt₀ : wk ≠ t₀) (hR : PR.table.Reads) (hrules : ∀ (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i), PR.rules (rEmb i ρ) = tagRule PR.one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ) {f : Q → A} : (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (tagFirstRd emb) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (tagFirstRd emb) f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }

The one leftward step a caller's rightward dispatch into the machinery owes: at its first phase, the walk back down to the marker.