The transition table, and the two promises it has to keep

The instance a hardness reduction into DescriptiveComplexity.DWideAcceptSpace emits is a wide machine, and a wide machine is eleven relations on a finite type (DescriptiveComplexity.Problems.Wide.Instance reads the smallest one). This file says what those eleven relations are, once and for all, in terms of a table: the program's rules, each with its guard, its two phases, the symbol it reads and the one it writes, and the direction it moves in.

What a rule is, and why it lives in the tag

DescriptiveComplexity.Draw.Table is indexed by two arbitrary types – R, the rules, and P, the phases – which are the two halves of DescriptiveComplexity.Draw.Tag. A transition is therefore an element (ctrl r, pad w): its rule is its tag and its tuple carries only the rule's data, the elements the rule acts at. That is the library's “index rules by attribute values, not by the transition” read at the level of the layout, and it is what will make every defining formula of the interpretation a decision taken when the formula is built – the source phase, the destination phase and the direction of a rule are functions of its tag alone.

Semantics first

Nothing here is a formula. The eleven relations are plain predicates on the tagged-tuple universe, and the instance is only assumed to read them (DescriptiveComplexity.Draw.Table.Reads); the interpretation that makes the assumption true is written later, and the equivalence is definitional, the interpreted universe being the tagged tuples themselves. Everything a program proves is therefore proved once, about any structure reading the table.

What the file delivers

for	theorem
a rule fires, moving right	DescriptiveComplexity.Draw.Table.fire_right
a rule fires, moving left	DescriptiveComplexity.Draw.Table.fire_left
the promise of WideAcceptSpace	DescriptiveComplexity.Draw.Table.wellFormed
the promise DWideAcceptSpace adds	DescriptiveComplexity.Draw.Table.deterministic

The two promises cost exactly what the layout was designed to make them cost. Well-formedness is the order being linear – it is DescriptiveComplexity.tagTupleLe, so DescriptiveComplexity.Wide.isLinOrd_tagTupleLe settles it – plus the input and the blank being functional, which they are because both are written as equations. Determinism is one condition on the table, DescriptiveComplexity.Draw.Table.Sep: two guarded rules agreeing on the state they apply in and the symbol they read are the same rule with the same data. The padding of DescriptiveComplexity.Draw.pad is what makes that a condition about payloads rather than about tuples, which is the whole reason it is there.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Univ (A R P K : Type) (dd : ℕ) : Type

The universe the reduction emits: tagged tuples, one block per tag. An abbrev, so that it is literally the interpreted universe and a pair may be destructured without ceremony.

Equations

• DescriptiveComplexity.Draw.Univ A R P K dd = (DescriptiveComplexity.Draw.Tag R P K × (Fin dd → A))

structure DescriptiveComplexity.Draw.Table (A R P K : Type) (c dd : ℕ) : Type

The transition table of the emitted machine. The reduction chooses the two designated elements of the alphabet, the payload width, and – rule by rule – a guard, the two phases, the two payloads of the state, the two payloads of the symbol, and the direction.

The three remaining fields are the machine's constants: its start state, its accepting states, its blank, and the symbol the input channel writes in the cell of each element (the register file of DescriptiveComplexity.Problems.Wide.Marks).

• zero : A

  The designated element a track holds when its bit is clear.

• one : A

  The designated element a track holds when its bit is set.

• zero_ne_one : self.zero ≠ self.one

  The two designated elements differ: what a track is read back by.

• payload_le : c ≤ dd

  The payload fits in the tuples of the universe.

• guard : R → (Fin c → A) → Prop

  Which data make the rule a transition.

• srcPh : R → P

  The phase a rule applies in.

• dstPh : R → P

  The phase a rule moves to.

• srcPl : R → (Fin c → A) → Fin c → A

  The pointer of the state a rule applies in.

• dstPl : R → (Fin c → A) → Fin c → A

  The pointer of the state a rule moves to.

• readPl : R → (Fin c → A) → Fin c → A

  The tracks of the symbol a rule reads.

• writePl : R → (Fin c → A) → Fin c → A

  The tracks of the symbol a rule writes.

• moveRight : R → Prop

  Whether a rule moves the head right.

• startPh : P

  The phase of the start state.

