The clocked program lays its file out

The file-laying phase, assembled: the run (DescriptiveComplexity.Draw.Prog.reachesIn_buildFile) at the layout of DescriptiveComplexity.Draw.Data.blkLaid, the write and the pointer of DescriptiveComplexity.Draw.Data.buildSpec, and the rules of DescriptiveComplexity.Draw.Data.nexRule.

What ties them is that a sweep of the file's stretch is a walk of the file: every address the sweep stops at is some register's cell (DescriptiveComplexity.exists_ixSegCell_eq), and the address it moves to is the cell of the register the pointer moves to (DescriptiveComplexity.wmIncr_ixSegCell). So the phase and the control at an address are read off the register that address is – the block into the phase, the tuple into the control – and the step the sweep asks for is one of the three rules at that phase, chosen by whether the pointer's tuple is the last of its block.

What the run asks of the tape outside the stretch is that it be what the background says there, not that it be blank: the marker is planted before the file is laid, and the marker's cell lies below the file.

The run is DescriptiveComplexity.Draw.Data.reachesIn_buildBlkFile, and what it costs is the stretch: one step per register, which is (|K| + 1) · |A| ^ dd₀ of them (DescriptiveComplexity.card_blkFile).

The guessing phase is the same walk over the same registers, writing at each the value the certificate has there (DescriptiveComplexity.Draw.Data.reachesIn_guessBlkTracks); it exists for every certificate, which is what makes it a guess. Only the write differs, so the two share the pointer, the phase family and the step's case analysis.

After either sweep the machine stands one cell past the file: it steps back onto the last register (DescriptiveComplexity.Draw.Data.step_doneBack) and walks down to the marker (reachesIn_homeAfterBuild), which is DescriptiveComplexity.Draw.HomeKit's walk at the file's own top.

The three chain into DescriptiveComplexity.Draw.Data.reachesIn_buildPhase, whose budget is 2 · card + base: the stretch out and back, the turn-around, and the descent from the file's foot to the marker. DescriptiveComplexity.Draw.Data.reachesIn_guessPhase is the guess's copy of that, at the same number – it is the same walk.

The three single steps that join the phases are here as well: DescriptiveComplexity.Draw.Data.step_startBuild plants the marker and enters the file, step_homeBuildExit turns round at the marker and re-enters it for the guess, and step_homeGuessExit enters the evaluation. The whole opening is those five legs, and DescriptiveComplexity.TMData.reachesIn_five adds them up: twice a phase and three steps.

noncomputable def DescriptiveComplexity.Draw.Data.regAt {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R' P' I) (dflt : I) (r : Univ A R' P' dt.KIx dt.dd → Prop) : I

The register an address is, where it is one: what the pointer holds when the sweep stands there.

Equations

• DescriptiveComplexity.Draw.Data.regAt F dflt r = if h : ∃ (v : I), r = F.cell v then h.choose else dflt

