The active-transition family emitter

activeTransitionClausesF quantifies over rows, machine states, three head positions, three read symbols, and the choice bit; per tuple it emits seven implication clauses (the eight-literal reading condition plus one consequence each). States, symbols, and the choice bit are finite data unrolled at definition level (bigSeqTM over their lists); rows and positions are runtime loops.

theorem Complexity.SAT.bigSeq_emit_hoareTime {α : Type u_1} (F : α → TM Emit.nT) (E : α → List Bool) (b : ℕ) (inp₀ : Tape) (W : Fin Emit.nT → Tape) (hinp₀ : TM.Parked inp₀) (hWP : ∀ (i : Fin Emit.nT), TM.Parked (W i)) (l : List α) : (∀ a ∈ l, ∀ (ys : List Bool), (F a).HoareTime (TM.EmitPred inp₀ W ys) (TM.EmitPred inp₀ W (ys ++ E a)) b) → ∀ (ys : List Bool), (TM.bigSeqTM (List.map F l)).HoareTime (TM.EmitPred inp₀ W ys) (TM.EmitPred inp₀ W (ys ++ List.flatMap E l)) (l.length * (b + 1) + 1)

Unrolled emission: if every element's machine appends its word from any accumulator, the bigSeqTM of the mapped list appends the flatMap.

theorem Complexity.SAT.flatMap_range_split {γ : Type u_1} (n : ℕ) (G : ℕ → List γ) : List.flatMap G (List.range (n + 1)) = G 0 ++ List.flatMap (fun (j : ℕ) => G (1 + j)) (List.range n)

Peel the zero iteration off a range flatMap.

def Complexity.SAT.setupPosTM (p : Fin Emit.nT) : Option Dir3 → TM Emit.nT

Load posMove-of-a-position into the scratch position register: copy, then adjust by the (definition-level) move. none means the halting state's frozen head.

Equations

• Complexity.SAT.setupPosTM p none = Complexity.TM.copyIntoTM p Complexity.SAT.Emit.auxReg2
• Complexity.SAT.setupPosTM p (some Complexity.Dir3.stay) = Complexity.TM.copyIntoTM p Complexity.SAT.Emit.auxReg2
• Complexity.SAT.setupPosTM p (some Complexity.Dir3.left) = (Complexity.TM.copyIntoTM p Complexity.SAT.Emit.auxReg2).seqTM (Complexity.TM.decRegTM Complexity.SAT.Emit.auxReg2)
• Complexity.SAT.setupPosTM p (some Complexity.Dir3.right) = (Complexity.TM.copyIntoTM p Complexity.SAT.Emit.auxReg2).seqTM (Complexity.TM.incRegTM Complexity.SAT.Emit.auxReg2)

def Complexity.SAT.posMoveOpt (v : ℕ) : Option Dir3 → ℕ

The value setupPosTM leaves in auxReg2.

Equations

• Complexity.SAT.posMoveOpt v none = v
• Complexity.SAT.posMoveOpt v (some d) = Complexity.SAT.Tableau.posMove v d

theorem Complexity.SAT.posMoveOpt_le (v P : ℕ) (mv : Option Dir3) (hv : v ≤ P) : posMoveOpt v mv ≤ P + 1

posMoveOpt moves a position bounded by P to one bounded by P + 1.

theorem Complexity.SAT.setupPosTM_hoareTime (p : Fin Emit.nT) (hp : p ≠ Emit.auxReg2) (mv : Option Dir3) (M v a : ℕ) (hv : v + 1 ≤ M) (ha : a ≤ M) (inp₀ : Tape) (work₀ : Fin Emit.nT → Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) (hwork₀ : ∀ (i : Fin Emit.nT), TM.Parked (work₀ i)) (hpv : work₀ p = TM.regTape v) (haux : work₀ Emit.auxReg2 = TM.regTape a) : (setupPosTM p mv).HoareTime (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ (Function.update work₀ Emit.auxReg2 (TM.regTape (posMoveOpt v mv))) ys) (2 * TM.opBudget M + 1)

setupPosTM Hoare specification: auxReg2 := posMoveOpt of the position register's value.

noncomputable def Complexity.SAT.activeCondD (N : NTM 1) (q : N.Q) (si sw so : Γ) (b : Bool) : List (LitDesc Emit.nT)

Descriptors of the eight-literal reading condition.

