The two guards the program's own sites are written from, and the stage atom

Above the combinators the program stops being generic: its checkpoints are guarded by DescriptiveComplexity.Draw.Data.exitG – at the marker, which is nobody's register – and its trips are named by DescriptiveComplexity.Draw.Data.nameG – this cell is the canonically padded cell of the element whose block is b and whose first dd0 coordinates the control holds. Both are conjunctions of the three atoms, so both are definable once and for all, and with them the stage atom's machinery – the largest single subroutine of the program – follows kit by kit.

The naming guard is stated at an arbitrary coordinate function (DescriptiveComplexity.Draw.Data.nameGF), the caller owing the comparison g (name j) = cf f j rather than the value: the leaf reads of the element loops compute an encoded tuple there, and what they owe is the same shape as what the coordinate loops owe.

The two guards

theorem DescriptiveComplexity.Draw.Data.uGDefinable_exitG {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => dt.exitG e.one g

The standard exit guard is definable: at the marker, which is nobody's register.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_nameGF {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {b : Fin dt.ko ⊕ Fin dt.ki} {cf : (e : Env L) → (Q → e.α) → Fin dt.dd0 → e.α} (hcf : ∀ (j : Fin dt.dd0), UGDefinable fun (e : Env L) (f : Q → e.α) (g : dt.SlotIx → e.α) => g (Slot.name j) = cf e f j) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : dt.SlotIx → e.α) => dt.nameGF e.one b (cf e) f g

A naming guard is definable, given that each of its coordinates is compared definably: the block flag and the padding flag are atoms, and the comparison is the caller's.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_nameG {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (b : Fin dt.ko ⊕ Fin dt.ki) (coord : Fin dt.dd0 → Q) : UGDefinable fun (e : Env L) (f : Q → e.α) (g : dt.SlotIx → e.α) => dt.nameG e.one b coord f g

The naming guard of a coordinate loop is definable: its coordinates are control slots, so each comparison is one atom.

The stage atom

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_stageRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {k : ℕ} {emb : StagePh k → P} {srcTrack : Fin k → dt.SlotIx} {srcBlk dstBlk : Fin k → Fin dt.ko ⊕ Fin dt.ki} {coord : Fin dt.dd0 → Q} {bitFlag : (e : Env L) → (Q → e.α) → Prop} {setBit : (e : Env L) → Bool → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {initLv advLv : (e : Env L) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {IsMaxLv : (e : Env L) → (Q → e.α) → Prop} {oldSlot : dt.SlotIx} {setAv : (e : Env L) → Bool → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {exitPh : P} (hbit : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → 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 : dt.SlotIx → e.α) => IsMaxLv e f) (hav : ∀ (b : Bool), UStDefinable fun (e : Env L) => setAv e b) : URulesDefinable fun (e : Env L) => dt.stageRule e.zero e.one emb srcTrack srcBlk dstBlk coord (bitFlag e) (setBit e) (initLv e) (advLv e) (IsMaxLv e) oldSlot (setAv e) exitPh

A stage atom's machinery is definable: eleven kits and their exit rules, the exits all guarded by the standard one, plus the argument tuple loops, whose two naming guards are the coordinate loops'.