The phase tower: the program's phase and site types, assembled

The full program's phase type, from the leaves up: per classified atom its machinery's phases – a stage atom's random access, an expansion atom's tag-branched loops, a comparison's coordinate loop – then the matrix as a sequence over the atoms, the gates as a sequence over the argument blocks, one variable's machinery around them, the evaluation's spine over the variable list, and the outer program around everything.

The kind-dependent types are indexed by the kind itself (DescriptiveComplexity.Draw.Data.KindPh and friends match on a DescriptiveComplexity.Draw.MatAtom), so every downstream definition reduces per constructor; the stuck DescriptiveComplexity.Draw.Data.kindOf application appears only at the instantiation (DescriptiveComplexity.Draw.Data.AtomPh etc.).

The element loops of an atom run one read trip per atom of the defining matrix – the guard atoms' trips read a harmless witness cell and their flags are ignored by the folds – so the loop lengths match the DescriptiveComplexity.Draw.Data.kindReads budgets exactly.

The per-kind machinery types

noncomputable def DescriptiveComplexity.Draw.Data.relNr {L : FirstOrder.Language} (dt : Data L) {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) : ℕ

The loop count of an expansion atom's branch: one read per block atom of the defining matrix – the base-vocabulary atoms are guards and need no trip.

Equations

• dt.relNr e τ = (DescriptiveComplexity.Draw.blkAtoms (dt.relPk e τ).mat).length

noncomputable def DescriptiveComplexity.Draw.Data.domNr {L : FirstOrder.Language} (dt : Data L) (t : dt.X.Tag) : ℕ

The loop count of a domain branch.

Equations

• dt.domNr t = (DescriptiveComplexity.Draw.blkAtoms (dt.domPk t).mat).length

noncomputable def DescriptiveComplexity.Draw.Data.KindPh {L : FirstOrder.Language} (dt : Data L) {n : ℕ} : MatAtom dt.X dt.d.B n → Type

The machinery phases of an atom kind: a stage atom's random access, an expansion atom's tag-branched loops, a comparison's coordinate loop.

Equations

