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.

theorem DescriptiveComplexity.CoordWalk.stepAt_toParam {L : FirstOrder.Language} (C : CoordWalk L) {A : Type} [L.Structure A] (z : Fin C.par → A) (a b : C.toParam.Node A) : C.toParam.StepAt z a b ↔ C.StepAt z (a.1, a.2 ∘ ⇑C.coordEquiv) (b.1, b.2 ∘ ⇑C.coordEquiv)

theorem DescriptiveComplexity.CoordWalk.reachAt_toParam {L : FirstOrder.Language} (C : CoordWalk L) {A : Type} [L.Structure A] (z : Fin C.par → A) (a b : C.toParam.Node A) : C.toParam.ReachAt z a b ↔ C.ReachAt z (a.1, a.2 ∘ ⇑C.coordEquiv) (b.1, b.2 ∘ ⇑C.coordEquiv)

theorem DescriptiveComplexity.CoordWalk.functional_toParam {L : FirstOrder.Language} (C : CoordWalk L) {A : Type} [L.Structure A] (h : C.Functional A) : C.toParam.Functional A

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

noncomputable def DescriptiveComplexity.ParamTCSpec.setSlice {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) (u : (D p.1 p.2).Coord → A) : S.FlatCoord D → A

A tuple with one slice replaced.

Equations

• DescriptiveComplexity.ParamTCSpec.setSlice t p u (Sum.inl q) = t (Sum.inl q)
• DescriptiveComplexity.ParamTCSpec.setSlice t p u (Sum.inr ⟨q, c⟩) = if h : q = p then u (cast ⋯ c) else t (Sum.inr ⟨q, c⟩)

theorem DescriptiveComplexity.ParamTCSpec.setSlice_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)} {A : Type} (t : S.FlatCoord D → A) (p : S.Mode × S.Mode) (u : (D p.1 p.2).Coord → A) (q : Fin S.k ⊕ Fin S.k) : setSlice t p u (Sum.inl q) = t (Sum.inl q)

theorem DescriptiveComplexity.ParamTCSpec.setSlice_comp_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)} {A : Type} (t : S.FlatCoord D → A) (p : S.Mode × S.Mode) (u : (D p.1 p.2).Coord → A) : setSlice t p u ∘ Sum.inl = t ∘ Sum.inl

theorem DescriptiveComplexity.ParamTCSpec.tsl_setSlice_self {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) (u : (D p.1 p.2).Coord → A) : tsl (setSlice t p u) p = u

theorem DescriptiveComplexity.ParamTCSpec.setSlice_of_not_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)} {A : Type} (t : S.FlatCoord D → A) (p : S.Mode × S.Mode) (u : (D p.1 p.2).Coord → A) (c : S.FlatCoord D) (hc : ¬S.InSlice D p c) : setSlice t p u c = t c

theorem DescriptiveComplexity.ParamTCSpec.dpar_setSlice {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) (u : (D p.1 p.2).Coord → A) (z : Fin S.par → A) : dpar (setSlice t p u) z = dpar t z

theorem DescriptiveComplexity.ParamTCSpec.setSlice_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) : setSlice t p (tsl t p) = t

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_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)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (p : S.Mode × S.Mode) (t t' : S.FlatCoord D → A) : (S.copyExceptF D p).Realize (Sum.elim (Sum.elim t t') z) ↔ ∀ (c : S.FlatCoord D), ¬S.InSlice D p c → t' c = t c

theorem DescriptiveComplexity.ParamTCSpec.realize_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)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (t t' : S.FlatCoord D → A) : (S.minSlicesF D).Realize (Sum.elim (Sum.elim t t') z) ↔ ∀ (c : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) (a : A), t' (Sum.inr c) ≤ a

theorem DescriptiveComplexity.ParamTCSpec.realize_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)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (t t' : S.FlatCoord D → A) : (S.resetF D).Realize (Sum.elim (Sum.elim t t') z) ↔ 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

theorem DescriptiveComplexity.ParamTCSpec.realize_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)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) (t t' : S.FlatCoord D → A) : (S.copyCurF D).Realize (Sum.elim (Sum.elim t t') z) ↔ tx t' = tx t

theorem DescriptiveComplexity.ParamTCSpec.realize_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)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) [Nonempty A] (c c' : S.Mode) (t t' : S.FlatCoord D → A) : (S.candSuccF D c c').Realize (Sum.elim (Sum.elim t t') z) ↔ toLex (c, toLex (ty t)) ⋖ toLex (c', toLex (ty t'))

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

def DescriptiveComplexity.ParamTCSpec.Adv {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) (p' : S.Mode × S.Mode) (t t' : S.FlatCoord D → A) : Prop

The advance, as a relation between the two nodes.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.realize_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)) {A : Type} [L.Structure A] [LinearOrder A] (z : Fin S.par → A) [Nonempty A] (p : S.Mode × S.Mode) (d : (D p.1 p.2).Mode) (p' : S.Mode × S.Mode) (t t' : S.FlatCoord D → A) : (S.advF D p d p').Realize (Sum.elim (Sum.elim t t') z) ↔ S.Adv D z p d p' t t'

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

