The handed program accepts, from the sentence alone

DescriptiveComplexity.Draw.Data.wideRegAccept_regLaid_of_rules joins the two legs of the run at the file the register channel hands over, and asks the caller for some thirty facts. Most of them are not about the instance at all: they follow from the marking (hasInp_up, exists_regBotElt), from the order (exists_openingWalkReg, exists_regValEnum), from where the marker is (exitG_at_marker), from what the guess wrote (guessTracks_hdict_of_old) and from what a leg leaves behind (parked_ixSpineStOfB).

This file supplies all of those, so that what is left of the run is what the reduction decides: the assignment its guess writes, the sentence being true, the order on the expanded universe, and the three numbers of the clock.

The stage addresses lie in the logical interval

The run, from the sentence and the clock

theorem DescriptiveComplexity.Draw.Data.wideRegAccept_of_out_of_rules {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [LinearOrder A] [Nonempty A] [Finite A] [Finite dt.KIx] [Nonempty dt.KIx] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [Finite (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {R' : Type} [LinearOrder R'] [Finite R'] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {bot : Option dt.KIx} (hE : NexEmitted PR bot) (hR : PR.table.Reads) (hdd : dt.dd0 < dt.dd) (harity : ∀ (iv : dt.d.B.ι), 0 < dt.d.B.arity iv) (σ : dt.d.B.Assignment (dt.X.Map A)) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hout : dt.X.Map A ⊨ dt.d.out) {a b k j m : ℕ} (hk : 1 ≤ k) (hkj : k + 1 < j) (hm : 0 < m) (hcard : (k + j) * m ≤ Nat.card (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (ha : dt.ixEvalWidth A (dt.nexRegW A R' (Option dt.KIx)) (dt.nexRegWP A R' (Option dt.KIx)) (dt.nexRegWR A R' (Option dt.KIx)) (dt.nexRegWK A R' (Option dt.KIx)) ≤ a) (haa : a ≤ 2 ^ (k * m)) (hb : dt.regBound + 1 ≤ b) (hbb : b ≤ 2 ^ (k * m)) (hopenle : 4 * dt.regBound + 8 ≤ 2 ^ ((k + 1) * m)) : WideRegAccept.Holds (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)

The handed program accepts, from the sentence alone. wideRegAccept_regLaid_of_rules with everything the drawing decides supplied: the marking and its consequences (regFacts_of_marked), the file's two ends (exists_regTop, exists_regBot), the opening's walk (exists_openingWalkReg), the rounds (exists_regValEnum), the two exits (exitG_at_marker), the dictionary the guess wrote (guessTracks_hdict_of_old), the scratch it parks (parked_ixSpineStOfB) and the region the stage atoms stay inside (belowTop_regLaid).

What is left is what the reduction decides: the assignment its guess writes, the sentence being true at it, the order on the expanded universe, and the three numbers of the clock – the last stated against the file's own bound, so that a reduction proves them of its drawing and of nothing else.