The guards of the alternating machine, and the configuration block

The first of the three layers that put DescriptiveComplexity.ATMAcceptSpace in EXPTIME. Everything here is bookkeeping:

• the symbols of FirstOrder.Language.turingAlt 2 in the ordered expansion, as abbreviations with declared types – a raw Sum.inl r inside FirstOrder.Language.Relations.formula₁ does not elaborate;
• one guard per symbol, at an arbitrary variable type, with its realization lemma, in the style of DescriptiveComplexity.Problems.Machine.Fixpoint;
• the derived guards minPosG, succPosG, initTapeG and the two promise sentences wfS (DescriptiveComplexity.TMData.WellFormed) and blocksSplitS (DescriptiveComplexity.ATMData.BlocksSplit);
• the configuration block cfgBlock – one variable for the state, one for the head, one for the tape – its atoms at one and at two copies, and the lifts that read a base guard there.

The block has a binary variable for the tape because a DescriptiveComplexity.Config carries a function A → A; that the variable is one is the content of DescriptiveComplexity.ATMSpace.isCfgS, and DescriptiveComplexity.ATMSpace.cfgOf is the assignment a configuration is.

The ordered vocabulary and its symbols

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.tmaOrd : FirstOrder.Language

The ordered expansion of the alternating machine vocabulary, at two blocks.

Equations

• DescriptiveComplexity.ATMSpace.tmaOrd = (FirstOrder.Language.turingAlt 2).sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.posnO : tmaOrd.Relations 1

The position symbol.

Equations

• DescriptiveComplexity.ATMSpace.posnO = Sum.inl FirstOrder.Language.atmPosn

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.trO : tmaOrd.Relations 1

The transition symbol.

Equations

• DescriptiveComplexity.ATMSpace.trO = Sum.inl FirstOrder.Language.atmTr

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.startO : tmaOrd.Relations 1

The start-state symbol.

Equations

• DescriptiveComplexity.ATMSpace.startO = Sum.inl FirstOrder.Language.atmStart

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.accO : tmaOrd.Relations 1

The accepting-state symbol.

Equations

• DescriptiveComplexity.ATMSpace.accO = Sum.inl FirstOrder.Language.atmAcc

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.blankO : tmaOrd.Relations 1

The blank symbol.

Equations

• DescriptiveComplexity.ATMSpace.blankO = Sum.inl FirstOrder.Language.atmBlank

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.rightO : tmaOrd.Relations 1

The move-right symbol.

Equations

• DescriptiveComplexity.ATMSpace.rightO = Sum.inl FirstOrder.Language.atmRight

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.leO : tmaOrd.Relations 2

The order symbol of the machine.

Equations

• DescriptiveComplexity.ATMSpace.leO = Sum.inl FirstOrder.Language.atmLe

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.srcO : tmaOrd.Relations 2

The transition-source symbol.

Equations

• DescriptiveComplexity.ATMSpace.srcO = Sum.inl FirstOrder.Language.atmSrc

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.readO : tmaOrd.Relations 2

The transition-read symbol.

Equations

• DescriptiveComplexity.ATMSpace.readO = Sum.inl FirstOrder.Language.atmRead

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.dstO : tmaOrd.Relations 2

The transition-destination symbol.

Equations

• DescriptiveComplexity.ATMSpace.dstO = Sum.inl FirstOrder.Language.atmDst

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.writeO : tmaOrd.Relations 2

The transition-write symbol.

Equations

• DescriptiveComplexity.ATMSpace.writeO = Sum.inl FirstOrder.Language.atmWrite

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.inpO : tmaOrd.Relations 2

The input symbol.

Equations

• DescriptiveComplexity.ATMSpace.inpO = Sum.inl FirstOrder.Language.atmInp

@[reducible, inline]

abbrev DescriptiveComplexity.ATMSpace.blkO (i : Fin 2) : tmaOrd.Relations 1

The mark of the i-th player.

Equations

• DescriptiveComplexity.ATMSpace.blkO i = Sum.inl (FirstOrder.Language.atmBlk i)

One guard per symbol

noncomputable def DescriptiveComplexity.ATMSpace.posnG {γ : Type} (x : γ) : tmaOrd.Formula γ

x is a position.

Equations

• DescriptiveComplexity.ATMSpace.posnG x = DescriptiveComplexity.ATMSpace.posnO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.trG {γ : Type} (x : γ) : tmaOrd.Formula γ

x is a transition.

Equations

• DescriptiveComplexity.ATMSpace.trG x = DescriptiveComplexity.ATMSpace.trO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.startG {γ : Type} (x : γ) : tmaOrd.Formula γ

x is a start state.

Equations

• DescriptiveComplexity.ATMSpace.startG x = DescriptiveComplexity.ATMSpace.startO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.accG {γ : Type} (x : γ) : tmaOrd.Formula γ

x is an accepting state.

Equations

• DescriptiveComplexity.ATMSpace.accG x = DescriptiveComplexity.ATMSpace.accO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.blankG {γ : Type} (x : γ) : tmaOrd.Formula γ

x is the blank symbol.

Equations

• DescriptiveComplexity.ATMSpace.blankG x = DescriptiveComplexity.ATMSpace.blankO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.rightG {γ : Type} (x : γ) : tmaOrd.Formula γ

