The runs: the program's rules are its kits' rules

Every composite of the layer discharges its run theorem from one hypothesis about the program – hrules : ∀ ρ, PR.rules (rEmb ρ) = κ.rule …, “my rules are among yours, under this injection of rule names”. For a program assembled from sites (DescriptiveComplexity.Draw.Data.progAsm) that hypothesis is definitional: the rule names are the sigma of the sites' shapes, so a kit's rule at site i is the program's rule at ⟨i, Sum.inl ρ⟩, verbatim.

This file is that plumbing, one lemma per call site of the outer loop, all rfl. With it, each composite's run theorem applies to the assembled program by naming its site; what a leg then needs is only the background equations, which DescriptiveComplexity.Problems.Wide.DrawBack proves once.

The designated elements

@[simp]

theorem DescriptiveComplexity.Draw.Data.prog_zero {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) : (dt.prog zero one hzo args hpl).zero = zero

@[simp]

theorem DescriptiveComplexity.Draw.Data.prog_one {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) : (dt.prog zero one hzo args hpl).one = one

The rules, site by site

Each lemma names a call site's rule-name injection: the site, and Sum.inl into its kit's shape.

theorem DescriptiveComplexity.Draw.Data.prog_rules_tgtTop {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : TrackRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.tgtTop, Sum.inl ρ⟩ = (dt.tgtTopKit one OuterPh.tgtTopP).rule zero one ρ

The startup pattern write of TARGET.

theorem DescriptiveComplexity.Draw.Data.prog_rules_seek1 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : SeekRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.seek1, Sum.inl ρ⟩ = (dt.seekKit OuterPh.seek1P).rule zero one ρ

The startup seek of the working cell to the logical top.

theorem DescriptiveComplexity.Draw.Data.prog_rules_reset1 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : ResetRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.reset1, Sum.inl ρ⟩ = { t := Slot.mir, bt := Slot.bot, wk := Slot.wk, emb := OuterPh.reset1P }.rule one ρ

The startup reset of the marker to the bottom cell.

theorem DescriptiveComplexity.Draw.Data.prog_rules_clearMir1 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : TrackRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.clearMir1, Sum.inl ρ⟩ = (dt.clearMirKit OuterPh.clearMir1P).rule zero one ρ

The startup clear of the mirror.

theorem DescriptiveComplexity.Draw.Data.prog_rules_sweepAdv {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : AdvRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.sweepAdv, Sum.inl ρ⟩ = (dt.advKit OuterPh.advP).rule zero one ρ

One round of the outer sweep.

theorem DescriptiveComplexity.Draw.Data.prog_rules_reset2 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : ResetRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.reset2, Sum.inl ρ⟩ = { t := Slot.mir, bt := Slot.bot, wk := Slot.wk, emb := OuterPh.reset2P }.rule one ρ

The post-sweep reset of the marker.

theorem DescriptiveComplexity.Draw.Data.prog_rules_clearMir2 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : TrackRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.clearMir2, Sum.inl ρ⟩ = (dt.clearMirKit OuterPh.clearMir2P).rule zero one ρ

The post-sweep clear of the mirror.

theorem DescriptiveComplexity.Draw.Data.prog_rules_compare {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : SweepRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.compare, Sum.inl ρ⟩ = (dt.compareKit one OuterPh.cmpP).rule one ρ

The convergence sweep.

theorem DescriptiveComplexity.Draw.Data.prog_rules_homeCmp {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : HomeKit.HomeRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.homeCmp, Sum.inl ρ⟩ = { t := Slot.mir, wk := Slot.wk, ph := OuterPh.homeCmpP }.rule one ρ

The walk home after a failed convergence sweep.

theorem DescriptiveComplexity.Draw.Data.prog_rules_copy {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : WSweepRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.copy, Sum.inl ρ⟩ = (dt.copyKit OuterPh.copyP).rule one ρ

The copy-back sweep.

theorem DescriptiveComplexity.Draw.Data.prog_rules_homeCopy {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : HomeKit.HomeRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.homeCopy, Sum.inl ρ⟩ = { t := Slot.mir, wk := Slot.wk, ph := OuterPh.homeCopyP }.rule one ρ

The walk home after the copy-back.

theorem DescriptiveComplexity.Draw.Data.prog_rules_homeOut {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (ρ : HomeKit.HomeRule) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.homeOut, Sum.inl ρ⟩ = { t := Slot.mir, wk := Slot.wk, ph := OuterPh.homeOutP }.rule one ρ

The walk home before the output evaluation.

A rule of the assembly drives a step

The kits' discharges wrap this for their own rules; the program's bespoke rules – the startup step, the sites' exits – cite it directly.

theorem DescriptiveComplexity.Draw.Data.prog_hasRight {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (i : dt.SF) (ρ : (dt.progAsm zero one hzo args).Sh i) {f : Q → A} {g : dt.SlotIx → A} (hg : ((dt.progAsm zero one hzo args).rule i ρ).guard f g) (hmr : ((dt.progAsm zero one hzo args).rule i ρ).moveRight) : (dt.prog zero one hzo args hpl).HasRight ((dt.progAsm zero one hzo args).rule i ρ).srcPh f g ((dt.progAsm zero one hzo args).rule i ρ).dstPh (((dt.progAsm zero one hzo args).rule i ρ).dstSt f g) (((dt.progAsm zero one hzo args).rule i ρ).wr f g)

A rightward rule of the assembly is a HasRight witness, at its own destination data.

theorem DescriptiveComplexity.Draw.Data.prog_hasLeft {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) (i : dt.SF) (ρ : (dt.progAsm zero one hzo args).Sh i) {f : Q → A} {g : dt.SlotIx → A} (hg : ((dt.progAsm zero one hzo args).rule i ρ).guard f g) (hml : ¬((dt.progAsm zero one hzo args).rule i ρ).moveRight) : (dt.prog zero one hzo args hpl).HasLeft ((dt.progAsm zero one hzo args).rule i ρ).srcPh f g ((dt.progAsm zero one hzo args).rule i ρ).dstPh (((dt.progAsm zero one hzo args).rule i ρ).dstSt f g) (((dt.progAsm zero one hzo args).rule i ρ).wr f g)

A leftward rule of the assembly is a HasLeft witness.

Time zero: the initial tape is the empty state's background

The pass layer walks the background of DescriptiveComplexity.Draw.Data.back; the initial tape is DescriptiveComplexity.Draw.Prog.initBack, the marks over the blank. They are the same function, at the state where every register and marker is clear – which is why the all-blank start needs no initialization sweep, and what lets the first leg of the run be stated in the presentation all the others use.

noncomputable def DescriptiveComplexity.Draw.Data.emptySt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} : TapeStD dt A R' P'

The machine's state at time zero: every register, stage track and marker clear.

Equations

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

theorem DescriptiveComplexity.Draw.Data.initBack_eq_back {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hlin : IsLinOrd WMLe) : (dt.prog zero one hzo args hpl).initBack = dt.back wmSeg zero one ⋯ dt.emptySt

The initial tape is the empty state's background.

The first leg: startup plants the two permanent markers

The one rule of the start site fires wherever it stands – it stands at the empty address – writes the working-cell marker and the bottom mark there and steps right, into the pattern write of TARGET.

noncomputable def DescriptiveComplexity.Draw.Data.startSt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} : TapeStD dt A R' P'

The state after the startup step: the marker and the bottom mark at the empty address, everything else still clear.

Equations

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

theorem DescriptiveComplexity.Draw.Data.step_start {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') : (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.start fun (x : Q) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.emptySt) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.tgtTopP TrackPh.up) fun (x : Q) => zero), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.startSt) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The startup step: from the initial configuration to the entry of the TARGET pattern write, with both markers planted at the empty address.

The glue between legs

A pass presents the tape as DescriptiveComplexity.Draw.Prog.trackTapeAt: the walked track's digits computed from a set, every other slot read off the background. Since the background of DescriptiveComplexity.Draw.Data.back already carries each register's digits at its own slot, that presentation is the background – which is what lets one leg's conclusion be the next leg's hypothesis, whichever track each of them walks.

theorem DescriptiveComplexity.Draw.Data.trackTape_back {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] {st st' : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {t : dt.SlotIx} {m : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hagree : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) (s : dt.SlotIx), s ≠ t → dt.back wmSeg zero one ⋯ st r s = dt.back wmSeg zero one ⋯ st' r s) (ht : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), dt.back wmSeg zero one ⋯ st' r t = bitVal zero one (regBit m r)) : (dt.prog zero one hzo args hpl).trackTapeAt wmSeg t (dt.back wmSeg zero one ⋯ st) m = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => (dt.prog zero one hzo args hpl).syElt (dt.back wmSeg zero one ⋯ st' r)

A pass's presentation is the background it walks, once the walked slot's state agrees with the set the pass carries. Stated with the state after the pass, so it also reads a pass's result back into the state.

theorem DescriptiveComplexity.Draw.Data.trackTape_back_swap {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {t t' : dt.SlotIx} {m m' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (ht : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), dt.back wmSeg zero one ⋯ st r t = bitVal zero one (regBit m r)) (ht' : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), dt.back wmSeg zero one ⋯ st r t' = bitVal zero one (regBit m' r)) : (dt.prog zero one hzo args hpl).trackTapeAt wmSeg t (dt.back wmSeg zero one ⋯ st) m = (dt.prog zero one hzo args hpl).trackTapeAt wmSeg t' (dt.back wmSeg zero one ⋯ st) m'

Handing the walk between tracks costs nothing: two passes walking different registers of the same state present the same tape.

theorem DescriptiveComplexity.Draw.Data.back_mir {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] (st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF) (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) : dt.back wmSeg zero one ⋯ st r Slot.mir = bitVal zero one (regBit st.mir r)

The four machine registers carry their track's digits at their own slot, which is the hypothesis both glue lemmas ask for.

theorem DescriptiveComplexity.Draw.Data.back_tgt {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] (st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF) (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) : dt.back wmSeg zero one ⋯ st r Slot.tgt = bitVal zero one (regBit st.tgt r)

theorem DescriptiveComplexity.Draw.Data.back_val {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] (st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF) (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) : dt.back wmSeg zero one ⋯ st r Slot.val = bitVal zero one (regBit st.val r)

The second leg: startup writes the logical top into TARGET

The pattern write of DescriptiveComplexity.Draw.MapKit: a round trip up the register file writing, at each cell, the digit its other tracks decide – here “this cell's element carries an argument tag”, read off the one-hot blk marks. The result is the address of the logical top, which the seek that follows takes the working cell to.

noncomputable def DescriptiveComplexity.Draw.Data.tgtTopSt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} : TapeStD dt A R' P'

The state after startup's pattern write: TARGET holds the logical top – the cells of the argument-tagged elements.

Equations

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

theorem DescriptiveComplexity.Draw.Data.reaches_tgtTop {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {fc : Q → A} {s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.tgtTopP TrackPh.up) fc), head := Sum.inl s, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.startSt) dt.startSt.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.tgtTopP TrackPh.run) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.tgtTopSt) dt.tgtTopSt.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The pattern write's leg: from the entry of the trip to its return at the marker, with TARGET holding the logical top.

theorem DescriptiveComplexity.Draw.Data.reaches_startup₁ {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.start fun (x : Q) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.emptySt) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.tgtTopP TrackPh.run) fun (x : Q) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.tgtTopSt) dt.tgtTopSt.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The run so far, chained: from the initial configuration – the marks over the blank, the head on the empty address – to the return of the pattern write, with both markers planted and TARGET holding the logical top.

The third leg: the working cell seeks the logical top

The random access of DescriptiveComplexity.Draw.SeekKit, at the target TARGET now holds. Two single steps bracket it: the pattern write's exit steps right off the marker into the seek's loop head (as every exit into a loop head does), and the loop head's stay rule walks straight back down to it.

noncomputable def DescriptiveComplexity.Draw.Data.atSt {L : FirstOrder.Language} (dt : Data L) {A R' P' I : Type} (st : TapeSt dt A R' P' I) (v : Univ A R' P' dt.KIx dt.dd → Prop) : TapeSt dt A R' P' I

The state with the working-cell marker at a given address.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.seekEndSt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (st : TapeStD dt A R' P') (v : Univ A R' P' dt.KIx dt.dd → Prop) : TapeStD dt A R' P'

The state after the seek: the marker and the mirror both at the target.

Equations

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

theorem DescriptiveComplexity.Draw.Data.ne_empty_of_wmIncr {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] {v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') : v' ≠ fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False

The successor of the empty address is not empty: it holds the greatest element.

theorem DescriptiveComplexity.Draw.Data.step_tgtTop_exit {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) (hreg : ¬∃ (u : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) = wmSeg u) : (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.tgtTopP TrackPh.run) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.chk) fc), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The pattern write's exit: off the marker, rightwards, into the seek's loop head.

theorem DescriptiveComplexity.Draw.Data.step_seek1_home {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) : (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.chk) fc), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.chk) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The seek's loop head walks back to the marker: the one step the rightward exit above owes.