Equations

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

structure Complexity.SAT.ActiveBase (Qc steps P M t pi pw po : ℕ) (base : Fin Emit.nT → Tape) : Prop

The standing register facts of the active family's leaves.

• hM : 4 * (steps + 1) * max Qc 3 * (P + 2) * 4 ≤ M

  The mixed-radix capacity product is within the modulus bound M.

• ht : t < steps

  The row index is below the row count.

• hpi : pi ≤ P

  The input-head position is within the position bound.

• hpw : pw ≤ P

  The work-head position is within the position bound.

• hpo : po ≤ P

  The output-head position is within the position bound.

• parked (l : Fin Emit.nT) : TM.Parked (base l)

  Every work tape is parked (head at cell 0).

• hrA : base Emit.rA = TM.regTape (steps + 1)

  Radix register A holds the row capacity steps + 1.

• hrB : base Emit.rB = TM.regTape (max Qc 3)

  Radix register B holds the state capacity max Qc 3.

• hrC : base Emit.rC = TM.regTape (P + 2)

  Radix register C holds the position capacity P + 2.

• hrD : base Emit.rD = TM.regTape 4

  Radix register D holds the symbol capacity 4.

• htReg : base Emit.tReg = TM.regTape t

  The row register holds the current row t.

• htPlus : base Emit.tPlusReg = TM.regTape (t + 1)

  The successor-row register holds t + 1.

• hp1 : base Emit.pos1Reg = TM.regTape pi

  The first position register holds the input-head position.

• hp2 : base Emit.pos2Reg = TM.regTape pw

  The second position register holds the work-head position.

• hp3 : base Emit.pos3Reg = TM.regTape po

  The third position register holds the output-head position.

theorem Complexity.SAT.ActiveBase.update_aux {Qc steps P M t pi pw po : ℕ} {base : Fin Emit.nT → Tape} (hB : ActiveBase Qc steps P M t pi pw po base) (z : ℕ) : ActiveBase Qc steps P M t pi pw po (Function.update base Emit.auxReg2 (TM.regTape z))

The base facts survive scratch-position updates.

theorem Complexity.SAT.activeCondD_spec (N : NTM 1) (q : N.Q) (si sw so : Γ) (b : Bool) {Qc steps P M t pi pw po : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw po base) : List.Forall₂ (LitDesc.Spec base Emit.tmp Emit.tmp2 M (steps + 1) (max Qc 3) (P + 2) 4) (activeCondD N q si sw so b) (Tableau.activeCondF N steps P t q pi si pw sw po so b)

The reading condition denotes activeCondF.

noncomputable def Complexity.SAT.activeClauseTM (N : NTM 1) (q : N.Q) (si sw so : Γ) (b : Bool) (d9 : LitDesc Emit.nT) : TM Emit.nT

One conseq clause emission: the condition plus one consequence literal.

Equations

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

noncomputable def Complexity.SAT.activeLeafTM (N : NTM 1) (q : N.Q) (si sw so : Γ) (b : Bool) (wSymVal oSymVal : Γ) (mvI mvW mvO : Option Dir3) : TM Emit.nT

The per-tuple leaf: the seven implication clauses, with the write symbols and head moves resolved at definition level.

Equations

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

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

Budget of the leaf.

Equations

• Complexity.SAT.activeLeafBudget M = 7 * Complexity.SAT.clauseBudget 9 M + 7 * Complexity.TM.opBudget M + 13

theorem Complexity.SAT.activeClauseTM_hoareTime (N : NTM 1) (q : N.Q) (si sw so : Γ) (b : Bool) {Qc steps P M t pi pw po : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw po base) {d9 : LitDesc Emit.nT} {ℓ9 : Lit} (h9 : LitDesc.Spec base Emit.tmp Emit.tmp2 M (steps + 1) (max Qc 3) (P + 2) 4 d9 ℓ9) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeClauseTM N q si sw so b d9).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ ((Tableau.activeCondF N steps P t q pi si pw sw po so b ++ [ℓ9]).encode ++ [true, false]))) (clauseBudget 9 M)

One conseq-clause emission from an ActiveBase state.

