Writing the emitted machine down

DescriptiveComplexity.Problems.Wide.DrawTable says what the eleven relations of a wide-machine instance are, as predicates on tagged tuples; the definability layer (DescriptiveComplexity.Problems.Wide.DrawFactor and the files above it) says that every attribute of every rule is decided by one formula for every instance. This file joins the two: the shapes each relation has, as formulas, with their realizations.

Where the coordinates go

A defining formula of an n-ary relation has free variables Fin n × Fin dd: the i-th argument's tuple is fun j => v (i, j). A rule's payload occupies the first c = card (CtlIx ⊕ SlotIx) of those, so the guard and payload formulas the definability layer hands over – which live over Fin c and over Fin c ⊕ Fin c – are relabeled onto (i, castLE hpl k) and nothing else happens to them.

What a tag decides

Everything a tag decides is decided when the formula is built, by DescriptiveComplexity.Draw.sideF: which rule a transition is, and so its two phases and its direction; which phase a state is in; that a symbol is a symbol. What is left for the formula is the shape – a tuple is canonically padded (DescriptiveComplexity.canonF, read at the layout's IsPad by DescriptiveComplexity.Draw.realize_canonF_isPad) – and the payload.

A condition the tag decides

noncomputable def DescriptiveComplexity.Draw.sideF {L : FirstOrder.Language} (γ : Type) (p : Prop) : (L.sum FirstOrder.Language.order).Formula γ

A condition decided when the formula is built.

Equations

• DescriptiveComplexity.Draw.sideF γ p = if p then ⊤ else ⊥

@[simp]

theorem DescriptiveComplexity.Draw.realize_sideF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {p : Prop} : (sideF γ p).Realize v ↔ p

The coordinates a payload occupies

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.argVar (n dd : ℕ) (i : Fin n) : Fin dd → Fin n × Fin dd

The coordinates of the i-th argument.

Equations

• DescriptiveComplexity.Draw.argVar n dd i j = (i, j)

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.payVar {Q W : Type} [Fintype Q] [Fintype W] {dd : ℕ} (n : ℕ) (hc : Fintype.card (Q ⊕ W) ≤ dd) (i : Fin n) : Fin (Fintype.card (Q ⊕ W)) → Fin n × Fin dd

The coordinates the i-th argument's payload occupies.

Equations

• DescriptiveComplexity.Draw.payVar n hc i k = (i, Fin.castLE hc k)

A guard and a payload, relabeled

noncomputable def DescriptiveComplexity.Draw.guardAt {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd n : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) (i : Fin n) (φ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)))) : (L.sum FirstOrder.Language.order).Formula (Fin n × Fin dd)

A guard, at the payload of the i-th argument.

Equations

• DescriptiveComplexity.Draw.guardAt hc i φ = FirstOrder.Language.Formula.relabel (DescriptiveComplexity.Draw.payVar n hc i) φ

noncomputable def DescriptiveComplexity.Draw.payAt {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd n : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) (i i' : Fin n) (χ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)) ⊕ Fin (Fintype.card (Q ⊕ W)))) : (L.sum FirstOrder.Language.order).Formula (Fin n × Fin dd)

A payload written from another, at two arguments.

Equations

• DescriptiveComplexity.Draw.payAt hc i i' χ = FirstOrder.Language.Formula.relabel (Sum.elim (DescriptiveComplexity.Draw.payVar n hc i) (DescriptiveComplexity.Draw.payVar n hc i')) χ

theorem DescriptiveComplexity.Draw.realize_guardAt {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd n : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) {A : Type} [L.Structure A] [LinearOrder A] {v : Fin n × Fin dd → A} {i : Fin n} {φ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)))} : (guardAt hc i φ).Realize v ↔ φ.Realize (unpad hc fun (j : Fin dd) => v (i, j))

theorem DescriptiveComplexity.Draw.realize_payAt {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd n : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) {A : Type} [L.Structure A] [LinearOrder A] {v : Fin n × Fin dd → A} {i i' : Fin n} {χ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)) ⊕ Fin (Fintype.card (Q ⊕ W)))} : (payAt hc i i' χ).Realize v ↔ χ.Realize (Sum.elim (unpad hc fun (j : Fin dd) => v (i, j)) (unpad hc fun (j : Fin dd) => v (i', j)))

The three shapes a defining formula has

Every one of the eleven relations is one of three shapes: a guarded padded tuple (a transition, an accepting state), an attribute – an element of a tag the formula names whose payload is written from another's – or a constant, a tag and the all-clear tuple.

theorem DescriptiveComplexity.Draw.eq_pad_iff {Q W : Type} [Fintype Q] [Fintype W] {dd : ℕ} {A : Type} {zero : A} (hc : Fintype.card (Q ⊕ W) ≤ dd) (u : Fin dd → A) (w : Fin (Fintype.card (Q ⊕ W)) → A) : u = pad zero w ↔ IsPad (Fintype.card (Q ⊕ W)) zero u ∧ unpad hc u = w

Being a given padded tuple splits into being padded and carrying the payload, which is what a defining formula can say separately.

noncomputable def DescriptiveComplexity.Draw.padGuardF {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) (p : Prop) (φ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)))) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dd)

