The interpretation of the Savitch reduction

The defining formulas of the reduction of SUCCINCT-REACH to QSAT, and the resulting first-order interpretation DescriptiveComplexity.qsatInterp, of dimension 2 over the ordered expansion of FirstOrder.Language.transSys.

Every relation of FirstOrder.Language.qsat is defined by a formula that only depends on the tags of its arguments, and each of those formulas is read off the tables of DescriptiveComplexity.Problems.Qsat.Tags:

• DescriptiveComplexity.varF and DescriptiveComplexity.clF are the marks DescriptiveComplexity.QVarOn and DescriptiveComplexity.QClOn;
• DescriptiveComplexity.occF collects, from the fixed literal list DescriptiveComplexity.qLits of a clause tag, those literals that are on the variable tag and sign asked for – so a single generic realization lemma (DescriptiveComplexity.realize_occF) replaces a case analysis on all pairs of tags;
• DescriptiveComplexity.prefF is the lexicographic comparison DescriptiveComplexity.KeyLt of the two keys, built from static numerals and two order atoms.

The section “Characterization of the interpreted relations” reads each of them back through DescriptiveComplexity.FOInterpretation.relMap_map; those lemmas are the only interface the correctness proof uses.

The formula builders of the reduction

They live in their own namespace: short names like leF or occF are what every reduction of the library calls its builders, and the umbrella DescriptiveComplexity.Problems imports them all at once.

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.transOrd : FirstOrder.Language

The ordered expansion of the vocabulary of transition systems: the source vocabulary of the reduction.

Equations

• DescriptiveComplexity.QsatRed.transOrd = FirstOrder.Language.transSys.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.svSym : transOrd.Relations 1

The symbol for “is a state variable”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.svSym = Sum.inl FirstOrder.Language.tsStateVar

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.srcSym : transOrd.Relations 1

The symbol for “is a source clause”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.srcSym = Sum.inl FirstOrder.Language.tsSrcCl

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.tgtSym : transOrd.Relations 1

The symbol for “is a target clause”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.tgtSym = Sum.inl FirstOrder.Language.tsTgtCl

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.stepSym : transOrd.Relations 1

The symbol for “is a transition clause”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.stepSym = Sum.inl FirstOrder.Language.tsStepCl

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.nxtSym : transOrd.Relations 2

The symbol for “is the next-state copy of”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.nxtSym = Sum.inl FirstOrder.Language.tsNext

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.pSym : transOrd.Relations 2

The symbol for “occurs positively in”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.pSym = Sum.inl FirstOrder.Language.tsPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.nSym : transOrd.Relations 2

The symbol for “occurs negatively in”, in the ordered expansion.

Equations

• DescriptiveComplexity.QsatRed.nSym = Sum.inl FirstOrder.Language.tsNegIn

Atomic formula builders

def DescriptiveComplexity.QsatRed.svF {α : Type} (x : α) : transOrd.Formula α

x is a state variable, as a formula.

Equations

• DescriptiveComplexity.QsatRed.svF x = DescriptiveComplexity.QsatRed.svSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatRed.srcF {α : Type} (c : α) : transOrd.Formula α

c is a source clause, as a formula.

Equations

• DescriptiveComplexity.QsatRed.srcF c = DescriptiveComplexity.QsatRed.srcSym.formula₁ (FirstOrder.Language.var c)

def DescriptiveComplexity.QsatRed.tgtF {α : Type} (c : α) : transOrd.Formula α

c is a target clause, as a formula.

Equations

• DescriptiveComplexity.QsatRed.tgtF c = DescriptiveComplexity.QsatRed.tgtSym.formula₁ (FirstOrder.Language.var c)

def DescriptiveComplexity.QsatRed.stepF {α : Type} (c : α) : transOrd.Formula α

c is a transition clause, as a formula.

Equations

• DescriptiveComplexity.QsatRed.stepF c = DescriptiveComplexity.QsatRed.stepSym.formula₁ (FirstOrder.Language.var c)

def DescriptiveComplexity.QsatRed.nxtF {α : Type} (x y : α) : transOrd.Formula α

y is the next-state copy of x, as a formula.

Equations