theorem DescriptiveComplexity.Draw.Data.regAt_cell {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {I : Type} {F : LaidFile dt A R' P' I} (hinj : Function.Injective F.cell) (dflt v : I) : regAt F dflt (F.cell v) = v

At a register's cell it is that register.

The step the sweep asks for, at a register

theorem DescriptiveComplexity.Draw.Data.hasRight_buildAt {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one (dt.buildSpec PR.zero PR.one coord) γ ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (v : Wide.BlkIx dt.KIx A dt.dd) (hv : v ≠ blkTop A dt.KIx dt.dd) (g : dt.SlotIx → A) : PR.HasRight (NexPh.buildP v.1) (dt.ctlOf coord f₀ v.2) g (NexPh.buildP (blkNext A dt.KIx dt.dd v).1) (dt.ctlOf coord f₀ (blkNext A dt.KIx dt.dd v).2) (dt.buildWr PR.zero PR.one coord v.1 (dt.ctlOf coord f₀ v.2))

The file-laying sweep's step at a register short of the last: whichever of the two rules the pointer's tuple selects – stay in the block, or roll over into the next – it writes the register's mark, advances the pointer to the next register and moves right. Which one fired is invisible from here, which is what lets the run treat the sweep as one step per register.

theorem DescriptiveComplexity.Draw.Data.hasRight_buildAtTop {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one (dt.buildSpec PR.zero PR.one coord) γ ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (g : dt.SlotIx → A) : PR.HasRight (NexPh.buildP (blkTop A dt.KIx dt.dd).1) (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2) g NexPh.buildDoneP (dt.ctlOf coord f₀ (blkNext A dt.KIx dt.dd (blkTop A dt.KIx dt.dd)).2) (dt.buildWr PR.zero PR.one coord (blkTop A dt.KIx dt.dd).1 (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2))

The step at the last register: the same write and the same advance, into the phase one cell past the file, where the machine turns round.

The phase and the control at an address

noncomputable def DescriptiveComplexity.Draw.Data.phAt {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {J : Type} (G : LaidFile dt A R' (NexPh (Option dt.KIx) PE) J) (blk : J → Option dt.KIx) (inb : Option dt.KIx → NexPh (Option dt.KIx) PE) (done : NexPh (Option dt.KIx) PE) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) : NexPh (Option dt.KIx) PE

The phase at an address: the sweep's phase at the block of the register it is, and the turn-around phase off the file – which is where the sweep's last step lands. Both sweeps use it, at their own two phases.

Equations

• DescriptiveComplexity.Draw.Data.phAt G blk inb done r = if h : ∃ (v : J), r = G.cell v then inb (blk h.choose) else done

noncomputable def DescriptiveComplexity.Draw.Data.fcAt {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {I : Type} (F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I) (dflt : I) (coord : Fin dt.dd → dt.CtlIx) (f₀ : dt.CtlIx → A) (tup : I → Fin dt.dd → A) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) : dt.CtlIx → A

The control at an address: the pointer holding the tuple of the register it is.

Equations

• DescriptiveComplexity.Draw.Data.fcAt F dflt coord f₀ tup r = dt.ctlOf coord f₀ (tup (DescriptiveComplexity.Draw.Data.regAt F dflt r))

theorem DescriptiveComplexity.Draw.Data.phAt_cell {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {I : Type} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} (hinj : Function.Injective F.cell) (blk : I → Option dt.KIx) (inb : Option dt.KIx → NexPh (Option dt.KIx) PE) (done : NexPh (Option dt.KIx) PE) (v : I) : phAt F blk inb done (F.cell v) = inb (blk v)

At a register's cell the phase is that register's block.

theorem DescriptiveComplexity.Draw.Data.phAt_not_cell {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {I : Type} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {blk : I → Option dt.KIx} {inb : Option dt.KIx → NexPh (Option dt.KIx) PE} {done : NexPh (Option dt.KIx) PE} {r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hr : ∀ (v : I), r ≠ F.cell v) : phAt F blk inb done r = done

Off the file the phase is the turn-around one.

theorem DescriptiveComplexity.Draw.Data.fcAt_cell {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {I : Type} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {dflt : I} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} (hinj : Function.Injective F.cell) (tup : I → Fin dt.dd → A) (v : I) : fcAt F dflt coord f₀ tup (F.cell v) = dt.ctlOf coord f₀ (tup v)

At a register's cell the control holds that register's tuple.

theorem DescriptiveComplexity.Draw.Data.fcAt_not_cell {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {I : Type} {F : LaidFile dt A R' (NexPh (Option dt.KIx) PE) I} {dflt : I} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {tup : I → Fin dt.dd → A} {r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hr : ∀ (v : I), r ≠ F.cell v) : fcAt F dflt coord f₀ tup r = dt.ctlOf coord f₀ (tup dflt)

Off the file the control holds the default register's tuple.

The written symbol

theorem DescriptiveComplexity.Draw.Data.buildWr_eq_passTracks {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (hmir : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.mir u) (htgt : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.tgt u) (hsav : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.sav u) (hval : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.val u) (hwk : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.wk ((dt.blkLaid h hpos hbase).cell v)) (hbot : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.bot ((dt.blkLaid h hpos hbase).cell v)) (hltp : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.ltp ((dt.blkLaid h hpos hbase).cell v)) (hold : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.old i ((dt.blkLaid h hpos hbase).cell v)) (hnew : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.new i ((dt.blkLaid h hpos hbase).cell v)) (v : Wide.BlkIx dt.KIx A dt.dd) (f : dt.CtlIx → A) (hf : dt.ptrTup coord f = v.2) : dt.buildWr PR.zero PR.one coord v.1 f = PR.passTracksAt (dt.blkLaid h hpos hbase).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos hbase).toLayout PR.zero PR.one ⋯ st) (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) ((dt.blkLaid h hpos hbase).cell v)

The sweep's write is the symbol the run asks for: the background of the file at the register's cell, presented along the walked track. The track carries no register digit – the file is being laid, nothing is marked yet – so what the presentation adds is the blank the mark already has there.

The run

theorem DescriptiveComplexity.Draw.Data.hasRight_buildSweep {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one (dt.buildSpec PR.zero PR.one coord) γ ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (hmir : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.mir u) (htgt : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.tgt u) (hsav : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.sav u) (hval : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.val u) (hwk : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.wk ((dt.blkLaid h hpos ⋯).cell v)) (hbot : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.bot ((dt.blkLaid h hpos ⋯).cell v)) (hltp : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.ltp ((dt.blkLaid h hpos ⋯).cell v)) (hold : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.old i ((dt.blkLaid h hpos ⋯).cell v)) (hnew : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.new i ((dt.blkLaid h hpos ⋯).cell v)) {bg₀ : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} (s u : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) (hi : WMIncr WMLe s u) (hlb : WMSetLe WMLe ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) s) (hub : WMSetLe WMLe u (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base)) : PR.HasRight (phAt (dt.blkLaid h hpos ⋯) Prod.fst NexPh.buildP NexPh.buildDoneP s) (fcAt (dt.blkLaid h hpos ⋯) (blkTop A dt.KIx dt.dd) coord f₀ Prod.snd s) (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir bg₀ (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) s) (phAt (dt.blkLaid h hpos ⋯) Prod.fst NexPh.buildP NexPh.buildDoneP u) (fcAt (dt.blkLaid h hpos ⋯) (blkTop A dt.KIx dt.dd) coord f₀ Prod.snd u) (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) s)

The step of the file-laying sweep, at an arbitrary address of the stretch: the address is some register's cell, and the rule at that register writes its mark, advances the pointer and moves right – onto the next register's cell, or, at the last, onto the address past the file.

theorem DescriptiveComplexity.Draw.Data.reachesIn_buildBlkFile {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {rEmb : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one (dt.buildSpec PR.zero PR.one coord) γ ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (hmir : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.mir u) (htgt : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.tgt u) (hsav : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.sav u) (hval : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.val u) (hwk : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.wk ((dt.blkLaid h hpos ⋯).cell v)) (hbot : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.bot ((dt.blkLaid h hpos ⋯).cell v)) (hltp : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.ltp ((dt.blkLaid h hpos ⋯).cell v)) (hold : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.old i ((dt.blkLaid h hpos ⋯).cell v)) (hnew : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.new i ((dt.blkLaid h hpos ⋯).cell v)) {bg₀ : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hbelow : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) → dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st r = bg₀ r) (habove : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), ¬WMSetLt WMLe r (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) → dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st r = bg₀ r) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) - wideRank ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd))) { state := Sum.inr (PR.stElt (NexPh.buildP (blkBot A dt.KIx dt.dd).1) (dt.ctlOf coord f₀ (blkBot A dt.KIx dt.dd).2)), head := Sum.inl ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir bg₀ fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.buildDoneP (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2)), head := Sum.inl (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) }

The clocked program lays its file out: from the first register's cell to the address one past the last, one step per register, turning the blank the tape starts with into the background of the file it has built.

The run is DescriptiveComplexity.Draw.Prog.reachesIn_buildFile's, at the layout of a clocked program's file, with the write and the pointer of DescriptiveComplexity.Draw.Data.buildSpec and the rules of DescriptiveComplexity.Draw.Data.nexRule; what it costs is the stretch, one step per register.

The guessing sweep

The same walk over the same registers, with DescriptiveComplexity.Draw.Data.guessSpec in place of buildSpec: what changes at a cell is the stage tracks, and which value is written there is a shape of the rule, so the sweep is the program's one nondeterministic phase. The steps below are the build's with the guessed value carried along.

theorem DescriptiveComplexity.Draw.Data.hasRight_guessAt {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] {SE PE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β' : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmbG : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrulesG : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmbG i ρ) = dt.nexRule PR.one β' (dt.guessSpec PR.zero PR.one coord) ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (v : Wide.BlkIx dt.KIx A dt.dd) (hv : v ≠ blkTop A dt.KIx dt.dd) (x : dt.d.B.ι → Bool) (g : dt.SlotIx → A) : PR.HasRight (NexPh.guessP v.1) (dt.ctlOf coord f₀ v.2) g (NexPh.guessP (blkNext A dt.KIx dt.dd v).1) (dt.ctlOf coord f₀ (blkNext A dt.KIx dt.dd v).2) (dt.guessWr PR.zero PR.one x g)

The guessing sweep's step at a register short of the last, at one value.

theorem DescriptiveComplexity.Draw.Data.hasRight_guessAtTop {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] {SE PE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β' : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmbG : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrulesG : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmbG i ρ) = dt.nexRule PR.one β' (dt.guessSpec PR.zero PR.one coord) ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (x : dt.d.B.ι → Bool) (g : dt.SlotIx → A) : PR.HasRight (NexPh.guessP (blkTop A dt.KIx dt.dd).1) (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2) g NexPh.guessDoneP (dt.ctlOf coord f₀ (blkNext A dt.KIx dt.dd (blkTop A dt.KIx dt.dd)).2) (dt.guessWr PR.zero PR.one x g)

The guessing sweep's step at the last register.

theorem DescriptiveComplexity.Draw.Data.hasRight_guessSweep {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β' : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmbG : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrulesG : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmbG i ρ) = dt.nexRule PR.one β' (dt.guessSpec PR.zero PR.one coord) ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) (s u : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) (hi : WMIncr WMLe s u) (hlb : WMSetLe WMLe ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) s) (hub : WMSetLe WMLe u (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base)) : PR.HasRight (phAt (dt.blkLaid h hpos ⋯) Prod.fst NexPh.guessP NexPh.guessDoneP s) (fcAt (dt.blkLaid h hpos ⋯) (blkTop A dt.KIx dt.dd) coord f₀ Prod.snd s) (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) s) (phAt (dt.blkLaid h hpos ⋯) Prod.fst NexPh.guessP NexPh.guessDoneP u) (fcAt (dt.blkLaid h hpos ⋯) (blkTop A dt.KIx dt.dd) coord f₀ Prod.snd u) (PR.passTracksAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) (fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) s)

