Walking the register file

The phase a wide machine spends its life in. Its register file is one recognizable cell per element of the instance (DescriptiveComplexity.RegFile), and every register operation – read a bit, flip one, increment a mirror, compare two – is the same walk:

stand on the cell of u, write there, and scan right to the cell of the next element; repeat until the file is exhausted.

DescriptiveComplexity.RegFile.reachesIn_regStep is one such move and DescriptiveComplexity.RegFile.reachesIn_regWalk is the whole traversal, the latter being the only induction a program has to be given: the machine's state and its tape are handed over as functions of the element the pointer has reached, and what is discharged is a single move between an element and its successor.

Both come in the other direction too (DescriptiveComplexity.RegFile.reachesIn_regStepBack, DescriptiveComplexity.RegFile.reachesIn_regWalkBack), and that reading is not a convenience: the least significant digit of an address is the WMLe-greatest element, so a program incrementing its mirror – clear the trailing digits, set the first that is clear – walks the file from its last register towards its first.

Getting to a register in the first place – the last one, to begin a downward pass, and the first one, to come back from it – is DescriptiveComplexity.RegFile.reachesIn_toReg and DescriptiveComplexity.RegFile.reachesIn_toRegBack: one scan each, stopped by a symbol the target register carries and the others do not. Only the two ends of the file need such a symbol; in a file the input channel marks, those in between are all the same one, and must be, since a symbol is an element and there are as many registers as elements.

Two facts make a move between consecutive registers a single scan rather than a search: consecutive elements have no register between them (DescriptiveComplexity.RegFile.gap), so the scan cannot overshoot or stop early; and the pointer lives in the machine's control, where a state may hold an element of the instance, so no address arithmetic is involved in knowing which register one is on.

What a walk costs

Each statement comes in a budgeted form and an erased one. A move between consecutive registers costs exactly the addresses lying between them, and a walk of a stretch of the file costs the registers it crosses times whatever bound the caller puts on one move. Which form a program uses is the whole difference between the space-bounded wide problems and the clocked one: the file the input channel marks is a geometric ruler in the top half of the tape, so walking it is affordable only when nothing is counting.

Every statement is also given at DescriptiveComplexity.wmSeg, so that a program written against the file of the input channel names no DescriptiveComplexity.RegFile at all.

What indexes the registers is a parameter. Every proof here is about the order the cells are laid out in and about nothing else, so each statement is made at a DescriptiveComplexity.IxFile – a file over an arbitrary ordered index – and the elementwise form is its diagonal (DescriptiveComplexity.RegFile.toIx), one line each. The pointer is a function of the index and the states stay elements of the instance, which is what makes the generalization free: a walk never holds an index anywhere the machine can see, only its caller does. Two linear orders separate in the general form – the addresses' and the index's – and a statement that needs only one says so.

def DescriptiveComplexity.bitAtOf {A I : Type} (cell : I → A → Prop) (m : I → Prop) (r : A → Prop) : Prop

What a track shows at a cell: its digit, if the cell is some element's register; nothing at any other cell. A program's tape is a function of this and of the address, and of nothing else about the track.

Stated at the cells rather than at a DescriptiveComplexity.RegFile, because a program's tape is a definition and a file carries proofs: threading the whole record through the definitions would make them depend on the linearity of the order, which nothing about them does. The file appears in the theorems below, where the proofs are wanted.

Equations

• DescriptiveComplexity.bitAtOf cell m r = ∃ (u : I), r = cell u ∧ m u

theorem DescriptiveComplexity.bitAtOf_of_not_reg {A I : Type} {cell : I → A → Prop} {m : I → Prop} {r : A → Prop} (hno : ∀ (u : I), r ≠ cell u) : ¬bitAtOf cell m r

At a cell that is nobody's register a track shows nothing.

theorem DescriptiveComplexity.bitAtOf_congr {A I : Type} {cell : I → A → Prop} {m m' : I → Prop} {u : I} (hag : ∀ (v : I), v ≠ u → (m v ↔ m' v)) {r : A → Prop} (hr : r ≠ cell u) : bitAtOf cell m r = bitAtOf cell m' r

The coherence condition of the passes, discharged. Two tracks agreeing off one element show the same thing at every cell but that element's register – whatever else the program keeps in its symbols, since they enter the tape only through this.