• DescriptiveComplexity.QsatRed.nxtF x y = DescriptiveComplexity.QsatRed.nxtSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.QsatRed.posF {α : Type} (c x : α) : transOrd.Formula α

x occurs positively in c, as a formula.

Equations

• DescriptiveComplexity.QsatRed.posF c x = DescriptiveComplexity.QsatRed.pSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatRed.negF {α : Type} (c x : α) : transOrd.Formula α

x occurs negatively in c, as a formula.

Equations

• DescriptiveComplexity.QsatRed.negF c x = DescriptiveComplexity.QsatRed.nSym.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.QsatRed.leF {α : Type} (x y : α) : transOrd.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.QsatRed.leF x y = FirstOrder.Language.leSymb.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.QsatRed.eqF {α : Type} (x y : α) : transOrd.Formula α

x = y, as a formula.

Equations

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

def DescriptiveComplexity.QsatRed.ltF {α : Type} (x y : α) : transOrd.Formula α

x < y, as a formula.

Equations

• DescriptiveComplexity.QsatRed.ltF x y = DescriptiveComplexity.QsatRed.leF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.QsatRed.eqF x y)

noncomputable def DescriptiveComplexity.QsatRed.isBotF {α : Type} (x : α) : transOrd.Formula α

x is a minimum of the input order, as a formula.

Equations

• DescriptiveComplexity.QsatRed.isBotF x = DescriptiveComplexity.botF x

noncomputable def DescriptiveComplexity.QsatRed.minSVF {α : Type} (x : α) : transOrd.Formula α

x is the first state variable, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.QsatRed.maxSVF {α : Type} (x : α) : transOrd.Formula α

x is the last state variable, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.QsatRed.predSVF {α : Type} (x y : α) : transOrd.Formula α

x is the state variable just above the state variable y, as a formula.

Equations

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

Realization of the atomic builders

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_svF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x : α} : (svF x).Realize V ↔ IsSV (V x)

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_srcF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {c : α} : (srcF c).Realize V ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsSrcCl ![V c]

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_tgtF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {c : α} : (tgtF c).Realize V ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsTgtCl ![V c]

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_stepF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {c : α} : (stepF c).Realize V ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsStepCl ![V c]

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_nxtF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x y : α} : (nxtF x y).Realize V ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNext ![V x, V y]

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_posF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {c x : α} : (posF c x).Realize V ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![V c, V x]

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_negF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {c x : α} : (negF c x).Realize V ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![V c, V x]

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_leF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x y : α} : (leF x y).Realize V ↔ V x ≤ V y

@[simp]

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

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_ltF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x y : α} : (ltF x y).Realize V ↔ V x < V y

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_isBotF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x : α} : (isBotF x).Realize V ↔ IsBot (V x)

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_minSVF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x : α} : (minSVF x).Realize V ↔ IsMinSV (V x)

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_maxSVF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x : α} : (maxSVF x).Realize V ↔ IsMaxSV (V x)

@[simp]

theorem DescriptiveComplexity.QsatRed.realize_predSVF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {α : Type} {V : α → A} {x y : α} : (predSVF x y).Realize V ↔ IsPredSV (V x) (V y)

The defining formulas

noncomputable def DescriptiveComplexity.QsatRed.varF {α : Type} : QVarTag → α → α → transOrd.Formula α

The mark of a variable tag, as a formula in its two coordinates.

Equations

• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sS = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sT = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sB = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sZ = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.svF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sU = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.svF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sV = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.svF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.aS = fun (x q : α) => DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.aT = fun (x q : α) => DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.aP = fun (x q : α) => DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.varF DescriptiveComplexity.QVarTag.sE = fun (p q : α) => DescriptiveComplexity.QsatRed.isBotF p ⊓ DescriptiveComplexity.QsatRed.isBotF q

noncomputable def DescriptiveComplexity.QsatRed.clF {α : Type} : QClTag → α → α → transOrd.Formula α

The guard of a clause tag, as a formula in its two coordinates.

Equations

