The transition table of the QBF machine is a table

Before any run is considered: each transition has exactly one destination and one symbol written, and the places where two tags could both apply are identified. A mistake in the table shows up here first, which is why this comes before the correctness proof.

Unlike the SAT machine there are three such places, not two:

• at ⊢ in a leftward sweep, the three ways a sweep can end – hand over to the next sweep, start the check, or accept because there is no clause at all – are separated by the sweep index (i + 1 < k against i + 1 = k) and, for the last two, by whether the instance has a clause;
• at a marker in the check phase, the turn to the next clause and the accepting turn are separated, for a conjunctive matrix, by whether the clause just settled was the last one; for a disjunctive matrix they fire at different flags and so never compete;
• at a cell holding false in a rightward sweep, tGSet and tGKeep false are both applicable. That is the guessing choice, and it is the one ambiguity DescriptiveComplexity.AltQbf.altTr_unique does not resolve: it is the round's move.

The elements of the machine, compared

theorem DescriptiveComplexity.AltQbf.acstI_eq_iff {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : AltBase} {i i' : Fin (k + 1)} : acstI t i = acstI t' i' ↔ t = t' ∧ i = i'

theorem DescriptiveComplexity.AltQbf.aoneI_eq_iff {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : AltBase} {i i' : Fin (k + 1)} {a a' : A} : aoneI t i a = aoneI t' i' a' ↔ t = t' ∧ i = i' ∧ a = a'

The table is functional

The three branch points

Reading the tag off the state and the symbol

At most one transition applies, away from the guess

theorem DescriptiveComplexity.AltQbf.altTr_unique {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {τ τ' q a : AltV k A} (hτ : AltTr cnf τ) (hτ' : AltTr cnf τ') (hs : AltSrc cnf τ q) (hs' : AltSrc cnf τ' q) (hr : AltRead τ a) (hr' : AltRead τ' a) (hguess : ¬∃ (i : Fin (k + 1)) (x : A), q = stG i true ∧ a = symV false x) : τ = τ'

At most one transition applies, away from the one nondeterministic choice of a guessing sweep: the state and the symbol read pin the base tag (DescriptiveComplexity.AltQbf.base_cases), the base tag pins the rest (DescriptiveComplexity.AltQbf.altTr_payload), and the two remaining ambiguities are the exclusive branch points.