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

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.

The chain

The sequencer

The element loop

The tag-branched machinery

The tuple loop