Documentation

DescriptiveComplexity.Problems.Machine.AltPos

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.AltQbf.AltBase does not depend on k, and a tag's sweep index only ever refines the order inside a family (DescriptiveComplexity.AltQbf.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.AltQbf.altTr_unique rather than a second induction.

The three kinds of position #

The tape order #

source
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.

Dependency graph

Singling the markers and the cells out #

The order between the three kinds #

source
theorem DescriptiveComplexity.AltQbf.posStart_le_posCell {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) :
tagTupleLe posStart (posCell x)
Dependency graph
source
theorem DescriptiveComplexity.AltQbf.posCell_le_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) :
tagTupleLe (posCell x) posEnd
Dependency graph
source
theorem DescriptiveComplexity.AltQbf.posStart_le_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
tagTupleLe posStart posEnd
Dependency graph

The head's first and last moves of a sweep #

source
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
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.AltQbf.le_qtopA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) :
    a ≤ qtopA
    Dependency graph

    Determinism away from the guess #