The step of the guessing sweep, at an arbitrary address of the stretch: the address is some register's cell, and the rule at that register writes the value the certificate has there onto the stage tracks, advances the pointer and moves right. Which value it is, is the shape – the program's one guess.

theorem DescriptiveComplexity.Draw.Data.reachesIn_guessBlkTracks {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} {β' : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} {rEmbG : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} (hrulesG : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmbG i ρ) = dt.nexRule PR.one β' (dt.guessSpec PR.zero PR.one coord) ruleE evalEntry bot i ρ) (hcoord : Function.Injective coord) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) ∨ ¬WMSetLt WMLe r (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) → (σ i r ↔ st.old i r)) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) - wideRank ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd))) { state := Sum.inr (PR.stElt (NexPh.guessP (blkBot A dt.KIx dt.dd).1) (dt.ctlOf coord f₀ (blkBot A dt.KIx dt.dd).2)), head := Sum.inl ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.guessDoneP (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2)), head := Sum.inl (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) }

The clocked program guesses its certificate: the same walk over the same registers as the file-laying sweep, writing at each the value the certificate has there. Which value that is, is the rule's shape, so the run exists for every certificate – which is what makes the phase a guess and the program nondeterministic exactly here.

The turn-around and the walk home

theorem DescriptiveComplexity.Draw.Data.step_doneBack {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : Wide.BlkIx dt.KIx A dt.dd → Prop} {f : dt.CtlIx → A} {p p' : NexPh (Option dt.KIx) PE} (hex : ∀ (g : dt.SlotIx → A), PR.HasLeft p f g p' f g) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt p f), head := Sum.inl (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt p' f), head := Sum.inl ((dt.blkLaid h hpos ⋯).cell (blkTop A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir rest m) (PR.syElt PR.blank) }

The turn-around after a sweep: standing one cell past the file in the done phase, the machine steps back onto the last register, and its walk home begins there. The step writes nothing, so both sides read the same tape.

theorem DescriptiveComplexity.Draw.Data.reachesIn_homeAfterBuild {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {PE : Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} {v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hwkS : st.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) => r = v) {f : dt.CtlIx → A} {ph : NexPh (Option dt.KIx) PE} {rHome : HomeKit.HomeRule → R'} (hrulesH : ∀ (ρ : HomeKit.HomeRule), PR.rules (rHome ρ) = { t := Slot.mir, wk := Slot.wk, ph := ph }.rule PR.one ρ) (hle : WMSetLe WMLe v ((dt.blkLaid h hpos hbase).cell (blkTop A dt.KIx dt.dd))) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank ((dt.blkLaid h hpos hbase).cell (blkTop A dt.KIx dt.dd)) - wideRank v) { state := Sum.inr (PR.stElt ph f), head := Sum.inl ((dt.blkLaid h hpos hbase).cell (blkTop A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos hbase).toLayout PR.zero PR.one ⋯ st) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt ph f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos hbase).toLayout PR.zero PR.one ⋯ st) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) }

The walk home after a sweep: from the last register down to the marker, one step per address, the tape riding along.

theorem DescriptiveComplexity.Draw.Data.reachesIn_buildPhase {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} (hcoord : Function.Injective coord) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (hmir : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.mir u) (htgt : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.tgt u) (hsav : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.sav u) (hval : ∀ (u : Wide.BlkIx dt.KIx A dt.dd), ¬st.val u) (hwk : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.wk ((dt.blkLaid h hpos ⋯).cell v)) (hbot : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.bot ((dt.blkLaid h hpos ⋯).cell v)) (hltp : ∀ (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.ltp ((dt.blkLaid h hpos ⋯).cell v)) (hold : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.old i ((dt.blkLaid h hpos ⋯).cell v)) (hnew : ∀ (i : dt.d.B.ι) (v : Wide.BlkIx dt.KIx A dt.dd), ¬st.new i ((dt.blkLaid h hpos ⋯).cell v)) {v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hwkS : st.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) => r = v) (hv0 : wideRank v = 0) (hle : WMSetLe WMLe v ((dt.blkLaid h hpos ⋯).cell (blkTop A dt.KIx dt.dd))) {bg₀ : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} (hbelow : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) → dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st r = bg₀ r) (habove : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), ¬WMSetLt WMLe r (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) → dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st r = bg₀ r) {rEmbB : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} (hrulesB : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbB i ρ) = dt.nexRule PR.one (dt.buildSpec PR.zero PR.one coord) γ ruleE evalEntry bot i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (2 * Nat.card (Wide.BlkIx dt.KIx A dt.dd) + base) { state := Sum.inr (PR.stElt (NexPh.buildP (blkBot A dt.KIx dt.dd).1) (dt.ctlOf coord f₀ (blkBot A dt.KIx dt.dd).2)), head := Sum.inl ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir bg₀ fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.homeBuildP (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) }

