The evaluation with its verdict read, and the two exits

The forward run of a clocked program at the file the register channel hands it assumes the sentence and runs into the accepting phase. A backward reading cannot assume it – the verdict is what it is trying to determine – so this file carries the evaluation in the other form: the run exists whatever the stage says, and the accepting bit it leaves is the sentence's value (nexProgHanded_reachesIn_eval_verdict).

The two exits of the walks home come with it (exitG_at_marker): they are facts about where the marker is, and nothing about what the machine has written, so both directions of the correctness supply them the same way.

The two exits, at the marker

theorem DescriptiveComplexity.Draw.Data.exitG_at_marker {L' : FirstOrder.Language} {dt' : Data L'} {A' R'' P'' I' : Type} [Fintype dt'.SlotIx] {PR' : Prog A' R'' P'' dt'.CtlIx dt'.SlotIx dt'.KIx dt'.dd} {lay : Layout dt' A' R'' P'' I'} {st : TapeSt dt' A' R'' P'' I'} {v : Univ A' R'' P'' dt'.KIx dt'.dd → Prop} (hwk : st.wk v) (hnc : ∀ (u : I'), v ≠ lay.cell u) : dt'.exitG PR'.one (PR'.passTracksAt lay.cell Slot.mir (dt'.ixBack lay PR'.zero PR'.one ⋯ st) (fun (x : I') => False) v)

The exit condition holds at the marker: the head is on the address the wk track marks, and that address is nobody's register. Both are what the entry state says, so the two exits an opening asks for are facts about where the marker is, not about what the machine has written.

The evaluation, at the handed program

theorem DescriptiveComplexity.Draw.Data.nexProgHanded_reachesIn_eval_verdict {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [LinearOrder A] [Nonempty A] [Finite A] [Finite dt.KIx] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [Finite (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {R' : Type} [LinearOrder R'] [Finite R'] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} {bot : Option dt.KIx} (hE : NexEmitted PR bot) (h : IsLinOrd WMLe) (hR : PR.table.Reads) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y) (harg : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup PR.zero c)) (hargall : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (i : dt.KIx), x.1 = Tag.arg i) → WMHasInp x) (hupinp : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {botE : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp botE) (hleast : ∀ (y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe botE y) (hbotarg : ∀ (i : dt.KIx), botE.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R' (Option dt.KIx)) (htopF : ∀ (u : dt.RegIx), (regLaid h hord).le u gtop) (hbotF : ∀ (u : dt.RegIx), (regLaid h hord).le gbot u) {v v' : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v ((regLaid h hord).cell gbot)) (hvlog : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), v x → ∃ (i : dt.KIx), x.1 = Tag.arg i) (hvi : WMIncr WMLe v v') {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → dt.NexRegIx A R' (Option dt.KIx) → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R' (Option dt.KIx)) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr (regLaid h hord).le (mV a) (mV a')) (hTestT : ∀ (u : dt.RegIx), dt.InnerFull (regLaid h hord).blk (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : dt.RegIx), ¬dt.InnerFull (regLaid h hord).blk (mV a) u) (st₀ : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R' (Option dt.KIx))) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmir₀ : st₀.mir = ixMark (dt.regElt A R' (Option dt.KIx)) v) (hbot₀ : st₀.bot = fun (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (stL : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R' (Option dt.KIx))) (fsL : dt.CtlIx → A) (hstL : stL = dt.ixSpineStOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (regGatedSemP PR h hord mV) (Fin.last dt.nv)) (hfsL : fsL = dt.ixSpineFsOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (regGatedSemP PR h hord mV) (Fin.last dt.nv)) (hmirL : stL.mir = ixMark (dt.regElt A R' (Option dt.KIx)) v) (hbotL : stL.bot = fun (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : stL.sav = ixMark (dt.regElt A R' (Option dt.KIx)) v) (htgtL : stL.tgt = ixMark (dt.regElt A R' (Option dt.KIx)) v) {Use : dt.NexRegIx A R' (Option dt.KIx) → Prop} (hUse : ∀ (a : ιV) (u : dt.NexRegIx A R' (Option dt.KIx)), mV a u → Use u) (hmono : ∀ (u u' : dt.RegIx), WMLt (regLaid h hord).le u u' ↔ WMLt WMLe (dt.regElt A R' (Option dt.KIx) u) (dt.regElt A R' (Option dt.KIx) u')) (hup : ∀ (u : dt.NexRegIx A R' (Option dt.KIx)) (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), Use u → WMLt WMLe (dt.regElt A R' (Option dt.KIx) u) x → ∃ (u' : dt.NexRegIx A R' (Option dt.KIx)), Use u' ∧ dt.regElt A R' (Option dt.KIx) u' = x) (hKin : ∀ (a : ιV) (t : Tag R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), ixAddr (dt.regElt A R' (Option dt.KIx)) (mV a) (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (ixAddr (dt.regElt A R' (Option dt.KIx)) (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {Below : (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A), Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → (st₀.old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf none)), Below (ixAddr (dt.regElt A R' (Option dt.KIx)) (dt.ixStageTgt (regLaid h hord) ⋯ none ts (have __src := dt.ixRoundSt stL (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark (dt.regElt A R' (Option dt.KIx)) v, val := __src.val, old := __src.old, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (dt.d.B.arity iv)))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) : ∃ (fq : dt.CtlIx → A) (cT : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))), (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R' (Option dt.KIx)) (dt.nexRegWP A R' (Option dt.KIx)) (dt.nexRegWR A R' (Option dt.KIx)) (dt.nexRegWK A R' (Option dt.KIx)) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R' (Option dt.KIx)) (dt.nexRegWP A R' (Option dt.KIx)) (dt.nexRegWR A R' (Option dt.KIx)) (dt.nexRegWK A R' (Option dt.KIx)) (Nat.card ιV)) { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) f₀), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ st₀) st₀.val) (PR.syElt PR.blank) } cT ∧ cT.state = Sum.inr (PR.stElt NexPh.acceptP fq) ∧ ((dt.varArgsOf PR.zero PR.one none).accBit fq ↔ dt.X.Map A ⊨ dt.d.out)

The clocked evaluation, at the program, with the verdict read rather than assumed: the clocked evaluation without the sentence as a hypothesis, the accepting bit coming back as the sentence's own value. This is the form a backward reading needs – the run exists whatever the verdict, and the bit says which.