The transcription: QSAT ≤ᶠᵒ[≤] DTMAcceptSpace

The first-order half of the reduction. The machine of a quantified Boolean formula was built semantically in DescriptiveComplexity.Problems.Machine.QsatProgram, and its correctness DescriptiveComplexity.QsatTM.qsatMachine_correct proved in DescriptiveComplexity.Problems.Machine.QsatRun. This file writes the defining formulas of an interpretation of Language.turing in ordered QSAT instances and shows each realizes exactly the corresponding predicate of the machine.

Method

The method is that of DescriptiveComplexity.Problems.Machine.Interp, one level up: the elements of the machine have only two shapes, qCst s and qOne s x, so the binary symbols get one shape helper each (DescriptiveComplexity.QsatTM.qCstF, DescriptiveComplexity.QsatTM.qOneF) with one realization lemma, and every defining formula then matches on its first tag alone. Comparisons of tags – which are static data – are decided in Lean rather than in the formula, so ⊤ and ⊥ do most of the work.

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.qsatOrd : FirstOrder.Language

The vocabulary the reduction reads: quantified CNF instances with the ambient order.

Equations

• DescriptiveComplexity.QsatTM.qsatOrd = FirstOrder.Language.qsat.sum FirstOrder.Language.order

The symbols of the ordered expansion

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.isVarSym : qsatOrd.Relations 1

The symbol for “is a quantified variable”.

Equations

• DescriptiveComplexity.QsatTM.isVarSym = Sum.inl FirstOrder.Language.qsIsVar

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.allVarSym : qsatOrd.Relations 1

The symbol for “is universally quantified”.

Equations

• DescriptiveComplexity.QsatTM.allVarSym = Sum.inl FirstOrder.Language.qsAllVar

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.precSym : qsatOrd.Relations 2

The symbol for the quantifier prefix.

Equations

• DescriptiveComplexity.QsatTM.precSym = Sum.inl FirstOrder.Language.qsPrefixLt

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.isClSym : qsatOrd.Relations 1

The symbol for “is a clause”.

Equations

• DescriptiveComplexity.QsatTM.isClSym = Sum.inl FirstOrder.Language.qsIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.posInSym : qsatOrd.Relations 2

The symbol for a positive occurrence.

Equations

• DescriptiveComplexity.QsatTM.posInSym = Sum.inl FirstOrder.Language.qsPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.negInSym : qsatOrd.Relations 2

The symbol for a negative occurrence.

Equations

• DescriptiveComplexity.QsatTM.negInSym = Sum.inl FirstOrder.Language.qsNegIn

@[reducible, inline]

abbrev DescriptiveComplexity.QsatTM.ordSym : qsatOrd.Relations 2

The ambient order symbol.

Equations

• DescriptiveComplexity.QsatTM.ordSym = Sum.inr FirstOrder.Language.leSymb

The builders

def DescriptiveComplexity.QsatTM.vF {α : Type} (x : α) : qsatOrd.Formula α

x is a quantified variable.

Equations

• DescriptiveComplexity.QsatTM.vF x = DescriptiveComplexity.QsatTM.isVarSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatTM.aF {α : Type} (x : α) : qsatOrd.Formula α

x is universally quantified.

Equations

• DescriptiveComplexity.QsatTM.aF x = DescriptiveComplexity.QsatTM.allVarSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatTM.precF {α : Type} (x y : α) : qsatOrd.Formula α

x is quantified outside y.

Equations

• DescriptiveComplexity.QsatTM.precF x y = DescriptiveComplexity.QsatTM.precSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.QsatTM.clF {α : Type} (x : α) : qsatOrd.Formula α

x is a clause.

Equations

• DescriptiveComplexity.QsatTM.clF x = DescriptiveComplexity.QsatTM.isClSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatTM.posF {α : Type} (c x : α) : qsatOrd.Formula α

x occurs positively in c.

Equations

