The geometry of the QBF machine's tape #
Where the cells sit: which tagged tuples are positions, which is the lowest and which the highest, and what the immediate neighbor of each one is. Everything the run needs to know about movement, proved once, before any transition is taken.
The content is that the tape
⊢ v₁ v₂ … vₙ ⊣
is exactly the position order DescriptiveComplexity.QsatTM.QLe: the left marker
is DescriptiveComplexity.MinPos, the right marker is DescriptiveComplexity.MaxPos,
and DescriptiveComplexity.SuccPos steps from the left marker to the outermost
variable, from a variable to the next one the prefix binds, and from the
innermost variable to the right marker. The degenerate instance – no quantified
variable at all – is the case where the two markers are neighbors.
All of it needs the instance to be well formed, since that is exactly when the
prefix order is a linear order on the variables and QLe is a linear order at
all (DescriptiveComplexity.QsatTM.isLinOrd_qLe).