The clause families of the tableau, on decoded fields

A candidate clause is three field records and three signs (Cand): what the describer reads off its 3m + 3 input bits. Cand.Dec c cl says the candidate decodes to the tableau clause cl (each record to the variable of the corresponding literal, each sign to its polarity). For each sub-family of the tableau of the interpreter machine (startClauses, freeClauses, bdryClauses, emitClauses, finalClauses of Tableau.lean) this file gives a predicate on candidates, stated on the numeric fields alone, and proves it exact: it holds iff the candidate decodes to a clause of the sub-family. The window family is Window.lean; the formulas computing these predicates are FamilyFml.lean (planning/succinct-cook-levin.md, S3).

Candidates and decoding

structure MIPRE.TM.CookLevin.Desc.Cand : Type

A candidate clause: three field records and three signs.

• F₁ : Fields
• s₁ : Bool
• F₂ : Fields
• s₂ : Bool
• F₃ : Fields
• s₃ : Bool

def MIPRE.TM.CookLevin.Desc.LitDec (e G : ℕ) (F : Fields) (s : Bool) (l : SAT.Lit (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G)) : Prop

The record F with sign s decodes to the literal l.

Equations

• MIPRE.TM.CookLevin.Desc.LitDec e G F s l = (MIPRE.TM.CookLevin.Desc.decodeVar e G F = some l.var ∧ s = l.pos)

def MIPRE.TM.CookLevin.Desc.Cand.Dec (e G : ℕ) (c : Cand) (cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G)) : Prop

The candidate decodes to the clause cl.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.Cand.dec_unit (e G : ℕ) (c : Cand) (v : TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) (b : Bool) : Dec e G c (unit v b) ↔ decodeVar e G c.F₁ = some v ∧ c.s₁ = b ∧ decodeVar e G c.F₂ = some v ∧ c.s₂ = b ∧ decodeVar e G c.F₃ = some v ∧ c.s₃ = b

theorem MIPRE.TM.CookLevin.Desc.Cand.dec_cl (e G : ℕ) (c : Cand) (l₁ l₂ l₃ : SAT.Lit (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G)) : Dec e G c (SAT.cl l₁ l₂ l₃) ↔ decodeVar e G c.F₁ = some l₁.var ∧ c.s₁ = l₁.pos ∧ decodeVar e G c.F₂ = some l₂.var ∧ c.s₂ = l₂.pos ∧ decodeVar e G c.F₃ = some l₃.var ∧ c.s₃ = l₃.pos

Codes of positions and values

theorem MIPRE.TM.CookLevin.Desc.tapeOfCode_of_lt {k : ℕ} (h : k < 13) : ∃ (d : Tape 7 6), tapeOfCode k = some d

theorem MIPRE.TM.CookLevin.Desc.symOfCode_of_lt {k : ℕ} (h : k < 7) : ∃ (v : CellVal Interp.Sym), symOfCode k = some v

theorem MIPRE.TM.CookLevin.Desc.qOfCode_of_lt {k : ℕ} (h : k < QC) : ∃ (q : Option Interp.Ctl), qOfCode k = some q

theorem MIPRE.TM.CookLevin.Desc.tapeCode_lt_seven_iff (d : Tape 7 6) : tapeCode d < 7 ↔ ∃ (j : Fin 7), d = Sum.inl j

theorem MIPRE.TM.CookLevin.Desc.startCell_val (S : ℕ) (d : Tape 7 6) : ↑(startCell S d) = if tapeCode d < 7 then 3 else S + 3

The start cell, numerically.

theorem MIPRE.TM.CookLevin.Desc.isBdry_iff {S : ℕ} (p : Pos S) : p.IsBdry ↔ ↑p < 2 ∨ 2 * S + 5 ≤ ↑p

Boundary cells, numerically.

def MIPRE.TM.CookLevin.Desc.cellCode (x : List Interp.Sym) (S p : ℕ) : ℕ

The code of the value of cell p of an input tape holding x.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.symCode_inputCellVal (x : List Interp.Sym) {S : ℕ} (p : Pos S) : symCode (inputCellVal x p) = cellCode x S ↑p

