Flattening a walk whose steps are decided: the suspension

The nested case of the normal form for FO(TC): a walk over an expansion – whose step formulas read the reachability relations of other walks – becomes a walk over the base vocabulary (DescriptiveComplexity.ParamTCSpec.flat), given a DescriptiveComplexity.Decider for each of its step formulas. The outer walk is suspended at a node, the decider of the step to a candidate successor is run, and where it exits yes the outer walk resumes at that successor.

Two ways to pick the candidate

• Guessing (det := false): the candidate is chosen nondeterministically. Reachability in the flat walk is then reachability in the outer one (DescriptiveComplexity.ParamTCSpec.reachAt_flat_iff), for any outer walk.
• Searching (det := true): the candidates are tried in the mode-major lexicographic order of nodes, the next one after a no. The flat walk is then functional when the deciders are (DescriptiveComplexity.ParamTCSpec.functional_flat), and it simulates the outer walk provided that one is functional (DescriptiveComplexity.ParamTCSpec.reachAt_flat_iff_of_functional) – as the deterministic reading of a walk is.

A node of the outer walk is encoded with the candidate and every decider's coordinates at the minimum (DescriptiveComplexity.ParamTCSpec.flatEnc), which is where the walk resumes after a yes; this is what makes the encoding a bijection onto the outer nodes the flat walk can stand on.

The flat walk carries its coordinates as a type rather than an arity (DescriptiveComplexity.CoordWalk), the coordinates of the deciders being a dependent sum over the pairs of modes; DescriptiveComplexity.CoordWalk.toParam enumerates them for the DescriptiveComplexity.ParamTCSpec the rest of the development consumes.

Walks with a type of coordinates

structure DescriptiveComplexity.CoordWalk (L : FirstOrder.Language) : Type 1

A parameterized walk whose coordinates are an arbitrary finite type.

• Mode : Type

  The modes.

• modeFinite : Finite self.Mode

  Modes are finite.

• Coord : Type

  The coordinates.

• coordFinite : Finite self.Coord

  Tuples are finite.

• par : ℕ

  The number of parameters.

• step : self.Mode → self.Mode → L.Formula ((self.Coord ⊕ self.Coord) ⊕ Fin self.par)

  The step formula, one per pair of modes.

@[reducible, inline]

abbrev DescriptiveComplexity.CoordWalk.Node {L : FirstOrder.Language} (C : CoordWalk L) (A : Type) : Type

A node: a mode and a tuple.

Equations

• C.Node A = (C.Mode × (C.Coord → A))

def DescriptiveComplexity.CoordWalk.StepAt {L : FirstOrder.Language} (C : CoordWalk L) {A : Type} [L.Structure A] (z : Fin C.par → A) (a b : C.Node A) : Prop

One step, at a valuation of the parameters.

Equations

• C.StepAt z a b = (C.step a.1 b.1).Realize (Sum.elim (Sum.elim a.2 b.2) z)

@[reducible, inline]

abbrev DescriptiveComplexity.CoordWalk.ReachAt {L : FirstOrder.Language} (C : CoordWalk L) {A : Type} [L.Structure A] (z : Fin C.par → A) : C.Node A → C.Node A → Prop

Reachability, at a valuation of the parameters.

Equations

• C.ReachAt z = Relation.ReflTransGen (C.StepAt z)

def DescriptiveComplexity.CoordWalk.Functional {L : FirstOrder.Language} (C : CoordWalk L) (A : Type) [L.Structure A] : Prop

The walk is functional when no node has two successors.

Equations

• C.Functional A = ∀ (z : Fin C.par → A) (a b c : C.Node A), C.StepAt z a b → C.StepAt z a c → b = c

noncomputable def DescriptiveComplexity.CoordWalk.coordEquiv {L : FirstOrder.Language} (C : CoordWalk L) : C.Coord ≃ Fin (Nat.card C.Coord)

The coordinates, enumerated.

Equations

• C.coordEquiv = (Fintype.equivFin C.Coord).trans (finCongr ⋯)

@[reducible]

noncomputable def DescriptiveComplexity.CoordWalk.toParam {L : FirstOrder.Language} (C : CoordWalk L) : ParamTCSpec L

The walk with its coordinates enumerated, as a DescriptiveComplexity.ParamTCSpec. Reducible, so that its modes and parameters are those of the walk transparently.

Equations

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

The flat walk

