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.altTr_unique does not resolve: it is the round's move.

The elements of the machine, compared #

source

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'

Dependency graph

source

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'

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altV_ext {k : ℕ} {A : Type} {τ τ' : AltV k A} (ht : τ.1 = τ'.1) (h0 : τ.2 0 = τ'.2 0) (h1 : τ.2 1 = τ'.2 1) :

τ = τ'

Two elements agree when their tag and both coordinates do.

Dependency graph

The table is functional #

source

theorem DescriptiveComplexity.AltQbf.altWrite_functional {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a a' : AltV k A} (h : AltWrite τ a) (h' : AltWrite τ a') :

a = a'

A transition writes exactly one symbol.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altDst_functional {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {τ q q' : AltV k A} (h : AltDst cnf τ q) (h' : AltDst cnf τ q') :

q = q'

A transition moves to exactly one state. The only case with a choice is the check clause, whose two branches are separated by the flag and by DescriptiveComplexity.QbfLit.

Dependency graph

The three branch points #

source

theorem DescriptiveComplexity.AltQbf.altTr_next_end_excl {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {cnf : Bool} {τ τ' : AltV k A} (h : AltTr cnf τ) (h' : AltTr cnf τ') (hτ : τ.1.1 = AltBase.tGNext) (hτ' : τ'.1.1 = AltBase.tGEndAcc ∨ τ'.1.1 = AltBase.tGEndChk) (hi : τ.1.2 = τ'.1.2) :

False

A sweep hands over, or ends: the two are separated by the sweep index.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altTr_end_excl {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {cnf : Bool} {τ τ' : AltV k A} (h : AltTr cnf τ) (h' : AltTr cnf τ') (hτ : τ.1.1 = AltBase.tGEndAcc) (hτ' : τ'.1.1 = AltBase.tGEndChk) :

False

The end of the last sweep is not ambiguous: an instance either has a clause to check or has none.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altTr_turn_excl {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {cnf : Bool} {τ τ' : AltV k A} {d d' : Bool} (h : AltTr cnf τ) (h' : AltTr cnf τ') (hτ : τ.1.1 = AltBase.tTurnNext d) (hτ' : τ'.1.1 = AltBase.tTurnAcc d') (hcnf : cnf = true) (hc : τ.2 0 = τ'.2 0) :

False

A turn is not ambiguous: for a conjunctive matrix the clause just checked either has a successor or is the last one, and for a disjunctive one the two turns fire at different flags.

Dependency graph

Reading the tag off the state and the symbol #

source

def DescriptiveComplexity.AltQbf.stateBase (cnf : Bool) :

AltBase → AltBase

Which base tag the state a transition applies in carries.

Equations

Instances For

Dependency graph

source

def DescriptiveComplexity.AltQbf.readBase :

AltBase → AltBase

Which base tag the symbol a transition reads carries.

Equations

Instances For

Dependency graph

source

def DescriptiveComplexity.AltQbf.isTrBase :

AltBase → Bool

The base tags that a transition may carry.

Equations

Instances For

Dependency graph

source

def DescriptiveComplexity.AltQbf.isSweepBase :

AltBase → Bool

The base tags whose source state is a sweeping state, and so carries the transition's own sweep index.

Equations

Instances For

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altTr_isTrBase {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {cnf : Bool} {τ : AltV k A} (hτ : AltTr cnf τ) :

isTrBase τ.1.1 = true

Only transitions have transition tags.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altSrc_base {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {τ q : AltV k A} (hτ : AltTr cnf τ) (hs : AltSrc cnf τ q) :

q.1.1 = stateBase cnf τ.1.1 ∧ (isSweepBase τ.1.1 = true → q.1.2 = τ.1.2)

The state a transition applies in has the base tag its own tag names, and its sweep index.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altRead_base {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {τ a : AltV k A} (hτ : AltTr cnf τ) (hr : AltRead τ a) :

a.1.1 = readBase τ.1.1

The symbol a transition reads has the base tag its own tag names.

Dependency graph

At most one transition applies, away from the guess #

source

def DescriptiveComplexity.AltQbf.isEndBase :

AltBase → Bool

The base tags at which a sweep ends.

Equations

Instances For

Dependency graph

source

def DescriptiveComplexity.AltQbf.isTurnBase :

AltBase → Bool

The base tags of a turn in the check phase.

Equations

Instances For

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.base_cases (cnf : Bool) (t t' : AltBase) :

isTrBase t = true → isTrBase t' = true → stateBase cnf t = stateBase cnf t' → readBase t = readBase t' → t = t' ∨ t = AltBase.tGKeep false ∧ t' = AltBase.tGSet ∨ t = AltBase.tGSet ∧ t' = AltBase.tGKeep false ∨ t = AltBase.tGNext ∧ (t' = AltBase.tGEndAcc ∨ t' = AltBase.tGEndChk) ∨ (t = AltBase.tGEndAcc ∨ t = AltBase.tGEndChk) ∧ t' = AltBase.tGNext ∨ t = AltBase.tGEndAcc ∧ t' = AltBase.tGEndChk ∨ t = AltBase.tGEndChk ∧ t' = AltBase.tGEndAcc ∨ (∃ (d : Bool), t = AltBase.tTurnNext d ∧ t' = AltBase.tTurnAcc d) ∨ ∃ (d : Bool), t = AltBase.tTurnAcc d ∧ t' = AltBase.tTurnNext d

The state and the symbol pin the tag, up to the three branch points: the guessing choice, the end of a sweep and the turn.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altTr_index_zero {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {cnf : Bool} {τ : AltV k A} (hτ : AltTr cnf τ) (h : ¬isSweepBase τ.1.1 = true) :

↑τ.1.2 = 0

Away from the sweeps, a transition's sweep index is 0.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.isSweepBase_congr (cnf : Bool) (t t' : AltBase) :

isTrBase t = true → isTrBase t' = true → stateBase cnf t = stateBase cnf t' → isSweepBase t = isSweepBase t'

Whether a transition's source is a sweeping state is determined by the base tag of that state.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altTr_payload {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) (hb : τ.1.1 = τ'.1.1) :

τ = τ'

Equal base tags force equal transitions: the state and the symbol pin one coordinate and the sweep index, and the promises in DescriptiveComplexity.AltTr pin the other.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altSrc_read_guess {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {τ q a : AltV k A} (hb : τ.1.1 = AltBase.tGKeep false ∨ τ.1.1 = AltBase.tGSet) (hs : AltSrc cnf τ q) (hr : AltRead τ a) :

q = stG τ.1.2 true ∧ a = symV false (τ.2 0)

At a guessing choice, the state and the symbol read are what DescriptiveComplexity.altTr_unique's hypothesis excludes.

Dependency graph

source

theorem DescriptiveComplexity.AltQbf.altTr_turn_pair {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {τ τ' q : AltV k A} (hτ : AltTr cnf τ) (hτ' : AltTr cnf τ') (hs : AltSrc cnf τ q) (hs' : AltSrc cnf τ' q) {d : Bool} (hb : τ.1.1 = AltBase.tTurnNext d) (hb' : τ'.1.1 = AltBase.tTurnAcc d) :

False

The two turns never compete: for a conjunctive matrix the clause just settled is either the last one or has a successor, and for a disjunctive one they fire at different flags, so their source states differ.

Dependency graph

source

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.base_cases), the base tag pins the rest (DescriptiveComplexity.altTr_payload), and the two remaining ambiguities are the exclusive branch points.

Dependency graph

Documentation

DescriptiveComplexity.Problems.Machine.AltTable

The transition table of the QBF machine is a table #

The elements of the machine, compared #

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 #