A guarded padded tuple: the tag decides everything but the shape, and the guard is the definability layer's formula at the payload.

Equations

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

noncomputable def DescriptiveComplexity.Draw.attrF {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) (p : Prop) (χ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)) ⊕ Fin (Fintype.card (Q ⊕ W)))) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dd)

An attribute of a transition: an element of the tag the rule names, whose payload the rule writes from the transition's own.

Equations

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

theorem DescriptiveComplexity.Draw.realize_padGuardF {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) {A : Type} [L.Structure A] [LinearOrder A] {zero : A} (h₀ : IsBot zero) {p : Prop} {φ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)))} {v : Fin 1 × Fin dd → A} : (padGuardF hc p φ).Realize v ↔ p ∧ (IsPad (Fintype.card (Q ⊕ W)) zero fun (j : Fin dd) => v (0, j)) ∧ φ.Realize (unpad hc fun (j : Fin dd) => v (0, j))

theorem DescriptiveComplexity.Draw.realize_attrF {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {dd : ℕ} (hc : Fintype.card (Q ⊕ W) ≤ dd) {A : Type} [L.Structure A] [LinearOrder A] {zero : A} (h₀ : IsBot zero) {p : Prop} {χ : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (Q ⊕ W)) ⊕ Fin (Fintype.card (Q ⊕ W)))} {F : (Fin (Fintype.card (Q ⊕ W)) → A) → Fin (Fintype.card (Q ⊕ W)) → A} (hχ : ∀ (w y : Fin (Fintype.card (Q ⊕ W)) → A), y = F w ↔ χ.Realize (Sum.elim w y)) {v : Fin 2 × Fin dd → A} : (attrF hc p χ).Realize v ↔ p ∧ (fun (j : Fin dd) => v (1, j)) = pad zero (F (unpad hc fun (j : Fin dd) => v (0, j)))

A constant: a tag and the all-clear tuple

noncomputable def DescriptiveComplexity.Draw.constF {L : FirstOrder.Language} {dd : ℕ} (p : Prop) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dd)

A constant: a tag and the all-clear tuple – the start state, the blank.

Equations

• DescriptiveComplexity.Draw.constF p = DescriptiveComplexity.Draw.sideF (Fin 1 × Fin dd) p ⊓ DescriptiveComplexity.canonF 0 (DescriptiveComplexity.Draw.argVar 1 dd 0)

theorem DescriptiveComplexity.Draw.realize_constF {L : FirstOrder.Language} {dd : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {zero : A} (h₀ : IsBot zero) {p : Prop} {v : Fin 1 × Fin dd → A} : (constF p).Realize v ↔ p ∧ (fun (j : Fin dd) => v (0, j)) = fun (x : Fin dd) => zero

The two extremes of the interpreted universe

The input channel's mark asks whether a cell is the first or the last of the tape, and the tape is ordered block-major. It would be a mistake to write those as quantifiers over the interpreted universe: in that order an element is least exactly when its tag is the least tag and its tuple is all-clear, and greatest exactly when its tag is the greatest and its tuple is all-set – a decision the tag makes, conjoined with a shape formula.

theorem DescriptiveComplexity.Draw.tupLeLex_all_iff {d : ℕ} {A : Type} [LinearOrder A] (u : Fin d → A) : (∀ (v : Fin d → A), tupLeLex u v) ↔ ∀ (j : Fin d), IsBot (u j)

A tuple below every other is the all-clear one.

theorem DescriptiveComplexity.Draw.isLeast_tagTupleLe_iff {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] (x : Tag × (Fin d → A)) : (∀ (y : Tag × (Fin d → A)), tagTupleLe x y) ↔ (∀ (t : Tag), x.1 ≤ t) ∧ ∀ (j : Fin d), IsBot (x.2 j)

A tagged tuple below every other: the least tag and the all-clear tuple.

theorem DescriptiveComplexity.Draw.tupLeLex_all_iff' {d : ℕ} {A : Type} [LinearOrder A] (u : Fin d → A) : (∀ (v : Fin d → A), tupLeLex v u) ↔ ∀ (j : Fin d), IsTop (u j)

A tuple above every other is the all-set one.

theorem DescriptiveComplexity.Draw.isGreatest_tagTupleLe_iff {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] (x : Tag × (Fin d → A)) : (∀ (y : Tag × (Fin d → A)), tagTupleLe y x) ↔ (∀ (t : Tag), t ≤ x.1) ∧ ∀ (j : Fin d), IsTop (x.2 j)

A tagged tuple above every other: the greatest tag and the all-set tuple.

The static data of a rule, extracted

DescriptiveComplexity.Draw.URuleDefinable says the two phases, the direction, the guard and the two payloads of a rule do not depend on the instance. What an interpretation writes down is those, and this is where they are named.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.RTagOf (S : Type) (Sh : S → Type) : Type

The rule names of the emitted machine, as a type the instance does not mention: one name per shape of each site. Both the site type and its shapes belong to the program, so the type is taken at an arbitrary pair; the space-bounded program's own are Draw.Data.SF and Draw.Data.SFSh, the clocked program's are its own.

Equations

• DescriptiveComplexity.Draw.Data.RTagOf S Sh = ((i : S) × Sh i)

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.ITagOf {L : FirstOrder.Language} (dt : Data L) (S : Type) (Sh : S → Type) (P : Type) : Type

The tags of the interpreted universe, at an arbitrary site type and an arbitrary phase type.

Equations

• dt.ITagOf S Sh P = DescriptiveComplexity.Draw.Tag (DescriptiveComplexity.Draw.Data.RTagOf S Sh) P dt.KIx

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.RTag {L : FirstOrder.Language} (dt : Data L) : Type

The rule names of the space-bounded program.

Equations

• dt.RTag = DescriptiveComplexity.Draw.Data.RTagOf dt.SF dt.SFSh

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.Data.ITag {L : FirstOrder.Language} (dt : Data L) : Type

The tags of the space-bounded program's interpreted universe.

Equations

• dt.ITag = dt.ITagOf dt.SF dt.SFSh dt.PF

noncomputable def DescriptiveComplexity.Draw.Data.srcPhOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) : P

