The clocked evaluation at the file the channel hands over

A program that lays its file puts the registers at consecutive addresses, each one bit above the last. This file prices the clocked evaluation at the file the register channel hands over instead, where the registers are the cells the channel writes and a step of a walk across the file can cost as much as the whole file (DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_reachesIn).

The four widths are regW, regWP, regWR, regWK (DescriptiveComplexity.Draw.Data.regW and its neighbors), each bounded by one number, regWidthBound: three of the four are linear in the file's own bound, and the seek is quadratic, being a pass of the file per bit of its target.

One number above the register file's four widths

def DescriptiveComplexity.Draw.Data.regWidthBound (t B : ℕ) : ℕ

One number above all four widths of the handed file: the file's bound and the walk across it, squared, with room for the constants.

Equations

• DescriptiveComplexity.Draw.Data.regWidthBound t B = 16 * (B + t * B + 16) ^ 2

theorem DescriptiveComplexity.Draw.Data.regWidthBound_le_two_pow (N : ℕ) : regWidthBound N (2 ^ N) ≤ 2 ^ (4 * N + 14)

The width bound, as a power of two: at the file's own bound 2 ^ N and its N registers, the widths are below 2 ^ (4 N + 14). Every clock argument wants the widths as an exponent, and this is where the polynomial becomes one.

theorem DescriptiveComplexity.Draw.Data.regW_le {t B : ℕ} : 2 * B + 2 ≤ regWidthBound t B

theorem DescriptiveComplexity.Draw.Data.regWP_le {t B : ℕ} : 2 * B + t * B + 3 ≤ regWidthBound t B

theorem DescriptiveComplexity.Draw.Data.regWR_le {t B : ℕ} : B + 4 ≤ regWidthBound t B

