The configuration block, and the four sentences of the machine

The second layer: the block whose assignments are the configurations, and the DescriptiveComplexity.SOGameSpec an alternating machine is.

• DescriptiveComplexity.ATMSpace.cfgBlock has one variable for the state, one for the head and one – binary – for the tape, a DescriptiveComplexity.Config carrying a function A → A;
• DescriptiveComplexity.ATMSpace.isCfgS says an assignment is a configuration: the two unary variables are singletons and the binary one is a function. DescriptiveComplexity.ATMSpace.cfgOf is the assignment a configuration is, and DescriptiveComplexity.ATMSpace.exists_cfgOf the equivalence;
• the four sentences follow DescriptiveComplexity.TMData.Step, DescriptiveComplexity.ATMData.IsUniv, DescriptiveComplexity.TMData.Acc and DescriptiveComplexity.TMData.IsInit. Every quantifier in them ranges over the base – a transition, a state, a head position, a symbol – which is what keeps them first-order there.

The two promises DescriptiveComplexity.TMData.WellFormed and DescriptiveComplexity.ATMData.BlocksSplit are conjoined to start: DescriptiveComplexity.ExpDefinable compares P A with Q (X.Map A) and has nowhere else to put a condition on A alone.

The block

inductive DescriptiveComplexity.ATMSpace.CIx : Type

The relation variables a configuration is made of.

• st : CIx

  The current state.

• hd : CIx

  The cell the head is on.

• tp : CIx

  The contents of each cell.

@[instance_reducible]

instance DescriptiveComplexity.ATMSpace.instDecidableEqCIx : DecidableEq CIx

Equations

• DescriptiveComplexity.ATMSpace.instDecidableEqCIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.ATMSpace.instFintypeCIx : Fintype CIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.cfgBlock : SOBlock

The configuration block: a unary variable for the state, a unary one for the head, and a binary one for the tape.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.cfg1 : FirstOrder.Language

The base vocabulary expanded by one copy of the block.

Equations

• DescriptiveComplexity.ATMSpace.cfg1 = DescriptiveComplexity.ATMSpace.tmaOrd.sum DescriptiveComplexity.ATMSpace.cfgBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.cfg2 : FirstOrder.Language

The base vocabulary expanded by two copies of the block.

Equations

• DescriptiveComplexity.ATMSpace.cfg2 = DescriptiveComplexity.ATMSpace.cfg1.sum DescriptiveComplexity.ATMSpace.cfgBlock.lang

The atoms of the block

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.stS : cfg1.Relations 1

The state variable, at one copy.

Equations

• DescriptiveComplexity.ATMSpace.stS = Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.st, DescriptiveComplexity.ATMSpace.stS._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.hdS : cfg1.Relations 1

The head variable, at one copy.

Equations

• DescriptiveComplexity.ATMSpace.hdS = Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.hd, DescriptiveComplexity.ATMSpace.hdS._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.tpS : cfg1.Relations 2

The tape variable, at one copy.

Equations

• DescriptiveComplexity.ATMSpace.tpS = Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.tp, DescriptiveComplexity.ATMSpace.tpS._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.stA : cfg2.Relations 1

The state variable of the current configuration.

Equations

