The stage atoms, instantiated: the copy loops

The second semantic instantiation: the tuple loops of a stage atom's machinery, at the pack DescriptiveComplexity.Draw.Data.stageArgs. Each argument position runs one copy loop – a read at the source block's cell, the bit through the control's copy flag, a write at the TARGET block's cell – and this file proves its three invariants and its run:

• DescriptiveComplexity.Draw.Data.readLv_stageIter0/_stageIter1 – the loop element is the round's tuple, before and after the store;
• DescriptiveComplexity.Draw.Data.stageIterD_iff – the closed form of the destination track: a cell holds a bit exactly when some round already wrote it – the round's source bit – or it held one from the start and no round has touched it;
• DescriptiveComplexity.Draw.Data.stageTuple_run – the copy loop's run at the generated families, by DescriptiveComplexity.Draw.tuple_run_iter with the name guards discharged through DescriptiveComplexity.Draw.Data.nameG_iff.

The chaining of the k loops and the whole stage atom's run assemble on top, with DescriptiveComplexity.Draw.Data.stage_run.

noncomputable def DescriptiveComplexity.Draw.Data.stageXS {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (zero : A) (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)) : Univ A R P dt.KIx dt.dd

The source cell of a copy round: the padded cell of the round's tuple in the position's source block.

Equations

• dt.stageXS zero vi iv ts ℓ b = dt.blkElt (dt.lvBlk vi (ts ℓ)) (DescriptiveComplexity.Draw.pad zero (ofLex b))

noncomputable def DescriptiveComplexity.Draw.Data.stageXD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (zero : A) (iv : dt.d.B.ι) (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)) : Univ A R P dt.KIx dt.dd

The destination cell of a copy round: the padded cell of the round's tuple in the TARGET block of the position.

Equations

• dt.stageXD zero iv ℓ b = dt.blkElt (Sum.inl (Fin.castLE ⋯ ℓ)) (DescriptiveComplexity.Draw.pad zero (ofLex b))

