The family formulas as programs

Every formula of FamilyFml.lean as a program reading a shared input: a candidate of readers (CandR), the width e in unary, and the data the explicit families need. The statement of each is progR … i = familyF (eu i).length Gc … (C.ev i), and its proof is simp over the constants of the layout — the shape of the formula matches definitionally, because CandR.ev is a structure literal of the programs' own values.

The constants are the only content: Sof e = 2 ^ e and 2 * Sof e + k = 2 ^ (e + 1) + k come from pow2P and incN, and numR turns a number and a width into the bit string of the field constant (planning/succinct-cook-levin.md, S3).

Conjunctions and disjunctions of readers

noncomputable def MIPRE.TM.CookLevin.Desc.andR {ι : Type u_1} [Cost.SizedEncoding ι] (fs : List (Cost.PolyTimeFun ι SAT.Fml)) : Cost.PolyTimeFun ι SAT.Fml

andList of readers.

Equations

• MIPRE.TM.CookLevin.Desc.andR fs = MIPRE.SAT.andListP.ap₁ (MIPRE.Cost.PolyTimeFun.listOf fs)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.andR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs : List (Cost.PolyTimeFun ι SAT.Fml)) (i : ι) : (andR fs).toFun i = SAT.Fml.andList (List.map (fun (f : Cost.PolyTimeFun ι SAT.Fml) => f.toFun i) fs)

noncomputable def MIPRE.TM.CookLevin.Desc.orR {ι : Type u_1} [Cost.SizedEncoding ι] (fs : List (Cost.PolyTimeFun ι SAT.Fml)) : Cost.PolyTimeFun ι SAT.Fml

orList of readers.

Equations

• MIPRE.TM.CookLevin.Desc.orR fs = MIPRE.SAT.orListP.ap₁ (MIPRE.Cost.PolyTimeFun.listOf fs)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.orR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs : List (Cost.PolyTimeFun ι SAT.Fml)) (i : ι) : (orR fs).toFun i = SAT.Fml.orList (List.map (fun (f : Cost.PolyTimeFun ι SAT.Fml) => f.toFun i) fs)