The phase a rule fires from.

Equations

• DescriptiveComplexity.Draw.Data.srcPhOf hdef r = ⋯.choose

noncomputable def DescriptiveComplexity.Draw.Data.dstPhOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) : P

The phase it moves to.

Equations

• DescriptiveComplexity.Draw.Data.dstPhOf hdef r = ⋯.choose

noncomputable def DescriptiveComplexity.Draw.Data.rightOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) : Bool

Its direction.

Equations

• DescriptiveComplexity.Draw.Data.rightOf hdef r = ⋯.choose

noncomputable def DescriptiveComplexity.Draw.Data.guardFOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)))

Its guard, as a formula over the payload coordinates.

Equations

• DescriptiveComplexity.Draw.Data.guardFOf hdef r = Exists.choose ⋯

noncomputable def DescriptiveComplexity.Draw.Data.dstFOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) ⊕ Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)))

The payload of the state it moves to, as a formula.

Equations

• DescriptiveComplexity.Draw.Data.dstFOf hdef r = Exists.choose ⋯

noncomputable def DescriptiveComplexity.Draw.Data.wrFOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) ⊕ Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)))

The payload of the symbol it writes, as a formula.

Equations

• DescriptiveComplexity.Draw.Data.wrFOf hdef r = Exists.choose ⋯

noncomputable def DescriptiveComplexity.Draw.Data.srcFOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) ⊕ Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)))

The payload of the state a rule fires in: the pointer, unchanged. One formula for every rule.

Equations

• DescriptiveComplexity.Draw.Data.srcFOf = Exists.choose ⋯

noncomputable def DescriptiveComplexity.Draw.Data.readFOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) ⊕ Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)))

And of the symbol it reads: the tracks, unchanged.

Equations

• DescriptiveComplexity.Draw.Data.readFOf = Exists.choose ⋯

What they say

theorem DescriptiveComplexity.Draw.Data.srcPhOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) (e : Env L) : (rules e r.fst r.snd).srcPh = srcPhOf hdef r

theorem DescriptiveComplexity.Draw.Data.dstPhOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) (e : Env L) : (rules e r.fst r.snd).dstPh = dstPhOf hdef r

theorem DescriptiveComplexity.Draw.Data.rightOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) (e : Env L) : (rules e r.fst r.snd).moveRight ↔ rightOf hdef r = true

theorem DescriptiveComplexity.Draw.Data.guardFOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) (e : Env L) (w : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → e.α) : ((rules e r.fst r.snd).guard (fun (q : dt.CtlIx) => unslot w (Sum.inl q)) fun (s : dt.SlotIx) => unslot w (Sum.inr s)) ↔ (guardFOf hdef r).Realize w

theorem DescriptiveComplexity.Draw.Data.dstFOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) (e : Env L) (w y : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → e.α) : y = stPl e.zero ((rules e r.fst r.snd).dstSt (fun (q : dt.CtlIx) => unslot w (Sum.inl q)) fun (s : dt.SlotIx) => unslot w (Sum.inr s)) ↔ (dstFOf hdef r).Realize (Sum.elim w y)

theorem DescriptiveComplexity.Draw.Data.wrFOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (r : RTagOf S Sh) (e : Env L) (w y : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → e.α) : y = syPl e.zero ((rules e r.fst r.snd).wr (fun (q : dt.CtlIx) => unslot w (Sum.inl q)) fun (s : dt.SlotIx) => unslot w (Sum.inr s)) ↔ (wrFOf hdef r).Realize (Sum.elim w y)

