The clause-family emitters

One emitting machine per tableauCNFFlat family handled here — the accept, state/cell/head one-hot, and frame families — each with a Hoare specification appending exactly that family's CNF.encode image. (The start and active families are emitted in EmitterStart and EmitterActive.)

The emitter's tape layout is fixed once (Emit.nT = 20 work tapes, named indices below), so register-distinctness side conditions are all decide.

@[reducible, inline]

abbrev Complexity.SAT.Emit.nT : ℕ

Number of work tapes of the reduction emitter.

Equations

• Complexity.SAT.Emit.nT = 20

@[reducible, inline]

abbrev Complexity.SAT.Emit.rA : Fin nT

Register holding radix A = steps + 1.

Equations

• Complexity.SAT.Emit.rA = 0

@[reducible, inline]

abbrev Complexity.SAT.Emit.rB : Fin nT

Register holding radix B = max Qc 3.

Equations

• Complexity.SAT.Emit.rB = 1

@[reducible, inline]

abbrev Complexity.SAT.Emit.rC : Fin nT

Register holding radix C = P + 2.

Equations

• Complexity.SAT.Emit.rC = 2

@[reducible, inline]

abbrev Complexity.SAT.Emit.rD : Fin nT

Register holding radix D = 4.

Equations

• Complexity.SAT.Emit.rD = 3

@[reducible, inline]

abbrev Complexity.SAT.Emit.tmp : Fin nT

Numeral scratch register.

Equations

• Complexity.SAT.Emit.tmp = 4

@[reducible, inline]

abbrev Complexity.SAT.Emit.tmp2 : Fin nT

Second numeral scratch register.

Equations

• Complexity.SAT.Emit.tmp2 = 5

@[reducible, inline]

abbrev Complexity.SAT.Emit.nReg : Fin nT

Register holding the input length |x|.

Equations

• Complexity.SAT.Emit.nReg = 6

@[reducible, inline]

abbrev Complexity.SAT.Emit.stepsReg : Fin nT

Register holding steps = p.eval |x|.

Equations

• Complexity.SAT.Emit.stepsReg = 7

@[reducible, inline]

abbrev Complexity.SAT.Emit.pReg : Fin nT

Register holding P = steps + |x| + 1.

Equations

• Complexity.SAT.Emit.pReg = 8

@[reducible, inline]

abbrev Complexity.SAT.Emit.tReg : Fin nT

Register holding the row counter t.

Equations

• Complexity.SAT.Emit.tReg = 9

@[reducible, inline]

abbrev Complexity.SAT.Emit.tFuel : Fin nT

Register holding the row-loop fuel.

Equations

• Complexity.SAT.Emit.tFuel = 10

@[reducible, inline]

abbrev Complexity.SAT.Emit.tPlusReg : Fin nT

Register holding the successor row t + 1.

Equations

• Complexity.SAT.Emit.tPlusReg = 11

@[reducible, inline]

abbrev Complexity.SAT.Emit.pos1Reg : Fin nT

Register holding the position counter (pos / pi).

Equations

• Complexity.SAT.Emit.pos1Reg = 12

@[reducible, inline]

abbrev Complexity.SAT.Emit.pos1Fuel : Fin nT

Register holding the position-loop fuel (P + 1).

Equations

• Complexity.SAT.Emit.pos1Fuel = 13

@[reducible, inline]

abbrev Complexity.SAT.Emit.pos2Reg : Fin nT

Register holding the second position counter (pos' / pw).

Equations

• Complexity.SAT.Emit.pos2Reg = 14

@[reducible, inline]

abbrev Complexity.SAT.Emit.pos2Fuel : Fin nT

Register holding the second position fuel (P + 1).

Equations

• Complexity.SAT.Emit.pos2Fuel = 15

@[reducible, inline]

abbrev Complexity.SAT.Emit.pos3Reg : Fin nT

Register holding the third position counter (po).

Equations

• Complexity.SAT.Emit.pos3Reg = 16

@[reducible, inline]

abbrev Complexity.SAT.Emit.pos3Fuel : Fin nT

Register holding the third position fuel (P + 1).

Equations

• Complexity.SAT.Emit.pos3Fuel = 17

@[reducible, inline]

abbrev Complexity.SAT.Emit.auxReg : Fin nT

Spare register.

Equations

• Complexity.SAT.Emit.auxReg = 18

@[reducible, inline]

abbrev Complexity.SAT.Emit.auxReg2 : Fin nT

Second spare register.

Equations

• Complexity.SAT.Emit.auxReg2 = 19

theorem Complexity.SAT.forall₂_map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : β → γ → Prop} (g : α → β) (h : α → γ) {l : List α} (hp : ∀ a ∈ l, R (g a) (h a)) : List.Forall₂ R (List.map g l) (List.map h l)

