Documentation

DescriptiveComplexity.Problems.Machine.QsatProgram

The machine of a quantified Boolean formula #

The program half of QSAT ≤ᶠᵒ[≤] DTMAcceptSpace: the states, symbols and transitions of the machine built inside a QSAT instance, on the tape laid out in DescriptiveComplexity.Problems.Machine.QsatTape.

The program #

Iterative evaluation of a quantified Boolean formula. The recursion stack is not a stack: each variable's own cell carries its current value b together with a bit f recording that both values have already been tried, which is all the standard algorithm needs.

  Desc      ⊢ → at each cell write (0,0), moving right → ⊣, then evaluate
  Eval f d c  sweep in direction d accumulating f := f ∨ QLit c x b;
              at the marker: ¬f → the matrix is false;
                             f and c has a successor → next clause, turn round;
                             f and c is the last → the matrix is true
  ToEnd b   walk right to ⊣, turn round, and return the value b
  Proc b    at the innermost unfinished variable x:
              the level is decided (∃ and b, or ∀ and ¬b, or f already set)
                                            → move left, keep returning b
              otherwise                     → write (1,1), move right, Desc
            at ⊢: b → accept; ¬b → no transition, the run dies

The machine is deterministic, which is the whole point: DTMAcceptSpace folds DescriptiveComplexity.TMData.Deterministic into its yes-instances, and a deterministic run is also what makes the converse half of correctness free (Relation.ReflTransGen.total_of_right_unique).

Malformed instances #

DescriptiveComplexity.QsatHolds requires DescriptiveComplexity.QsatWf, so an instance whose prefix order is not a strict linear order on the marked variables must map to a machine that cannot accept. That is arranged by a guard on the accepting predicate (DescriptiveComplexity.QsatTM.QAcc) rather than by the tape order, which would not catch every violation.

Semantics first #

As in DescriptiveComplexity.Problems.Machine.Hardness, everything here is a plain predicate on tagged tuples: the machine is assembled as a DescriptiveComplexity.TMData and reasoned about directly, and only later transcribed into defining formulas. A transition table type-checks whatever it says, so it has to be validated by proofs – which is what the second half of this file is.

The instance, read #

def DescriptiveComplexity.QsatTM.QCl {A : Type} [FirstOrder.Language.qsat.Structure A] (c : A) :

Being a clause of the matrix.

Equations

DescriptiveComplexity.QsatTM.QCl c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsClause ![c]

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QPosIn {A : Type} [FirstOrder.Language.qsat.Structure A] (c x : A) :

The variable x occurs positively in the clause c.

Equations

DescriptiveComplexity.QsatTM.QPosIn c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPosIn ![c, x]

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QNegIn {A : Type} [FirstOrder.Language.qsat.Structure A] (c x : A) :

The variable x occurs negatively in the clause c.

Equations

DescriptiveComplexity.QsatTM.QNegIn c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsNegIn ![c, x]

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QLit {A : Type} [FirstOrder.Language.qsat.Structure A] (c x : A) (b : Bool) :

The literal test: the cell of x, holding the truth value b, satisfies the clause c. This is the first-order test on the source structure that the evaluation sweep performs.

Equations

DescriptiveComplexity.QsatTM.QLit c x b = (DescriptiveComplexity.QsatTM.QPosIn c x ∧ b = true ∨ DescriptiveComplexity.QsatTM.QNegIn c x ∧ b = false)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QMinCl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (c : A) :

c is the lowest clause in the ambient order.

Equations

DescriptiveComplexity.QsatTM.QMinCl c = (DescriptiveComplexity.QsatTM.QCl c ∧ ∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → c ≤ e)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QMaxCl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (c : A) :

c is the highest clause in the ambient order.

Equations

DescriptiveComplexity.QsatTM.QMaxCl c = (DescriptiveComplexity.QsatTM.QCl c ∧ ∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → e ≤ c)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QNextCl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (c c' : A) :

c' is the clause immediately above c.

Equations

DescriptiveComplexity.QsatTM.QNextCl c c' = (DescriptiveComplexity.QsatTM.QCl c ∧ DescriptiveComplexity.QsatTM.QCl c' ∧ c < c' ∧ ∀ (e : A), DescriptiveComplexity.QsatTM.QCl e → c < e → c' ≤ e)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QShort {A : Type} [FirstOrder.Language.qsat.Structure A] (v : Bool) (x : A) :

The level is already decided: a returning value v settles the quantifier at x on its own – an existential level reached by a winning branch, a universal one by a losing branch.

Equations

DescriptiveComplexity.QsatTM.QShort v x = (DescriptiveComplexity.IsQAll x ∧ v = false ∨ ¬DescriptiveComplexity.IsQAll x ∧ v = true)

Instances For

