A program's rules run its register passes

DescriptiveComplexity.Problems.Wide.Mirror and DescriptiveComplexity.Problems.Wide.Test are the three shapes a register pass comes in – write with an accumulator, write without one, read with one – stated about an abstract tape and an abstract supply of transitions. This file joins them to a DescriptiveComplexity.Draw.Prog: the tape is DescriptiveComplexity.Draw.Prog.trackTapeAt, the transitions come from the program's rules, and what is left for the program to supply is a rule per case and nothing else.

What a program owes

DescriptiveComplexity.Draw.Prog.HasLeft is the contract: in this phase, at this pointer, reading these tracks, the program has a rule that goes to that phase and that pointer, writes those tracks, and moves left. Every hypothesis below is a family of those, and the symbols are computed for the caller – it never sees DescriptiveComplexity.regBit, never writes a tape equation, and never mentions FirstOrder.Language.wide. (A whole-track overwrite, and a file test with the question asked of the cell, are in DescriptiveComplexity.Problems.Wide.DrawSub: a wrapper that quantified its per-cell data independently of the symbol could be served by no deterministic table.)

The register mark

Each pass needs to tell a register cell from a cell of the working area, because its rules act at the first and merely walk over the second. One track slot rg carries that (hrest below: the slot is set exactly at the cells of the file), and the guards read it. That is also what separates the acting rules from the walking one, so it is what DescriptiveComplexity.Draw.Prog.sep_of is discharged from in these phases.

Which file

Nothing here is about where the registers are. The passes that need only the cells take the family (DescriptiveComplexity.Draw.Prog.passTracksAt, and the lemmas whose cell is inferred from the statement); the passes that need a file to be a file – the two walks up and down to a marked register, and the mirror increment – take a DescriptiveComplexity.RegFile and are named file…. The wmSeg statements below them are those at DescriptiveComplexity.wmSegFile, which is the file a space-bounded program gets free from the input channel; a clocked program builds its own low on the tape and calls the same lemmas at it.

One restriction, and where it bites

DescriptiveComplexity.reaches_mirrorIncr may stop in a state that depends on the carry position, and the version here does not use that freedom: it stops in a single state, because a state's payload holds elements of the source structure while the carry position is an element of the emitted universe, and the registers are anonymous. The carry position is still delivered, as u₀ with its characterization, so every use that only has to move an address – advancing the working cell, seeking – is served. The inner loop of the step-formula evaluator, which folds accumulators against the block that rolled over, needs an indexed variant: the mark of a register cell records which block that register lies in (finitely many kinds, so finitely many rules), and the stopping rule reads it off the symbol. That variant is not built here.

The contract