def MIPRE.TM.CookLevin.Desc.workCode (S p : ℕ) : ℕ

The code of the value of cell p of a work tape at time 0.

Equations

• MIPRE.TM.CookLevin.Desc.workCode S p = if p < 2 ∨ 2 * S + 5 ≤ p then 6 else 5

theorem MIPRE.TM.CookLevin.Desc.symCode_workCellVal₀ {S : ℕ} (p : Pos S) : symCode (workCellVal₀ p) = workCode S ↑p

theorem MIPRE.TM.CookLevin.Desc.cellCode_replicate (T S p : ℕ) : cellCode (List.replicate T Interp.Sym.one) S p = if p < 2 ∨ 2 * S + 5 ≤ p then 6 else if 3 ≤ p ∧ p < T + 3 then 1 else 5

The unary tape 1^T: cells 3 .. T + 2 hold 1.

Decoding by kind: existence and same-variable lemmas

theorem MIPRE.TM.CookLevin.Desc.exists_cell (e G : ℕ) {F : Fields} (h : IsCell e F) : ∃ (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)

theorem MIPRE.TM.CookLevin.Desc.exists_head (e G : ℕ) {F : Fields} (h : IsHead e F) : ∃ (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)), decodeVar e G F = some (TabVar.head t d p)

theorem MIPRE.TM.CookLevin.Desc.exists_state (e G : ℕ) {F : Fields} (h : IsState e F) : ∃ (t : Fin (Sof e + 1)) (q : Option Interp.Ctl), decodeVar e G F = some (TabVar.state t q)

theorem MIPRE.TM.CookLevin.Desc.exists_emitOne (e G : ℕ) {F : Fields} (h : IsEmitOne e F) : ∃ (t : Fin (Sof e)), decodeVar e G F = some (TabVar.emitOne t)

theorem MIPRE.TM.CookLevin.Desc.exists_emitBad (e G : ℕ) {F : Fields} (h : IsEmitBad e F) : ∃ (t : Fin (Sof e)), decodeVar e G F = some (TabVar.emitBad t)

theorem MIPRE.TM.CookLevin.Desc.exists_emitted (e G : ℕ) {F : Fields} (h : IsEmitted e F) : ∃ (t : Fin (Sof e + 1)), decodeVar e G F = some (TabVar.emitted t)

theorem MIPRE.TM.CookLevin.Desc.exists_aux (e G : ℕ) {F : Fields} (h : IsAux e G F) : ∃ (t : Fin (Sof e)) (js : Tape 7 6 → Center (Sof e)) (g : Fin G), decodeVar e G F = some (TabVar.aux t js g)