theorem Complexity.SAT.activeLeafTM_hoareTime (N : NTM 1) (q : N.Q) (si sw so : Γ) (b : Bool) (wSymVal oSymVal : Γ) (mvI mvW mvO : Option Dir3) {Qc steps P M t pi pw po : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw po base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hwSym : wSymVal = if q = N.qhalt then sw else if pw = 0 then sw else ((N.δ b q si (fun (x : Fin 1) => sw) so).2.1 0).toΓ) (hoSym : oSymVal = if q = N.qhalt then so else if po = 0 then so else (N.δ b q si (fun (x : Fin 1) => sw) so).2.2.1.toΓ) (hmvI : posMoveOpt pi mvI = if q = N.qhalt then pi else Tableau.posMove pi (N.δ b q si (fun (x : Fin 1) => sw) so).2.2.2.1) (hmvW : posMoveOpt pw mvW = if q = N.qhalt then pw else Tableau.posMove pw ((N.δ b q si (fun (x : Fin 1) => sw) so).2.2.2.2.1 0)) (hmvO : posMoveOpt po mvO = if q = N.qhalt then po else Tableau.posMove po (N.δ b q si (fun (x : Fin 1) => sw) so).2.2.2.2.2) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeLeafTM N q si sw so b wSymVal oSymVal mvI mvW mvO).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b))) (activeLeafBudget M)

activeLeafTM Hoare specification: appends the encoded activeClausesAtF for the tuple.

noncomputable def Complexity.SAT.activeBLevelTM (N : NTM 1) (q : N.Q) (si sw so : Γ) (pwZero poZero : Bool) : TM Emit.nT

The choice-bit unroll, with the position-zero flags static.

Equations

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

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

Budget of the choice-bit unroll: two leaves.

Equations

• Complexity.SAT.activeBLevelBudget M = 2 * (Complexity.SAT.activeLeafBudget M + 1) + 1

theorem Complexity.SAT.activeBLevelTM_hoareTime (N : NTM 1) (q : N.Q) (si sw so : Γ) (pwZero poZero : Bool) {Qc steps P M t pi pw po : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw po base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hpwZ : pwZero = true → pw = 0) (hpwZ' : pwZero = false → pw ≠ 0) (hpoZ : poZero = true → po = 0) (hpoZ' : poZero = false → po ≠ 0) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeBLevelTM N q si sw so pwZero poZero).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false])) (activeBLevelBudget M)

activeBLevelTM Hoare specification.

noncomputable def Complexity.SAT.activeSoLevelTM (N : NTM 1) (q : N.Q) (si sw : Γ) (pwZero poZero : Bool) : TM Emit.nT

The output-symbol unroll.

Equations

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

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

Budget of the output-symbol unroll: four choice-bit levels.

Equations

• Complexity.SAT.activeSoLevelBudget M = 4 * (Complexity.SAT.activeBLevelBudget M + 1) + 1

theorem Complexity.SAT.activeSoLevelTM_hoareTime (N : NTM 1) (q : N.Q) (si sw : Γ) (pwZero poZero : Bool) {Qc steps P M t pi pw po : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw po base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hpwZ : pwZero = true → pw = 0) (hpwZ' : pwZero = false → pw ≠ 0) (hpoZ : poZero = true → po = 0) (hpoZ' : poZero = false → po ≠ 0) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeSoLevelTM N q si sw pwZero poZero).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms)) (activeSoLevelBudget M)

activeSoLevelTM Hoare specification.

noncomputable def Complexity.SAT.activePoSplitTM (N : NTM 1) (q : N.Q) (si sw : Γ) (pwZero : Bool) : TM Emit.nT

The output-position block: the po = 0 instance, then the sweep over po = 1..P.

Equations

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

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

Budget of the output-position block: the po = 0 instance plus the counter setup, the sweep loop, and the counter reset.

Equations

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