Pointwise Forall₂ between two maps of the same list.

theorem Complexity.SAT.forall₂_append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ u₁ : List α} {l₂ u₂ : List β} : List.Forall₂ R l₁ l₂ → List.Forall₂ R u₁ u₂ → List.Forall₂ R (l₁ ++ u₁) (l₂ ++ u₂)

Forall₂ is preserved by appending componentwise-related lists.

def Complexity.SAT.atMostOneD {n : ℕ} (mk : ℕ → LitDesc n) : List ℕ → List (List (LitDesc n))

Descriptor mirror of atMostOne.

Equations

• Complexity.SAT.atMostOneD mk [] = []
• Complexity.SAT.atMostOneD mk (q :: qs) = List.map (fun (q' : ℕ) => [mk q, mk q']) qs ++ Complexity.SAT.atMostOneD mk qs

def Complexity.SAT.exactlyOneD {n : ℕ} (mkPos mkNeg : ℕ → LitDesc n) (qs : List ℕ) : List (List (LitDesc n))

Descriptor mirror of exactlyOne.

Equations

• Complexity.SAT.exactlyOneD mkPos mkNeg qs = List.map mkPos qs :: Complexity.SAT.atMostOneD mkNeg qs

theorem Complexity.SAT.forall₂_atMostOneD {n : ℕ} {R : LitDesc n → Lit → Prop} (mk : ℕ → LitDesc n) (f : ℕ → ℕ) {qs : List ℕ} : (∀ q ∈ qs, R (mk q) { sign := false, var := f q }) → List.Forall₂ (List.Forall₂ R) (atMostOneD mk qs) (Tableau.atMostOne (List.map f qs))

atMostOneD mk qs denotes atMostOne (qs.map f) clause-by-clause, provided each descriptor mk q denotes the negative literal on f q.

theorem Complexity.SAT.forall₂_exactlyOneD {n : ℕ} {R : LitDesc n → Lit → Prop} (mkPos mkNeg : ℕ → LitDesc n) (f : ℕ → ℕ) {qs : List ℕ} (hpos : ∀ q ∈ qs, R (mkPos q) { sign := true, var := f q }) (hneg : ∀ q ∈ qs, R (mkNeg q) { sign := false, var := f q }) : List.Forall₂ (List.Forall₂ R) (exactlyOneD mkPos mkNeg qs) (Tableau.exactlyOne (List.map f qs))

exactlyOneD mkPos mkNeg qs denotes exactlyOne (qs.map f) clause-by-clause, given the positive/negative literal denotations.

theorem Complexity.SAT.atMostOneD_length_le {n : ℕ} (mk : ℕ → LitDesc n) (qs : List ℕ) (c : List (LitDesc n)) : c ∈ atMostOneD mk qs → c.length ≤ 2

Clause sizes in atMostOneD are 2.

theorem Complexity.SAT.atMostOneD_card_le {n : ℕ} (mk : ℕ → LitDesc n) (qs : List ℕ) : (atMostOneD mk qs).length ≤ qs.length * qs.length

atMostOneD over m indices has at most m² clauses.

noncomputable def Complexity.SAT.acceptDescs (N : NTM 1) : List (List (LitDesc Emit.nT))

Descriptors of the two accept clauses.

Equations

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

noncomputable def Complexity.SAT.emitAcceptTM (N : NTM 1) : TM Emit.nT

The accept-family emitter.

Equations

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