noncomputable def MIPRE.TM.CookLevin.Desc.andTwo {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

and of two readers.

Equations

• MIPRE.TM.CookLevin.Desc.andTwo f g = MIPRE.SAT.Fml.andF.ap₂ f g

@[simp]

theorem MIPRE.TM.CookLevin.Desc.andTwo_apply {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (andTwo f g).toFun i = (f.toFun i).and (g.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.orTwo {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

or of two readers.

Equations

• MIPRE.TM.CookLevin.Desc.orTwo f g = MIPRE.SAT.Fml.orF.ap₂ f g

@[simp]

theorem MIPRE.TM.CookLevin.Desc.orTwo_apply {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (orTwo f g).toFun i = (f.toFun i).or (g.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.notR {ι : Type u_1} [Cost.SizedEncoding ι] (f : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

not of a reader.

Equations

• MIPRE.TM.CookLevin.Desc.notR f = MIPRE.SAT.Fml.notF.ap₁ f

@[simp]

theorem MIPRE.TM.CookLevin.Desc.notR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (f : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (notR f).toFun i = (f.toFun i).not

noncomputable def MIPRE.TM.CookLevin.Desc.xnorR {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

xnor of two readers.

Equations

• MIPRE.TM.CookLevin.Desc.xnorR f g = MIPRE.SAT.xnorP.ap₂ f g

@[simp]

theorem MIPRE.TM.CookLevin.Desc.xnorR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (xnorR f g).toFun i = (f.toFun i).xnor (g.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.muxR {ι : Type u_1} [Cost.SizedEncoding ι] (s f g : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

mux of three readers.

Equations

• MIPRE.TM.CookLevin.Desc.muxR s f g = MIPRE.SAT.muxP.ap₃ s f g

@[simp]

theorem MIPRE.TM.CookLevin.Desc.muxR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (s f g : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (muxR s f g).toFun i = (s.toFun i).mux (f.toFun i) (g.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.eqC {ι : Type u_1} [Cost.SizedEncoding ι] (fs : Cost.PolyTimeFun ι (List SAT.Fml)) (c : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι SAT.Fml

eqConst.

Equations

• MIPRE.TM.CookLevin.Desc.eqC fs c = MIPRE.SAT.eqConstP.ap₂ fs c

@[simp]

theorem MIPRE.TM.CookLevin.Desc.eqC_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs : Cost.PolyTimeFun ι (List SAT.Fml)) (c : Cost.PolyTimeFun ι Cost.BitStr) (i : ι) : (eqC fs c).toFun i = SAT.Fml.eqConst (fs.toFun i) (c.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.ltC {ι : Type u_1} [Cost.SizedEncoding ι] (fs : Cost.PolyTimeFun ι (List SAT.Fml)) (c : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι SAT.Fml

ltConst.

Equations

• MIPRE.TM.CookLevin.Desc.ltC fs c = MIPRE.SAT.ltConstP.ap₂ fs c

@[simp]

theorem MIPRE.TM.CookLevin.Desc.ltC_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs : Cost.PolyTimeFun ι (List SAT.Fml)) (c : Cost.PolyTimeFun ι Cost.BitStr) (i : ι) : (ltC fs c).toFun i = SAT.Fml.ltConst (fs.toFun i) (c.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.eqF {ι : Type u_1} [Cost.SizedEncoding ι] (fs gs : Cost.PolyTimeFun ι (List SAT.Fml)) : Cost.PolyTimeFun ι SAT.Fml

eqFields.

Equations

• MIPRE.TM.CookLevin.Desc.eqF fs gs = MIPRE.SAT.eqFieldsP.ap₂ fs gs

@[simp]

theorem MIPRE.TM.CookLevin.Desc.eqF_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs gs : Cost.PolyTimeFun ι (List SAT.Fml)) (i : ι) : (eqF fs gs).toFun i = SAT.Fml.eqFields (fs.toFun i) (gs.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.ltF {ι : Type u_1} [Cost.SizedEncoding ι] (fs gs : Cost.PolyTimeFun ι (List SAT.Fml)) : Cost.PolyTimeFun ι SAT.Fml

ltFields.

Equations

• MIPRE.TM.CookLevin.Desc.ltF fs gs = MIPRE.SAT.ltFieldsP.ap₂ fs gs

@[simp]

theorem MIPRE.TM.CookLevin.Desc.ltF_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs gs : Cost.PolyTimeFun ι (List SAT.Fml)) (i : ι) : (ltF fs gs).toFun i = SAT.Fml.ltFields (fs.toFun i) (gs.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.addRelR {ι : Type u_1} [Cost.SizedEncoding ι] (fs gs : Cost.PolyTimeFun ι (List SAT.Fml)) (c : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι SAT.Fml

addConstRel.

Equations

• MIPRE.TM.CookLevin.Desc.addRelR fs gs c = MIPRE.SAT.addConstRelP.comp ((fs.pair gs).pair c)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.addRelR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (fs gs : Cost.PolyTimeFun ι (List SAT.Fml)) (c : Cost.PolyTimeFun ι Cost.BitStr) (i : ι) : (addRelR fs gs c).toFun i = SAT.Fml.addConstRel (fs.toFun i) (gs.toFun i) (c.toFun i)

The constants of the layout

noncomputable def MIPRE.TM.CookLevin.Desc.numR {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (kR : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι Cost.BitStr

A field constant, from a width in unary and the number.

Equations

• MIPRE.TM.CookLevin.Desc.numR w kR = MIPRE.TM.CookLevin.Desc.nbitsR w (MIPRE.Cost.PolyTimeFun.natBits.ap₁ kR)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.numR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (kR : Cost.PolyTimeFun ι ℕ) (i : ι) : (numR w kR).toFun i = nbits (List.length (w.toFun i)) (kR.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.numC {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) : Cost.PolyTimeFun ι Cost.BitStr

A field constant with a fixed value.

Equations

• MIPRE.TM.CookLevin.Desc.numC w k = MIPRE.TM.CookLevin.Desc.nbitsR w (MIPRE.TM.CookLevin.Desc.bitsR k)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.numC_apply {ι : Type u_1} [Cost.SizedEncoding ι] (w : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (numC w k).toFun i = nbits (List.length (w.toFun i)) k

noncomputable def MIPRE.TM.CookLevin.Desc.SofR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι ℕ

Sof e.

Equations

• MIPRE.TM.CookLevin.Desc.SofR eu = MIPRE.TM.CookLevin.Desc.pow2P.ap₁ eu

@[simp]

theorem MIPRE.TM.CookLevin.Desc.SofR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (SofR eu).toFun i = Sof (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.twoSR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι ℕ

2 * Sof e, as Sof (e + 1).

Equations

• MIPRE.TM.CookLevin.Desc.twoSR eu = MIPRE.TM.CookLevin.Desc.pow2P.ap₁ (MIPRE.TM.CookLevin.Desc.addU.ap₂ eu (MIPRE.Cost.PolyTimeFun.const (MIPRE.Cost.unary 1)))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.twoSR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (twoSR eu).toFun i = 2 * Sof (List.length (eu.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.SofAddR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) : Cost.PolyTimeFun ι ℕ

Sof e + k.

Equations

• MIPRE.TM.CookLevin.Desc.SofAddR eu k = (MIPRE.TM.CookLevin.Desc.incN k).ap₁ (MIPRE.TM.CookLevin.Desc.SofR eu)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.SofAddR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (SofAddR eu k).toFun i = Sof (List.length (eu.toFun i)) + k

noncomputable def MIPRE.TM.CookLevin.Desc.twoSAddR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) : Cost.PolyTimeFun ι ℕ

2 * Sof e + k.

Equations

• MIPRE.TM.CookLevin.Desc.twoSAddR eu k = (MIPRE.TM.CookLevin.Desc.incN k).ap₁ (MIPRE.TM.CookLevin.Desc.twoSR eu)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.twoSAddR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (twoSAddR eu k).toFun i = 2 * Sof (List.length (eu.toFun i)) + k

The kind predicates

noncomputable def MIPRE.TM.CookLevin.Desc.numEqR {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

numEqF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.numEqR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) (i : ι) : (numEqR A B).toFun i = numEqF (A.ev i) (B.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isCellR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isCellF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isCellR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isCellR eu A).toFun i = isCellF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isHeadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isHeadF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isHeadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isHeadR eu A).toFun i = isHeadF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isStateR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isStateF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isStateR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isStateR eu A).toFun i = isStateF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isEmitOneR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isEmitOneF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isEmitOneR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isEmitOneR eu A).toFun i = isEmitOneF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isEmitBadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isEmitBadF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isEmitBadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isEmitBadR eu A).toFun i = isEmitBadF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isEmittedR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isEmittedF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isEmittedR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isEmittedR eu A).toFun i = isEmittedF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.isAuxR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

isAuxF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.isAuxR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (isAuxR eu A).toFun i = isAuxF (List.length (eu.toFun i)) Gc (A.ev i)

The same-variable formulas

noncomputable def MIPRE.TM.CookLevin.Desc.cellEqR {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

cellEqF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.cellEqR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) (i : ι) : (cellEqR A B).toFun i = cellEqF (A.ev i) (B.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.headEqR {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

headEqF.

Equations

• MIPRE.TM.CookLevin.Desc.headEqR A B = MIPRE.TM.CookLevin.Desc.andR [MIPRE.TM.CookLevin.Desc.eqF A.t B.t, MIPRE.TM.CookLevin.Desc.eqF A.d B.d, MIPRE.TM.CookLevin.Desc.eqF A.p B.p]

@[simp]

theorem MIPRE.TM.CookLevin.Desc.headEqR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) (i : ι) : (headEqR A B).toFun i = headEqF (A.ev i) (B.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.stateEqR {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

stateEqF.

Equations

• MIPRE.TM.CookLevin.Desc.stateEqR A B = MIPRE.TM.CookLevin.Desc.andR [MIPRE.TM.CookLevin.Desc.eqF A.t B.t, MIPRE.TM.CookLevin.Desc.eqF A.q B.q]

@[simp]

theorem MIPRE.TM.CookLevin.Desc.stateEqR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) (i : ι) : (stateEqR A B).toFun i = stateEqF (A.ev i) (B.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.auxEqR {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

auxEqF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.auxEqR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) (i : ι) : (auxEqR A B).toFun i = auxEqF (A.ev i) (B.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.samePosR {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

samePosF.

Equations

• MIPRE.TM.CookLevin.Desc.samePosR A B = MIPRE.TM.CookLevin.Desc.andR [MIPRE.TM.CookLevin.Desc.eqF A.t B.t, MIPRE.TM.CookLevin.Desc.eqF A.d B.d, MIPRE.TM.CookLevin.Desc.eqF A.p B.p]

@[simp]

theorem MIPRE.TM.CookLevin.Desc.samePosR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A B : FieldsR ι) (i : ι) : (samePosR A B).toFun i = samePosF (A.ev i) (B.ev i)

Mapping over a list read off the input

noncomputable def MIPRE.TM.CookLevin.Desc.mapR {ι : Type u_1} [Cost.SizedEncoding ι] {α : Type u_2} {γ : Type u_3} [Cost.SizedEncoding α] [Cost.SizedEncoding γ] (F : Cost.PolyTimeFun (α × ι) γ) (l : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι (List γ)

Mapping a reader of pairs over a list read off the input.

Equations

• MIPRE.TM.CookLevin.Desc.mapR F l = F.mapWith.comp (l.pair (MIPRE.Cost.PolyTimeFun.id ι))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.mapR_apply {ι : Type u_1} [Cost.SizedEncoding ι] {α : Type u_2} {γ : Type u_3} [Cost.SizedEncoding α] [Cost.SizedEncoding γ] (F : Cost.PolyTimeFun (α × ι) γ) (l : Cost.PolyTimeFun ι (List α)) (i : ι) : (mapR F l).toFun i = List.map (fun (a : α) => F.toFun (a, i)) (l.toFun i)

Unit clauses and signs

noncomputable def MIPRE.TM.CookLevin.Desc.unitCellR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

unitCellF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unitCellR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (unitCellR eu C).toFun i = unitCellF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.unitHeadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

unitHeadF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unitHeadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (unitHeadR eu C).toFun i = unitHeadF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.unitStateR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

unitStateF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unitStateR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (unitStateR eu C).toFun i = unitStateF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.unitEmitBadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

unitEmitBadF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unitEmitBadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (unitEmitBadR eu C).toFun i = unitEmitBadF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.unitEmittedR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

unitEmittedF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unitEmittedR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (unitEmittedR eu C).toFun i = unitEmittedF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.unitAuxR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

unitAuxF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unitAuxR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (unitAuxR eu C).toFun i = unitAuxF (List.length (eu.toFun i)) Gc (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.sameSignsR {ι : Type u_1} [Cost.SizedEncoding ι] (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

sameSignsF.

Equations

• MIPRE.TM.CookLevin.Desc.sameSignsR C = MIPRE.TM.CookLevin.Desc.andTwo (MIPRE.TM.CookLevin.Desc.xnorR C.σ₂ C.σ₁) (MIPRE.TM.CookLevin.Desc.xnorR C.σ₃ C.σ₁)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.sameSignsR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (C : CandR ι) (i : ι) : (sameSignsR C).toFun i = sameSignsF (C.ev i)

Positions and values

noncomputable def MIPRE.TM.CookLevin.Desc.bdryR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

bdryF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.bdryR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (bdryR eu A).toFun i = bdryF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.startCellR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

startCellF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.startCellR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (startCellR eu A).toFun i = startCellF (List.length (eu.toFun i)) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.workValR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

workValF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.workValR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (workValR eu A).toFun i = workValF (List.length (eu.toFun i)) (A.ev i)

theorem MIPRE.TM.CookLevin.Desc.lookupList_eq (e : ℕ) (A : FieldsF) (k : ℕ) (cs : List ℕ) : lookupList e A k cs = List.map (fun (p : ℕ × ℕ) => (SAT.Fml.eqConst A.p (nbits (W e) p.2)).and (SAT.Fml.eqConst A.v (nbits 3 p.1))) (cs.zip (List.range' k cs.length))

The lookup table, written as a map over the codes paired with their positions.

noncomputable def MIPRE.TM.CookLevin.Desc.lookupR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (codes : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι (List SAT.Fml)

lookupList, from cell 3.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.lookupR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (codes : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (lookupR eu A codes).toFun i = lookupList (List.length (eu.toFun i)) (A.ev i) 3 (codes.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.cellValR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (codes : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

cellValF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.cellValR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (codes : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (cellValR eu A codes).toFun i = cellValF (List.length (eu.toFun i)) (A.ev i) (codes.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.unaryValR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (TR : Cost.PolyTimeFun ι ℕ) : Cost.PolyTimeFun ι SAT.Fml

unaryValF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.unaryValR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (TR : Cost.PolyTimeFun ι ℕ) (i : ι) : (unaryValR eu A TR).toFun i = unaryValF (List.length (eu.toFun i)) (TR.toFun i) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeTapeR {ι : Type u_1} [Cost.SizedEncoding ι] (A : FieldsR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeTapeF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeTapeR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (A : FieldsR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeTapeR A frees).toFun i = freeTapeF (frees.toFun i) (A.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.tZeroR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) : Cost.PolyTimeFun ι SAT.Fml

tZeroF.

Equations

• MIPRE.TM.CookLevin.Desc.tZeroR eu A = MIPRE.TM.CookLevin.Desc.eqC A.t (MIPRE.TM.CookLevin.Desc.numC (MIPRE.TM.CookLevin.Desc.WU eu) 0)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.tZeroR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (A : FieldsR ι) (i : ι) : (tZeroR eu A).toFun i = tZeroF (List.length (eu.toFun i)) (A.ev i)

The start family

noncomputable def MIPRE.TM.CookLevin.Desc.startHeadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

startHeadF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.startHeadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (startHeadR eu C).toFun i = startHeadF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.startStateR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

startStateF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.startStateR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (startStateR eu C).toFun i = startStateF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.startFixedR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) : Cost.PolyTimeFun ι SAT.Fml

startFixedF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.startFixedR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (i : ι) : (startFixedR eu C tabs).toFun i = startFixedF (List.length (eu.toFun i)) (tabs.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.startWorkR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

startWorkF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.startWorkR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (startWorkR eu C).toFun i = startWorkF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.startR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) : Cost.PolyTimeFun ι SAT.Fml

startF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.startR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (i : ι) : (startR eu C tabs).toFun i = startF (List.length (eu.toFun i)) (tabs.toFun i) (C.ev i)

The free family

noncomputable def MIPRE.TM.CookLevin.Desc.freeBdryR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeBdryF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeBdryR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeBdryR eu C frees).toFun i = freeBdryF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeOtherR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeOtherF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeOtherR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeOtherR eu C frees).toFun i = freeOtherF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeTwoR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeTwoF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeTwoR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeTwoR eu C frees).toFun i = freeTwoF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeOneOfR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeOneOfF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeOneOfR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeOneOfR eu C frees).toFun i = freeOneOfF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeNandR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeNandF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeNandR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeNandR eu C frees).toFun i = freeNandF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeBlankR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeBlankF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeBlankR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeBlankR eu C frees).toFun i = freeBlankF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.freeR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

freeF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.freeR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (freeR eu C frees).toFun i = freeF (List.length (eu.toFun i)) (frees.toFun i) (C.ev i)

The boundary, emission and final families

noncomputable def MIPRE.TM.CookLevin.Desc.bdryCellR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

bdryCellF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.bdryCellR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (bdryCellR eu C).toFun i = bdryCellF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.bdryHeadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

bdryHeadF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.bdryHeadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (bdryHeadR eu C).toFun i = bdryHeadF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.bdryPredR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

bdryPredF.

Equations

• MIPRE.TM.CookLevin.Desc.bdryPredR eu C = MIPRE.TM.CookLevin.Desc.orTwo (MIPRE.TM.CookLevin.Desc.bdryCellR eu C) (MIPRE.TM.CookLevin.Desc.bdryHeadR eu C)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.bdryPredR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (bdryPredR eu C).toFun i = bdryPredF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitZeroR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitZeroF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitZeroR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitZeroR eu C).toFun i = emitZeroF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitStepR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitStepF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitStepR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitStepR eu C).toFun i = emitStepF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitMonoR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitMonoF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitMonoR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitMonoR eu C).toFun i = emitMonoF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitOneR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitOneF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitOneR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitOneR eu C).toFun i = emitOneF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitOnceR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitOnceF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitOnceR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitOnceR eu C).toFun i = emitOnceF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitBadR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitBadF.

Equations

• MIPRE.TM.CookLevin.Desc.emitBadR eu C = MIPRE.TM.CookLevin.Desc.andR [MIPRE.TM.CookLevin.Desc.unitEmitBadR eu C, MIPRE.TM.CookLevin.Desc.sameSignsR C, MIPRE.TM.CookLevin.Desc.notR C.σ₁]

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitBadR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitBadR eu C).toFun i = emitBadF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.emitPredR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

emitPredF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.emitPredR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (emitPredR eu C).toFun i = emitPredF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.finalStateR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

finalStateF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.finalStateR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (finalStateR eu C).toFun i = finalStateF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.finalEmittedR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

finalEmittedF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.finalEmittedR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (finalEmittedR eu C).toFun i = finalEmittedF (List.length (eu.toFun i)) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.finalPredR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

finalPredF.

Equations

• MIPRE.TM.CookLevin.Desc.finalPredR eu C = MIPRE.TM.CookLevin.Desc.orTwo (MIPRE.TM.CookLevin.Desc.finalStateR eu C) (MIPRE.TM.CookLevin.Desc.finalEmittedR eu C)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.finalPredR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (finalPredR eu C).toFun i = finalPredF (List.length (eu.toFun i)) (C.ev i)

The five explicit families

noncomputable def MIPRE.TM.CookLevin.Desc.mainR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

mainF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.mainR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (mainR eu C tabs frees).toFun i = mainF (List.length (eu.toFun i)) (tabs.toFun i) (frees.toFun i) (C.ev i)

The window family

The templates of the check circuit are a constant of the describer — Gc is fixed — so the program maps over tplsOf Gc chk at the Lean level and the descriptors never have to be encoded: each becomes a const reader.

theorem MIPRE.TM.CookLevin.Desc.selectF_zipWith (hot : List Bool) (fs : List SAT.Fml) : List.zipWith (fun (b : Bool) (f : SAT.Fml) => (SAT.Fml.const b).and f) hot fs = List.map (fun (p : Bool × SAT.Fml) => (SAT.Fml.const p.1).and p.2) (hot.zip fs)

selectF, written as a map over the pairs.

theorem MIPRE.TM.CookLevin.Desc.selectF_eq (hot : List Bool) (fs : List SAT.Fml) : selectF hot fs = SAT.Fml.orList (List.map (fun (p : Bool × SAT.Fml) => (SAT.Fml.const p.1).and p.2) (hot.zip fs))

noncomputable def MIPRE.TM.CookLevin.Desc.selectR {ι : Type u_1} [Cost.SizedEncoding ι] (hot : Cost.PolyTimeFun ι (List Bool)) (fs : Cost.PolyTimeFun ι (List SAT.Fml)) : Cost.PolyTimeFun ι SAT.Fml

selectF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.selectR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (hot : Cost.PolyTimeFun ι (List Bool)) (fs : Cost.PolyTimeFun ι (List SAT.Fml)) (i : ι) : (selectR hot fs).toFun i = selectF (hot.toFun i) (fs.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.posR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (dHot : List Bool) (δ : Cost.BitStr) : Cost.PolyTimeFun ι SAT.Fml

posF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.posR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (dHot : List Bool) (δ : Cost.BitStr) (i : ι) : (posR eu Fa A dHot δ).toFun i = posF (List.length (eu.toFun i)) (Fa.ev i) (A.ev i) dHot δ

noncomputable def MIPRE.TM.CookLevin.Desc.winMatchR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (w : WDesc) : Cost.PolyTimeFun ι SAT.Fml

winMatchN.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.winMatchR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (w : WDesc) (i : ι) : (winMatchR eu Fa A w).toFun i = winMatchN (List.length (eu.toFun i)) (Fa.ev i) (A.ev i) w

noncomputable def MIPRE.TM.CookLevin.Desc.auxMatchR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (u : Cost.BitStr) : Cost.PolyTimeFun ι SAT.Fml

auxMatchN.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.auxMatchR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (u : Cost.BitStr) (i : ι) : (auxMatchR eu Fa A u).toFun i = auxMatchN (List.length (eu.toFun i)) Gc (Fa.ev i) (A.ev i) u

noncomputable def MIPRE.TM.CookLevin.Desc.specMatchR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (l : LDesc) : Cost.PolyTimeFun ι SAT.Fml

specMatchN.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.specMatchR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (Fa A : FieldsR ι) (l : LDesc) (i : ι) : (specMatchR eu Fa A l).toFun i = specMatchN (List.length (eu.toFun i)) Gc (Fa.ev i) (A.ev i) l

noncomputable def MIPRE.TM.CookLevin.Desc.tplR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tp : NTpl) : Cost.PolyTimeFun ι SAT.Fml

tplN.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.tplR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tp : NTpl) (i : ι) : (tplR eu C tp).toFun i = tplN (List.length (eu.toFun i)) Gc tp (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.windowGatesR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

windowGatesN, on the templates of the check circuit.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.windowGatesR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (windowGatesR eu C).toFun i = windowGatesN (List.length (eu.toFun i)) Gc (tplsOf Gc chk) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.windowOutR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

windowOutF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.windowOutR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (windowOutR eu C).toFun i = windowOutF (List.length (eu.toFun i)) Gc (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.windowR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

windowN.

Equations

• MIPRE.TM.CookLevin.Desc.windowR eu C = MIPRE.TM.CookLevin.Desc.orTwo (MIPRE.TM.CookLevin.Desc.windowGatesR eu C) (MIPRE.TM.CookLevin.Desc.windowOutR eu C)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.windowR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (i : ι) : (windowR eu C).toFun i = windowN (List.length (eu.toFun i)) Gc (tplsOf Gc chk) (C.ev i)

The whole tableau

noncomputable def MIPRE.TM.CookLevin.Desc.tableauR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

tableauF.

Equations

• MIPRE.TM.CookLevin.Desc.tableauR eu C tabs frees = MIPRE.TM.CookLevin.Desc.orTwo (MIPRE.TM.CookLevin.Desc.mainR eu C tabs frees) (MIPRE.TM.CookLevin.Desc.windowR eu C)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.tableauR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (tableauR eu C tabs frees).toFun i = tableauF (List.length (eu.toFun i)) Gc (tabs.toFun i) (frees.toFun i) (tplsOf Gc chk) (C.ev i)

The answer-end clauses

noncomputable def MIPRE.TM.CookLevin.Desc.ansEndR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (C : CandR ι) : Cost.PolyTimeFun ι SAT.Fml

ansEndF.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.ansEndR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (C : CandR ι) (i : ι) : (ansEndR eu TR C).toFun i = ansEndF (List.length (eu.toFun i)) (TR.toFun i) (C.ev i)

noncomputable def MIPRE.TM.CookLevin.Desc.tableauPlusR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (frees : Cost.PolyTimeFun ι (List ℕ)) : Cost.PolyTimeFun ι SAT.Fml

tableauPlusF.

Equations

• MIPRE.TM.CookLevin.Desc.tableauPlusR eu TR C tabs frees = MIPRE.TM.CookLevin.Desc.orTwo (MIPRE.TM.CookLevin.Desc.tableauR eu C tabs frees) (MIPRE.TM.CookLevin.Desc.ansEndR eu TR C)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.tableauPlusR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (C : CandR ι) (tabs : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))) (frees : Cost.PolyTimeFun ι (List ℕ)) (i : ι) : (tableauPlusR eu TR C tabs frees).toFun i = tableauPlusF (List.length (eu.toFun i)) Gc (TR.toFun i) (tabs.toFun i) (frees.toFun i) (tplsOf Gc chk) (C.ev i)