The stage atom's run

The run theorem of DescriptiveComplexity.Draw.Data.stageRule – the random access. The tuple loops stay abstract (one hypothesis for the whole chain, discharged by DescriptiveComplexity.Draw.tuple_run at instantiation); this file contributes the itinerary around them: save the mirror, clear the target, run the loops, reset, clear the mirror, seek the target, read the stage bit under the head, restore the target, and come home the same way.

The statement is in the DescriptiveComplexity.Draw.TapeSt idiom: the machine's mutable state is a record, each leg one update, and every slot equation a kit asks for is definitional in DescriptiveComplexity.Draw.Data.ixBack; the handoff between legs walking different tracks is DescriptiveComplexity.Draw.Data.trackTape_back_gen.

The file is a parameter. A clocked program has no register per element, so the run is stated at an arbitrary DescriptiveComplexity.Draw.LaidFile with the address correspondence of DescriptiveComplexity.Problems.Wide.IxAddr: what the mirror, the save and the target hold are the marks of their addresses (DescriptiveComplexity.ixMark), and the seek's verdict is again an equality of addresses because the correspondence carries the order. The elementwise file is that at the identity (DescriptiveComplexity.Draw.Data.diagLaid), which is what stageAtSt, stageEndSt and trackTape_back_gen_diag are.

noncomputable def DescriptiveComplexity.Draw.Data.ixStageAtSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) (v mT : Univ A R P dt.KIx dt.dd → Prop) : TapeSt dt A R P I

The state at the far end of the random access: marker and mirror on the target, the mirror's address saved, the target built.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixStageEndSt {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (elt : I → Univ A R P dt.KIx dt.dd) (v : Univ A R P dt.KIx dt.dd → Prop) : TapeSt dt A R P I

The state the random access returns in: the target and the save both holding the home address, everything else as at entry.

Equations

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

theorem DescriptiveComplexity.Draw.Data.trackTape_back_gen {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} [Fintype Q] [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 Q dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {stA stB : TapeSt dt A R P I} {t : dt.SlotIx} {m : I → Prop} (hagree : ∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx), s ≠ t → dt.ixBack F.toLayout PR.zero PR.one ⋯ stA r s = dt.ixBack F.toLayout PR.zero PR.one ⋯ stB r s) (ht : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), dt.ixBack F.toLayout PR.zero PR.one ⋯ stB r t = bitVal PR.zero PR.one (bitAtOf F.cell m r)) : PR.trackTapeAt F.cell t (dt.ixBack F.toLayout PR.zero PR.one ⋯ stA) m = fun (r : Univ A R P dt.KIx dt.dd → Prop) => PR.syElt (dt.ixBack F.toLayout PR.zero PR.one ⋯ stB r)

A leg's after-tape, read against the state it produced: the walked track moves into the new state's background, whose other slots agree with the old one's. The generic sibling of the concrete DescriptiveComplexity.Draw.Data.trackTape_back.

