The matrix's stages: the atom runs in the sequencer's shape

The sequencer (DescriptiveComplexity.Draw.seq_run) drives its stages through one uniform interface: entry one cell to the marker's right, one fixed walked track, exit at the next checkpoint. This file wraps the four instantiated atom runs into that shape:

• DescriptiveComplexity.Draw.elem_back – the walk-back a dispatch into an element loop owes (the machinery's own .e0 stay rule);
• DescriptiveComplexity.Draw.Data.stageEndSt_eq – the boundary discipline: a stage atom entered with SAV and TARGET at the home address leaves the state unchanged, so the matrix's background is constant across its atoms;
• the three wrappers cmp_hStage/exp_hStage/stage_hStage, all at the Slot.val-walked presentation of one boundary state – the presentation DescriptiveComplexity.Draw.Data.var_run hands the matrix.

The element loop's walk-back

theorem DescriptiveComplexity.Draw.elem_back {A R P Q W K : 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} {nr : ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ElemPh nr → P} {rdTrack : Fin nr → W} {MatchOf : Fin nr → (Q → A) → (W → A) → Prop} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : (Q → A) → (W → A) → Q → A} {IsMaxEl : (Q → A) → Prop} {exitPh : P} {rEmb : (i : ElemSite nr) → ElemSh nr 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 : ElemSite nr) (ρ : ElemSh nr i), PR.rules (rEmb i ρ) = elemRule PR.one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ) {f : Q → A} : (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb ElemPh.e0) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb ElemPh.e0) 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 an element loop owes: at its entry checkpoint, the walk back down to the marker.

The boundary discipline

theorem DescriptiveComplexity.Draw.Data.stageEndSt_eq {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (hs : st.sav = v) (ht : st.tgt = v) : stageEndSt st v = st

A stage atom entered at the boundary leaves the state unchanged: with SAV and TARGET already at the home address, the restore restores what was there.

theorem DescriptiveComplexity.Draw.Data.trackTape_val_eq_mir {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (st : TapeStD dt A R P) : PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ st) st.val = PR.trackTapeAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir

The val-walked and the mir-walked presentations of one state coincide: both are the naked background.

The comparison atom, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.cmp_hStage {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hordM : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] (vi : dt.VarIx) (av : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf vi)) {emb : ElemPh 2 → P} {exitPh : P} {rEmb : (i : ElemSite 2) → ElemSh 2 i → R} [Finite dt.KIx] (hrules : ∀ (i : ElemSite 2) (ρ : ElemSh 2 i), PR.rules (rEmb i ρ) = elemRule PR.one Slot.wk Slot.reg emb (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).rdTrack (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).MatchOf (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).setFlag (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).initEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).advEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gbot : Univ A R P dt.KIx dt.dd} (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb ElemPh.e0) 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 exitPh ((dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt (cmpFam (laidFile RF hordM) PR.zero PR.one ⋯ vi av hnf isEq j₁ j₂ st v f (toLex topTup) (Fin.last 2)) (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 ⋯ st) st.val) (PR.syElt PR.blank) }

The comparison atom, entered by a dispatch: from its entry checkpoint one cell to the marker's right, at the Slot.val-walked presentation, to the exit phase back at the same cell.

