The loop variables are definable: the one write that is not a copy

Everything the EXPSPACE program writes is a copy of one of its slots or one of the two designated elements – except the loop advance. A loop element is a tuple over the instance, and advancing it is DescriptiveComplexity.Draw.tupNext, the lexicographic successor: the coordinates below the one that rolls over keep their value, the one that rolls over takes the next element of the order, and the ones above it reset.

Two things make that definable all the same.

• Which coordinate rolls over is decided by which coordinates are maximal, and that is in the equality pattern – so the case split is read off the pattern (DescriptiveComplexity.Draw.uSlotDefinable_cases).
• The value at the carry is DescriptiveComplexity.ordSucc of a single coordinate, which is exactly the source DescriptiveComplexity.SlotVal.succ names.

DescriptiveComplexity.Draw.tupNext_apply_of_carry is the coordinatewise reading of tupNext, and the three statements after it are what a variable's pack owes for its loop: the loop started, the loop advanced, and the loop exhausted – at both widths.

tupNext, coordinate by coordinate

theorem DescriptiveComplexity.Draw.tupNext_apply_of_carry {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {zero : A} (hb : IsBot zero) {t : Fin D → A} {p : Fin D} (hp : ¬IsTop (t p)) (hab : ∀ (j : Fin D), p < j → IsTop (t j)) (j : Fin D) : tupNext t j = if j < p then t j else if j = p then ordSucc (t j) else zero

The next tuple, coordinate by coordinate: below the carry a copy, at the carry the next element, above it the least one. This is the reading the interpretation writes down.

The three obligations of a loop element

The narrow width