theorem DescriptiveComplexity.Draw.Data.stage_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} {k : ℕ} [Fintype Q] [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 Q dt.SlotIx dt.KIx dt.dd} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) {emb : StagePh k → P} {srcTrack : Fin k → dt.SlotIx} {srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {oldSlot : dt.SlotIx} {setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {exitPh : P} {rEmb : (i : StageSite k) → StageSh k i → R} (hrules : ∀ (i : StageSite k) (ρ : StageSh k i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd F.le) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeSt dt A R P I} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = ixMark elt 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) {mT : Univ A R P dt.KIx dt.dd → Prop} (hTh : IxHolds elt Use mT) (hvh : IxHolds elt Use v) (hT : WMSetLt WMLe mT (F.cell gbot)) {T' : Univ A R P dt.KIx dt.dd → Prop} (hTi : WMIncr WMLe mT T') {f₀ fL : Q → A} {b : Bool} (hbT : dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v mT) mT oldSlot = PR.one ↔ b = true) (holdmir : oldSlot ≠ Slot.mir) {wG : ℕ} (hgap : ∀ (u u' : I), IxSucc F.le u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ wG) (wP wR wK wL : ℕ) (hwP : wideRank (F.cell gtop) + 2 + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) ≤ wP) (hwR : ∀ (s : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe s (F.cell gbot) → wideRank s + 4 ≤ wR) (hwK : ∀ (T : Univ A R P dt.KIx dt.dd → Prop), WMSetLt WMLe T (F.cell gbot) → wideRank T * (1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) + (wideRank (F.cell gtop) + ((ixRank F.le gtop - ixRank F.le gbot) * wG + 1) + wideRank (F.cell gbot) + 4)) + 1 + (wideRank (F.cell gtop) + 3 + (ixRank F.le gtop - ixRank F.le gbot) * wG + wideRank (F.cell gbot)) ≤ wK) (hLoopsIn : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn wL { state := Sum.inr (PR.stElt (stageFirstTup emb) (initLv f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : I) => False, sav := ixMark elt 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 F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : I) => False, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (ixMark elt v)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) fL), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := ixMark elt mT, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (ixMark elt v)) (PR.syElt PR.blank) }) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn (5 * wP + 2 * wR + 2 * wK + wL + 13) { state := Sum.inr (PR.stElt (emb (StagePh.savP TrackPh.up)) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (setAv b fL (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v mT) mT))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageEndSt st elt v)) (dt.ixStageEndSt st elt v).mir) (PR.syElt PR.blank) }

The stage atom's run, on a clock: from its entry phase one cell to the right of the marker – save, clear, the loops, the reset–clear–seek out, the read under the head, the restore, and the reset–clear–seek home – to the exit phase, the verdict setAv b in the control and the marker, mirror and save restored at the home address. Five passes of the file, two resets, two seeks, the loops, and the thirteen dispatches between them.

theorem DescriptiveComplexity.Draw.Data.stage_run {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} {k : ℕ} [Fintype Q] [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 Q dt.SlotIx dt.KIx dt.dd} {I : Type} [Finite I] (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} {Use : I → Prop} (hinj : Function.Injective elt) (hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u')) (hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x) {emb : StagePh k → P} {srcTrack : Fin k → dt.SlotIx} {srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {oldSlot : dt.SlotIx} {setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {exitPh : P} {rEmb : (i : StageSite k) → StageSh k i → R} (hrules : ∀ (i : StageSite k) (ρ : StageSh k i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd F.le) {gtop gbot : I} (htop : ∀ (y : I), F.le y gtop) (hbot : ∀ (y : I), F.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeSt dt A R P I} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (hmirSt : st.mir = ixMark elt 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) {mT : Univ A R P dt.KIx dt.dd → Prop} (hTh : IxHolds elt Use mT) (hvh : IxHolds elt Use v) (hT : WMSetLt WMLe mT (F.cell gbot)) {T' : Univ A R P dt.KIx dt.dd → Prop} (hTi : WMIncr WMLe mT T') {f₀ fL : Q → A} (hLoops : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (stageFirstTup emb) (initLv f₀ (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : I) => False, sav := ixMark elt 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 F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := fun (x : I) => False, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (ixMark elt v)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) fL), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := ixMark elt mT, sav := ixMark elt v, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (ixMark elt v)) (PR.syElt PR.blank) }) {b : Bool} (hbT : dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v mT) mT oldSlot = PR.one ↔ b = true) (holdmir : oldSlot ≠ Slot.mir) : 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 F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (setAv b fL (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageAtSt st elt v mT) mT))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixStageEndSt st elt v)) (dt.ixStageEndSt st elt v).mir) (PR.syElt PR.blank) }

The stage atom's run, the budget forgotten: what a space-bounded caller reads. The width of a trip is then the largest of the finitely many the atom takes.

The chain of the copy loops

The k tuple loops run head to tail – position ℓ's exit is DescriptiveComplexity.Draw.Data.stageNextTup emb ℓ – so their chain is one induction over the positions, each round an abstract per-position run (discharged by the copy loop's instantiation) between the walk-backs this file's rules provide.

def DescriptiveComplexity.Draw.Data.stagePhaseAt {P : Type} {k : ℕ} (emb : StagePh k → P) (n : ℕ) : P

The phase before the n-th copy loop – the first reset's checkpoint once the positions are exhausted.

Equations

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

theorem DescriptiveComplexity.Draw.Data.stage_loops_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} {k : ℕ} [Fintype Q] [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 Q dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {emb : StagePh k → P} {srcTrack : Fin k → dt.SlotIx} {srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {oldSlot : dt.SlotIx} {setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {exitPh : P} {rEmb : (i : StageSite k) → StageSh k i → R} (hrules : ∀ (i : StageSite k) (ρ : StageSh k i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (trkOf : Fin (k + 1) → dt.SlotIx) (restOf : Fin (k + 1) → (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A) (mOf : Fin (k + 1) → I → Prop) (hwkOf : ∀ (ℓ : Fin (k + 1)) (r : Univ A R P dt.KIx dt.dd → Prop), restOf ℓ r Slot.wk = bitVal PR.zero PR.one (r = v)) (hwkTrk : ∀ (ℓ : Fin (k + 1)), Slot.wk ≠ trkOf ℓ) (fAt : Fin (k + 1) → Q → A) (wT : ℕ) (hLoopIn : ∀ (ℓ : Fin k), (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn wT { state := Sum.inr (PR.stElt (emb (StagePh.tupP ℓ (ChainPh.chk ⟨0, ⋯⟩))) (fAt ℓ.castSucc)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell (trkOf ℓ.castSucc) (restOf ℓ.castSucc) (mOf ℓ.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (stageNextTup emb ℓ) (fAt ℓ.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf ℓ.succ) (restOf ℓ.succ) (mOf ℓ.succ)) (PR.syElt PR.blank) }) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((wT + 1) * k) { state := Sum.inr (PR.stElt (stageFirstTup emb) (fAt 0)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf 0) (restOf 0) (mOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) (fAt (Fin.last k))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf (Fin.last k)) (restOf (Fin.last k)) (mOf (Fin.last k))) (PR.syElt PR.blank) }

The copy loops, chained, on a clock: from the phase entering the first loop – one cell to the marker's right, as every dispatch leaves it – to the first reset's checkpoint, each position's run handed to the next by its own walk-back, and one walk-back and one loop paid per position.

theorem DescriptiveComplexity.Draw.Data.stage_loops_run {L : FirstOrder.Language} (dt : Data L) {A R P Q : Type} {k : ℕ} [Fintype Q] [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 Q dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {emb : StagePh k → P} {srcTrack : Fin k → dt.SlotIx} {srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {initLv advLv : (Q → A) → (dt.SlotIx → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {oldSlot : dt.SlotIx} {setAv : Bool → (Q → A) → (dt.SlotIx → A) → Q → A} {exitPh : P} {rEmb : (i : StageSite k) → StageSh k i → R} (hrules : ∀ (i : StageSite k) (ρ : StageSh k i), PR.rules (rEmb i ρ) = dt.stageRule PR.zero PR.one emb srcTrack srcBlk dstBlk coord bitFlag setBit initLv advLv IsMaxLv oldSlot setAv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (trkOf : Fin (k + 1) → dt.SlotIx) (restOf : Fin (k + 1) → (Univ A R P dt.KIx dt.dd → Prop) → dt.SlotIx → A) (mOf : Fin (k + 1) → I → Prop) (hwkOf : ∀ (ℓ : Fin (k + 1)) (r : Univ A R P dt.KIx dt.dd → Prop), restOf ℓ r Slot.wk = bitVal PR.zero PR.one (r = v)) (hwkTrk : ∀ (ℓ : Fin (k + 1)), Slot.wk ≠ trkOf ℓ) (fAt : Fin (k + 1) → Q → A) (hLoop : ∀ (ℓ : Fin k), Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb (StagePh.tupP ℓ (ChainPh.chk ⟨0, ⋯⟩))) (fAt ℓ.castSucc)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell (trkOf ℓ.castSucc) (restOf ℓ.castSucc) (mOf ℓ.castSucc)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (stageNextTup emb ℓ) (fAt ℓ.succ)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf ℓ.succ) (restOf ℓ.succ) (mOf ℓ.succ)) (PR.syElt PR.blank) }) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (stageFirstTup emb) (fAt 0)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf 0) (restOf 0) (mOf 0)) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (emb StagePh.cR1) (fAt (Fin.last k))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell (trkOf (Fin.last k)) (restOf (Fin.last k)) (mOf (Fin.last k))) (PR.syElt PR.blank) }

The copy loops, chained, the budget forgotten: from the phase entering the first loop – one cell to the marker's right, as every dispatch leaves it – to the first reset's checkpoint, each position's run handed to the next by its own walk-back.

The elementwise instantiation

The space-bounded program's file is the input channel's ruler, one register per element: the runs above are that file at the identity embedding, and these are the statements their callers had before the file became a parameter.

noncomputable def DescriptiveComplexity.Draw.Data.stageAtSt {L : FirstOrder.Language} {dt : Data L} {A R P : Type} (st : TapeStD dt A R P) (v mT : Univ A R P dt.KIx dt.dd → Prop) : TapeStD dt A R P

The far state of the random access at the elementwise file.

Equations

• DescriptiveComplexity.Draw.Data.stageAtSt st v mT = dt.ixStageAtSt st id v mT

noncomputable def DescriptiveComplexity.Draw.Data.stageEndSt {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) : TapeStD dt A R P

The state the random access returns in, at the elementwise file.

Equations

• DescriptiveComplexity.Draw.Data.stageEndSt st v = dt.ixStageEndSt st id v

theorem DescriptiveComplexity.Draw.Data.trackTape_back_gen_diag {L : FirstOrder.Language} {dt : Data L} {A R P Q : Type} [Fintype Q] [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 Q 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) {stA stB : TapeStD dt A R P} {t : dt.SlotIx} {m : Univ A R P dt.KIx dt.dd → Prop} (hagree : ∀ (r : Univ A R P dt.KIx dt.dd → Prop) (s : dt.SlotIx), s ≠ t → dt.back RF.cell PR.zero PR.one ⋯ stA r s = dt.back RF.cell PR.zero PR.one ⋯ stB r s) (ht : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), dt.back RF.cell PR.zero PR.one ⋯ stB r t = bitVal PR.zero PR.one (bitAtOf RF.cell m r)) : PR.trackTapeAt RF.cell t (dt.back RF.cell PR.zero PR.one ⋯ stA) m = fun (r : Univ A R P dt.KIx dt.dd → Prop) => PR.syElt (dt.back RF.cell PR.zero PR.one ⋯ stB r)

A leg's after-tape at the elementwise file.