def MIPRE.TM.CookLevin.Desc.cellEq (F F' : Fields) : Prop

Two records denote the same cell variable.

Equations

• MIPRE.TM.CookLevin.Desc.cellEq F F' = (F.t = F'.t ∧ F.d = F'.d ∧ F.p = F'.p ∧ F.v = F'.v)

def MIPRE.TM.CookLevin.Desc.headEq (F F' : Fields) : Prop

Two records denote the same head variable.

Equations

• MIPRE.TM.CookLevin.Desc.headEq F F' = (F.t = F'.t ∧ F.d = F'.d ∧ F.p = F'.p)

def MIPRE.TM.CookLevin.Desc.stateEq (F F' : Fields) : Prop

Two records denote the same state variable.

Equations

• MIPRE.TM.CookLevin.Desc.stateEq F F' = (F.t = F'.t ∧ F.q = F'.q)

def MIPRE.TM.CookLevin.Desc.auxEq (F F' : Fields) : Prop

Two records denote the same gate variable.

Equations

• MIPRE.TM.CookLevin.Desc.auxEq F F' = (F.t = F'.t ∧ (∀ (k : Fin 13), F.js k = F'.js k) ∧ F.g = F'.g)

theorem MIPRE.TM.CookLevin.Desc.decodeVar_cell_congr (e G : ℕ) {F F' : Fields} (h : IsCell e F) (h' : IsCell e F') (heq : cellEq F F') : decodeVar e G F = decodeVar e G F'

theorem MIPRE.TM.CookLevin.Desc.cellEq_of_decode (e G : ℕ) {F F' : Fields} {t : Fin (Sof e + 1)} {d : Tape 7 6} {p : Pos (Sof e)} {v : CellVal Interp.Sym} (h : decodeVar e G F = some (TabVar.cell t d p v)) (h' : decodeVar e G F' = some (TabVar.cell t d p v)) : cellEq F F'

theorem MIPRE.TM.CookLevin.Desc.decodeVar_head_congr (e G : ℕ) {F F' : Fields} (h : IsHead e F) (h' : IsHead e F') (heq : headEq F F') : decodeVar e G F = decodeVar e G F'

theorem MIPRE.TM.CookLevin.Desc.headEq_of_decode (e G : ℕ) {F F' : Fields} {t : Fin (Sof e + 1)} {d : Tape 7 6} {p : Pos (Sof e)} (h : decodeVar e G F = some (TabVar.head t d p)) (h' : decodeVar e G F' = some (TabVar.head t d p)) : headEq F F'

theorem MIPRE.TM.CookLevin.Desc.decodeVar_state_congr (e G : ℕ) {F F' : Fields} (h : IsState e F) (h' : IsState e F') (heq : stateEq F F') : decodeVar e G F = decodeVar e G F'

theorem MIPRE.TM.CookLevin.Desc.stateEq_of_decode (e G : ℕ) {F F' : Fields} {t : Fin (Sof e + 1)} {q : Option Interp.Ctl} (h : decodeVar e G F = some (TabVar.state t q)) (h' : decodeVar e G F' = some (TabVar.state t q)) : stateEq F F'

theorem MIPRE.TM.CookLevin.Desc.decodeVar_emitBad_congr (e G : ℕ) {F F' : Fields} (h : IsEmitBad e F) (h' : IsEmitBad e F') (heq : F.t = F'.t) : decodeVar e G F = decodeVar e G F'

theorem MIPRE.TM.CookLevin.Desc.decodeVar_emitted_congr (e G : ℕ) {F F' : Fields} (h : IsEmitted e F) (h' : IsEmitted e F') (heq : F.t = F'.t) : decodeVar e G F = decodeVar e G F'

theorem MIPRE.TM.CookLevin.Desc.decodeVar_aux_congr (e G : ℕ) {F F' : Fields} (h : IsAux e G F) (h' : IsAux e G F') (heq : auxEq F F') : decodeVar e G F = decodeVar e G F'

theorem MIPRE.TM.CookLevin.Desc.auxEq_of_decode (e G : ℕ) {F F' : Fields} {t : Fin (Sof e)} {js : Tape 7 6 → Center (Sof e)} {g : Fin G} (h : decodeVar e G F = some (TabVar.aux t js g)) (h' : decodeVar e G F' = some (TabVar.aux t js g)) : auxEq F F'

theorem MIPRE.TM.CookLevin.Desc.symCode_inj {v v' : CellVal Interp.Sym} : symCode v = symCode v' ↔ v = v'

theorem MIPRE.TM.CookLevin.Desc.qCode_inj {q q' : Option Interp.Ctl} : qCode q = qCode q' ↔ q = q'

theorem MIPRE.TM.CookLevin.Desc.tapeCode_inl (j : Fin 7) : tapeCode (Sum.inl j) = ↑j

theorem MIPRE.TM.CookLevin.Desc.tapeCode_inr (j : Fin 6) : tapeCode (Sum.inr j) = 7 + ↑j

theorem MIPRE.TM.CookLevin.Desc.seven_le_tapeCode_iff (d : Tape 7 6) : 7 ≤ tapeCode d ↔ ∃ (j : Fin 6), d = Sum.inr j

Unit clauses by kind

def MIPRE.TM.CookLevin.Desc.UnitCell (e : ℕ) (c : Cand) : Prop

The three records denote the same cell variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.UnitHead (e : ℕ) (c : Cand) : Prop

The three records denote the same head variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.UnitState (e : ℕ) (c : Cand) : Prop

The three records denote the same state variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.UnitEmitBad (e : ℕ) (c : Cand) : Prop

The three records denote the same emitBad variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.UnitEmitted (e : ℕ) (c : Cand) : Prop

The three records denote the same emitted variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.UnitAux (e G : ℕ) (c : Cand) : Prop

The three records denote the same gate variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.SameSigns (c : Cand) : Prop

The three signs agree.

Equations

• MIPRE.TM.CookLevin.Desc.SameSigns c = (c.s₂ = c.s₁ ∧ c.s₃ = c.s₁)

theorem MIPRE.TM.CookLevin.Desc.dec_unit_cell (e G : ℕ) (c : Cand) (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym) (b : Bool) : Cand.Dec e G c (unit (TabVar.cell t d p v) b) ↔ decodeVar e G c.F₁ = some (TabVar.cell t d p v) ∧ UnitCell e c ∧ c.s₁ = b ∧ SameSigns c

theorem MIPRE.TM.CookLevin.Desc.dec_unit_head (e G : ℕ) (c : Cand) (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) (b : Bool) : Cand.Dec e G c (unit (TabVar.head t d p) b) ↔ decodeVar e G c.F₁ = some (TabVar.head t d p) ∧ UnitHead e c ∧ c.s₁ = b ∧ SameSigns c

theorem MIPRE.TM.CookLevin.Desc.dec_unit_state (e G : ℕ) (c : Cand) (t : Fin (Sof e + 1)) (q : Option Interp.Ctl) (b : Bool) : Cand.Dec e G c (unit (TabVar.state t q) b) ↔ decodeVar e G c.F₁ = some (TabVar.state t q) ∧ UnitState e c ∧ c.s₁ = b ∧ SameSigns c

theorem MIPRE.TM.CookLevin.Desc.dec_unit_emitBad (e G : ℕ) (c : Cand) (t : Fin (Sof e)) (b : Bool) : Cand.Dec e G c (unit (TabVar.emitBad t) b) ↔ decodeVar e G c.F₁ = some (TabVar.emitBad t) ∧ UnitEmitBad e c ∧ c.s₁ = b ∧ SameSigns c

theorem MIPRE.TM.CookLevin.Desc.dec_unit_emitted (e G : ℕ) (c : Cand) (t : Fin (Sof e + 1)) (b : Bool) : Cand.Dec e G c (unit (TabVar.emitted t) b) ↔ decodeVar e G c.F₁ = some (TabVar.emitted t) ∧ UnitEmitted e c ∧ c.s₁ = b ∧ SameSigns c

theorem MIPRE.TM.CookLevin.Desc.dec_unit_aux (e G : ℕ) (c : Cand) (t : Fin (Sof e)) (js : Tape 7 6 → Center (Sof e)) (g : Fin G) (b : Bool) : Cand.Dec e G c (unit (TabVar.aux t js g) b) ↔ decodeVar e G c.F₁ = some (TabVar.aux t js g) ∧ UnitAux e G c ∧ c.s₁ = b ∧ SameSigns c

theorem MIPRE.TM.CookLevin.Desc.exists_mem_union {α : Type u_1} (A B : Set α) (P : α → Prop) : (∃ x ∈ A ∪ B, P x) ↔ (∃ x ∈ A, P x) ∨ ∃ x ∈ B, P x

The start family

def MIPRE.TM.CookLevin.Desc.StartHead (e : ℕ) (c : Cand) : Prop

unit (head 0 d p) (decide (p = startCell S d)).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.startHead_iff (e G : ℕ) (c : Cand) : StartHead e c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (d : Tape 7 6) (p : Pos (Sof e)), cl = unit (TabVar.head 0 d p) (decide (p = startCell (Sof e) d))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.StartState (e : ℕ) (c : Cand) : Prop

unit (state 0 q) (decide (q = some U.q₀)).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.startState_iff (e G : ℕ) (c : Cand) : StartState e c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (q : Option Interp.Ctl), cl = unit (TabVar.state 0 q) (decide (q = some Interp.U.q₀))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.StartFixed (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

unit (cell 0 (inl j) p v) (decide (v = inputCellVal x p)) for fixed j = some x.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.startFixed_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : StartFixed e fixed c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (x : List Interp.Sym) (p : Pos (Sof e)) (v : CellVal Interp.Sym), fixed j = some x ∧ cl = unit (TabVar.cell 0 (Sum.inl j) p v) (decide (v = inputCellVal x p))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.StartWork (e : ℕ) (c : Cand) : Prop

unit (cell 0 (inr j) p v) (decide (v = workCellVal₀ p)).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.startWork_iff (e G : ℕ) (c : Cand) : StartWork e c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym), cl = unit (TabVar.cell 0 (Sum.inr j) p v) (decide (v = workCellVal₀ p))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.StartPred (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

The start family.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.startPred_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : StartPred e fixed c ↔ ∃ cl ∈ startClauses (Sof e) G Interp.U fixed, Cand.Dec e G c cl

The free family

def MIPRE.TM.CookLevin.Desc.FreeTape (fixed : Fin 7 → Option (List Interp.Sym)) (F : Fields) : Prop

The tape F.d is free.

Equations

• MIPRE.TM.CookLevin.Desc.FreeTape fixed F = ∃ (j : Fin 7), fixed j = none ∧ F.d = ↑j

def MIPRE.TM.CookLevin.Desc.Bdry (S p : ℕ) : Prop

p is a boundary cell.

Equations

• MIPRE.TM.CookLevin.Desc.Bdry S p = (p < 2 ∨ 2 * S + 5 ≤ p)

@[instance_reducible]

instance MIPRE.TM.CookLevin.Desc.instDecidableBdry (S p : ℕ) : Decidable (Bdry S p)

Equations

• MIPRE.TM.CookLevin.Desc.instDecidableBdry S p = id inferInstance

def MIPRE.TM.CookLevin.Desc.FreeBdry (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

unit (cell 0 (inl j) p v) (decide (v = bdry)) for p a boundary cell.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freeBdry_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreeBdry e fixed c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (p : Pos (Sof e)) (v : CellVal Interp.Sym), fixed j = none ∧ p.IsBdry ∧ cl = unit (TabVar.cell 0 (Sum.inl j) p v) (decide (v = CellVal.bdry))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.FreeOther (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

unit (cell 0 (inl j) p v) false for p interior and v none of 0, 1, blank.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freeOther_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreeOther e fixed c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (p : Pos (Sof e)) (v : CellVal Interp.Sym), fixed j = none ∧ ¬p.IsBdry ∧ v ≠ CellVal.sym Interp.Sym.zero ∧ v ≠ CellVal.sym Interp.Sym.one ∧ v ≠ CellVal.blank ∧ cl = unit (TabVar.cell 0 (Sum.inl j) p v) false}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.FreeTwo (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

unit (cell 0 (inl j) 2 v) (decide (v = blank)).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freeTwo_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreeTwo e fixed c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (v : CellVal Interp.Sym), fixed j = none ∧ cl = unit (TabVar.cell 0 (Sum.inl j) ⟨2, ⋯⟩ v) (decide (v = CellVal.blank))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.samePos (F F' : Fields) : Prop

The records F and F' denote cells of the same tape and position.

Equations

• MIPRE.TM.CookLevin.Desc.samePos F F' = (F.t = F'.t ∧ F.d = F'.d ∧ F.p = F'.p)

def MIPRE.TM.CookLevin.Desc.FreeOneOf (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

cell 0 (inl j) p 0 ∨ cell 0 (inl j) p 1 ∨ cell 0 (inl j) p blank for p interior.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freeOneOf_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreeOneOf e fixed c ↔ ∃ c' ∈ {c' : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (p : Pos (Sof e)), fixed j = none ∧ ¬p.IsBdry ∧ c' = SAT.cl { var := TabVar.cell 0 (Sum.inl j) p (CellVal.sym Interp.Sym.zero), pos := true } { var := TabVar.cell 0 (Sum.inl j) p (CellVal.sym Interp.Sym.one), pos := true } { var := TabVar.cell 0 (Sum.inl j) p CellVal.blank, pos := true }}, Cand.Dec e G c c'

def MIPRE.TM.CookLevin.Desc.FreeNand (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

nand2 (cell 0 (inl j) p v) (cell 0 (inl j) p v') for p interior and v ≠ v'.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freeNand_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreeNand e fixed c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (p : Pos (Sof e)) (v : CellVal Interp.Sym) (v' : CellVal Interp.Sym), fixed j = none ∧ ¬p.IsBdry ∧ v ≠ v' ∧ cl = nand2 (TabVar.cell 0 (Sum.inl j) p v) (TabVar.cell 0 (Sum.inl j) p v')}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.FreeBlank (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

imp2 (cell 0 (inl j) p blank) (cell 0 (inl j) p' blank) for 2 < p < p', p' interior.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freeBlank_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreeBlank e fixed c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (j : Fin 7) (p : Pos (Sof e)) (p' : Pos (Sof e)), fixed j = none ∧ 2 < ↑p ∧ ¬p'.IsBdry ∧ p < p' ∧ cl = imp2 (TabVar.cell 0 (Sum.inl j) p CellVal.blank) (TabVar.cell 0 (Sum.inl j) p' CellVal.blank)}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.FreePred (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

The free family.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.freePred_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : FreePred e fixed c ↔ ∃ cl ∈ freeClauses (Sof e) G Interp.Sym.zero Interp.Sym.one fixed, Cand.Dec e G c cl

The boundary family

def MIPRE.TM.CookLevin.Desc.BdryCell (e : ℕ) (c : Cand) : Prop

unit (cell t d p v) (decide (v = bdry)) for p a boundary cell.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.bdryCell_iff (e G : ℕ) (c : Cand) : BdryCell e c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)) (v : CellVal Interp.Sym), p.IsBdry ∧ cl = unit (TabVar.cell t d p v) (decide (v = CellVal.bdry))}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.BdryHead (e : ℕ) (c : Cand) : Prop

unit (head t d p) false for p a boundary cell.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.bdryHead_iff (e G : ℕ) (c : Cand) : BdryHead e c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e + 1)) (d : Tape 7 6) (p : Pos (Sof e)), p.IsBdry ∧ cl = unit (TabVar.head t d p) false}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.BdryPred (e : ℕ) (c : Cand) : Prop

The boundary family.

Equations

• MIPRE.TM.CookLevin.Desc.BdryPred e c = (MIPRE.TM.CookLevin.Desc.BdryCell e c ∨ MIPRE.TM.CookLevin.Desc.BdryHead e c)

theorem MIPRE.TM.CookLevin.Desc.bdryPred_iff (e G : ℕ) (c : Cand) : BdryPred e c ↔ ∃ cl ∈ bdryClauses (Sof e) G, Cand.Dec e G c cl

The emission family

def MIPRE.TM.CookLevin.Desc.EmitZero (e : ℕ) (c : Cand) : Prop

unit (emitted 0) false.

Equations

• MIPRE.TM.CookLevin.Desc.EmitZero e c = (MIPRE.TM.CookLevin.Desc.UnitEmitted e c ∧ MIPRE.TM.CookLevin.Desc.SameSigns c ∧ c.F₁.t = 0 ∧ c.s₁ = false)

theorem MIPRE.TM.CookLevin.Desc.emitZero_iff (e G : ℕ) (c : Cand) : EmitZero e c ↔ ∃ cl ∈ {unit (TabVar.emitted 0) false}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.EmitStep (e : ℕ) (c : Cand) : Prop

¬ emitted (t + 1) ∨ emitted t ∨ emitOne t.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.emitStep_iff (e G : ℕ) (c : Cand) : EmitStep e c ↔ ∃ c' ∈ {c' : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e)), c' = SAT.cl { var := TabVar.emitted t.succ, pos := false } { var := TabVar.emitted t.castSucc, pos := true } { var := TabVar.emitOne t, pos := true }}, Cand.Dec e G c c'

def MIPRE.TM.CookLevin.Desc.EmitMono (e : ℕ) (c : Cand) : Prop

imp2 (emitted t) (emitted (t + 1)).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.emitMono_iff (e G : ℕ) (c : Cand) : EmitMono e c ↔ ∃ c' ∈ {c' : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e)), c' = imp2 (TabVar.emitted t.castSucc) (TabVar.emitted t.succ)}, Cand.Dec e G c c'

def MIPRE.TM.CookLevin.Desc.EmitOne (e : ℕ) (c : Cand) : Prop

imp2 (emitOne t) (emitted (t + 1)).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.emitOne_iff (e G : ℕ) (c : Cand) : EmitOne e c ↔ ∃ c' ∈ {c' : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e)), c' = imp2 (TabVar.emitOne t) (TabVar.emitted t.succ)}, Cand.Dec e G c c'

def MIPRE.TM.CookLevin.Desc.EmitOnce (e : ℕ) (c : Cand) : Prop

nand2 (emitOne t) (emitted t).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.emitOnce_iff (e G : ℕ) (c : Cand) : EmitOnce e c ↔ ∃ c' ∈ {c' : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e)), c' = nand2 (TabVar.emitOne t) (TabVar.emitted t.castSucc)}, Cand.Dec e G c c'

def MIPRE.TM.CookLevin.Desc.EmitBad (e : ℕ) (c : Cand) : Prop

unit (emitBad t) false.

Equations

• MIPRE.TM.CookLevin.Desc.EmitBad e c = (MIPRE.TM.CookLevin.Desc.UnitEmitBad e c ∧ MIPRE.TM.CookLevin.Desc.SameSigns c ∧ c.s₁ = false)

theorem MIPRE.TM.CookLevin.Desc.emitBad_iff (e G : ℕ) (c : Cand) : EmitBad e c ↔ ∃ cl ∈ {cl : SAT.Clause3 (TabVar 7 6 Interp.Sym Interp.Ctl (Sof e) G) | ∃ (t : Fin (Sof e)), cl = unit (TabVar.emitBad t) false}, Cand.Dec e G c cl

def MIPRE.TM.CookLevin.Desc.EmitPred (e : ℕ) (c : Cand) : Prop

The emission family.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.emitPred_iff (e G : ℕ) (c : Cand) : EmitPred e c ↔ ∃ cl ∈ emitClauses (Sof e) G, Cand.Dec e G c cl

The final family

def MIPRE.TM.CookLevin.Desc.FinalState (e : ℕ) (c : Cand) : Prop

unit (state S none) true.

Equations

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

def MIPRE.TM.CookLevin.Desc.FinalEmitted (e : ℕ) (c : Cand) : Prop

unit (emitted S) true.

Equations

• MIPRE.TM.CookLevin.Desc.FinalEmitted e c = (MIPRE.TM.CookLevin.Desc.UnitEmitted e c ∧ MIPRE.TM.CookLevin.Desc.SameSigns c ∧ c.F₁.t = MIPRE.TM.CookLevin.Desc.Sof e ∧ c.s₁ = true)

def MIPRE.TM.CookLevin.Desc.FinalPred (e : ℕ) (c : Cand) : Prop

The final family.

Equations

• MIPRE.TM.CookLevin.Desc.FinalPred e c = (MIPRE.TM.CookLevin.Desc.FinalState e c ∨ MIPRE.TM.CookLevin.Desc.FinalEmitted e c)

theorem MIPRE.TM.CookLevin.Desc.finalPred_iff (e G : ℕ) (c : Cand) : FinalPred e c ↔ ∃ cl ∈ finalClauses (Sof e) G, Cand.Dec e G c cl

The non-window families together

def MIPRE.TM.CookLevin.Desc.MainPred (e : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : Prop

The five explicit families.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.mainPred_iff (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (c : Cand) : MainPred e fixed c ↔ ∃ cl ∈ startClauses (Sof e) G Interp.U fixed ∪ freeClauses (Sof e) G Interp.Sym.zero Interp.Sym.one fixed ∪ bdryClauses (Sof e) G ∪ emitClauses (Sof e) G ∪ finalClauses (Sof e) G, Cand.Dec e G c cl

The candidate decodes to a clause of the five explicit families iff MainPred.