Deciding reachability in a walk: Immerman–Szelepcsényi with parameters

The atom case of the normal form for FO(TC): the reachability relation of a parameterized walk (DescriptiveComplexity.ParamTCSpec) has a DescriptiveComplexity.Decider (DescriptiveComplexity.ParamTCSpec.reachDecider). Its yes exit is the walk itself, run from the first endpoint until it stands on the second; its no exit is the inductive-counting walk of DescriptiveComplexity.TransitiveClosureCompl, which certifies that the second endpoint is not reached.

Parameters as constants

The complement construction is stated for a sentence: a DescriptiveComplexity.TCSpec, whose source and target formulas have no free variables beyond the tuple. What is needed here is the complement of a relation – the parameters of the walk and its two endpoints are free. The two are reconciled without touching the 950 lines of the counting machine: the free variables become constants of the vocabulary (FirstOrder.Language.withConstants), the walk becomes a sentence over the enlarged vocabulary (DescriptiveComplexity.ParamTCSpec.constSpec), the complement is taken there, and its formulas are read back with the constants as variables (DescriptiveComplexity.fromConst). Mathlib's FirstOrder.Language.BoundedFormula.constantsVarsEquiv is the bridge, in both directions, and a structure interprets the constants by the valuation of the parameters (DescriptiveComplexity.constStructure).

Formulas with parameters, as sentences with constants

@[reducible, inline]

abbrev DescriptiveComplexity.withPar (L₀ : FirstOrder.Language) (γ : Type) : FirstOrder.Language

The vocabulary with one constant per parameter.

Equations

• DescriptiveComplexity.withPar L₀ γ = L₀.withConstants γ

noncomputable def DescriptiveComplexity.collapseOrder (L₀ : FirstOrder.Language) (γ : Type) : (withPar (L₀.sum FirstOrder.Language.order) γ).sum FirstOrder.Language.order →ᴸ withPar (L₀.sum FirstOrder.Language.order) γ

The vocabulary map reading the second copy of the order, in the ordered expansion of the vocabulary with constants, as the first.

Equations

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

noncomputable def DescriptiveComplexity.toConst {L₀ : FirstOrder.Language} {γ β : Type} (φ : (L₀.sum FirstOrder.Language.order).Formula (γ ⊕ β)) : ((withPar (L₀.sum FirstOrder.Language.order) γ).sum FirstOrder.Language.order).Formula β

A formula with parameters, as a formula over the vocabulary with constants, over its ordered expansion.

Equations

• DescriptiveComplexity.toConst φ = FirstOrder.Language.LHom.sumInl.onFormula (FirstOrder.Language.BoundedFormula.constantsVarsEquiv.symm φ)

noncomputable def DescriptiveComplexity.fromConst {L₀ : FirstOrder.Language} {γ β : Type} (φ : ((withPar (L₀.sum FirstOrder.Language.order) γ).sum FirstOrder.Language.order).Formula β) : (L₀.sum FirstOrder.Language.order).Formula (γ ⊕ β)

A formula over the ordered expansion of the vocabulary with constants, as a formula with parameters.

Equations

• DescriptiveComplexity.fromConst φ = FirstOrder.Language.BoundedFormula.constantsVarsEquiv ((DescriptiveComplexity.collapseOrder L₀ γ).onFormula φ)

@[instance_reducible]

noncomputable def DescriptiveComplexity.constStructure {L₀ : FirstOrder.Language} {γ A : Type} [L₀.Structure A] [LinearOrder A] (c : γ → A) : (withPar (L₀.sum FirstOrder.Language.order) γ).Structure A

The structure over the vocabulary with constants, the constants read by a valuation of the parameters.

Equations

• DescriptiveComplexity.constStructure c = inferInstance

theorem DescriptiveComplexity.realize_toConst {L₀ : FirstOrder.Language} {γ A : Type} [L₀.Structure A] [LinearOrder A] {β : Type} (c : γ → A) (φ : (L₀.sum FirstOrder.Language.order).Formula (γ ⊕ β)) (u : β → A) : (toConst φ).Realize u ↔ φ.Realize (Sum.elim c u)

