The spine, instantiated: one variable's machinery per position

DescriptiveComplexity.Draw.Data.eval_run chains one abstract machinery run per spine position; this file discharges each leg at the program's own rules. A leg is three pieces: the walk back into the variable's entry checkpoint (DescriptiveComplexity.Draw.Data.step_var_back), the whole machinery (DescriptiveComplexity.Draw.Data.varMachine_run), and the written exit step (DescriptiveComplexity.Draw.Data.step_var_exit) – whose write is the variable's stage bit, so the tape state after the leg is DescriptiveComplexity.Draw.Data.postVarSt: the round state at the exhausted VAL, the new track updated at the marker.

The enumeration of the VAL loop (ιV/mV) is shared by every position – it enumerates the register contents, which do not depend on the variable – and stays abstract here, with the per-position semantic data (DescriptiveComplexity.Draw.Data.KindSem, the gates' domain facts), to be supplied by the encoding layer.

noncomputable def DescriptiveComplexity.Draw.Data.postVarSt {L : FirstOrder.Language} (dt : Data L) {A R : Type} (v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (i : dt.d.B.ι) (b : Prop) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.back_postVarSt_off {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) {zero one : A} {st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {i : dt.d.B.ι} {b : Prop} (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hr : r ≠ v) : dt.back RF.cell zero one ⋯ (dt.postVarSt v st m i b) r = dt.back RF.cell zero one ⋯ (dt.roundSt st m) r

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

theorem DescriptiveComplexity.Draw.Data.back_postVarSt_v {L : FirstOrder.Language} (dt : Data L) {A R : Type} [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) {zero one : A} {st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))} {m : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {i : dt.d.B.ι} {b : Prop} : dt.back RF.cell zero one ⋯ (dt.postVarSt v st m i b) v = Function.update (dt.back RF.cell zero one ⋯ (dt.roundSt st m) v) (Slot.new i) (bitVal zero one b)

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

One position's leg

noncomputable def DescriptiveComplexity.Draw.Data.legCtl {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

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

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.legCtlT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

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

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.legStT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.legStT_fields {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : (dt.legStT RF hord mV j st tOf semT f₀).mir = st.mir ∧ (dt.legStT RF hord mV j st tOf semT f₀).wk = st.wk ∧ (dt.legStT RF hord mV j st tOf semT f₀).bot = st.bot ∧ (dt.legStT RF hord mV j st tOf semT f₀).old = st.old ∧ (dt.legStT RF hord mV j st tOf semT f₀).ltp = st.ltp ∧ (dt.legStT RF hord mV j st tOf semT f₀).val = mV aT

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

theorem DescriptiveComplexity.Draw.Data.legCtlT_eq_legCtl {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hreg : ¬∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), v = RF.cell u) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.legCtlT RF hord mV j st tOf (semCastT RF (dt.varAt j) st v mV sem₀) f₀ = dt.legCtl RF hord mV j st tOf sem₀ f₀

A position's threaded leg computes the unthreaded fold: its VAL loop is the unthreaded loop (varFMT_eq_varFM), its last round the unthreaded round (varFXT_eq_roundFX), and the background it folds against is the round state's, the loop's exit differing from it in SAV and TARGET alone. This is what makes the branched leg's stage bit (DescriptiveComplexity.Draw.Data.legBitB) the verdict DescriptiveComplexity.Draw.Data.accVerdict_next reads.

theorem DescriptiveComplexity.Draw.Data.varLeg_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsav : st.sav = v) (htgt : st.tgt = v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt st (mV a)) (dt.kindOf (dt.varAt j) b)) (hDom : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (dt.smEntry j))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk j.succ)) (dt.legCtl RF hord mV j st tOf semOf f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.postVarSt v st (mV aT) (dt.varList.get j) ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).accBit (dt.legCtl RF hord mV j st tOf semOf f₀)))) (mV aT)) (PR.syElt PR.blank) }

One spine position's leg: from the dispatch's landing one cell right of the marker, back to it, through the variable's whole machinery, and out through the written exit – the stage bit at the marker now the machinery's verdict, the phase the next checkpoint.

theorem DescriptiveComplexity.Draw.Data.varLeg_run_thread {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (hDom : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (dt.smEntry j))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk j.succ)) (dt.legCtlT RF hord mV j st tOf semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.legStT RF hord mV j st tOf semT f₀)) (mV aT)) (PR.syElt PR.blank) }

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

theorem DescriptiveComplexity.Draw.Data.varLegFail_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (ℓ₀ : Fin (dt.arOf (dt.varAt j))) (hTestLt : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), ↑ℓ < ↑ℓ₀ → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) {u₀ : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hfail : ¬TestOf ℓ₀ u₀) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (dt.smEntry j))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk j.succ)) (dt.failCtl RF (dt.varAt j) st tOf ℓ₀ ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).enterSt f₀ (dt.back RF.cell PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.postVarSt v st st.val (dt.varList.get j) False)) st.val) (PR.syElt PR.blank) }

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