A caller finishes with congrArg: its tape is some g r (bitAtOf cell m r), and this says the second argument does not move.

One move of the walk

theorem DescriptiveComplexity.IxFile.reachesIn_regStep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u)) ∧ WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe r (F.cell x)) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ WMRight τ) : (wideData A).ReachesIn (wideRank (F.cell u') - wideRank (F.cell u)) { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u'), tape := wideTape f' b }

One move of a register walk. In the state q, on the cell of u, the machine writes there and moves right; then, in the state q', it scans over the cells that are nobody's register; it arrives on the cell of the successor of u, having spent exactly the addresses lying between the two registers.

The write is described the way every write in this development is – by naming the new symbol assignment f' and saying it agrees with f off the cell of u – and the scan is asked for only at the cells that are nobody's register, which is exactly where DescriptiveComplexity.RegFile.gap says the machine will pass.

theorem DescriptiveComplexity.IxFile.reaches_regStep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u)) ∧ WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe r (F.cell x)) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u'), tape := wideTape f' b }

One move of a register walk, the budget forgotten.

The whole traversal

theorem DescriptiveComplexity.IxFile.reachesIn_regWalk {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {b : A} {st : I → A} {tp : I → (A → Prop) → A} {u₀ : I} {w : ℕ} (hmove : ∀ (u u' : I), IxSucc ile u u' → ile u₀ u → (wideData A).ReachesIn w { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b } { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b }) (u : I) : ile u₀ u → (wideData A).ReachesIn ((ixRank ile u - ixRank ile u₀) * w) { state := Sum.inr (st u₀), head := Sum.inl (F.cell u₀), tape := wideTape (tp u₀) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk. Give the machine's state and its tape as functions of the element its pointer has reached, discharge one move of at most w steps between each element of a stretch and its successor, and the machine walks the whole stretch, paying w per register crossed.

This is the only induction a program is given about its register file: with it, a phase is described by what it does at one register, and the traversal never appears again.

theorem DescriptiveComplexity.IxFile.reaches_regWalk {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {b : A} {st : I → A} {tp : I → (A → Prop) → A} {u₀ : I} (hmove : ∀ (u u' : I), IxSucc ile u u' → ile u₀ u → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b } { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b }) (u : I) : ile u₀ u → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u₀), head := Sum.inl (F.cell u₀), tape := wideTape (tp u₀) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk, the budget forgotten: each move is a run of any length whatever.

Reaching a named register

Before a pass can start, and between one pass and the next, the head has to get to a particular register – the last one to begin a downward pass, the first one to come back from it, or the one a pointer in the control names. Each is a scan whose stopping symbol is the name the register carries, and the two facts that make it one scan are that the registers are ordered like their elements and that a register's symbol names it.

theorem DescriptiveComplexity.IxFile.reachesIn_toReg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : I} {s : A → Prop} (hle : WMSetLe WMLe s (F.cell u)) (hother : ∀ (x : I), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe r (F.cell x)) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : (wideData A).ReachesIn (wideRank (F.cell u) - wideRank s) { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking up to a distinguished register. From any cell at or below the register of u, in a fixed state, the machine scans right to it. The caller offers the scanning transition at the cells that are nobody's register and at the registers of the other elements – which in a file marked by the input channel all hold the one generic mark, so that is a single transition – and withholds it at the symbol the register of u carries, which is what stops the scan.

theorem DescriptiveComplexity.IxFile.reaches_toReg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : I} {s : A → Prop} (hle : WMSetLe WMLe s (F.cell u)) (hother : ∀ (x : I), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe r (F.cell x)) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking up to a distinguished register, the budget forgotten.

theorem DescriptiveComplexity.IxFile.reachesIn_toRegBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : I} {s : A → Prop} (hle : WMSetLe WMLe (F.cell u) s) (hother : ∀ (x : I), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ ¬WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : (wideData A).ReachesIn (wideRank s - wideRank (F.cell u)) { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking back down to a named register, the same reading downwards: from any cell at or above the register of u, the machine scans left to it.

theorem DescriptiveComplexity.IxFile.reaches_toRegBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : I} {s : A → Prop} (hle : WMSetLe WMLe (F.cell u) s) (hother : ∀ (x : I), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ ¬WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking back down to a named register, the budget forgotten.

Walking the file the other way

The least significant digit of an address is the WMLe-greatest element (DescriptiveComplexity.Problems.Wide.Increment), so a program incrementing its mirror propagates the carry from the last register towards the first: the walk it does is this one.

theorem DescriptiveComplexity.IxFile.reachesIn_regStepBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u')) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u')) ∧ ¬WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u' → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ ¬WMRight τ) : (wideData A).ReachesIn (wideRank (F.cell u') - wideRank (F.cell u)) { state := Sum.inr q, head := Sum.inl (F.cell u'), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u), tape := wideTape f' b }

One move of a register walk, downwards. In the state q, on the cell of u', the machine writes there and moves left; then it scans left over the cells that are nobody's register and arrives on the cell of the element u' succeeds.

theorem DescriptiveComplexity.IxFile.reaches_regStepBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (ha : IsLinOrd WMLe) (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u')) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u')) ∧ ¬WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u' → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : I), WMSetLe WMLe (F.cell x) r) → (∀ (x : I), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ ¬WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (F.cell u'), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u), tape := wideTape f' b }

