The handed program, with room on its clock

DescriptiveComplexity.Draw.Data.nexProgHanded is the program a reduction into DescriptiveComplexity.WideRegAccept emits, and its clock is 2 ^ |Tag| at its own rule names. The clock's one remaining obligation (clock_count_of_tags) is that those names outnumber a constant of the kernel – and a program may always have more of them, since a rule whose guard is False changes nothing (PadRules.lean).

This file is that program: the same rules at the same sites, plus n sites carrying a rule that never fires. Its record, its channel, its marks and its phases are the originals – only the rule names are wider – so every constant the clock is measured against is unchanged and the count goes up by n.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexRIxPad {L : FirstOrder.Language} (dt : Data L) (G : Type) (n : ℕ) : Type

The rule names of the padded program: the clocked program's sites, and n more carrying a rule that never fires.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexITagPad {L : FirstOrder.Language} (dt : Data L) (G : Type) (n : ℕ) : Type

The tags of the padded machine's universe: the padded rule names, the alphabet's, the phases and the argument blocks.

Equations

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

theorem DescriptiveComplexity.Draw.Data.card_nexRIxPad {L : FirstOrder.Language} (dt : Data L) {G : Type} [Finite G] [Finite dt.KIx] [Finite dt.SEF] [∀ (e : dt.SEF), Finite (dt.NexSESh e)] (n : ℕ) : Nat.card (dt.NexRIxPad G n) = Nat.card dt.NexRIx + n

What the padding buys, at this program's rule names: one name per junk site, and nothing else moves.