The whole opening phase: from the first register's cell with the pointer at the first register, the machine lays the file out, turns round one cell past it, and walks home to the marker – in twice the file's length and its base, which is the stretch out and back with the turn-around and the descent below the file.

theorem DescriptiveComplexity.Draw.Data.reachesIn_guessPhase {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {coord : Fin dt.dd → dt.CtlIx} {f₀ : dt.CtlIx → A} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} (hcoord : Function.Injective coord) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) < Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {st : TapeSt dt A R' (NexPh (Option dt.KIx) PE) (Wide.BlkIx dt.KIx A dt.dd)} (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → Prop) {v : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hwkS : { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) => r = v) (hv0 : wideRank v = 0) (hle : WMSetLe WMLe v ((dt.blkLaid h hpos ⋯).cell (blkTop A dt.KIx dt.dd))) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), WMSetLt WMLe r ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)) ∨ ¬WMSetLt WMLe r (ixSegTop (Wide.BlkIx dt.KIx A dt.dd) h base) → (σ i r ↔ st.old i r)) {rEmbG2 : (i : NexSite SE) → NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i → R'} {betaG : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesG2 : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) (dt.d.B.ι → Bool) ShE i), PR.rules (rEmbG2 i ρ) = dt.nexRule PR.one betaG (dt.guessSpec PR.zero PR.one coord) ruleE evalEntry bot i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (2 * Nat.card (Wide.BlkIx dt.KIx A dt.dd) + base) { state := Sum.inr (PR.stElt (NexPh.guessP (blkBot A dt.KIx dt.dd).1) (dt.ctlOf coord f₀ (blkBot A dt.KIx dt.dd).2)), head := Sum.inl ((dt.blkLaid h hpos ⋯).cell (blkBot A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ st) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.homeGuessP (dt.ctlOf coord f₀ (blkTop A dt.KIx dt.dd).2)), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos ⋯).cell Slot.mir (dt.ixBack (dt.blkLaid h hpos ⋯).toLayout PR.zero PR.one ⋯ { mir := st.mir, tgt := st.tgt, sav := st.sav, val := st.val, old := σ, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) fun (x : Wide.BlkIx dt.KIx A dt.dd) => False) (PR.syElt PR.blank) }