theorem DescriptiveComplexity.Draw.Data.srcFOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (e : Env L) (w y : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → e.α) : (y = stPl e.zero fun (q : dt.CtlIx) => unslot w (Sum.inl q)) ↔ srcFOf.Realize (Sum.elim w y)

theorem DescriptiveComplexity.Draw.Data.readFOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (e : Env L) (w y : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → e.α) : (y = syPl e.zero fun (s : dt.SlotIx) => unslot w (Sum.inr s)) ↔ readFOf.Realize (Sum.elim w y)

The transitions, and their five attributes

Each is one of the shapes above at the data the tag names: a transition is a guarded padded tuple, its four payload attributes are attributes, and its direction is decided outright.

noncomputable def DescriptiveComplexity.Draw.Data.trF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) : dt.ITagOf S Sh P → (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dt.dd)

Being a transition.

Equations

• DescriptiveComplexity.Draw.Data.trF hpl hdef (DescriptiveComplexity.Draw.Tag.ctrl r) = DescriptiveComplexity.Draw.padGuardF hpl True (DescriptiveComplexity.Draw.Data.guardFOf hdef r)
• DescriptiveComplexity.Draw.Data.trF hpl hdef x✝ = ⊥

noncomputable def DescriptiveComplexity.Draw.Data.rightF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) : dt.ITagOf S Sh P → (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dt.dd)

Moving the head right.

Equations

• DescriptiveComplexity.Draw.Data.rightF hdef (DescriptiveComplexity.Draw.Tag.ctrl r) = DescriptiveComplexity.Draw.sideF (Fin 1 × Fin dt.dd) (DescriptiveComplexity.Draw.Data.rightOf hdef r = true)
• DescriptiveComplexity.Draw.Data.rightF hdef x✝ = ⊥