theorem Complexity.SAT.emitAcceptTM_hoareTime (N : NTM 1) (steps P M : ℕ) (hM : 4 * (steps + 1) * max (Fintype.card N.Q) 3 * (P + 2) * 4 ≤ M) (inp₀ : Tape) (work₀ : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin Emit.nT), TM.Parked (work₀ i)) (hrA : work₀ Emit.rA = TM.regTape (steps + 1)) (hrB : work₀ Emit.rB = TM.regTape (max (Fintype.card N.Q) 3)) (hrC : work₀ Emit.rC = TM.regTape (P + 2)) (hrD : work₀ Emit.rD = TM.regTape 4) (hsteps : work₀ Emit.stepsReg = TM.regTape steps) : (emitAcceptTM N).HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch work₀ Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.acceptClausesF N steps P))) (cnfBudget 2 1 M)

emitAcceptTM Hoare specification: appends the encoded accept clauses.

def Complexity.SAT.oneHotStatesLeafD (Qc : ℕ) : List (List (LitDesc Emit.nT))

Leaf descriptors: exactly one state at the row read from tReg.

Equations

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

def Complexity.SAT.emitOneHotStatesTM (Qc : ℕ) : TM Emit.nT

The state one-hot emitter: loop the leaf over all rows.

Equations

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

theorem Complexity.SAT.emitOneHotStatesTM_hoareTime (N : NTM 1) (steps P M : ℕ) (hM : 4 * (steps + 1) * max (Fintype.card N.Q) 3 * (P + 2) * 4 ≤ M) (inp₀ : Tape) (work₀ : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin Emit.nT), TM.Parked (work₀ i)) (hrA : work₀ Emit.rA = TM.regTape (steps + 1)) (hrB : work₀ Emit.rB = TM.regTape (max (Fintype.card N.Q) 3)) (hrC : work₀ Emit.rC = TM.regTape (P + 2)) (hrD : work₀ Emit.rD = TM.regTape 4) (htReg : work₀ Emit.tReg = TM.regTape 0) (htFuel : work₀ Emit.tFuel = TM.regTape (steps + 1)) : (emitOneHotStatesTM (Fintype.card N.Q)).HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch (Function.update work₀ Emit.tReg (TM.regTape (steps + 1))) Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.oneHotStatesF N steps P))) (loopBudget M (cnfBudget (1 + M * M) (M + 2) M))

emitOneHotStatesTM Hoare specification: appends the encoded state one-hot family, leaving the row counter at steps + 1.

def Complexity.SAT.cellLeafD (tp : ℕ) : List (List (LitDesc Emit.nT))

Leaf descriptors: exactly one symbol per row/tape/position.

Equations

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

def Complexity.SAT.posChunkTM (tp : ℕ) : TM Emit.nT

Position sweep at one tape index: loop the leaf over positions, then return the position counter to zero.

Equations

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

def Complexity.SAT.cellsBodyTM : TM Emit.nT

The oneHotCells row body: position sweeps at the three tape indices.

Equations

• Complexity.SAT.cellsBodyTM = (Complexity.SAT.posChunkTM 0).seqTM ((Complexity.SAT.posChunkTM 1).seqTM (Complexity.SAT.posChunkTM 2))

def Complexity.SAT.emitOneHotCellsTM : TM Emit.nT

The cell one-hot emitter: loop the row body over all rows.

Equations

• Complexity.SAT.emitOneHotCellsTM = Complexity.SAT.emitLoopTM Complexity.SAT.cellsBodyTM Complexity.SAT.Emit.tReg Complexity.SAT.Emit.tFuel

def Complexity.SAT.posChunkBudget (M : ℕ) : ℕ

Budget of one position sweep.

Equations

• Complexity.SAT.posChunkBudget M = Complexity.SAT.loopBudget M (Complexity.SAT.cnfBudget 17 6 M) + 1 + Complexity.TM.opBudget M

theorem Complexity.SAT.posChunkTM_hoareTime (tp : ℕ) (htp : tp < 3) (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) : (posChunkTM tp).HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (pos : ℕ) => CNF.encode (Tableau.exactlyOne (List.map (Tableau.vCellF Qc steps P i tp pos) (List.range 4)))) (List.range (P + 1)))) (posChunkBudget M)

posChunkTM Hoare specification (at row i, tape index tp).

def Complexity.SAT.cellsBodyBudget (M : ℕ) : ℕ

Budget of the oneHotCells row body.

Equations

• Complexity.SAT.cellsBodyBudget M = 3 * Complexity.SAT.posChunkBudget M + 2