• DescriptiveComplexity.QsatRed.clF DescriptiveComplexity.QClTag.cSrc = fun (p q : α) => DescriptiveComplexity.QsatRed.srcF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF DescriptiveComplexity.QClTag.cTgt = fun (p q : α) => DescriptiveComplexity.QsatRed.tgtF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF DescriptiveComplexity.QClTag.cStep = fun (p q : α) => DescriptiveComplexity.QsatRed.stepF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF (DescriptiveComplexity.QClTag.lS a) = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF (DescriptiveComplexity.QClTag.lT a) = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF (DescriptiveComplexity.QClTag.lU a) = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF (DescriptiveComplexity.QClTag.lV a) = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.nxtF p q
• DescriptiveComplexity.QsatRed.clF (DescriptiveComplexity.QClTag.bE a) = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.isBotF q
• DescriptiveComplexity.QsatRed.clF (DescriptiveComplexity.QClTag.lev a a_1 a_2) = fun (p q : α) => DescriptiveComplexity.QsatRed.svF p ⊓ DescriptiveComplexity.QsatRed.svF q

noncomputable def DescriptiveComplexity.QsatRed.allF {α : Type} (v : QVarTag) (p q : α) : transOrd.Formula α

The mark of the universally quantified variables: only the bits b_ℓ.

Equations

• DescriptiveComplexity.QsatRed.allF v p q = if v = DescriptiveComplexity.QVarTag.sB then DescriptiveComplexity.QsatRed.varF v p q else ⊥

noncomputable def DescriptiveComplexity.QsatRed.natLexF {α : Type} (a b : ℕ) (φ : transOrd.Formula α) : transOrd.Formula α

A static component of a lexicographic comparison decides by itself, unless the two values are equal.

Equations

• DescriptiveComplexity.QsatRed.natLexF a b φ = if a < b then ⊤ else if b < a then ⊥ else φ