One move of a register walk, downwards, the budget forgotten.

theorem DescriptiveComplexity.IxFile.reachesIn_regWalkBack {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {b : A} {st : I → A} {tp : I → (A → Prop) → A} {u₁ : I} {w : ℕ} (hmove : ∀ (u u' : I), IxSucc ile u u' → ile u' u₁ → (wideData A).ReachesIn w { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }) (u : I) : ile u u₁ → (wideData A).ReachesIn ((ixRank ile u₁ - ixRank ile u) * w) { state := Sum.inr (st u₁), head := Sum.inl (F.cell u₁), tape := wideTape (tp u₁) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk, downwards: the mirror of DescriptiveComplexity.RegFile.reachesIn_regWalk, from the top of a stretch of the file to any element of it. This is the shape of a mirror increment – clear the trailing digits, set the first that is clear – so it is the walk a program does most.

theorem DescriptiveComplexity.IxFile.reaches_regWalkBack {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} [Finite I] {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) {b : A} {st : I → A} {tp : I → (A → Prop) → A} {u₁ : I} (hmove : ∀ (u u' : I), IxSucc ile u u' → ile u' u₁ → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }) (u : I) : ile u u₁ → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u₁), head := Sum.inl (F.cell u₁), tape := wideTape (tp u₁) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk, downwards, the budget forgotten.

A track over the register file

The passes of DescriptiveComplexity.Problems.Wide.Mirror and DescriptiveComplexity.Problems.Wide.Test take the tape as a function of one track, tapeOf m, and each asks for the same coherence condition: changing the track at one element changes the tape at that element's cell and nowhere else. A program does not verify that by hand. It builds its tape by reading the track through DescriptiveComplexity.RegFile.bitAt – the track's digit at a register cell, nothing anywhere else – and DescriptiveComplexity.RegFile.bitAt_congr is the condition, discharged once for every program and every alphabet.

@[reducible]

def DescriptiveComplexity.IxFile.bitAt {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (m : I → Prop) (r : A → Prop) : Prop

What a track shows at a cell of a given file.

Equations

• F.bitAt m r = DescriptiveComplexity.bitAtOf F.cell m r

@[simp]

theorem DescriptiveComplexity.IxFile.bitAt_cell {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) (h : IsLinOrd ile) (m : I → Prop) (u : I) : F.bitAt m (F.cell u) ↔ m u

theorem DescriptiveComplexity.IxFile.bitAt_of_not_reg {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) {m : I → Prop} {r : A → Prop} (hno : ∀ (u : I), r ≠ F.cell u) : ¬F.bitAt m r

At a cell that is nobody's register a track shows nothing.

theorem DescriptiveComplexity.IxFile.bitAt_congr {A : Type} [FirstOrder.Language.wide.Structure A] {I : Type} {ile : I → I → Prop} (F : IxFile A I ile) {m m' : I → Prop} {u : I} (hag : ∀ (v : I), v ≠ u → (m v ↔ m' v)) {r : A → Prop} (hr : r ≠ F.cell u) : F.bitAt m r = F.bitAt m' r

The coherence condition of the passes, discharged. Two tracks agreeing off one element show the same thing at every cell but that element's register – whatever else the program keeps in its symbols, since they enter the tape only through this.

A caller finishes with congrArg: its tape is some g r (F.bitAt m r), and this says the second argument does not move.

One move of the walk

theorem DescriptiveComplexity.RegFile.reachesIn_regStep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u)) ∧ WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe r (F.cell x)) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ WMRight τ) : (wideData A).ReachesIn (wideRank (F.cell u') - wideRank (F.cell u)) { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u'), tape := wideTape f' b }

One move of a register walk. In the state q, on the cell of u, the machine writes there and moves right; then, in the state q', it scans over the cells that are nobody's register; it arrives on the cell of the successor of u, having spent exactly the addresses lying between the two registers.

The write is described the way every write in this development is – by naming the new symbol assignment f' and saying it agrees with f off the cell of u – and the scan is asked for only at the cells that are nobody's register, which is exactly where DescriptiveComplexity.RegFile.gap says the machine will pass.

theorem DescriptiveComplexity.RegFile.reaches_regStep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u)) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u)) ∧ WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe r (F.cell x)) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u'), tape := wideTape f' b }