noncomputable def DescriptiveComplexity.Draw.Data.srcF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (t t' : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The state a transition applies in.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.srcF hpl hdef t t' = ⊥

noncomputable def DescriptiveComplexity.Draw.Data.readF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t t' : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The symbol it reads.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.readF hpl t t' = ⊥

noncomputable def DescriptiveComplexity.Draw.Data.dstF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (t t' : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The state it moves to.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.dstF hpl hdef t t' = ⊥

noncomputable def DescriptiveComplexity.Draw.Data.writeF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (t t' : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The symbol it writes.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.writeF hpl hdef t t' = ⊥

What they say

theorem DescriptiveComplexity.Draw.Data.realize_trF_ctrl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (e : Env L) (r : RTagOf S Sh) {v : Fin 1 × Fin dt.dd → e.α} : (trF hpl hdef (Tag.ctrl r)).Realize v ↔ (IsPad (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) e.zero fun (j : Fin dt.dd) => v (0, j)) ∧ (rules e r.fst r.snd).guard (fun (q : dt.CtlIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inl q)) fun (s : dt.SlotIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inr s)

theorem DescriptiveComplexity.Draw.Data.realize_rightF_ctrl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hdef : URulesDefinable rules) (e : Env L) (r : RTagOf S Sh) {v : Fin 1 × Fin dt.dd → e.α} : (rightF hdef (Tag.ctrl r)).Realize v ↔ (rules e r.fst r.snd).moveRight

theorem DescriptiveComplexity.Draw.Data.realize_srcF_ctrl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (e : Env L) (r : RTagOf S Sh) (t' : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (srcF hpl hdef (Tag.ctrl r) t').Realize v ↔ (t', fun (j : Fin dt.dd) => v (1, j)) = stateElt e.zero (srcPhOf hdef r) (stPl e.zero fun (q : dt.CtlIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inl q))

theorem DescriptiveComplexity.Draw.Data.realize_readF_ctrl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (r : RTagOf S Sh) (t' : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (readF hpl (Tag.ctrl r) t').Realize v ↔ (t', fun (j : Fin dt.dd) => v (1, j)) = symElt e.zero (syPl e.zero fun (s : dt.SlotIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inr s))

theorem DescriptiveComplexity.Draw.Data.realize_dstF_ctrl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (e : Env L) (r : RTagOf S Sh) (t' : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (dstF hpl hdef (Tag.ctrl r) t').Realize v ↔ (t', fun (j : Fin dt.dd) => v (1, j)) = stateElt e.zero (dstPhOf hdef r) (stPl e.zero ((rules e r.fst r.snd).dstSt (fun (q : dt.CtlIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inl q)) fun (s : dt.SlotIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inr s)))

theorem DescriptiveComplexity.Draw.Data.realize_writeF_ctrl {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (e : Env L) (r : RTagOf S Sh) (t' : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (writeF hpl hdef (Tag.ctrl r) t').Realize v ↔ (t', fun (j : Fin dt.dd) => v (1, j)) = symElt e.zero (syPl e.zero ((rules e r.fst r.snd).wr (fun (q : dt.CtlIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inl q)) fun (s : dt.SlotIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inr s)))

Two more shapes: a bit, and an all-set tuple

noncomputable def DescriptiveComplexity.Draw.bitAtF {L : FirstOrder.Language} {γ : Type} (y : γ) (φ : (L.sum FirstOrder.Language.order).Formula γ) : (L.sum FirstOrder.Language.order).Formula γ

A variable holds the bit of a condition.

Equations

• DescriptiveComplexity.Draw.bitAtF y φ = φ ⊓ DescriptiveComplexity.topF y ⊔ FirstOrder.Language.BoundedFormula.not φ ⊓ DescriptiveComplexity.botF y

noncomputable def DescriptiveComplexity.Draw.topTupF {L : FirstOrder.Language} {γ : Type} {D : ℕ} (u : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

Every coordinate of a tuple is the greatest element: the mirror of DescriptiveComplexity.canonF at length 0.

Equations

• DescriptiveComplexity.Draw.topTupF u = DescriptiveComplexity.listInf (List.map (fun (j : Fin D) => DescriptiveComplexity.topF (u j)) (List.finRange D))

theorem DescriptiveComplexity.Draw.realize_bitAtF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {zero one : A} (h₀ : IsBot zero) (h₁ : IsTop one) {y : γ} {φ : (L.sum FirstOrder.Language.order).Formula γ} : (bitAtF y φ).Realize v ↔ v y = bitVal zero one (φ.Realize v)

theorem DescriptiveComplexity.Draw.realize_topTupF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {D : ℕ} {u : Fin D → γ} : (topTupF u).Realize v ↔ ∀ (j : Fin D), IsTop (v (u j))

noncomputable def DescriptiveComplexity.Draw.Data.accFOf {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {P : Type} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p : P) : (L.sum FirstOrder.Language.order).Formula (Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)))

The accepting predicate of a phase, as a formula.

Equations

• DescriptiveComplexity.Draw.Data.accFOf hacc p = Exists.choose ⋯

theorem DescriptiveComplexity.Draw.Data.accFOf_spec {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {P : Type} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p : P) (e : Env L) (w : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) → e.α) : (accept e p fun (q : dt.CtlIx) => unslot w (Sum.inl q)) ↔ (accFOf hacc p).Realize w

noncomputable def DescriptiveComplexity.Draw.Data.accF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) : dt.ITagOf S Sh P → (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dt.dd)

Being an accepting state.

Equations

• DescriptiveComplexity.Draw.Data.accF hpl hacc (DescriptiveComplexity.Draw.Tag.phase p) = DescriptiveComplexity.Draw.padGuardF hpl True (DescriptiveComplexity.Draw.Data.accFOf hacc p)
• DescriptiveComplexity.Draw.Data.accF hpl hacc x✝ = ⊥

noncomputable def DescriptiveComplexity.Draw.Data.startF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (p₀ : P) (t : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dt.dd)

Being the start state: the start phase and the all-clear tuple.

Equations

• DescriptiveComplexity.Draw.Data.startF p₀ t = DescriptiveComplexity.Draw.constF (t = DescriptiveComplexity.Draw.Tag.phase p₀)

noncomputable def DescriptiveComplexity.Draw.Data.blankF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (t : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dt.dd)

Being the blank: the alphabet tag and the all-clear tuple.

Equations

• DescriptiveComplexity.Draw.Data.blankF t = DescriptiveComplexity.Draw.constF (t = DescriptiveComplexity.Draw.Tag.sym)

theorem DescriptiveComplexity.Draw.Data.realize_accF_phase {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (e : Env L) (p : P) {v : Fin 1 × Fin dt.dd → e.α} : (accF hpl hacc (Tag.phase p)).Realize v ↔ (IsPad (Fintype.card (dt.CtlIx ⊕ dt.SlotIx)) e.zero fun (j : Fin dt.dd) => v (0, j)) ∧ accept e p fun (q : dt.CtlIx) => unslot (unpad hpl fun (j : Fin dt.dd) => v (0, j)) (Sum.inl q)

theorem DescriptiveComplexity.Draw.Data.realize_startF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (e : Env L) (p₀ : P) (t : dt.ITagOf S Sh P) {v : Fin 1 × Fin dt.dd → e.α} : (startF p₀ t).Realize v ↔ (t, fun (j : Fin dt.dd) => v (0, j)) = (Tag.phase p₀, fun (x : Fin dt.dd) => e.zero)

theorem DescriptiveComplexity.Draw.Data.realize_blankF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} (e : Env L) (t : dt.ITagOf S Sh P) {v : Fin 1 × Fin dt.dd → e.α} : (blankF t).Realize v ↔ (t, fun (j : Fin dt.dd) => v (0, j)) = (Tag.sym, fun (x : Fin dt.dd) => e.zero)

The input channel

The one relation with content. The mark a cell starts with (DescriptiveComplexity.Draw.slotMark) is a register file: the register flag is set, the first and last cells of the tape are flagged, the block flags decode the cell's tag, the name slots carry the cell's own first dd₀ coordinates and the padding flag says the rest are clear. Every one of those is a tag decision, a shape formula, or an equality of variables – the two extremes because of DescriptiveComplexity.Draw.isLeast_tagTupleLe_iff and its dual.

noncomputable def DescriptiveComplexity.Draw.Data.markSlotF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (t : dt.ITagOf S Sh P) (y : Fin 2 × Fin dt.dd) : dt.SlotIx → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

What one slot of a cell's mark holds, at the variable that slot occupies.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.markSlotF t y DescriptiveComplexity.Draw.Slot.reg = DescriptiveComplexity.topF y
• DescriptiveComplexity.Draw.Data.markSlotF t y x✝ = DescriptiveComplexity.botF y

noncomputable def DescriptiveComplexity.Draw.Data.markCoordF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t : dt.ITagOf S Sh P) (k : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

One coordinate of a cell's mark: the control slots of a symbol are clear, the track slots are the register file's.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.markF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The whole mark, coordinate by coordinate.

Equations

• DescriptiveComplexity.Draw.Data.markF hpl t = DescriptiveComplexity.listInf (List.map (DescriptiveComplexity.Draw.Data.markCoordF hpl t) (List.finRange (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))))

noncomputable def DescriptiveComplexity.Draw.Data.inpF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t t' : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The input channel: the cell of an element holds that element's mark.

Equations

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

theorem DescriptiveComplexity.Draw.Data.realize_markSlotF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (e : Env L) (t : dt.ITagOf S Sh P) (y : Fin 2 × Fin dt.dd) (s : dt.SlotIx) {v : Fin 2 × Fin dt.dd → e.α} : (markSlotF t y s).Realize v ↔ v y = slotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j)) s

theorem DescriptiveComplexity.Draw.Data.realize_markCoordF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (t : dt.ITagOf S Sh P) (k : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))) {v : Fin 2 × Fin dt.dd → e.α} : (markCoordF hpl t k).Realize v ↔ unpad hpl (fun (j : Fin dt.dd) => v (1, j)) k = syPl e.zero (slotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j))) k

