The rule names of the EXPSPACE program are finitely many

DescriptiveComplexity.Problems.Wide.DrawTower gives every site type of the program's tower a Finite instance, and every leaf kit's rule type has one where it is defined; what was missing is the tower's shapes – the rules each site contributes – and hence the rule names themselves, which the run layer asks for as the hypothesis Finite (dt.RIx …) and which an interpretation needs of its tag type.

There is no mathematics here: a shape is a match on a site whose leaves are a kit's rules, a sum of them with a verdict, or the shape one level down, so each instance is one line per constructor. They are stated at the abstract machineries first (ChainSh, SeqSh, ElemSh, StageSh, TagSh, RoundSh, VarSh, EvalSh, OuterSh), then read up the concrete tower to DescriptiveComplexity.Draw.Data.SFSh, and the file ends at DescriptiveComplexity.Draw.Data.finite_RIx.

The branch rules of a tag dispatch

instance DescriptiveComplexity.Draw.instFiniteBrRule {T : Type} [Finite T] : Finite (BrRule T)

The shapes of the abstract machineries

instance DescriptiveComplexity.Draw.instFiniteTupleSh (c : TupleSS) : Finite (TupleSh c)

instance DescriptiveComplexity.Draw.instFiniteChainSh {n : ℕ} {SS : Type} {ShS : SS → Type} [∀ (s : SS), Finite (ShS s)] (c : ChainSite n SS) : Finite (ChainSh n SS ShS c)

instance DescriptiveComplexity.Draw.instFiniteElemSh {nr : ℕ} (c : ElemSite nr) : Finite (ElemSh nr c)

instance DescriptiveComplexity.Draw.instFiniteStageSh {k : ℕ} (c : StageSite k) : Finite (StageSh k c)

instance DescriptiveComplexity.Draw.instFiniteTagSh {m : ℕ} {T : Type} [Finite T] {nrOf : T → ℕ} (c : TagSite m T nrOf) : Finite (TagSh m T nrOf c)

instance DescriptiveComplexity.Draw.instFiniteSeqSh {n : ℕ} {SA : Fin n → Type} {ShA : (a : Fin n) → SA a → Type} [∀ (a : Fin n) (s : SA a), Finite (ShA a s)] (c : SeqSite n SA) : Finite (SeqSh n ShA c)

instance DescriptiveComplexity.Draw.instFiniteRoundSh {SG SX : Type} {ShG : SG → Type} {ShX : SX → Type} [∀ (s : SG), Finite (ShG s)] [∀ (s : SX), Finite (ShX s)] (c : RoundSite SG SX) : Finite (RoundSh SG SX ShG ShX c)

instance DescriptiveComplexity.Draw.instFiniteVarSh {SG SX B : Type} {ShG : SG → Type} {ShX : SX → Type} [∀ (s : SG), Finite (ShG s)] [∀ (s : SX), Finite (ShX s)] [Finite B] (c : VarSite SG SX) : Finite (VarSh SG SX ShG ShX B c)

instance DescriptiveComplexity.Draw.instFiniteEvalSh {nv : ℕ} {SM : Type} {ShM : SM → Type} [∀ (s : SM), Finite (ShM s)] (c : EvalSite nv SM) : Finite (EvalSh nv SM ShM c)

instance DescriptiveComplexity.Draw.instFiniteOuterSh {SE : Type} {ShE : SE → Type} [∀ (s : SE), Finite (ShE s)] (c : OuterSite SE) : Finite (OuterSh SE ShE c)

And of the concrete tower

instance DescriptiveComplexity.Draw.Data.instFiniteKindSh {L : FirstOrder.Language} (dt : Data L) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) (s : dt.KindSite κ) : Finite (dt.KindSh κ s)

instance DescriptiveComplexity.Draw.Data.instFiniteAtomSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) (s : dt.AtomSite v a) : Finite (dt.AtomSh v a s)

instance DescriptiveComplexity.Draw.Data.instFiniteGateBlockSh {L : FirstOrder.Language} (dt : Data L) (s : dt.GateBlockSite) : Finite (dt.GateBlockSh s)

instance DescriptiveComplexity.Draw.Data.instFiniteMatrixSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (s : dt.MatrixSite v) : Finite (dt.MatrixSh v s)

instance DescriptiveComplexity.Draw.Data.instFiniteGatesSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (s : dt.GatesSite v) : Finite (dt.GatesSh v s)

instance DescriptiveComplexity.Draw.Data.instFiniteIGatesSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (s : dt.IGatesSite v) : Finite (dt.IGatesSh v s)

instance DescriptiveComplexity.Draw.Data.instFiniteRoundShF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (s : dt.RoundSiteF v) : Finite (dt.RoundShF v s)

instance DescriptiveComplexity.Draw.Data.instFiniteVarShF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (s : dt.VarSiteF v) : Finite (dt.VarShF v s)

instance DescriptiveComplexity.Draw.Data.instFiniteSMSh {L : FirstOrder.Language} (dt : Data L) (s : dt.SMF) : Finite (dt.SMSh s)

instance DescriptiveComplexity.Draw.Data.instFiniteSESh {L : FirstOrder.Language} (dt : Data L) (s : dt.SEF) : Finite (dt.SESh s)

instance DescriptiveComplexity.Draw.Data.instFiniteSFSh {L : FirstOrder.Language} (dt : Data L) (s : dt.SF) : Finite (dt.SFSh s)

instance DescriptiveComplexity.Draw.Data.instFiniteNexEvalSh {nv : ℕ} {SM : Type} {ShM : SM → Type} [∀ (s : SM), Finite (ShM s)] (s : EvalSite nv SM) : Finite (NexEvalSh nv SM ShM s)

The rule shapes of the clocked evaluation are finite too: two rules at a checkpoint, the shared tower's at a machinery site.

instance DescriptiveComplexity.Draw.Data.instFiniteNexSESh {L : FirstOrder.Language} (dt : Data L) (s : dt.SEF) : Finite (dt.NexSESh s)

The rule names

instance DescriptiveComplexity.Draw.Data.finite_RIx {L : FirstOrder.Language} (dt : Data L) {A Q : Type} [Fintype Q] [Fintype dt.SlotIx] [LinearOrder A] {zero one : A} (hzo : zero ≠ one) (args : (v : dt.VarIx) → dt.VarArgs v) : Finite (dt.RIx zero one hzo args)

The rule names of the program are finitely many: a site and one of its rules, both of finitely many. This is the hypothesis the run layer carries and the finiteness an interpretation needs of its tag type.