theorem DescriptiveComplexity.ParamTCSpec.flat_stepAt_inr_inr_same {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) [Nonempty A] (p : S.Mode × S.Mode) (d d' : (D p.1 p.2).Mode) (t t' : S.FlatCoord D → A) : (S.flat D det).StepAt z (Sum.inr ⟨p, d⟩, t) (Sum.inr ⟨p, d'⟩, t') ↔ ((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) ∨ det = true ∧ d' = (D p.1 p.2).start ∧ S.Adv D z p d p t t'

A step between decider nodes of the same pair of modes: the run, or an advance.

theorem DescriptiveComplexity.ParamTCSpec.flat_stepAt_inr_inr_ne {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) [Nonempty A] {p p' : S.Mode × S.Mode} (hne : p ≠ p') (d : (D p.1 p.2).Mode) (d' : (D p'.1 p'.2).Mode) (t t' : S.FlatCoord D → A) : (S.flat D det).StepAt z (Sum.inr ⟨p, d⟩, t) (Sum.inr ⟨p', d'⟩, t') ↔ det = true ∧ d' = (D p'.1 p'.2).start ∧ S.Adv D z p d p' t t'

A step between decider nodes of different pairs of modes: an advance only.

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₀

theorem DescriptiveComplexity.ParamTCSpec.bot_unique {A : Type} [LinearOrder A] {u u' : A} (h : ∀ (a : A), u ≤ a) (h' : ∀ (a : A), u' ≤ a) : u = u'

Coordinates at the minimum are equal.

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))

def DescriptiveComplexity.ParamTCSpec.FlatInv {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] [instE : ((L.sum FirstOrder.Language.order).sum B.lang).Structure A] (z : Fin S.par → A) (a : S.Node A) (c : (S.flat D det).Node A) : Prop

What the flat walk may have reached from the encoding of a: an outer node reached from a, or a decider node whose outer node is reached from a and whose decider has run from its start.

Equations

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

theorem DescriptiveComplexity.ParamTCSpec.flatInv_of_reachAt {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] [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) (a : S.Node A) {c : (S.flat D det).Node A} (h : (S.flat D det).ReachAt z (S.flatEnc D det a₀ a) c) : S.FlatInv D z a c

theorem DescriptiveComplexity.ParamTCSpec.reachAt_of_flat_reachAt {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] [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) (a b : S.Node A) (h : (S.flat D det).ReachAt z (S.flatEnc D det a₀ a) (S.flatEnc D det a₀ b)) : S.ReachAt z a b

The flat walk reaches only what the outer walk reaches.

theorem DescriptiveComplexity.ParamTCSpec.flat_reachAt_of_decider {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} [Nonempty A] (p : S.Mode × S.Mode) (t : S.FlatCoord D → A) {e e' : (D p.1 p.2).Node A} (h : (D p.1 p.2).ReachAt (dpar t z) e e') : (S.flat D det).ReachAt z (Sum.inr ⟨p, e.1⟩, setSlice t p e.2) (Sum.inr ⟨p, e'.1⟩, setSlice t p e'.2)

A run of a decider lifts to the flat walk, on its slice.

theorem DescriptiveComplexity.ParamTCSpec.flat_finish {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] [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) (m n : S.Mode) (x y : Fin S.k → A) (h : S.StepAt z (m, x) (n, y)) : (S.flat D det).ReachAt z (Sum.inr ⟨(m, n), (D m n).start⟩, Sum.elim (Sum.elim x y) fun (x : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) => a₀) (S.flatEnc D det a₀ (n, y))

Finishing a step: from the start of the decider of a step that holds, the flat walk reaches the encoding of the step's target.

theorem DescriptiveComplexity.ParamTCSpec.flat_reachAt_of_reachAt {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} (h : S.ReachAt z a b) : (S.flat D false).ReachAt z (S.flatEnc D false a₀ a) (S.flatEnc D false a₀ b)

Guessing: the flat walk reaches what the outer walk reaches.

@[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.flat_search {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) (m n : S.Mode) (x y : Fin S.k → A) (h : S.StepAt z (m, x) (n, y)) (κ : S.Cand A) (n' : S.Mode) (y' : Fin S.k → A) : toLex (n', toLex y') = κ → κ ≤ toLex (n, toLex y) → (S.flat D true).ReachAt z (Sum.inr ⟨(m, n'), (D m n').start⟩, Sum.elim (Sum.elim x y') fun (x : (p : S.Mode × S.Mode) × (D p.1 p.2).Coord) => a₀) (S.flatEnc D true a₀ (n, y))

Searching: from a candidate at or before the successor, the flat walk reaches the encoding of the successor, the outer walk being functional.

theorem DescriptiveComplexity.ParamTCSpec.flat_reachAt_of_reachAt_det {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} (h : S.ReachAt z a b) : (S.flat D true).ReachAt z (S.flatEnc D true a₀ a) (S.flatEnc D true a₀ b)

Searching: the flat walk reaches what a functional outer walk reaches.

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.adv_unique {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 p₁ p₂ : S.Mode × S.Mode} {d : (D p.1 p.2).Mode} {t t₁ t₂ : S.FlatCoord D → A} (h₁ : S.Adv D z p d p₁ t t₁) (h₂ : S.Adv D z p d p₂ t t₂) : p₁ = p₂ ∧ t₁ = t₂

Two advances from the same node go to the same node.

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.