theorem Complexity.SAT.activePoSplitTM_hoareTime (N : NTM 1) (q : N.Q) (si sw : Γ) (pwZero : Bool) {Qc steps P M t pi pw : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw 0 base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hf3 : base Emit.pos3Fuel = TM.regTape P) (hpwZ : pwZero = true → pw = 0) (hpwZ' : pwZero = false → pw ≠ 0) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activePoSplitTM N q si sw pwZero).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1)))) (activePoSplitBudget M)

activePoSplitTM Hoare specification (at po = 0 boundary state).

noncomputable def Complexity.SAT.activeSwLevelTM (N : NTM 1) (q : N.Q) (si : Γ) (pwZero : Bool) : TM Emit.nT

The work-symbol unroll.

Equations

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

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

Budget of the work-symbol unroll: four output-position blocks.

Equations

• Complexity.SAT.activeSwLevelBudget M = 4 * (Complexity.SAT.activePoSplitBudget M + 1) + 1

theorem Complexity.SAT.activeSwLevelTM_hoareTime (N : NTM 1) (q : N.Q) (si : Γ) (pwZero : Bool) {Qc steps P M t pi pw : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi pw 0 base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hf3 : base Emit.pos3Fuel = TM.regTape P) (hpwZ : pwZero = true → pw = 0) (hpwZ' : pwZero = false → pw ≠ 0) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeSwLevelTM N q si pwZero).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (sw : Γ) => List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms)) (activeSwLevelBudget M)

activeSwLevelTM Hoare specification.

noncomputable def Complexity.SAT.activePwSplitTM (N : NTM 1) (q : N.Q) (si : Γ) : TM Emit.nT

The work-position block: the pw = 0 instance, then the sweep over pw = 1..P.

Equations

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

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

Budget of the work-position block: the pw = 0 instance plus the counter setup, the sweep loop, and the counter reset.

Equations

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

theorem Complexity.SAT.activePwSplitTM_hoareTime (N : NTM 1) (q : N.Q) (si : Γ) {Qc steps P M t pi : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi 0 0 base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hf2 : base Emit.pos2Fuel = TM.regTape P) (hf3 : base Emit.pos3Fuel = TM.regTape P) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activePwSplitTM N q si).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (pw : ℕ) => List.flatMap (fun (sw : Γ) => List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1)))) (activePwSplitBudget M)

activePwSplitTM Hoare specification (at pw = po = 0 boundary state).

noncomputable def Complexity.SAT.activeSiLevelTM (N : NTM 1) (q : N.Q) : TM Emit.nT

The input-symbol unroll.

Equations

• Complexity.SAT.activeSiLevelTM N q = Complexity.TM.bigSeqTM (List.map (fun (si : Complexity.Γ) => Complexity.SAT.activePwSplitTM N q si) Complexity.SAT.Tableau.allSyms)

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

Budget of the input-symbol unroll: four work-position blocks.

Equations

• Complexity.SAT.activeSiLevelBudget M = 4 * (Complexity.SAT.activePwSplitBudget M + 1) + 1

theorem Complexity.SAT.activeSiLevelTM_hoareTime (N : NTM 1) (q : N.Q) {Qc steps P M t pi : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t pi 0 0 base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hf2 : base Emit.pos2Fuel = TM.regTape P) (hf3 : base Emit.pos3Fuel = TM.regTape P) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeSiLevelTM N q).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (si : Γ) => List.flatMap (fun (pw : ℕ) => List.flatMap (fun (sw : Γ) => List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms)) (activeSiLevelBudget M)

activeSiLevelTM Hoare specification.

noncomputable def Complexity.SAT.activePiLoopTM (N : NTM 1) (q : N.Q) : TM Emit.nT

The input-position sweep for one machine state.

Equations

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

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

Budget of the input-position sweep: the loop plus the counter reset.

Equations

• Complexity.SAT.activePiLoopBudget M = Complexity.SAT.loopBudget M (Complexity.SAT.activeSiLevelBudget M) + 1 + Complexity.TM.opBudget M

theorem Complexity.SAT.activePiLoopTM_hoareTime (N : NTM 1) (q : N.Q) {Qc steps P M t : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t 0 0 0 base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hf1 : base Emit.pos1Fuel = TM.regTape (P + 1)) (hf2 : base Emit.pos2Fuel = TM.regTape P) (hf3 : base Emit.pos3Fuel = TM.regTape P) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activePiLoopTM N q).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (pi : ℕ) => List.flatMap (fun (si : Γ) => List.flatMap (fun (pw : ℕ) => List.flatMap (fun (sw : Γ) => List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1)))) (activePiLoopBudget M)

activePiLoopTM Hoare specification (at the row boundary state).

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

The machine-state unroll.

Equations

• Complexity.SAT.activeQLevelTM N = Complexity.TM.bigSeqTM (List.map (fun (q : N.Q) => Complexity.SAT.activePiLoopTM N q) Finset.univ.toList)

def Complexity.SAT.activeQLevelBudget (N : NTM 1) (M : ℕ) : ℕ

