The outer composition: the sweep's rounds

One round of the outer sweep, at the concrete program: the whole per-address evaluation (DescriptiveComplexity.Draw.Data.evalSpine_run), the boundary dispatch into ADVANCE (the last checkpoint's erasing rule, off the ltp cell), the advance itself (DescriptiveComplexity.Draw.Data.reaches_sweepAdv), the exit dispatch into the next address's first checkpoint and its walk back. The walk is handed between the VAL track (the evaluation's presentation) and the MIRROR track (the advance's) by DescriptiveComplexity.Draw.Data.trackTape_back_swap, which costs nothing because the background carries every register's digits at its own slot.

The evaluation's rules, at the program

theorem DescriptiveComplexity.Draw.Data.prog_rules_eval {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [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 (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : dt.SEF) (ρ : dt.SESh e) : (dt.prog zero one hzo args hpl).rules ⟨OuterSite.eval e, ρ⟩ = dt.evalRuleF zero one args e ρ

The program's rule at an evaluation site is the evaluation's.

theorem DescriptiveComplexity.Draw.Data.prog_hasRight_eval {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} {e : dt.SEF} {ρ : dt.SESh e} {f f' : dt.CtlIx → A} {g g' : dt.SlotIx → A} {p p' : dt.PF} (hg : (dt.evalRuleF zero one args e ρ).guard f g) (hp : (dt.evalRuleF zero one args e ρ).srcPh = p) (hp' : (dt.evalRuleF zero one args e ρ).dstPh = p') (hf' : (dt.evalRuleF zero one args e ρ).dstSt f g = f') (hg' : (dt.evalRuleF zero one args e ρ).wr f g = g') (hmr : (dt.evalRuleF zero one args e ρ).moveRight) : (dt.prog zero one hzo args hpl).HasRight p f g p' f' g'

An evaluation rule with a true guard is a HasRight witness of the program.

theorem DescriptiveComplexity.Draw.Data.prog_hasLeft_eval {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd} {e : dt.SEF} {ρ : dt.SESh e} {f f' : dt.CtlIx → A} {g g' : dt.SlotIx → A} {p p' : dt.PF} (hg : (dt.evalRuleF zero one args e ρ).guard f g) (hp : (dt.evalRuleF zero one args e ρ).srcPh = p) (hp' : (dt.evalRuleF zero one args e ρ).dstPh = p') (hf' : (dt.evalRuleF zero one args e ρ).dstSt f g = f') (hg' : (dt.evalRuleF zero one args e ρ).wr f g = g') (hml : ¬(dt.evalRuleF zero one args e ρ).moveRight) : (dt.prog zero one hzo args hpl).HasLeft p f g p' f' g'

An evaluation rule with a true guard is a HasLeft witness of the program.

The two boundary pieces of a round

theorem DescriptiveComplexity.Draw.Data.step_evalChk_back {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {k : Fin (dt.nv + 1)} {fc : dt.CtlIx → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {mval v 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) (hvi : WMIncr WMLe v 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.evalP (EvalPh.chk k)) fc), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st) mval) ((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.evalP (EvalPh.chk k)) fc), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st) mval) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The walk back into a checkpoint: an entering dispatch lands one cell right of the marker; the checkpoint's stay rule steps back to it.

theorem DescriptiveComplexity.Draw.Data.hasRight_evalAdv {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {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) {v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (wmSeg gbot)) {fc : dt.CtlIx → 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 = v) (hltp : ¬st.ltp v) : (dt.prog zero one hzo args hpl).HasRight (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) 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)

The erasing dispatch into the advance, as the HasRight the advance's round theorem consumes: at the last checkpoint below the ltp cell, erase the marker and enter the advance – stated at the MIRROR-walked presentation the advance runs on.

theorem DescriptiveComplexity.Draw.Data.hasRight_evalReset {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {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) {v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (wmSeg gbot)) {fc : dt.CtlIx → 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 = v) (hltp : st.ltp v) : (dt.prog zero one hzo args hpl).HasRight (OuterPh.evalP (EvalPh.chk (Fin.last dt.nv))) fc ((dt.prog zero one hzo args hpl).passTracksAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ st) st.mir v) (OuterPh.reset2P ResetPh.scan) fc ((dt.prog zero one hzo args hpl).passTracksAt wmSeg Slot.mir (dt.back wmSeg zero one ⋯ (dt.offSt st)) st.mir v)

The erasing dispatch into the post-sweep reset: at the last checkpoint on the ltp cell, erase the marker and enter the reset.

The post-sweep reset and mirror clear

theorem DescriptiveComplexity.Draw.Data.reaches_reset2 {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {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) {vT : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hvT : WMSetLt WMLe vT (wmSeg gbot)) {fc : dt.CtlIx → 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 = vT) (hltp : st.ltp vT) (hbotSt : st.bot = 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) : 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.evalP (EvalPh.chk (Fin.last dt.nv))) fc), head := Sum.inl vT, 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.reset2P 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.offSt 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) }

