The clause families as formulas

For each family predicate of Families.lean and Window.lean, the formula computing it on a candidate of field formulas (CandF: three FieldsF and three sign formulas), with its exact semantics (eval_startF, …, eval_windowF) and its input bound. The fixed input tapes enter through value formulas (cellValF for a listed string, unaryValF for the unary time bound), tied to fixed by TapeSpec; the free tapes through the list of their indices (FreeSpec) (planning/succinct-cook-levin.md, S3).

Helpers

theorem MIPRE.TM.CookLevin.Desc.Bool.eq_decide_of_iff {b : Bool} {P : Prop} [Decidable P] (h : b = true ↔ P) : b = decide P

theorem MIPRE.TM.CookLevin.Desc.eval_eqN {fs : List SAT.Fml} {w k : ℕ} (hl : fs.length = w) (hk : k < 2 ^ w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.eqConst fs (nbits w k)) = true ↔ SAT.Fml.val fs x = k

theorem MIPRE.TM.CookLevin.Desc.eval_ltN {fs : List SAT.Fml} {w k : ℕ} (hl : fs.length = w) (hk : k < 2 ^ w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.ltConst fs (nbits w k)) = true ↔ SAT.Fml.val fs x < k

theorem MIPRE.TM.CookLevin.Desc.eval_eqF {fs gs : List SAT.Fml} {w : ℕ} (hl : fs.length = w) (hg : gs.length = w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.eqFields fs gs) = true ↔ SAT.Fml.val fs x = SAT.Fml.val gs x

theorem MIPRE.TM.CookLevin.Desc.eval_ltF {fs gs : List SAT.Fml} {w : ℕ} (hl : fs.length = w) (hg : gs.length = w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.ltFields fs gs) = true ↔ SAT.Fml.val fs x < SAT.Fml.val gs x

theorem MIPRE.TM.CookLevin.Desc.eval_addN {fs gs : List SAT.Fml} {w k : ℕ} (hl : fs.length = w) (hg : gs.length = w) (hk : k < 2 ^ w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.addConstRel fs gs (nbits w k)) = true ↔ SAT.Fml.val gs x = SAT.Fml.val fs x + k

