The kinds of variables, on fields and as formulas

For the fields F of an index, the predicates IsCell, IsHead, … saying that F denotes a variable of that kind (with its range checks), the characterization of decodeVar by them (decodeVar_cell_iff, …), and the formulas computing all of these on the field formulas of a literal (isCellF, numEqF, …) with their semantics (planning/succinct-cook-levin.md, S3).

Numeric equality of fields

structure MIPRE.TM.CookLevin.Desc.FieldsF.Lengths (e G : ℕ) (A : FieldsF) : Prop

The lengths of the field formulas of a literal.

• tag : A.tag.length = 3
• t : A.t.length = W e
• d : A.d.length = 4
• p : A.p.length = W e
• v : A.v.length = 3
• q : A.q.length = Qb
• js (k : Fin 13) : (A.js k).length = W e
• g : A.g.length = Gb G

theorem MIPRE.TM.CookLevin.Desc.litFields_lengths (e G T b : ℕ) : FieldsF.Lengths e G (litFields e G T b)

def MIPRE.TM.CookLevin.Desc.numEqF (A B : FieldsF) : SAT.Fml

The formula: the numeric fields of A and B agree.

Equations

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

Kinds

def MIPRE.TM.CookLevin.Desc.IsCell (e : ℕ) (F : Fields) : Prop

The fields denote a cell variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.IsHead (e : ℕ) (F : Fields) : Prop

The fields denote a head variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.IsState (e : ℕ) (F : Fields) : Prop

The fields denote a state variable.

Equations

• MIPRE.TM.CookLevin.Desc.IsState e F = (F.flag = true ∧ F.tag = 2 ∧ F.t ≤ MIPRE.TM.CookLevin.Desc.Sof e ∧ F.q < MIPRE.TM.CookLevin.Desc.QC)

def MIPRE.TM.CookLevin.Desc.IsEmitOne (e : ℕ) (F : Fields) : Prop

The fields denote an emitOne variable.

Equations

• MIPRE.TM.CookLevin.Desc.IsEmitOne e F = (F.flag = true ∧ F.tag = 3 ∧ F.t < MIPRE.TM.CookLevin.Desc.Sof e)

def MIPRE.TM.CookLevin.Desc.IsEmitBad (e : ℕ) (F : Fields) : Prop

The fields denote an emitBad variable.

Equations

• MIPRE.TM.CookLevin.Desc.IsEmitBad e F = (F.flag = true ∧ F.tag = 4 ∧ F.t < MIPRE.TM.CookLevin.Desc.Sof e)

def MIPRE.TM.CookLevin.Desc.IsEmitted (e : ℕ) (F : Fields) : Prop

The fields denote an emitted variable.

Equations

• MIPRE.TM.CookLevin.Desc.IsEmitted e F = (F.flag = true ∧ F.tag = 5 ∧ F.t ≤ MIPRE.TM.CookLevin.Desc.Sof e)

def MIPRE.TM.CookLevin.Desc.IsAux (e G : ℕ) (F : Fields) : Prop

The fields denote a gate variable.

Equations

• MIPRE.TM.CookLevin.Desc.IsAux e G F = (F.flag = true ∧ F.tag = 6 ∧ F.t < MIPRE.TM.CookLevin.Desc.Sof e ∧ (∀ (k : Fin 13), F.js k < 2 * MIPRE.TM.CookLevin.Desc.Sof e + 3) ∧ F.g < G)

theorem MIPRE.TM.CookLevin.Desc.tape_eq_inl_of_lt (d : Tape 7 6) (h : tapeCode d < 7) : d = Sum.inl ⟨tapeCode d, h⟩

Decoding by kind

theorem MIPRE.TM.CookLevin.Desc.decodeVar_cell_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym) : decodeVar e G F = some (TabVar.cell t d p v) ↔ IsCell e F ∧ F.t = ↑t ∧ F.d = tapeCode d ∧ F.p = ↑p ∧ F.v = symCode v

theorem MIPRE.TM.CookLevin.Desc.decodeVar_head_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) : decodeVar e G F = some (TabVar.head t d p) ↔ IsHead e F ∧ F.t = ↑t ∧ F.d = tapeCode d ∧ F.p = ↑p

