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.

theorem DescriptiveComplexity.Draw.Data.exists_argElt {L : FirstOrder.Language} {dt : Data L} {A : Type} [Nonempty A] [Nonempty dt.KIx] {R' : Type} : ∃ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) (i : dt.KIx), x.1 = Tag.arg i

An argument element: the drawn universe has one, the argument blocks and the alphabet being nonempty. It is what puts an element above the one the channel marks below them, which is what the opening's walk needs.

theorem DescriptiveComplexity.Draw.Data.exists_above_botElt {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [LinearOrder A] [Nonempty A] [Nonempty dt.KIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {R' : Type} [LinearOrder R'] [FirstOrder.Language.wide.Structure (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} (hR : PR.table.Reads) {botE : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotarg : ∀ (i : dt.KIx), botE.1 ≠ Tag.arg i) : ∃ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLt WMLe botE z

An element above the one the channel marks below the argument tags: any argument element is one, the argument tags being the greatest. This is what the opening's walk asks of the instance, and the drawing always has it.

The stage addresses lie in the logical interval

theorem DescriptiveComplexity.Draw.Data.belowTop_regLaid {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [LinearOrder A] [Nonempty A] [Finite A] [Finite dt.KIx] [Nonempty dt.KIx] [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)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hdd : dt.dd0 < dt.dd) (harg : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup PR.zero c)) {vi : dt.VarIx} {iv : dt.d.B.ι} (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (st : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R' (Option dt.KIx))) (n : ℕ) : WMSetLt WMLe (ixAddr (dt.regElt A R' (Option dt.KIx)) (dt.ixStageTgt (regLaid hlin hord) ⋯ vi ts st n)) logicalTop

Every address a stage atom reads is below the logical top, at the handed file: wmSetLt_ixStageTgt_logicalTop, read against the machine's own order. This is the hbelow an evaluation asks for, and it asks nothing of the instance.

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.