One move of a register walk, the budget forgotten.

The whole traversal

theorem DescriptiveComplexity.RegFile.reachesIn_regWalk {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {b : A} {st : A → A} {tp : A → (A → Prop) → A} {u₀ : A} {w : ℕ} (hmove : ∀ (u u' : A), WMSucc A u u' → WMLe u₀ u → (wideData A).ReachesIn w { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b } { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b }) (u : A) : WMLe u₀ u → (wideData A).ReachesIn ((wmRank u - wmRank u₀) * w) { state := Sum.inr (st u₀), head := Sum.inl (F.cell u₀), tape := wideTape (tp u₀) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk. Give the machine's state and its tape as functions of the element its pointer has reached, discharge one move of at most w steps between each element of a stretch and its successor, and the machine walks the whole stretch, paying w per register crossed.

This is the only induction a program is given about its register file: with it, a phase is described by what it does at one register, and the traversal never appears again.

theorem DescriptiveComplexity.RegFile.reaches_regWalk {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {b : A} {st : A → A} {tp : A → (A → Prop) → A} {u₀ : A} (hmove : ∀ (u u' : A), WMSucc A u u' → WMLe u₀ u → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b } { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b }) (u : A) : WMLe u₀ u → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u₀), head := Sum.inl (F.cell u₀), tape := wideTape (tp u₀) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk, the budget forgotten: each move is a run of any length whatever.

Reaching a named register

Before a pass can start, and between one pass and the next, the head has to get to a particular register – the last one to begin a downward pass, the first one to come back from it, or the one a pointer in the control names. Each is a scan whose stopping symbol is the name the register carries, and the two facts that make it one scan are that the registers are ordered like their elements and that a register's symbol names it.

theorem DescriptiveComplexity.RegFile.reachesIn_toReg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : A} {s : A → Prop} (hle : WMSetLe WMLe s (F.cell u)) (hother : ∀ (x : A), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe r (F.cell x)) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : (wideData A).ReachesIn (wideRank (F.cell u) - wideRank s) { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking up to a distinguished register. From any cell at or below the register of u, in a fixed state, the machine scans right to it. The caller offers the scanning transition at the cells that are nobody's register and at the registers of the other elements – which in a file marked by the input channel all hold the one generic mark, so that is a single transition – and withholds it at the symbol the register of u carries, which is what stops the scan.

theorem DescriptiveComplexity.RegFile.reaches_toReg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : A} {s : A → Prop} (hle : WMSetLe WMLe s (F.cell u)) (hother : ∀ (x : A), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe r (F.cell x)) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking up to a distinguished register, the budget forgotten.

theorem DescriptiveComplexity.RegFile.reachesIn_toRegBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : A} {s : A → Prop} (hle : WMSetLe WMLe (F.cell u) s) (hother : ∀ (x : A), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ ¬WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (F.cell x) r) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : (wideData A).ReachesIn (wideRank s - wideRank (F.cell u)) { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking back down to a named register, the same reading downwards: from any cell at or above the register of u, the machine scans left to it.

theorem DescriptiveComplexity.RegFile.reaches_toRegBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : A} {s : A → Prop} (hle : WMSetLe WMLe (F.cell u) s) (hother : ∀ (x : A), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell x)) ∧ WMDst τ q ∧ WMWrite τ (f (F.cell x)) ∧ ¬WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (F.cell x) r) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (F.cell u), tape := wideTape f b }