theorem MIPRE.TM.CookLevin.Desc.eval_xnor_iff (f g : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (f.xnor g) = true ↔ SAT.Fml.eval x f = SAT.Fml.eval x g

theorem MIPRE.TM.CookLevin.Desc.eval_sign (σ f : SAT.Fml) (x : ℕ → Bool) {P : Prop} [Decidable P] (hf : SAT.Fml.eval x f = true ↔ P) : SAT.Fml.eval x (σ.xnor f) = true ↔ SAT.Fml.eval x σ = decide P

theorem MIPRE.TM.CookLevin.Desc.eval_signConst (σ : SAT.Fml) (b : Bool) (x : ℕ → Bool) : SAT.Fml.eval x (σ.xnor (SAT.Fml.const b)) = true ↔ SAT.Fml.eval x σ = b

theorem MIPRE.TM.CookLevin.Desc.eval_not_iff (f : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x f.not = true ↔ ¬SAT.Fml.eval x f = true

theorem MIPRE.TM.CookLevin.Desc.eval_and_iff (f g : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (f.and g) = true ↔ SAT.Fml.eval x f = true ∧ SAT.Fml.eval x g = true

theorem MIPRE.TM.CookLevin.Desc.eval_or_iff (f g : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (f.or g) = true ↔ SAT.Fml.eval x f = true ∨ SAT.Fml.eval x g = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₂ (a b : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₃ (a b c : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₄ (a b c d : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c, d]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true ∧ SAT.Fml.eval x d = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₅ (a b c d f : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c, d, f]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true ∧ SAT.Fml.eval x d = true ∧ SAT.Fml.eval x f = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₆ (a b c d f g : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c, d, f, g]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true ∧ SAT.Fml.eval x d = true ∧ SAT.Fml.eval x f = true ∧ SAT.Fml.eval x g = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₇ (a b c d f g h : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c, d, f, g, h]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true ∧ SAT.Fml.eval x d = true ∧ SAT.Fml.eval x f = true ∧ SAT.Fml.eval x g = true ∧ SAT.Fml.eval x h = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₈ (a b c d f g h i : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c, d, f, g, h, i]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true ∧ SAT.Fml.eval x d = true ∧ SAT.Fml.eval x f = true ∧ SAT.Fml.eval x g = true ∧ SAT.Fml.eval x h = true ∧ SAT.Fml.eval x i = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList₉ (a b c d f g h i j : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList [a, b, c, d, f, g, h, i, j]) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x b = true ∧ SAT.Fml.eval x c = true ∧ SAT.Fml.eval x d = true ∧ SAT.Fml.eval x f = true ∧ SAT.Fml.eval x g = true ∧ SAT.Fml.eval x h = true ∧ SAT.Fml.eval x i = true ∧ SAT.Fml.eval x j = true

theorem MIPRE.TM.CookLevin.Desc.InputsLt.and' {n : ℕ} {f g : SAT.Fml} (hf : SAT.Fml.InputsLt n f) (hg : SAT.Fml.InputsLt n g) : SAT.Fml.InputsLt n (f.and g)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.or' {n : ℕ} {f g : SAT.Fml} (hf : SAT.Fml.InputsLt n f) (hg : SAT.Fml.InputsLt n g) : SAT.Fml.InputsLt n (f.or g)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.not' {n : ℕ} {f : SAT.Fml} (hf : SAT.Fml.InputsLt n f) : SAT.Fml.InputsLt n f.not

theorem MIPRE.TM.CookLevin.Desc.InputsLt.list_cons {n : ℕ} {f : SAT.Fml} {l : List SAT.Fml} (hf : SAT.Fml.InputsLt n f) (hl : ∀ g ∈ l, SAT.Fml.InputsLt n g) (g : SAT.Fml) : g ∈ f :: l → SAT.Fml.InputsLt n g

theorem MIPRE.TM.CookLevin.Desc.InputsLt.list_nil {n : ℕ} (g : SAT.Fml) : g ∈ [] → SAT.Fml.InputsLt n g

Input bounds of the field formulas

structure MIPRE.TM.CookLevin.Desc.FieldsF.InputsLt (n : ℕ) (A : FieldsF) : Prop

The field formulas read only inputs below n.

• flag : SAT.Fml.InputsLt n A.flag
• tag (f : SAT.Fml) : f ∈ A.tag → SAT.Fml.InputsLt n f
• t (f : SAT.Fml) : f ∈ A.t → SAT.Fml.InputsLt n f
• d (f : SAT.Fml) : f ∈ A.d → SAT.Fml.InputsLt n f
• p (f : SAT.Fml) : f ∈ A.p → SAT.Fml.InputsLt n f
• v (f : SAT.Fml) : f ∈ A.v → SAT.Fml.InputsLt n f
• q (f : SAT.Fml) : f ∈ A.q → SAT.Fml.InputsLt n f
• js (k : Fin 13) (f : SAT.Fml) : f ∈ A.js k → SAT.Fml.InputsLt n f
• g (f : SAT.Fml) : f ∈ A.g → SAT.Fml.InputsLt n f
• ansOk : SAT.Fml.InputsLt n A.ansOk

theorem MIPRE.TM.CookLevin.Desc.InputsLt.muxList {n : ℕ} {s : SAT.Fml} {as bs : List SAT.Fml} (hs : SAT.Fml.InputsLt n s) (ha : ∀ f ∈ as, SAT.Fml.InputsLt n f) (hb : ∀ f ∈ bs, SAT.Fml.InputsLt n f) (f : SAT.Fml) : f ∈ Desc.muxList s as bs → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.cst {n w c : ℕ} (f : SAT.Fml) : f ∈ Desc.cst w c → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.take {n : ℕ} {l : List SAT.Fml} (h : ∀ f ∈ l, SAT.Fml.InputsLt n f) (k : ℕ) (f : SAT.Fml) : f ∈ List.take k l → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.tail {n : ℕ} {l : List SAT.Fml} (h : ∀ f ∈ l, SAT.Fml.InputsLt n f) (f : SAT.Fml) : f ∈ l.tail → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.headD {n : ℕ} {l : List SAT.Fml} (h : ∀ f ∈ l, SAT.Fml.InputsLt n f) : SAT.Fml.InputsLt n (l.headD (SAT.Fml.const false))

theorem MIPRE.TM.CookLevin.Desc.InputsLt.flagF (e G b n : ℕ) (hn : b + mOf e G ≤ n) : SAT.Fml.InputsLt n (Desc.flagF e G b)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.jF (e G b n : ℕ) (hn : b + mOf e G ≤ n) (f : SAT.Fml) : f ∈ Desc.jF e G b → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.rF (e G T b n : ℕ) (hn : b + mOf e G ≤ n) (f : SAT.Fml) : f ∈ Desc.rF e G T b → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.pAnsF (e G T b n : ℕ) (hn : b + mOf e G ≤ n) (f : SAT.Fml) : f ∈ Desc.pAnsF e G T b → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.fieldOff (e G b n : ℕ) (hn : b + mOf e G ≤ n) (off w : ℕ) (h : off + w ≤ mOf e G) (f : SAT.Fml) : f ∈ SAT.Fml.field (b + off) w → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.jsOff_add_le (e G : ℕ) (k : Fin 13) : jsOff e ↑k + W e ≤ mOf e G

theorem MIPRE.TM.CookLevin.Desc.qOff_add_le (e G : ℕ) : qOff e + Qb ≤ mOf e G

theorem MIPRE.TM.CookLevin.Desc.gOff_add_le (e G : ℕ) : gOff e + Gb G ≤ mOf e G

theorem MIPRE.TM.CookLevin.Desc.litFields_inputsLt (e G T b n : ℕ) (hn : b + mOf e G ≤ n) : FieldsF.InputsLt n (litFields e G T b)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isCellF {e n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isCellF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isHeadF {e n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isHeadF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isStateF {e n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isStateF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isEmitOneF {e n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isEmitOneF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isEmitBadF {e n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isEmitBadF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isEmittedF {e n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isEmittedF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.isAuxF {e G n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.isAuxF e G A)

Candidates of formulas

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

A candidate of formulas: three field records and three sign formulas.

• A₁ : FieldsF
• σ₁ : SAT.Fml
• A₂ : FieldsF
• σ₂ : SAT.Fml
• A₃ : FieldsF
• σ₃ : SAT.Fml

def MIPRE.TM.CookLevin.Desc.evalCand (C : CandF) (x : ℕ → Bool) : Cand

The candidate a candidate of formulas evaluates to.

Equations

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

structure MIPRE.TM.CookLevin.Desc.CandF.Lengths (e G : ℕ) (C : CandF) : Prop

The three records have the field lengths.

• A₁ : FieldsF.Lengths e G C.A₁
• A₂ : FieldsF.Lengths e G C.A₂
• A₃ : FieldsF.Lengths e G C.A₃

structure MIPRE.TM.CookLevin.Desc.CandF.InputsLt (n : ℕ) (C : CandF) : Prop

The candidate reads only inputs below n.

• A₁ : FieldsF.InputsLt n C.A₁
• σ₁ : SAT.Fml.InputsLt n C.σ₁
• A₂ : FieldsF.InputsLt n C.A₂
• σ₂ : SAT.Fml.InputsLt n C.σ₂
• A₃ : FieldsF.InputsLt n C.A₃
• σ₃ : SAT.Fml.InputsLt n C.σ₃

Same-variable formulas

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

cellEq.

Equations

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

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

headEq.

Equations

• MIPRE.TM.CookLevin.Desc.headEqF A B = MIPRE.SAT.Fml.andList [MIPRE.SAT.Fml.eqFields A.t B.t, MIPRE.SAT.Fml.eqFields A.d B.d, MIPRE.SAT.Fml.eqFields A.p B.p]

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

stateEq.

Equations

• MIPRE.TM.CookLevin.Desc.stateEqF A B = MIPRE.SAT.Fml.andList [MIPRE.SAT.Fml.eqFields A.t B.t, MIPRE.SAT.Fml.eqFields A.q B.q]

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

auxEq.

Equations

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

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

samePos.

Equations

• MIPRE.TM.CookLevin.Desc.samePosF A B = MIPRE.SAT.Fml.andList [MIPRE.SAT.Fml.eqFields A.t B.t, MIPRE.SAT.Fml.eqFields A.d B.d, MIPRE.SAT.Fml.eqFields A.p B.p]

theorem MIPRE.TM.CookLevin.Desc.eval_cellEqF (e G : ℕ) {A B : FieldsF} (hA : FieldsF.Lengths e G A) (hB : FieldsF.Lengths e G B) (x : ℕ → Bool) : SAT.Fml.eval x (cellEqF A B) = true ↔ cellEq (evalFields A x) (evalFields B x)

theorem MIPRE.TM.CookLevin.Desc.eval_headEqF (e G : ℕ) {A B : FieldsF} (hA : FieldsF.Lengths e G A) (hB : FieldsF.Lengths e G B) (x : ℕ → Bool) : SAT.Fml.eval x (headEqF A B) = true ↔ headEq (evalFields A x) (evalFields B x)

theorem MIPRE.TM.CookLevin.Desc.eval_stateEqF (e G : ℕ) {A B : FieldsF} (hA : FieldsF.Lengths e G A) (hB : FieldsF.Lengths e G B) (x : ℕ → Bool) : SAT.Fml.eval x (stateEqF A B) = true ↔ stateEq (evalFields A x) (evalFields B x)

theorem MIPRE.TM.CookLevin.Desc.eval_samePosF (e G : ℕ) {A B : FieldsF} (hA : FieldsF.Lengths e G A) (hB : FieldsF.Lengths e G B) (x : ℕ → Bool) : SAT.Fml.eval x (samePosF A B) = true ↔ samePos (evalFields A x) (evalFields B x)

theorem MIPRE.TM.CookLevin.Desc.eval_tEqF (e G : ℕ) {A B : FieldsF} (hA : FieldsF.Lengths e G A) (hB : FieldsF.Lengths e G B) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.eqFields A.t B.t) = true ↔ (evalFields A x).t = (evalFields B x).t

theorem MIPRE.TM.CookLevin.Desc.eval_auxEqF (e G : ℕ) {A B : FieldsF} (hA : FieldsF.Lengths e G A) (hB : FieldsF.Lengths e G B) (x : ℕ → Bool) : SAT.Fml.eval x (auxEqF A B) = true ↔ auxEq (evalFields A x) (evalFields B x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.cellEqF {n : ℕ} {A B : FieldsF} (hA : FieldsF.InputsLt n A) (hB : FieldsF.InputsLt n B) : SAT.Fml.InputsLt n (Desc.cellEqF A B)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.headEqF {n : ℕ} {A B : FieldsF} (hA : FieldsF.InputsLt n A) (hB : FieldsF.InputsLt n B) : SAT.Fml.InputsLt n (Desc.headEqF A B)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.stateEqF {n : ℕ} {A B : FieldsF} (hA : FieldsF.InputsLt n A) (hB : FieldsF.InputsLt n B) : SAT.Fml.InputsLt n (Desc.stateEqF A B)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.samePosF {n : ℕ} {A B : FieldsF} (hA : FieldsF.InputsLt n A) (hB : FieldsF.InputsLt n B) : SAT.Fml.InputsLt n (Desc.samePosF A B)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.tEqF {n : ℕ} {A B : FieldsF} (hA : FieldsF.InputsLt n A) (hB : FieldsF.InputsLt n B) : SAT.Fml.InputsLt n (SAT.Fml.eqFields A.t B.t)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.auxEqF {n : ℕ} {A B : FieldsF} (hA : FieldsF.InputsLt n A) (hB : FieldsF.InputsLt n B) : SAT.Fml.InputsLt n (Desc.auxEqF A B)

Unit clauses and signs

def MIPRE.TM.CookLevin.Desc.unitCellF (e : ℕ) (C : CandF) : SAT.Fml

UnitCell.

Equations

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

def MIPRE.TM.CookLevin.Desc.unitHeadF (e : ℕ) (C : CandF) : SAT.Fml

UnitHead.

Equations

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

def MIPRE.TM.CookLevin.Desc.unitStateF (e : ℕ) (C : CandF) : SAT.Fml

UnitState.

Equations

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

def MIPRE.TM.CookLevin.Desc.unitEmitBadF (e : ℕ) (C : CandF) : SAT.Fml

UnitEmitBad.

Equations

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

def MIPRE.TM.CookLevin.Desc.unitEmittedF (e : ℕ) (C : CandF) : SAT.Fml

UnitEmitted.

Equations

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

def MIPRE.TM.CookLevin.Desc.unitAuxF (e G : ℕ) (C : CandF) : SAT.Fml

UnitAux.

Equations

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

def MIPRE.TM.CookLevin.Desc.sameSignsF (C : CandF) : SAT.Fml

SameSigns.

Equations

• MIPRE.TM.CookLevin.Desc.sameSignsF C = (C.σ₂.xnor C.σ₁).and (C.σ₃.xnor C.σ₁)

theorem MIPRE.TM.CookLevin.Desc.eval_unitCellF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (unitCellF e C) = true ↔ UnitCell e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_unitHeadF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (unitHeadF e C) = true ↔ UnitHead e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_unitStateF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (unitStateF e C) = true ↔ UnitState e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_unitEmitBadF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (unitEmitBadF e C) = true ↔ UnitEmitBad e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_unitEmittedF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (unitEmittedF e C) = true ↔ UnitEmitted e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_unitAuxF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (unitAuxF e G C) = true ↔ UnitAux e G (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_sameSignsF {C : CandF} (x : ℕ → Bool) : SAT.Fml.eval x (sameSignsF C) = true ↔ SameSigns (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unitCellF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.unitCellF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unitHeadF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.unitHeadF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unitStateF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.unitStateF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unitEmitBadF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.unitEmitBadF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unitEmittedF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.unitEmittedF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unitAuxF (e G : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.unitAuxF e G C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.sameSignsF {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.sameSignsF C)

Positions and values

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

Bdry S p.

Equations

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

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

p = 3 for an input tape, S + 3 for a work tape: the start cell.

Equations

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

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

v = workCode S p.

Equations

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

def MIPRE.TM.CookLevin.Desc.lookupList (e : ℕ) (A : FieldsF) : ℕ → List ℕ → List SAT.Fml

The lookup table of a string of codes from cell k: p = k + i ∧ v = codes[i].

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.lookupList e A x✝ [] = []

def MIPRE.TM.CookLevin.Desc.cellValF (e : ℕ) (A : FieldsF) (codes : List ℕ) : SAT.Fml

v = cellCode x S p for the string x of codes codes, of length at most S.

Equations

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

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

v = cellCode 1^T S p.

Equations

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

def MIPRE.TM.CookLevin.Desc.codesOf (x : List Interp.Sym) : List ℕ

The codes of a string.

Equations

• MIPRE.TM.CookLevin.Desc.codesOf x = List.map (fun (s : MIPRE.TM.Interp.Sym) => MIPRE.TM.CookLevin.Desc.symCode (MIPRE.TM.CookLevin.CellVal.sym s)) x

theorem MIPRE.TM.CookLevin.Desc.codesOf_lt (x : List Interp.Sym) (c : ℕ) : c ∈ codesOf x → c < 7

theorem MIPRE.TM.CookLevin.Desc.twoS5_lt (e : ℕ) : 2 * Sof e + 5 < 2 ^ W e

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

theorem MIPRE.TM.CookLevin.Desc.eval_bdryF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (bdryF e A) = true ↔ Bdry (Sof e) (evalFields A x).p

theorem MIPRE.TM.CookLevin.Desc.eval_startCellF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (startCellF e A) = true ↔ (evalFields A x).p = if (evalFields A x).d < 7 then 3 else Sof e + 3

theorem MIPRE.TM.CookLevin.Desc.eval_workValF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (workValF e A) = true ↔ (evalFields A x).v = workCode (Sof e) (evalFields A x).p

theorem MIPRE.TM.CookLevin.Desc.eval_lookupList (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (codes : List ℕ) (hc : ∀ c ∈ codes, c < 8) (k : ℕ) : k + codes.length < 2 ^ W e → (SAT.Fml.eval x (SAT.Fml.orList (lookupList e A k codes)) = true ↔ ∃ (i : ℕ) (h : i < codes.length), SAT.Fml.val A.p x = k + i ∧ SAT.Fml.val A.v x = codes[i])

theorem MIPRE.TM.CookLevin.Desc.eval_cellValF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (s : List Interp.Sym) (hs : s.length ≤ Sof e) : SAT.Fml.eval x (cellValF e A (codesOf s)) = true ↔ (evalFields A x).v = cellCode s (Sof e) (evalFields A x).p

theorem MIPRE.TM.CookLevin.Desc.eval_unaryValF (e G : ℕ) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (T : ℕ) (hT : T ≤ Sof e) : SAT.Fml.eval x (unaryValF e T A) = true ↔ (evalFields A x).v = cellCode (List.replicate T Interp.Sym.one) (Sof e) (evalFields A x).p

theorem MIPRE.TM.CookLevin.Desc.InputsLt.bdryF (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.bdryF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.startCellF (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.startCellF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.workValF (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.workValF e A)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.lookupList (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) (codes : List ℕ) (k : ℕ) (f : SAT.Fml) : f ∈ Desc.lookupList e A k codes → SAT.Fml.InputsLt n f

theorem MIPRE.TM.CookLevin.Desc.InputsLt.cellValF (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) (codes : List ℕ) : SAT.Fml.InputsLt n (Desc.cellValF e A codes)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.unaryValF (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) (T : ℕ) : SAT.Fml.InputsLt n (Desc.unaryValF e T A)

More helpers

theorem MIPRE.TM.CookLevin.Desc.eval_andList_cons (a : SAT.Fml) (l : List SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList (a :: l)) = true ↔ SAT.Fml.eval x a = true ∧ SAT.Fml.eval x (SAT.Fml.andList l) = true

theorem MIPRE.TM.CookLevin.Desc.eval_andList_nil (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.andList []) = true ↔ True

theorem MIPRE.TM.CookLevin.Desc.eval_not_false (f : SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x f.not = true ↔ SAT.Fml.eval x f = false

theorem MIPRE.TM.CookLevin.Desc.eval_gtN {fs : List SAT.Fml} {w k : ℕ} (hl : fs.length = w) (hk : k + 1 < 2 ^ w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.ltConst fs (nbits w (k + 1))).not = true ↔ k < SAT.Fml.val fs x

theorem MIPRE.TM.CookLevin.Desc.eval_geN {fs : List SAT.Fml} {w k : ℕ} (hl : fs.length = w) (hk : k < 2 ^ w) (x : ℕ → Bool) : SAT.Fml.eval x (SAT.Fml.ltConst fs (nbits w k)).not = true ↔ k ≤ SAT.Fml.val fs x

structure MIPRE.TM.CookLevin.Desc.FreeSpec (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) : Prop

The tapes fixed j = none are the indices frees.

• lt (j : ℕ) : j ∈ frees → j < 7
• iff (j : Fin 7) : fixed j = none ↔ ↑j ∈ frees

structure MIPRE.TM.CookLevin.Desc.TapeSpec (e : ℕ) (A : FieldsF) (fixed : Fin 7 → Option (List Interp.Sym)) (tabs : List (ℕ × SAT.Fml)) : Prop

The entries (j, vf) of tabs are the fixed tapes fixed j = some x, with vf computing v = cellCode x S p on the record A.

• entry (jv : ℕ × SAT.Fml) : jv ∈ tabs → ∃ (j : Fin 7) (x : List Interp.Sym), jv.1 = ↑j ∧ fixed j = some x ∧ ∀ (x' : ℕ → Bool), SAT.Fml.eval x' jv.2 = decide ((evalFields A x').v = cellCode x (Sof e) (evalFields A x').p)
• complete (j : Fin 7) (x : List Interp.Sym) : fixed j = some x → ∃ (vf : SAT.Fml), (↑j, vf) ∈ tabs

def MIPRE.TM.CookLevin.Desc.freeTapeF (frees : List ℕ) (A : FieldsF) : SAT.Fml

FreeTape.

Equations

• MIPRE.TM.CookLevin.Desc.freeTapeF frees A = MIPRE.SAT.Fml.orList (List.map (fun (j : ℕ) => MIPRE.SAT.Fml.eqConst A.d (MIPRE.TM.CookLevin.Desc.nbits 4 j)) frees)

theorem MIPRE.TM.CookLevin.Desc.eval_freeTapeF (e G : ℕ) {fixed : Fin 7 → Option (List Interp.Sym)} {frees : List ℕ} (hs : FreeSpec fixed frees) {A : FieldsF} (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) : SAT.Fml.eval x (freeTapeF frees A) = true ↔ FreeTape fixed (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeTapeF {n : ℕ} (frees : List ℕ) {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.freeTapeF frees A)

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

t = 0.

Equations

• MIPRE.TM.CookLevin.Desc.tZeroF e A = MIPRE.SAT.Fml.eqConst A.t (MIPRE.TM.CookLevin.Desc.nbits (MIPRE.TM.CookLevin.Desc.W e) 0)

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

theorem MIPRE.TM.CookLevin.Desc.InputsLt.tZeroF (e : ℕ) {n : ℕ} {A : FieldsF} (hA : FieldsF.InputsLt n A) : SAT.Fml.InputsLt n (Desc.tZeroF e A)

The start family

def MIPRE.TM.CookLevin.Desc.startHeadF (e : ℕ) (C : CandF) : SAT.Fml

StartHead.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.startStateF (e : ℕ) (C : CandF) : SAT.Fml

StartState.

Equations

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

def MIPRE.TM.CookLevin.Desc.startFixedF (e : ℕ) (tabs : List (ℕ × SAT.Fml)) (C : CandF) : SAT.Fml

StartFixed, for the tapes tabs.

Equations

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

def MIPRE.TM.CookLevin.Desc.startWorkF (e : ℕ) (C : CandF) : SAT.Fml

StartWork.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.startF (e : ℕ) (tabs : List (ℕ × SAT.Fml)) (C : CandF) : SAT.Fml

StartPred.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.eval_startHeadF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (startHeadF e C) = true ↔ StartHead e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_startStateF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (startStateF e C) = true ↔ StartState e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_startFixedF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (tabs : List (ℕ × SAT.Fml)) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (hs : TapeSpec e C.A₁ fixed tabs) : SAT.Fml.eval x (startFixedF e tabs C) = true ↔ StartFixed e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_startWorkF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (startWorkF e C) = true ↔ StartWork e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_startF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (tabs : List (ℕ × SAT.Fml)) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (hs : TapeSpec e C.A₁ fixed tabs) : SAT.Fml.eval x (startF e tabs C) = true ↔ StartPred e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.startHeadF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.startHeadF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.startStateF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.startStateF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.startFixedF (e : ℕ) {n : ℕ} (tabs : List (ℕ × SAT.Fml)) (htabs : ∀ jv ∈ tabs, SAT.Fml.InputsLt n jv.2) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.startFixedF e tabs C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.startWorkF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.startWorkF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.startF (e : ℕ) {n : ℕ} (tabs : List (ℕ × SAT.Fml)) (htabs : ∀ jv ∈ tabs, SAT.Fml.InputsLt n jv.2) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.startF e tabs C)

The free family

def MIPRE.TM.CookLevin.Desc.freeBdryF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreeBdry.

Equations

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

def MIPRE.TM.CookLevin.Desc.freeOtherF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreeOther.

Equations

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

def MIPRE.TM.CookLevin.Desc.freeTwoF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreeTwo.

Equations

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

def MIPRE.TM.CookLevin.Desc.freeOneOfF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreeOneOf.

Equations

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

def MIPRE.TM.CookLevin.Desc.freeNandF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreeNand.

Equations

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

def MIPRE.TM.CookLevin.Desc.freeBlankF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreeBlank.

Equations

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

def MIPRE.TM.CookLevin.Desc.freeF (e : ℕ) (frees : List ℕ) (C : CandF) : SAT.Fml

FreePred.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.eval_freeBdryF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeBdryF e frees C) = true ↔ FreeBdry e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_freeOtherF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeOtherF e frees C) = true ↔ FreeOther e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_freeTwoF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeTwoF e frees C) = true ↔ FreeTwo e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_freeOneOfF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeOneOfF e frees C) = true ↔ FreeOneOf e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_freeNandF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeNandF e frees C) = true ↔ FreeNand e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_freeBlankF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeBlankF e frees C) = true ↔ FreeBlank e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_freeF (e G : ℕ) (fixed : Fin 7 → Option (List Interp.Sym)) (frees : List ℕ) (hs : FreeSpec fixed frees) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (freeF e frees C) = true ↔ FreePred e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeBdryF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeBdryF e frees C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeOtherF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeOtherF e frees C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeTwoF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeTwoF e frees C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeOneOfF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeOneOfF e frees C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeNandF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeNandF e frees C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeBlankF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeBlankF e frees C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.freeF (e : ℕ) {n : ℕ} (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.freeF e frees C)

The boundary, emission and final families

def MIPRE.TM.CookLevin.Desc.bdryCellF (e : ℕ) (C : CandF) : SAT.Fml

BdryCell.

Equations

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

def MIPRE.TM.CookLevin.Desc.bdryHeadF (e : ℕ) (C : CandF) : SAT.Fml

BdryHead.

Equations

• MIPRE.TM.CookLevin.Desc.bdryHeadF e C = MIPRE.SAT.Fml.andList [MIPRE.TM.CookLevin.Desc.unitHeadF e C, MIPRE.TM.CookLevin.Desc.sameSignsF C, MIPRE.TM.CookLevin.Desc.bdryF e C.A₁, C.σ₁.not]

def MIPRE.TM.CookLevin.Desc.bdryPredF (e : ℕ) (C : CandF) : SAT.Fml

BdryPred.

Equations

• MIPRE.TM.CookLevin.Desc.bdryPredF e C = (MIPRE.TM.CookLevin.Desc.bdryCellF e C).or (MIPRE.TM.CookLevin.Desc.bdryHeadF e C)

def MIPRE.TM.CookLevin.Desc.emitZeroF (e : ℕ) (C : CandF) : SAT.Fml

EmitZero.

Equations

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

def MIPRE.TM.CookLevin.Desc.emitStepF (e : ℕ) (C : CandF) : SAT.Fml

EmitStep.

Equations

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

def MIPRE.TM.CookLevin.Desc.emitMonoF (e : ℕ) (C : CandF) : SAT.Fml

EmitMono.

Equations

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

def MIPRE.TM.CookLevin.Desc.emitOneF (e : ℕ) (C : CandF) : SAT.Fml

EmitOne.

Equations

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

def MIPRE.TM.CookLevin.Desc.emitOnceF (e : ℕ) (C : CandF) : SAT.Fml

EmitOnce.

Equations

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

def MIPRE.TM.CookLevin.Desc.emitBadF (e : ℕ) (C : CandF) : SAT.Fml

EmitBad.

Equations

• MIPRE.TM.CookLevin.Desc.emitBadF e C = MIPRE.SAT.Fml.andList [MIPRE.TM.CookLevin.Desc.unitEmitBadF e C, MIPRE.TM.CookLevin.Desc.sameSignsF C, C.σ₁.not]

def MIPRE.TM.CookLevin.Desc.emitPredF (e : ℕ) (C : CandF) : SAT.Fml

EmitPred.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.finalStateF (e : ℕ) (C : CandF) : SAT.Fml

FinalState.

Equations

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

def MIPRE.TM.CookLevin.Desc.finalEmittedF (e : ℕ) (C : CandF) : SAT.Fml

FinalEmitted.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.finalPredF (e : ℕ) (C : CandF) : SAT.Fml

FinalPred.

Equations

• MIPRE.TM.CookLevin.Desc.finalPredF e C = (MIPRE.TM.CookLevin.Desc.finalStateF e C).or (MIPRE.TM.CookLevin.Desc.finalEmittedF e C)

theorem MIPRE.TM.CookLevin.Desc.eval_bdryCellF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (bdryCellF e C) = true ↔ BdryCell e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_bdryHeadF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (bdryHeadF e C) = true ↔ BdryHead e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_bdryPredF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (bdryPredF e C) = true ↔ BdryPred e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitZeroF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitZeroF e C) = true ↔ EmitZero e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitStepF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitStepF e C) = true ↔ EmitStep e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitMonoF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitMonoF e C) = true ↔ EmitMono e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitOneF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitOneF e C) = true ↔ EmitOne e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitOnceF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitOnceF e C) = true ↔ EmitOnce e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitBadF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitBadF e C) = true ↔ EmitBad e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_emitPredF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (emitPredF e C) = true ↔ EmitPred e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_finalStateF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (finalStateF e C) = true ↔ FinalState e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_finalEmittedF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (finalEmittedF e C) = true ↔ FinalEmitted e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_finalPredF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (finalPredF e C) = true ↔ FinalPred e (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.bdryCellF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.bdryCellF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.bdryHeadF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.bdryHeadF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.bdryPredF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.bdryPredF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitZeroF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitZeroF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitStepF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitStepF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitMonoF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitMonoF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitOneF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitOneF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitOnceF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitOnceF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitBadF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitBadF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.emitPredF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.emitPredF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.finalStateF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.finalStateF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.finalEmittedF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.finalEmittedF e C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.finalPredF (e : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.finalPredF e C)

The five explicit families

noncomputable def MIPRE.TM.CookLevin.Desc.mainF (e : ℕ) (tabs : List (ℕ × SAT.Fml)) (frees : List ℕ) (C : CandF) : SAT.Fml

MainPred.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.eval_mainF (e G : ℕ) {fixed : Fin 7 → Option (List Interp.Sym)} {tabs : List (ℕ × SAT.Fml)} {frees : List ℕ} {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (ht : TapeSpec e C.A₁ fixed tabs) (hf : FreeSpec fixed frees) : SAT.Fml.eval x (mainF e tabs frees C) = true ↔ MainPred e fixed (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.mainF (e : ℕ) {n : ℕ} (tabs : List (ℕ × SAT.Fml)) (htabs : ∀ jv ∈ tabs, SAT.Fml.InputsLt n jv.2) (frees : List ℕ) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.mainF e tabs frees C)

The window family

The templates of the check circuit enter the formula as data: a window variable is a descriptor (WDesc: a one-hot kind, and the tape, offset, value and state as bit strings), a literal spec an LDesc, so that the describer program builds the window formula by a fold over a constant list of descriptors, never inspecting a WinVar or a Gate.

def MIPRE.TM.CookLevin.Desc.oneHot (n k : ℕ) : List Bool

The one-hot vector of length n with its k-th entry set.

Equations

• MIPRE.TM.CookLevin.Desc.oneHot n k = List.map (fun (i : ℕ) => decide (i = k)) (List.range n)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_oneHot (n k : ℕ) : (oneHot n k).length = n

theorem MIPRE.TM.CookLevin.Desc.getElem_oneHot (n k i : ℕ) (h : i < (oneHot n k).length) : (oneHot n k)[i] = decide (i = k)

def MIPRE.TM.CookLevin.Desc.selectF (hot : List Bool) (fs : List SAT.Fml) : SAT.Fml

Select by a one-hot vector: ⋁ᵢ bᵢ ∧ fᵢ.

Equations

• MIPRE.TM.CookLevin.Desc.selectF hot fs = MIPRE.SAT.Fml.orList (List.zipWith (fun (b : Bool) (f : MIPRE.SAT.Fml) => (MIPRE.SAT.Fml.const b).and f) hot fs)

theorem MIPRE.TM.CookLevin.Desc.eval_selectF (hot : List Bool) (fs : List SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (selectF hot fs) = true ↔ ∃ (i : ℕ) (h : i < (List.zipWith (fun (b : Bool) (f : SAT.Fml) => (SAT.Fml.const b).and f) hot fs).length), hot[i] = true ∧ SAT.Fml.eval x fs[i] = true

theorem MIPRE.TM.CookLevin.Desc.eval_selectF_oneHot (n k : ℕ) (fs : List SAT.Fml) (hl : fs.length = n) (hk : k < n) (x : ℕ → Bool) : SAT.Fml.eval x (selectF (oneHot n k) fs) = true ↔ SAT.Fml.eval x fs[k] = true

theorem MIPRE.TM.CookLevin.Desc.eval_selectF_none (n : ℕ) (fs : List SAT.Fml) (x : ℕ → Bool) : SAT.Fml.eval x (selectF (List.replicate n false) fs) = false

theorem MIPRE.TM.CookLevin.Desc.InputsLt.selectF {n : ℕ} (hot : List Bool) {fs : List SAT.Fml} (hfs : ∀ f ∈ fs, SAT.Fml.InputsLt n f) : SAT.Fml.InputsLt n (Desc.selectF hot fs)

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

A window variable as data: the kind (one-hot over cellPre, headPre, cellPost, headPost, statePre, statePost, emitOne, emitBad), the tape (4 bits, and one-hot over the 13 tapes), the offset (3 bits), the value (3 bits), the state (Qb bits).

• kind : List Bool
• d : Cost.BitStr
• dHot : List Bool
• δ : Cost.BitStr
• v : Cost.BitStr
• q : Cost.BitStr

noncomputable def MIPRE.TM.CookLevin.Desc.wvDesc : WinVar 7 6 Interp.Sym Interp.Ctl → WDesc

The descriptor of a window variable.

Equations

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

def MIPRE.TM.CookLevin.Desc.badDesc : WDesc

The descriptor of nothing: no kind.

Equations

• MIPRE.TM.CookLevin.Desc.badDesc = { kind := List.replicate 8 false, d := [], dHot := [], δ := [], v := [], q := [] }

def MIPRE.TM.CookLevin.Desc.posF (e : ℕ) (Fa A : FieldsF) (dHot : List Bool) (δ : Cost.BitStr) : SAT.Fml

p = js_d + δ, the tape d given one-hot.

Equations

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

def MIPRE.TM.CookLevin.Desc.winMatchN (e : ℕ) (Fa A : FieldsF) (w : WDesc) : SAT.Fml

WinMatch, on a descriptor.

Equations

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

def MIPRE.TM.CookLevin.Desc.auxMatchN (e G : ℕ) (Fa A : FieldsF) (u : Cost.BitStr) : SAT.Fml

SpecMatch for a gate spec, with the gate index as bits.

Equations

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

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

A literal spec as data.

• isAux : Bool
• u : Cost.BitStr
• w : WDesc

def MIPRE.TM.CookLevin.Desc.specMatchN (e G : ℕ) (Fa A : FieldsF) (l : LDesc) : SAT.Fml

SpecMatch, on a descriptor.

Equations

• MIPRE.TM.CookLevin.Desc.specMatchN e G Fa A l = (MIPRE.SAT.Fml.const l.isAux).mux (MIPRE.TM.CookLevin.Desc.auxMatchN e G Fa A l.u) (MIPRE.TM.CookLevin.Desc.winMatchN e Fa A l.w)

noncomputable def MIPRE.TM.CookLevin.Desc.wvDescs : List WDesc

The descriptors of the window variables, in the canonical order.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.LitSpec.toN (G : ℕ) : LitSpec → LDesc

The descriptor of a spec.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.LitSpec.toN G (MIPRE.TM.CookLevin.Desc.LitSpec.win n) = { isAux := false, u := [], w := MIPRE.TM.CookLevin.Desc.wvDescs.getD n MIPRE.TM.CookLevin.Desc.badDesc }

@[reducible, inline]

abbrev MIPRE.TM.CookLevin.Desc.NTpl : Type

A template as data.

Equations

• MIPRE.TM.CookLevin.Desc.NTpl = ((MIPRE.TM.CookLevin.Desc.LDesc × Bool) × (MIPRE.TM.CookLevin.Desc.LDesc × Bool) × MIPRE.TM.CookLevin.Desc.LDesc × Bool)

noncomputable def MIPRE.TM.CookLevin.Desc.Tpl.toN (G : ℕ) (tp : Tpl) : NTpl

The descriptor of a template.

Equations

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

def MIPRE.TM.CookLevin.Desc.tplN (e G : ℕ) (tp : NTpl) (C : CandF) : SAT.Fml

TplMatch, on a descriptor.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.tplsFrom (G : ℕ) : ℕ → List SAT.Gate → List (List NTpl)

The template descriptors of the gates gs, numbered from g₀.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.TM.CookLevin.Desc.tplsFrom G x✝ [] = []

noncomputable def MIPRE.TM.CookLevin.Desc.tplsOf (G : ℕ) (chk : SAT.Circuit) : List (List NTpl)

The template descriptors of the check circuit: the constant of the describer.

Equations

• MIPRE.TM.CookLevin.Desc.tplsOf G chk = MIPRE.TM.CookLevin.Desc.tplsFrom G 0 chk.gates

def MIPRE.TM.CookLevin.Desc.windowGatesN (e G : ℕ) (tpls : List (List NTpl)) (C : CandF) : SAT.Fml

WindowGates, on the descriptors tpls.

Equations

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

def MIPRE.TM.CookLevin.Desc.windowOutF (e G : ℕ) (C : CandF) : SAT.Fml

WindowOut.

Equations

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

def MIPRE.TM.CookLevin.Desc.windowN (e G : ℕ) (tpls : List (List NTpl)) (C : CandF) : SAT.Fml

WindowPred.

Equations

• MIPRE.TM.CookLevin.Desc.windowN e G tpls C = (MIPRE.TM.CookLevin.Desc.windowGatesN e G tpls C).or (MIPRE.TM.CookLevin.Desc.windowOutF e G C)

theorem MIPRE.TM.CookLevin.Desc.eval_posF (e G : ℕ) {Fa A : FieldsF} (hFa : FieldsF.Lengths e G Fa) (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (d : Tape 7 6) (δ : ℕ) (hδ : δ < 8) : SAT.Fml.eval x (posF e Fa A (oneHot 13 (tapeCode d)) (nbits 3 δ)) = true ↔ SAT.Fml.val A.p x = SAT.Fml.val (Fa.js ⟨tapeCode d, ⋯⟩) x + δ

theorem MIPRE.TM.CookLevin.Desc.eval_winMatchN (e G : ℕ) {Fa A : FieldsF} (hFa : FieldsF.Lengths e G Fa) (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (wv : WinVar 7 6 Interp.Sym Interp.Ctl) : SAT.Fml.eval x (winMatchN e Fa A (wvDesc wv)) = true ↔ WinMatch e (evalFields Fa x) wv (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_winMatchN_bad (e : ℕ) {Fa A : FieldsF} (x : ℕ → Bool) : SAT.Fml.eval x (winMatchN e Fa A badDesc) = false

theorem MIPRE.TM.CookLevin.Desc.eval_auxMatchN (e G : ℕ) {Fa A : FieldsF} (hFa : FieldsF.Lengths e G Fa) (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (u : ℕ) (hu : u < G) : SAT.Fml.eval x (auxMatchN e G Fa A (nbits (Gb G) u)) = true ↔ SpecMatch e G (evalFields Fa x) (LitSpec.aux u) (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_specMatchN_aux (e G : ℕ) {Fa A : FieldsF} (hFa : FieldsF.Lengths e G Fa) (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (u : ℕ) (hu : u < G) : SAT.Fml.eval x (specMatchN e G Fa A (LitSpec.toN G (LitSpec.aux u))) = true ↔ SpecMatch e G (evalFields Fa x) (LitSpec.aux u) (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.wvDescs_getD (n : ℕ) : wvDescs.getD n badDesc = if h : n < winCard 7 6 Interp.Sym Interp.Ctl then wvDesc ((Fintype.equivFin (WinVar 7 6 Interp.Sym Interp.Ctl)).symm ⟨n, h⟩) else badDesc

theorem MIPRE.TM.CookLevin.Desc.eval_specMatchN_win (e G : ℕ) {Fa A : FieldsF} (hFa : FieldsF.Lengths e G Fa) (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (n : ℕ) : SAT.Fml.eval x (specMatchN e G Fa A (LitSpec.toN G (LitSpec.win n))) = true ↔ SpecMatch e G (evalFields Fa x) (LitSpec.win n) (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_specMatchN (e G : ℕ) {Fa A : FieldsF} (hFa : FieldsF.Lengths e G Fa) (hA : FieldsF.Lengths e G A) (x : ℕ → Bool) (sp : LitSpec) (hsp : ∀ (u : ℕ), sp = LitSpec.aux u → u < G) : SAT.Fml.eval x (specMatchN e G Fa A (LitSpec.toN G sp)) = true ↔ SpecMatch e G (evalFields Fa x) sp (evalFields A x)

theorem MIPRE.TM.CookLevin.Desc.eval_tplN (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (tp : Tpl) (hsp : ∀ (sp : LitSpec), sp = tp.1.1 ∨ sp = tp.2.1.1 ∨ sp = tp.2.2.1 → ∀ (u : ℕ), sp = LitSpec.aux u → u < G) : SAT.Fml.eval x (tplN e G (Tpl.toN G tp) C) = true ↔ TplMatch e G tp (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.mem_tplsFrom (G : ℕ) (gs : List SAT.Gate) (g₀ : ℕ) (l : List NTpl) : l ∈ tplsFrom G g₀ gs ↔ ∃ (i : ℕ) (h : i < gs.length), l = List.map (Tpl.toN G) (gateTemplates (g₀ + i) gs[i])

theorem MIPRE.TM.CookLevin.Desc.eval_windowGatesN (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (chk : SAT.Circuit) (hG : G = chk.gates.length) (hC' : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) : SAT.Fml.eval x (windowGatesN e G (tplsOf G chk) C) = true ↔ WindowGates e G chk (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_windowOutF (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) : SAT.Fml.eval x (windowOutF e G C) = true ↔ WindowOut e G (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.eval_windowN (e G : ℕ) {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (chk : SAT.Circuit) (hG : G = chk.gates.length) (hC' : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) : SAT.Fml.eval x (windowN e G (tplsOf G chk) C) = true ↔ WindowPred e G chk (evalCand C x)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.posF (e : ℕ) {n : ℕ} {Fa A : FieldsF} (hFa : FieldsF.InputsLt n Fa) (hA : FieldsF.InputsLt n A) (dHot : List Bool) (δ : Cost.BitStr) : SAT.Fml.InputsLt n (Desc.posF e Fa A dHot δ)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.winMatchN (e : ℕ) {n : ℕ} {Fa A : FieldsF} (hFa : FieldsF.InputsLt n Fa) (hA : FieldsF.InputsLt n A) (w : WDesc) : SAT.Fml.InputsLt n (Desc.winMatchN e Fa A w)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.auxMatchN (e G : ℕ) {n : ℕ} {Fa A : FieldsF} (hFa : FieldsF.InputsLt n Fa) (hA : FieldsF.InputsLt n A) (u : Cost.BitStr) : SAT.Fml.InputsLt n (Desc.auxMatchN e G Fa A u)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.specMatchN (e G : ℕ) {n : ℕ} {Fa A : FieldsF} (hFa : FieldsF.InputsLt n Fa) (hA : FieldsF.InputsLt n A) (l : LDesc) : SAT.Fml.InputsLt n (Desc.specMatchN e G Fa A l)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.tplN (e G : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) (tp : NTpl) : SAT.Fml.InputsLt n (Desc.tplN e G tp C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.windowGatesN (e G : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) (tpls : List (List NTpl)) : SAT.Fml.InputsLt n (Desc.windowGatesN e G tpls C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.windowOutF (e G : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.windowOutF e G C)

theorem MIPRE.TM.CookLevin.Desc.InputsLt.windowN (e G : ℕ) {n : ℕ} {C : CandF} (hC : CandF.InputsLt n C) (tpls : List (List NTpl)) : SAT.Fml.InputsLt n (Desc.windowN e G tpls C)

The whole tableau

noncomputable def MIPRE.TM.CookLevin.Desc.tableauF (e G : ℕ) (tabs : List (ℕ × SAT.Fml)) (frees : List ℕ) (tpls : List (List NTpl)) (C : CandF) : SAT.Fml

The formula of the tableau on a candidate: the five explicit families or the window family.

Equations

• MIPRE.TM.CookLevin.Desc.tableauF e G tabs frees tpls C = (MIPRE.TM.CookLevin.Desc.mainF e tabs frees C).or (MIPRE.TM.CookLevin.Desc.windowN e G tpls C)

theorem MIPRE.TM.CookLevin.Desc.eval_tableauF (e G : ℕ) {fixed : Fin 7 → Option (List Interp.Sym)} {tabs : List (ℕ × SAT.Fml)} {frees : List ℕ} {C : CandF} (hC : CandF.Lengths e G C) (x : ℕ → Bool) (ht : TapeSpec e C.A₁ fixed tabs) (hf : FreeSpec fixed frees) (chk : SAT.Circuit) (hG : G = chk.gates.length) (hC' : chk.RefsLt) (hin : chk.InputsLt) (hinp : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl) (hne : chk.gates ≠ []) : SAT.Fml.eval x (tableauF e G tabs frees (tplsOf G chk) C) = true ↔ ∃ cl ∈ tableau Interp.U Interp.Sym.zero Interp.Sym.one (Sof e) fixed chk, Cand.Dec e chk.gates.length (evalCand C x) cl

The tableau formula is exact: it accepts a candidate iff the candidate decodes to a clause of tableau U 0 1 S fixed chk.

theorem MIPRE.TM.CookLevin.Desc.InputsLt.tableauF (e G : ℕ) {n : ℕ} (tabs : List (ℕ × SAT.Fml)) (htabs : ∀ jv ∈ tabs, SAT.Fml.InputsLt n jv.2) (frees : List ℕ) (tpls : List (List NTpl)) {C : CandF} (hC : CandF.InputsLt n C) : SAT.Fml.InputsLt n (Desc.tableauF e G tabs frees tpls C)