Dependency graph

The elements of the machine #

noncomputable def DescriptiveComplexity.QsatTM.qBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

A

The least element of the instance, to which every constant of the machine is pinned.

Equations

DescriptiveComplexity.QsatTM.qBot = ⋯.choose

Instances For

Dependency graph

theorem DescriptiveComplexity.QsatTM.qBot_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) :

Dependency graph

theorem DescriptiveComplexity.QsatTM.isMinTup_qBot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

IsMinTup fun (x : Fin 2) => qBot

Dependency graph

noncomputable def DescriptiveComplexity.QsatTM.qCst {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : QTag) :

QV A

A constant of the machine: a tag on the pair of least elements.

Equations

DescriptiveComplexity.QsatTM.qCst t = (t, fun (x : Fin 2) => DescriptiveComplexity.QsatTM.qBot)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.QsatTM.qOne {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : QTag) (a : A) :

QV A

A tag carrying one element, pinned in the second coordinate.

Equations

DescriptiveComplexity.QsatTM.qOne t a = (t, ![a, DescriptiveComplexity.QsatTM.qBot ])

Instances For

Dependency graph

Symbols #

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.symStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

QV A

The left-marker symbol.

Equations

DescriptiveComplexity.QsatTM.symStart = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.sStart

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.symEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

QV A

The right-marker symbol.

Equations

DescriptiveComplexity.QsatTM.symEnd = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.sEnd

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.symV {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b f : Bool) (x : A) :

QV A

The symbol of the cell of x: value b, flag f.

Equations

DescriptiveComplexity.QsatTM.symV b f x = DescriptiveComplexity.QsatTM.qOne (DescriptiveComplexity.QsatTM.QTag.sVal b f) x

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.markerSym {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (d : Bool) :

QV A

The marker a sweep in direction d ends at.

Equations

DescriptiveComplexity.QsatTM.markerSym d = if d = true then DescriptiveComplexity.QsatTM.symEnd else DescriptiveComplexity.QsatTM.symStart

Instances For

Dependency graph

Positions #

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

QV A

The left-marker cell.

Equations

DescriptiveComplexity.QsatTM.posStart = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.pStart

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) :

QV A

The cell of the variable x.

Equations

DescriptiveComplexity.QsatTM.posCell x = DescriptiveComplexity.QsatTM.qOne DescriptiveComplexity.QsatTM.QTag.pCell x

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

QV A

The right-marker cell.

Equations

DescriptiveComplexity.QsatTM.posEnd = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.pEnd

Instances For

Dependency graph

States #

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stDesc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

QV A

Descending: initialising the cells to the right.

Equations

DescriptiveComplexity.QsatTM.stDesc = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.qDesc

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stEval {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f d : Bool) (c : A) :

QV A

Evaluating the clause c, flag f, sweeping in direction d.

Equations

DescriptiveComplexity.QsatTM.stEval f d c = DescriptiveComplexity.QsatTM.qOne (DescriptiveComplexity.QsatTM.QTag.qEval f d) c

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stToEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b : Bool) :

QV A

Carrying the value b to the right marker.

Equations

DescriptiveComplexity.QsatTM.stToEnd b = DescriptiveComplexity.QsatTM.qCst (DescriptiveComplexity.QsatTM.QTag.qToEnd b)

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stProc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (b : Bool) :

QV A

Returning the value b through the prefix.

Equations

DescriptiveComplexity.QsatTM.stProc b = DescriptiveComplexity.QsatTM.qCst (DescriptiveComplexity.QsatTM.QTag.qProc b)

Instances For

Dependency graph

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.QsatTM.stAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :

QV A

The accepting state.

Equations

DescriptiveComplexity.QsatTM.stAcc = DescriptiveComplexity.QsatTM.qCst DescriptiveComplexity.QsatTM.QTag.qAcc

Instances For

Dependency graph

The transition table #

def DescriptiveComplexity.QsatTM.IsMin1 {A : Type} [LinearOrder A] (p : QV A) :

The second coordinate of a tuple is the least element: the padding of the tags that carry a single element.

Equations

DescriptiveComplexity.QsatTM.IsMin1 p = ∀ (a : A), p.2 1 ≤ a

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QTr {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (τ : QV A) :

Which tagged tuples are transitions. The payload is pinned exactly as far as the transition needs it.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QSrc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ q : QV A) :

The state a transition applies in.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QRead {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : QV A) :

The symbol a transition reads.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QDst {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ q : QV A) :

The state a transition moves to. The only place the instance is consulted is the evaluation sweep, where the new flag depends on DescriptiveComplexity.QsatTM.QLit.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QWrite {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : QV A) :

The symbol a transition writes: the descent resets a cell, the switch sets the second value with the flag up, and everything else leaves the tape as it found it.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QRight {A : Type} (τ : QV A) :