def DescriptiveComplexity.Draw.Prog.HasLeft {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) (p : P) (f : Q → A) (g : W → A) (p' : P) (f' : Q → A) (g' : W → A) : Prop

The program has a leftward rule here: in the phase p at the pointer f, reading the tracks g, some rule of it goes to the phase p' at the pointer f', writes the tracks g' and moves left.

Equations

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

def DescriptiveComplexity.Draw.Prog.HasRight {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) (p : P) (f : Q → A) (g : W → A) (p' : P) (f' : Q → A) (g' : W → A) : Prop

The program has a rightward rule here.

Equations

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

theorem DescriptiveComplexity.Draw.Prog.step_of_hasLeft {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} (hR : PR.table.Reads) {p p' : P} {f f' : Q → A} {g g' : W → A} (h : PR.HasLeft p f g p' f' g') : ∃ (τ : Univ A R P K dd), WMTr τ ∧ WMSrc τ (PR.stElt p f) ∧ WMRead τ (PR.syElt g) ∧ WMDst τ (PR.stElt p' f') ∧ WMWrite τ (PR.syElt g') ∧ ¬WMRight τ

A leftward rule is a transition with its six attributes.

theorem DescriptiveComplexity.Draw.Prog.step_of_hasRight {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} (hR : PR.table.Reads) {p p' : P} {f f' : Q → A} {g g' : W → A} (h : PR.HasRight p f g p' f' g') : ∃ (τ : Univ A R P K dd), WMTr τ ∧ WMSrc τ (PR.stElt p f) ∧ WMRead τ (PR.syElt g) ∧ WMDst τ (PR.stElt p' f') ∧ WMWrite τ (PR.syElt g') ∧ WMRight τ

A rightward rule is a transition with its six attributes.

The tracks a pass reads

noncomputable def DescriptiveComplexity.Draw.Prog.passTracksAt {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] (PR : Prog A R P Q W K dd) {I : Type} (cell : I → Univ A R P K dd → Prop) (t : W) (rest : (Univ A R P K dd → Prop) → W → A) (m : I → Prop) (r : Univ A R P K dd → Prop) : W → A

The tracks the tape carries at a cell: the walked track's digit in the slot t, the program's own bits elsewhere. Everything a rule of a register pass reads is this, at a register cell or at a cell of the working area.

The register file enters as its cells and not as a DescriptiveComplexity.RegFile, for the reason DescriptiveComplexity.Draw.Prog.trackTapeAt does: this is a definition, and a file carries proofs. What indexes those cells is a parameter, as it is throughout the address layer: a program on a clock cannot give every element of the universe a register, and the tracks do not care which does.

Equations

• PR.passTracksAt cell t rest m r s = if s = t then DescriptiveComplexity.Draw.bitVal PR.zero PR.one (DescriptiveComplexity.bitAtOf cell m r) else rest r s

theorem DescriptiveComplexity.Draw.Prog.trackTapeAt_eq {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] (PR : Prog A R P Q W K dd) {I : Type} (cell : I → Univ A R P K dd → Prop) (t : W) (rest : (Univ A R P K dd → Prop) → W → A) (m : I → Prop) (r : Univ A R P K dd → Prop) : PR.trackTapeAt cell t rest m r = PR.syElt (PR.passTracksAt cell t rest m r)

theorem DescriptiveComplexity.Draw.Prog.passTracks_cell {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} {t : W} {rest : (Univ A R P K dd → Prop) → W → A} (F : IxFile (Univ A R P K dd) I ile) (hix : IsLinOrd ile) (m : I → Prop) (u : I) : PR.passTracksAt F.cell t rest m (F.cell u) = fun (s : W) => if s = t then bitVal PR.zero PR.one (m u) else rest (F.cell u) s

At a register cell the walked slot holds the track's digit there.

theorem DescriptiveComplexity.Draw.Prog.passTracks_cell_apply {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} {t : W} {rest : (Univ A R P K dd → Prop) → W → A} (F : IxFile (Univ A R P K dd) I ile) (hix : IsLinOrd ile) (m : I → Prop) (u : I) : PR.passTracksAt F.cell t rest m (F.cell u) t = bitVal PR.zero PR.one (m u)

The walked slot at a register cell: the track's digit there, which is what the acting rules of a pass are guarded by.

theorem DescriptiveComplexity.Draw.Prog.passTracks_of_ne {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} {t : W} {rest : (Univ A R P K dd → Prop) → W → A} {sl : W} (hne : sl ≠ t) (m : I → Prop) (r : Univ A R P K dd → Prop) : PR.passTracksAt cell t rest m r sl = rest r sl

A slot other than the walked one shows what the program keeps there. Every guard of a register pass that is not about the track itself reads through this.

theorem DescriptiveComplexity.Draw.Prog.passTracks_congr {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} {t : W} {bgA bgB : (Univ A R P K dd → Prop) → W → A} {r : Univ A R P K dd → Prop} (hbg : bgA r = bgB r) (m : I → Prop) : PR.passTracksAt cell t bgA m r = PR.passTracksAt cell t bgB m r

The tracks at a cell read the background there and nowhere else. Two backgrounds agreeing at one address present the same tracks there, whatever they do elsewhere – which is what lets a sweep describe its progress by a frontier rather than by an induction.

theorem DescriptiveComplexity.Draw.Prog.passTracks_rg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} {t rg : W} {rest : (Univ A R P K dd → Prop) → W → A} (hne : t ≠ rg) (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = cell u)) (m : I → Prop) (r : Univ A R P K dd → Prop) : PR.passTracksAt cell t rest m r rg = bitVal PR.zero PR.one (∃ (u : I), r = cell u)

The register mark, read: the slot rg is set exactly at the cells of the file, which is what tells the acting rules of a pass from its walking one.

One step in the working area

A register pass leaves the program's other bits alone; the work between passes is the other way round – the track is untouched and the background changes, at the one cell the head is on. That is one step, and it is the only place a program's own data is written.

theorem DescriptiveComplexity.Draw.Prog.trackTape_frame {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] {PR : Prog A R P Q W K dd} {I : Type} {cell : I → Univ A R P K dd → Prop} {t : W} {rest rest' : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hframe : ∀ (r : Univ A R P K dd → Prop), r ≠ v → rest' r = rest r) (r : Univ A R P K dd → Prop) : r ≠ v → PR.trackTapeAt cell t rest' m r = PR.trackTapeAt cell t rest m r

Backgrounds agreeing off a cell present tapes agreeing off it.

theorem DescriptiveComplexity.Draw.Prog.step_move {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v v') {t : W} {rest rest' : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} (hframe : ∀ (r : Univ A R P K dd → Prop), r ≠ v → rest' r = rest r) {p p' : P} {f f' : Q → A} (hrule : PR.HasRight p f (PR.passTracksAt cell t rest m v) p' f' (PR.passTracksAt cell t rest' m v)) : (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p' f'), head := Sum.inl v', tape := wideTape (PR.trackTapeAt cell t rest' m) (PR.syElt PR.blank) }

