The combinators carry definability up the tower

DescriptiveComplexity.Problems.Wide.DrawDefKit discharges the leaves; this file carries DescriptiveComplexity.Draw.URuleDefinable through the combinators the EXPSPACE program is assembled by – the chain, the sequencer, the element loop, the tag-branched machinery and the tuple loop.

Each combinator contributes only checkpoints, and a checkpoint's rule has the same three shapes everywhere: a walk back to the marker (stay), and one or two dispatches, whose guards are the standard exit guard conjoined with a question the caller supplies and whose destination pointers are the caller's control updates. So each proof is: the leaves by DescriptiveComplexity.Problems.Wide.DrawDefKit, the checkpoints by the atoms, and nothing else.

A rule may be transported along an equality of families

theorem DescriptiveComplexity.Draw.URuleDefinable.congr {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {rl rl' : (e : Env L) → Rule e.α Q W P} (h : URuleDefinable rl) (he : ∀ (e : Env L), rl' e = rl e) : URuleDefinable rl'

A rule without its source phase

structure DescriptiveComplexity.Draw.UPreDefinable {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] (pr : (e : Env L) → PreRule e.α Q W P) : Prop

A dispatch descriptor is definable: the same three obligations, its source phase being the checkpoint's.

• dstPh : ∃ (p : P), ∀ (e : Env L), (pr e).dstPh = p

  The phase it moves to is the same at every instance.

• right : ∃ (b : Bool), ∀ (e : Env L), (pr e).moveRight ↔ b = true

  And so is its direction.

• guard : UGDefinable fun (e : Env L) => (pr e).guard

  Its guard reads its data only through the equality pattern.

• dst : UStDefinable fun (e : Env L) => (pr e).dstSt

  The pointer it leaves is definable slot by slot.

• wr : UTrDefinable fun (e : Env L) => (pr e).wr

  And so are the tracks it writes.

theorem DescriptiveComplexity.Draw.UPreDefinable.toRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {pr : (e : Env L) → PreRule e.α Q W P} (h : UPreDefinable pr) (p : P) : URuleDefinable fun (e : Env L) => (pr e).toRule p

A descriptor at a source phase is a definable rule.

theorem DescriptiveComplexity.Draw.uPreDefinable_dsp {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {wk rg : W} {p : P} {b : Bool} {N : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {F : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} (hN : UGDefinable N) (hF : UStDefinable F) : UPreDefinable fun (e : Env L) => { guard := fun (f : Q → e.α) (g : W → e.α) => (g wk = e.one ∧ g rg ≠ e.one) ∧ N e f g, dstPh := p, dstSt := F e, wr := fun (x : Q → e.α) (g : W → e.α) => g, moveRight := b = true }

The dispatch shape of every checkpoint: the standard exit guard, conjoined with a question the caller supplies, a control update and the tracks riding along.

The chain

theorem DescriptiveComplexity.Draw.uRulesDefinable_chainRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {PS SS : Type} {n : ℕ} {ShS : SS → Type} {wk : W} {emb : ChainPh n PS → P} {ruleS : (e : Env L) → (s : SS) → ShS s → Rule e.α Q W P} {dsp : (e : Env L) → Fin n → Bool → PreRule e.α Q W P} (hS : URulesDefinable ruleS) (hdsp : ∀ (k : Fin n) (b : Bool), UPreDefinable fun (e : Env L) => dsp e k b) : URulesDefinable fun (e : Env L) => chainRule e.one wk emb (ruleS e) (dsp e)

A chain's rules are definable: its stages' are the parameter, and each checkpoint contributes the walk back and its two descriptors.

The sequencer

theorem DescriptiveComplexity.Draw.uRulesDefinable_seqRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {n : ℕ} {PA SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} {wk rg : W} {emb : SeqPh n PA → P} {ruleA : (e : Env L) → (a : Fin n) → (s : SA a) → ShA a s → Rule e.α Q W P} {entry : (a : Fin n) → PA a} {enterSt : (e : Env L) → Fin n → (Q → e.α) → (W → e.α) → Q → e.α} {exitPh : P} (hA : ∀ (a : Fin n) (s : SA a) (ρ : ShA a s), URuleDefinable fun (e : Env L) => ruleA e a s ρ) (hen : ∀ (a : Fin n), UStDefinable fun (e : Env L) => enterSt e a) : URulesDefinable fun (e : Env L) => seqRule e.one wk rg emb (ruleA e) entry (enterSt e) exitPh

A sequencer's rules are definable: its stages' are the parameter, its dispatch enters the next stage with the caller's control update or leaves after the last, and the second descriptor is dead.

The element loop

theorem DescriptiveComplexity.Draw.uRulesDefinable_elemRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {nr : ℕ} {wk rg : W} {emb : ElemPh nr → P} {rdTrack : Fin nr → W} {MatchOf : Fin nr → (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {setFlag : (e : Env L) → Fin nr → Bool → (Q → e.α) → (W → e.α) → Q → e.α} {initEl advEl exitSt : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} {IsMaxEl : (e : Env L) → (Q → e.α) → Prop} {exitPh : P} (hM : ∀ (j : Fin nr), UGDefinable (MatchOf j)) (hset : ∀ (j : Fin nr) (b : Bool), UStDefinable fun (e : Env L) => setFlag e j b) (hinit : UStDefinable initEl) (hadv : UStDefinable advEl) (hexit : UStDefinable exitSt) (hmax : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => IsMaxEl e f) : URulesDefinable fun (e : Env L) => elemRule e.one wk rg emb rdTrack (fun (j : Fin nr) => MatchOf j e) (setFlag e) (initEl e) (advEl e) (exitSt e) (IsMaxEl e) exitPh

An element loop's rules are definable: the read trips by DescriptiveComplexity.Draw.ReadKit.uRuleDefinable, and the three checkpoints – the entry, each read's verdict exit and the fold – by the dispatch shape.

The tag-branched machinery

theorem DescriptiveComplexity.Draw.uRulesDefinable_tagRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {T : Type} {m : ℕ} {nrOf : T → ℕ} {wk rg : W} {emb : TagPh m T nrOf → P} {rdTrackT : Fin m → W} {MatchT : Fin m → (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {setTagFlag : (e : Env L) → Fin m → Bool → (Q → e.α) → (W → e.α) → Q → e.α} {TagsAre : (e : Env L) → T → (Q → e.α) → Prop} {rdTrackE : (τ : T) → Fin (nrOf τ) → W} {MatchE : (τ : T) → Fin (nrOf τ) → (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {setFlagE : (e : Env L) → (τ : T) → Fin (nrOf τ) → Bool → (Q → e.α) → (W → e.α) → Q → e.α} {initEl advEl exitSt : (e : Env L) → T → (Q → e.α) → (W → e.α) → Q → e.α} {IsMaxEl : (e : Env L) → T → (Q → e.α) → Prop} {exitPh : P} (hMT : ∀ (i : Fin m), UGDefinable (MatchT i)) (hsetT : ∀ (i : Fin m) (b : Bool), UStDefinable fun (e : Env L) => setTagFlag e i b) (hTags : ∀ (τ : T), UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => TagsAre e τ f) (hME : ∀ (τ : T) (j : Fin (nrOf τ)), UGDefinable (MatchE τ j)) (hsetE : ∀ (τ : T) (j : Fin (nrOf τ)) (b : Bool), UStDefinable fun (e : Env L) => setFlagE e τ j b) (hinit : ∀ (τ : T), UStDefinable fun (e : Env L) => initEl e τ) (hadv : ∀ (τ : T), UStDefinable fun (e : Env L) => advEl e τ) (hexit : ∀ (τ : T), UStDefinable fun (e : Env L) => exitSt e τ) (hmax : ∀ (τ : T), UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => IsMaxEl e τ f) : URulesDefinable fun (e : Env L) => tagRule e.one wk rg emb rdTrackT (fun (i : Fin m) => MatchT i e) (setTagFlag e) (TagsAre e) rdTrackE (fun (τ : T) (j : Fin (nrOf τ)) => MatchE τ j e) (setFlagE e) (initEl e) (advEl e) (exitSt e) (IsMaxEl e) exitPh

A tag-branched machinery's rules are definable: the witness reads by the read kit, the branch checkpoint by the dispatch shape – one dispatch per tag, each guarded by the caller's decoding question – and the loops by DescriptiveComplexity.Draw.uRulesDefinable_elemRule.

The tuple loop

theorem DescriptiveComplexity.Draw.uRulesDefinable_tupleStageRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {wk rg tSrc tDst : W} {emb : ChainPh 3 TuplePS → P} {MatchS MatchD : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {bitFlag : (e : Env L) → (Q → e.α) → Prop} {setBit : (e : Env L) → Bool → (Q → e.α) → (W → e.α) → Q → e.α} (hS : UGDefinable MatchS) (hD : UGDefinable MatchD) (hbit : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => bitFlag e f) (hset : ∀ (b : Bool), UStDefinable fun (e : Env L) => setBit e b) : URulesDefinable fun (e : Env L) => tupleStageRule e.zero e.one wk rg emb tSrc tDst (MatchS e) (MatchD e) (bitFlag e) (setBit e)

A tuple loop's stages are definable: the read trip storing its bit and the write trip handing it back.

theorem DescriptiveComplexity.Draw.uPreDefinable_tupleDsp {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {wk rg : W} {emb : ChainPh 3 TuplePS → P} {initLv advLv : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} {IsMaxLv : (e : Env L) → (Q → e.α) → Prop} {exitPh : P} (hinit : UStDefinable initLv) (hadv : UStDefinable advLv) (hmax : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => IsMaxLv e f) (k : Fin 3) (b : Bool) : UPreDefinable fun (e : Env L) => tupleDsp e.one wk rg emb (initLv e) (advLv e) (IsMaxLv e) exitPh k b

A tuple loop's dispatch descriptors are definable: begin, hand over, advance or leave.

theorem DescriptiveComplexity.Draw.uRulesDefinable_tupleRule {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] [DecidableEq W] {wk rg tSrc tDst : W} {emb : ChainPh 3 TuplePS → P} {MatchS MatchD : (e : Env L) → (Q → e.α) → (W → e.α) → Prop} {bitFlag : (e : Env L) → (Q → e.α) → Prop} {setBit : (e : Env L) → Bool → (Q → e.α) → (W → e.α) → Q → e.α} {initLv advLv : (e : Env L) → (Q → e.α) → (W → e.α) → Q → e.α} {IsMaxLv : (e : Env L) → (Q → e.α) → Prop} {exitPh : P} (hS : UGDefinable MatchS) (hD : UGDefinable MatchD) (hbit : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => bitFlag e f) (hset : ∀ (b : Bool), UStDefinable fun (e : Env L) => setBit e b) (hinit : UStDefinable initLv) (hadv : UStDefinable advLv) (hmax : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => IsMaxLv e f) : URulesDefinable fun (e : Env L) => tupleRule e.zero e.one wk rg emb tSrc tDst (MatchS e) (MatchD e) (bitFlag e) (setBit e) (initLv e) (advLv e) (IsMaxLv e) exitPh

A tuple loop's rules are definable, the chain over its two stages.