theorem MIPRE.TM.CookLevin.Desc.decodeVar_state_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e + 1)) (q : Option Interp.Ctl) : decodeVar e G F = some (TabVar.state t q) ↔ IsState e F ∧ F.t = ↑t ∧ F.q = qCode q

theorem MIPRE.TM.CookLevin.Desc.decodeVar_emitOne_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e)) : decodeVar e G F = some (TabVar.emitOne t) ↔ IsEmitOne e F ∧ F.t = ↑t

theorem MIPRE.TM.CookLevin.Desc.decodeVar_emitBad_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e)) : decodeVar e G F = some (TabVar.emitBad t) ↔ IsEmitBad e F ∧ F.t = ↑t

theorem MIPRE.TM.CookLevin.Desc.decodeVar_emitted_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e + 1)) : decodeVar e G F = some (TabVar.emitted t) ↔ IsEmitted e F ∧ F.t = ↑t

theorem MIPRE.TM.CookLevin.Desc.decodeVar_aux_iff (e G : ℕ) (F : Fields) (t : Fin (Sof e)) (js : Tape 7 6 → Center (Sof e)) (g : Fin G) : decodeVar e G F = some (TabVar.aux t js g) ↔ IsAux e G F ∧ F.t = ↑t ∧ (∀ (d : Tape 7 6), F.js ⟨tapeCode d, ⋯⟩ = ↑(js d)) ∧ F.g = ↑g

Kinds as formulas

def MIPRE.TM.CookLevin.Desc.isCellF (e : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes a cell variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.isHeadF (e : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes a head variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.isStateF (e : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes a state variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.isEmitOneF (e : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes an emitOne variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.isEmitBadF (e : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes an emitBad variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.isEmittedF (e : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes an emitted variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.isAuxF (e G : ℕ) (A : FieldsF) : SAT.Fml

The formula: A denotes a gate variable.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.eval_eqTag (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (k : ℕ) (hk : k < 8) : SAT.Fml.eval x (SAT.Fml.eqConst A.tag (nbits 3 k)) = true ↔ SAT.Fml.val A.tag x = k

theorem MIPRE.TM.CookLevin.Desc.eval_ltT (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (k : ℕ) (hk : k < 2 ^ W e) : SAT.Fml.eval x (SAT.Fml.ltConst A.t (nbits (W e) k)) = true ↔ SAT.Fml.val A.t x < k

theorem MIPRE.TM.CookLevin.Desc.eval_ltD (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (k : ℕ) (hk : k < 16) : SAT.Fml.eval x (SAT.Fml.ltConst A.d (nbits 4 k)) = true ↔ SAT.Fml.val A.d x < k

theorem MIPRE.TM.CookLevin.Desc.eval_ltP (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (k : ℕ) (hk : k < 2 ^ W e) : SAT.Fml.eval x (SAT.Fml.ltConst A.p (nbits (W e) k)) = true ↔ SAT.Fml.val A.p x < k

theorem MIPRE.TM.CookLevin.Desc.eval_ltV (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (k : ℕ) (hk : k < 8) : SAT.Fml.eval x (SAT.Fml.ltConst A.v (nbits 3 k)) = true ↔ SAT.Fml.val A.v x < k

theorem MIPRE.TM.CookLevin.Desc.S_succ_lt (e : ℕ) : Sof e + 1 < 2 ^ W e

theorem MIPRE.TM.CookLevin.Desc.eval_isCellF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isCellF e A) = true ↔ IsCell e (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_isHeadF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isHeadF e A) = true ↔ IsHead e (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_isStateF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isStateF e A) = true ↔ IsState e (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_isEmitOneF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isEmitOneF e A) = true ↔ IsEmitOne e (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_isEmitBadF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isEmitBadF e A) = true ↔ IsEmitBad e (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_isEmittedF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isEmittedF e A) = true ↔ IsEmitted e (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_isAuxF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (isAuxF e G A) = true ↔ IsAux e G (evalFields A x)