Where a backward reading of an accepting run starts

A run that accepts ends in NexPh.acceptP, which is one of the phases the program can never leave (NexPh.PostGuess). So somewhere along the run there is a first configuration in a post-guess phase, and this file finds it and recognizes its tape.

Two facts do it. The phases before it are all the outer layer's, so the rules fired up to that point keep the file, keep the addressed tracks and write bits (nexRule_keepsFile_of_ne_eval and its two siblings) – which is exactly what DescriptiveComplexity.Draw.Data.ShapedAt propagates along a run. And an accepting configuration is in a post-guess phase, so the search has something to find.

What comes out is a configuration whose tape is an ixBack of some tape state and whose phase is post-guess: the point where the machine's nondeterminism is spent, the guess is written on the tape, and the rest of the run is the evaluation's – deterministic, and read forward.

The first time a property holds

The run from the entry, forward again

The tape state the entry carries

theorem DescriptiveComplexity.Draw.Data.exists_entry_state {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] [Finite dt.KIx] [Nonempty A] [Nonempty dt.KIx] [L.IsRelational] [L.Structure 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)] {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) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (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) {v₀ : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hvreg : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x → v₀ ≠ wmRegSeg x) (g : ℕ → Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))) (hhead : ∀ (i : ℕ), ∃ (v : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), (g i).head = Sum.inl v) (hhead0 : (g 0).head = Sum.inl v₀) (hstate0 : (g 0).state = Sum.inr (PR.stElt NexPh.start fun (x : dt.CtlIx) => PR.zero)) (h0 : (g 0).tape = wideTape (PR.trackTapeAt (regLaid hlin hord).cell Slot.mir PR.initBackReg fun (x : dt.RegIx) => False) (PR.syElt PR.blank)) (n : ℕ) (hstep : ∀ i < n, (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step (g i) (g (i + 1))) (hacc : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Acc (g n).state) : ∃ m ≤ n, ∃ (st : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.RegIx), (g m).tape = wideTape (PR.trackTapeAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ st) fun (x : dt.RegIx) => False) (PR.syElt PR.blank) ∧ (st.wk = fun (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v₀) ∧ (st.mir = fun (x : dt.RegIx) => False) ∧ (st.tgt = fun (x : dt.RegIx) => False) ∧ (st.sav = fun (x : dt.RegIx) => False) ∧ (st.val = fun (x : dt.RegIx) => False) ∧ (st.bot = fun (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v₀) ∧ (∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), (g m).state = Sum.inr (stateElt PR.zero p f) → p.PostGuess) ∧ ∃ (fm : dt.CtlIx → A), (g m).state = Sum.inr (PR.stElt NexPh.homeGuessP fm)

The entry's tape, read as a tape state. The channel's tape is recognizable (tapeShape_initBackReg), the reading survives to the first post-guess time (exists_postGuess_shaped) and there the tape is an ixBack (exists_ixBack_of_shape) whose mirror, target, saved mirror and valuation are empty. The marker is the one write of the opening the reading has to read: the start step sets it at the cell the head began on and no later rule touches it (track_set_of_seq, nexProgHanded_setsSlot_wk, nexProgHanded_keepsSlot_wk), so the state's working track marks that cell alone.

That is every hypothesis the evaluation's entry state is asked for except the stage tracks, which are the guess's and are read off the same ixBack.

No acceptance, from a false verdict at the entry