theorem DescriptiveComplexity.Draw.Data.varLegUngated_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf (dt.varAt j)) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (htagOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))) = tOf ℓ) (hTestOf : ∀ (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) (ℓ₀ : Fin (dt.arOf (dt.varAt j))) (hbad : ¬((∀ (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ₀) ∧ ExpExpansion.DomHolds (tOf ℓ₀, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ₀)))))))) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (dt.smEntry j))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk j.succ)) (dt.ungatedCtl RF (dt.varAt j) st tOf ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).enterSt f₀ (dt.back RF.cell PR.zero PR.one ⋯ st v)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.postVarSt v st st.val (dt.varList.get j) False)) st.val) (PR.syElt PR.blank) }

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

The output's leg

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

noncomputable def DescriptiveComplexity.Draw.Data.outFM {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.roundSt st (mV a)) (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : ιV → dt.CtlIx → A

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

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.outCtl {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.roundSt st (mV a)) (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.outLeg_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf none) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsav : st.sav = v) (htgt : st.tgt = v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.roundSt st (mV a)) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) (hacc : (dt.varArgsOf PR.zero PR.one none).accBit (dt.outCtl RF hord mV st tOf semOf f₀)) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub dt.smEntryOut)) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt OuterPh.acceptP (dt.outCtl RF hord mV st tOf semOf f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT))) (mV aT)) (PR.syElt PR.blank) }

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

noncomputable def DescriptiveComplexity.Draw.Data.outStE {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.matSt none (varRdSt st p (mV a)) v ↑b) (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

• dt.outStE RF hord mV st tOf semT f₀ = DescriptiveComplexity.Draw.Data.varStE RF hord none st v mV semT (DescriptiveComplexity.Draw.Data.varFG RF none st v tOf f₀) aT

noncomputable def DescriptiveComplexity.Draw.Data.outCtlT {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.matSt none (varRdSt st p (mV a)) v ↑b) (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.outCtlT_eq_outCtl {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hreg : ¬∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), v = RF.cell u) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf none) → dt.X.Tag) (sem₀ : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.roundSt st (mV a)) (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : dt.outCtlT RF hord mV st tOf (semCastT RF none st v mV sem₀) f₀ = dt.outCtl RF hord mV st tOf sem₀ f₀

The output's threaded leg computes the unthreaded fold: as DescriptiveComplexity.Draw.Data.legCtlT_eq_legCtl at the output variable – the VAL loop is the unthreaded loop, its last round the unthreaded round, and the exit state differs from the round state in SAV and TARGET alone, which the background does not see off the register file. This is what makes outLeg_run_thread's hacc the verdict DescriptiveComplexity.Draw.Data.accVerdict_out reads.

noncomputable def DescriptiveComplexity.Draw.Data.outStA {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (tOf : Fin (dt.arOf none) → dt.X.Tag) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.matSt none (varRdSt st p (mV a)) v ↑b) (dt.kindOf none b)) (f₀ : dt.CtlIx → A) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.outLeg_run_verdict {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf none) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.matSt none (varRdSt st p (mV a)) v ↑b) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub dt.smEntryOut)) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt OuterPh.acceptP (dt.outCtlT RF hord mV st tOf semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.outStA RF hord mV st tOf semT f₀)) (mV aT)) (PR.syElt PR.blank) }

The output's leg – threaded, whatever the verdict: as DescriptiveComplexity.Draw.Data.outLeg_run without the boundary hypotheses hsav/htgt, which nothing supplies at the end of a sweep – the advance refreshes the marker and the mirror, not the two scratch registers – and without any assumption on the verdict. The leg ends in the accepting phase either way; what the verdict decides is the bit the exit writes at the marker (DescriptiveComplexity.Draw.Data.outStA), and with it whether the machine's accepting predicate holds of the state it stops in.

theorem DescriptiveComplexity.Draw.Data.outLeg_run_thread {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOf : Fin (dt.arOf none) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semT : (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.matSt none (varRdSt st p (mV a)) v ↑b) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOf ℓ u) (f₀ : dt.CtlIx → A) (hacc : (dt.varArgsOf PR.zero PR.one none).accBit (dt.outCtlT RF hord mV st tOf semT f₀)) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub dt.smEntryOut)) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt OuterPh.acceptP (dt.outCtlT RF hord mV st tOf semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.outStE RF hord mV st tOf semT f₀)) (mV aT)) (PR.syElt PR.blank) }

The output's leg – threaded, the verdict holding: the special case of DescriptiveComplexity.Draw.Data.outLeg_run_verdict in which the accepting write at the marker is idempotent, so the leg ends at the machinery's own exit state and nothing of the tape moves.

