ADVANCE: moving the working cell one address, mirror in tow

The round every sweep of the EXPSPACE program repeats: erase the working-cell marker and step right; write it at the next address and step on; scan up to the top of the register file; bounce – the scan cannot overshoot the maximal cell, so entering the downward pass costs two steps, left to the top's predecessor and back right, changing phase; run the mirror increment down the file (DescriptiveComplexity.Draw.Prog.reaches_fileIncr); scan back down to the marker.

DescriptiveComplexity.Draw.Prog.reaches_fileAdvance is the whole round, and the first composite of the layer: two Prog.step_moves, a Prog.reaches_toCell, two bounce steps, a pass and a Prog.reaches_toCellBack, chained by Relation.ReflTransGen. Its hypotheses are the six rule families of the phases it visits plus the background's slot equations, and nothing else – which is the evidence the pass layer's interfaces (the element-valued background, the cell-coupled walking rules, the stop-ahead bounds) are the right ones: every one of them is consumed here.

The working cell and its successor lie strictly below the register file, so the cell-coupled walking hypotheses – whose cells are all at or above a register – never meet the marker, and one rule family per walking phase serves both the pass's descent and the return scan.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_fileAdvance {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] {I : Type} [Finite I] {ile : I → I → Prop} {PR : Prog A R P Q W K dd} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t rg rl wk : W} (hnerg : t ≠ rg) (hnerl : rl ≠ t) (hnewk : wk ≠ t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v v') (hv' : WMSetLt WMLe v' (F.cell gbot)) {m m' : I → Prop} (him : WMIncr ile m m') {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), r ≠ v' → restB r = restN r) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r wk = bitVal PR.zero PR.one (r = v')) (hrgB : ∀ (r : Univ A R P K dd → Prop), restB r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrlB : ∀ (r : Univ A R P K dd → Prop), restB r rl = bitVal PR.zero PR.one (r = F.cell gtop)) {p₀ p₁ p₂ p₂b p₃ p₄ : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt F.cell t restA m v) p₁ fc (PR.passTracksAt F.cell t restN m v)) (h₁ : PR.HasRight p₁ fc (PR.passTracksAt F.cell t restN m v') p₂ fc (PR.passTracksAt F.cell t restB m v')) (hscanUp : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight p₂ fc g p₂ fc g) (hb₁ : PR.HasLeft p₂ fc (PR.passTracksAt F.cell t restB m (F.cell gtop)) p₂b fc (PR.passTracksAt F.cell t restB m (F.cell gtop))) (hb₂ : ∀ (g : W → A), PR.HasRight p₂b fc g p₃ fc g) (hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft p₃ fc g p₃ fc (Function.update g t PR.zero)) (hset : ∀ (g : W → A), g t = PR.zero → g rg = PR.one → PR.HasLeft p₃ fc g p₄ fc (Function.update g t PR.one)) (hhold : ∀ (g : W → A), g rg = PR.one → PR.HasLeft p₄ fc g p₄ fc g) (hwalkC : ∀ (k : I → Prop) (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft p₃ fc (PR.passTracksAt F.cell t restB k r) p₃ fc (PR.passTracksAt F.cell t restB k r)) (hwalkD : ∀ (k : I → Prop) (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft p₄ fc (PR.passTracksAt F.cell t restB k r) p₄ fc (PR.passTracksAt F.cell t restB k r)) (hback : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft p₄ fc g p₄ fc g) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell gtop) + ((ixRank ile gtop - ixRank ile gbot) * w + 1) + wideRank (F.cell gbot) + 4) { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p₄ fc), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell t restB m') (PR.syElt PR.blank) }

One round of a sweep: the working-cell marker moves from v to its increment v', the mirror track from m to its increment m', and the head comes back to the marker. See the module docstring for the itinerary; the hypotheses are the rule families of the six phases visited and the slot equations of the three backgrounds (marker at v, marker nowhere, marker at v').

theorem DescriptiveComplexity.Draw.Prog.reaches_fileAdvance {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] {I : Type} [Finite I] {ile : I → I → Prop} {PR : Prog A R P Q W K dd} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t rg rl wk : W} (hnerg : t ≠ rg) (hnerl : rl ≠ t) (hnewk : wk ≠ t) {gtop gbot : I} (htop : ∀ (y : I), ile y gtop) (hbot : ∀ (y : I), ile gbot y) {v v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v v') (hv' : WMSetLt WMLe v' (F.cell gbot)) {m m' : I → Prop} (him : WMIncr ile m m') {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), r ≠ v' → restB r = restN r) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r wk = bitVal PR.zero PR.one (r = v')) (hrgB : ∀ (r : Univ A R P K dd → Prop), restB r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) (hrlB : ∀ (r : Univ A R P K dd → Prop), restB r rl = bitVal PR.zero PR.one (r = F.cell gtop)) {p₀ p₁ p₂ p₂b p₃ p₄ : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt F.cell t restA m v) p₁ fc (PR.passTracksAt F.cell t restN m v)) (h₁ : PR.HasRight p₁ fc (PR.passTracksAt F.cell t restN m v') p₂ fc (PR.passTracksAt F.cell t restB m v')) (hscanUp : ∀ (g : W → A), g rl ≠ PR.one → PR.HasRight p₂ fc g p₂ fc g) (hb₁ : PR.HasLeft p₂ fc (PR.passTracksAt F.cell t restB m (F.cell gtop)) p₂b fc (PR.passTracksAt F.cell t restB m (F.cell gtop))) (hb₂ : ∀ (g : W → A), PR.HasRight p₂b fc g p₃ fc g) (hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft p₃ fc g p₃ fc (Function.update g t PR.zero)) (hset : ∀ (g : W → A), g t = PR.zero → g rg = PR.one → PR.HasLeft p₃ fc g p₄ fc (Function.update g t PR.one)) (hhold : ∀ (g : W → A), g rg = PR.one → PR.HasLeft p₄ fc g p₄ fc g) (hwalkC : ∀ (k : I → Prop) (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft p₃ fc (PR.passTracksAt F.cell t restB k r) p₃ fc (PR.passTracksAt F.cell t restB k r)) (hwalkD : ∀ (k : I → Prop) (r : Univ A R P K dd → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → PR.HasLeft p₄ fc (PR.passTracksAt F.cell t restB k r) p₄ fc (PR.passTracksAt F.cell t restB k r)) (hback : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft p₄ fc g p₄ fc g) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p₄ fc), head := Sum.inl v', tape := wideTape (PR.trackTapeAt F.cell t restB m') (PR.syElt PR.blank) }

One round of a sweep, the budget forgotten.