The whole guessing phase: the same three legs at the guess's own phases, and the same count – the guess is the file-laying walk with a different write, so it costs exactly what that one costs.

theorem DescriptiveComplexity.Draw.Data.step_startBuild {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {v v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') {rest rest' : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : Wide.BlkIx dt.KIx A dt.dd → Prop} {f : dt.CtlIx → A} (hframe : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), r ≠ v → rest' r = rest r) (hwr : PR.passTracksAt (dt.blkLaid h hpos hbase).cell Slot.mir rest' m v = Function.update (Function.update (PR.passTracksAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m v) Slot.wk PR.one) Slot.bot PR.one) {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry (blkBot A dt.KIx dt.dd).1 i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.start f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest' m) (PR.syElt PR.blank) }

The opening step: from the empty address the machine plants the marker and moves right, into the walk that takes it to the file's base. The base is above the program's data, so it is not the marker's neighbor and the walk is not a step.

theorem DescriptiveComplexity.Draw.Data.reachesIn_approachWalk {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {s₀ s₁ : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hle : WMSetLe WMLe s₀ s₁) {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : Wide.BlkIx dt.KIx A dt.dd → Prop} {f : dt.CtlIx → A} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry (blkBot A dt.KIx dt.dd).1 i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) }

The approach walk: the machine moves right in one phase, writing nothing, from wherever the opening step left it up to any address it likes. Its cost is the stretch it crosses.

