The tuple loop's run

The run theorem of DescriptiveComplexity.Draw.tupleRule: per enumerated tuple, a read trip at the source cell, the bit stored into the control, a write trip at the destination cell reading it back, and the advance – so the loop copies a bit per round, and the destination track evolves.

That evolution is what distinguishes this statement from the element loop's: the background is a family over the enumeration, each round's write moving the destination track from mD a to DescriptiveComplexity.Draw.tuplePost – the update at the round's destination cell with the round's source bit – and the next round's background carrying exactly that. Everything else follows the established shape: an abstract finite linear order for the enumeration, control families fs0/fs1 around the store, and the loop closed by DescriptiveComplexity.Draw.reflTransGen_of_ordLoop.

def DescriptiveComplexity.Draw.tuplePost {I ι : Type} (mSrc : I → Prop) (mD : ι → I → Prop) (xS xD : ι → I) (a : ι) : I → Prop

The destination track after a round's write: the round's source bit at its destination cell, everything else untouched.

Equations

• DescriptiveComplexity.Draw.tuplePost mSrc mD xS xD a y = (y = xD a ∧ mSrc (xS a) ∨ y ≠ xD a ∧ mD a y)

theorem DescriptiveComplexity.Draw.tuple_run {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} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ChainPh 3 TuplePS → P} {tSrc tDst : W} {MatchS MatchD : (Q → A) → (W → A) → Prop} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (W → A) → Q → A} {initLv advLv : (Q → A) → (W → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {exitPh : P} {rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R} (hrules : ∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i), PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {ι : Type} [LinearOrder ι] [Finite ι] {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) {restOf : ι → (Univ A R P K dd → Prop) → W → A} {mSrc : I → Prop} {mD : ι → I → Prop} (hwkS : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hsrc : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r tSrc = bitVal PR.zero PR.one (bitAtOf RF.cell mSrc r)) (hdst : ∀ (a : ι) (r : Univ A R P K dd → Prop), restOf a r tDst = bitVal PR.zero PR.one (bitAtOf RF.cell (mD a) r)) (hwkSrc : wk ≠ tSrc) (hwkDst : wk ≠ tDst) (hrgSrc : rg ≠ tSrc) (hrgDst : rg ≠ tDst) (xS xD : ι → I) (fs0 fs1 : ι → Q → A) (hnameS : ∀ (a : ι), MatchS (fs0 a) (PR.passTracksAt RF.cell tSrc (restOf a) mSrc (RF.cell (xS a)))) (huniqS : ∀ (a : ι) (r : Univ A R P K dd → Prop), MatchS (fs0 a) (PR.passTracksAt RF.cell tSrc (restOf a) mSrc r) → r = RF.cell (xS a)) (hnameD : ∀ (a : ι), MatchD (fs1 a) (PR.passTracksAt RF.cell tDst (restOf a) (mD a) (RF.cell (xD a)))) (huniqD : ∀ (a : ι) (r : Univ A R P K dd → Prop), MatchD (fs1 a) (PR.passTracksAt RF.cell tDst (restOf a) (mD a) r) → r = RF.cell (xD a)) (hstoreT : ∀ (a : ι), mSrc (xS a) → fs1 a = setBit true (fs0 a) (restOf a v)) (hstoreF : ∀ (a : ι), ¬mSrc (xS a) → fs1 a = setBit false (fs0 a) (restOf a v)) (hbitFlag : ∀ (a : ι), bitFlag (fs1 a) ↔ mSrc (xS a)) (hadv : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → advLv (fs1 a) (restOf a v) = fs0 a') (hcov : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → ∀ (y : I), mD a' y ↔ tuplePost mSrc mD xS xD a y) (hagree : ∀ (a a' : ι), a < a' → (∀ (b : ι), ¬(a < b ∧ b < a')) → ∀ (r : Univ A R P K dd → Prop) (s : W), s ≠ tDst → restOf a' r s = restOf a r s) (hmaxT : IsMaxLv (fs1 aT)) (hmaxF : ∀ a < aT, ¬IsMaxLv (fs1 a)) {f₀ : Q → A} (hinit : initLv f₀ (restOf a₀ v) = fs0 a₀) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, tuple_run._proof_1⟩)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell tSrc (restOf a₀) mSrc) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (fs1 aT)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell tDst (restOf aT) (tuplePost mSrc mD xS xD aT)) (PR.syElt PR.blank) }

The tuple loop'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 loop takes.