Which transitions move the head right: the descent and the carry always do, a sweep goes in its own direction, a turn reverses, and the return walks leftwards.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QAcc {A : Type} [FirstOrder.Language.qsat.Structure A] (q : QV A) :

Accepting states, guarded by well-formedness of the instance: a malformed instance is a no-instance of QSAT, and its machine has no accepting state at all.

Equations

DescriptiveComplexity.QsatTM.QAcc q = (DescriptiveComplexity.QsatWf A ∧ q.1 = DescriptiveComplexity.QsatTM.QTag.qAcc)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.QStart {A : Type} [LinearOrder A] (q : QV A) :

Start states: just DescriptiveComplexity.QsatTM.stDesc.

Equations

DescriptiveComplexity.QsatTM.QStart q = (q.1 = DescriptiveComplexity.QsatTM.QTag.qDesc ∧ DescriptiveComplexity.IsMinTup q.2)

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qsatMachine (A : Type) [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

The machine of a quantified Boolean formula.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

The table is a table #

Before any run is considered: each transition has exactly one destination and symbol written, and the state together with the symbol read pins the transition. A mistake in the table shows up here first, which is why these come before the correctness proof.

theorem DescriptiveComplexity.QsatTM.qV_ext {A : Type} {τ τ' : QV 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

theorem DescriptiveComplexity.QsatTM.qOne_eq_qOne_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : QTag} {a a' : A} :

qOne t a = qOne t' a' ↔ t = t' ∧ a = a'

Dependency graph

theorem DescriptiveComplexity.QsatTM.qWrite_functional {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a a' : QV A} (h : QWrite τ a) (h' : QWrite τ a') :

a = a'

A transition writes exactly one symbol.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qDst_functional {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ q q' : QV A} (h : QDst τ q) (h' : QDst τ q') :

q = q'

A transition moves to exactly one state. The only case with a choice is the evaluation sweep, whose two branches are separated by the flag and by DescriptiveComplexity.QsatTM.QLit.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTr_descEnd_excl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {τ τ' : QV A} (h : QTr τ) (h' : QTr τ') (hτ : τ.1 = QTag.tDescEndTrue) (hτ' : τ'.1 = QTag.tDescEndEval) :

The end of the descent is not ambiguous: the matrix either has a clause or has none.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTr_turn_excl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {τ τ' : QV A} {d d' : Bool} (h : QTr τ) (h' : QTr τ') (hτ : τ.1 = QTag.tTurnNext d) (hτ' : τ'.1 = QTag.tTurnLast d') (hc : τ.2 0 = τ'.2 0) :

A turn is not ambiguous: the clause just evaluated either has a successor or is the last one.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTr_proc_excl {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {τ τ' : QV A} {v b f v' b' f' : Bool} (h : QTr τ) (h' : QTr τ') (hτ : τ.1 = QTag.tProcSkip v b f) (hτ' : τ'.1 = QTag.tProcSwitch v' b' f') (hv : v = v') (hx : τ.2 0 = τ'.2 0) (hf : f = f') :

The return step is not ambiguous: a level either is decided – by the quantifier or by its flag – or is not.

Dependency graph

The tag of a transition, seen from the state and the symbol #

def DescriptiveComplexity.QsatTM.qStateTag :

The tag of the state a transition applies in, as a function of its own tag. Junk tags are sent to themselves; they are never transitions.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qReadTag :

The tag of the symbol a transition reads, as a function of its own tag.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.QsatTM.qSrc_tag {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ q : QV A} (hτ : QTr τ) (hs : QSrc τ q) :

q.1 = qStateTag τ.1

The state pins the transition's tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qRead_tag {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ a : QV A} (hτ : QTr τ) (hr : QRead τ a) :

a.1 = qReadTag τ.1

The symbol read pins the transition's tag.

Dependency graph

def DescriptiveComplexity.QsatTM.qIsTrTag :

Being the tag of a transition.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qIsDescEndTrue :

The tag ending the descent with no clause to evaluate.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qIsDescEndEval :

The tag ending the descent with a clause to evaluate.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qIsTurnNext :

The tag turning to the next clause.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qIsTurnLast :

The tag finishing the last clause.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qIsProcSkip :

The tag passing a decided level on.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.QsatTM.qIsProcSwitch :

The tag switching a level to its second value.

Equations

Instances For

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTag_cases (t t' : QTag) :

qIsTrTag t = true → qIsTrTag t' = true → qStateTag t = qStateTag t' → qReadTag t = qReadTag t' → t = t' ∨ qIsDescEndTrue t = true ∧ qIsDescEndEval t' = true ∨ qIsDescEndEval t = true ∧ qIsDescEndTrue t' = true ∨ qIsTurnNext t = true ∧ qIsTurnLast t' = true ∨ qIsTurnLast t = true ∧ qIsTurnNext t' = true ∨ qIsProcSkip t = true ∧ qIsProcSwitch t' = true ∨ qIsProcSwitch t = true ∧ qIsProcSkip t' = true

The state and the symbol determine the transition's tag, up to the three known branch points: the end of the descent, a turn, and the return step. A finite check over the tags – no case analysis by hand.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qIsDescEndTrue_iff {t : QTag} :

qIsDescEndTrue t = true ↔ t = QTag.tDescEndTrue

Dependency graph

theorem DescriptiveComplexity.QsatTM.qIsDescEndEval_iff {t : QTag} :

qIsDescEndEval t = true ↔ t = QTag.tDescEndEval

Dependency graph

theorem DescriptiveComplexity.QsatTM.qIsTurnNext_iff {t : QTag} :

qIsTurnNext t = true ↔ ∃ (d : Bool), t = QTag.tTurnNext d

Dependency graph

theorem DescriptiveComplexity.QsatTM.qIsTurnLast_iff {t : QTag} :

qIsTurnLast t = true ↔ ∃ (d : Bool), t = QTag.tTurnLast d

Dependency graph

theorem DescriptiveComplexity.QsatTM.qIsProcSkip_iff {t : QTag} :

qIsProcSkip t = true ↔ ∃ (v : Bool) (b : Bool) (f : Bool), t = QTag.tProcSkip v b f

Dependency graph

theorem DescriptiveComplexity.QsatTM.qIsProcSwitch_iff {t : QTag} :

qIsProcSwitch t = true ↔ ∃ (v : Bool) (b : Bool) (f : Bool), t = QTag.tProcSwitch v b f

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTr_isTrTag {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {τ : QV A} (hτ : QTr τ) :

qIsTrTag τ.1 = true

Only transitions have transition tags.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qSrc_turnNext {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : QV A} {d : Bool} (h : τ.1 = QTag.tTurnNext d) (hs : QSrc τ q) :

q = stEval true d (τ.2 0)

Reading off DescriptiveComplexity.QsatTM.QSrc at a turn-to-next tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qSrc_turnLast {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : QV A} {d : Bool} (h : τ.1 = QTag.tTurnLast d) (hs : QSrc τ q) :

q = stEval true d (τ.2 0)

Reading off DescriptiveComplexity.QsatTM.QSrc at a turn-to-last tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qSrc_procSkip {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : QV A} {v b f : Bool} (h : τ.1 = QTag.tProcSkip v b f) (hs : QSrc τ q) :

Reading off DescriptiveComplexity.QsatTM.QSrc at a skip tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qSrc_procSwitch {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ q : QV A} {v b f : Bool} (h : τ.1 = QTag.tProcSwitch v b f) (hs : QSrc τ q) :

Reading off DescriptiveComplexity.QsatTM.QSrc at a switch tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qRead_procSkip {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a : QV A} {v b f : Bool} (h : τ.1 = QTag.tProcSkip v b f) (hr : QRead τ a) :

a = symV b f (τ.2 0)

Reading off DescriptiveComplexity.QsatTM.QRead at a skip tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qRead_procSwitch {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {τ a : QV A} {v b f : Bool} (h : τ.1 = QTag.tProcSwitch v b f) (hr : QRead τ a) :

a = symV b f (τ.2 0)

Reading off DescriptiveComplexity.QsatTM.QRead at a switch tag.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTr_payload {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : QV A} (hτ : QTr τ) (hτ' : QTr τ') (hs : QSrc τ q) (hs' : QSrc τ' q) (hr : QRead τ a) (hr' : QRead τ' a) (ht : τ.1 = τ'.1) :

τ = τ'

Equal tags force equal payloads: the state and the symbol pin one coordinate, the promises in DescriptiveComplexity.QsatTM.QTr pin the other.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qTr_unique {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : QV A} (hτ : QTr τ) (hτ' : QTr τ') (hs : QSrc τ q) (hs' : QSrc τ' q) (hr : QRead τ a) (hr' : QRead τ' a) :

τ = τ'

At most one transition applies in a given state on a given symbol: the state and the symbol read pin the tag (DescriptiveComplexity.QsatTM.qTag_cases), the tag pins the payload (DescriptiveComplexity.QsatTM.qTr_payload), and the three branch points are exclusive.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qStart_unique {A : Type} [LinearOrder A] {q q' : QV A} (h : QStart q) (h' : QStart q') :

q = q'

There is exactly one start state.

Dependency graph

theorem DescriptiveComplexity.QsatTM.qsatMachine_deterministic {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :

(qsatMachine A).Deterministic

The machine is deterministic.

Dependency graph