• DescriptiveComplexity.QsatTM.posF c x = DescriptiveComplexity.QsatTM.posInSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatTM.negF {α : Type} (c x : α) : qsatOrd.Formula α

x occurs negatively in c.

Equations

• DescriptiveComplexity.QsatTM.negF c x = DescriptiveComplexity.QsatTM.negInSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatTM.ordF {α : Type} (x y : α) : qsatOrd.Formula α

x ≤ y in the ambient order.

Equations

• DescriptiveComplexity.QsatTM.ordF x y = DescriptiveComplexity.QsatTM.ordSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.QsatTM.eqF {α : Type} (x y : α) : qsatOrd.Formula α

x = y.

Equations

• DescriptiveComplexity.QsatTM.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.QsatTM.ordLtF {α : Type} (x y : α) : qsatOrd.Formula α

x < y in the ambient order.

Equations

• DescriptiveComplexity.QsatTM.ordLtF x y = DescriptiveComplexity.QsatTM.ordF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.QsatTM.eqF x y)

noncomputable def DescriptiveComplexity.QsatTM.minF {α : Type} (x : α) : qsatOrd.Formula α

x is the least element of the ambient order.

Equations

• DescriptiveComplexity.QsatTM.minF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.QsatTM.ordF (Sum.inl x) (Sum.inr 0))

def DescriptiveComplexity.QsatTM.pLeF {α : Type} (x y : α) : qsatOrd.Formula α

The tape order on elements: quantified variables first in prefix order, everything else after them in the ambient order.

Equations

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

noncomputable def DescriptiveComplexity.QsatTM.minClF {α : Type} (c : α) : qsatOrd.Formula α

c is the lowest clause.

Equations

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

noncomputable def DescriptiveComplexity.QsatTM.maxClF {α : Type} (c : α) : qsatOrd.Formula α

c is the highest clause.

Equations

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

noncomputable def DescriptiveComplexity.QsatTM.nextClF {α : Type} (c c' : α) : qsatOrd.Formula α

c' is the clause immediately above c.

Equations

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

noncomputable def DescriptiveComplexity.QsatTM.noClF {α : Type} : qsatOrd.Formula α

There is no clause at all.

Equations

• DescriptiveComplexity.QsatTM.noClF = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.QsatTM.clF (Sum.inr 0)))

def DescriptiveComplexity.QsatTM.litF {α : Type} (b : Bool) (c x : α) : qsatOrd.Formula α

The cell of x, holding the value b, satisfies the clause c.

Equations

• DescriptiveComplexity.QsatTM.litF b c x = if b = true then DescriptiveComplexity.QsatTM.posF c x else DescriptiveComplexity.QsatTM.negF c x

def DescriptiveComplexity.QsatTM.shortF {α : Type} (v : Bool) (x : α) : qsatOrd.Formula α

The returning value v settles the quantifier at x.

Equations

• DescriptiveComplexity.QsatTM.shortF v x = if v = true then FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.QsatTM.aF x) else DescriptiveComplexity.QsatTM.aF x

noncomputable def DescriptiveComplexity.QsatTM.wfF {α : Type} : qsatOrd.Formula α

Well-formedness of the instance, as a sentence with unused free variables.

Equations

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

