The start-clause family emitter

startClausesF pins row 0 of the tableau: the start state, the three head positions, and every initial cell symbol. The cell symbols of tape 0 are the input bits, so their unit clauses are emitted by a probe loop — load the variable's positional part, symProbeTM the input symbol index into the scratch, emit. Tapes 1 and 2 are blank beyond ▷, so their loops are ordinary constant-digit clause loops.

def Complexity.SAT.fSym : Γ → Fin 4

The symbol-index map, packaged for the probe.

Equations

• Complexity.SAT.fSym s = ⟨Complexity.SAT.Tableau.symIdx s, ⋯⟩

theorem Complexity.SAT.probeBudget {p d M : ℕ} (hp : p ≤ M) (hd : d ≤ M) : 3 * p + 2 * d + 20 ≤ TM.opBudget M

The probe's bound fits the budget.

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

The four constant start clauses: start state and the three heads.

Equations

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

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

The constant start clauses emitter.

Equations

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

theorem Complexity.SAT.emitStartConstTM_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) : (emitStartConstTM 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 [[{ sign := true, var := Tableau.vStateF (Fintype.card N.Q) steps P 0 (Tableau.stateIdx N N.qstart) }], [{ sign := true, var := Tableau.vHeadF (Fintype.card N.Q) steps P 0 0 0 }], [{ sign := true, var := Tableau.vHeadF (Fintype.card N.Q) steps P 0 1 0 }], [{ sign := true, var := Tableau.vHeadF (Fintype.card N.Q) steps P 0 2 0 }]])) (cnfBudget 4 1 M)

emitStartConstTM Hoare specification.

def Complexity.SAT.startCellD (tp d : ℕ) : LitDesc Emit.nT

The cell unit clause at position read from pos1Reg, constant symbol digit d.

Equations

• Complexity.SAT.startCellD tp d = { sign := true, tag := 2, sa := Sum.inr 0, sb := Sum.inr tp, sc := Sum.inl Complexity.SAT.Emit.pos1Reg, sd := Sum.inr d }

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

One start-cell block for tape tp ∈ {1,2}: the ▷ clause at position 0, then the blank clauses at positions 1..P.

Equations

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

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

Budget of one blank-tape start block.

Equations

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

theorem Complexity.SAT.startBlankPartTM_hoareTime (tp : ℕ) (htp1 : 1 ≤ tp) (htp : tp < 3) (x : List Bool) (Qc steps P M : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (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) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVpReg : V Emit.pReg = TM.regTape P) : (startBlankPartTM 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 (List.map (fun (pos : ℕ) => [{ sign := true, var := Tableau.vCellF Qc steps P 0 tp pos (Tableau.symIdx (Tableau.initCellSym x tp pos)) }]) (List.range (P + 1))))) (startBlankBudget M)

startBlankPartTM Hoare specification (tape tp ∈ {1,2}).

def Complexity.SAT.startProbeBodyTM : TM Emit.nT

The probe loop body: load the positional part of the cell variable, probe the input symbol index into the scratch, emit the unit clause.

Equations

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

def Complexity.SAT.startProbePartTM : TM Emit.nT

The input-tape start-cell block.

Equations

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

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

Budget of the probe body.

Equations

• Complexity.SAT.startProbeBodyBudget M = Complexity.TM.loadBudget M + 4 * Complexity.TM.opBudget M + 7

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

Budget of the input-tape start block.

Equations

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

theorem Complexity.SAT.startProbeBodyTM_hoareTime (x : List Bool) (Qc steps P M j : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (hj : j < P) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hhead : inp₀.head = 1) (hwfcell : inp₀.cells 0 = Γ.start) (hcells : ∀ (pos : ℕ), inp₀.cells pos = Tableau.initCellSym x 0 pos) (hV : ∀ (l : Fin Emit.nT), TM.Parked (V l)) (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) (hVp1 : V Emit.pos1Reg = TM.regTape (1 + j)) : startProbeBodyTM.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 [[{ sign := true, var := Tableau.vCellF Qc steps P 0 0 (1 + j) (Tableau.symIdx (Tableau.initCellSym x 0 (1 + j))) }]])) (startProbeBodyBudget M)

startProbeBodyTM Hoare specification (at position 1 + j).

theorem Complexity.SAT.startProbePartTM_hoareTime (x : List Bool) (Qc steps P M : ℕ) (hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M) (inp₀ : Tape) (V : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hhead : inp₀.head = 1) (hwfcell : inp₀.cells 0 = Γ.start) (hcells : ∀ (pos : ℕ), inp₀.cells pos = Tableau.initCellSym x 0 pos) (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) (hVp1 : V Emit.pos1Reg = TM.regTape 0) (hVpReg : V Emit.pReg = TM.regTape P) : startProbePartTM.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 (List.map (fun (pos : ℕ) => [{ sign := true, var := Tableau.vCellF Qc steps P 0 0 pos (Tableau.symIdx (Tableau.initCellSym x 0 pos)) }]) (List.range (P + 1))))) (startProbeBudget M)

startProbePartTM Hoare specification: the input-tape start cells.

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

The start-family emitter: the constant clauses, then the three per-tape cell blocks.

Equations

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

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

Budget of the start family.

Equations

• Complexity.SAT.startBudget M = Complexity.SAT.cnfBudget 4 1 M + 1 + (Complexity.SAT.startProbeBudget M + 1 + (Complexity.SAT.startBlankBudget M + 1 + Complexity.SAT.startBlankBudget M))

theorem Complexity.SAT.emitStartTM_hoareTime (N : NTM 1) (x : List Bool) (steps P M : ℕ) (hP : P = steps + x.length + 1) (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₀) (hhead : inp₀.head = 1) (hwfcell : inp₀.cells 0 = Γ.start) (hcells : ∀ (pos : ℕ), inp₀.cells pos = Tableau.initCellSym x 0 pos) (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) (hp1 : work₀ Emit.pos1Reg = TM.regTape 0) (hpReg : work₀ Emit.pReg = TM.regTape P) : (emitStartTM 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.startClausesF N steps x))) (startBudget M)

emitStartTM Hoare specification: appends the encoded start clauses.