The expansion atom, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.exp_hStage {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hordM : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (e : dt.X.E.Relations k) (av : Fin dt.natMax) (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim) (hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim) {emb : TagPh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) → P} {exitPh : P} {rEmb : (i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)) → TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i → R} [Finite dt.KIx] (hrules : ∀ (i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)) (ρ : TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i), PR.rules (rEmb i ρ) = tagRule PR.one Slot.wk Slot.reg emb (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackT (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchT (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setTagFlag (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).TagsAre (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackE (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchE (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setFlagE (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).initEl (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).advEl (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gbot : Univ A R P dt.KIx dt.dd} (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly PR.zero PR.one (pts ℓ)) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (tagFirstRd emb) 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 exitPh ((dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (fun (ℓ : Fin k) => (↑(pts ℓ)).1) (dt.expFam RF PR.zero PR.one vi ts e av st (fun (ℓ : Fin k) => (↑(pts ℓ)).1) hk hn hrd v (expTagFam RF PR.zero PR.one vi ts e av st hk hn hrd v f (Fin.last (k * Fintype.card dt.X.Tag))) (toLex topTup) (Fin.last (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1))) (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 ⋯ st) st.val) (PR.syElt PR.blank) }

The expansion atom, entered by a dispatch: from its first phase one cell to the marker's right, at the Slot.val-walked presentation, to the exit phase back at the same cell.

The stage atom, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.stage_hStage {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (av : Fin dt.natMax) {emb : StagePh (dt.d.B.arity iv) → P} {exitPh : P} {rEmb : (i : StageSite (dt.d.B.arity iv)) → StageSh (dt.d.B.arity iv) i → R} [Finite dt.KIx] (hrules : ∀ (i : StageSite (dt.d.B.arity iv)) (ρ : StageSh (dt.d.B.arity iv) i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb (dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack (dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk (dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk (dt.stageArgs PR.zero PR.one vi iv ts av).coord (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag (dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv (dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv (dt.stageArgs PR.zero PR.one vi iv ts av).oldSlot (dt.stageArgs PR.zero PR.one vi iv ts av).setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (hsav : st.sav = v) (htgt : st.tgt = v) (b : Bool) (hb : st.old iv (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv)) ↔ b = true) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (StagePh.savP TrackPh.up)) 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 exitPh ((dt.stageArgs PR.zero PR.one vi iv ts av).setAv b (dt.stageFAt RF PR.zero PR.one vi iv ts av st v f (dt.d.B.arity iv)) (dt.back RF.cell PR.zero PR.one ⋯ (stageAtSt st v (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv))) (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv))))), 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) }

The stage atom, entered by a dispatch: at the boundary discipline – SAV and TARGET at the home address – the random access runs and restores the state, so the sequencer's background is untouched.

theorem DescriptiveComplexity.Draw.Data.stage_hStage_thread {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (av : Fin dt.natMax) {emb : StagePh (dt.d.B.arity iv) → P} {exitPh : P} {rEmb : (i : StageSite (dt.d.B.arity iv)) → StageSh (dt.d.B.arity iv) i → R} [Finite dt.KIx] (hrules : ∀ (i : StageSite (dt.d.B.arity iv)) (ρ : StageSh (dt.d.B.arity iv) i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb (dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack (dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk (dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk (dt.stageArgs PR.zero PR.one vi iv ts av).coord (dt.stageArgs PR.zero PR.one vi iv ts av).bitFlag (dt.stageArgs PR.zero PR.one vi iv ts av).setBit (dt.stageArgs PR.zero PR.one vi iv ts av).initLv (dt.stageArgs PR.zero PR.one vi iv ts av).advLv (dt.stageArgs PR.zero PR.one vi iv ts av).IsMaxLv (dt.stageArgs PR.zero PR.one vi iv ts av).oldSlot (dt.stageArgs PR.zero PR.one vi iv ts av).setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) (hwork : ∀ {r : Univ A R P dt.KIx dt.dd → Prop}, ¬r gbot → ∀ (u : Univ A R P dt.KIx dt.dd), WMSetLt WMLe r (RF.cell u)) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = v) (hbotSt : st.bot = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = fun (x : Univ A R P dt.KIx dt.dd) => False) (b : Bool) (hb : st.old iv (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv)) ↔ b = true) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (StagePh.savP TrackPh.up)) 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 exitPh ((dt.stageArgs PR.zero PR.one vi iv ts av).setAv b (dt.stageFAt RF PR.zero PR.one vi iv ts av st v f (dt.d.B.arity iv)) (dt.back RF.cell PR.zero PR.one ⋯ (stageAtSt st v (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv))) (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv))))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.val (dt.back RF.cell PR.zero PR.one ⋯ (stageEndSt st v)) (stageEndSt st v).val) (PR.syElt PR.blank) }

The stage atom, threaded: the same run as DescriptiveComplexity.Draw.Data.stage_hStage with no boundary discipline assumed – the random access writes the home address into SAV and TARGET whatever they held, so its exit state is the normalized DescriptiveComplexity.Draw.Data.stageEndSt st v rather than st.

This is the form the outer sweep needs: at a swept address SAV and TARGET still hold the previous address (the advance refreshes only the marker and the mirror), so stage_hStage's two hypotheses are unavailable there and the normalization has to be carried instead of assumed.

One gate block, in the sequencer's shape

theorem DescriptiveComplexity.Draw.Data.gateBlock_hStage_pos {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (b : Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) {emb : dt.GateBlockPh → P} (wellG : (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {failPh exitPh : P} {rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i), PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.gateArgs PR.zero PR.one b hc hn hrd) wellG setFail failPh exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : Univ A R P dt.KIx dt.dd → Prop) (hcompat : ∀ (u : Univ A R P dt.KIx dt.dd), wellG (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ Test u) (t : dt.X.Tag) (htag : dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex b))) = t) (hTest : ∀ (u : Univ A R P dt.KIx dt.dd), Test u) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) 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 exitPh ((dt.gateArgs PR.zero PR.one b hc hn hrd).exitSt t (dt.gateFam RF PR.zero PR.one b st t hc hn hrd v (dt.gateTagFam RF PR.zero PR.one b st hc hn hrd v f (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup) (Fin.last (dt.domNr t))) (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 ⋯ st) st.val) (PR.syElt PR.blank) }

A passing gate block, entered by a dispatch: every register is well-shaped, so the file test passes, the domain evaluation runs on the block's decoded tag, and the block exits to the next checkpoint.

theorem DescriptiveComplexity.Draw.Data.gateBlock_hStage_neg {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (b : Fin dt.ko ⊕ Fin dt.ki) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) {emb : dt.GateBlockPh → P} (wellG : (dt.SlotIx → A) → Prop) (setFail : (dt.CtlIx → A) → (dt.SlotIx → A) → dt.CtlIx → A) {failPh exitPh : P} {rEmb : (i : dt.GateBlockSite) → dt.GateBlockSh i → R} [Finite dt.KIx] (hrules : ∀ (i : dt.GateBlockSite) (ρ : dt.GateBlockSh i), PR.rules (rEmb i ρ) = dt.gateBlockRule PR.one emb (dt.gateArgs PR.zero PR.one b hc hn hrd) wellG setFail failPh exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A R P dt.KIx dt.dd} (htop : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeStD dt A R P} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (Test : Univ A R P dt.KIx dt.dd → Prop) (hcompat : ∀ (u : Univ A R P dt.KIx dt.dd), wellG (PR.passTracksAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir (RF.cell u)) ↔ Test u) {u : Univ A R P dt.KIx dt.dd} (hTest : ¬Test u) (f : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (Sum.inl TestPh.up)) 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 failPh (setFail 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 ⋯ st) st.val) (PR.syElt PR.blank) }

A failing gate block: some register is not well-shaped, so the file test fails and the block leaves the whole gate sequence through the failing exit, the fail store applied at the marker's symbol.