Walking back down to a named register, the budget forgotten.

Walking the file the other way

The least significant digit of an address is the WMLe-greatest element (DescriptiveComplexity.Problems.Wide.Increment), so a program incrementing its mirror propagates the carry from the last register towards the first: the walk it does is this one.

theorem DescriptiveComplexity.RegFile.reachesIn_regStepBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u')) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u')) ∧ ¬WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u' → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (F.cell x) r) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ ¬WMRight τ) : (wideData A).ReachesIn (wideRank (F.cell u') - wideRank (F.cell u)) { state := Sum.inr q, head := Sum.inl (F.cell u'), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u), tape := wideTape f' b }

One move of a register walk, downwards. In the state q, on the cell of u', the machine writes there and moves left; then it scans left over the cells that are nobody's register and arrives on the cell of the element u' succeeds.

theorem DescriptiveComplexity.RegFile.reaches_regStepBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (F.cell u')) ∧ WMDst τ q' ∧ WMWrite τ (f' (F.cell u')) ∧ ¬WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ F.cell u' → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (F.cell x) r) → (∀ (x : A), r ≠ F.cell x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ ¬WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (F.cell u'), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (F.cell u), tape := wideTape f' b }

One move of a register walk, downwards, the budget forgotten.

theorem DescriptiveComplexity.RegFile.reachesIn_regWalkBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {b : A} {st : A → A} {tp : A → (A → Prop) → A} {u₁ : A} {w : ℕ} (hmove : ∀ (u u' : A), WMSucc A u u' → WMLe u' u₁ → (wideData A).ReachesIn w { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }) (u : A) : WMLe u u₁ → (wideData A).ReachesIn ((wmRank u₁ - wmRank u) * w) { state := Sum.inr (st u₁), head := Sum.inl (F.cell u₁), tape := wideTape (tp u₁) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk, downwards: the mirror of DescriptiveComplexity.RegFile.reachesIn_regWalk, from the top of a stretch of the file to any element of it. This is the shape of a mirror increment – clear the trailing digits, set the first that is clear – so it is the walk a program does most.

theorem DescriptiveComplexity.RegFile.reaches_regWalkBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (F : RegFile A) (h : IsLinOrd WMLe) {b : A} {st : A → A} {tp : A → (A → Prop) → A} {u₁ : A} (hmove : ∀ (u u' : A), WMSucc A u u' → WMLe u' u₁ → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u'), head := Sum.inl (F.cell u'), tape := wideTape (tp u') b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }) (u : A) : WMLe u u₁ → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u₁), head := Sum.inl (F.cell u₁), tape := wideTape (tp u₁) b } { state := Sum.inr (st u), head := Sum.inl (F.cell u), tape := wideTape (tp u) b }

A register walk, downwards, the budget forgotten.

A track over the register file

The passes of DescriptiveComplexity.Problems.Wide.Mirror and DescriptiveComplexity.Problems.Wide.Test take the tape as a function of one track, tapeOf m, and each asks for the same coherence condition: changing the track at one element changes the tape at that element's cell and nowhere else. A program does not verify that by hand. It builds its tape by reading the track through DescriptiveComplexity.RegFile.bitAt – the track's digit at a register cell, nothing anywhere else – and DescriptiveComplexity.RegFile.bitAt_congr is the condition, discharged once for every program and every alphabet.

@[reducible]

def DescriptiveComplexity.RegFile.bitAt {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) (m r : A → Prop) : Prop

What a track shows at a cell of a given file.

Equations

• F.bitAt m r = F.toIx.bitAt m r

@[simp]

theorem DescriptiveComplexity.RegFile.bitAt_cell {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) (h : IsLinOrd WMLe) (m : A → Prop) (u : A) : F.bitAt m (F.cell u) ↔ m u

theorem DescriptiveComplexity.RegFile.bitAt_of_not_reg {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) {m r : A → Prop} (hno : ∀ (u : A), r ≠ F.cell u) : ¬F.bitAt m r

At a cell that is nobody's register a track shows nothing.