@[instance_reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.outerModeOrder {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) : LinearOrder S.Mode

An arbitrary linear order on the modes of the outer walk, for the search.

Equations

• S.outerModeOrder = DescriptiveComplexity.finiteLinearOrder S.Mode

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.FlatCoord {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) : Type

The coordinates of the flat walk: the current tuple and the candidate, then the coordinates of every decider.

Equations

• S.FlatCoord D = ((Fin S.k ⊕ Fin S.k) ⊕ (p : S.Mode × S.Mode) × (D p.1 p.2).Coord)

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.FlatMode {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) : Type

The modes of the flat walk: a mode of the outer walk, or a pair of modes with a mode of their decider.

Equations

• S.FlatMode D = (S.Mode ⊕ (p : S.Mode × S.Mode) × (D p.1 p.2).Mode)

def DescriptiveComplexity.ParamTCSpec.InSlice {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) (c : S.FlatCoord D) : Prop

A coordinate belongs to the slice of a pair of modes.

Equations

• S.InSlice D p c = ∃ (d : (D p.1 p.2).Coord), c = Sum.inr ⟨p, d⟩

The formulas

def DescriptiveComplexity.ParamTCSpec.flatRunVar {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) : ((D p.1 p.2).Coord ⊕ (D p.1 p.2).Coord) ⊕ (Fin S.k ⊕ Fin S.k) ⊕ Fin S.par → (S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par

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

Equations

• S.flatRunVar D p (Sum.inl (Sum.inl c)) = Sum.inl (Sum.inl (Sum.inr ⟨p, c⟩))
• S.flatRunVar D p (Sum.inl (Sum.inr c)) = Sum.inl (Sum.inr (Sum.inr ⟨p, c⟩))
• S.flatRunVar D p (Sum.inr (Sum.inl q)) = Sum.inl (Sum.inl (Sum.inl q))
• S.flatRunVar D p (Sum.inr (Sum.inr j)) = Sum.inr j

def DescriptiveComplexity.ParamTCSpec.flatExitVar {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) : (D p.1 p.2).Coord ⊕ (Fin S.k ⊕ Fin S.k) ⊕ Fin S.par → (S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par

The variables of a decider's exit, in the flat walk's step (read on the current tuple).

Equations

• S.flatExitVar D p (Sum.inl c) = Sum.inl (Sum.inl (Sum.inr ⟨p, c⟩))
• S.flatExitVar D p (Sum.inr (Sum.inl q)) = Sum.inl (Sum.inl (Sum.inl q))
• S.flatExitVar D p (Sum.inr (Sum.inr j)) = Sum.inr j

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.fcur {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (c : S.FlatCoord D) : (S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par

The current tuple's coordinate, as a step variable.

Equations

• S.fcur D c = Sum.inl (Sum.inl c)

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.fnext {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (c : S.FlatCoord D) : (S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par

The next tuple's coordinate, as a step variable.

Equations

• S.fnext D c = Sum.inl (Sum.inr c)

noncomputable def DescriptiveComplexity.ParamTCSpec.copyExceptF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

Every coordinate outside a slice is copied.

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.minSlicesF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

Every decider coordinate of the next tuple is at the minimum.

Equations

• S.minSlicesF D = FirstOrder.Language.Formula.iInf fun (c : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) => DescriptiveComplexity.minF (S.fnext D (Sum.inr c))

noncomputable def DescriptiveComplexity.ParamTCSpec.resetF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

The next tuple is the candidate, with everything else at the minimum.

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.copyCurF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

The current tuple is copied.

Equations

• S.copyCurF D = DescriptiveComplexity.copyF (fun (i : Fin S.k) => S.fcur D (Sum.inl (Sum.inl i))) fun (i : Fin S.k) => S.fnext D (Sum.inl (Sum.inl i))

noncomputable def DescriptiveComplexity.ParamTCSpec.candSuccF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (c c' : S.Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

The candidate advances: same mode and the successor tuple, or the next mode with the tuple from the maximum to the minimum.

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.initF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) (p : S.Mode × S.Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

Entering a decider: the current tuple is copied and the decider's coordinates are reset; when searching, the candidate is the least node.

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.runF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) (d d' : (D p.1 p.2).Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

Running a decider: its step on its slice, everything else copied.

Equations

• S.runF D p d d' = FirstOrder.Language.Formula.relabel (S.flatRunVar D p) ((D p.1 p.2).step d d') ⊓ S.copyExceptF D p

noncomputable def DescriptiveComplexity.ParamTCSpec.retF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

Resuming the outer walk: the decider exits yes, and the walk stands on the candidate.

Equations

• S.retF D p d = FirstOrder.Language.Formula.relabel (S.flatExitVar D p) ((D p.1 p.2).exit d true) ⊓ S.resetF D

noncomputable def DescriptiveComplexity.ParamTCSpec.advF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (p' : S.Mode × S.Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

Trying the next candidate: the decider exits no, the candidate advances, and the decider's coordinates are reset.

Equations

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

noncomputable def DescriptiveComplexity.ParamTCSpec.innerF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (p' : S.Mode × S.Mode) (d' : (D p'.1 p'.2).Mode) : (L.sum FirstOrder.Language.order).Formula ((S.FlatCoord D ⊕ S.FlatCoord D) ⊕ Fin S.par)

The step between two decider nodes: the run, or (when searching) an advance to the start of the next candidate's decider.

Equations

• S.innerF D det p d p' d' = (if h : p = p' then S.runF D p d (cast ⋯ d') else ⊥) ⊔ if det = true ∧ d' = (D p'.1 p'.2).start then S.advF D p d p' else ⊥

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.flat {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) (det : Bool) : CoordWalk (L.sum FirstOrder.Language.order)

The flat walk: the outer walk with each step decided in place. Guessing (det = false) or searching (det = true) the candidate.

Equations

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

Tuples of the flat walk

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.tx {L : FirstOrder.Language} {B : SOBlock} {S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)} {D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)} {A : Type} (t : S.FlatCoord D → A) : Fin S.k → A

The current tuple.

Equations

• DescriptiveComplexity.ParamTCSpec.tx t i = t (Sum.inl (Sum.inl i))

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.ty {L : FirstOrder.Language} {B : SOBlock} {S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)} {D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)} {A : Type} (t : S.FlatCoord D → A) : Fin S.k → A

The candidate.

Equations

• DescriptiveComplexity.ParamTCSpec.ty t i = t (Sum.inl (Sum.inr i))

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.tsl {L : FirstOrder.Language} {B : SOBlock} {S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)} {D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)} {A : Type} (t : S.FlatCoord D → A) (p : S.Mode × S.Mode) : (D p.1 p.2).Coord → A

The slice of a pair of modes.

Equations

• DescriptiveComplexity.ParamTCSpec.tsl t p c = t (Sum.inr ⟨p, c⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.dpar {L : FirstOrder.Language} {B : SOBlock} {S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)} {D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)} {A : Type} (t : S.FlatCoord D → A) (z : Fin S.par → A) : (Fin S.k ⊕ Fin S.k) ⊕ Fin S.par → A