One step of the program to the right, writing its own data at the cell it leaves. The track is carried along untouched, so a step and a register pass compose without either having to know what the other keeps on the tape.

theorem DescriptiveComplexity.Draw.Prog.step_moveBack {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {v v' : Univ A R P K dd → Prop} (hi : WMIncr WMLe v' v) {t : W} {rest rest' : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} (hframe : ∀ (r : Univ A R P K dd → Prop), r ≠ v → rest' r = rest r) {p p' : P} {f f' : Q → A} (hrule : PR.HasLeft p f (PR.passTracksAt cell t rest m v) p' f' (PR.passTracksAt cell t rest' m v)) : (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p' f'), head := Sum.inl v', tape := wideTape (PR.trackTapeAt cell t rest' m) (PR.syElt PR.blank) }

One step of the program to the left.

Getting to a marked register

The two ends of the file have to be recognized on sight – the last one to begin a downward pass, the first one to come back from one – and that is all that has to be. One slot marks the target cell, one rule family walks over everything else, and the same theorem serves both ends by taking the target as a parameter.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_fileToMark {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t sl : W} (hne : sl ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {u : I} (hsl : ∀ (r : Univ A R P K dd → Prop), rest r sl = bitVal PR.zero PR.one (r = F.cell u)) {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), g sl = PR.zero → PR.HasRight p f g p f g) {s : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s (F.cell u)) : (wideData (Univ A R P K dd)).ReachesIn (wideRank (F.cell u) - wideRank s) { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl (F.cell u), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }

Walking up to a marked register. From any cell at or below the register of u, the machine scans right to it, stopped by the slot sl that marks that cell and no other. The cost is the stretch of addresses it crosses.

theorem DescriptiveComplexity.Draw.Prog.reaches_fileToMark {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t sl : W} (hne : sl ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {u : I} (hsl : ∀ (r : Univ A R P K dd → Prop), rest r sl = bitVal PR.zero PR.one (r = F.cell u)) {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), g sl = PR.zero → PR.HasRight p f g p f g) {s : Univ A R P K dd → Prop} (hle : WMSetLe WMLe s (F.cell u)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl (F.cell u), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }

Walking up to a marked register, the budget forgotten.

Seeking a marked cell

The other navigation a program does, and the one it does in the working area: walk until the cell whose slot sl is set. Unlike the register ends, the program does not know which cell that will be – it wrote the mark itself, exponentially many rounds ago – so the arrival comes with the promise that nothing passed was marked, which is where the extremum is taken.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_seek {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t sl : W} (hne : sl ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), g sl ≠ PR.one → PR.HasRight p f g p f g) {s : Univ A R P K dd → Prop} (hex : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe s r) : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe s r ∧ (∀ (r' : Univ A R P K dd → Prop), WMSetLe WMLe s r' → WMSetLt WMLe r' r → rest r' sl ≠ PR.one) ∧ (wideData (Univ A R P K dd)).ReachesIn (wideRank r - wideRank s) { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl r, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Seeking right to the nearest marked cell.

theorem DescriptiveComplexity.Draw.Prog.reaches_seek {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t sl : W} (hne : sl ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), g sl ≠ PR.one → PR.HasRight p f g p f g) {s : Univ A R P K dd → Prop} (hex : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe s r) : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe s r ∧ (∀ (r' : Univ A R P K dd → Prop), WMSetLe WMLe s r' → WMSetLt WMLe r' r → rest r' sl ≠ PR.one) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl r, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Seeking right to the nearest marked cell, the budget forgotten.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_seekBack {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t sl : W} (hne : sl ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), g sl ≠ PR.one → PR.HasLeft p f g p f g) {s : Univ A R P K dd → Prop} (hex : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe r s) : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe r s ∧ (∀ (r' : Univ A R P K dd → Prop), WMSetLt WMLe r r' → WMSetLe WMLe r' s → rest r' sl ≠ PR.one) ∧ (wideData (Univ A R P K dd)).ReachesIn (wideRank s - wideRank r) { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl r, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Seeking left to the nearest marked cell.

theorem DescriptiveComplexity.Draw.Prog.reaches_seekBack {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {cell : I → Univ A R P K dd → Prop} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t sl : W} (hne : sl ≠ t) {rest : (Univ A R P K dd → Prop) → W → A} {p : P} {f : Q → A} {m : I → Prop} (hgo : ∀ (g : W → A), g sl ≠ PR.one → PR.HasLeft p f g p f g) {s : Univ A R P K dd → Prop} (hex : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe r s) : ∃ (r : Univ A R P K dd → Prop), rest r sl = PR.one ∧ WMSetLe WMLe r s ∧ (∀ (r' : Univ A R P K dd → Prop), WMSetLt WMLe r r' → WMSetLe WMLe r' s → rest r' sl ≠ PR.one) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl s, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p f), head := Sum.inl r, tape := wideTape (PR.trackTapeAt cell t rest m) (PR.syElt PR.blank) }

Seeking left to the nearest marked cell, the budget forgotten.

The mirror increment

The stopped phase may depend on the register the increment carried at – on the block that rolled over, which is what the fold of DescriptiveComplexity.Problems.Wide.Fold has to know. The machine cannot name that register: a state's payload holds elements of the source structure, and the registers are anonymous. What it can do is read the block off the mark, since a reduction chooses what each register cell starts holding and there are finitely many blocks; so the stopping rule comes in one copy per block, and the phase it goes to is the copy's.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_fileIncrBlk {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {ile : I → I → Prop} [Finite I] (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {m m' : I → Prop} (hi : WMIncr ile m m') {t rg : W} (hne : t ≠ rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) {B : Type} {bs : B → W} (hbs : ∀ (b : B), bs b ≠ t) {blkOf : I → B} (hblk : ∀ (u : I) (b : B), rest (F.cell u) (bs b) = bitVal PR.zero PR.one (blkOf u = b)) {pc : P} {pd : B → P} {fc : Q → A} (hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft pc fc g pc fc (Function.update g t PR.zero)) (hset : ∀ (b : B) (g : W → A), g t = PR.zero → g rg = PR.one → g (bs b) = PR.one → (∀ (b' : B), g (bs b') = PR.one → b' = b) → PR.HasLeft pc fc g (pd b) fc (Function.update g t PR.one)) (hhold : ∀ (b : B) (g : W → A), g rg = PR.one → PR.HasLeft (pd b) fc g (pd b) fc g) (hwalk : ∀ (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 pc fc (PR.passTracksAt F.cell t rest k r) pc fc (PR.passTracksAt F.cell t rest k r)) (hwalkD : ∀ (b : B) (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 (pd b) fc (PR.passTracksAt F.cell t rest k r) (pd b) fc (PR.passTracksAt F.cell t rest k r)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (u₀ : I) (p : Univ A R P K dd → Prop), (¬m u₀ ∧ ∀ (v : I), WMLt ile u₀ v → m v) ∧ WMIncr WMLe p (F.cell bot) ∧ (wideData (Univ A R P K dd)).ReachesIn ((ixRank ile top - ixRank ile bot) * w + 1) { state := Sum.inr (PR.stElt pc fc), head := Sum.inl (F.cell top), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (pd (blkOf u₀)) fc), head := Sum.inl p, tape := wideTape (PR.trackTapeAt F.cell t rest m') (PR.syElt PR.blank) }

A program increments its mirror, and lands in the phase of the block that carried. From the last register in the carrying phase with the track at m, the machine walks down the file and arrives just below the first register with the track at the increment of m, in the phase pd b for the block b of the carry position.

The four families of rules are the whole of what the program supplies, and each is a statement about the tracks a symbol carries, not about the tape.

theorem DescriptiveComplexity.Draw.Prog.reachesIn_fileIncr {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {ile : I → I → Prop} [Finite I] (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {m m' : I → Prop} (hi : WMIncr ile m m') {t rg : W} (hne : t ≠ rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) {pc pd : P} {fc : Q → A} (hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft pc fc g pc fc (Function.update g t PR.zero)) (hset : ∀ (g : W → A), g t = PR.zero → g rg = PR.one → PR.HasLeft pc fc g pd fc (Function.update g t PR.one)) (hhold : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pd fc g pd fc g) (hwalk : ∀ (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 pc fc (PR.passTracksAt F.cell t rest k r) pc fc (PR.passTracksAt F.cell t rest 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 pd fc (PR.passTracksAt F.cell t rest k r) pd fc (PR.passTracksAt F.cell t rest k r)) {w : ℕ} (hgap : ∀ (u u' : I), IxSucc ile u u' → wideRank (F.cell u') - wideRank (F.cell u) ≤ w) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (u₀ : I) (p : Univ A R P K dd → Prop), (¬m u₀ ∧ ∀ (v : I), WMLt ile u₀ v → m v) ∧ WMIncr WMLe p (F.cell bot) ∧ (wideData (Univ A R P K dd)).ReachesIn ((ixRank ile top - ixRank ile bot) * w + 1) { state := Sum.inr (PR.stElt pc fc), head := Sum.inl (F.cell top), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pd fc), head := Sum.inl p, tape := wideTape (PR.trackTapeAt F.cell t rest m') (PR.syElt PR.blank) }

A program increments its mirror, stopping in one phase whatever carried: DescriptiveComplexity.Draw.Prog.reachesIn_fileIncrBlk with a single block, the register mark serving as its indicator. This is the form every use that only has to move an address takes – advancing the working cell, seeking.

theorem DescriptiveComplexity.Draw.Prog.reaches_fileIncrBlk {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {ile : I → I → Prop} [Finite I] (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {m m' : I → Prop} (hi : WMIncr ile m m') {t rg : W} (hne : t ≠ rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) {B : Type} {bs : B → W} (hbs : ∀ (b : B), bs b ≠ t) {blkOf : I → B} (hblk : ∀ (u : I) (b : B), rest (F.cell u) (bs b) = bitVal PR.zero PR.one (blkOf u = b)) {pc : P} {pd : B → P} {fc : Q → A} (hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft pc fc g pc fc (Function.update g t PR.zero)) (hset : ∀ (b : B) (g : W → A), g t = PR.zero → g rg = PR.one → g (bs b) = PR.one → (∀ (b' : B), g (bs b') = PR.one → b' = b) → PR.HasLeft pc fc g (pd b) fc (Function.update g t PR.one)) (hhold : ∀ (b : B) (g : W → A), g rg = PR.one → PR.HasLeft (pd b) fc g (pd b) fc g) (hwalk : ∀ (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 pc fc (PR.passTracksAt F.cell t rest k r) pc fc (PR.passTracksAt F.cell t rest k r)) (hwalkD : ∀ (b : B) (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 (pd b) fc (PR.passTracksAt F.cell t rest k r) (pd b) fc (PR.passTracksAt F.cell t rest k r)) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (u₀ : I) (p : Univ A R P K dd → Prop), (¬m u₀ ∧ ∀ (v : I), WMLt ile u₀ v → m v) ∧ WMIncr WMLe p (F.cell bot) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt pc fc), head := Sum.inl (F.cell top), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (pd (blkOf u₀)) fc), head := Sum.inl p, tape := wideTape (PR.trackTapeAt F.cell t rest m') (PR.syElt PR.blank) }

A program increments its mirror, landing in the phase of the block that carried, the budget forgotten.

theorem DescriptiveComplexity.Draw.Prog.reaches_fileIncr {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)] {PR : Prog A R P Q W K dd} [Finite A] [Finite R] [Finite P] [Finite K] {I : Type} {ile : I → I → Prop} [Finite I] (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {m m' : I → Prop} (hi : WMIncr ile m m') {t rg : W} (hne : t ≠ rg) {rest : (Univ A R P K dd → Prop) → W → A} (hrest : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = F.cell u)) {pc pd : P} {fc : Q → A} (hclear : ∀ (g : W → A), g t = PR.one → g rg = PR.one → PR.HasLeft pc fc g pc fc (Function.update g t PR.zero)) (hset : ∀ (g : W → A), g t = PR.zero → g rg = PR.one → PR.HasLeft pc fc g pd fc (Function.update g t PR.one)) (hhold : ∀ (g : W → A), g rg = PR.one → PR.HasLeft pd fc g pd fc g) (hwalk : ∀ (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 pc fc (PR.passTracksAt F.cell t rest k r) pc fc (PR.passTracksAt F.cell t rest 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 pd fc (PR.passTracksAt F.cell t rest k r) pd fc (PR.passTracksAt F.cell t rest k r)) {top bot : I} (htop : ∀ (v : I), ile v top) (hbot : ∀ (v : I), ile bot v) : ∃ (u₀ : I) (p : Univ A R P K dd → Prop), (¬m u₀ ∧ ∀ (v : I), WMLt ile u₀ v → m v) ∧ WMIncr WMLe p (F.cell bot) ∧ Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt pc fc), head := Sum.inl (F.cell top), tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pd fc), head := Sum.inl p, tape := wideTape (PR.trackTapeAt F.cell t rest m') (PR.syElt PR.blank) }

A program increments its mirror, stopping in one phase whatever carried, the budget forgotten.