The positions of the QBF machine's tape, concretely

Where the head is, and what follows what: the left marker is the lowest position, the cell of the least element follows it, the right marker follows the cell of the greatest element, and cells are ordered as their elements are.

Every fact about the tags here is a decide: DescriptiveComplexity.AltBase does not depend on k, and a tag's sweep index only ever refines the order inside a family (DescriptiveComplexity.altTag_lt_of_base_lt). That is what the pair-shaped tag of DescriptiveComplexity.Problems.Machine.AltTape buys.

The file ends with the determinism of the machine away from the guessing choice, which is what makes the ⇐ half of correctness a corollary of DescriptiveComplexity.altTr_unique rather than a second induction.

The three kinds of position

theorem DescriptiveComplexity.AltQbf.altPosn_posStart {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltPosn posStart

The left marker is a position.

theorem DescriptiveComplexity.AltQbf.altPosn_posCell {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : AltPosn (posCell x)

The cell of an element is a position.

theorem DescriptiveComplexity.AltQbf.altPosn_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : AltPosn posEnd

The right marker is a position.

The tape order

theorem DescriptiveComplexity.AltQbf.altTagTupleLe_refl {k : ℕ} {A : Type} [LinearOrder A] (p : AltV k A) : tagTupleLe p p

The tape order is reflexive.

theorem DescriptiveComplexity.AltQbf.altTagTupleLe_of_tag_lt {k : ℕ} {A : Type} [LinearOrder A] {p q : AltV k A} (h : p.1 < q.1) : tagTupleLe p q

A tag strictly below another puts its tuples below all of theirs.

theorem DescriptiveComplexity.AltQbf.altTag_lt_of_base_lt {k : ℕ} {t t' : AltBase} (h : altBaseIdx t < altBaseIdx t') (i i' : Fin (k + 1)) : (t, i) < (t', i')

A lower base tag is a lower tag, whatever the sweep indices: the order on tags is the base tag first.

theorem DescriptiveComplexity.AltQbf.altTagTupleLe_tag_le {k : ℕ} {A : Type} [LinearOrder A] {p q : AltV k A} (h : tagTupleLe p q) : p.1 ≤ q.1

The tape order refines the tag order.

theorem DescriptiveComplexity.AltQbf.altBaseIdx_le_of_tag_le {k : ℕ} {t t' : AltTag k} (h : t ≤ t') : altBaseIdx t.1 ≤ altBaseIdx t'.1

The tag order refines the base-tag numbering.

Singling the markers and the cells out

theorem DescriptiveComplexity.AltQbf.eq_posStart_of_posn {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : AltV k A} (hp : AltPosn p) (h : p.1.1 = AltBase.pStart) : p = posStart

There is only one left marker.

theorem DescriptiveComplexity.AltQbf.eq_posCell_of_posn {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : AltV k A} (hp : AltPosn p) (h : p.1.1 = AltBase.pCell) : p = posCell (p.2 0)

A cell is the cell of the element it carries.

theorem DescriptiveComplexity.AltQbf.eq_posEnd_of_posn {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : AltV k A} (hp : AltPosn p) (h : p.1.1 = AltBase.pEnd) : p = posEnd

There is only one right marker.

The order between the three kinds

theorem DescriptiveComplexity.AltQbf.posStart_le_posCell {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe posStart (posCell x)

theorem DescriptiveComplexity.AltQbf.posCell_le_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe (posCell x) posEnd

theorem DescriptiveComplexity.AltQbf.posStart_le_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : tagTupleLe posStart posEnd

theorem DescriptiveComplexity.AltQbf.pStart_idx_lt {t : AltBase} (h : t ≠ AltBase.pStart) : altBaseIdx AltBase.pStart < altBaseIdx t

Every base tag other than the left marker's is above it.

theorem DescriptiveComplexity.AltQbf.minPos_posStart {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : MinPos tagTupleLe AltPosn posStart

The left marker is the lowest position: the head starts there.

theorem DescriptiveComplexity.AltQbf.posCell_le_iff {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {x y : A} : tagTupleLe (posCell x) (posCell y) ↔ x ≤ y

Cells are ordered as their elements are: the tape order between two cells is the source order between the elements they belong to, which is what makes a sweep over the cells a walk along the instance.

The head's first and last moves of a sweep

theorem DescriptiveComplexity.AltQbf.base_le_pCell {t : AltBase} (h : altBaseIdx t ≤ altBaseIdx AltBase.pCell) : t = AltBase.pStart ∨ t = AltBase.pCell

Only the two lowest base tags are at or below a cell's.

theorem DescriptiveComplexity.AltQbf.base_between {t : AltBase} (h₁ : altBaseIdx AltBase.pCell ≤ altBaseIdx t) (h₂ : altBaseIdx t ≤ altBaseIdx AltBase.pEnd) : t = AltBase.pCell ∨ t = AltBase.pEnd

Only the two highest of the bracketing base tags lie between a cell's and the right marker's.

theorem DescriptiveComplexity.AltQbf.succPos_posStart_posCell {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SuccPos tagTupleLe AltPosn posStart (posCell qbotA)

The head's first move. The cell of the least element follows the left marker immediately: a sweep starts by stepping over ⊢.

noncomputable def DescriptiveComplexity.AltQbf.qtopA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : A

The greatest element of the instance: the last cell of the tape.

Equations

• DescriptiveComplexity.AltQbf.qtopA = ⋯.choose

theorem DescriptiveComplexity.AltQbf.le_qtopA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : a ≤ qtopA

theorem DescriptiveComplexity.AltQbf.succPos_posCell_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SuccPos tagTupleLe AltPosn (posCell qtopA) posEnd

The head's last move of a sweep. The right marker follows the cell of the greatest element: this is where a sweep turns round.

Determinism away from the guess

theorem DescriptiveComplexity.AltQbf.step_functional_off_guess {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {c c₁ c₂ : Config (AltV k A)} (hguess : ¬∃ (i : Fin (k + 1)) (x : A), c.state = stG i true ∧ c.tape c.head = symV false x) (h₁ : (altMachine k A cnf).Step c c₁) (h₂ : (altMachine k A cnf).Step c c₂) : c₁ = c₂

The machine is deterministic away from the guessing choice. Once the transition is pinned (DescriptiveComplexity.altTr_unique), the successor configuration is too: its state by altDst_functional, the cell under the head by altWrite_functional, every other cell by the frame condition, and the head itself by uniqueness of the neighbour in the direction the transition names.