Budget of the machine-state unroll: one input-position sweep per state.

Equations

• Complexity.SAT.activeQLevelBudget N M = Fintype.card N.Q * (Complexity.SAT.activePiLoopBudget M + 1) + 1

theorem Complexity.SAT.activeQLevelTM_hoareTime (N : NTM 1) {Qc steps P M t : ℕ} {base : Fin Emit.nT → Tape} (hQc : Qc = Fintype.card N.Q) (hB : ActiveBase Qc steps P M t 0 0 0 base) (haux2 : base Emit.auxReg2 = TM.regTape 0) (hf1 : base Emit.pos1Fuel = TM.regTape (P + 1)) (hf2 : base Emit.pos2Fuel = TM.regTape P) (hf3 : base Emit.pos3Fuel = TM.regTape P) (inp₀ : Tape) (ys : List Bool) (hinp₀ : TM.Parked inp₀) : (activeQLevelTM N).HoareTime (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) ys) (TM.EmitPred inp₀ (TM.scratch base Emit.tmp Emit.tmp2 0) (ys ++ List.flatMap (fun (q : N.Q) => List.flatMap (fun (pi : ℕ) => List.flatMap (fun (si : Γ) => List.flatMap (fun (pw : ℕ) => List.flatMap (fun (sw : Γ) => List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P t q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1))) Finset.univ.toList)) (activeQLevelBudget N M)

activeQLevelTM Hoare specification.

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

The active row body: bump the successor-row register, then the state unroll.

Equations

• Complexity.SAT.activeRowTM N = (Complexity.TM.incRegTM Complexity.SAT.Emit.tPlusReg).seqTM (Complexity.SAT.activeQLevelTM N)

def Complexity.SAT.activeRowBudget (N : NTM 1) (M : ℕ) : ℕ

Budget of the row body: the register bump plus the state unroll.

Equations

• Complexity.SAT.activeRowBudget N M = Complexity.TM.opBudget M + 1 + Complexity.SAT.activeQLevelBudget N M

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

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

Equations

• Complexity.SAT.emitActiveTM N = Complexity.SAT.emitLoopTM (Complexity.SAT.activeRowTM N) Complexity.SAT.Emit.tReg Complexity.SAT.Emit.tFuel

theorem Complexity.SAT.activeRowTM_hoareTime (N : NTM 1) (Qc steps P M i : ℕ) (hQc : Qc = Fintype.card N.Q) (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) (hVp2 : V Emit.pos2Reg = TM.regTape 0) (hVp3 : V Emit.pos3Reg = TM.regTape 0) (hVaux2 : V Emit.auxReg2 = TM.regTape 0) (hVf1 : V Emit.pos1Fuel = TM.regTape (P + 1)) (hVf2 : V Emit.pos2Fuel = TM.regTape P) (hVf3 : V Emit.pos3Fuel = TM.regTape P) : (activeRowTM N).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 (q : N.Q) => List.flatMap (fun (pi : ℕ) => List.flatMap (fun (si : Γ) => List.flatMap (fun (pw : ℕ) => List.flatMap (fun (sw : Γ) => List.flatMap (fun (po : ℕ) => List.flatMap (fun (so : Γ) => List.flatMap (fun (b : Bool) => CNF.encode (Tableau.activeClausesAtF N steps P i q pi si pw sw po so b)) [true, false]) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1))) Tableau.allSyms) (List.range (P + 1))) Finset.univ.toList)) (activeRowBudget N M)

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

theorem Complexity.SAT.emitActiveTM_hoareTime (N : NTM 1) (Qc steps P M : ℕ) (hQc : Qc = Fintype.card N.Q) (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) (hp2 : work₀ Emit.pos2Reg = TM.regTape 0) (hp3 : work₀ Emit.pos3Reg = TM.regTape 0) (haux2 : work₀ Emit.auxReg2 = TM.regTape 0) (hf1 : work₀ Emit.pos1Fuel = TM.regTape (P + 1)) (hf2 : work₀ Emit.pos2Fuel = TM.regTape P) (hf3 : work₀ Emit.pos3Fuel = TM.regTape P) : (emitActiveTM N).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.activeTransitionClausesF N steps P))) (loopBudget M (activeRowBudget N M))

emitActiveTM Hoare specification: appends the encoded active transition family, leaving row counter and successor-row register at steps.