Which leg a position takes

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

theorem DescriptiveComplexity.Draw.Data.exists_least_fail {n : ℕ} {α : Sort u_1} {T : Fin n → α → Prop} (h : ¬∀ (ℓ : Fin n) (u : α), T ℓ u) : ∃ (ℓ₀ : Fin n) (u₀ : α), ¬T ℓ₀ u₀ ∧ ∀ (ℓ : Fin n), ↑ℓ < ↑ℓ₀ → ∀ (u : α), T ℓ u

The least failing index, with a witness: from a family that is not everywhere true, the first index at which it fails, together with a value at which it does and the fact that every earlier index is everywhere true. This is DescriptiveComplexity.Draw.Data.varLegFail_run's ℓ₀/hTestLt/hfail produced from the plain negation, which is all a per-address case split has.

def DescriptiveComplexity.Draw.Data.shapeAt {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) : Prop

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

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.tagAt {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (ℓ : Fin (dt.arOf (dt.varAt j))) : dt.X.Tag

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

Equations

• dt.tagAt j st ℓ = dt.dspTagOf PR.zero PR.one (DescriptiveComplexity.wmBlk st.mir (DescriptiveComplexity.Draw.Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))

def DescriptiveComplexity.Draw.Data.tagDomAt {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (ℓ : Fin (dt.arOf (dt.varAt j))) : Prop

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

Equations

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

def DescriptiveComplexity.Draw.Data.gatedAt {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) : Prop

A position is gated when every block passes both halves.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.legStB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))

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

Equations

• dt.legStB RF hord mV j st semT f₀ = if hg : dt.gatedAt RF j st then dt.legStT RF hord mV j st (dt.tagAt j st) (semT hg) f₀ else dt.postVarSt v st st.val (dt.varList.get j) False

noncomputable def DescriptiveComplexity.Draw.Data.legCtlB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : dt.CtlIx → A

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

Equations

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

theorem DescriptiveComplexity.Draw.Data.legStB_fields {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : (dt.legStB RF hord mV j st semT f₀).mir = st.mir ∧ (dt.legStB RF hord mV j st semT f₀).wk = st.wk ∧ (dt.legStB RF hord mV j st semT f₀).bot = st.bot ∧ (dt.legStB RF hord mV j st semT f₀).old = st.old ∧ (dt.legStB RF hord mV j st semT f₀).ltp = st.ltp

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

noncomputable def DescriptiveComplexity.Draw.Data.legBitB {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : Prop

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

Equations

• dt.legBitB RF hord mV j st semT f₀ = if hg : dt.gatedAt RF j st then (dt.varArgsOf PR.zero PR.one (dt.varAt j)).accBit (dt.legCtlT RF hord mV j st (dt.tagAt j st) (semT hg) f₀) else False

theorem DescriptiveComplexity.Draw.Data.legStB_new {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {v : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] {aT : ιV} (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) (i' : dt.d.B.ι) (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) : (dt.legStB RF hord mV j st semT f₀).new i' r = if i' = dt.varList.get j ∧ r = v then dt.legBitB RF hord mV j st semT f₀ else st.new i' r

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

theorem DescriptiveComplexity.Draw.Data.varLegB_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (j : Fin dt.nv) (st : TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (hwkSt : st.wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmir : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semT : dt.gatedAt RF j st → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt st p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.sub (dt.smEntry j))) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk j.succ)) (dt.legCtlB RF hord mV j st semT f₀)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (dt.legStB RF hord mV j st semT f₀)) (dt.legStB RF hord mV j st semT f₀).val) (PR.syElt PR.blank) }

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

The spine