theorem Complexity.SAT.cellsBodyTM_hoareTime (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) : cellsBodyTM.HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (tp : ℕ) => List.flatMap (fun (pos : ℕ) => CNF.encode (Tableau.exactlyOne (List.map (Tableau.vCellF Qc steps P i tp pos) (List.range 4)))) (List.range (P + 1))) (List.range 3))) (cellsBodyBudget M)

cellsBodyTM Hoare specification (at row i).

theorem Complexity.SAT.emitOneHotCellsTM_hoareTime (Qc steps P M : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (inp₀ : Tape) (work₀ : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin Emit.nT), TM.Parked (work₀ i)) (hrA : work₀ Emit.rA = TM.regTape (steps + 1)) (hrB : work₀ Emit.rB = TM.regTape (max Qc 3)) (hrC : work₀ Emit.rC = TM.regTape (P + 2)) (hrD : work₀ Emit.rD = TM.regTape 4) (htReg : work₀ Emit.tReg = TM.regTape 0) (htFuel : work₀ Emit.tFuel = TM.regTape (steps + 1)) (hp1 : work₀ Emit.pos1Reg = TM.regTape 0) (hf1 : work₀ Emit.pos1Fuel = TM.regTape (P + 1)) : emitOneHotCellsTM.HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch (Function.update work₀ Emit.tReg (TM.regTape (steps + 1))) Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.oneHotCellsF Qc steps P))) (loopBudget M (cellsBodyBudget M))

emitOneHotCellsTM Hoare specification: appends the encoded cell one-hot family, leaving the row counter at steps + 1.

theorem Complexity.SAT.flatMap_congr {α : Type u_1} {β : Type u_2} {l : List α} {f g : α → List β} (h : ∀ a ∈ l, f a = g a) : List.flatMap f l = List.flatMap g l

flatMap respects pointwise-equal functions on the list's members.

theorem Complexity.SAT.atMostOne_map_range (m : ℕ) (f : ℕ → ℕ) : Tableau.atMostOne (List.map f (List.range m)) = List.flatMap (fun (q : ℕ) => List.map (fun (j : ℕ) => [{ sign := false, var := f q }, { sign := false, var := f (q + 1 + j) }]) (List.range (m - (q + 1)))) (List.range m)

atMostOne over a mapped range as rectangle loops with shrinking inner ranges — the shape the head emitter's nested loops produce.

def Complexity.SAT.headLitD (sign : Bool) (tp : ℕ) (posSrc : Fin Emit.nT) : LitDesc Emit.nT

One head literal: row from tReg, tape index hardwired, position from posSrc.

Equations

• Complexity.SAT.headLitD sign tp posSrc = { sign := sign, tag := 3, sa := Sum.inl Complexity.SAT.Emit.tReg, sb := Sum.inr tp, sc := Sum.inl posSrc, sd := Sum.inr 0 }

def Complexity.SAT.headAtLeastTM (tp : ℕ) : TM Emit.nT

The at-least-one head clause: loop the positive literal over all positions, close the clause, return the position counter.

Equations

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

def Complexity.SAT.headAtLeastBudget (M : ℕ) : ℕ

Budget of the at-least-one head clause.

Equations

• Complexity.SAT.headAtLeastBudget M = Complexity.SAT.loopBudget M (Complexity.TM.emitVarBudget M + 1 + (2 * Complexity.TM.opBudget M + 1)) + 1 + (2 + 1 + Complexity.TM.opBudget M)

theorem Complexity.SAT.headLitD_spec {tp : ℕ} (htp : tp < 3) {Qc steps P M i pos : ℕ} (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (hpos : pos ≤ P) {posSrc : Fin Emit.nT} (hst : posSrc ≠ Emit.tmp) (hst2 : posSrc ≠ Emit.tmp2) {base : Fin Emit.nT → Tape} (sgn : Bool) (hbt : base Emit.tReg = TM.regTape i) (hbp : base posSrc = TM.regTape pos) : LitDesc.Spec base Emit.tmp Emit.tmp2 M (steps + 1) (max Qc 3) (P + 2) 4 (headLitD sgn tp posSrc) { sign := sgn, var := Tableau.vHeadF Qc steps P i tp pos }

The head-literal denotation lemma, shared by both head clause shapes.

theorem Complexity.SAT.headAtLeastTM_hoareTime (tp : ℕ) (htp : tp < 3) (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) : (headAtLeastTM tp).HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) (ys ++ ((Tableau.atLeastOne (List.map (Tableau.vHeadF Qc steps P i tp) (List.range (P + 1)))).encode ++ [true, false]))) (headAtLeastBudget M)