Realization of the builders

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_vF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (vF x).Realize v ↔ IsQVar (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_aF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (aF x).Realize v ↔ IsQAll (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_precF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (precF x y).Realize v ↔ QPrec (v x) (v y)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_clF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (clF x).Realize v ↔ QCl (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_posF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {c x : α} : (posF c x).Realize v ↔ QPosIn (v c) (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_negF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {c x : α} : (negF c x).Realize v ↔ QNegIn (v c) (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_ordF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ordF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_eqF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_ordLtF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ordLtF x y).Realize v ↔ v x < v y

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_minF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (minF x).Realize v ↔ ∀ (a : A), v x ≤ a

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_pLeF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (pLeF x y).Realize v ↔ PLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_clFAll {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (minClF x).Realize v ↔ QMinCl (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_maxClF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x : α} : (maxClF x).Realize v ↔ QMaxCl (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_nextClF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (nextClF x y).Realize v ↔ QNextCl (v x) (v y)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_noClF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} : noClF.Realize v ↔ ∀ (e : A), ¬QCl e

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_litF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {b : Bool} {c x : α} : (litF b c x).Realize v ↔ QLit (v c) (v x) b

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_shortF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} {b : Bool} {x : α} : (shortF b x).Realize v ↔ QShort b (v x)

@[simp]

theorem DescriptiveComplexity.QsatTM.realize_wfF {α A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] {v : α → A} : wfF.Realize v ↔ QsatWf A

The two shapes of the machine's elements, as formulas

noncomputable def DescriptiveComplexity.QsatTM.qCstF (s t' : QTag) : qsatOrd.Formula (Fin 2 × Fin 2)

The second argument of a binary symbol is the constant qCst s.

Equations

• DescriptiveComplexity.QsatTM.qCstF s t' = if t' = s then DescriptiveComplexity.QsatTM.minF (1, 0) ⊓ DescriptiveComplexity.QsatTM.minF (1, 1) else ⊥

noncomputable def DescriptiveComplexity.QsatTM.qOneF (s : QTag) (x : Fin 2 × Fin 2) (t' : QTag) : qsatOrd.Formula (Fin 2 × Fin 2)

The second argument of a binary symbol is qOne s (v x).

Equations

• DescriptiveComplexity.QsatTM.qOneF s x t' = if t' = s then DescriptiveComplexity.QsatTM.eqF (1, 0) x ⊓ DescriptiveComplexity.QsatTM.minF (1, 1) else ⊥

theorem DescriptiveComplexity.QsatTM.realize_qCstF {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 2 → A} {s : QTag} {q : QV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) : (qCstF s q.1).Realize v ↔ q = qCst s

theorem DescriptiveComplexity.QsatTM.realize_qOneF {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {v : Fin 2 × Fin 2 → A} {s : QTag} {x : Fin 2 × Fin 2} {q : QV A} (h0 : v (1, 0) = q.2 0) (h1 : v (1, 1) = q.2 1) : (qOneF s x q.1).Realize v ↔ q = qOne s (v x)

The defining formulas

noncomputable def DescriptiveComplexity.QsatTM.posnF : QTag → qsatOrd.Formula (Fin 1 × Fin 2)

Defining formula for posn.

Equations

• DescriptiveComplexity.QsatTM.posnF DescriptiveComplexity.QsatTM.QTag.pStart = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.posnF DescriptiveComplexity.QsatTM.QTag.pCell = DescriptiveComplexity.QsatTM.vF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.posnF DescriptiveComplexity.QsatTM.QTag.pEnd = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.posnF x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.trF : QTag → qsatOrd.Formula (Fin 1 × Fin 2)

Defining formula for tr: the payload promises of DescriptiveComplexity.QsatTM.QTr.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.QsatTM.trF DescriptiveComplexity.QsatTM.QTag.tDescStart = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tDescCell b f) = DescriptiveComplexity.QsatTM.vF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF DescriptiveComplexity.QsatTM.QTag.tDescEndEval = DescriptiveComplexity.QsatTM.minClF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tEval b f fl d) = DescriptiveComplexity.QsatTM.clF (0, 0) ⊓ DescriptiveComplexity.QsatTM.vF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tTurnNext d) = DescriptiveComplexity.QsatTM.nextClF (0, 0) (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tTurnLast d) = DescriptiveComplexity.QsatTM.maxClF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tTurnFalse d) = DescriptiveComplexity.QsatTM.clF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tToEndCell v b f) = DescriptiveComplexity.QsatTM.vF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tToEndStart v) = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF (DescriptiveComplexity.QsatTM.QTag.tToEndTurn v) = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF DescriptiveComplexity.QsatTM.QTag.tProcAcc = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.trF x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.startF : QTag → qsatOrd.Formula (Fin 1 × Fin 2)

Defining formula for start.

Equations

• DescriptiveComplexity.QsatTM.startF DescriptiveComplexity.QsatTM.QTag.qDesc = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.startF x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.accF : QTag → qsatOrd.Formula (Fin 1 × Fin 2)

Defining formula for acc: the accepting state, guarded by well-formedness of the instance.

Equations

• DescriptiveComplexity.QsatTM.accF DescriptiveComplexity.QsatTM.QTag.qAcc = DescriptiveComplexity.QsatTM.wfF
• DescriptiveComplexity.QsatTM.accF x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.blankF : QTag → qsatOrd.Formula (Fin 1 × Fin 2)

Defining formula for blank.

Equations

• DescriptiveComplexity.QsatTM.blankF DescriptiveComplexity.QsatTM.QTag.sBlank = DescriptiveComplexity.QsatTM.minF (0, 0) ⊓ DescriptiveComplexity.QsatTM.minF (0, 1)
• DescriptiveComplexity.QsatTM.blankF x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.rightF : QTag → qsatOrd.Formula (Fin 1 × Fin 2)

Defining formula for right: a static condition on the tag.

Equations

• DescriptiveComplexity.QsatTM.rightF DescriptiveComplexity.QsatTM.QTag.tDescStart = ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tDescCell b f) = ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tEval b f fl d) = if d = true then ⊤ else ⊥
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tTurnNext d) = if d = true then ⊥ else ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tTurnLast d) = if d = true then ⊥ else ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tTurnFalse d) = if d = true then ⊥ else ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tToEndCell v b f) = ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tToEndStart v) = ⊤
• DescriptiveComplexity.QsatTM.rightF (DescriptiveComplexity.QsatTM.QTag.tProcSwitch v b f) = ⊤
• DescriptiveComplexity.QsatTM.rightF DescriptiveComplexity.QsatTM.QTag.tProcAcc = ⊤
• DescriptiveComplexity.QsatTM.rightF x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.leTagF (t t' : QTag) : qsatOrd.Formula (Fin 2 × Fin 2)

Defining formula for le: the tag indices are static, so only the same-tag case needs a formula.

Equations

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

noncomputable def DescriptiveComplexity.QsatTM.inpF : QTag → QTag → qsatOrd.Formula (Fin 2 × Fin 2)

Defining formula for inp, the initial tape.

Equations

• DescriptiveComplexity.QsatTM.inpF DescriptiveComplexity.QsatTM.QTag.pStart x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.inpF DescriptiveComplexity.QsatTM.QTag.pCell x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal false false) (0, 0) x✝
• DescriptiveComplexity.QsatTM.inpF DescriptiveComplexity.QsatTM.QTag.pEnd x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.inpF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.tsrcF : QTag → QTag → qsatOrd.Formula (Fin 2 × Fin 2)