The reset's leg after a completed sweep, the last checkpoint's erasing exit included: from the ltp cell to the reset's landing phase at the empty address, the bottom marker rewritten.

theorem DescriptiveComplexity.Draw.Data.step_reset2_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → 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.reset2P 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.clearMir2P 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 post-sweep reset's exit: off the marker, rightwards, into the mirror clear.

theorem DescriptiveComplexity.Draw.Data.reaches_clearMir2 {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → 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.clearMir2P 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.clearMir2P 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 pre-compare mirror clear's leg: the trip that empties the mirror register, returning to the marker at the empty address.

One round of the sweep

theorem DescriptiveComplexity.Draw.Data.sweepRound {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 v' v'' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hvi : WMIncr WMLe v v') (hvi' : WMIncr WMLe v' v'') (hv : WMSetLt WMLe v (wmSeg gbot)) (hv' : WMSetLt WMLe v' (wmSeg gbot)) {st₀ stE : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {fs₀ fsE : dt.CtlIx → A} (hspine : 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.evalP (EvalPh.chk 0)) fs₀), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st₀) st₀.val) ((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.evalP (EvalPh.chk (Fin.last dt.nv))) fsE), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ stE) stE.val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkE : stE.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hmirE : stE.mir = v) (hltpE : ¬stE.ltp 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.evalP (EvalPh.chk 0)) fs₀), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st₀) st₀.val) ((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.evalP (EvalPh.chk 0)) fsE), head := Sum.inl v', tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (have __src := dt.atSt stE v'; { mir := v', tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) stE.val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

One round of the outer sweep, with its evaluation: from the first checkpoint at the marker, through the whole per-address evaluation (given as a hypothesis – the caller instantiates it by DescriptiveComplexity.Draw.Data.evalSpine_run), out through the erasing boundary dispatch, the advance, and back into the first checkpoint at the next address. The marker, the mirror and the head all step on in lockstep.

The whole sweep

theorem DescriptiveComplexity.Draw.Data.reaches_sweep {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {s₀ s₁ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hs₀ : WMSetLe WMLe s₀ s₁) (hs₁ : WMSetLt WMLe s₁ (wmSeg gbot)) {SW stE : (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} {FS fsE : (Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) → dt.CtlIx → A} (hspine : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt 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.evalP (EvalPh.chk 0)) (FS v)), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (SW v)) (SW v).val) ((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.evalP (EvalPh.chk (Fin.last dt.nv))) (fsE v)), head := Sum.inl v, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (stE v)) (stE v).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkE : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → (stE v).wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = v) (hmirE : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → (stE v).mir = v) (hltpE : ∀ (v : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLe WMLe s₀ v → WMSetLt WMLe v s₁ → ¬(stE v).ltp v) (hSW : ∀ (v v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMIncr WMLe v v' → WMSetLe WMLe s₀ v → WMSetLe WMLe v' s₁ → SW v' = have __src := dt.atSt (stE v) v'; { mir := v', tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (hFS : ∀ (v v' : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMIncr WMLe v v' → WMSetLe WMLe s₀ v → WMSetLe WMLe v' s₁ → FS v' = fsE 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.evalP (EvalPh.chk 0)) (FS s₀)), head := Sum.inl s₀, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (SW s₀)) (SW s₀).val) ((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.evalP (EvalPh.chk 0)) (FS s₁)), head := Sum.inl s₁, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (SW s₁)) (SW s₁).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The outer sweep: from the first checkpoint at the bottom of the stretch to the first checkpoint at its top, one round per address – each round the per-address evaluation and the advance, glued by DescriptiveComplexity.Draw.Data.sweepRound. The evaluation runs, the end-state facts and the two cover equations (the tape and control threads across addresses) are per-address hypotheses; everything else is DescriptiveComplexity.reaches_of_wideRounds.

Entering the convergence sweep

A plain sweep cannot be entered from the left of the empty address, so clearMir2's verdict exit is COMPARE's first step: it tests the empty address's cell and lands at its successor, in exactly the sweep's state there. The sweep then continues from the successor (DescriptiveComplexity.Draw.FlagSweepKit.reaches is general in its stretch, which reaches_compareFrom exposes).

theorem DescriptiveComplexity.Draw.Data.reaches_compareFrom {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → 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) {s₀ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hle : WMSetLe WMLe s₀ 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) s₀), 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 (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 from an arbitrary start: the generalization of DescriptiveComplexity.Draw.Data.reaches_compare the folded first step needs.

theorem DescriptiveComplexity.Draw.Data.step_clearMir2_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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} (hvi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : dt.CtlIx → 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.clearMir2P 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 (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) v'), 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) }

COMPARE's folded first step: clearMir2's verdict exit tests the empty address's cell and lands at its successor, in the sweep's state there.

The compare verdicts, and the copy-back ring

At the ltp cell the sweep's verdict dispatches: passing to the output's walk home, failing to the copy-back's. The copy-back has the same folded entry as the sweep it corrects: homeCmp's exit rewrites the empty address's cell and lands at its successor, and the copy exits at the ltp cell into its own walk home, whose exit re-enters the evaluation.

theorem DescriptiveComplexity.Draw.Data.step_compare_exit_pos {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {ltpAddr vp : 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) (hvp : WMIncr WMLe vp ltpAddr) (hyes : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), st.old i r ↔ st.new i r) : (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) 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) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeOutP fc), head := Sum.inl vp, 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 passing verdict: at the ltp cell with every address below agreed, step off it into the output's walk home.

theorem DescriptiveComplexity.Draw.Data.step_compare_exit_neg {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {ltpAddr vp : 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) (hvp : WMIncr WMLe vp ltpAddr) (hno : ¬∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), st.old i r ↔ st.new i r) : (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) 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) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeCmpP fc), head := Sum.inl vp, 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 failing verdict: at the ltp cell with some address below disagreed, step off it into the copy-back's walk home.

