FO(TC) is closed under complement

Immerman–Szelepcsényi, as a theorem about the logic: on finite ordered structures, the complement of an FO(TC) definable problem is FO(TC) definable (Immerman 1988, Szelepcsényi 1988).

The proof runs the inductive-counting machine of DescriptiveComplexity.InductiveCounting inside a single transitive closure. The machine's nodes are the nodes of the given DescriptiveComplexity.TCSpec, linearly ordered mode-major by the order of the structure; its configurations are a finite control together with eight registers, each holding a node or a count, and each stored as one k-tuple of elements beside a mode kept in the control. So a configuration is a mode together with a 8k-tuple, which is exactly what a TCSpec of arity 8k can walk on.

The one thing the translation must supply is the formulas: each atomic constraint of DescriptiveComplexity.InductiveCounting.VAtom becomes, given the modes recorded by the two control states, either a first-order formula over the two tuples or the information that no tuples can satisfy it (compileAtom). Since the modes are finite control data, every mode-level condition – "these two registers hold the same mode", "this mode is the least one", "this mode is covered by that one" – is decided outside the formula, and what remains for the formula is a condition on tuples of elements: equality, the lexicographic minimum, maximum or successor (DescriptiveComplexity.OrderWalk), or one of the given spec's own formulas.

Padding a specification with a spare mode

noncomputable def DescriptiveComplexity.TCSpec.pad {L : FirstOrder.Language} (spec : TCSpec L) : TCSpec L

The specification with one spare, isolated mode added, so that the mode type is nonempty: the new mode has no transitions and is neither a source nor a target.

Equations

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

instance DescriptiveComplexity.TCSpec.instNonemptyPadMode {L : FirstOrder.Language} (spec : TCSpec L) : Nonempty spec.pad.Mode

theorem DescriptiveComplexity.TCSpec.pad_accepts_iff {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) [L.Structure A] [LinearOrder A] : spec.pad.Accepts A ↔ spec.Accepts A

Padding does not change acceptance.

The nodes of a specification as a finite linear order

@[reducible, inline]

abbrev DescriptiveComplexity.TCCompl.NodeOrd {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) : Type

The nodes of the walk, ordered mode-major and then lexicographically on tuples.

Equations

• DescriptiveComplexity.TCCompl.NodeOrd spec A = Lex (spec.Mode × Lex (Fin spec.k → A))

def DescriptiveComplexity.TCCompl.toNode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (z : NodeOrd spec A) : spec.Node A

The node underlying an ordered node.

Equations

• DescriptiveComplexity.TCCompl.toNode z = ((ofLex z).1, ofLex (ofLex z).2)

def DescriptiveComplexity.TCCompl.ofNode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (n : spec.Node A) : NodeOrd spec A

The ordered node of a node.

Equations

• DescriptiveComplexity.TCCompl.ofNode n = toLex (n.1, toLex n.2)

@[simp]

theorem DescriptiveComplexity.TCCompl.toNode_ofNode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (n : spec.Node A) : toNode (ofNode n) = n

@[simp]

theorem DescriptiveComplexity.TCCompl.ofNode_toNode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (z : NodeOrd spec A) : ofNode (toNode z) = z