theorem DescriptiveComplexity.Draw.Data.reaches_seek1 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {fc : Q → A} : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.chk) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.tgtTopSt) dt.tgtTopSt.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.ty) fc), head := Sum.inl dt.tgtTopSt.tgt, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.seekEndSt dt.tgtTopSt dt.tgtTopSt.tgt)) (dt.seekEndSt dt.tgtTopSt dt.tgtTopSt.tgt).mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The seek's leg: from the loop head at the empty address to the passing verdict on the target's cell, marker and mirror in tow.

theorem DescriptiveComplexity.Draw.Data.reaches_startup₂ {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.start fun (x : Q) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.emptySt) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.ty) fun (x : Q) => zero), head := Sum.inl dt.tgtTopSt.tgt, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.seekEndSt dt.tgtTopSt dt.tgtTopSt.tgt)) (dt.seekEndSt dt.tgtTopSt dt.tgtTopSt.tgt).mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

Startup, up to the logical top: from the initial configuration to the verdict of the seek – the marker and the mirror on the last logical address, where the end marker is about to be planted.

The fourth leg: the end marker is planted and the marker goes home

The seek's exit is the erasing step the reset asks for as its one hypothesis: at the logical top it clears the working-cell marker, plants the permanent ltp end marker there and steps right; the reset then scans down to the bot cell, writes the marker and bounces back.