noncomputable def DescriptiveComplexity.Draw.Data.stageRestF {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) (zero one : A) (st : TapeStD dt A R P) (m' : Univ A R P dt.KIx dt.dd → Prop) : (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A

The background of a copy loop, as a function of the destination content: the state with the TARGET register at the given track.

Equations

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

theorem DescriptiveComplexity.Draw.Data.stageRestF_off {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) {zero one : A} {st : TapeStD dt A R P} (m₁ m₂ r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx) (hs : s ≠ Slot.tgt) : dt.stageRestF RF zero one st m₁ r s = dt.stageRestF RF zero one st m₂ r s

The destination-dependent background moves only at the TARGET slot.

The loop element through the copy's operations

theorem DescriptiveComplexity.Draw.Data.readLv_setCtl_bitFlagC {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (b : Prop) (f : dt.CtlIx → A) : dt.readLv (dt.setCtl zero one dt.bitFlagC b f) = dt.readLv f

The loop element rides along the copied bit's store.

theorem DescriptiveComplexity.Draw.Data.readLv_stageIter0 {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (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} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {vAdr mD₀ : Univ A R P dt.KIx dt.dd → Prop} {f₀ : dt.CtlIx → A} {zero one : A} (b : Lex (Fin dt.dd0 → A)) : dt.readLv (tupleIter0 (dt.stageArgs zero one vi iv ts av).setBit (dt.stageArgs zero one vi iv ts av).initLv (dt.stageArgs zero one vi iv ts av).advLv (dt.lvSet st vi (ts ℓ)) vAdr (dt.stageRestF RF zero one st) (dt.stageXS zero vi iv ts ℓ) (dt.stageXD zero iv ℓ) mD₀ f₀ b) = ofLex b

The copy loop's generated round tuples: the pre-store control's loop element is the round's tuple.

theorem DescriptiveComplexity.Draw.Data.readLv_stageIter1 {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (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} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {vAdr mD₀ : Univ A R P dt.KIx dt.dd → Prop} {f₀ : dt.CtlIx → A} {zero one : A} (b : Lex (Fin dt.dd0 → A)) : dt.readLv (tupleIter1 (dt.stageArgs zero one vi iv ts av).setBit (dt.stageArgs zero one vi iv ts av).initLv (dt.stageArgs zero one vi iv ts av).advLv (dt.lvSet st vi (ts ℓ)) vAdr (dt.stageRestF RF zero one st) (dt.stageXS zero vi iv ts ℓ) (dt.stageXD zero iv ℓ) mD₀ f₀ b) = ofLex b

The post-store control's loop element is still the round's tuple.

The built TARGET, in closed form

theorem DescriptiveComplexity.Draw.Data.stageXD_injective {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {iv : dt.d.B.ι} {ℓ : Fin (dt.d.B.arity iv)} {zero : A} (b b' : Lex (Fin dt.dd0 → A)) (h : dt.stageXD zero iv ℓ b = dt.stageXD zero iv ℓ b') : b = b'

The destination cells are distinct: the padded cell of a tuple determines the tuple.

theorem DescriptiveComplexity.Draw.Data.stageIterD_iff {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {mD₀ : Univ A R P dt.KIx dt.dd → Prop} {zero : A} (b : Lex (Fin dt.dd0 → A)) (y : Univ A R P dt.KIx dt.dd) : tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS zero vi iv ts ℓ) (dt.stageXD zero iv ℓ) mD₀ b y ↔ (∃ u < b, y = dt.stageXD zero iv ℓ u ∧ dt.lvSet st vi (ts ℓ) (dt.stageXS zero vi iv ts ℓ u)) ∨ (∀ u < b, y ≠ dt.stageXD zero iv ℓ u) ∧ mD₀ y

The built TARGET block, in closed form: a cell of the copy loop's destination holds a bit exactly when it is the destination cell of some tuple whose source bit is set – the loop having visited every tuple – or it held one from the start, off the loop's cells.

The copy loop's run

theorem DescriptiveComplexity.Draw.Data.stageTuple_run {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {av : Fin dt.natMax} {ℓ : Fin (dt.d.B.arity iv)} {st : TapeStD dt A R P} {emb : ChainPh 3 TuplePS → P} {exitPh : P} {rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R} [Finite dt.KIx] (hrules : ∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i), PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one Slot.wk Slot.reg emb ((dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack ℓ) Slot.tgt (dt.nameG PR.one ((dt.stageArgs PR.zero PR.one vi iv ts av).srcBlk ℓ) dt.lvC) (dt.nameG PR.one ((dt.stageArgs PR.zero PR.one vi iv ts av).dstBlk ℓ) dt.lvC) (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 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') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (mD₀ : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, ⋯⟩)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell ((dt.stageArgs PR.zero PR.one vi iv ts av).srcTrack ℓ) (dt.stageRestF RF PR.zero PR.one st (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀ (toLex botTup))) (dt.lvSet st vi (ts ℓ))) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (tupleIter1 (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.lvSet st vi (ts ℓ)) v (dt.stageRestF RF PR.zero PR.one st) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀ f₀ (toLex topTup))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.tgt (dt.stageRestF RF PR.zero PR.one st (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀ (toLex topTup))) (tuplePost (dt.lvSet st vi (ts ℓ)) (tupleIterD (dt.lvSet st vi (ts ℓ)) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) mD₀) (dt.stageXS PR.zero vi iv ts ℓ) (dt.stageXD PR.zero iv ℓ) (toLex topTup))) (PR.syElt PR.blank) }

One copy loop's run: from its entry checkpoint at the marker to the exit phase one cell to its right, the TARGET block of the position holding the source block's bits at every tuple's cell.

The copy loops, chained: the TARGET built position by position

Position ℓ's loop copies its source block over what the earlier positions built. The composed content and the control each thread through by one recursion, DescriptiveComplexity.Draw.Data.stage_loops_run chains the runs – every handover a backed-track equality – and DescriptiveComplexity.Draw.Data.stage_run closes the whole random access over the chain.

noncomputable def DescriptiveComplexity.Draw.Data.stageTgtD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] (zero : A) (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) : ℕ → Univ A R P dt.KIx dt.dd → Prop

The TARGET after the first n copy loops: each position's loop writes its source bits at its destination cells over what the earlier positions built.

Equations

• One or more equations did not get rendered due to their size.
• dt.stageTgtD zero vi iv ts st v 0 = fun (x : DescriptiveComplexity.Draw.Univ A R P dt.KIx dt.dd) => False

theorem DescriptiveComplexity.Draw.Data.stageTgtD_arg {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) {y : Univ A R P dt.KIx dt.dd} (hy : dt.stageTgtD zero vi iv ts st v n y) : ∃ (i : dt.KIx), y.1 = Tag.arg i

The target of a random access is an address of argument cells alone: every cell it holds was written by a copy round, at that round's destination (stageXD, in an argument block), over the empty address. This is wmSetLe_logicalTop's hypothesis, and so the first half of «the address a stage atom reads lies in the logical interval».

theorem DescriptiveComplexity.Draw.Data.stageTgtD_isPad {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) {y : Univ A R P dt.KIx dt.dd} (hy : dt.stageTgtD zero vi iv ts st v n y) : IsPad dt.dd0 zero y.2

The target of a random access is padded: every cell it holds is a destination cell, and those carry the round's tuple in the name slots and zero beyond them (stageXD writes pad). With stageTgtD_arg this is what places the address strictly below the logical top, whose blocks are full.

theorem DescriptiveComplexity.Draw.Data.wmSetLt_stageTgtD_logicalTop {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [Finite A] [Finite R] [Finite P] [Nonempty A] {zero one : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (hne : zero ≠ one) (hV : IsLinOrd tupLeLex) (hd : dt.dd0 < dt.dd) (i : dt.KIx) (n : ℕ) : WMSetLt (lexRel (fun (x1 x2 : Tag R P dt.KIx) => x1 ≤ x2) tupLeLex) (dt.stageTgtD zero vi iv ts st v n) logicalTop

The address a stage atom reads lies in the logical interval: it is built from padded destination cells in argument blocks alone (stageTgtD_arg, stageTgtD_isPad), which is exactly wmSetLt_logicalTop_of_isPad. This is the hbelow the dictionary invariant of DescriptiveComplexity.Draw.Data.stageSt_old is owed: the invariant is an equivalence over the interval and nowhere else, so an address that is read has to be shown to lie there.

noncomputable def DescriptiveComplexity.Draw.Data.stageFAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] (zero one : A) (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (av : Fin dt.natMax) (st : TapeStD dt A R P) (v : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) : ℕ → dt.CtlIx → A

The control after the first n copy loops.

Equations

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

theorem DescriptiveComplexity.Draw.Data.stageTgtD_congr_scratch {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (n : ℕ) : dt.stageTgtD zero vi iv ts st v n = dt.stageTgtD zero vi iv ts st' v n

The TARGET a random access builds is blind to the two scratch registers: every copy round reads a level's register set, and the loop pins SAV at the home address itself.

theorem DescriptiveComplexity.Draw.Data.stageFAt_congr_scratch {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] {zero one : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), v = RF.cell u) (f₀ : dt.CtlIx → A) (n : ℕ) : dt.stageFAt RF zero one vi iv ts av st v f₀ n = dt.stageFAt RF zero one vi iv ts av st' v f₀ n

The control of the copy loops is blind to them too – the destination-dependent background overwrites TARGET, and the loop reads it at the home cell alone.

theorem DescriptiveComplexity.Draw.Data.stageXD_pos_eq {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {zero : A} {iv : dt.d.B.ι} {ℓ ℓ' : Fin (dt.d.B.arity iv)} {u u' : Lex (Fin dt.dd0 → A)} (h : dt.stageXD zero iv ℓ u = dt.stageXD zero iv ℓ' u') : ℓ = ℓ'

Distinct positions write distinct blocks: the cell of a copy round names the position that wrote it.

theorem DescriptiveComplexity.Draw.Data.stageTgtD_iff {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} (n : ℕ) (y : Univ A R P dt.KIx dt.dd) : dt.stageTgtD zero vi iv ts st v n y ↔ ∃ (ℓ : Fin (dt.d.B.arity iv)) (u : Lex (Fin dt.dd0 → A)), ↑ℓ < n ∧ y = dt.stageXD zero iv ℓ u ∧ dt.lvSet { mir := st.mir, tgt := st.tgt, sav := v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } vi (ts ℓ) (dt.stageXS zero vi iv ts ℓ u)

The composed TARGET, in closed form: after the first n loops a cell holds a bit exactly when some position below n copied it there – the source block's bit at the same tuple. Distinct positions write distinct blocks, so the loops never collide and the disjunction is honest.

theorem DescriptiveComplexity.Draw.Data.stageTgtD_mem {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero : A} {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {n : ℕ} {y : Univ A R P dt.KIx dt.dd} (h : dt.stageTgtD zero vi iv ts st v n y) : ∃ (ℓ : Fin (dt.d.B.arity iv)) (u : Lex (Fin dt.dd0 → A)), y = dt.stageXD zero iv ℓ u

Every cell of the composed TARGET is some position's destination cell.

theorem DescriptiveComplexity.Draw.Data.stageChain_run {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {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) {gbot : Univ A R P dt.KIx dt.dd} (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = v) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (stageFirstTup emb) ((dt.stageArgs PR.zero PR.one vi iv ts av).initLv f₀ (dt.back RF.cell PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : Univ A R P dt.KIx dt.dd) => False, sav := v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp } v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : Univ A R P dt.KIx dt.dd) => False, sav := v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) v) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) (dt.stageFAt RF PR.zero PR.one vi iv ts av st v f₀ (dt.d.B.arity iv))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.mir (dt.back RF.cell PR.zero PR.one ⋯ { mir := st.mir, tgt := dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv), sav := v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) v) (PR.syElt PR.blank) }

The copy loops of a stage atom, chained and instantiated: from the phase entering the first loop to the first reset's checkpoint, the TARGET holding the composed content of every position – exactly the hLoops leg of DescriptiveComplexity.Draw.Data.stage_run.

theorem DescriptiveComplexity.Draw.Data.stageAtom_run {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)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] {vi : dt.VarIx} {iv : dt.d.B.ι} {ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)} {av : Fin dt.natMax} {st : TapeStD dt A R P} {v : Univ A R P dt.KIx dt.dd → Prop} {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) {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' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (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) (f₀ : dt.CtlIx → A) (b : Bool) (hb : st.old iv (dt.stageTgtD PR.zero vi iv ts st v (dt.d.B.arity iv)) ↔ b = true) : 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.mir (dt.back RF.cell PR.zero PR.one ⋯ st) st.mir) (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.mir (dt.back RF.cell PR.zero PR.one ⋯ (stageEndSt st v)) (stageEndSt st v).mir) (PR.syElt PR.blank) }

The stage atom's run, fully instantiated: from its entry phase to the exit phase, the verdict – the old track's bit at the cell the built TARGET addresses – stored in the atom's control slot, the marker, mirror and save restored at the home address. Every leg of the random access is closed: the save, the clear, the copy loops with their composed content, the seek out, the read under the head, the restore and the seek home.