theorem DescriptiveComplexity.Draw.Data.step_approachEnter {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {x : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe x ((dt.blkLaid h hpos hbase).cell (blkBot A dt.KIx dt.dd))) {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : Wide.BlkIx dt.KIx A dt.dd → Prop} {f : dt.CtlIx → A} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry (blkBot A dt.KIx dt.dd).1 i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl x, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.buildP (blkBot A dt.KIx dt.dd).1) f), head := Sum.inl ((dt.blkLaid h hpos hbase).cell (blkBot A dt.KIx dt.dd)), tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) }

The approach's exit: the machine stops walking and moves right into the phase that lays the first block, so the file's first register is where it has arrived.

theorem DescriptiveComplexity.Draw.Data.step_homeBuildExit {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Nonempty A] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {v s₀ : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v s₀) {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : Wide.BlkIx dt.KIx A dt.dd → Prop} {f : dt.CtlIx → A} (hex : dt.exitG PR.one (PR.passTracksAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m v)) {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry (blkBot A dt.KIx dt.dd).1 i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.homeBuildP f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.guessP (blkBot A dt.KIx dt.dd).1) (betaS.st0 f (PR.passTracksAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m v))), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) }

The dispatch out of the walk home: at the marker, the machine turns round and moves right into the guessing phase – the step between the file-laying phase and the guess. Where it lands is the marker's neighbor, which is where the guess begins: the certificate lives in the data region, below the file. It writes nothing.

theorem DescriptiveComplexity.Draw.Data.step_homeGuessExit {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {bot : Option dt.KIx} (hR : PR.table.Reads) (h : IsLinOrd WMLe) {base : ℕ} (hpos : 0 < base) (hbase : base + Nat.card (Wide.BlkIx dt.KIx A dt.dd) ≤ Nat.card { p : WPoint (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd) // (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Posn p }) {v v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {m : Wide.BlkIx dt.KIx A dt.dd → Prop} {f : dt.CtlIx → A} (hex : dt.exitG PR.one (PR.passTracksAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m v)) {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry bot i ρ) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.homeGuessP f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP evalEntry) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (dt.blkLaid h hpos hbase).cell Slot.mir rest m) (PR.syElt PR.blank) }

The dispatch into the evaluation: at the marker after the guess's walk home, the machine enters the evaluation's first phase one cell to the right.

The opening's steps, at any file

The five steps above read the file only through the presentation of the tape – Prog.trackTapeAt cell … – so they hold at whatever cells a program's file has. A program that is handed its file (DescriptiveComplexity.WideRegAccept) uses them at the channel's cells, where a program that lays one uses them at DescriptiveComplexity.Draw.Data.blkLaid. Nothing but the presentation changes, and the two sweep sites the steps mention are parameters already.

theorem DescriptiveComplexity.Draw.Data.step_startAny {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest rest' : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {v v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (hframe : ∀ (r : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop), r ≠ v → rest' r = rest r) (hwr : PR.passTracksAt cell Slot.mir rest' m v = Function.update (Function.update (PR.passTracksAt cell Slot.mir rest m v) Slot.wk PR.one) Slot.bot PR.one) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.start f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt cell Slot.mir rest' m) (PR.syElt PR.blank) }

The opening step, at any file: the machine plants the marker and the bottom mark at the cell it starts on and moves right into the approach.

theorem DescriptiveComplexity.Draw.Data.reachesIn_approachAny {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {s₀ s₁ : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hle : WMSetLe WMLe s₀ s₁) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).ReachesIn (wideRank s₁ - wideRank s₀) { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl s₁, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) }

The approach walk, at any file: the machine moves right in one phase, writing nothing, as far as it likes.

theorem DescriptiveComplexity.Draw.Data.step_approachEnterAny {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {x y : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe x y) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.approachP f), head := Sum.inl x, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.buildP botS) f), head := Sum.inl y, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) }

