Every leaf kit's rules are definable

The first floor of the discharge DescriptiveComplexity.Problems.Wide.DrawFactor sets up: each kit – the small, separately checkable composites the EXPSPACE program's rule set is a sum of – meets DescriptiveComplexity.Draw.URuleDefinable for every one of its rule families, given that its own abstract parameters do.

Two things make each proof a line: every kit's guard is a Boolean combination of the three atoms (a slot holds one, a slot holds zero, two slots hold the same element) with the kit's parameters, and every kit leaves its pointer alone, writing at most one track slot – DescriptiveComplexity.Draw.UTrDefinable.update with a designated element, a copy of another slot, or a bit whose question is the kit's parameter.

The kits are stated at a family of kits, one per environment: the slots, the phase embedding and the shape are the same at every instance – they are what an interpretation's tag decides – and only the parameters vary with it.

The named read and write trips

theorem DescriptiveComplexity.Draw.ReadKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {t wk : W} {emb : ReadPh → P} {M : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} (hM : UGDefinable M) (ρ : ReadRule) : URuleDefinable fun (e : Env L) => { t := t, wk := wk, Match := M e, emb := emb }.rule e.one ρ

A read trip's rules are definable, given its name guard: every shape's guard is one atom, or its negation, or the name guard, and nothing is written.

theorem DescriptiveComplexity.Draw.WriteKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t wk : W} {emb : WritePh → P} {M : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {bVal : (e : Env L) → (Q → e.α) → Prop} (hM : UGDefinable M) (hb : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => bVal e f) (ρ : WriteRule) : URuleDefinable fun (e : Env L) => { t := t, wk := wk, Match := M e, bVal := bVal e, emb := emb }.rule e.zero e.one ρ

A write trip's rules are definable, given its name guard and the question behind the bit it writes.

The register-file passes

theorem DescriptiveComplexity.Draw.TestKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {t rg rl wk : W} {emb : TestPh → P} {TestG : (e : Env L) → (W → e.α) → Prop} (hT : UGDefinable fun (e : Env L) (x : Q → e.α) (g : W → e.α) => TestG e g) (ρ : TestRule) : URuleDefinable fun (e : Env L) => { t := t, rg := rg, rl := rl, wk := wk, TestG := TestG e, emb := emb }.rule e.one ρ

A file test's rules are definable, given its per-register question.

theorem DescriptiveComplexity.Draw.ClearKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t rg rl wk : W} {emb : TrackPh → P} (ρ : TrackRule) : URuleDefinable fun (e : Env L) => { t := t, rg := rg, rl := rl, wk := wk, emb := emb }.rule e.zero e.one ρ

A track-clearing pass's rules are definable.

theorem DescriptiveComplexity.Draw.CopyKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t src rg rl wk : W} {emb : TrackPh → P} (ρ : TrackRule) : URuleDefinable fun (e : Env L) => { t := t, src := src, rg := rg, rl := rl, wk := wk, emb := emb }.rule e.one ρ

A track-copying pass's rules are definable.

theorem DescriptiveComplexity.Draw.MapKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t rg rl wk : W} {emb : TrackPh → P} {Fb : (e : Env L) → (W → e.α) → Prop} (hF : UGDefinable fun (e : Env L) (x : Q → e.α) (g : W → e.α) => Fb e g) (ρ : TrackRule) : URuleDefinable fun (e : Env L) => { t := t, rg := rg, rl := rl, wk := wk, Fb := Fb e, emb := emb }.rule e.zero e.one ρ

A track-mapping pass's rules are definable, given the question behind the bit it writes.

The three roaming passes

theorem DescriptiveComplexity.Draw.IncrKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {B : Type} [Finite B] {t rg rl wk : W} {bs : B → W} {emb : IncrPh B → P} (ρ : IncrRule B) : URuleDefinable fun (e : Env L) => { t := t, rg := rg, rl := rl, wk := wk, bs := bs, emb := emb }.rule e.zero e.one ρ

An increment's rules are definable: the one-hot clause of the setting rule is a conjunction over the block marks of an implication whose conclusion is decided when the formula is built.

theorem DescriptiveComplexity.Draw.SeekKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t tg rg rl wk : W} {emb : SeekPh → P} (ρ : SeekRule) : URuleDefinable fun (e : Env L) => { t := t, tg := tg, rg := rg, rl := rl, wk := wk, emb := emb }.rule e.zero e.one ρ

A seek's rules are definable: its comparison is an equivalence of two atoms.

theorem DescriptiveComplexity.Draw.AdvKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t rg rl wk : W} {emb : AdvPh → P} (ρ : AdvRule) : URuleDefinable fun (e : Env L) => { t := t, rg := rg, rl := rl, wk := wk, emb := emb }.rule e.zero e.one ρ

An advance's rules are definable.

The reset, the walk home and the two sweeps

theorem DescriptiveComplexity.Draw.ResetKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {t bt wk : W} {emb : ResetPh → P} (ρ : ResetRule) : URuleDefinable fun (e : Env L) => { t := t, bt := bt, wk := wk, emb := emb }.rule e.one ρ

A reset's rules are definable.

theorem DescriptiveComplexity.Draw.HomeKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {t wk : W} {ph : P} (ρ : HomeRule) : URuleDefinable fun (e : Env L) => { t := t, wk := wk, ph := ph }.rule e.one ρ

The walk home is definable.

theorem DescriptiveComplexity.Draw.FlagSweepKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {t ltp : W} {emb : SweepPh → P} {TestG : (e : Env L) → (W → e.α) → Prop} (hT : UGDefinable fun (e : Env L) (x : Q → e.α) (g : W → e.α) => TestG e g) (ρ : SweepRule) : URuleDefinable fun (e : Env L) => { t := t, ltp := ltp, TestG := TestG e, emb := emb }.rule e.one ρ

A flag sweep's rules are definable, given its per-cell question.

theorem DescriptiveComplexity.Draw.WriteSweepKit.uRuleDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {t ltp : W} {ph : P} {wrG : (e : Env L) → (W → e.α) → W → e.α} (hw : UTrDefinable fun (e : Env L) (x : Q → e.α) (g : W → e.α) => wrG e g) (ρ : WSweepRule) : URuleDefinable fun (e : Env L) => { t := t, ltp := ltp, wrG := fun (g : W → e.α) => wrG e g, ph := ph }.rule e.one ρ

A write sweep's rule is definable, given the rewrite it carries.