def DescriptiveComplexity.TCCompl.edge {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (z z' : NodeOrd spec A) : Prop

The edges of the walk, on ordered nodes.

Equations

• DescriptiveComplexity.TCCompl.edge z z' = spec.Step (DescriptiveComplexity.TCCompl.toNode z) (DescriptiveComplexity.TCCompl.toNode z')

def DescriptiveComplexity.TCCompl.src {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (z : NodeOrd spec A) : Prop

The starting nodes of the walk, on ordered nodes.

Equations

• DescriptiveComplexity.TCCompl.src z = spec.IsSrc (DescriptiveComplexity.TCCompl.toNode z)

def DescriptiveComplexity.TCCompl.tgt {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (z : NodeOrd spec A) : Prop

The accepting nodes of the walk, on ordered nodes.

Equations

• DescriptiveComplexity.TCCompl.tgt z = spec.IsTgt (DescriptiveComplexity.TCCompl.toNode z)

theorem DescriptiveComplexity.TCCompl.reach_of_edge {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {z z' : NodeOrd spec A} (h : Relation.ReflTransGen edge z z') : spec.Reach (toNode z) (toNode z')

theorem DescriptiveComplexity.TCCompl.edge_of_reach {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {u v : spec.Node A} (h : spec.Reach u v) : Relation.ReflTransGen edge (ofNode u) (ofNode v)

theorem DescriptiveComplexity.TCCompl.exists_reach_iff {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) [L.Structure A] [LinearOrder A] : (∃ (a : NodeOrd spec A) (b : NodeOrd spec A), src a ∧ tgt b ∧ Relation.ReflTransGen edge a b) ↔ spec.Accepts A

Acceptance of the specification, read on the ordered nodes.

Registers inside one tuple

@[reducible, inline]

abbrev DescriptiveComplexity.TCCompl.dim {L : FirstOrder.Language} (spec : TCSpec L) : ℕ

The arity of the complement specification: eight registers of k elements each.

Equations

• DescriptiveComplexity.TCCompl.dim spec = 8 * spec.k

@[reducible, inline]

abbrev DescriptiveComplexity.TCCompl.Var {L : FirstOrder.Language} (spec : TCSpec L) : Type

The variables of a transition formula: two tuples of that arity.

Equations

• DescriptiveComplexity.TCCompl.Var spec = (Fin (DescriptiveComplexity.TCCompl.dim spec) ⊕ Fin (DescriptiveComplexity.TCCompl.dim spec))

def DescriptiveComplexity.TCCompl.regIdx {L : FirstOrder.Language} (spec : TCSpec L) (r : InductiveCounting.Reg) (i : Fin spec.k) : Fin (dim spec)

The variable holding coordinate i of register r.

Equations

• DescriptiveComplexity.TCCompl.regIdx spec r i = finProdFinEquiv (r, i)

def DescriptiveComplexity.TCCompl.slotSel {L : FirstOrder.Language} (spec : TCSpec L) : InductiveCounting.Slot → Fin spec.k → Var spec

The variables holding the tuple a slot reads.

Equations

• DescriptiveComplexity.TCCompl.slotSel spec (false, r) = fun (i : Fin spec.k) => Sum.inl (DescriptiveComplexity.TCCompl.regIdx spec r i)
• DescriptiveComplexity.TCCompl.slotSel spec (true, r) = fun (i : Fin spec.k) => Sum.inr (DescriptiveComplexity.TCCompl.regIdx spec r i)

def DescriptiveComplexity.TCCompl.regTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (x : Fin (dim spec) → A) (r : InductiveCounting.Reg) : Fin spec.k → A

The tuple a register holds inside a tuple of the walk.

Equations

• DescriptiveComplexity.TCCompl.regTup x r i = x (DescriptiveComplexity.TCCompl.regIdx spec r i)

def DescriptiveComplexity.TCCompl.mkTup {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (f : InductiveCounting.Reg → Fin spec.k → A) : Fin (dim spec) → A

Assembling the eight registers into one tuple.

Equations

• DescriptiveComplexity.TCCompl.mkTup spec f q = f (finProdFinEquiv.symm q).1 (finProdFinEquiv.symm q).2

@[simp]

theorem DescriptiveComplexity.TCCompl.regTup_mkTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (f : InductiveCounting.Reg → Fin spec.k → A) (r : InductiveCounting.Reg) : regTup (mkTup spec f) r = f r

def DescriptiveComplexity.TCCompl.slotTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (x y : Fin (dim spec) → A) : InductiveCounting.Slot → Fin spec.k → A

The tuple a slot reads, from the two tuples of a transition.

Equations

• DescriptiveComplexity.TCCompl.slotTup x y (false, r) = DescriptiveComplexity.TCCompl.regTup x r
• DescriptiveComplexity.TCCompl.slotTup x y (true, r) = DescriptiveComplexity.TCCompl.regTup y r

theorem DescriptiveComplexity.TCCompl.realize_slotSel {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (x y : Fin (dim spec) → A) (a : InductiveCounting.Slot) (i : Fin spec.k) : Sum.elim x y (slotSel spec a i) = slotTup x y a i

The formulas of the atomic constraints

noncomputable def DescriptiveComplexity.TCCompl.eqTupF {L : FirstOrder.Language} (spec : TCSpec L) (a b : InductiveCounting.Slot) : (L.sum FirstOrder.Language.order).Formula (Var spec)

Two slots hold the same tuple.

Equations

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

noncomputable def DescriptiveComplexity.TCCompl.stepF {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) (a b : InductiveCounting.Slot) : (L.sum FirstOrder.Language.order).Formula (Var spec)

The two slots hold tuples joined by a transition of the given modes.

Equations

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

noncomputable def DescriptiveComplexity.TCCompl.srcF {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) (a : InductiveCounting.Slot) : (L.sum FirstOrder.Language.order).Formula (Var spec)

The slot holds a starting tuple of the given mode.

Equations

• DescriptiveComplexity.TCCompl.srcF spec m a = FirstOrder.Language.Formula.relabel (DescriptiveComplexity.TCCompl.slotSel spec a) (spec.src m)

noncomputable def DescriptiveComplexity.TCCompl.tgtF {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) (a : InductiveCounting.Slot) : (L.sum FirstOrder.Language.order).Formula (Var spec)

The slot holds an accepting tuple of the given mode.

Equations

• DescriptiveComplexity.TCCompl.tgtF spec m a = FirstOrder.Language.Formula.relabel (DescriptiveComplexity.TCCompl.slotSel spec a) (spec.tgt m)

theorem DescriptiveComplexity.TCCompl.realize_eqTupF {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (a b : InductiveCounting.Slot) : (eqTupF spec a b).Realize (Sum.elim x y) ↔ slotTup x y a = slotTup x y b

theorem DescriptiveComplexity.TCCompl.realize_stepF {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (m m' : spec.Mode) (a b : InductiveCounting.Slot) : (stepF spec m m' a b).Realize (Sum.elim x y) ↔ spec.Step (m, slotTup x y a) (m', slotTup x y b)

theorem DescriptiveComplexity.TCCompl.realize_srcF {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (m : spec.Mode) (a : InductiveCounting.Slot) : (srcF spec m a).Realize (Sum.elim x y) ↔ spec.IsSrc (m, slotTup x y a)

theorem DescriptiveComplexity.TCCompl.realize_tgtF {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (m : spec.Mode) (a : InductiveCounting.Slot) : (tgtF spec m a).Realize (Sum.elim x y) ↔ spec.IsTgt (m, slotTup x y a)

theorem DescriptiveComplexity.TCCompl.realize_minTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (a : InductiveCounting.Slot) : (minTupF (slotSel spec a)).Realize (Sum.elim x y) ↔ ∀ (p : Fin spec.k) (z : A), slotTup x y a p ≤ z

theorem DescriptiveComplexity.TCCompl.realize_maxTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (a : InductiveCounting.Slot) : (maxTupF (slotSel spec a)).Realize (Sum.elim x y) ↔ ∀ (p : Fin spec.k) (z : A), z ≤ slotTup x y a p

theorem DescriptiveComplexity.TCCompl.realize_succTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (x y : Fin (dim spec) → A) (a b : InductiveCounting.Slot) : (succTupF (slotSel spec a) (slotSel spec b)).Realize (Sum.elim x y) ↔ TupSucc (slotTup x y a) (slotTup x y b)

Register values

def DescriptiveComplexity.TCCompl.fuse {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} (om : Option spec.Mode) (t : Fin spec.k → A) : WithBot (NodeOrd spec A)

The value of a register: ⊥ when the control records no mode, the node made of the mode and the tuple otherwise.

Equations

• DescriptiveComplexity.TCCompl.fuse spec none t = ⊥
• DescriptiveComplexity.TCCompl.fuse spec (some m) t = ↑(DescriptiveComplexity.TCCompl.ofNode (m, t))

theorem DescriptiveComplexity.TCCompl.fuse_none {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (t : Fin spec.k → A) : fuse spec none t = ⊥

theorem DescriptiveComplexity.TCCompl.fuse_some {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (m : spec.Mode) (t : Fin spec.k → A) : fuse spec (some m) t = ↑(ofNode (m, t))

theorem DescriptiveComplexity.TCCompl.fuse_eq_iff {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} {m m' : spec.Mode} {t t' : Fin spec.k → A} : fuse spec (some m) t = fuse spec (some m') t' ↔ m = m' ∧ t = t'

theorem DescriptiveComplexity.TCCompl.fuse_ne_bot {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} {m : spec.Mode} {t : Fin spec.k → A} : fuse spec (some m) t ≠ ⊥

theorem DescriptiveComplexity.TCCompl.covBy_fuse {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [LinearOrder A] [Nonempty A] {m m' : spec.Mode} {t t' : Fin spec.k → A} : fuse spec (some m) t ⋖ fuse spec (some m') t' ↔ m = m' ∧ TupSucc t t' ∨ m ⋖ m' ∧ (∀ (p : Fin spec.k) (z : A), z ≤ t p) ∧ ∀ (p : Fin spec.k) (z : A), t' p ≤ z

theorem DescriptiveComplexity.TCCompl.bot_covBy_fuse {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [LinearOrder A] {m : spec.Mode} {t : Fin spec.k → A} : ⊥ ⋖ fuse spec (some m) t ↔ (∀ (m' : spec.Mode), m ≤ m') ∧ ∀ (p : Fin spec.k) (z : A), t p ≤ z

theorem DescriptiveComplexity.TCCompl.eW_fuse {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {m m' : spec.Mode} {t t' : Fin spec.k → A} : InductiveCounting.EW edge (fuse spec (some m) t) (fuse spec (some m') t') ↔ spec.Step (m, t) (m', t')

theorem DescriptiveComplexity.TCCompl.eW_fuse_none_left {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {om : Option spec.Mode} {t t' : Fin spec.k → A} : ¬InductiveCounting.EW edge (fuse spec none t) (fuse spec om t')

theorem DescriptiveComplexity.TCCompl.eW_fuse_none_right {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] {om : Option spec.Mode} {t t' : Fin spec.k → A} : ¬InductiveCounting.EW edge (fuse spec om t) (fuse spec none t')

theorem DescriptiveComplexity.TCCompl.pW_fuse {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} {P : NodeOrd spec A → Prop} {m : spec.Mode} {t : Fin spec.k → A} : InductiveCounting.PW P (fuse spec (some m) t) ↔ P (ofNode (m, t))

theorem DescriptiveComplexity.TCCompl.pW_fuse_none {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} {P : NodeOrd spec A → Prop} {t : Fin spec.k → A} : ¬InductiveCounting.PW P (fuse spec none t)

theorem DescriptiveComplexity.TCCompl.pW_fuse_isMin {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [LinearOrder A] {m : spec.Mode} {t : Fin spec.k → A} : InductiveCounting.PW (fun (p : NodeOrd spec A) => ∀ (z : NodeOrd spec A), p ≤ z) (fuse spec (some m) t) ↔ (∀ (m' : spec.Mode), m ≤ m') ∧ ∀ (p : Fin spec.k) (z : A), t p ≤ z

theorem DescriptiveComplexity.TCCompl.pW_fuse_isMax {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [LinearOrder A] {m : spec.Mode} {t : Fin spec.k → A} : InductiveCounting.PW (fun (p : NodeOrd spec A) => ∀ (z : NodeOrd spec A), z ≤ p) (fuse spec (some m) t) ↔ (∀ (m' : spec.Mode), m' ≤ m) ∧ ∀ (p : Fin spec.k) (z : A), z ≤ t p

Compiling an atomic constraint

def DescriptiveComplexity.TCCompl.slotMode {L : FirstOrder.Language} (spec : TCSpec L) (pm qm : InductiveCounting.Reg → Option spec.Mode) : InductiveCounting.Slot → Option spec.Mode

The mode a slot reads, from the modes the two control states record.

Equations

• DescriptiveComplexity.TCCompl.slotMode spec pm qm (false, r) = pm r
• DescriptiveComplexity.TCCompl.slotMode spec pm qm (true, r) = qm r

noncomputable def DescriptiveComplexity.TCCompl.compileAtom {L : FirstOrder.Language} (spec : TCSpec L) [LinearOrder spec.Mode] (pm qm : InductiveCounting.Reg → Option spec.Mode) : InductiveCounting.VAtom → Option ((L.sum FirstOrder.Language.order).Formula (Var spec))

The formula of an atomic constraint, given the modes recorded by the two control states: none when those modes already make the constraint unsatisfiable. Every mode-level condition is decided here, outside the formula.

Equations

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

def DescriptiveComplexity.TCCompl.regsOf {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (pm : InductiveCounting.Reg → Option spec.Mode) (x : Fin (dim spec) → A) : InductiveCounting.Reg → WithBot (NodeOrd spec A)

The registers a control state and a tuple describe.

Equations

• DescriptiveComplexity.TCCompl.regsOf pm x r = DescriptiveComplexity.TCCompl.fuse spec (pm r) (DescriptiveComplexity.TCCompl.regTup x r)

theorem DescriptiveComplexity.TCCompl.slotVal_regsOf {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (pm qm : InductiveCounting.Reg → Option spec.Mode) (x y : Fin (dim spec) → A) (a : InductiveCounting.Slot) : InductiveCounting.slotVal (regsOf pm x) (regsOf qm y) a = fuse spec (slotMode spec pm qm a) (slotTup x y a)

theorem DescriptiveComplexity.TCCompl.ofNode_eq_iff {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} {m m' : spec.Mode} {t t' : Fin spec.k → A} : ofNode (m, t) = ofNode (m', t') ↔ m = m' ∧ t = t'

theorem DescriptiveComplexity.TCCompl.holds_iff_compileAtom {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (pm qm : InductiveCounting.Reg → Option spec.Mode) (x y : Fin (dim spec) → A) (a : InductiveCounting.VAtom) : InductiveCounting.VAtom.Holds edge src tgt (regsOf pm x) (regsOf qm y) a ↔ ∃ (f : (L.sum FirstOrder.Language.order).Formula (Var spec)), compileAtom spec pm qm a = some f ∧ f.Realize (Sum.elim x y)

The atomic constraints are first-order: given the modes, an atomic constraint holds of the registers exactly when its compiled formula holds of the tuples.

Compiling a table entry

noncomputable def DescriptiveComplexity.TCCompl.compileConj {L : FirstOrder.Language} (spec : TCSpec L) [LinearOrder spec.Mode] (pm qm : InductiveCounting.Reg → Option spec.Mode) : List InductiveCounting.VAtom → Option ((L.sum FirstOrder.Language.order).Formula (Var spec))

The formula of one alternative: the conjunction of its atomic constraints.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.TCCompl.compileConj spec pm qm [] = some ⊤

noncomputable def DescriptiveComplexity.TCCompl.compileDisj {L : FirstOrder.Language} (spec : TCSpec L) [LinearOrder spec.Mode] (pm qm : InductiveCounting.Reg → Option spec.Mode) (ls : List (List InductiveCounting.VAtom)) : (L.sum FirstOrder.Language.order).Formula (Var spec)

The formula of a table entry: the disjunction of its satisfiable alternatives.

Equations

• DescriptiveComplexity.TCCompl.compileDisj spec pm qm ls = DescriptiveComplexity.listSup (List.filterMap (DescriptiveComplexity.TCCompl.compileConj spec pm qm) ls)

theorem DescriptiveComplexity.TCCompl.sat_iff_compileConj {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (pm qm : InductiveCounting.Reg → Option spec.Mode) (x y : Fin (dim spec) → A) (l : List InductiveCounting.VAtom) : InductiveCounting.Sat edge src tgt (regsOf pm x) (regsOf qm y) l ↔ ∃ (f : (L.sum FirstOrder.Language.order).Formula (Var spec)), compileConj spec pm qm l = some f ∧ f.Realize (Sum.elim x y)

theorem DescriptiveComplexity.TCCompl.exists_sat_iff_compileDisj {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (pm qm : InductiveCounting.Reg → Option spec.Mode) (x y : Fin (dim spec) → A) (ls : List (List InductiveCounting.VAtom)) : (∃ l ∈ ls, InductiveCounting.Sat edge src tgt (regsOf pm x) (regsOf qm y) l) ↔ (compileDisj spec pm qm ls).Realize (Sum.elim x y)

The complement specification

@[reducible, inline]

abbrev DescriptiveComplexity.TCCompl.Ctrl {L : FirstOrder.Language} (spec : TCSpec L) : Type

The control states of the counting machine: a phase, the flag, and the mode of each of the eight registers.

Equations

• DescriptiveComplexity.TCCompl.Ctrl spec = (DescriptiveComplexity.InductiveCounting.Phase × Bool × (DescriptiveComplexity.InductiveCounting.Reg → Option spec.Mode))

noncomputable def DescriptiveComplexity.TCCompl.srcFormula {L : FirstOrder.Language} (spec : TCSpec L) [LinearOrder spec.Mode] (p : Ctrl spec) : (L.sum FirstOrder.Language.order).Formula (Fin (dim spec))

The formula defining the initial configurations: the source scan is about to start with a zero count and the outer register at the least node.

Equations

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

noncomputable def DescriptiveComplexity.TCCompl.complSpec {L : FirstOrder.Language} (spec : TCSpec L) [LinearOrder spec.Mode] : TCSpec L

The complement specification: the inductive-counting machine, as a single transitive closure over 8k-tuples.

Equations

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

def DescriptiveComplexity.TCCompl.toCfg {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} (n : (complSpec spec).Node A) : InductiveCounting.Cfg (NodeOrd spec A)

The configuration a node of the complement specification describes.

Equations

• DescriptiveComplexity.TCCompl.toCfg n = { phase := n.1.1, flag := n.1.2.1, regs := DescriptiveComplexity.TCCompl.regsOf n.1.2.2 n.2 }

noncomputable def DescriptiveComplexity.TCCompl.splitMode {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (w : WithBot (NodeOrd spec A)) : Option spec.Mode

The mode a register value records.

Equations

• DescriptiveComplexity.TCCompl.splitMode none = none
• DescriptiveComplexity.TCCompl.splitMode (some z) = some (DescriptiveComplexity.TCCompl.toNode z).1

noncomputable def DescriptiveComplexity.TCCompl.splitTup {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [Nonempty A] (w : WithBot (NodeOrd spec A)) : Fin spec.k → A

The tuple a register value records.

Equations

• DescriptiveComplexity.TCCompl.splitTup none = fun (x : Fin spec.k) => Classical.arbitrary A
• DescriptiveComplexity.TCCompl.splitTup (some z) = (DescriptiveComplexity.TCCompl.toNode z).2

theorem DescriptiveComplexity.TCCompl.fuse_split {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [Nonempty A] (w : WithBot (NodeOrd spec A)) : fuse spec (splitMode w) (splitTup w) = w

noncomputable def DescriptiveComplexity.TCCompl.ofCfg {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [Nonempty A] (s : InductiveCounting.Cfg (NodeOrd spec A)) : (complSpec spec).Node A

Every configuration comes from a node of the complement specification.

Equations

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

theorem DescriptiveComplexity.TCCompl.toCfg_ofCfg {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [Nonempty A] (s : InductiveCounting.Cfg (NodeOrd spec A)) : toCfg (ofCfg s) = s

theorem DescriptiveComplexity.TCCompl.step_iff {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (n n' : (complSpec spec).Node A) : (complSpec spec).Step n n' ↔ InductiveCounting.CfgStep edge src tgt (toCfg n) (toCfg n')

theorem DescriptiveComplexity.TCCompl.cfgReach_of_reach {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {n n' : (complSpec spec).Node A} (h : (complSpec spec).Reach n n') : InductiveCounting.CfgReach edge src tgt (toCfg n) (toCfg n')

theorem DescriptiveComplexity.TCCompl.reach_of_cfgReach {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {n : (complSpec spec).Node A} {s : InductiveCounting.Cfg (NodeOrd spec A)} (h : InductiveCounting.CfgReach edge src tgt (toCfg n) s) : ∃ (n' : (complSpec spec).Node A), toCfg n' = s ∧ (complSpec spec).Reach n n'

theorem DescriptiveComplexity.TCCompl.regsOf_eq_bot_iff {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} (pm : InductiveCounting.Reg → Option spec.Mode) (x : Fin (dim spec) → A) (r : InductiveCounting.Reg) : regsOf pm x r = ⊥ ↔ pm r = none

theorem DescriptiveComplexity.TCCompl.realize_srcFormula {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] (p : Ctrl spec) (x : Fin (dim spec) → A) : (srcFormula spec p).Realize x ↔ p.1 = InductiveCounting.Phase.initCount ∧ p.2.1 = false ∧ p.2.2 InductiveCounting.Reg.c = none ∧ ∃ (m : spec.Mode), p.2.2 InductiveCounting.Reg.v = some m ∧ (∀ (m' : spec.Mode), m ≤ m') ∧ ∀ (i : Fin spec.k) (z : A), x (regIdx spec InductiveCounting.Reg.v i) ≤ z

theorem DescriptiveComplexity.TCCompl.isSrc_iff {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] (n : (complSpec spec).Node A) : (complSpec spec).IsSrc n ↔ InductiveCounting.CfgIsSrc (toCfg n)

theorem DescriptiveComplexity.TCCompl.realize_tgtFormula {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] (p : Ctrl spec) (x : Fin (dim spec) → A) : ((complSpec spec).tgt p).Realize x ↔ p.1 = InductiveCounting.Phase.accept

theorem DescriptiveComplexity.TCCompl.isTgt_iff {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] (n : (complSpec spec).Node A) : (complSpec spec).IsTgt n ↔ InductiveCounting.CfgIsTgt (toCfg n)

theorem DescriptiveComplexity.TCCompl.accepts_iff {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] : (complSpec spec).Accepts A ↔ InductiveCounting.MachineAccepts edge src tgt

theorem DescriptiveComplexity.TCCompl.complSpec_accepts_iff {L : FirstOrder.Language} {spec : TCSpec L} [LinearOrder spec.Mode] {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] [Nonempty spec.Mode] [Finite A] : (complSpec spec).Accepts A ↔ ¬spec.Accepts A

The complement specification is correct: it accepts exactly the structures the given specification rejects.