Correctness of the positive native tableau rules

The positive local rules compute the next native configuration exactly. The finite domain must contain both input endmarkers and the next work-head position. No property of an arbitrary recursive approximation is assumed: the monotonicity theorem applies to every row, and correctness is proved separately on the rows of actual native configurations.

Main results

• read_row, situation_row: positive read and situation predicates have native semantics.
• elsewhere_row: the positive replacement for head negation is exact on native rows.
• rowStep_row: the positive rules compute exactly the next native configuration.

theorem Cslib.Complexity.ImmermanVardi.Tableau.read_row {m B : ℕ} {State : Type} {input : List Bool} {cfg : Turing.Cfg m Bool State input} (hb : ∀ (i : Fin m), |cfg.workTapePos i| < ↑B) (i : Fin m) (s : Option Bool) : read (row cfg) i s ↔ Turing.MultiTapeTM.Feature.Holds cfg (Turing.MultiTapeTM.Feature.read i s)

The positive read rule recovers the symbol under a head inside the finite domain.

theorem Cslib.Complexity.ImmermanVardi.Tableau.situation_row {m B : ℕ} {State : Type} {input : List Bool} {cfg : Turing.Cfg m Bool State input} (hn : input.length + 1 < B) (hb : ∀ (i : Fin m), |cfg.workTapePos i| < ↑B) (y : Turing.MultiTapeTM.Situation m State) (a : Fin B) : situation input (row cfg) y a ↔ Turing.MultiTapeTM.Feature.Holds cfg (Turing.MultiTapeTM.Feature.sit y)

Positive situation predicates agree with the native situation.

theorem Cslib.Complexity.ImmermanVardi.Tableau.elsewhere_row {m B : ℕ} {State : Type} {input : List Bool} {cfg : Turing.Cfg m Bool State input} (hb : ∀ (i : Fin m), |cfg.workTapePos i| < ↑B) (i : Fin m) (sign : Bool) (a : Fin B) : elsewhere (row cfg) i sign a ↔ ¬Turing.MultiTapeTM.Feature.Holds cfg (Turing.MultiTapeTM.Feature.head i (offset sign a))

A positively witnessed other head position is equivalent to head inequality.

theorem Cslib.Complexity.ImmermanVardi.Tableau.inputPrev_row {m B : ℕ} {State : Type} {input : List Bool} {cfg : Turing.Cfg m Bool State input} (hn : input.length + 1 < B) (d : SignType) (a : Fin B) : inputPrev input (row cfg) d a ↔ Turing.moveInputPosNat input.length (↑cfg.inputPos) d = ↑a

The positive input-head predecessor rule describes the native clamped move.

theorem Cslib.Complexity.ImmermanVardi.Tableau.headPrev_row {m B : ℕ} {State : Type} {input : List Bool} {cfg : Turing.Cfg m Bool State input} (hb : ∀ (i : Fin m), |cfg.workTapePos i| + 1 < ↑B) (i : Fin m) (sign : Bool) (d : SignType) (a : Fin B) : headPrev (row cfg) i sign d a ↔ cfg.workTapePos i + ↑d = offset sign a

The positive work-head predecessor rule describes the native signed move.

theorem Cslib.Complexity.ImmermanVardi.Tableau.rowStep_row {m B : ℕ} {State : Type} {input : List Bool} {cfg : Turing.Cfg m Bool State input} [Finite State] (tm : Turing.MultiTapeTM m Bool State) (hn : input.length + 1 < B) (hb : ∀ (i : Fin m), |cfg.workTapePos i| + 1 < ↑B) (q : Tag m State) (a : Fin B) : rowStep tm input (row cfg) q a ↔ row (Turing.MultiTapeTM.step cfg) q a

The positive rules produce exactly the row of the next native configuration.