• DescriptiveComplexity.ATMSpace.stA = Sum.inl (Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.st, DescriptiveComplexity.ATMSpace.stS._proof_1⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.hdA : cfg2.Relations 1

The head variable of the current configuration.

Equations

• DescriptiveComplexity.ATMSpace.hdA = Sum.inl (Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.hd, DescriptiveComplexity.ATMSpace.hdS._proof_1⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.tpA : cfg2.Relations 2

The tape variable of the current configuration.

Equations

• DescriptiveComplexity.ATMSpace.tpA = Sum.inl (Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.tp, DescriptiveComplexity.ATMSpace.tpS._proof_1⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.stB : cfg2.Relations 1

The state variable of the next configuration.

Equations

• DescriptiveComplexity.ATMSpace.stB = Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.st, DescriptiveComplexity.ATMSpace.stS._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.hdB : cfg2.Relations 1

The head variable of the next configuration.

Equations

• DescriptiveComplexity.ATMSpace.hdB = Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.hd, DescriptiveComplexity.ATMSpace.hdS._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.tpB : cfg2.Relations 2

The tape variable of the next configuration.

Equations

• DescriptiveComplexity.ATMSpace.tpB = Sum.inr ⟨DescriptiveComplexity.ATMSpace.CIx.tp, DescriptiveComplexity.ATMSpace.tpS._proof_1⟩

noncomputable def DescriptiveComplexity.ATMSpace.stF {γ : Type} (x : γ) : cfg1.Formula γ

x is the state, at one copy.

Equations

• DescriptiveComplexity.ATMSpace.stF x = DescriptiveComplexity.ATMSpace.stS.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.hdF {γ : Type} (x : γ) : cfg1.Formula γ

x is the head, at one copy.

Equations

• DescriptiveComplexity.ATMSpace.hdF x = DescriptiveComplexity.ATMSpace.hdS.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.tpF {γ : Type} (x y : γ) : cfg1.Formula γ

The cell x holds y, at one copy.

Equations

• DescriptiveComplexity.ATMSpace.tpF x y = DescriptiveComplexity.ATMSpace.tpS.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.stAF {γ : Type} (x : γ) : cfg2.Formula γ

x is the state of the current configuration.

Equations

• DescriptiveComplexity.ATMSpace.stAF x = DescriptiveComplexity.ATMSpace.stA.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.hdAF {γ : Type} (x : γ) : cfg2.Formula γ

x is the head of the current configuration.

Equations

• DescriptiveComplexity.ATMSpace.hdAF x = DescriptiveComplexity.ATMSpace.hdA.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.tpAF {γ : Type} (x y : γ) : cfg2.Formula γ

The cell x holds y in the current configuration.

Equations

• DescriptiveComplexity.ATMSpace.tpAF x y = DescriptiveComplexity.ATMSpace.tpA.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.stBF {γ : Type} (x : γ) : cfg2.Formula γ

x is the state of the next configuration.

Equations

• DescriptiveComplexity.ATMSpace.stBF x = DescriptiveComplexity.ATMSpace.stB.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.hdBF {γ : Type} (x : γ) : cfg2.Formula γ

x is the head of the next configuration.

Equations

• DescriptiveComplexity.ATMSpace.hdBF x = DescriptiveComplexity.ATMSpace.hdB.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.tpBF {γ : Type} (x y : γ) : cfg2.Formula γ

The cell x holds y in the next configuration.

Equations

• DescriptiveComplexity.ATMSpace.tpBF x y = DescriptiveComplexity.ATMSpace.tpB.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.lift1 {γ : Type} (φ : tmaOrd.Formula γ) : cfg1.Formula γ

A base guard, read at one copy of the block.

Equations

• DescriptiveComplexity.ATMSpace.lift1 φ = FirstOrder.Language.LHom.sumInl.onFormula φ

noncomputable def DescriptiveComplexity.ATMSpace.lift2 {γ : Type} (φ : tmaOrd.Formula γ) : cfg2.Formula γ

A base guard, read at two copies of the block.

Equations

• DescriptiveComplexity.ATMSpace.lift2 φ = FirstOrder.Language.LHom.sumInl.onFormula (FirstOrder.Language.LHom.sumInl.onFormula φ)

What an assignment says

def DescriptiveComplexity.ATMSpace.St {A : Type} (ρ : cfgBlock.Assignment A) (q : A) : Prop

The state an assignment names.

Equations

• DescriptiveComplexity.ATMSpace.St ρ q = ρ DescriptiveComplexity.ATMSpace.CIx.st fun (x : Fin (DescriptiveComplexity.ATMSpace.cfgBlock.arity DescriptiveComplexity.ATMSpace.CIx.st)) => q

def DescriptiveComplexity.ATMSpace.Hd {A : Type} (ρ : cfgBlock.Assignment A) (h : A) : Prop

The head position an assignment names.

Equations

• DescriptiveComplexity.ATMSpace.Hd ρ h = ρ DescriptiveComplexity.ATMSpace.CIx.hd fun (x : Fin (DescriptiveComplexity.ATMSpace.cfgBlock.arity DescriptiveComplexity.ATMSpace.CIx.hd)) => h

def DescriptiveComplexity.ATMSpace.Tp {A : Type} (ρ : cfgBlock.Assignment A) (p a : A) : Prop

The tape an assignment names.

Equations

• DescriptiveComplexity.ATMSpace.Tp ρ p a = ρ DescriptiveComplexity.ATMSpace.CIx.tp ![p, a]

theorem DescriptiveComplexity.ATMSpace.apply₁ {A : Type} (f : (Fin 1 → A) → Prop) (v : Fin 1 → A) : f v ↔ f fun (x : Fin 1) => v 0

A unary variable is read at its only argument.

theorem DescriptiveComplexity.ATMSpace.apply₂ {A : Type} (f : (Fin 2 → A) → Prop) (v : Fin 2 → A) : f v ↔ f ![v 0, v 1]

A binary variable is read at its two arguments.

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_stF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ : cfgBlock.Assignment A) (x : γ) : (stF x).Realize v ↔ St ρ (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_hdF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ : cfgBlock.Assignment A) (x : γ) : (hdF x).Realize v ↔ Hd ρ (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_tpF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ : cfgBlock.Assignment A) (x y : γ) : (tpF x y).Realize v ↔ Tp ρ (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_stAF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (x : γ) : (stAF x).Realize v ↔ St ρ (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_hdAF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (x : γ) : (hdAF x).Realize v ↔ Hd ρ (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_tpAF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (x y : γ) : (tpAF x y).Realize v ↔ Tp ρ (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_stBF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (x : γ) : (stBF x).Realize v ↔ St σ (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_hdBF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (x : γ) : (hdBF x).Realize v ↔ Hd σ (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_tpBF {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (x y : γ) : (tpBF x y).Realize v ↔ Tp σ (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_lift1 {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ : cfgBlock.Assignment A) (φ : tmaOrd.Formula γ) : (lift1 φ).Realize v ↔ φ.Realize v

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_lift2 {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (ρ σ : cfgBlock.Assignment A) (φ : tmaOrd.Formula γ) : (lift2 φ).Realize v ↔ φ.Realize v

Configurations

def DescriptiveComplexity.ATMSpace.cfgOf {A : Type} (c : Config A) : cfgBlock.Assignment A

The assignment a configuration is.

Equations

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

@[simp]

theorem DescriptiveComplexity.ATMSpace.st_cfgOf {A : Type} (c : Config A) (q : A) : St (cfgOf c) q ↔ q = c.state

@[simp]

theorem DescriptiveComplexity.ATMSpace.hd_cfgOf {A : Type} (c : Config A) (h : A) : Hd (cfgOf c) h ↔ h = c.head

@[simp]

theorem DescriptiveComplexity.ATMSpace.tp_cfgOf {A : Type} (c : Config A) (p a : A) : Tp (cfgOf c) p a ↔ c.tape p = a

def DescriptiveComplexity.ATMSpace.IsCfg {A : Type} (ρ : cfgBlock.Assignment A) : Prop

An assignment is a configuration: the two unary variables are singletons and the binary one is a function.

Equations

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

theorem DescriptiveComplexity.ATMSpace.isCfg_cfgOf {A : Type} (c : Config A) : IsCfg (cfgOf c)

theorem DescriptiveComplexity.ATMSpace.exists_cfgOf {A : Type} {ρ : cfgBlock.Assignment A} (h : IsCfg ρ) : ∃ (c : Config A), ρ = cfgOf c

A configuration assignment is the assignment of a configuration.

The four sentences

noncomputable def DescriptiveComplexity.ATMSpace.isCfgS : cfg1.Sentence

An assignment is a configuration, as a sentence over one copy.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.isCfgBS : cfg2.Sentence

The next configuration is a configuration, as a sentence over two copies.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.univS : cfg1.Sentence

The state is marked by the universal player.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.wonS : cfg1.Sentence

The state is accepting.

Equations

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

theorem DescriptiveComplexity.ATMSpace.realize_isCfgS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (ρ : cfgBlock.Assignment A) : A ⊨ isCfgS ↔ IsCfg ρ

theorem DescriptiveComplexity.ATMSpace.realize_isCfgBS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (ρ σ : cfgBlock.Assignment A) : A ⊨ isCfgBS ↔ IsCfg σ

theorem DescriptiveComplexity.ATMSpace.realize_univS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (c : Config A) : A ⊨ univS ↔ FirstOrder.Language.Structure.RelMap (FirstOrder.Language.atmBlk 1) ![c.state]

theorem DescriptiveComplexity.ATMSpace.realize_wonS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (c : Config A) : A ⊨ wonS ↔ ATMAcc c.state

The step relation

Seven elements of the base are quantified – the transition, the two states, the two head positions, the symbol read and the symbol written – and one pair is quantified universally, for the cells the head does not touch. Nothing here quantifies over a configuration, which is what keeps the sentence first-order over the base.

noncomputable def DescriptiveComplexity.ATMSpace.stepS : cfg2.Sentence

One step of the machine, as a sentence over two copies of the block.

Equations

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

The starting configurations

noncomputable def DescriptiveComplexity.ATMSpace.isInitS : cfg1.Sentence

An initial configuration, as a sentence over one copy.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.startS : cfg1.Sentence

A starting state of the game: the two promises about the instance, and an initial configuration.

Equations

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

theorem DescriptiveComplexity.ATMSpace.realize_stepS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (c c' : Config A) : A ⊨ stepS ↔ (atmData 2 A).Step c c'

theorem DescriptiveComplexity.ATMSpace.realize_isInitS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (c : Config A) : A ⊨ isInitS ↔ (atmData 2 A).IsInit c

theorem DescriptiveComplexity.ATMSpace.realize_startS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (ρ : cfgBlock.Assignment A) : A ⊨ startS ↔ (atmData 2 A).WellFormed ∧ (atmData 2 A).BlocksSplit ∧ ∃ (c : Config A), ρ = cfgOf c ∧ (atmData 2 A).IsInit c