theorem DescriptiveComplexity.Draw.Data.step_homeCmp_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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} (hvi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : dt.CtlIx → 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.homeCmpP 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.copyP fc), head := Sum.inl v', 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 v')) st.mir) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

COPY's folded first step: homeCmp's exit rewrites the empty address's cell – every old track taking its new digit – and lands at its successor, in the copy-back's frontier presentation there.

theorem DescriptiveComplexity.Draw.Data.reaches_copyFrom {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → 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) {s₀ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hle : WMSetLe WMLe s₀ 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 s₀, 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 s₀)) 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 from an arbitrary start: the generalization of DescriptiveComplexity.Draw.Data.reaches_copy the folded first step needs.

theorem DescriptiveComplexity.Draw.Data.step_copy_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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 : dt.CtlIx → A} {st : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {ltpAddr vp : 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) (hvp : WMIncr WMLe vp ltpAddr) : (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 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) } { state := Sum.inr ((dt.prog zero one hzo args hpl).stElt OuterPh.homeCopyP fc), head := Sum.inl vp, 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 exit: at the ltp cell, step off it into its walk home.

theorem DescriptiveComplexity.Draw.Data.step_homeCopy_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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} (hvi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : dt.CtlIx → 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.homeCopyP 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.evalP (EvalPh.chk 0)) 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 copy-back's walk home exits into the next sweep: off the marker, rightwards, into the first checkpoint.

theorem DescriptiveComplexity.Draw.Data.step_homeOut_exit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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} (hvi : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v') {fc : dt.CtlIx → 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.homeOutP 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.evalP (EvalPh.sub dt.smEntryOut)) 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 output's walk home exits into the out machinery: off the marker, rightwards, into its entry checkpoint.

Closing a stage

After the sweep's last round the machine stands at the first checkpoint on the ltp cell. One more evaluation runs there (its writes are junk the copy never propagates and nothing reads), then the erasing .dspB exit, the reset, the mirror clear and the convergence sweep. Its verdict closes the stage: failing, the copy-back rewrites every old track and the walk home re-enters the evaluation – the next stage's entry; passing, the walk home enters the out machinery.

theorem DescriptiveComplexity.Draw.Data.stageClose_neg {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {ltpAddr : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hneT : ∃ (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), ltpAddr x) {st0 stT : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {fs0 fsT : dt.CtlIx → A} (hspineT : 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.evalP (EvalPh.chk 0)) fs0), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st0) st0.val) ((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.evalP (EvalPh.chk (Fin.last dt.nv))) fsT), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ stT) stT.val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkT : stT.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hltpT : stT.ltp = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hbotT : stT.bot = 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) (hno : ¬∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), stT.old i r ↔ stT.new i r) : 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.evalP (EvalPh.chk 0)) fs0), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st0) st0.val) ((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.evalP (EvalPh.chk 0)) fsT), 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.val (dt.back wmSeg zero one ⋯ (dt.copySt zero one hzo args (have __src := dt.atSt (dt.offSt stT) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) ltpAddr)) (dt.copySt zero one hzo args (have __src := dt.atSt (dt.offSt stT) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) ltpAddr).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