theorem DescriptiveComplexity.realize_fromConst {L₀ : FirstOrder.Language} {γ A : Type} [L₀.Structure A] [LinearOrder A] {β : Type} (c : γ → A) (φ : ((withPar (L₀.sum FirstOrder.Language.order) γ).sum FirstOrder.Language.order).Formula β) (u : β → A) : (fromConst φ).Realize (Sum.elim c u) ↔ φ.Realize u

A parameterized walk, as a sentence over the vocabulary with constants

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.AtomPar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : Type

The parameters of the reachability atom of a walk: the two endpoints and the walk's own parameters, packed as DescriptiveComplexity.ParamTCSpec.pack does.

Equations

• W.AtomPar = Fin (W.k + W.k + W.par)

def DescriptiveComplexity.ParamTCSpec.constStepVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : (Fin W.k ⊕ Fin W.k) ⊕ Fin W.par → W.AtomPar ⊕ Fin W.k ⊕ Fin W.k

The variables of the step formula, the walk's parameters read off the atom's parameters.

Equations

• W.constStepVar (Sum.inl p) = Sum.inr p
• W.constStepVar (Sum.inr j) = Sum.inl (W.parIx j)

noncomputable def DescriptiveComplexity.ParamTCSpec.eqLeftF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : (L.sum FirstOrder.Language.order).Formula (W.AtomPar ⊕ Fin W.k)

“The tuple is the first endpoint.”

Equations

• W.eqLeftF = FirstOrder.Language.Formula.iInf fun (i : Fin W.k) => (FirstOrder.Language.var (Sum.inr i)).equal (FirstOrder.Language.var (Sum.inl (W.leftIx i)))

noncomputable def DescriptiveComplexity.ParamTCSpec.eqRightF {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) : (L.sum FirstOrder.Language.order).Formula (W.AtomPar ⊕ Fin W.k)

“The tuple is the second endpoint.”

Equations