Defining formula for tsrc.

Equations

• DescriptiveComplexity.QsatTM.tsrcF DescriptiveComplexity.QsatTM.QTag.tDescStart x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tDescCell b f) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tsrcF DescriptiveComplexity.QsatTM.QTag.tDescEndTrue x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tsrcF DescriptiveComplexity.QsatTM.QTag.tDescEndEval x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tEval b f fl d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.qEval fl d) (0, 0) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tTurnNext d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.qEval true d) (0, 0) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tTurnLast d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.qEval true d) (0, 0) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tTurnFalse d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.qEval false d) (0, 0) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tToEndCell b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd b) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tToEndStart b) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd b) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tToEndTurn b) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd b) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tProcSkip b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qProc b) x✝
• DescriptiveComplexity.QsatTM.tsrcF (DescriptiveComplexity.QsatTM.QTag.tProcSwitch b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qProc b) x✝
• DescriptiveComplexity.QsatTM.tsrcF DescriptiveComplexity.QsatTM.QTag.tProcAcc x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qProc true) x✝
• DescriptiveComplexity.QsatTM.tsrcF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.treadF : QTag → QTag → qsatOrd.Formula (Fin 2 × Fin 2)

Defining formula for tread.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.QsatTM.treadF DescriptiveComplexity.QsatTM.QTag.tDescStart x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tDescCell b f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b f) (0, 0) x✝
• DescriptiveComplexity.QsatTM.treadF DescriptiveComplexity.QsatTM.QTag.tDescEndTrue x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.treadF DescriptiveComplexity.QsatTM.QTag.tDescEndEval x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tEval b f fl d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b f) (0, 1) x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tToEndCell b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b_1 f) (0, 0) x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tToEndStart b) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tToEndTurn b) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tProcSkip b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b_1 f) (0, 0) x✝
• DescriptiveComplexity.QsatTM.treadF (DescriptiveComplexity.QsatTM.QTag.tProcSwitch b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b_1 f) (0, 0) x✝
• DescriptiveComplexity.QsatTM.treadF DescriptiveComplexity.QsatTM.QTag.tProcAcc x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.treadF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.tdstF : QTag → QTag → qsatOrd.Formula (Fin 2 × Fin 2)