noncomputable def DescriptiveComplexity.Draw.Data.nexProgHandedPad {L : FirstOrder.Language} (dt : Data L) {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] (zero one : A) [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad G n)] : Prog A (dt.NexRIxPad G n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd

The handed program with n junk rule names: the same program, its rule names padded.

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.Draw.Data.nexProgHandedPadAt {L : FirstOrder.Language} (dt : Data L) {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [L.IsRelational] [L.Structure A] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] : Prog A (dt.NexRIxPad (dt.d.B.ι → Bool) n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd

The padded program a clocked reduction emits: nexProgHanded with n junk rule names.

Equations

• dt.nexProgHandedPadAt hzo hpl bot n = dt.nexProgHandedPad zero one hzo hpl (dt.regionSpec zero one) (fun (w : dt.VarIx) => dt.varArgsOf zero one w) bot n

The interpretation, and that it reads the padded table

theorem DescriptiveComplexity.Draw.Data.nexProgHandedPad_eq_progFrom {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (e : Env L) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (γ : GuessSpec e.α dt.CtlIx dt.SlotIx (Option dt.KIx) (dt.d.B.ι → Bool)) (arg : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] : dt.nexProgHandedPad e.zero e.one ⋯ hpl γ arg bot n = progFrom hpl e (padRulesAt (NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh) (fun (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i) => dt.nexRule e.one (dt.nullSpec (Option dt.KIx)) γ (dt.nexEvalRuleF e.zero e.one arg) (EvalPh.chk 0) bot i ρ) NexPh.approachP n) NexPh.start (fun (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → e.α) => p = NexPh.acceptP ∧ (arg none).accBit f) (regFileMarkArg hpl)

The padded program is the definability layer's, at the padded rules.

noncomputable def DescriptiveComplexity.Draw.Data.nexInterpHandedPad {L : FirstOrder.Language} (dt : Data L) [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) (bot : Option dt.KIx) (n : ℕ) [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.wide (dt.ITagOf (NexSite dt.SEF ⊕ Fin n) (padSh (NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh) n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))) dt.dd

The padded machine, written down: the interpretation whose universe is tagged by the padded rule names – the clock's budget, widened by the junk sites and by nothing else.

Equations

• dt.nexInterpHandedPad hpl h bot n = DescriptiveComplexity.Draw.Data.drawInterp hpl ⋯ ⋯ DescriptiveComplexity.Draw.NexPh.start (DescriptiveComplexity.Draw.Data.regFileMarkArg hpl)

theorem DescriptiveComplexity.Draw.Data.reads_nexProgHandedPad {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) (bot : Option dt.KIx) (n : ℕ) (e : Env L) [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] [ws : FirstOrder.Language.wide.Structure (Univ e.α (dt.NexRIxPad (dt.d.B.ι → Bool) n) (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (hws : ws = (dt.nexInterpHandedPad hpl h bot n).mapStructure e.α) : (dt.nexProgHandedPad e.zero e.one ⋯ hpl (dt.regionSpec e.zero e.one) (args e) bot n).table.Reads

The interpreted structure reads the padded program's table: the same statement as at the unpadded program, at the wider rule names.

The padded program separates just as the program does

theorem DescriptiveComplexity.Draw.Data.nexProgHandedPad_sepOn {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {zero one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {args : (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} {n : ℕ} [LinearOrder (dt.NexRIxPad G n)] [LinearOrder dt.NexRIx] : (dt.nexProgHandedPad zero one hzo hpl γ args bot n).table.SepOn NexPh.PostGuess

The padded program separates after its guess: at the old rule names this is nexProgHanded_sep_rules, and a junk name fires on nothing.

theorem DescriptiveComplexity.Draw.Data.nexProgHandedPad_srcPh_ne_acceptP {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {zero one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {args : (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} {n : ℕ} [LinearOrder (dt.NexRIxPad G n)] [LinearOrder dt.NexRIx] (r : dt.NexRIxPad G n) : (dt.nexProgHandedPad zero one hzo hpl γ args bot n).table.srcPh r ≠ NexPh.acceptP

No rule of the padded program fires from its accepting phase: at an old name that is nexProgHanded_srcPh_ne_acceptP, and a junk rule fires from the start phase.

The marking's consequences, at any program with that channel

What a backward reading needs of the rules

def DescriptiveComplexity.Draw.Data.NexCovered {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] (PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd) {G : Type} (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : Prop

The rules a program of this shape has: at every rule name, either the rule of a site of the clocked program, or a rule that never fires. That is all a backward reading asks – it meets a rule by the name a step carries, not by the site it was written at – and both the emitted program and the padded one answer it, the second by its junk names.

Equations

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

theorem DescriptiveComplexity.Draw.Data.nexCovered_nexProgHandedPad {L : FirstOrder.Language} {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {zero : A} {G : Type} {one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {n : ℕ} [LinearOrder (dt.NexRIxPad G n)] (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : NexCovered (dt.nexProgHandedPad zero one hzo hpl γ args bot n) γ args bot

And so is the padded one, its junk names carrying a rule that never fires.

theorem DescriptiveComplexity.Draw.Data.regFacts_of_marked {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] [LinearOrder R'] [Finite R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [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} {zero : A} (hR : PR.table.Reads) (hmk : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) : (∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup zero c)) ∧ (∀ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (i : dt.KIx), z.1 = Tag.arg i) → WMHasInp z) ∧ (∀ (z w : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe z w → WMHasInp z → WMHasInp w) ∧ ∃ (botE : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp botE ∧ (∀ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp z → WMLe botE z) ∧ ∀ (i : dt.KIx), botE.1 ≠ Tag.arg i

What the marking, the order and the marker give the run, at any program whose channel writes for the argument elements and the one below them: the seven facts the join asks about the channel and the file's ends. This is This is the marking's seven consequences with the program abstracted, so that a padded program gets them by the same statement.

What a reduction's program provides, in one record

structure DescriptiveComplexity.Draw.Data.NexEmitted {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (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) : Type

The facts a clocked program of this shape provides, collected: its rules at the named sites, its channel's marks, its constants, its accepting predicate and the separation its determinism is read off. Every layer of the run takes this one hypothesis, and the two programs a reduction may emit – the plain one and the padded one that buys the clock its room – provide it the same way, by rfl at each field.

• site (i : NexSite dt.SEF) : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i → R'

  The rule name of a site and a shape.

• rules_site (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i) : PR.rules (self.site i ρ) = dt.nexRule PR.one (dt.nullSpec (Option dt.KIx)) (dt.regionSpec PR.zero PR.one) (dt.nexEvalRuleF PR.zero PR.one fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) (EvalPh.chk 0) bot i ρ

  And the rule it names is the clocked one.

• homeBuild : HomeKit.HomeRule → R'

  The rule name of a step of the walk home after the file is laid.

• rules_homeBuild (ρ : HomeKit.HomeRule) : PR.rules (self.homeBuild ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeBuildP }.rule PR.one ρ

  And it names that step.

• homeGuess : HomeKit.HomeRule → R'

  The rule name of a step of the walk home after the guess.

• rules_homeGuess (ρ : HomeKit.HomeRule) : PR.rules (self.homeGuess ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeGuessP }.rule PR.one ρ

  And it names that step.

• covered : NexCovered PR (dt.regionSpec PR.zero PR.one) (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) bot

  Every rule name carries a site's rule or one that never fires.

• mark (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) : PR.mark x = regSlotMark PR.zero PR.one ⋯ x

  The mark the channel writes.

• marked (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) : PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x

  And who it writes for: the argument elements and the one below them.

• blank (s : dt.SlotIx) : PR.blank s = PR.zero

  The tape is blank where the channel wrote nothing.

• startPh : PR.startPh = NexPh.start

  The machine starts in the start phase …

• startSt : PR.startSt = fun (x : dt.CtlIx) => PR.zero

  … with its control clear.

• accept_iff (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → A) : PR.accept p f ↔ p = NexPh.acceptP ∧ (dt.varArgsOf PR.zero PR.one none).accBit f

  It accepts in the accepting phase, at the output variable's bit.

• sepOn : PR.table.SepOn NexPh.PostGuess

  Two rules firing on the same data after the guess are the same rule.

• dstPh_postGuess (r : R') : (PR.table.srcPh r).PostGuess → (PR.table.dstPh r).PostGuess

  The post-guess phases are closed.

• srcPh_ne_acceptP (r : R') : PR.table.srcPh r ≠ NexPh.acceptP

  And no rule fires from the accepting phase.

theorem DescriptiveComplexity.Draw.Data.NexEmitted.uniqueFrom {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [Finite dt.KIx] [LinearOrder R'] [Finite R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [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) (cfg : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))) (hcfg : ∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), cfg.state = Sum.inr (stateElt PR.zero p f) → p.PostGuess) : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).UniqueFrom cfg

The machine is deterministic after its guess, at any program of this shape: separation there, and the post-guess phases closed.

theorem DescriptiveComplexity.Draw.Data.NexEmitted.acceptPh {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {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) (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → A) (h : PR.accept p f) : p = NexPh.acceptP

An accepting control is in the accepting phase.

def DescriptiveComplexity.Draw.Data.nexEmitted_nexProgHandedPad {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] {zero one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {n : ℕ} [LinearOrder (dt.NexRIxPad (dt.d.B.ι → Bool) n)] [LinearOrder dt.NexRIx] (bot : Option dt.KIx) : NexEmitted (dt.nexProgHandedPad zero one hzo hpl (dt.regionSpec zero one) (fun (w : dt.VarIx) => dt.varArgsOf zero one w) bot n) bot

And so does the padded one, its junk names never firing.

Equations

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

Determinism after the guess, at any program of this shape

theorem DescriptiveComplexity.Draw.Data.stuck_acceptP_of {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [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} (hR : PR.table.Reads) (hne : ∀ (r : R'), PR.table.srcPh r ≠ NexPh.acceptP) {x : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))} {f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A} (hx : x.state = Sum.inr (stateElt PR.zero NexPh.acceptP f)) (y : 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)).Step x y

The accepting phase is stuck, at any program no rule fires from it.

theorem DescriptiveComplexity.Draw.Data.stuck_of_acc_of {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [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} (hR : PR.table.Reads) (hne : ∀ (r : R'), PR.table.srcPh r ≠ NexPh.acceptP) (haccPh : ∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → A), PR.accept p f → p = NexPh.acceptP) (e : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))) (hacc : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Acc e.state) (e' : 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)).Step e e'

An accepting configuration is stuck: it is in the accepting phase, and no rule fires from there.

theorem DescriptiveComplexity.Draw.Data.not_acc_of_verdict_false_of {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [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} (hR : PR.table.Reads) (huniq : ∀ (cfg : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))), (∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), cfg.state = Sum.inr (stateElt PR.zero p f) → p.PostGuess) → (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).UniqueFrom cfg) (hne : ∀ (r : R'), PR.table.srcPh r ≠ NexPh.acceptP) (haccPh : ∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : dt.CtlIx → A), PR.accept p f → p = NexPh.acceptP) {entry cT c : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))} (hentry : ∀ (p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (f : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → A), entry.state = Sum.inr (stateElt PR.zero p f) → p.PostGuess) (hrun : Relation.ReflTransGen (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step entry cT) {fq : dt.CtlIx → A} (hstate : cT.state = Sum.inr (PR.stElt NexPh.acceptP fq)) (hbit : ¬PR.accept NexPh.acceptP fq) (hreach : Relation.ReflTransGen (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Step entry c) (hacc : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).Acc c.state) : False

A configuration whose verdict is false accepts nothing below it, at any program that is deterministic after the guess: the run into the accepting phase with the bit clear is a dead end that does not accept, and there is only one run. What it reads of it is uniqueness after the guess and the accepting phase's two facts.

The opening, at any program with those rules

theorem DescriptiveComplexity.Draw.Data.reachesIn_openingReg {L : FirstOrder.Language} [L.IsRelational] {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] [Nonempty dt.KIx] [Finite dt.KIx] [LinearOrder R'] [Finite R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [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} (_hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {bot : Option dt.KIx} {rEmbS : (i : NexSite dt.SEF) → NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i → R'} (hrulesS : ∀ (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) (dt.d.B.ι → Bool) dt.NexSESh i), PR.rules (rEmbS i ρ) = dt.nexRule PR.one (dt.nullSpec (Option dt.KIx)) (dt.regionSpec PR.zero PR.one) (dt.nexEvalRuleF PR.zero PR.one fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) (EvalPh.chk 0) bot i ρ) {rHomeB rHomeG : HomeKit.HomeRule → R'} (hrulesHB : ∀ (ρ : HomeKit.HomeRule), PR.rules (rHomeB ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeBuildP }.rule PR.one ρ) (hrulesHG : ∀ (ρ : HomeKit.HomeRule), PR.rules (rHomeG ρ) = { t := Slot.mir, wk := Slot.wk, ph := NexPh.homeGuessP }.rule PR.one ρ) (hmark : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), PR.mark x = regSlotMark PR.zero PR.one ⋯ x) (hmk : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), PR.marked x ↔ (∃ (k : dt.KIx), x.1 = Tag.arg k) ∨ IsTopNonArg x) (hblank : ∀ (s : dt.SlotIx), PR.blank s = PR.zero) (hstartPh : PR.startPh = NexPh.start) (hstartSt : PR.startSt = fun (x : dt.CtlIx) => PR.zero) (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 v₁ x y y' s₀ s₁ v' : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hvreg : ∀ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (k : dt.KIx), z.1 = Tag.arg k) ∨ IsTopNonArg z → v ≠ wmRegSeg z) (hvi₁ : WMIncr WMLe v v₁) (hwalk : WMSetLe WMLe v₁ x) (hxy : WMIncr WMLe x y) (hyy' : WMIncr WMLe y y') (hyv : WMSetLe WMLe v y) (hvs₀ : WMIncr WMLe v s₀) (hle : WMSetLe WMLe s₀ s₁) (hne₁ : ∃ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), s₁ z) (hvv' : WMIncr WMLe v v') (hexB : dt.exitG PR.one (PR.passTracksAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (dt.nexEntrySt v)) (fun (x : dt.RegIx) => False) v)) (σ : dt.d.B.ι → (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) → Prop) (hout : ∀ (i : dt.d.B.ι) (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop), WMSetLt WMLe r s₀ ∨ ¬WMSetLt WMLe r s₁ → ¬σ i r) (hexG : dt.exitG PR.one (PR.passTracksAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (have __src := dt.nexEntrySt v; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := σ, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (fun (x : dt.RegIx) => False) v)) : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (wideRank x - wideRank v₁ + (wideRank y - wideRank v) + (wideRank s₁ - wideRank s₀ + (wideRank s₁ - wideRank v)) + 7) { state := Sum.inr (PR.stElt PR.startPh PR.startSt), head := Sum.inl v, tape := wideTape (PR.trackTapeAt (regLaid hlin hord).cell Slot.mir PR.initBackReg fun (x : dt.RegIx) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) fun (x : dt.CtlIx) => PR.zero), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid hlin hord).cell Slot.mir (dt.ixBack (regLaid hlin hord).toLayout PR.zero PR.one ⋯ (have __src := dt.nexEntrySt v; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := σ, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) fun (x : dt.RegIx) => False) (PR.syElt PR.blank) }