The control's reads and writes are definable #
Everything the program keeps in its control is a bit – a flag, an
accumulator, a verdict – and every write of one is
DescriptiveComplexity.Draw.Data.putVec or its one-slot special case
setCtl: the named slots take the bits of a family, and every other slot rides
along. So one lemma per shape settles the whole control layer, given that the
questions behind the bits are definable.
Reading is the same statement one step simpler:
DescriptiveComplexity.Draw.Data.readVec is an existential over the levels of
a slot family, and ctlBit is a single atom.
Reading #
theorem
DescriptiveComplexity.Draw.Data.uGDefinable_readVec
{L : FirstOrder.Language}
{dt : Data L}
[Fintype dt.SlotIx]
{m : ℕ}
(accs : Fin m → dt.CtlIx)
(j : ℕ)
:
A vector of control slots, read at a level: one atom below the length, and nothing above it – a decision the formula is built with.