theorem DescriptiveComplexity.Draw.Data.evalSpine_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsOf : Fin (dt.nv + 1) → dt.CtlIx → A) (hwkOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOfJ : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOfJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ (stOf j.castSucc)) (stOf j.castSucc).mir (RF.cell u)) ↔ TestOfJ j ℓ u) (tOfJ : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hwitOfJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))) (t' : dt.X.Tag), wmBlk (stOf j.castSucc).mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOfJ j ℓ) (hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = v) (hbotOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).sav = v) (htgtOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).tgt = v) (semOfJ : (j : Fin dt.nv) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.roundSt (stOf j.castSucc) (mV a)) (dt.kindOf (dt.varAt j) b)) (hDomJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))), ExpExpansion.DomHolds (tOfJ j ℓ, decRho dt.ly PR.zero PR.one (wmBlk (stOf j.castSucc).mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOfJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOfJ j ℓ u) (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.postVarSt v (stOf j.castSucc) (mV aT) (dt.varList.get j) ((dt.varArgsOf PR.zero PR.one (dt.varAt j)).accBit (dt.legCtl RF hord mV j (stOf j.castSucc) (tOfJ j) (semOfJ j) (fsOf j.castSucc)))) (hfs : ∀ (j : Fin dt.nv), fsOf j.succ = dt.legCtl RF hord mV j (stOf j.castSucc) (tOfJ j) (semOfJ j) (fsOf j.castSucc)) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) (fsOf (Fin.last dt.nv))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stOf (Fin.last dt.nv))) (stOf (Fin.last dt.nv)).val) (PR.syElt PR.blank) }

The evaluation's spine, fully instantiated: from the checkpoint before the first variable to the checkpoint after the last, one whole machinery per position – each leg DescriptiveComplexity.Draw.Data.varLeg_run, the tape and control threads given as families with one cover equation per position.

theorem DescriptiveComplexity.Draw.Data.evalSpine_run_thread {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsOf : Fin (dt.nv + 1) → dt.CtlIx → A) (hwkOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (TestOfJ : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hcompatOfJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ (stOf j.castSucc)) (stOf j.castSucc).mir (RF.cell u)) ↔ TestOfJ j ℓ u) (tOfJ : (j : Fin dt.nv) → Fin (dt.arOf (dt.varAt j)) → dt.X.Tag) (hwitOfJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))) (t' : dt.X.Tag), wmBlk (stOf j.castSucc).mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOfJ j ℓ) (hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = v) (hbotOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semTJ : (j : Fin dt.nv) → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt (stOf j.castSucc) p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt (stOf j.castSucc) p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (hDomJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))), ExpExpansion.DomHolds (tOfJ j ℓ, decRho dt.ly PR.zero PR.one (wmBlk (stOf j.castSucc).mir (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOfJ : ∀ (j : Fin dt.nv) (ℓ : Fin (dt.arOf (dt.varAt j))) (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), TestOfJ j ℓ u) (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.legStT RF hord mV j (stOf j.castSucc) (tOfJ j) (semTJ j) (fsOf j.castSucc)) (hfs : ∀ (j : Fin dt.nv), fsOf j.succ = dt.legCtlT RF hord mV j (stOf j.castSucc) (tOfJ j) (semTJ j) (fsOf j.castSucc)) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) (fsOf (Fin.last dt.nv))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stOf (Fin.last dt.nv))) (stOf (Fin.last dt.nv)).val) (PR.syElt PR.blank) }

The evaluation's spine, fully instantiated – threaded: as DescriptiveComplexity.Draw.Data.evalSpine_run with hsavOf and htgtOf gone. That is the point of the whole threading: the advance refreshes the marker and the mirror but not SAV and TARGET, so a sweep can meet those two hypotheses at one address at most, while every other hypothesis here is about the marker, the mirror and the tracks, which do ride.

theorem DescriptiveComplexity.Draw.Data.evalSpineB_run {L : FirstOrder.Language} (dt : Data L) {A R : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (OuterPh (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (OuterPh (EvalPh dt.nv dt.PMF))] {PR : Prog A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] {v v' : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {rEmb : (i : dt.SEF) → dt.SESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.SESh i), PR.rules (rEmb i ρ) = dt.evalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gtop gbot : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (htop : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (hmV0 : mV a₀ = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) 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 R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), ¬dt.InnerFull (fun (u : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (mV a) u) (stOf : Fin (dt.nv + 1) → TapeStD dt A R (OuterPh (EvalPh dt.nv dt.PMF))) (fsOf : Fin (dt.nv + 1) → dt.CtlIx → A) (hwkOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).wk = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = v) (hbotOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).bot = fun (r : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semTJ : (j : Fin dt.nv) → dt.gatedAt RF j (stOf j.castSucc) → (p : dt.Scratch A R (OuterPh (EvalPh dt.nv dt.PMF))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.igPassP RF PR.zero PR.one (dt.varAt j) (varRdSt (stOf j.castSucc) p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.KindSem PR.zero PR.one (dt.varAt j) (dt.matSt (dt.varAt j) (varRdSt (stOf j.castSucc) p (mV a)) v ↑b) (dt.kindOf (dt.varAt j) b)) (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.legStB RF hord mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) (hfs : ∀ (j : Fin dt.nv), fsOf j.succ = dt.legCtlB RF hord mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) : Relation.ReflTransGen (wideData (Univ A R (OuterPh (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) (fsOf (Fin.last dt.nv))), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stOf (Fin.last dt.nv))) (stOf (Fin.last dt.nv)).val) (PR.syElt PR.blank) }

The evaluation's spine at an arbitrary address: as DescriptiveComplexity.Draw.Data.evalSpine_run_thread with the gates no longer assumed to pass. Each position takes whichever of the three legs its own gates call for, and what the caller owes is only the marker, the mirror and the bottom mark – all of which the advance sets and every leg leaves alone. This is the form a sweep can use, since it visits junk addresses and gated ones alike.