The valuation of a decider's parameters: the current tuple, the candidate and the outer parameters.

Equations

• DescriptiveComplexity.ParamTCSpec.dpar t z = Sum.elim (t ∘ Sum.inl) z

def DescriptiveComplexity.ParamTCSpec.flatEnc {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} (det : Bool) (a₀ : A) (a : S.Node A) : (S.flat D det).Node A

The encoding of a node of the outer walk, at a bottom element a₀.

Equations

• S.flatEnc D det a₀ a = (Sum.inl a.1, Sum.elim (Sum.elim a.2 fun (x : Fin S.k) => a₀) fun (x : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) => a₀)

Semantics of the formulas

theorem DescriptiveComplexity.ParamTCSpec.realize_initF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (p : S.Mode × S.Mode) (t t' : S.FlatCoord D → A) : (S.initF D det p).Realize (Sum.elim (Sum.elim t t') z) ↔ (det = true → (∀ (c' : S.Mode), p.2 ≤ c') ∧ ∀ (i : Fin S.k) (a : A), t' (Sum.inl (Sum.inr i)) ≤ a) ∧ tx t' = tx t ∧ ∀ (c : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) (a : A), t' (Sum.inr c) ≤ a

theorem DescriptiveComplexity.ParamTCSpec.realize_runF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (p : S.Mode × S.Mode) (d d' : (D p.1 p.2).Mode) (t t' : S.FlatCoord D → A) : (S.runF D p d d').Realize (Sum.elim (Sum.elim t t') z) ↔ (D p.1 p.2).StepAt (dpar t z) (d, tsl t p) (d', tsl t' p) ∧ ∀ (c : S.FlatCoord D), ¬S.InSlice D p c → t' c = t c

theorem DescriptiveComplexity.ParamTCSpec.realize_exit_relabel {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (o : Bool) (t t' : S.FlatCoord D → A) : (FirstOrder.Language.Formula.relabel (S.flatExitVar D p) ((D p.1 p.2).exit d o)).Realize (Sum.elim (Sum.elim t t') z) ↔ (D p.1 p.2).ExitAt (dpar t z) (d, tsl t p) o

theorem DescriptiveComplexity.ParamTCSpec.realize_retF {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (t t' : S.FlatCoord D → A) : (S.retF D p d).Realize (Sum.elim (Sum.elim t t') z) ↔ (D p.1 p.2).ExitAt (dpar t z) (d, tsl t p) true ∧ tx t' = ty t ∧ (∀ (i : Fin S.k) (a : A), t' (Sum.inl (Sum.inr i)) ≤ a) ∧ ∀ (c : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) (a : A), t' (Sum.inr c) ≤ a

Steps of the flat walk