noncomputable def DescriptiveComplexity.Draw.Data.ltpSt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (st : TapeStD dt A R' P') (v : Univ A R' P' dt.KIx dt.dd → Prop) : TapeStD dt A R' P'

The state after the seek's exit: the marker erased, the end marker planted at the last logical address.

Equations

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

theorem DescriptiveComplexity.Draw.Data.reaches_reset1 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {fc : Q → A} : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.seek1P SeekPh.ty) fc), head := Sum.inl dt.tgtTopSt.tgt, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.seekEndSt dt.tgtTopSt dt.tgtTopSt.tgt)) dt.tgtTopSt.tgt) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.reset1P ResetPh.done) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.atSt (dt.ltpSt (dt.seekEndSt dt.tgtTopSt dt.tgtTopSt.tgt) dt.tgtTopSt.tgt) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False)) dt.tgtTopSt.tgt) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The reset's leg, the seek's exit included: from the passing verdict at the logical top to the reset's landing phase on the empty address, with the end marker planted.

The last leg of startup: the mirror is cleared

The reset left the mirror holding the logical top; the evaluation wants it at the empty address, matching the marker. One DescriptiveComplexity.Draw.ClearKit trip does it, entered by the reset's exit.

theorem DescriptiveComplexity.Draw.Data.step_reset1_exit {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) (hreg : ¬∃ (u : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) = wmSeg u) : (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.reset1P ResetPh.done) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.clearMir1P TrackPh.up) fc), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The reset's exit: off the marker, rightwards, into the mirror clear.