• startPl : Fin c → A

  The pointer of the start state.

• accept : P → (Fin c → A) → Prop

  Which states accept.

• blankPl : Fin c → A

  The tracks of the blank.

• markPl : Univ A R P K dd → Fin c → A

  The tracks of the symbol the input channel writes in the cell of an element.

• Marked : Univ A R P K dd → Prop

  Which elements the channel writes for. Every one of them by default, which is what DescriptiveComplexity.WideAccept's channel does; a program emitted into the register channel of DescriptiveComplexity.WideRegAccept restricts it, and the elements it leaves out have no register in the file the channel hands over.

The eleven relations, as predicates

def DescriptiveComplexity.Draw.Table.IsTr {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Prop

Being a transition: a ctrl-tagged element, canonically padded, whose data the rule of its tag admits. The padding is what gives a transition one spelling, and so the machine its determinism.

Equations

• T.IsTr τ = match τ.1 with | DescriptiveComplexity.Draw.Tag.ctrl r => DescriptiveComplexity.Draw.IsPad c T.zero τ.2 ∧ T.guard r (DescriptiveComplexity.Draw.unpad ⋯ τ.2) | x => False

def DescriptiveComplexity.Draw.Table.Src {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Univ A R P K dd → Prop

The state a transition applies in, read off its rule and its data.

Equations

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

def DescriptiveComplexity.Draw.Table.Read {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Univ A R P K dd → Prop

The symbol a transition reads.

Equations

• T.Read τ a = match τ.1 with | DescriptiveComplexity.Draw.Tag.ctrl r => a = DescriptiveComplexity.Draw.symElt T.zero (T.readPl r (DescriptiveComplexity.Draw.unpad ⋯ τ.2)) | x => False

def DescriptiveComplexity.Draw.Table.Dst {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Univ A R P K dd → Prop

The state a transition moves to.

Equations

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

def DescriptiveComplexity.Draw.Table.Write {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Univ A R P K dd → Prop

The symbol a transition writes.

Equations

• T.Write τ a = match τ.1 with | DescriptiveComplexity.Draw.Tag.ctrl r => a = DescriptiveComplexity.Draw.symElt T.zero (T.writePl r (DescriptiveComplexity.Draw.unpad ⋯ τ.2)) | x => False

def DescriptiveComplexity.Draw.Table.IsRight {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Prop

Moving right: a function of the rule alone, hence of the tag.

Equations

• T.IsRight τ = match τ.1 with | DescriptiveComplexity.Draw.Tag.ctrl r => T.moveRight r | x => False

def DescriptiveComplexity.Draw.Table.IsStart {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Prop

The start state.

Equations

• T.IsStart q = (q = DescriptiveComplexity.Draw.stateElt T.zero T.startPh T.startPl)

def DescriptiveComplexity.Draw.Table.IsAcc {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Prop

The accepting states: a phase-tagged, canonically padded element whose phase and pointer the table accepts.

Equations

• T.IsAcc q = match q.1 with | DescriptiveComplexity.Draw.Tag.phase p => DescriptiveComplexity.Draw.IsPad c T.zero q.2 ∧ T.accept p (DescriptiveComplexity.Draw.unpad ⋯ q.2) | x => False

def DescriptiveComplexity.Draw.Table.IsBlank {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Prop

The blank.

Equations

• T.IsBlank a = (a = DescriptiveComplexity.Draw.symElt T.zero T.blankPl)

def DescriptiveComplexity.Draw.Table.Inp {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Univ A R P K dd → Univ A R P K dd → Prop

The input channel: the cell of an element the table writes for holds the mark the table gives it. Functional outright, and total exactly on the elements the table marks.

Equations

• T.Inp x a = (T.Marked x ∧ a = DescriptiveComplexity.Draw.symElt T.zero (T.markPl x))

What a rule does

The five attributes of a transition, read at the element the rule and its data name. Each is the definitional unfolding of the predicate above with DescriptiveComplexity.Draw.unpad_pad applied to the payload, and together they are the only thing a program ever needs about the table.

theorem DescriptiveComplexity.Draw.Table.isTr_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) {r : R} {w : Fin c → A} (hg : T.guard r w) : T.IsTr (trElt T.zero r w)

theorem DescriptiveComplexity.Draw.Table.isAcc_stateElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) {p : P} {w : Fin c → A} (ha : T.accept p w) : T.IsAcc (stateElt T.zero p w)

theorem DescriptiveComplexity.Draw.Table.src_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) (r : R) (w : Fin c → A) : T.Src (trElt T.zero r w) (stateElt T.zero (T.srcPh r) (T.srcPl r w))

theorem DescriptiveComplexity.Draw.Table.read_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) (r : R) (w : Fin c → A) : T.Read (trElt T.zero r w) (symElt T.zero (T.readPl r w))

theorem DescriptiveComplexity.Draw.Table.dst_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) (r : R) (w : Fin c → A) : T.Dst (trElt T.zero r w) (stateElt T.zero (T.dstPh r) (T.dstPl r w))

theorem DescriptiveComplexity.Draw.Table.write_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) (r : R) (w : Fin c → A) : T.Write (trElt T.zero r w) (symElt T.zero (T.writePl r w))

theorem DescriptiveComplexity.Draw.Table.isRight_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) {r : R} (w : Fin c → A) (hd : T.moveRight r) : T.IsRight (trElt T.zero r w)

theorem DescriptiveComplexity.Draw.Table.not_isRight_trElt {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) {r : R} (w : Fin c → A) (hd : ¬T.moveRight r) : ¬T.IsRight (trElt T.zero r w)

An instance that reads the table

structure DescriptiveComplexity.Draw.Table.Reads {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] : Prop

An instance reads the table: its eleven relations are the predicates above and its order is the definable one. Everything a program proves is proved under this hypothesis, so the interpretation that emits the instance has exactly eleven obligations and no more.

• le (x y : Univ A R P K dd) : WMLe x y ↔ tagTupleLe x y

  The order is the block-major one on tagged tuples.

• tr (τ : Univ A R P K dd) : WMTr τ ↔ T.IsTr τ

  The transitions.

• start (q : Univ A R P K dd) : WMStart q ↔ T.IsStart q

  The start state.

• acc (q : Univ A R P K dd) : WMAcc q ↔ T.IsAcc q

  The accepting states.

• blank (a : Univ A R P K dd) : WMBlank a ↔ T.IsBlank a

  The blank.

• right (τ : Univ A R P K dd) : WMRight τ ↔ T.IsRight τ

  The direction.

• src (τ q : Univ A R P K dd) : WMSrc τ q ↔ T.Src τ q

  The state a transition applies in.

• read (τ a : Univ A R P K dd) : WMRead τ a ↔ T.Read τ a

  The symbol a transition reads.

• dst (τ q : Univ A R P K dd) : WMDst τ q ↔ T.Dst τ q

  The state a transition moves to.

• write (τ a : Univ A R P K dd) : WMWrite τ a ↔ T.Write τ a

  The symbol a transition writes.

• inp (x a : Univ A R P K dd) : WMInp x a ↔ T.Inp x a

  The input channel.

Firing a rule

The shape every subroutine of the address layer asks for – a transition with its six attributes, the direction being the one the caller wants. A program's whole interaction with the table is these two theorems.

theorem DescriptiveComplexity.Draw.Table.fire_right {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) {r : R} {w : Fin c → A} (hg : T.guard r w) (hd : T.moveRight r) {q a q' a' : Univ A R P K dd} (hq : q = stateElt T.zero (T.srcPh r) (T.srcPl r w)) (ha : a = symElt T.zero (T.readPl r w)) (hq' : q' = stateElt T.zero (T.dstPh r) (T.dstPl r w)) (ha' : a' = symElt T.zero (T.writePl r w)) : ∃ (τ : Univ A R P K dd), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q' ∧ WMWrite τ a' ∧ WMRight τ

A rule fires, moving right.

theorem DescriptiveComplexity.Draw.Table.fire_left {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) {r : R} {w : Fin c → A} (hg : T.guard r w) (hd : ¬T.moveRight r) {q a q' a' : Univ A R P K dd} (hq : q = stateElt T.zero (T.srcPh r) (T.srcPl r w)) (ha : a = symElt T.zero (T.readPl r w)) (hq' : q' = stateElt T.zero (T.dstPh r) (T.dstPl r w)) (ha' : a' = symElt T.zero (T.writePl r w)) : ∃ (τ : Univ A R P K dd), WMTr τ ∧ WMSrc τ q ∧ WMRead τ a ∧ WMDst τ q' ∧ WMWrite τ a' ∧ ¬WMRight τ

A rule fires, moving left.

The two promises

theorem DescriptiveComplexity.Draw.Table.isLinOrd_wmLe {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) : IsLinOrd WMLe

The order of the emitted instance is linear, being the definable order on tagged tuples.

theorem DescriptiveComplexity.Draw.Table.wellFormed {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] (hR : T.Reads) : (wideData (Univ A R P K dd)).WellFormed

The emitted instance is well formed. Three conditions (DescriptiveComplexity.wideData_wellFormed_iff), and all three are settled by the layout: the order is DescriptiveComplexity.tagTupleLe, and the input and the blank are equations.

def DescriptiveComplexity.Draw.Table.Sep {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) : Prop

The separation condition: two guarded rules that apply in the same state and read the same symbol are the same rule with the same data. This is the whole content of determinism, and the only obligation a concrete table has to discharge by hand.

Equations

• T.Sep = ∀ (r r' : R) (w w' : Fin c → A), T.guard r w → T.guard r' w' → T.srcPh r = T.srcPh r' → T.srcPl r w = T.srcPl r' w' → T.readPl r w = T.readPl r' w' → r = r' ∧ w = w'

def DescriptiveComplexity.Draw.Table.SepOn {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) (Ph : P → Prop) : Prop

The separation condition, asked at some phases only: two guarded rules that apply in the same state and read the same symbol are the same rule with the same data, provided the phase they apply in is one Ph names.

A program that guesses does not separate everywhere – that is what guessing is – but it separates at every phase it can be in once the guess is over, and DescriptiveComplexity.TMData.uniqueFrom_of_invariant asks for no more.

Equations

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

theorem DescriptiveComplexity.Draw.Table.tr_unique_of_sepOn {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) {Ph : P → Prop} (hsep : T.SepOn Ph) {q a : Univ A R P K dd} (hq : ∀ (p : P) (f : Fin c → A), q = stateElt T.zero p f → Ph p) (τ σ : Univ A R P K dd) : WMTr τ → WMTr σ → WMSrc τ q → WMSrc σ q → WMRead τ a → WMRead σ a → τ = σ

The transition is pinned wherever the phases separate: at a state whose phase satisfies Ph, the state and the symbol read name the transition. This is the hypothesis of DescriptiveComplexity.TMData.step_functional_at, and with it a guessing program is functional off its guess.

theorem DescriptiveComplexity.Draw.Table.dst_functional {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) (τ q q' : Univ A R P K dd) : WMDst τ q → WMDst τ q' → q = q'

A transition has one destination: it is an equation in the rule.

theorem DescriptiveComplexity.Draw.Table.write_functional {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) (τ a a' : Univ A R P K dd) : WMWrite τ a → WMWrite τ a' → a = a'

A transition writes one symbol: it is an equation in the rule.

theorem DescriptiveComplexity.Draw.Table.deterministic {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : T.Reads) (hsep : T.Sep) : (wideData (Univ A R P K dd)).Deterministic

The emitted instance is deterministic, given the separation condition. The three other clauses of DescriptiveComplexity.WideDet are free: the start state, the destination and the written symbol are all written as equations.

The bounds of the outer loop

DescriptiveComplexity.Draw.wmSetLe_logicalTop is about the block-major order on tagged tuples; a program's loop is about the order its instance carries. They are the same order, which is what the layout was chosen for, and this is where the two are joined.

theorem DescriptiveComplexity.Draw.Table.wmSetLe_congr_rel {α : Type} {Le Le' : α → α → Prop} (h : ∀ (x y : α), Le x y ↔ Le' x y) (s u : α → Prop) : WMSetLe Le s u ↔ WMSetLe Le' s u

The order on addresses depends on the order of the elements only through its extension.

theorem DescriptiveComplexity.Draw.Table.wmSetLe_logicalTop_reads {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] (hR : T.Reads) {s : Univ A R P K dd → Prop} (hjunk : ∀ (τ : Tag R P K), (∀ (i : K), τ ≠ Tag.arg i) → ∀ (v : Fin dd → A), ¬s (τ, v)) : WMSetLe WMLe s logicalTop

A logical address is at or below the last one, in the machine's own order: the addresses whose non-argument blocks are empty – the ones that hold the stage of the fixed point – are an initial interval of the tape, and this is the upper bound DescriptiveComplexity.reaches_of_wideRounds is given.

The two ends of a run

What a program starts from and what it has to reach, in the table's own terms. Between them and DescriptiveComplexity.Draw.Table.fire_right / DescriptiveComplexity.Draw.Table.fire_left, a program never mentions FirstOrder.Language.wide again.

theorem DescriptiveComplexity.Draw.Table.isInit {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] (hR : T.Reads) (hmk : ∀ (x : Univ A R P K dd), T.Marked x) {f : (Univ A R P K dd → Prop) → Univ A R P K dd} (hmark : ∀ (x : Univ A R P K dd), f (wmSeg x) = symElt T.zero (T.markPl x)) (hrest : ∀ (s : Univ A R P K dd → Prop), (∀ (x : Univ A R P K dd), s ≠ wmSeg x) → f s = symElt T.zero T.blankPl) : (wideData (Univ A R P K dd)).IsInit { state := Sum.inr (stateElt T.zero T.startPh T.startPl), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape f (symElt T.zero T.blankPl) }

The initial configuration of the emitted machine: the start state, the head on the empty address, the mark of each element in that element's cell and the blank everywhere else.

theorem DescriptiveComplexity.Draw.Table.acceptsSpace {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] (hR : T.Reads) (hmk : ∀ (x : Univ A R P K dd), T.Marked x) {f : (Univ A R P K dd → Prop) → Univ A R P K dd} (hmark : ∀ (x : Univ A R P K dd), f (wmSeg x) = symElt T.zero (T.markPl x)) (hrest : ∀ (s : Univ A R P K dd → Prop), (∀ (x : Univ A R P K dd), s ≠ wmSeg x) → f s = symElt T.zero T.blankPl) {cfg : Config (WPoint (Univ A R P K dd))} (hreach : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (stateElt T.zero T.startPh T.startPl), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape f (symElt T.zero T.blankPl) } cfg) {p : P} {w : Fin c → A} (hstate : cfg.state = Sum.inr (stateElt T.zero p w)) (ha : T.accept p w) : (wideData (Univ A R P K dd)).AcceptsSpace

The emitted machine accepts in bounded space: it starts as DescriptiveComplexity.Draw.Table.isInit says, roams, and ends in a state the table accepts.

theorem DescriptiveComplexity.Draw.Table.accepts {A R P K : Type} {c dd : ℕ} (T : Table A R P K c dd) [LinearOrder R] [LinearOrder P] [LinearOrder K] [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] (hR : T.Reads) (hmk : ∀ (x : Univ A R P K dd), T.Marked x) {f : (Univ A R P K dd → Prop) → Univ A R P K dd} (hmark : ∀ (x : Univ A R P K dd), f (wmSeg x) = symElt T.zero (T.markPl x)) (hrest : ∀ (s : Univ A R P K dd → Prop), (∀ (x : Univ A R P K dd), s ≠ wmSeg x) → f s = symElt T.zero T.blankPl) {n : ℕ} {cfg : Config (WPoint (Univ A R P K dd))} (hreach : (wideData (Univ A R P K dd)).ReachesIn n { state := Sum.inr (stateElt T.zero T.startPh T.startPl), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape f (symElt T.zero T.blankPl) } cfg) (hlt : n < 2 ^ Nat.card (Univ A R P K dd)) {p : P} {w : Fin c → A} (hstate : cfg.state = Sum.inr (stateElt T.zero p w)) (ha : T.accept p w) : (wideData (Univ A R P K dd)).Accepts

The emitted machine accepts on the clock: it starts as DescriptiveComplexity.Draw.Table.isInit says, runs for fewer steps than there are addresses – 2 ^ n of them, n the size of the drawn universe – and ends in a state the table accepts. This is the reading a time-bounded reduction needs, where DescriptiveComplexity.Draw.Table.acceptsSpace is the space-bounded one.