theorem DescriptiveComplexity.RegFile.bitAt_congr {A : Type} [FirstOrder.Language.wide.Structure A] (F : RegFile A) {m m' : A → Prop} {u : A} (hag : ∀ (v : A), v ≠ u → (m v ↔ m' v)) {r : A → Prop} (hr : r ≠ F.cell u) : F.bitAt m r = F.bitAt m' r

The coherence condition of the passes, discharged. Two tracks agreeing off one element show the same thing at every cell but that element's register – whatever else the program keeps in its symbols, since they enter the tape only through this.

A caller finishes with congrArg: its tape is some g r (F.bitAt m r), and this says the second argument does not move.

The same, at the file the input channel marks

Every statement above, read at DescriptiveComplexity.wmSegFile: this is the register file a space-bounded program uses, and these are the names its phases cite.

theorem DescriptiveComplexity.reaches_regStep {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (wmSeg u)) ∧ WMDst τ q' ∧ WMWrite τ (f' (wmSeg u)) ∧ WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ wmSeg u → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe r (wmSeg x)) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (wmSeg u), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (wmSeg u'), tape := wideTape f' b }

One move of a register walk over the file the input channel marks.

theorem DescriptiveComplexity.reaches_regWalk {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} {st : A → A} {tp : A → (A → Prop) → A} {u₀ : A} (hmove : ∀ (u u' : A), WMSucc A u u' → WMLe u₀ u → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u), head := Sum.inl (wmSeg u), tape := wideTape (tp u) b } { state := Sum.inr (st u'), head := Sum.inl (wmSeg u'), tape := wideTape (tp u') b }) (u : A) : WMLe u₀ u → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u₀), head := Sum.inl (wmSeg u₀), tape := wideTape (tp u₀) b } { state := Sum.inr (st u), head := Sum.inl (wmSeg u), tape := wideTape (tp u) b }

A register walk over the file the input channel marks.

theorem DescriptiveComplexity.reaches_toReg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : A} {s : A → Prop} (hle : WMSetLe WMLe s (wmSeg u)) (hother : ∀ (x : A), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (wmSeg x)) ∧ WMDst τ q ∧ WMWrite τ (f (wmSeg x)) ∧ WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe r (wmSeg x)) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (wmSeg u), tape := wideTape f b }

Walking up to a distinguished register of the file the input channel marks.

theorem DescriptiveComplexity.reaches_toRegBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {q b : A} {f : (A → Prop) → A} {u : A} {s : A → Prop} (hle : WMSetLe WMLe (wmSeg u) s) (hother : ∀ (x : A), x ≠ u → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (wmSeg x)) ∧ WMDst τ q ∧ WMWrite τ (f (wmSeg x)) ∧ ¬WMRight τ) (hskip : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (wmSeg x) r) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f r) ∧ WMDst τ q ∧ WMWrite τ (f r) ∧ ¬WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl s, tape := wideTape f b } { state := Sum.inr q, head := Sum.inl (wmSeg u), tape := wideTape f b }

Walking back down to a named register of the file the input channel marks.