theorem DescriptiveComplexity.QsatRed.realize_varF {α A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {V : α → A} {v : QVarTag} {p q : α} : (varF v p q).Realize V ↔ QVarOn v (V p) (V q)

theorem DescriptiveComplexity.QsatRed.realize_allF {α A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {V : α → A} {v : QVarTag} {p q : α} : (allF v p q).Realize V ↔ v = QVarTag.sB ∧ QVarOn v (V p) (V q)

theorem DescriptiveComplexity.QsatRed.realize_clF {α A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {V : α → A} {c : QClTag} {p q : α} : (clF c p q).Realize V ↔ QClOn c (V p) (V q)

theorem DescriptiveComplexity.QsatRed.realize_natLexF {α A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {V : α → A} {a b : ℕ} {φ : transOrd.Formula α} {P : Prop} (h : φ.Realize V ↔ P) : (natLexF a b φ).Realize V ↔ a < b ∨ a = b ∧ P

The coordinates of a two-argument defining formula

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.x₀ : Fin 2 × Fin 2

The first coordinate of the first argument.

Equations

• DescriptiveComplexity.QsatRed.x₀ = (0, 0)

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.y₀ : Fin 2 × Fin 2

The second coordinate of the first argument.

Equations

• DescriptiveComplexity.QsatRed.y₀ = (0, 1)

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.x₁ : Fin 2 × Fin 2

The first coordinate of the second argument.

Equations

• DescriptiveComplexity.QsatRed.x₁ = (1, 0)

@[reducible, inline]

abbrev DescriptiveComplexity.QsatRed.y₁ : Fin 2 × Fin 2

The second coordinate of the second argument.

Equations

• DescriptiveComplexity.QsatRed.y₁ = (1, 1)

noncomputable def DescriptiveComplexity.QsatRed.linkF : QLink → transOrd.Formula (Fin 2 × Fin 2)

Where a literal's variable sits, as a formula in the four coordinates.

Equations

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

theorem DescriptiveComplexity.QsatRed.realize_linkF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {k : QLink} {V : Fin 2 × Fin 2 → A} : (linkF k).Realize V ↔ LinkOn k (V x₀) (V y₀) (V x₁) (V y₁)

noncomputable def DescriptiveComplexity.QsatRed.occF (sgn : Bool) (ct : QClTag) (vt : QVarTag) : transOrd.Formula (Fin 2 × Fin 2)

The occurrence formula: the literals of the clause tag ct that are on the variable tag vt with the sign sgn, gathered into a disjunction.

Equations

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

theorem DescriptiveComplexity.QsatRed.realize_occF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {sgn : Bool} {ct : QClTag} {vt : QVarTag} {V : Fin 2 × Fin 2 → A} : (occF sgn ct vt).Realize V ↔ ∃ l ∈ qLits ct, l.vt = vt ∧ l.sign = sgn ∧ QClOn ct (V x₀) (V y₀) ∧ QVarOn vt (V x₁) (V y₁) ∧ LinkOn l.link (V x₀) (V y₀) (V x₁) (V y₁)

The prefix formula

def DescriptiveComplexity.QsatRed.KeyLtRaw {A : Type} [LinearOrder A] (g : ℕ) (l : A) (s : ℕ) (c : A) (o g' : ℕ) (l' : A) (s' : ℕ) (c' : A) (o' : ℕ) : Prop

The lexicographic comparison of two keys, spelled out: the static components decide by themselves, the two dynamic ones by an order atom.

Equations

• DescriptiveComplexity.QsatRed.KeyLtRaw g l s c o g' l' s' c' o' = (g < g' ∨ g = g' ∧ (l < l' ∨ l = l' ∧ (s < s' ∨ s = s' ∧ (c < c' ∨ c = c' ∧ o < o'))))

theorem DescriptiveComplexity.QsatRed.keyLt_iff_raw {A : Type} [LinearOrder A] (v v' : QVarTag) (p q p' q' : A) : KeyLt v p q v' p' q' ↔ KeyLtRaw (keyGrp v) (keyLev v p q) (keySlot v) (keySec v p q) (keyOrd v) (keyGrp v') (keyLev v' p' q') (keySlot v') (keySec v' p' q') (keyOrd v')

noncomputable def DescriptiveComplexity.QsatRed.keyBodyF (v v' : QVarTag) (lv sc lv' sc' : Fin 2 × Fin 2) : transOrd.Formula (Fin 2 × Fin 2)

The body of the prefix comparison, with the four coordinates selected.

Equations

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

theorem DescriptiveComplexity.QsatRed.realize_keyBodyF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {v v' : QVarTag} {lv sc lv' sc' : Fin 2 × Fin 2} {V : Fin 2 × Fin 2 → A} : (keyBodyF v v' lv sc lv' sc').Realize V ↔ KeyLtRaw (keyGrp v) (V lv) (keySlot v) (V sc) (keyOrd v) (keyGrp v') (V lv') (keySlot v') (V sc') (keyOrd v')

noncomputable def DescriptiveComplexity.QsatRed.prefF (v v' : QVarTag) : transOrd.Formula (Fin 2 × Fin 2)

The quantifier prefix, as a formula: both arguments are variables, and their keys compare lexicographically.

Equations

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

theorem DescriptiveComplexity.QsatRed.realize_prefF {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {v v' : QVarTag} {V : Fin 2 × Fin 2 → A} : (prefF v v').Realize V ↔ QVarOn v (V x₀) (V y₀) ∧ QVarOn v' (V x₁) (V y₁) ∧ KeyLt v (V x₀) (V y₀) v' (V x₁) (V y₁)

The interpretation

noncomputable def DescriptiveComplexity.qsatInterp : FOInterpretation QsatRed.transOrd FirstOrder.Language.qsat QTag 2

The Savitch interpretation: the QSAT instance whose prefix and matrix express reachability in the transition system described by the input, by recursive doubling.

Equations

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

Characterization of the interpreted relations

@[reducible, inline]

abbrev DescriptiveComplexity.QM (A : Type) [FirstOrder.Language.transSys.Structure A] [LinearOrder A] : Type

The universe of the constructed instance: a tag together with a pair of elements of the input.

Equations

• DescriptiveComplexity.QM A = DescriptiveComplexity.qsatInterp.Map A

instance DescriptiveComplexity.instFiniteQM {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] : Finite (QM A)

instance DescriptiveComplexity.instNonemptyQM {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Nonempty A] : Nonempty (QM A)

theorem DescriptiveComplexity.qsat_isVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (w : Fin 2 → A) : IsQVar (Sum.inl v, w) ↔ QVarOn v (w 0) (w 1)

The variables: the marked tagged pairs.

theorem DescriptiveComplexity.qsat_not_isVar {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (w : Fin 2 → A) : ¬IsQVar (Sum.inr c, w)

Elements carrying a clause tag are not variables.

theorem DescriptiveComplexity.qsat_isAll {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (w : Fin 2 → A) : IsQAll (Sum.inl v, w) ↔ v = QVarTag.sB ∧ QVarOn v (w 0) (w 1)

The universal variables: only the bits b_ℓ.

theorem DescriptiveComplexity.qsat_not_isAll {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {v : QVarTag} (hv : v ≠ QVarTag.sB) (w : Fin 2 → A) : ¬IsQAll (Sum.inl v, w)

Every variable tag other than sB is existential.

theorem DescriptiveComplexity.qsat_not_isAll_cl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (w : Fin 2 → A) : ¬IsQAll (Sum.inr c, w)

Elements carrying a clause tag are not universal.

theorem DescriptiveComplexity.qsat_isClause {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (w : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsClause ![(Sum.inr c, w)] ↔ QClOn c (w 0) (w 1)

The clauses: the guarded tagged pairs.

theorem DescriptiveComplexity.qsat_not_isClause {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (w : Fin 2 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsIsClause ![(Sum.inl v, w)]

Elements carrying a variable tag are not clauses.

theorem DescriptiveComplexity.qsat_prec {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v v' : QVarTag) (w w' : Fin 2 → A) : QPrec (Sum.inl v, w) (Sum.inl v', w') ↔ QVarOn v (w 0) (w 1) ∧ QVarOn v' (w' 0) (w' 1) ∧ KeyLt v (w 0) (w 1) v' (w' 0) (w' 1)

The prefix order relates two variables exactly as their keys compare.

theorem DescriptiveComplexity.qsat_not_prec_left {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (x : QM A) (w : Fin 2 → A) : ¬QPrec (Sum.inr c, w) x

The prefix order does not relate a clause on the left.

theorem DescriptiveComplexity.qsat_not_prec_right {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (x : QM A) (w : Fin 2 → A) : ¬QPrec x (Sum.inr c, w)

The prefix order does not relate a clause on the right.

theorem DescriptiveComplexity.qsat_posIn {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (v : QVarTag) (w y : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPosIn ![(Sum.inr c, w), (Sum.inl v, y)] ↔ ∃ l ∈ qLits c, l.vt = v ∧ l.sign = true ∧ QClOn c (w 0) (w 1) ∧ QVarOn v (y 0) (y 1) ∧ LinkOn l.link (w 0) (w 1) (y 0) (y 1)

The positive literals of a clause: the literals of its list that are on the given variable tag with a positive sign, and whose link pins that variable's coordinates.

theorem DescriptiveComplexity.qsat_negIn {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (c : QClTag) (v : QVarTag) (w y : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsNegIn ![(Sum.inr c, w), (Sum.inl v, y)] ↔ ∃ l ∈ qLits c, l.vt = v ∧ l.sign = false ∧ QClOn c (w 0) (w 1) ∧ QVarOn v (y 0) (y 1) ∧ LinkOn l.link (w 0) (w 1) (y 0) (y 1)

The negative literals of a clause.

theorem DescriptiveComplexity.qsat_not_posIn_cl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (x : QM A) (c : QClTag) (y : Fin 2 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPosIn ![x, (Sum.inr c, y)]

No literal is on an element carrying a clause tag.

theorem DescriptiveComplexity.qsat_not_negIn_cl {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (x : QM A) (c : QClTag) (y : Fin 2 → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsNegIn ![x, (Sum.inr c, y)]

No literal is on an element carrying a clause tag, negatively.

theorem DescriptiveComplexity.qsat_not_posIn_var {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (w : Fin 2 → A) (x : QM A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsPosIn ![(Sum.inl v, w), x]

An element carrying a variable tag has no literals.

theorem DescriptiveComplexity.qsat_not_negIn_var {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (v : QVarTag) (w : Fin 2 → A) (x : QM A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.qsNegIn ![(Sum.inl v, w), x]

An element carrying a variable tag has no negative literals.