The approach's exit, at any file: the machine stops walking and moves right into the sweep's first phase.

theorem DescriptiveComplexity.Draw.Data.step_homeBuildExitAny {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {v s₀ : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v s₀) (hex : dt.exitG PR.one (PR.passTracksAt cell Slot.mir rest m v)) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.homeBuildP f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.guessP botS) (betaS.st0 f (PR.passTracksAt cell Slot.mir rest m v))), head := Sum.inl s₀, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) }

The dispatch out of the walk home, at any file: at the marker the machine turns round into the guessing phase, its pointer reset by the sweep's own st0.

theorem DescriptiveComplexity.Draw.Data.step_homeGuessExitAny {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {v v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (hex : dt.exitG PR.one (PR.passTracksAt cell Slot.mir rest m v)) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.homeGuessP f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP evalEntry) f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) }

The dispatch into the evaluation, at any file.

theorem DescriptiveComplexity.Draw.Data.step_sweepDone {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {v v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (hroll : betaS.Roll botS f) (hdone : betaS.Done botS f) (hst : betaS.stRoll botS f (PR.passTracksAt cell Slot.mir rest m v) = f) (hwr : betaS.wr botS f (PR.passTracksAt cell Slot.mir rest m v) = PR.passTracksAt cell Slot.mir rest m v) : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (NexPh.buildP botS) f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.buildDoneP f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) }

A sweep that is over at once, in one step: when both of the sweep's tests hold where it starts, the phase fires its exit rule – it writes what the spec writes and leaves the pointer where the spec's roll-over leaves it, which for DescriptiveComplexity.Draw.Data.nullSpec is nothing and the same pointer. This is the whole of the file-laying phase of a program that is handed its file.

theorem DescriptiveComplexity.Draw.Data.step_doneBackAny {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [LinearOrder A] [LinearOrder R'] {SE PE G : Type} {ShE : SE → Type} [Fintype dt.CtlIx] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [Finite A] [Finite R'] [Finite dt.KIx] [LinearOrder (NexPh (Option dt.KIx) PE)] [Finite (NexPh (Option dt.KIx) PE)] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) PE) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {ruleE : (e : SE) → ShE e → Rule A dt.CtlIx dt.SlotIx (NexPh (Option dt.KIx) PE)} {evalEntry : PE} {I : Type} {cell : I → Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} {m : I → Prop} {rest : (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop) → dt.SlotIx → A} {f : dt.CtlIx → A} {botS : Option dt.KIx} {rEmbS : (i : NexSite SE) → NexSh SE (Option dt.KIx) G ShE i → R'} {betaS : SweepSpec A dt.CtlIx dt.SlotIx (Option dt.KIx)} (hrulesS : ∀ (i : NexSite SE) (ρ : NexSh SE (Option dt.KIx) G ShE i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one betaS γ ruleE evalEntry botS i ρ) (hR : PR.table.Reads) (h : IsLinOrd WMLe) {v v' : Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') : (wideData (Univ A R' (NexPh (Option dt.KIx) PE) dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt NexPh.buildDoneP f), head := Sum.inl v', tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.homeBuildP f), head := Sum.inl v, tape := wideTape (PR.trackTapeAt cell Slot.mir rest m) (PR.syElt PR.blank) }

The turn-around after a sweep, at any file: in the done phase the machine steps back one cell and its walk home begins there. It writes nothing.