headAtLeastTM Hoare specification (at row i, tape index tp).

def Complexity.SAT.headPairBodyTM (tp : ℕ) : TM Emit.nT

The pairwise at-most-one clauses: outer loop over the first position; per outer step, mirror the counter past it, sweep the (offset, shrinking) inner loop, and shrink the fuel.

Equations

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

def Complexity.SAT.headAtMostTM (tp : ℕ) : TM Emit.nT

The pairwise at-most-one head sweep: loop headPairBodyTM over the outer position, then return the position counter to zero.

Equations

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

def Complexity.SAT.pairBodyBudget (M : ℕ) : ℕ

Budget of one outer step of the pairwise sweep.

Equations

• Complexity.SAT.pairBodyBudget M = Complexity.SAT.loopBudget M (Complexity.SAT.clauseBudget 2 M) + 4 * Complexity.TM.opBudget M + 4

def Complexity.SAT.pairWord (Qc steps P i tp q : ℕ) : List Bool

The per-outer-position word of the pairwise sweep.

Equations

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

theorem Complexity.SAT.headPairBodyTM_hoareTime (tp : ℕ) (htp : tp < 3) (Qc steps P M i q : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (hq : q ≤ P) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp2 : V Emit.pos2Reg = TM.regTape 0) : (headPairBodyTM tp).HoareTime (TM.EmitPred inp₀ (Function.update (Function.update (Function.update (TM.scratch V Emit.tmp Emit.tmp2 0) Emit.pos1Reg (TM.regTape q)) Emit.auxReg (TM.regTape (P - q))) Emit.pos1Fuel { head := q + 2, cells := TM.regCells (P + 1) }) ys) (TM.EmitPred inp₀ (Function.update (Function.update (Function.update (TM.scratch V Emit.tmp Emit.tmp2 0) Emit.pos1Reg (TM.regTape q)) Emit.auxReg (TM.regTape (P - (q + 1)))) Emit.pos1Fuel { head := q + 2, cells := TM.regCells (P + 1) }) (ys ++ pairWord Qc steps P i tp q)) (pairBodyBudget M)

headPairBodyTM Hoare specification (at row i, outer position q): emits the pair clauses (q, q') for all q' > q, mirrors the counters home, and shrinks the fuel.

def Complexity.SAT.headAtMostBudget (M : ℕ) : ℕ

Budget of the pairwise at-most-one sweep.

Equations

• Complexity.SAT.headAtMostBudget M = Complexity.SAT.loopBudget M (Complexity.SAT.pairBodyBudget M) + 1 + Complexity.TM.opBudget M

theorem Complexity.SAT.headAtMostTM_hoareTime (tp : ℕ) (htp : tp < 3) (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) (hVp2 : V Emit.pos2Reg = TM.regTape 0) (hVaux : V Emit.auxReg = TM.regTape P) : (headAtMostTM tp).HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch (Function.update V Emit.auxReg (TM.regTape 0)) Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.atMostOne (List.map (Tableau.vHeadF Qc steps P i tp) (List.range (P + 1)))))) (headAtMostBudget M)

headAtMostTM Hoare specification (at row i, tape index tp): appends the encoded pairwise at-most-one clauses, consuming the shrink fuel (auxReg: P in, 0 out).

def Complexity.SAT.headLeafTM (tp : ℕ) : TM Emit.nT

One (row, tape) head leaf: initialize the shrink fuel, then the exactly-one block.

Equations

• Complexity.SAT.headLeafTM tp = (Complexity.TM.copyIntoTM Complexity.SAT.Emit.pReg Complexity.SAT.Emit.auxReg).seqTM ((Complexity.SAT.headAtLeastTM tp).seqTM (Complexity.SAT.headAtMostTM tp))

def Complexity.SAT.headLeafBudget (M : ℕ) : ℕ

Budget of one head leaf.

Equations

• Complexity.SAT.headLeafBudget M = Complexity.TM.opBudget M + 1 + (Complexity.SAT.headAtLeastBudget M + 1 + Complexity.SAT.headAtMostBudget M)