A failed stage closes into the next: from the first checkpoint on the ltp cell (the evaluation there a hypothesis) to the first checkpoint at the empty address, every old track below the top rewritten to its new digit.

theorem DescriptiveComplexity.Draw.Data.stageClose_pos {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {ltpAddr : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hneT : ∃ (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), ltpAddr x) {v₁ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hiE : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v₁) {st0 stT : TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {fs0 fsT : dt.CtlIx → A} (hspineT : 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.evalP (EvalPh.chk 0)) fs0), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st0) st0.val) ((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.evalP (EvalPh.chk (Fin.last dt.nv))) fsT), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ stT) stT.val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkT : stT.wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hltpT : stT.ltp = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hbotT : stT.bot = 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) (hyes : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), stT.old i r ↔ stT.new i r) : 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.evalP (EvalPh.chk 0)) fs0), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ st0) st0.val) ((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.evalP (EvalPh.sub dt.smEntryOut)) fsT), head := Sum.inl v₁, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (have __src := dt.atSt (dt.offSt stT) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (have __src := dt.atSt (dt.offSt stT) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

A passed stage closes into the output: the same ring up to the verdict, then the walk home and the dispatch into the out machinery's entry checkpoint.

MAIN

The loop: one sweep and one stage-closing ring per stage, iterated while the convergence sweep fails, and the passing ring at the first stage that stabilizes. Everything semantic – the per-stage tape and control families and the runs themselves – is a hypothesis family; the loop is a plain induction on the first converged index.

theorem DescriptiveComplexity.Draw.Data.reaches_main {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [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 (dt.CtlIx ⊕ 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) {ltpAddr : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hlt : WMSetLt WMLe ltpAddr (wmSeg gbot)) (hneT : ∃ (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd), ltpAddr x) {v₁ : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop} (hiE : WMIncr WMLe (fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False) v₁) {N : ℕ} {entrySt topSt stT : ℕ → TapeStD dt A (dt.RIx zero one hzo args) dt.PF} {entryFs topFs fsT : ℕ → dt.CtlIx → A} (hsweep : ∀ n ≤ N, 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.evalP (EvalPh.chk 0)) (entryFs n)), 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.val (dt.back wmSeg zero one ⋯ (entrySt n)) (entrySt n).val) ((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.evalP (EvalPh.chk 0)) (topFs n)), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (topSt n)) (topSt n).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hspineT : ∀ n ≤ N, 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.evalP (EvalPh.chk 0)) (topFs n)), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (topSt n)) (topSt n).val) ((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.evalP (EvalPh.chk (Fin.last dt.nv))) (fsT n)), head := Sum.inl ltpAddr, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (stT n)) (stT n).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }) (hwkT : ∀ n ≤ N, (stT n).wk = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hltpT : ∀ n ≤ N, (stT n).ltp = fun (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop) => r = ltpAddr) (hbotT : ∀ n ≤ N, (stT n).bot = 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) (hnotconv : ∀ n < N, ¬∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stT n).old i r ↔ (stT n).new i r) (hconv : ∀ (r : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd → Prop), WMSetLt WMLe r ltpAddr → ∀ (i : dt.d.B.ι), (stT N).old i r ↔ (stT N).new i r) (hnextSt : ∀ n < N, entrySt (n + 1) = dt.copySt zero one hzo args (have __src := dt.atSt (dt.offSt (stT n)) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) ltpAddr) (hnextFs : ∀ n < N, entryFs (n + 1) = fsT n) : 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.evalP (EvalPh.chk 0)) (entryFs 0)), 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.val (dt.back wmSeg zero one ⋯ (entrySt 0)) (entrySt 0).val) ((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.evalP (EvalPh.sub dt.smEntryOut)) (fsT N)), head := Sum.inl v₁, tape := wideTape ((dt.prog zero one hzo args hpl).trackTapeAt wmSeg Slot.val (dt.back wmSeg zero one ⋯ (have __src := dt.atSt (dt.offSt (stT N)) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (have __src := dt.atSt (dt.offSt (stT N)) fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False; { mir := fun (x : Univ A (dt.RIx zero one hzo args) dt.PF dt.KIx dt.dd) => False, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }).val) ((dt.prog zero one hzo args hpl).syElt (dt.prog zero one hzo args hpl).blank) }

The MAIN loop: from the first stage's entry at the empty address, through one sweep and one closing ring per stage, to the out machinery's entry checkpoint at the first stage whose convergence sweep passes.