theorem DescriptiveComplexity.Draw.Data.realize_markF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (t : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (markF hpl t).Realize v ↔ (unpad hpl fun (j : Fin dt.dd) => v (1, j)) = syPl e.zero (slotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j)))

theorem DescriptiveComplexity.Draw.Data.realize_inpF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (t t' : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (inpF hpl t t').Realize v ↔ (t', fun (j : Fin dt.dd) => v (1, j)) = symElt e.zero (syPl e.zero (slotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j))))

The register channel's own mark

The mark of DescriptiveComplexity.Draw.regSlotMark differs from the one above in a single slot – regFirst, which at the register channel says «greatest element carrying no argument block» rather than «least element» – so the formulas differ in a single conjunct, and everything else is reused.

theorem DescriptiveComplexity.Draw.Data.isTopNonArg_iff {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (e : Env L) (x : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : IsTopNonArg x ↔ (∀ (i : dt.KIx), x.1 ≠ Tag.arg i) ∧ (∀ (t : Tag (RTagOf S Sh) P dt.KIx), (∀ (i : dt.KIx), t ≠ Tag.arg i) → t ≤ x.1) ∧ ∀ (j : Fin dt.dd), IsTop (x.2 j)

What the regFirst slot has to say, in tag and tuple: the tag is one of the greatest carrying no argument block, and the tuple is the greatest. This is the reading DescriptiveComplexity.Draw.isGreatest_tagTupleLe_iff gives for the whole universe, restricted to the elements below the argument tags.

noncomputable def DescriptiveComplexity.Draw.Data.markSlotRegF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (t : dt.ITagOf S Sh P) (y : Fin 2 × Fin dt.dd) : dt.SlotIx → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

What one slot of a cell's mark holds at the register channel: the mark above, with regFirst reading the file's own first register.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.Data.markSlotRegF t y x✝ = DescriptiveComplexity.Draw.Data.markSlotF t y x✝

noncomputable def DescriptiveComplexity.Draw.Data.markCoordRegF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t : dt.ITagOf S Sh P) (k : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

@[inherit_doc markSlotRegF]

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.markRegF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The whole mark of the register channel, coordinate by coordinate.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.inpRegF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (t t' : dt.ITagOf S Sh P) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

The register channel: the cell of an element holds that element's mark, the mark being the register channel's.

Equations

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

theorem DescriptiveComplexity.Draw.Data.realize_markSlotRegF {L : FirstOrder.Language} {dt : Data L} {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (e : Env L) (t : dt.ITagOf S Sh P) (y : Fin 2 × Fin dt.dd) (s : dt.SlotIx) {v : Fin 2 × Fin dt.dd → e.α} : (markSlotRegF t y s).Realize v ↔ v y = regSlotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j)) s

theorem DescriptiveComplexity.Draw.Data.realize_markCoordRegF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (t : dt.ITagOf S Sh P) (k : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))) {v : Fin 2 × Fin dt.dd → e.α} : (markCoordRegF hpl t k).Realize v ↔ unpad hpl (fun (j : Fin dt.dd) => v (1, j)) k = syPl e.zero (regSlotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j))) k