theorem Complexity.SAT.headLeafTM_hoareTime (tp : ℕ) (htp : tp < 3) (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) (hVp2 : V Emit.pos2Reg = TM.regTape 0) (hVaux : V Emit.auxReg = TM.regTape 0) (hVpReg : V Emit.pReg = TM.regTape P) : (headLeafTM tp).HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.exactlyOne (List.map (Tableau.vHeadF Qc steps P i tp) (List.range (P + 1)))))) (headLeafBudget M)

headLeafTM Hoare specification (at row i, tape index tp).

def Complexity.SAT.headsBodyTM : TM Emit.nT

The oneHotHeads row body: head leaves at the three tape indices.

Equations

• Complexity.SAT.headsBodyTM = (Complexity.SAT.headLeafTM 0).seqTM ((Complexity.SAT.headLeafTM 1).seqTM (Complexity.SAT.headLeafTM 2))

def Complexity.SAT.emitOneHotHeadsTM : TM Emit.nT

The head one-hot emitter: loop the row body over all rows.

Equations

• Complexity.SAT.emitOneHotHeadsTM = Complexity.SAT.emitLoopTM Complexity.SAT.headsBodyTM Complexity.SAT.Emit.tReg Complexity.SAT.Emit.tFuel

def Complexity.SAT.headsBodyBudget (M : ℕ) : ℕ

Budget of the oneHotHeads row body.

Equations

• Complexity.SAT.headsBodyBudget M = 3 * Complexity.SAT.headLeafBudget M + 2

theorem Complexity.SAT.headsBodyTM_hoareTime (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i ≤ steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) (hVp2 : V Emit.pos2Reg = TM.regTape 0) (hVaux : V Emit.auxReg = TM.regTape 0) (hVpReg : V Emit.pReg = TM.regTape P) : headsBodyTM.HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (tp : ℕ) => CNF.encode (Tableau.exactlyOne (List.map (Tableau.vHeadF Qc steps P i tp) (List.range (P + 1))))) (List.range 3))) (headsBodyBudget M)

headsBodyTM Hoare specification (at row i).

theorem Complexity.SAT.emitOneHotHeadsTM_hoareTime (Qc steps P M : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (inp₀ : Tape) (work₀ : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin Emit.nT), TM.Parked (work₀ i)) (hrA : work₀ Emit.rA = TM.regTape (steps + 1)) (hrB : work₀ Emit.rB = TM.regTape (max Qc 3)) (hrC : work₀ Emit.rC = TM.regTape (P + 2)) (hrD : work₀ Emit.rD = TM.regTape 4) (htReg : work₀ Emit.tReg = TM.regTape 0) (htFuel : work₀ Emit.tFuel = TM.regTape (steps + 1)) (hp1 : work₀ Emit.pos1Reg = TM.regTape 0) (hf1 : work₀ Emit.pos1Fuel = TM.regTape (P + 1)) (hp2 : work₀ Emit.pos2Reg = TM.regTape 0) (haux : work₀ Emit.auxReg = TM.regTape 0) (hpReg : work₀ Emit.pReg = TM.regTape P) : emitOneHotHeadsTM.HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch (Function.update work₀ Emit.tReg (TM.regTape (steps + 1))) Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.oneHotHeadsF Qc steps P))) (loopBudget M (headsBodyBudget M))

emitOneHotHeadsTM Hoare specification: appends the encoded head one-hot family, leaving the row counter at steps + 1.

theorem Complexity.SAT.forall₂_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : β → γ → Prop} (F : α → List β) (G : α → List γ) {l : List α} (h : ∀ a ∈ l, List.Forall₂ R (F a) (G a)) : List.Forall₂ R (List.flatMap F l) (List.flatMap G l)

Forall₂ is preserved by flatMap with pointwise-related images.

def Complexity.SAT.frameDescs (tp s : ℕ) : List (List (LitDesc Emit.nT))

Descriptors of the two frame clauses at symbol s, tape index tp.

Equations

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

def Complexity.SAT.frameLeafD (tp : ℕ) : List (List (LitDesc Emit.nT))

The frame leaf at one (row, tape, position): both clauses for all four symbols.

Equations

• Complexity.SAT.frameLeafD tp = List.flatMap (Complexity.SAT.frameDescs tp) (List.range 4)