theorem DescriptiveComplexity.Draw.Data.reaches_clearMir1 {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) {s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.clearMir1P TrackPh.up) fc), head := Sum.inl s, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.clearMir1P TrackPh.run) fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := st.tgt, sav := st.sav, val := st.val, old := st.old, new := st.new, wk := st.wk, bot := st.bot, ltp := st.ltp }) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The mirror clear's leg: the trip that empties the mirror register, returning to the marker at the empty address.

noncomputable def DescriptiveComplexity.Draw.Data.startupSt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} : TapeStD dt A R' P'

The state startup leaves behind: the bottom mark at the empty address, the end marker at the logical top, TARGET holding that address, the mirror and the working-cell marker home at the empty address, every stage track still clear – which is stage zero of the iteration.

Equations

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

theorem DescriptiveComplexity.Draw.Data.reaches_startup {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.start fun (x : Q) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.emptySt) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.clearMir1P TrackPh.run) fun (x : Q) => zero), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ dt.startupSt) dt.startupSt.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

STARTUP, proved: from the initial configuration – the marks over the blank – to the entry of the per-address evaluation, with the machine's two permanent markers planted and every register where the loop expects it.

The convergence sweep

COMPARE is a plain sweep – one step per address, no register visit – whose verdict rides in the state (DescriptiveComplexity.sweepState): the passing phase exactly while every address below has agreed. Its per-cell question is read off the stage tracks, which is what DescriptiveComplexity.Draw.Data.compareKit fixes.

theorem DescriptiveComplexity.Draw.Data.reaches_compare {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {ltpAddr : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hltp : st.ltp = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr (sweepState (fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => ∀ (i : dt.d.B.ι), st.old i r ↔ st.new i r) ((dt.prog zero one hzo args hpl).stElt (OuterPh.cmpP SweepPh.py) fc) ((dt.prog zero one hzo args hpl).stElt (OuterPh.cmpP SweepPh.pn) fc) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr (sweepState (fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => ∀ (i : dt.d.B.ι), st.old i r ↔ st.new i r) ((dt.prog zero one hzo args hpl).stElt (OuterPh.cmpP SweepPh.py) fc) ((dt.prog zero one hzo args hpl).stElt (OuterPh.cmpP SweepPh.pn) fc) ltpAddr), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The convergence sweep's leg: from the empty address to the end-marked one, the verdict accumulated in the phase.

The copy-back sweep

COPY is the other plain sweep: one rewrite per address, every stage track taking its successor's digit, so that the next round's old is this round's new. Its background is a family indexed by the sweep's frontier – the addresses already passed hold the new stage, the others the old one.

noncomputable def DescriptiveComplexity.Draw.Data.copySt {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] (st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF) (s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) : TapeStD dt A (dt.RIx zero one hzo args) dt.PF

The state during the copy-back, at frontier s: the addresses strictly below s have taken their next-stage digits.

Equations

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

theorem DescriptiveComplexity.Draw.Data.reaches_copy {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {ltpAddr : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hltp : st.ltp = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.copyP fc), head := Sum.inl fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.copySt zero one hzo args st fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False)) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.copyP fc), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.copySt zero one hzo args st ltpAddr)) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The copy-back's leg: from the empty address to the end-marked one, every stage track rewritten on the way.