theorem DescriptiveComplexity.Draw.Data.regWK_le {t B : ℕ} : B * (1 + (2 * B + 3 + t * B) + (2 * B + 5 + t * B)) + 1 + (2 * B + 3 + t * B) ≤ regWidthBound t B

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.regWidthBd {L : FirstOrder.Language} (dt : Data L) (A R' P' : Type) [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

The register file's widths, under one number: the bound every address of the file is under, and the number of registers.

Equations

• dt.regWidthBd A R' P' = DescriptiveComplexity.Draw.Data.regWidthBound (Nat.card dt.RegIx) dt.regBound

theorem DescriptiveComplexity.Draw.Data.regW_le_bound {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : dt.regW ≤ dt.regWidthBd A R' P'

theorem DescriptiveComplexity.Draw.Data.regWP_le_bound {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : dt.regWP ≤ dt.regWidthBd A R' P'

theorem DescriptiveComplexity.Draw.Data.regWR_le_bound {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : dt.regWR ≤ dt.regWidthBd A R' P'

theorem DescriptiveComplexity.Draw.Data.regWK_le_bound {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : dt.regWK ≤ dt.regWidthBd A R' P'

theorem DescriptiveComplexity.Draw.Data.ixWidthBd_regLaid {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {q : ℕ} (hq : 16 ≤ q) (hwidth : dt.regWidthBd A R' P' ≤ q) (hd0 : Nat.card (Lex (Fin dt.dd0 → A)) + 1 ≤ q) (heDim : Nat.card (Lex (Fin dt.eDim → A)) + 1 ≤ q) (hntg : dt.ntgDim ≤ q) (hnf : dt.nfDim ≤ q) (hnat : ∀ (vi : dt.VarIx), dt.natOf vi ≤ q) (hnIn : ∀ (vi : dt.VarIx), dt.nIn vi ≤ q) (harOf : ∀ (vi : dt.VarIx), dt.arOf vi ≤ q) (harity : ∀ (iv : dt.d.B.ι), dt.d.B.arity iv ≤ q) (hnv : dt.nv ≤ q) : dt.IxWidthBd A dt.regW dt.regWP dt.regWR dt.regWK q

The tower's costs at the handed file are polynomial in one number: the IxWidthBd of DescriptiveComplexity.Draw.Data.ixLegWidth_le, at the four widths the register channel's file is charged; what an instantiation owes of the clock is again q ^ 25 ≤ 2 ^ (k · m).

theorem DescriptiveComplexity.Draw.Data.regWidthBd_le_two_pow {L : FirstOrder.Language} (dt : Data L) (A R' P' : Type) [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : dt.regWidthBd A R' P' ≤ 2 ^ (4 * Nat.card dt.RegIx + 14)

The file's widths, under a power of two of its register count: the file bounds every address by 2 ^ N at N registers, and the widths are quadratic in that. This is the first of the two places the clock's exponent comes from – the other is the record's own dimensions.

theorem DescriptiveComplexity.Draw.Data.ixEvalWidth_le_regLaid {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {q : ℕ} (hq : 16 ≤ q) (hwidth : dt.regWidthBd A R' P' ≤ q) (hd0 : Nat.card (Lex (Fin dt.dd0 → A)) + 1 ≤ q) (heDim : Nat.card (Lex (Fin dt.eDim → A)) + 1 ≤ q) (hntg : dt.ntgDim ≤ q) (hnf : dt.nfDim ≤ q) (hnat : ∀ (vi : dt.VarIx), dt.natOf vi ≤ q) (hnIn : ∀ (vi : dt.VarIx), dt.nIn vi ≤ q) (harOf : ∀ (vi : dt.VarIx), dt.arOf vi ≤ q) (harity : ∀ (iv : dt.d.B.ι), dt.d.B.arity iv ≤ q) (hnv : dt.nv ≤ q) : dt.ixEvalWidth A dt.regW dt.regWP dt.regWR dt.regWK ≤ q ^ 26

The evaluation's width at the handed file is polynomial in one number: DescriptiveComplexity.Draw.Data.ixEvalWidth_le at ixWidthBd_regLaid. This is the a of the clock – what one round of the evaluation costs – and what an instantiation owes is q ^ 26 ≤ 2 ^ (k · m).

theorem DescriptiveComplexity.Draw.Data.ixEvalWidth_le_two_pow_regLaid {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {q : ℕ} (hq : 16 ≤ q) (hwidth : dt.regWidthBd A R' P' ≤ q) (hd0 : Nat.card (Lex (Fin dt.dd0 → A)) + 1 ≤ q) (heDim : Nat.card (Lex (Fin dt.eDim → A)) + 1 ≤ q) (hntg : dt.ntgDim ≤ q) (hnf : dt.nfDim ≤ q) (hnat : ∀ (vi : dt.VarIx), dt.natOf vi ≤ q) (hnIn : ∀ (vi : dt.VarIx), dt.nIn vi ≤ q) (harOf : ∀ (vi : dt.VarIx), dt.arOf vi ≤ q) (harity : ∀ (iv : dt.d.B.ι), dt.d.B.arity iv ≤ q) (hnv : dt.nv ≤ q) : dt.ixEvalWidth A dt.regW dt.regWP dt.regWR dt.regWK ≤ 2 ^ (26 * (Nat.log 2 q + 1))

The evaluation's width, as a power of two: ixEvalWidth_le_regLaid read against the clock, which compares with 2 ^ (k · m) and not with a polynomial. A number is below the next power of two above it (Nat.lt_pow_succ_log_self), so twenty-six of them are below its twenty-sixth, and that is the exponent w a reduction hands the clock.

noncomputable def DescriptiveComplexity.Draw.Data.dimC {L : FirstOrder.Language} (dt : Data L) : ℕ

The dimensions that do not depend on the instance: the tag and formula budgets, the number of variables, and the atom, gate, argument and arity counts. They are the kernel's own, so a clock's exponent carries them as an additive constant.

Equations

• dt.dimC = max dt.ntgDim (max dt.nfDim (max dt.nv (max (⨆ (vi : dt.VarIx), max (dt.natOf vi) (max (dt.nIn vi) (dt.arOf vi))) (⨆ (iv : dt.d.B.ι), dt.d.B.arity iv))))

noncomputable def DescriptiveComplexity.Draw.Data.evalQ {L : FirstOrder.Language} (dt : Data L) (A R' P' : Type) [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : ℕ

One number dominating every dimension the width bound compares against: the pass widths, the two tuple counts, and the kernel's own dimensions (dimC). It is a maximum and nothing else, so each of the ten comparisons ixEvalWidth_le_regLaid asks for is one le_max away.

Equations

• dt.evalQ A R' P' = max 16 (max (dt.regWidthBd A R' P') (max (Nat.card (Lex (Fin dt.dd0 → A)) + 1) (max (Nat.card (Lex (Fin dt.eDim → A)) + 1) dt.dimC)))

theorem DescriptiveComplexity.Draw.Data.ixEvalWidth_le_two_pow_evalQ {L : FirstOrder.Language} (dt : Data L) {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] : dt.ixEvalWidth A dt.regW dt.regWP dt.regWR dt.regWK ≤ 2 ^ (26 * (Nat.log 2 (dt.evalQ A R' P') + 1))

The evaluation's width at the handed file, with nothing to discharge: ixEvalWidth_le_two_pow_regLaid at evalQ, whose ten comparisons hold by construction. This is the w of the clock, and it mentions the record alone.

The two bridges at the handed file

DescriptiveComplexity.Draw.Data.passEnc_regLaid and gateEnc_regLaid discharge the gates' bridges at the file the channel hands over. The generic lemmas they come from ask only that the registers stand for distinct elements, that the layout order is linear, and that a register's block and tuple are its element's – all of which the handed file has.

theorem DescriptiveComplexity.Draw.Data.passEnc_regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [Nonempty A] [L.Structure A] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hzo : PR.zero ≠ PR.one) (vi : dt.VarIx) (stV : TapeSt dt A R' P' dt.RegIx) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP (regLaid h hord) PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr (fun (u : dt.RegIx) => ↑u) stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))

The inner gates' bridge at the handed file: hpassEnc, discharged.

theorem DescriptiveComplexity.Draw.Data.gateEnc_regLaid {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R'] [LinearOrder P'] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] [Nonempty A] [L.Structure A] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite (Univ A R' P' dt.KIx dt.dd)] {PR : Prog A R' P' dt.CtlIx dt.SlotIx dt.KIx dt.dd} (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' P' dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hzo : PR.zero ≠ PR.one) (j : Fin dt.nv) (st : TapeSt dt A R' P' dt.RegIx) : dt.ixGatedAt (regLaid h hord) j st ↔ ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr (fun (u : dt.RegIx) => ↑u) st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))

The gates' bridge at the handed file: hgateEnc, discharged.

The evaluation itself

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.NexRegIx {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : Type

The handed file's index at the clocked phases.

Equations

• dt.NexRegIx A R B = dt.RegIx

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.regElt {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (u : dt.NexRegIx A R B) : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd

The element a register stands for: itself.

Equations

• dt.regElt A R B u = ↑u

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegW {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegW A R B = dt.regW

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegWP {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegWP A R B = dt.regWP

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegWR {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegWR A R B = dt.regWR

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.nexRegWK {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : ℕ

The handed file's four widths, at the clocked phases.

Equations

• dt.nexRegWK A R B = dt.regWK

theorem DescriptiveComplexity.Draw.Data.regElt_injective {L : FirstOrder.Language} (dt : Data L) (A R B : Type) [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] : Function.Injective (dt.regElt A R B)

Distinct registers stand for distinct elements.

theorem DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (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 B (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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (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 B (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 B (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 B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => 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) (stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsOf : Fin (dt.nv + 1) → dt.CtlIx → A) (hwkOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark (dt.regElt A R B) v) (hbotOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semTJ : (j : Fin dt.nv) → dt.ixGatedAt (regLaid h hord) j (stOf j.castSucc) → (p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP (regLaid h hord) PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) v ↑b) (dt.regElt A R B) (dt.kindOf (dt.varAt j) b)) (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB (regLaid h hord) ⋯ ⋯ ⋯ mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) (hfs : ∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB (regLaid h hord) ⋯ ⋯ ⋯ mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (TestOf : Fin (dt.arOf none) → dt.NexRegIx A R B → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv))) (stOf (Fin.last dt.nv)).mir ((regLaid h hord).cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk (ixAddr (dt.regElt A R B) (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmirL : (stOf (Fin.last dt.nv)).mir = ixMark (dt.regElt A R B) v) (hbotL : (stOf (Fin.last dt.nv)).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : (stOf (Fin.last dt.nv)).sav = ixMark (dt.regElt A R B) v) (htgtL : (stOf (Fin.last dt.nv)).tgt = ixMark (dt.regElt A R B) v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP (regLaid h hord) PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) (dt.regElt A R B) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr (dt.regElt A R B) (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), TestOf ℓ u) (hacc : (dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))) : (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV)) { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.acceptP (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT))) (mV aT)) (PR.syElt PR.blank) }

The clocked evaluation at the handed file: the walk-back the opening's dispatch owes, the branched spine over the spine's positions, and the exit into the accepting phase, charged the handed file's own widths. This is DescriptiveComplexity.Draw.Data.nexIxEvalB_reachesIn with every coherence of the register channel's file discharged; what is left is the program's own, and what the reduction still owes is its marking – the arguments, one element below them, and nothing else.

theorem DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_any_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (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 B (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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (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 B (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 B (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 B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => 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) (stOf : Fin (dt.nv + 1) → TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsOf : Fin (dt.nv + 1) → dt.CtlIx → A) (hwkOf : ∀ (k : Fin (dt.nv + 1)), (stOf k).wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmirOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).mir = ixMark (dt.regElt A R B) v) (hbotOf : ∀ (j : Fin dt.nv), (stOf j.castSucc).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (semTJ : (j : Fin dt.nv) → dt.ixGatedAt (regLaid h hord) j (stOf j.castSucc) → (p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP (regLaid h hord) PR.zero PR.one (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt (stOf j.castSucc) p (mV a)) v ↑b) (dt.regElt A R B) (dt.kindOf (dt.varAt j) b)) (hst : ∀ (j : Fin dt.nv), stOf j.succ = dt.ixLegStB (regLaid h hord) ⋯ ⋯ ⋯ mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) (hfs : ∀ (j : Fin dt.nv), fsOf j.succ = dt.ixLegCtlB (regLaid h hord) ⋯ ⋯ ⋯ mV j (stOf j.castSucc) (semTJ j) (fsOf j.castSucc)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (TestOf : Fin (dt.arOf none) → dt.NexRegIx A R B → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (stOf (Fin.last dt.nv))) (stOf (Fin.last dt.nv)).mir ((regLaid h hord).cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk (ixAddr (dt.regElt A R B) (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmirL : (stOf (Fin.last dt.nv)).mir = ixMark (dt.regElt A R B) v) (hbotL : (stOf (Fin.last dt.nv)).bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : (stOf (Fin.last dt.nv)).sav = ixMark (dt.regElt A R B) v) (htgtL : (stOf (Fin.last dt.nv)).tgt = ixMark (dt.regElt A R B) v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP (regLaid h hord) PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV a)) (dt.regElt A R B) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr (dt.regElt A R B) (stOf (Fin.last dt.nv)).mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), TestOf ℓ u) : (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV)) { state := Sum.inr (PR.stElt (NexPh.evalP (EvalPh.chk 0)) (fsOf 0)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (stOf 0)) (stOf 0).val) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt NexPh.acceptP (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv)))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => if r = v then Function.update (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT)) v) (dt.varArgsOf PR.zero PR.one none).newSlot (bitVal PR.zero PR.one ((dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV (stOf (Fin.last dt.nv)) tOf semOf (fsOf (Fin.last dt.nv))))) else dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt (stOf (Fin.last dt.nv)) (mV aT)) r) (mV aT)) (PR.syElt PR.blank) }

The clocked evaluation at the handed file, whatever the verdict: nexIxEvalB_regLaid_reachesIn with the verdict not assumed (nexIxEvalOutB_any_reachesIn).

The thread, and the run from the sentence alone

noncomputable def DescriptiveComplexity.Draw.Data.regGatedSem {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (hzo : PR.zero ≠ PR.one) {ιV : Type} (mV : ιV → dt.NexRegIx A R B → Prop) (w : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) : dt.ixGatedAt (regLaid h hord) j st → (p : dt.IxScratch A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP (regLaid h hord) PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) w ↑b) (dt.regElt A R B) (dt.kindOf (dt.varAt j) b)

The packs at the handed file, built: the conditioned family the branched thread takes as a parameter, from the gates' bridge and the inner gates' (gateEnc_regLaid, passEnc_regLaid) rather than assumed.

Equations

• dt.regGatedSem h hord hzo mV w j st hg p a hp b = dt.ixGatedSem (DescriptiveComplexity.Draw.Data.regLaid h hord) ⋯ ⋯ hzo h mV j st hg p a hp b

theorem DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_thread_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hzo : PR.zero ≠ PR.one) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (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 B (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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (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 B (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 B (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 B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => 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 B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmir₀ : st₀.mir = ixMark (dt.regElt A R B) v) (hbot₀ : st₀.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (stL : TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsL : dt.CtlIx → A) (hstL : stL = dt.ixSpineStOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) (hfsL : fsL = dt.ixSpineFsOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (TestOf : Fin (dt.arOf none) → dt.NexRegIx A R B → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ stL) stL.mir ((regLaid h hord).cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk (ixAddr (dt.regElt A R B) stL.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmirL : stL.mir = ixMark (dt.regElt A R B) v) (hbotL : stL.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : stL.sav = ixMark (dt.regElt A R B) v) (htgtL : stL.tgt = ixMark (dt.regElt A R B) v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP (regLaid h hord) PR.zero PR.one none (dt.ixRoundSt stL (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt stL (mV a)) (dt.regElt A R B) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr (dt.regElt A R B) stL.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), TestOf ℓ u) (hacc : (dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV stL tOf semOf fsL)) : (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (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) } { state := Sum.inr (PR.stElt NexPh.acceptP (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV stL tOf semOf fsL)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt stL (mV aT))) (mV aT)) (PR.syElt PR.blank) }

The clocked evaluation at the handed file, with its thread: the same run as nexIxEvalB_regLaid_reachesIn with the tape and control families constructed – the branched thread at the packs the bridges build – so that a program has only to name the state it enters the evaluation in.

theorem DescriptiveComplexity.Draw.Data.nexIxEvalB_regLaid_thread_any_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hzo : PR.zero ≠ PR.one) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (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 B (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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (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 B (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 B (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 B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => 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 B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmir₀ : st₀.mir = ixMark (dt.regElt A R B) v) (hbot₀ : st₀.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (stL : TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsL : dt.CtlIx → A) (hstL : stL = dt.ixSpineStOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) (hfsL : fsL = dt.ixSpineFsOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (TestOf : Fin (dt.arOf none) → dt.NexRegIx A R B → Prop) (hcompatOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), dt.wellShapedG PR.zero PR.one (Sum.inl (Fin.castLE ⋯ ℓ)) (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ stL) stL.mir ((regLaid h hord).cell u)) ↔ TestOf ℓ u) (tOf : Fin (dt.arOf none) → dt.X.Tag) (hwitOf : ∀ (ℓ : Fin (dt.arOf none)) (t' : dt.X.Tag), wmBlk (ixAddr (dt.regElt A R B) stL.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) (encTagTup dt.ly PR.zero PR.one t') ↔ t' = tOf ℓ) (hmirL : stL.mir = ixMark (dt.regElt A R B) v) (hbotL : stL.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : stL.sav = ixMark (dt.regElt A R B) v) (htgtL : stL.tgt = ixMark (dt.regElt A R B) v) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP (regLaid h hord) PR.zero PR.one none (dt.ixRoundSt stL (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt stL (mV a)) (dt.regElt A R B) (dt.kindOf none b)) (hDom : ∀ (ℓ : Fin (dt.arOf none)), ExpExpansion.DomHolds (tOf ℓ, decRho dt.ly PR.zero PR.one (wmBlk (ixAddr (dt.regElt A R B) stL.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ))))))) (hTestOf : ∀ (ℓ : Fin (dt.arOf none)) (u : dt.NexRegIx A R B), TestOf ℓ u) : (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (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) } { state := Sum.inr (PR.stElt NexPh.acceptP (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV stL tOf semOf fsL)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt (regLaid h hord).cell Slot.val (fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => if r = v then Function.update (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt stL (mV aT)) v) (dt.varArgsOf PR.zero PR.one none).newSlot (bitVal PR.zero PR.one ((dt.varArgsOf PR.zero PR.one none).accBit (dt.ixOutCtl (regLaid h hord) ⋯ ⋯ ⋯ mV stL tOf semOf fsL))) else dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.ixRoundSt stL (mV aT)) r) (mV aT)) (PR.syElt PR.blank) }

The clocked evaluation at the handed file, with its thread, whatever the verdict: the same run as nexIxEvalB_regLaid_reachesIn with the tape and control families constructed – the branched thread at the packs the bridges build – so that a program has only to name the state it enters the evaluation in.

theorem DescriptiveComplexity.Draw.Data.nexIxEvalOut_regLaid_realize_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] [LinearOrder (dt.X.Map A)] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hzo : PR.zero ≠ PR.one) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (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 B (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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (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 B (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 B (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 B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => 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 B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmir₀ : st₀.mir = ixMark (dt.regElt A R B) v) (hbot₀ : st₀.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (stL : TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsL : dt.CtlIx → A) (hstL : stL = dt.ixSpineStOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) (hfsL : fsL = dt.ixSpineFsOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (hmirL : stL.mir = ixMark (dt.regElt A R B) v) (hbotL : stL.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : stL.sav = ixMark (dt.regElt A R B) v) (htgtL : stL.tgt = ixMark (dt.regElt A R B) v) {Use : dt.NexRegIx A R B → Prop} (hUse : ∀ (a : ιV) (u : dt.NexRegIx A R B), mV a u → Use u) (hmono : ∀ (u u' : dt.RegIx), WMLt (regLaid h hord).le u u' ↔ WMLt WMLe (dt.regElt A R B u) (dt.regElt A R B u')) (hup : ∀ (u : dt.NexRegIx A R B) (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), Use u → WMLt WMLe (dt.regElt A R B u) x → ∃ (u' : dt.NexRegIx A R B), Use u' ∧ dt.regElt A R B u' = x) (hKin : ∀ (a : ιV) (t : Tag R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), ixAddr (dt.regElt A R B) (mV a) (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (ixAddr (dt.regElt A R B) (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {Below : (Univ A R (NexPh B (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) → (stL.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 B) (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 B) 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) (hout : dt.X.Map A ⊨ dt.d.out) : ∃ (fq : dt.CtlIx → A) (cT : Config (WPoint (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))), (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (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

The clocked evaluation at the handed file, from the sentence alone: the run above with the output's leg discharged. The output variable is nullary, so everything its leg asks about argument blocks is vacuous – there are none – and the one thing left is its verdict, which ixOutAcc_iff_out reads as the expansion's output sentence at the stage the tracks hold. So what a program has to bring to its own evaluation is the entry state, the enumeration, the stage its guess wrote, and the sentence being true.

theorem DescriptiveComplexity.Draw.Data.nexIxEvalOut_regLaid_verdict_reachesIn {L : FirstOrder.Language} (dt : Data L) {A R B : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder (NexPh B (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite A] [Finite R] [Finite (NexPh B (EvalPh dt.nv dt.PMF))] [Finite (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} [Nonempty A] [L.IsRelational] [L.Structure A] [Finite dt.KIx] [LinearOrder (dt.X.Map A)] (h : IsLinOrd WMLe) {rEmb : (i : dt.SEF) → dt.NexSESh i → R} (hrules : ∀ (i : dt.SEF) (ρ : dt.NexSESh i), PR.rules (rEmb i ρ) = dt.nexEvalRuleF PR.zero PR.one (fun (w : dt.VarIx) => dt.varArgsOf PR.zero PR.one w) i ρ) (hR : PR.table.Reads) (hzo : PR.zero ≠ PR.one) (hord : ∀ (x y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {e₀ : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R (NexPh B (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 B (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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y → WMHasInp x → WMHasInp y) {bot : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp bot) (hleast : ∀ (y : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp y → WMLe bot y) (hbotarg : ∀ (i : dt.KIx), bot.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R B) (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 B (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 B (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 B → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R B) => 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 B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (f₀ : dt.CtlIx → A) (hwk₀ : st₀.wk = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = v) (hmir₀ : st₀.mir = ixMark (dt.regElt A R B) v) (hbot₀ : st₀.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (stL : TapeSt dt A R (NexPh B (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R B)) (fsL : dt.CtlIx → A) (hstL : stL = dt.ixSpineStOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) (hfsL : fsL = dt.ixSpineFsOfB (regLaid h hord) ⋯ ⋯ ⋯ mV st₀ f₀ (dt.regGatedSem h hord hzo mV) (Fin.last dt.nv)) {rEmbO : (i : dt.VarSiteF none) → dt.VarShF none i → R} (hrulesOut : ∀ (i : dt.VarSiteF none) (ρ : dt.VarShF none i), PR.rules (rEmbO i ρ) = dt.varRuleF PR.zero PR.one none (dt.varArgsOf PR.zero PR.one none) (fun (p : dt.VarPhF none) => NexPh.evalP (EvalPh.sub (Sum.inr p))) NexPh.acceptP i ρ) (hmirL : stL.mir = ixMark (dt.regElt A R B) v) (hbotL : stL.bot = fun (r : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : stL.sav = ixMark (dt.regElt A R B) v) (htgtL : stL.tgt = ixMark (dt.regElt A R B) v) {Use : dt.NexRegIx A R B → Prop} (hUse : ∀ (a : ιV) (u : dt.NexRegIx A R B), mV a u → Use u) (hmono : ∀ (u u' : dt.RegIx), WMLt (regLaid h hord).le u u' ↔ WMLt WMLe (dt.regElt A R B u) (dt.regElt A R B u')) (hup : ∀ (u : dt.NexRegIx A R B) (x : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), Use u → WMLt WMLe (dt.regElt A R B u) x → ∃ (u' : dt.NexRegIx A R B), Use u' ∧ dt.regElt A R B u' = x) (hKin : ∀ (a : ιV) (t : Tag R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), ixAddr (dt.regElt A R B) (mV a) (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (ixAddr (dt.regElt A R B) (mV aT)) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {Below : (Univ A R (NexPh B (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) → (stL.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 B) (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 B) 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 B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))), (wideData (Univ A R (NexPh B (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn (1 + (dt.ixLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (Nat.card ιV) + 2) * dt.nv + 1 + dt.ixOutLegCost A (dt.nexRegW A R B) (dt.nexRegWP A R B) (dt.nexRegWR A R B) (dt.nexRegWK A R B) (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 handed file, and the verdict it leaves: the run above with the sentence not assumed, and the accepting bit read as what it is – the sentence's own value (ixOutAcc_iff_out). A backward reading uses this: the run exists whatever the verdict, and the bit says which.