def Complexity.SAT.framePosChunkTM (tp : ℕ) : TM Emit.nT

Frame position sweep at one tape index.

Equations

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

def Complexity.SAT.frameRowTM : TM Emit.nT

The frame row body: bump the successor-row register, then sweep the three tapes.

Equations

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

def Complexity.SAT.emitFrameTM : TM Emit.nT

The frame-family emitter: loop the row body over rows 0..steps-1.

Equations

• Complexity.SAT.emitFrameTM = Complexity.SAT.emitLoopTM Complexity.SAT.frameRowTM Complexity.SAT.Emit.tReg Complexity.SAT.Emit.tFuel

def Complexity.SAT.frameLeafF (Qc steps P t tp pos : ℕ) : CNF

The frame leaf formula at one (row, tape, position).

Equations

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

def Complexity.SAT.framePosChunkBudget (M : ℕ) : ℕ

Budget of one frame position sweep.

Equations

• Complexity.SAT.framePosChunkBudget M = Complexity.SAT.loopBudget M (Complexity.SAT.cnfBudget 8 3 M) + 1 + Complexity.TM.opBudget M

def Complexity.SAT.frameRowBudget (M : ℕ) : ℕ

Budget of the frame row body.

Equations

• Complexity.SAT.frameRowBudget M = Complexity.TM.opBudget M + 1 + (3 * Complexity.SAT.framePosChunkBudget M + 2)

theorem Complexity.SAT.framePosChunkTM_hoareTime (tp : ℕ) (htp : tp < 3) (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i < steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVtp : V Emit.tPlusReg = TM.regTape (i + 1)) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) : (framePosChunkTM tp).HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (pos : ℕ) => (frameLeafF Qc steps P i tp pos).encode) (List.range (P + 1)))) (framePosChunkBudget M)

framePosChunkTM Hoare specification (at row i, tape tp; the successor-row register holds i + 1).

theorem Complexity.SAT.frameRowTM_hoareTime (Qc steps P M i : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hi : i < steps) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hV : ∀ (j : Fin Emit.nT), TM.Parked (V j)) (hVrA : V Emit.rA = TM.regTape (steps + 1)) (hVrB : V Emit.rB = TM.regTape (max Qc 3)) (hVrC : V Emit.rC = TM.regTape (P + 2)) (hVrD : V Emit.rD = TM.regTape 4) (hVt : V Emit.tReg = TM.regTape i) (hVtp : V Emit.tPlusReg = TM.regTape i) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) : frameRowTM.HoareTime (TM.EmitPred inp₀ (TM.scratch V Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch (Function.update V Emit.tPlusReg (TM.regTape (i + 1))) Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (tp : ℕ) => List.flatMap (fun (pos : ℕ) => (frameLeafF Qc steps P i tp pos).encode) (List.range (P + 1))) (List.range 3))) (frameRowBudget M)

frameRowTM Hoare specification (at row i < steps; the successor-row register enters at i and leaves at i + 1).

theorem Complexity.SAT.emitFrameTM_hoareTime (Qc steps P M : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (inp₀ : Tape) (work₀ : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin Emit.nT), TM.Parked (work₀ i)) (hrA : work₀ Emit.rA = TM.regTape (steps + 1)) (hrB : work₀ Emit.rB = TM.regTape (max Qc 3)) (hrC : work₀ Emit.rC = TM.regTape (P + 2)) (hrD : work₀ Emit.rD = TM.regTape 4) (htReg : work₀ Emit.tReg = TM.regTape 0) (htFuel : work₀ Emit.tFuel = TM.regTape steps) (htp : work₀ Emit.tPlusReg = TM.regTape 0) (hp1 : work₀ Emit.pos1Reg = TM.regTape 0) (hf1 : work₀ Emit.pos1Fuel = TM.regTape (P + 1)) : emitFrameTM.HoareTime (TM.EmitPred inp₀ (TM.scratch work₀ Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch (Function.update (Function.update work₀ Emit.tReg (TM.regTape steps)) Emit.tPlusReg (TM.regTape steps)) Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.frameClausesF Qc steps P))) (loopBudget M (frameRowBudget M))

emitFrameTM Hoare specification: appends the encoded frame family, leaving row counter and successor-row register at steps.