The transition x moves the head right.

Equations

• DescriptiveComplexity.ATMSpace.rightG x = DescriptiveComplexity.ATMSpace.rightO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.blkG {γ : Type} (i : Fin 2) (x : γ) : tmaOrd.Formula γ

x is marked by the i-th player.

Equations

• DescriptiveComplexity.ATMSpace.blkG i x = (DescriptiveComplexity.ATMSpace.blkO i).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.ATMSpace.leG {γ : Type} (x y : γ) : tmaOrd.Formula γ

x ≤ y in the machine's own order.

Equations

• DescriptiveComplexity.ATMSpace.leG x y = DescriptiveComplexity.ATMSpace.leO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.srcG {γ : Type} (x y : γ) : tmaOrd.Formula γ

The transition x applies in the state y.

Equations

• DescriptiveComplexity.ATMSpace.srcG x y = DescriptiveComplexity.ATMSpace.srcO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.readG {γ : Type} (x y : γ) : tmaOrd.Formula γ

The transition x reads the symbol y.

Equations

• DescriptiveComplexity.ATMSpace.readG x y = DescriptiveComplexity.ATMSpace.readO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.dstG {γ : Type} (x y : γ) : tmaOrd.Formula γ

The transition x moves to the state y.

Equations

• DescriptiveComplexity.ATMSpace.dstG x y = DescriptiveComplexity.ATMSpace.dstO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.writeG {γ : Type} (x y : γ) : tmaOrd.Formula γ

The transition x writes the symbol y.

Equations

• DescriptiveComplexity.ATMSpace.writeG x y = DescriptiveComplexity.ATMSpace.writeO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.inpG {γ : Type} (x y : γ) : tmaOrd.Formula γ

The cell x initially holds the input symbol y.

Equations

• DescriptiveComplexity.ATMSpace.inpG x y = DescriptiveComplexity.ATMSpace.inpO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.ATMSpace.eqG {γ : Type} (x y : γ) : tmaOrd.Formula γ

x and y are the same element.

Equations

• DescriptiveComplexity.ATMSpace.eqG x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_posnG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (posnG x).Realize v ↔ ATMPosn (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_trG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (trG x).Realize v ↔ ATMTr (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_startG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (startG x).Realize v ↔ ATMStart (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_accG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (accG x).Realize v ↔ ATMAcc (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_blankG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (blankG x).Realize v ↔ ATMBlank (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_rightG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (rightG x).Realize v ↔ ATMRight (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_blkG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (i : Fin 2) (x : γ) : (blkG i x).Realize v ↔ FirstOrder.Language.Structure.RelMap (FirstOrder.Language.atmBlk i) ![v x]

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_leG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (leG x y).Realize v ↔ ATMLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_srcG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (srcG x y).Realize v ↔ ATMSrc (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_readG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (readG x y).Realize v ↔ ATMRead (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_dstG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (dstG x y).Realize v ↔ ATMDst (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_writeG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (writeG x y).Realize v ↔ ATMWrite (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_inpG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (inpG x y).Realize v ↔ ATMInp (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_eqG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (eqG x y).Realize v ↔ v x = v y

The derived guards

noncomputable def DescriptiveComplexity.ATMSpace.minPosG {γ : Type} (x : γ) : tmaOrd.Formula γ

x is a least position.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.succPosG {γ : Type} (x y : γ) : tmaOrd.Formula γ

y is the position immediately above x.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.initTapeG {γ : Type} (x y : γ) : tmaOrd.Formula γ

The cell x may initially hold the symbol y.

Equations

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

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_minPosG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x : γ) : (minPosG x).Realize v ↔ MinPos ATMLe ATMPosn (v x)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_succPosG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (succPosG x y).Realize v ↔ SuccPos ATMLe ATMPosn (v x) (v y)

@[simp]

theorem DescriptiveComplexity.ATMSpace.realize_initTapeG {γ A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (initTapeG x y).Realize v ↔ (atmData 2 A).InitTape (v x) (v y)

The two promises, as sentences

noncomputable def DescriptiveComplexity.ATMSpace.isLinOrdS : tmaOrd.Sentence

The machine's order is linear.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.wfS : tmaOrd.Sentence

Well-formedness, as a sentence: the order is linear, there is a position, the input is functional, and there is exactly one blank.

Equations

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

noncomputable def DescriptiveComplexity.ATMSpace.blocksSplitS : tmaOrd.Sentence

The two marks split the states, as a sentence: every state carries one of them and not both.

Equations

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

theorem DescriptiveComplexity.ATMSpace.realize_isLinOrdS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] : A ⊨ isLinOrdS ↔ IsLinOrd ATMLe

theorem DescriptiveComplexity.ATMSpace.realize_wfS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] : A ⊨ wfS ↔ (atmData 2 A).WellFormed

theorem DescriptiveComplexity.ATMSpace.realize_blocksSplitS {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] : A ⊨ blocksSplitS ↔ (atmData 2 A).BlocksSplit

The two marks split the states exactly when every state carries one and not both: a mark index of 2 or more marks nothing, so the uniqueness clause of DescriptiveComplexity.ATMData.BlocksSplit only speaks about 0 and 1.