Defining formula for tdst: the only place the instance is consulted is the evaluation sweep, where the new flag depends on the literal test.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.QsatTM.tdstF DescriptiveComplexity.QsatTM.QTag.tDescStart x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tDescCell b f) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tdstF DescriptiveComplexity.QsatTM.QTag.tDescEndTrue x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qProc true) x✝
• DescriptiveComplexity.QsatTM.tdstF DescriptiveComplexity.QsatTM.QTag.tDescEndEval x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.qEval false false) (0, 0) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tTurnNext d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.qEval false !d) (0, 1) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tTurnLast d) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd true) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tTurnFalse d) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd false) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tToEndCell b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd b) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tToEndStart b) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qToEnd b) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tToEndTurn b) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qProc b) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tProcSkip b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qCstF (DescriptiveComplexity.QsatTM.QTag.qProc b) x✝
• DescriptiveComplexity.QsatTM.tdstF (DescriptiveComplexity.QsatTM.QTag.tProcSwitch b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qDesc x✝
• DescriptiveComplexity.QsatTM.tdstF DescriptiveComplexity.QsatTM.QTag.tProcAcc x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.qAcc x✝
• DescriptiveComplexity.QsatTM.tdstF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.twriteF : QTag → QTag → qsatOrd.Formula (Fin 2 × Fin 2)

Defining formula for twrite.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.QsatTM.twriteF DescriptiveComplexity.QsatTM.QTag.tDescStart x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tDescCell b f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal false false) (0, 0) x✝
• DescriptiveComplexity.QsatTM.twriteF DescriptiveComplexity.QsatTM.QTag.tDescEndTrue x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.twriteF DescriptiveComplexity.QsatTM.QTag.tDescEndEval x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tEval b f fl d) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b f) (0, 1) x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tToEndCell b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b_1 f) (0, 0) x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tToEndStart b) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tToEndTurn b) x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sEnd x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tProcSkip b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal b_1 f) (0, 0) x✝
• DescriptiveComplexity.QsatTM.twriteF (DescriptiveComplexity.QsatTM.QTag.tProcSwitch b b_1 f) x✝ = DescriptiveComplexity.QsatTM.qOneF (DescriptiveComplexity.QsatTM.QTag.sVal true true) (0, 0) x✝
• DescriptiveComplexity.QsatTM.twriteF DescriptiveComplexity.QsatTM.QTag.tProcAcc x✝ = DescriptiveComplexity.QsatTM.qCstF DescriptiveComplexity.QsatTM.QTag.sStart x✝
• DescriptiveComplexity.QsatTM.twriteF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.QsatTM.qsatTuringInterp : FOInterpretation qsatOrd FirstOrder.Language.turing QTag 2