The walks home

A plain sweep leaves the machine at the top of the stretch while the marker never moved, so getting back is a scan: one phase, one rule. The outer program does it three times – after the convergence sweep, after the copy-back, and before the output evaluation – and they differ only in which phase they walk in.

theorem DescriptiveComplexity.Draw.Data.reaches_home {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (ph : dt.PF) {rEmb : HomeKit.HomeRule → dt.RIx zero one hzo args} (hrules : ∀ (ρ : HomeKit.HomeRule), (dt.prog zero one hzo args hpl).rules (rEmb ρ) = { t := Slot.mir, wk := Slot.wk, ph := ph }.rule one ρ) (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) {s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hle : WMSetLe WMLe v s) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt ph fc), head := Sum.inl s, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt ph fc), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

A walk home: from anywhere at or above the marker, back to it. The rule-name injection is the parameter, so the three home sites of the outer program instantiate it directly.

theorem DescriptiveComplexity.Draw.Data.reaches_homeCmp {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {v s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hle : WMSetLe WMLe v s) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeCmpP fc), head := Sum.inl s, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeCmpP fc), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The walk home after a failed convergence sweep.

theorem DescriptiveComplexity.Draw.Data.reaches_homeCopy {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {v s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hle : WMSetLe WMLe v s) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeCopyP fc), head := Sum.inl s, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeCopyP fc), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The walk home after the copy-back.

theorem DescriptiveComplexity.Draw.Data.reaches_homeOut {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) {fc : Q → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {v s : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hle : WMSetLe WMLe v s) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeOutP fc), head := Sum.inl s, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeOutP fc), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The walk home before the output evaluation.

One round of the outer sweep

ADVANCE is the round every sweep repeats: erase the marker, step on, write it at the next address, walk up to the register file, increment the mirror there so that it keeps mirroring the marker's address, and come back. Its entry – the erasing step – is the caller's rule, exactly as the reset's is, so the evaluation's boundary rule is what this leg takes as its h₀.

noncomputable def DescriptiveComplexity.Draw.Data.offSt {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} (st : TapeStD dt A R' P') : TapeStD dt A R' P'

The state with the marker erased: the middle of a marker move.

Equations

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

theorem DescriptiveComplexity.Draw.Data.reaches_sweepAdv {L : FirstOrder.Language} (dt : Data L) {A Q : Type} (zero one : A) [LinearOrder A] [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) [LinearOrder (dt.RIx zero one hzo args)] [LinearOrder dt.PF] (hpl : Fintype.card (Q ⊕ dt.SlotIx) ≤ dt.dd) [FirstOrder.Language.wide.Structure (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)] [Finite A] [Finite (dt.RIx zero one hzo args)] [Finite dt.PF] [Finite dt.KIx] (hR : (dt.prog zero one hzo args hpl).table.Reads) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {gtop gbot : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd} (htop : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe y gtop) (hbot : ∀ (y : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), WMLe gbot y) {fc : Q → A} {p₀ : dt.PF} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {v v' m' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hwk : st.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hi : WMIncr WMLe v v') (hv' : WMSetLt WMLe v' (wmSeg gbot)) (him : WMIncr WMLe st.mir m') (h₀ : (dt.prog zero one hzo args hpl).HasRight p₀ fc ((dt.prog zero one hzo args hpl).passTracksAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir v) (OuterPh.advP AdvPh.a1) fc ((dt.prog zero one hzo args hpl).passTracksAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.offSt st)) st.mir v)) : Relation.ReflTransGen (wideData (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd)).Step { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt p₀ fc), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt (OuterPh.advP AdvPh.a4) fc), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (have __src := dt.atSt st v'; { mir := m', tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) m') ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

One round of the outer sweep: the marker and the mirror both step on, in lockstep.