theorem DescriptiveComplexity.Draw.Data.realize_markRegF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (t : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (markRegF hpl t).Realize v ↔ (unpad hpl fun (j : Fin dt.dd) => v (1, j)) = syPl e.zero (regSlotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j)))

theorem DescriptiveComplexity.Draw.Data.realize_inpRegF {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (t t' : dt.ITagOf S Sh P) {v : Fin 2 × Fin dt.dd → e.α} : (inpRegF hpl t t').Realize v ↔ (t', fun (j : Fin dt.dd) => v (1, j)) = symElt e.zero (syPl e.zero (regSlotMark e.zero e.one ⋯ (t, fun (j : Fin dt.dd) => v (0, j))))

theorem DescriptiveComplexity.Draw.Data.pad_const {L : FirstOrder.Language} {dt : Data L} (e : Env L) {c : ℕ} : (pad e.zero fun (x : Fin c) => e.zero) = fun (x : Fin dt.dd) => e.zero

A payload of clear elements pads to a tuple of clear elements.

theorem DescriptiveComplexity.Draw.Data.stPl_const {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (e : Env L) : (stPl e.zero fun (x : dt.CtlIx) => e.zero) = fun (x : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))) => e.zero

The pointer the machine starts with is clear at every slot.

theorem DescriptiveComplexity.Draw.Data.syPl_const {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (e : Env L) : (syPl e.zero fun (x : dt.SlotIx) => e.zero) = fun (x : Fin (Fintype.card (dt.CtlIx ⊕ dt.SlotIx))) => e.zero

And so is the blank.

structure DescriptiveComplexity.Draw.Data.UMarkDef {L : FirstOrder.Language} (dt : Data L) [Fintype dt.SlotIx] (S : Type) (Sh : S → Type) (P : Type) : Type 1

A mark the interpretation can write down: what a cell holds before the machine runs, together with the formula that defines the input channel. The space-bounded program is handed a register file (regFileMark); the clocked program starts on a blank tape and builds its own file (blankMark).

• mark (e : Env L) : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd → dt.SlotIx → e.α

  What each cell holds.

• marked (e : Env L) : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd → Prop

  Which elements the channel writes for. All of them at the channel of DescriptiveComplexity.WideAccept; the register channel of DescriptiveComplexity.WideRegAccept restricts it, and the restriction is what puts the file it hands over inside the working region.

• form : dt.ITagOf S Sh P → dt.ITagOf S Sh P → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)

  The formula the interpretation writes for the input channel.

• spec (e : Env L) (t t' : dt.ITagOf S Sh P) (v : Fin 2 × Fin dt.dd → e.α) : (self.form t t').Realize v ↔ self.marked e (t, fun (j : Fin dt.dd) => v (0, j)) ∧ (t', fun (j : Fin dt.dd) => v (1, j)) = symElt e.zero (syPl e.zero (self.mark e (t, fun (j : Fin dt.dd) => v (0, j))))

  What that formula says: the first element is one the channel writes for, and the second is its cell.

noncomputable def DescriptiveComplexity.Draw.Data.regFileMark {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) : dt.UMarkDef S Sh P

The register file, as a mark: DescriptiveComplexity.Draw.slotMark defined by inpF.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.regFileMarkArg {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) : dt.UMarkDef S Sh P

The register file, at the argument elements only: the mark a program emitted into the register channel of DescriptiveComplexity.WideRegAccept writes. The content is DescriptiveComplexity.Draw.regSlotMark's, which differs from the segment channel's in the regFirst slot alone; what is new is that the channel writes for the argument-tagged elements and one element below them, the greatest carrying no argument block. That element is what puts the file the channel hands over above the working area: every cell holds it, and no logical address reaches down to it (DescriptiveComplexity.wmSetLt_wmRegSeg_of_above).

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.blankMark {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} : dt.UMarkDef S Sh P

A blank tape, as a mark: every cell is the blank, so the channel says no more than that the cell is a symbol with a clear payload.

Equations

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

The interpretation

Eleven relation symbols, eleven formulas – the ten above and the order, which is DescriptiveComplexity.lexLeF, the tags compared when the formula is built.

The program the interpretation writes down

noncomputable def DescriptiveComplexity.Draw.Data.progFrom {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (e : Env L) (rl : (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P) (p₀ : P) (acc : P → (dt.CtlIx → e.α) → Prop) (mk : dt.UMarkDef S Sh P) : Prog e.α (RTagOf S Sh) P dt.CtlIx dt.SlotIx dt.KIx dt.dd

The program at one instance: the rules the definability layer hands over, with the reduction's constants – an all-clear pointer, an all-clear blank and the register file of DescriptiveComplexity.Draw.slotMark.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.drawInterp {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.wide (dt.ITagOf S Sh P) dt.dd

The emitted machine, written down: an interpretation of the wide-machine vocabulary in the ordered source vocabulary, tagged by the program's own tags.

Equations

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

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.Draw.Data.wideStr {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)

The structure the interpretation puts on the emitted universe.

Equations

• DescriptiveComplexity.Draw.Data.wideStr hpl hdef hacc p₀ mk e = (DescriptiveComplexity.Draw.Data.drawInterp hpl hdef hacc p₀ mk).mapStructure e.α

theorem DescriptiveComplexity.Draw.Data.relMap_one {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) {R : FirstOrder.Language.wide.Relations 1} {φ : dt.ITagOf S Sh P → (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin dt.dd)} (hR : (drawInterp hpl hdef hacc p₀ mk).relFormula R = fun (t : Fin 1 → dt.ITagOf S Sh P) => φ (t 0)) (x : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : FirstOrder.Language.Structure.RelMap R ![x] ↔ (φ x.1).Realize fun (q : Fin 1 × Fin dt.dd) => x.2 q.2

The valuation a unary relation's argument supplies.

theorem DescriptiveComplexity.Draw.Data.relMap_two {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) {R : FirstOrder.Language.wide.Relations 2} {φ : dt.ITagOf S Sh P → dt.ITagOf S Sh P → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin dt.dd)} (hR : (drawInterp hpl hdef hacc p₀ mk).relFormula R = fun (t : Fin 2 → dt.ITagOf S Sh P) => φ (t 0) (t 1)) (x y : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : FirstOrder.Language.Structure.RelMap R ![x, y] ↔ (φ x.1 y.1).Realize fun (z : Fin 2 × Fin dt.dd) => (if z.1 = 0 then x.2 else y.2) z.2

The valuation a binary relation's arguments supply.

The interpreted structure reads the table

Eleven definitional unfoldings: each relation of the interpreted structure is its formula at the tags of its arguments, and each formula was built to say what the table says. The only two rewrites are the two phases of a rule, which DescriptiveComplexity.Draw.Data.srcPhOf and dstPhOf name.

theorem DescriptiveComplexity.Draw.Data.relMap_le {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (x y : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMLe x y ↔ tagTupleLe x y

theorem DescriptiveComplexity.Draw.Data.relMap_tr {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (τ : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMTr τ ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.IsTr τ

theorem DescriptiveComplexity.Draw.Data.relMap_right {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (τ : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMRight τ ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.IsRight τ

theorem DescriptiveComplexity.Draw.Data.relMap_src {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (τ q : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMSrc τ q ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.Src τ q

theorem DescriptiveComplexity.Draw.Data.relMap_read {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (τ a : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMRead τ a ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.Read τ a

theorem DescriptiveComplexity.Draw.Data.relMap_dst {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (τ q : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMDst τ q ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.Dst τ q

theorem DescriptiveComplexity.Draw.Data.relMap_write {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (τ a : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMWrite τ a ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.Write τ a

theorem DescriptiveComplexity.Draw.Data.relMap_start {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (q : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMStart q ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.IsStart q

theorem DescriptiveComplexity.Draw.Data.relMap_blank {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (a : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMBlank a ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.IsBlank a

theorem DescriptiveComplexity.Draw.Data.relMap_acc {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (q : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMAcc q ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.IsAcc q

theorem DescriptiveComplexity.Draw.Data.relMap_inp {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) (x a : Univ e.α (RTagOf S Sh) P dt.KIx dt.dd) : WMInp x a ↔ (progFrom hpl e (rules e) p₀ (accept e) mk).table.Inp x a

theorem DescriptiveComplexity.Draw.Data.reads_progFrom {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] {S : Type} {Sh : S → Type} {P : Type} [LinearOrder (RTagOf S Sh)] [LinearOrder P] {rules : (e : Env L) → (i : S) → Sh i → Rule e.α dt.CtlIx dt.SlotIx P} {accept : (e : Env L) → P → (dt.CtlIx → e.α) → Prop} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (hdef : URulesDefinable rules) (hacc : ∀ (p : P), UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => accept e p f) (p₀ : P) (mk : dt.UMarkDef S Sh P) (e : Env L) [ws : FirstOrder.Language.wide.Structure (Univ e.α (RTagOf S Sh) P dt.KIx dt.dd)] (hws : ws = wideStr hpl hdef hacc p₀ mk e) : (progFrom hpl e (rules e) p₀ (accept e) mk).table.Reads

The interpreted structure reads the program's table: the eleven obligations of DescriptiveComplexity.Draw.Table.Reads, one per relation symbol. Everything the run layer proves is proved under exactly this.