• dt.KindPh (DescriptiveComplexity.Draw.MatAtom.stage i a) = DescriptiveComplexity.Draw.StagePh (dt.d.B.arity i)
• dt.KindPh (DescriptiveComplexity.Draw.MatAtom.exp e a) = DescriptiveComplexity.Draw.TagPh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)
• dt.KindPh (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = DescriptiveComplexity.Draw.ElemPh 2
• dt.KindPh (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = DescriptiveComplexity.Draw.ElemPh 2

noncomputable def DescriptiveComplexity.Draw.Data.KindSite {L : FirstOrder.Language} (dt : Data L) {n : ℕ} : MatAtom dt.X dt.d.B n → Type

The machinery sites of an atom kind.

Equations

• dt.KindSite (DescriptiveComplexity.Draw.MatAtom.stage i a) = DescriptiveComplexity.Draw.StageSite (dt.d.B.arity i)
• dt.KindSite (DescriptiveComplexity.Draw.MatAtom.exp e a) = DescriptiveComplexity.Draw.TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)
• dt.KindSite (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = DescriptiveComplexity.Draw.ElemSite 2
• dt.KindSite (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = DescriptiveComplexity.Draw.ElemSite 2

noncomputable def DescriptiveComplexity.Draw.Data.KindSh {L : FirstOrder.Language} (dt : Data L) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) : dt.KindSite κ → Type

The rule shape of an atom kind's sites.

Equations

• dt.KindSh (DescriptiveComplexity.Draw.MatAtom.stage i a) = DescriptiveComplexity.Draw.StageSh (dt.d.B.arity i)
• dt.KindSh (DescriptiveComplexity.Draw.MatAtom.exp e a) = DescriptiveComplexity.Draw.TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)
• dt.KindSh (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = DescriptiveComplexity.Draw.ElemSh 2
• dt.KindSh (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = DescriptiveComplexity.Draw.ElemSh 2

The tower

noncomputable def DescriptiveComplexity.Draw.Data.AtomPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : Type

The machinery phases of the a-th atom of a variable's matrix.

Equations

• dt.AtomPh v a = dt.KindPh (dt.kindOf v a)

noncomputable def DescriptiveComplexity.Draw.Data.AtomSite {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : Type

The machinery sites of the a-th atom.

Equations

• dt.AtomSite v a = dt.KindSite (dt.kindOf v a)

noncomputable def DescriptiveComplexity.Draw.Data.AtomSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : dt.AtomSite v a → Type

The rule shapes of the a-th atom's sites.

Equations

• dt.AtomSh v a = dt.KindSh (dt.kindOf v a)

noncomputable def DescriptiveComplexity.Draw.Data.MatrixPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

The matrix's phases: the sequence over the classified atoms.

Equations

• dt.MatrixPh v = DescriptiveComplexity.Draw.SeqPh (dt.natOf v) (dt.AtomPh v)

noncomputable def DescriptiveComplexity.Draw.Data.MatrixSite {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

The matrix's sites.

Equations

• dt.MatrixSite v = DescriptiveComplexity.Draw.SeqSite (dt.natOf v) (dt.AtomSite v)

noncomputable def DescriptiveComplexity.Draw.Data.GateBlockPh {L : FirstOrder.Language} (dt : Data L) : Type

One gate block's phases: the well-shapedness file test, and the tag-branched domain evaluation.

Equations

• dt.GateBlockPh = (DescriptiveComplexity.Draw.TestPh ⊕ DescriptiveComplexity.Draw.TagPh (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr)

noncomputable def DescriptiveComplexity.Draw.Data.GateBlockSite {L : FirstOrder.Language} (dt : Data L) : Type

One gate block's sites: the file test's, and the domain evaluation's.

Equations

• dt.GateBlockSite = (Unit ⊕ DescriptiveComplexity.Draw.TagSite (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr)

noncomputable def DescriptiveComplexity.Draw.Data.GateBlockSh {L : FirstOrder.Language} (dt : Data L) : dt.GateBlockSite → Type

The rule shape of a gate block's sites.

Equations

• dt.GateBlockSh (Sum.inl val) = (DescriptiveComplexity.Draw.TestRule ⊕ Bool)
• dt.GateBlockSh (Sum.inr s) = DescriptiveComplexity.Draw.TagSh (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr s

noncomputable def DescriptiveComplexity.Draw.Data.GatesPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

The gates' phases: the sequence over the argument blocks.

Equations

• dt.GatesPh v = DescriptiveComplexity.Draw.SeqPh (dt.arOf v) fun (x : Fin (dt.arOf v)) => dt.GateBlockPh

noncomputable def DescriptiveComplexity.Draw.Data.GatesSite {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

The gates' sites.

Equations

• dt.GatesSite v = DescriptiveComplexity.Draw.SeqSite (dt.arOf v) fun (x : Fin (dt.arOf v)) => dt.GateBlockSite

noncomputable def DescriptiveComplexity.Draw.Data.nIn {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : ℕ

The number of quantified levels of a variable's pack.

Equations

• dt.nIn v = dt.nOf v - dt.arOf v

noncomputable def DescriptiveComplexity.Draw.Data.IGatesPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

The inner gates' phases: one gate block per quantified level of the variable's pack, at the VAL register's blocks.

Equations

• dt.IGatesPh v = DescriptiveComplexity.Draw.SeqPh (dt.nIn v) fun (x : Fin (dt.nIn v)) => dt.GateBlockPh

noncomputable def DescriptiveComplexity.Draw.Data.IGatesSite {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

The inner gates' sites.

Equations

• dt.IGatesSite v = DescriptiveComplexity.Draw.SeqSite (dt.nIn v) fun (x : Fin (dt.nIn v)) => dt.GateBlockSite

noncomputable def DescriptiveComplexity.Draw.Data.RoundPhF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

One round's machinery phases: the inner gates, the branch, and the matrix.

Equations

• dt.RoundPhF v = DescriptiveComplexity.Draw.RoundPh (dt.IGatesPh v) (dt.MatrixPh v)

noncomputable def DescriptiveComplexity.Draw.Data.VarPhF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

One variable's machinery phases, gates and round plugged in.

Equations

• dt.VarPhF v = DescriptiveComplexity.Draw.VarPh dt.CarryB (dt.GatesPh v) (dt.RoundPhF v)

noncomputable def DescriptiveComplexity.Draw.Data.varList {L : FirstOrder.Language} (dt : Data L) : List dt.d.B.ι

The enumeration of the fixed-point variables.

Equations

• dt.varList = Finset.univ.toList

noncomputable def DescriptiveComplexity.Draw.Data.nv {L : FirstOrder.Language} (dt : Data L) : ℕ

The number of fixed-point variables.

Equations

• dt.nv = dt.varList.length

noncomputable def DescriptiveComplexity.Draw.Data.varAt {L : FirstOrder.Language} (dt : Data L) (j : Fin dt.nv) : dt.VarIx

The variable at a spine position.

Equations

• dt.varAt j = some (dt.varList.get j)

noncomputable def DescriptiveComplexity.Draw.Data.PMF {L : FirstOrder.Language} (dt : Data L) : Type

The evaluation's machinery phases: one copy of the variable machinery per spine position, and the output's.

Equations

• dt.PMF = ((j : Fin dt.nv) × dt.VarPhF (dt.varAt j) ⊕ dt.VarPhF none)

@[reducible]

noncomputable def DescriptiveComplexity.Draw.Data.PEF {L : FirstOrder.Language} (dt : Data L) : Type

The evaluation's phases: the spine over the machineries.

Equations

• dt.PEF = DescriptiveComplexity.Draw.EvalPh dt.nv dt.PMF

@[reducible]

noncomputable def DescriptiveComplexity.Draw.Data.PF {L : FirstOrder.Language} (dt : Data L) : Type

The program's phases.

Equations

• dt.PF = DescriptiveComplexity.Draw.OuterPh dt.PEF

The site tower

noncomputable def DescriptiveComplexity.Draw.Data.MatrixSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.MatrixSite v → Type

The rule shape of the matrix's sites.

Equations

• dt.MatrixSh v = DescriptiveComplexity.Draw.SeqSh (dt.natOf v) (dt.AtomSh v)

noncomputable def DescriptiveComplexity.Draw.Data.GatesSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.GatesSite v → Type

The rule shape of the gates' sites.

Equations

• dt.GatesSh v = DescriptiveComplexity.Draw.SeqSh (dt.arOf v) fun (x : Fin (dt.arOf v)) => dt.GateBlockSh

noncomputable def DescriptiveComplexity.Draw.Data.IGatesSh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.IGatesSite v → Type

The rule shape of the inner gates' sites.

Equations

• dt.IGatesSh v = DescriptiveComplexity.Draw.SeqSh (dt.nIn v) fun (x : Fin (dt.nIn v)) => dt.GateBlockSh

noncomputable def DescriptiveComplexity.Draw.Data.RoundSiteF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

One round's machinery sites.

Equations

• dt.RoundSiteF v = DescriptiveComplexity.Draw.RoundSite (dt.IGatesSite v) (dt.MatrixSite v)

noncomputable def DescriptiveComplexity.Draw.Data.RoundShF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.RoundSiteF v → Type

The rule shape of one round's machinery sites.

Equations

• dt.RoundShF v = DescriptiveComplexity.Draw.RoundSh (dt.IGatesSite v) (dt.MatrixSite v) (dt.IGatesSh v) (dt.MatrixSh v)

noncomputable def DescriptiveComplexity.Draw.Data.VarSiteF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Type

One variable's machinery sites.

Equations

• dt.VarSiteF v = DescriptiveComplexity.Draw.VarSite (dt.GatesSite v) (dt.RoundSiteF v)

noncomputable def DescriptiveComplexity.Draw.Data.VarShF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.VarSiteF v → Type

The rule shape of one variable's machinery sites.

Equations

• dt.VarShF v = DescriptiveComplexity.Draw.VarSh (dt.GatesSite v) (dt.RoundSiteF v) (dt.GatesSh v) (dt.RoundShF v) dt.CarryB

noncomputable def DescriptiveComplexity.Draw.Data.SMF {L : FirstOrder.Language} (dt : Data L) : Type

The evaluation's machinery sites.

Equations

• dt.SMF = ((j : Fin dt.nv) × dt.VarSiteF (dt.varAt j) ⊕ dt.VarSiteF none)

noncomputable def DescriptiveComplexity.Draw.Data.SMSh {L : FirstOrder.Language} (dt : Data L) : dt.SMF → Type

The rule shape of the evaluation's machinery sites.

Equations

• dt.SMSh (Sum.inl ⟨j, s⟩) = dt.VarShF (dt.varAt j) s
• dt.SMSh (Sum.inr s) = dt.VarShF none s

noncomputable def DescriptiveComplexity.Draw.Data.SEF {L : FirstOrder.Language} (dt : Data L) : Type

The evaluation's sites.

Equations

• dt.SEF = DescriptiveComplexity.Draw.EvalSite dt.nv dt.SMF

noncomputable def DescriptiveComplexity.Draw.Data.SESh {L : FirstOrder.Language} (dt : Data L) : dt.SEF → Type

The rule shape of the evaluation's sites.

Equations

• dt.SESh = DescriptiveComplexity.Draw.EvalSh dt.nv dt.SMF dt.SMSh

noncomputable def DescriptiveComplexity.Draw.Data.SF {L : FirstOrder.Language} (dt : Data L) : Type

The program's sites.

Equations

• dt.SF = DescriptiveComplexity.Draw.OuterSite dt.SEF

noncomputable def DescriptiveComplexity.Draw.Data.SFSh {L : FirstOrder.Language} (dt : Data L) : dt.SF → Type

The rule shape of the program's sites.

Equations

• dt.SFSh = DescriptiveComplexity.Draw.OuterSh dt.SEF dt.SESh

The owner maps of the tower

Each machinery's phases are owned by its sites – the per-shape maps live with their rules (DescriptiveComplexity.Draw.elemOwn and friends); the maps below compose them up the tower.

noncomputable def DescriptiveComplexity.Draw.Data.kindOwn {L : FirstOrder.Language} (dt : Data L) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) : dt.KindPh κ → dt.KindSite κ

The owner map of an atom kind's machinery.

Equations

• dt.kindOwn (DescriptiveComplexity.Draw.MatAtom.stage i a) = DescriptiveComplexity.Draw.stageOwn
• dt.kindOwn (DescriptiveComplexity.Draw.MatAtom.exp e a) = DescriptiveComplexity.Draw.tagOwn
• dt.kindOwn (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = DescriptiveComplexity.Draw.elemOwn
• dt.kindOwn (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = DescriptiveComplexity.Draw.elemOwn

noncomputable def DescriptiveComplexity.Draw.Data.gateBlockOwn {L : FirstOrder.Language} (dt : Data L) : dt.GateBlockPh → dt.GateBlockSite

The owner map of a gate block.

Equations

• dt.gateBlockOwn (Sum.inl val) = Sum.inl ()
• dt.gateBlockOwn (Sum.inr p) = Sum.inr (DescriptiveComplexity.Draw.tagOwn p)

noncomputable def DescriptiveComplexity.Draw.Data.roundOwnF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.RoundPhF v → dt.RoundSiteF v

The owner map of one round's machinery.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.varOwnF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : dt.VarPhF v → dt.VarSiteF v

The owner map of one variable's machinery.

Equations

• dt.varOwnF v = DescriptiveComplexity.Draw.varOwn (DescriptiveComplexity.Draw.seqOwn fun (x : Fin (dt.arOf v)) => dt.gateBlockOwn) (dt.roundOwnF v)

noncomputable def DescriptiveComplexity.Draw.Data.smOwn {L : FirstOrder.Language} (dt : Data L) : dt.PMF → dt.SMF

The owner map of the evaluation's machineries.

Equations

• dt.smOwn (Sum.inl ⟨j, p⟩) = Sum.inl ⟨j, dt.varOwnF (dt.varAt j) p⟩
• dt.smOwn (Sum.inr p) = Sum.inr (dt.varOwnF none p)

noncomputable def DescriptiveComplexity.Draw.Data.seOwn {L : FirstOrder.Language} (dt : Data L) : dt.PEF → dt.SEF

The owner map of the evaluation's phases.

Equations

• dt.seOwn = DescriptiveComplexity.Draw.Data.evalOwn dt.smOwn

noncomputable def DescriptiveComplexity.Draw.Data.sfOwn {L : FirstOrder.Language} (dt : Data L) : dt.PF → dt.SF

The owner map of the program's phases.

Equations

• dt.sfOwn = DescriptiveComplexity.Draw.Data.outerOwner dt.seOwn

Finiteness, up the tower

The machine's universe carries the phases (and the rule names) as tags, so every type of the tower is finite; the instances go by injection into sums of the components'.

instance DescriptiveComplexity.Draw.instFiniteChainSite {n : ℕ} {SS : Type} [Finite SS] : Finite (ChainSite n SS)

instance DescriptiveComplexity.Draw.instFiniteStagePh {k : ℕ} : Finite (StagePh k)

instance DescriptiveComplexity.Draw.instFiniteStageSite {k : ℕ} : Finite (StageSite k)

instance DescriptiveComplexity.Draw.instFiniteElemPh {nr : ℕ} : Finite (ElemPh nr)

instance DescriptiveComplexity.Draw.instFiniteElemSite {nr : ℕ} : Finite (ElemSite nr)

instance DescriptiveComplexity.Draw.instFiniteTagPh {m : ℕ} {T : Type} [Finite T] {nrOf : T → ℕ} : Finite (TagPh m T nrOf)

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

instance DescriptiveComplexity.Draw.instFiniteSeqPh {n : ℕ} {PA : Fin n → Type} [∀ (a : Fin n), Finite (PA a)] : Finite (SeqPh n PA)

instance DescriptiveComplexity.Draw.instFiniteSeqSite {n : ℕ} {SA : Fin n → Type} [∀ (a : Fin n), Finite (SA a)] : Finite (SeqSite n SA)

instance DescriptiveComplexity.Draw.instFiniteVarPh {B PG PX : Type} [Finite B] [Finite PG] [Finite PX] : Finite (VarPh B PG PX)

instance DescriptiveComplexity.Draw.instFiniteVarSite {SG SX : Type} [Finite SG] [Finite SX] : Finite (VarSite SG SX)

instance DescriptiveComplexity.Draw.instFiniteEvalSite {nv : ℕ} {SM : Type} [Finite SM] : Finite (EvalSite nv SM)

instance DescriptiveComplexity.Draw.instFiniteOuterSite {SE : Type} [Finite SE] : Finite (OuterSite SE)

instance DescriptiveComplexity.Draw.Data.instFiniteKindPh {L : FirstOrder.Language} (dt : Data L) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) : Finite (dt.KindPh κ)

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

instance DescriptiveComplexity.Draw.Data.instFiniteAtomPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (a : Fin (dt.natOf v)) : Finite (dt.AtomPh v a)

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

instance DescriptiveComplexity.Draw.Data.instFiniteMatrixPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Finite (dt.MatrixPh v)

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

instance DescriptiveComplexity.Draw.Data.instFiniteGateBlockPh {L : FirstOrder.Language} (dt : Data L) : Finite dt.GateBlockPh

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

instance DescriptiveComplexity.Draw.Data.instFiniteGatesPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Finite (dt.GatesPh v)

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

instance DescriptiveComplexity.Draw.Data.instFiniteIGatesPh {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Finite (dt.IGatesPh v)

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

instance DescriptiveComplexity.Draw.Data.instFiniteRoundPhF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Finite (dt.RoundPhF v)

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

instance DescriptiveComplexity.Draw.Data.instFiniteVarPhF {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) : Finite (dt.VarPhF v)

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

instance DescriptiveComplexity.Draw.Data.instFinitePMF {L : FirstOrder.Language} (dt : Data L) : Finite dt.PMF

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

instance DescriptiveComplexity.Draw.Data.instFinitePEF {L : FirstOrder.Language} (dt : Data L) : Finite dt.PEF

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

instance DescriptiveComplexity.Draw.Data.instFinitePF {L : FirstOrder.Language} (dt : Data L) : Finite dt.PF

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