theorem DescriptiveComplexity.ParamTCSpec.flat_stepAt_inl_inr {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (m : S.Mode) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (t t' : S.FlatCoord D → A) : (S.flat D det).StepAt z (Sum.inl m, t) (Sum.inr ⟨p, d⟩, t') ↔ p.1 = m ∧ d = (D p.1 p.2).start ∧ (det = true → (∀ (c' : S.Mode), p.2 ≤ c') ∧ ∀ (i : Fin S.k) (a : A), t' (Sum.inl (Sum.inr i)) ≤ a) ∧ tx t' = tx t ∧ ∀ (c : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) (a : A), t' (Sum.inr c) ≤ a

theorem DescriptiveComplexity.ParamTCSpec.flat_not_stepAt_inl_inl {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (m n : S.Mode) (t t' : S.FlatCoord D → A) : ¬(S.flat D det).StepAt z (Sum.inl m, t) (Sum.inl n, t')

theorem DescriptiveComplexity.ParamTCSpec.flat_stepAt_inr_inl {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (n : S.Mode) (t t' : S.FlatCoord D → A) : (S.flat D det).StepAt z (Sum.inr ⟨p, d⟩, t) (Sum.inl n, t') ↔ p.2 = n ∧ (D p.1 p.2).ExitAt (dpar t z) (d, tsl t p) true ∧ tx t' = ty t ∧ (∀ (i : Fin S.k) (a : A), t' (Sum.inl (Sum.inr i)) ≤ a) ∧ ∀ (c : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) (a : A), t' (Sum.inr c) ≤ a

Correctness

theorem DescriptiveComplexity.ParamTCSpec.dpar_eq {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} (z : Fin S.par → A) (t : S.FlatCoord D → A) : Sum.elim (Sum.elim (tx t) (ty t)) z = dpar t z

theorem DescriptiveComplexity.ParamTCSpec.tuple_ext {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} {t t' : S.FlatCoord D → A} (hx : tx t' = tx t) (hy : ty t' = ty t) (hs : ∀ (p : S.Mode × S.Mode), tsl t' p = tsl t p) : t' = t

theorem DescriptiveComplexity.ParamTCSpec.tx_flatEnc {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {A : Type} (a₀ : A) (a : S.Node A) : tx (S.flatEnc D det a₀ a).2 = a.2

theorem DescriptiveComplexity.ParamTCSpec.ty_flatEnc {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {det : Bool} {A : Type} (a₀ : A) (a : S.Node A) : ty (S.flatEnc D det a₀ a).2 = fun (x : Fin S.k) => a₀

def DescriptiveComplexity.ParamTCSpec.DecidesSteps {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] [instE : ((L.sum FirstOrder.Language.order).sum B.lang).Structure A] (z : Fin S.par → A) : Prop

The step deciders decide the steps of the outer walk.

Equations

• S.DecidesSteps D z = ∀ (p : S.Mode × S.Mode) (x y : Fin S.k → A), (D p.1 p.2).Decides (Sum.elim (Sum.elim x y) z) (S.StepAt z (p.1, x) (p.2, y))

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.Cand {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (A : Type) [LinearOrder A] : Type

The candidates, ordered.

Equations

• S.Cand A = Lex (S.Mode × Lex (Fin S.k → A))

theorem DescriptiveComplexity.ParamTCSpec.reachAt_flat_iff {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] [instE : ((L.sum FirstOrder.Language.order).sum B.lang).Structure A] {z : Fin S.par → A} [Nonempty A] (hD : S.DecidesSteps D z) {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (a b : S.Node A) : (S.flat D false).ReachAt z (S.flatEnc D false a₀ a) (S.flatEnc D false a₀ b) ↔ S.ReachAt z a b

Guessing simulates the outer walk, at the encodings.

theorem DescriptiveComplexity.ParamTCSpec.reachAt_flat_iff_of_functional {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] [instE : ((L.sum FirstOrder.Language.order).sum B.lang).Structure A] {z : Fin S.par → A} [Nonempty A] [Finite A] (hD : S.DecidesSteps D z) {a₀ : A} (hbot : ∀ (a : A), a₀ ≤ a) (hS : ∀ (a b c : S.Node A), S.StepAt z a b → S.StepAt z a c → b = c) (a b : S.Node A) : (S.flat D true).ReachAt z (S.flatEnc D true a₀ a) (S.flatEnc D true a₀ b) ↔ S.ReachAt z a b

Searching simulates a functional outer walk, at the encodings.

Functionality of the searching flat walk

theorem DescriptiveComplexity.ParamTCSpec.functional_flat {L : FirstOrder.Language} {B : SOBlock} (S : ParamTCSpec ((L.sum FirstOrder.Language.order).sum B.lang)) (D : S.Mode → S.Mode → Decider L ((Fin S.k ⊕ Fin S.k) ⊕ Fin S.par)) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (hDf : ∀ (p : S.Mode × S.Mode), (D p.1 p.2).Functional A) : (S.flat D true).Functional A

The searching flat walk is functional when the deciders are.