• W.eqRightF = FirstOrder.Language.Formula.iInf fun (i : Fin W.k) => (FirstOrder.Language.var (Sum.inr i)).equal (FirstOrder.Language.var (Sum.inl (W.rightIx i)))

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.constSpec {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : TCSpec (withPar (L.sum FirstOrder.Language.order) W.AtomPar)

The walk as a sentence over the vocabulary with one constant per parameter of the atom: the same walk, whose sources are the first endpoint in the first mode and whose targets are the second endpoint in the second mode. Reducible: a node of it is a node of the walk.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.constSpec_step {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (a b : W.Node A) : (W.constSpec ma mb).Step a b ↔ W.StepAt (w ∘ W.parIx) a b

theorem DescriptiveComplexity.ParamTCSpec.constSpec_isSrc {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (a : W.Node A) : (W.constSpec ma mb).IsSrc a ↔ a.1 = ma ∧ a.2 = w ∘ W.leftIx

theorem DescriptiveComplexity.ParamTCSpec.constSpec_isTgt {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (a : W.Node A) : (W.constSpec ma mb).IsTgt a ↔ a.1 = mb ∧ a.2 = w ∘ W.rightIx

theorem DescriptiveComplexity.ParamTCSpec.constSpec_reach {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) (a b : W.Node A) : (W.constSpec ma mb).Reach a b ↔ W.ReachAt (w ∘ W.parIx) a b

theorem DescriptiveComplexity.ParamTCSpec.constSpec_accepts {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) : (W.constSpec ma mb).Accepts A ↔ W.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx)

The sentence says reachability between the two endpoints.

The complement, with parameters

noncomputable def DescriptiveComplexity.ParamTCSpec.coSpec {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : TCSpec (withPar (L.sum FirstOrder.Language.order) W.AtomPar)

The complement of the walk between two endpoints, with parameters: the inductive-counting walk of DescriptiveComplexity.TCCompl.complSpec run on the sentence with constants.

Equations

• W.coSpec ma mb = DescriptiveComplexity.TCCompl.complSpec (W.constSpec ma mb).pad

theorem DescriptiveComplexity.ParamTCSpec.coSpec_accepts {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] (ma mb : W.Mode) (w : W.AtomPar → A) [Finite A] [Nonempty A] : (W.coSpec ma mb).Accepts A ↔ ¬W.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx)

The complement accepts exactly when the second endpoint is not reached.

The decider

def DescriptiveComplexity.ParamTCSpec.yesVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : (Fin W.k ⊕ Fin W.k) ⊕ Fin W.par → ((Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ W.AtomPar

The variables of the walk's step, in the decider's.

Equations

• W.yesVar ma mb (Sum.inl (Sum.inl i)) = Sum.inl (Sum.inl (Sum.inl i))
• W.yesVar ma mb (Sum.inl (Sum.inr i)) = Sum.inl (Sum.inr (Sum.inl i))
• W.yesVar ma mb (Sum.inr j) = Sum.inr (W.parIx j)

def DescriptiveComplexity.ParamTCSpec.noVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : W.AtomPar ⊕ Fin (W.coSpec ma mb).k ⊕ Fin (W.coSpec ma mb).k → ((Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ W.AtomPar

The variables of the complement's step, in the decider's.

Equations

• W.noVar ma mb (Sum.inl g) = Sum.inr g
• W.noVar ma mb (Sum.inr (Sum.inl i)) = Sum.inl (Sum.inl (Sum.inr i))
• W.noVar ma mb (Sum.inr (Sum.inr i)) = Sum.inl (Sum.inr (Sum.inr i))

def DescriptiveComplexity.ParamTCSpec.coSrcVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : W.AtomPar ⊕ Fin (W.coSpec ma mb).k → ((Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ W.AtomPar

The variables of the complement's source formula, read on the next tuple of the decider's step.

Equations

• W.coSrcVar ma mb (Sum.inl g) = Sum.inr g
• W.coSrcVar ma mb (Sum.inr i) = Sum.inl (Sum.inr (Sum.inr i))

def DescriptiveComplexity.ParamTCSpec.coExitVar {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : W.AtomPar ⊕ Fin (W.coSpec ma mb).k → (Fin W.k ⊕ Fin (W.coSpec ma mb).k) ⊕ W.AtomPar

The variables of the complement's target formula, in the decider's exit.

Equations

• W.coExitVar ma mb (Sum.inl g) = Sum.inr g
• W.coExitVar ma mb (Sum.inr i) = Sum.inl (Sum.inr i)

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.reachDecider {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) (ma mb : W.Mode) : Decider L W.AtomPar

The decider of reachability between two modes, at the two endpoints and the parameters: from its start it either enters the walk at the first endpoint and exits yes on standing at the second, or enters the complement walk at one of its sources and exits no at one of its targets. The coordinates of the idle branch are copied along.

Equations

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

Steps and exits

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_stepAt_none_inl {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (m : W.Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).StepAt w (none, t) (some (Sum.inl m), t') ↔ m = ma ∧ t' ∘ Sum.inl = w ∘ W.leftIx ∧ t' ∘ Sum.inr = t ∘ Sum.inr

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_stepAt_none_inr {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (c : (W.coSpec ma mb).Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).StepAt w (none, t) (some (Sum.inr c), t') ↔ (W.coSpec ma mb).IsSrc (c, t' ∘ Sum.inr) ∧ t' ∘ Sum.inl = t ∘ Sum.inl

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_stepAt_inl_inl {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (m n : W.Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).StepAt w (some (Sum.inl m), t) (some (Sum.inl n), t') ↔ W.StepAt (w ∘ W.parIx) (m, t ∘ Sum.inl) (n, t' ∘ Sum.inl) ∧ t' ∘ Sum.inr = t ∘ Sum.inr

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_stepAt_inr_inr {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (c c' : (W.coSpec ma mb).Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).StepAt w (some (Sum.inr c), t) (some (Sum.inr c'), t') ↔ (W.coSpec ma mb).Step (c, t ∘ Sum.inr) (c', t' ∘ Sum.inr) ∧ t' ∘ Sum.inl = t ∘ Sum.inl

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_stepAt_none_none {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : ¬(W.reachDecider ma mb).StepAt w (none, t) (none, t')

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_stepAt_some_none {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (m : W.Mode ⊕ (W.coSpec ma mb).Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : ¬(W.reachDecider ma mb).StepAt w (some m, t) (none, t')

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_stepAt_inl_inr {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (m : W.Mode) (c : (W.coSpec ma mb).Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : ¬(W.reachDecider ma mb).StepAt w (some (Sum.inl m), t) (some (Sum.inr c), t')

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_stepAt_inr_inl {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (c : (W.coSpec ma mb).Mode) (m : W.Mode) (t t' : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : ¬(W.reachDecider ma mb).StepAt w (some (Sum.inr c), t) (some (Sum.inl m), t')

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_exitAt_inl_true {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (m : W.Mode) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).ExitAt w (some (Sum.inl m), t) true ↔ m = mb ∧ t ∘ Sum.inl = w ∘ W.rightIx

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_exitAt_inl_false {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (m : W.Mode) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : ¬(W.reachDecider ma mb).ExitAt w (some (Sum.inl m), t) false

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_exitAt_inr_false {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (c : (W.coSpec ma mb).Mode) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).ExitAt w (some (Sum.inr c), t) false ↔ (W.coSpec ma mb).IsTgt (c, t ∘ Sum.inr)

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_exitAt_inr_true {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (c : (W.coSpec ma mb).Mode) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) : ¬(W.reachDecider ma mb).ExitAt w (some (Sum.inr c), t) true

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_not_exitAt_none {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) (o : Bool) : ¬(W.reachDecider ma mb).ExitAt w (none, t) o

Lifting the two walks

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_reachAt_of_reachAt {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) {a b : W.Node A} (h : W.ReachAt (w ∘ W.parIx) a b) (r : Fin (W.coSpec ma mb).k → A) : (W.reachDecider ma mb).ReachAt w (some (Sum.inl a.1), Sum.elim a.2 r) (some (Sum.inl b.1), Sum.elim b.2 r)

A path of the walk lifts to the yes branch.

theorem DescriptiveComplexity.ParamTCSpec.reachDecider_reachAt_of_coReach {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) {a b : (W.coSpec ma mb).Node A} (h : (W.coSpec ma mb).Reach a b) (l : Fin W.k → A) : (W.reachDecider ma mb).ReachAt w (some (Sum.inr a.1), Sum.elim l a.2) (some (Sum.inr b.1), Sum.elim l b.2)

A path of the complement lifts to the no branch.

def DescriptiveComplexity.ParamTCSpec.ReachInv {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) (c : (W.reachDecider ma mb).Node A) : Prop

What the decider may have reached: its start, a node of the walk reached from the first endpoint, or a node of the complement reached from one of its sources.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.reachInv_of_reachAt {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) (t : Fin W.k ⊕ Fin (W.coSpec ma mb).k → A) {c : (W.reachDecider ma mb).Node A} (h : (W.reachDecider ma mb).ReachAt w (none, t) c) : W.ReachInv w t c

theorem DescriptiveComplexity.ParamTCSpec.decides_reachDecider {L : FirstOrder.Language} (W : ParamTCSpec (L.sum FirstOrder.Language.order)) {A : Type} [L.Structure A] [LinearOrder A] {ma mb : W.Mode} (w : W.AtomPar → A) [Finite A] [Nonempty A] : (W.reachDecider ma mb).Decides w (W.ReachAt (w ∘ W.parIx) (ma, w ∘ W.leftIx) (mb, w ∘ W.rightIx))

The decider decides reachability between its two modes, at the two endpoints and the parameters.

The deciders of a family

noncomputable def DescriptiveComplexity.TCFamily.reachDeciders {L : FirstOrder.Language} (F : TCFamily (L.sum FirstOrder.Language.order)) (q : F.block.ι) : Decider L (Fin (F.block.arity q))

The reachability deciders of a family: one per relation variable of its block.

Equations

• F.reachDeciders q = (F.spec q.fst).reachDecider q.snd.1 q.snd.2

theorem DescriptiveComplexity.TCFamily.decides_reachDeciders {L : FirstOrder.Language} (F : TCFamily (L.sum FirstOrder.Language.order)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (q : F.block.ι) (w : Fin (F.block.arity q) → A) : (F.reachDeciders q).Decides w (F.reachAssign A q w)

The deciders decide the family's reachability relations.