theorem DescriptiveComplexity.reaches_regStepBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {u u' : A} (hs : WMSucc A u u') {q q' b : A} {f f' : (A → Prop) → A} (hwrite : ∃ (τ : A), WMTr τ ∧ WMSrc τ q ∧ WMRead τ (f (wmSeg u')) ∧ WMDst τ q' ∧ WMWrite τ (f' (wmSeg u')) ∧ ¬WMRight τ) (hagree : ∀ (r : A → Prop), r ≠ wmSeg u' → f' r = f r) (hscan : ∀ (r : A → Prop), (∃ (x : A), WMSetLe WMLe (wmSeg x) r) → (∀ (x : A), r ≠ wmSeg x) → ∃ (τ : A), WMTr τ ∧ WMSrc τ q' ∧ WMRead τ (f' r) ∧ WMDst τ q' ∧ WMWrite τ (f' r) ∧ ¬WMRight τ) : Relation.ReflTransGen (wideData A).Step { state := Sum.inr q, head := Sum.inl (wmSeg u'), tape := wideTape f b } { state := Sum.inr q', head := Sum.inl (wmSeg u), tape := wideTape f' b }

One move of a register walk, downwards, over the file the input channel marks.

theorem DescriptiveComplexity.reaches_regWalkBack {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) {b : A} {st : A → A} {tp : A → (A → Prop) → A} {u₁ : A} (hmove : ∀ (u u' : A), WMSucc A u u' → WMLe u' u₁ → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u'), head := Sum.inl (wmSeg u'), tape := wideTape (tp u') b } { state := Sum.inr (st u), head := Sum.inl (wmSeg u), tape := wideTape (tp u) b }) (u : A) : WMLe u u₁ → Relation.ReflTransGen (wideData A).Step { state := Sum.inr (st u₁), head := Sum.inl (wmSeg u₁), tape := wideTape (tp u₁) b } { state := Sum.inr (st u), head := Sum.inl (wmSeg u), tape := wideTape (tp u) b }

A register walk, downwards, over the file the input channel marks.

def DescriptiveComplexity.regBit {A : Type} [FirstOrder.Language.wide.Structure A] (m r : A → Prop) : Prop

What a track shows at a cell of the file the input channel marks.

Equations

• DescriptiveComplexity.regBit m r = DescriptiveComplexity.bitAtOf DescriptiveComplexity.wmSeg m r

@[simp]

theorem DescriptiveComplexity.regBit_wmSeg {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (m : A → Prop) (u : A) : regBit m (wmSeg u) ↔ m u

theorem DescriptiveComplexity.regBit_congr {A : Type} [FirstOrder.Language.wide.Structure A] {m m' : A → Prop} {u : A} (hag : ∀ (v : A), v ≠ u → (m v ↔ m' v)) {r : A → Prop} (hr : r ≠ wmSeg u) : regBit m r = regBit m' r

The coherence condition of the three passes, discharged, at the file the input channel marks.

The accumulator of a downward pass

A pass down the register file carries one bit of information in its control: whether everything it has seen so far behaved. Since it walks downwards, “so far” is “at every register above the one it is on”, and the two states of the pass are therefore a function of the suffix. Both subroutines built on the walk – the mirror increment (DescriptiveComplexity.Problems.Wide.Mirror) and the file tests (DescriptiveComplexity.Problems.Wide.Test) – are that shape, so it is settled here.

noncomputable def DescriptiveComplexity.accState {A I : Type} (ile : I → I → Prop) (P : I → Prop) (qy qn : A) (w : I) : A

The state a downward pass is in on arriving at the register of w: the first state exactly when the property holds at every register strictly above.

Equations

• DescriptiveComplexity.accState ile P qy qn w = if ∀ (v : I), DescriptiveComplexity.WMLt ile w v → P v then qy else qn

noncomputable def DescriptiveComplexity.accStateAfter {A I : Type} (ile : I → I → Prop) (P : I → Prop) (qy qn : A) (w : I) : A

The state a downward pass is in on leaving the register of w: the same with w itself taken into account.

Equations

• DescriptiveComplexity.accStateAfter ile P qy qn w = if ∀ (v : I), ile w v → P v then qy else qn

theorem DescriptiveComplexity.accStateAfter_succ {A I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} (h : IsLinOrd ile) {u u' : I} (hs : IxSucc ile u u') : accStateAfter ile P qy qn u' = accState ile P qy qn u

Leaving one register is arriving at the next one down.

theorem DescriptiveComplexity.accState_top {A I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} {top : I} (htop : ∀ (v : I), ile v top) : accState ile P qy qn top = qy

At the last register nothing has been seen yet, so the pass starts in the first state.

theorem DescriptiveComplexity.accState_cases {A I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} (w : I) : accState ile P qy qn w = qy ∨ accState ile P qy qn w = qn

A pass is in one of its two states, whatever it has seen.

theorem DescriptiveComplexity.accStateAfter_bot_neg {A I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} {bot : I} (hbot : ∀ (v : I), ile bot v) {u : I} (hu : ¬P u) : accStateAfter ile P qy qn bot = qn

A pass that saw a failure ends in the second state.

theorem DescriptiveComplexity.accStateAfter_bot_pos {A I : Type} {ile : I → I → Prop} {P : I → Prop} {qy qn : A} {bot : I} (hall : ∀ (u : I), P u) : accStateAfter ile P qy qn bot = qy

A pass that saw no failure ends in the first state.