The interpretation of the machine vocabulary in an ordered QSAT instance.

Equations

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

Each formula defines its predicate

def DescriptiveComplexity.QsatTM.qsatMapEquiv {A : Type} : QV A ≃ qsatTuringInterp.Map A

The identity equivalence between the tagged tuples and the interpreted universe.

Equations

• DescriptiveComplexity.QsatTM.qsatMapEquiv = Equiv.refl (DescriptiveComplexity.QsatTM.QV A)

theorem DescriptiveComplexity.QsatTM.relMap_posn {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p : QV A) : TMPosn (qsatMapEquiv p) ↔ QPosn p

theorem DescriptiveComplexity.QsatTM.relMap_start {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p : QV A) : TMStart (qsatMapEquiv p) ↔ QStart p

theorem DescriptiveComplexity.QsatTM.relMap_acc {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p : QV A) : TMAcc (qsatMapEquiv p) ↔ QAcc p

theorem DescriptiveComplexity.QsatTM.relMap_blank {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p : QV A) : TMBlank (qsatMapEquiv p) ↔ QBlank p

theorem DescriptiveComplexity.QsatTM.relMap_right {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p : QV A) : TMRight (qsatMapEquiv p) ↔ QRight p

theorem DescriptiveComplexity.QsatTM.relMap_le {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p q : QV A) : TMLe (qsatMapEquiv p) (qsatMapEquiv q) ↔ QLe p q

theorem DescriptiveComplexity.QsatTM.qInp_pStart_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : QV A} : QInp (QTag.pStart, w) a ↔ a = qCst QTag.sStart

theorem DescriptiveComplexity.QsatTM.qInp_pCell_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : QV A} : QInp (QTag.pCell, w) a ↔ a = qOne (QTag.sVal false false) (w 0)

theorem DescriptiveComplexity.QsatTM.qInp_pEnd_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : QV A} : QInp (QTag.pEnd, w) a ↔ a = qCst QTag.sEnd

theorem DescriptiveComplexity.QsatTM.relMap_inp {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : QV A) : TMInp (qsatMapEquiv p) (qsatMapEquiv q) ↔ QInp p q

theorem DescriptiveComplexity.QsatTM.relMap_tsrc {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : QV A) : TMSrc (qsatMapEquiv p) (qsatMapEquiv q) ↔ QSrc p q

theorem DescriptiveComplexity.QsatTM.relMap_tread {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : QV A) : TMRead (qsatMapEquiv p) (qsatMapEquiv q) ↔ QRead p q

theorem DescriptiveComplexity.QsatTM.relMap_twrite {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : QV A) : TMWrite (qsatMapEquiv p) (qsatMapEquiv q) ↔ QWrite p q

theorem DescriptiveComplexity.QsatTM.relMap_tr {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] (p : QV A) : TMTr (qsatMapEquiv p) ↔ QTr p

theorem DescriptiveComplexity.QsatTM.relMap_tdst {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : QV A) : TMDst (qsatMapEquiv p) (qsatMapEquiv q) ↔ QDst p q

The reduction

theorem DescriptiveComplexity.QsatTM.agree_qsatMachine {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TMData.Agree qsatMapEquiv.symm (tmData (qsatTuringInterp.Map A)) (qsatMachine A)

The interpreted structure describes the machine of the instance.

theorem DescriptiveComplexity.QsatTM.dtmAcceptSpace_map_iff {A : Type} [FirstOrder.Language.qsat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : DTMAcceptSpace.Holds (qsatTuringInterp.Map A) ↔ QsatHolds A

The image is a yes-instance exactly when the formula is true.

noncomputable def DescriptiveComplexity.QsatTM.qsat_ordered_fo_reduction_dtmAcceptSpace : OrderedFOReduction QSAT DTMAcceptSpace

QSAT ≤ᶠᵒ[≤] DTMAcceptSpace: the deterministic space-bounded machine that evaluates a quantified Boolean formula, built inside its instance.

Equations

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