Push-count table of a situation to Top window of a stack
DefinitionPush-count table of a situation#✓fully proved
Fix an encoding record \(E\) of a finite multi-stack machine. For a situation \(i\) and a stack number \(k\), \(\mathrm{pl}(i, k)\) is the number of symbols that the effect of situation \(i\) has pushed onto the stack that the inverse stack numbering of \(E\) assigns to \(k\) and that are still on top of that stack at the end of the step.
def pl (i k : ℕ) : ℕ := ((E.res i).2.2.1 (E.kd k)).lengthUses 2 · Used by 34
DefinitionConsumption table of a situation#✓fully proved
Fix an encoding record \(E\) of a finite multi-stack machine. For a situation \(i\) and a stack number \(k\), \(\mathrm{cn}(i, k)\) is the number of original symbols that the effect of situation \(i\) consumes from the stack that the inverse stack numbering of \(E\) assigns to \(k\); a symbol pushed and then popped within the same step is not counted.
def cn (i k : ℕ) : ℕ := (E.res i).2.2.2 (E.kd k)Uses 2 · Used by 33
DefinitionPushed-symbol table of a situation#✓fully proved
Fix an encoding record \(E\) of a finite multi-stack machine. For a situation \(i\), a stack number \(k\) and a depth \(j\), \(\mathrm{pu}(i, k, j)\) is the code of the symbol at position \(j\) from the top (counting from \(0\)) among the symbols that the effect of situation \(i\) leaves pushed on the stack that the inverse stack numbering of \(E\) assigns to \(k\), and \(0\) if fewer than \(j + 1\) symbols are left pushed there.
def pu (i k j : ℕ) : ℕ := (((E.res i).2.2.1 (E.kd k))[j]?).elim 0 (E.enc (E.kd k))Uses 2 · Used by 32
TheoremThe symbol-code bound is positive#✓fully proved
For an encoding \(E\) of a finite TM2 machine, the symbol-code bound \(g\) of \(E\) satisfies \(0 < g\).
theorem g_pos : 0 < E.gUses 2 · Used by 13
TheoremSymbols left pushed by a situation are effective#✓fully proved
Let \(E\) be an encoding of a finite multi-stack Turing machine \(M\), and for each stack \(k\) of \(M\) let \(s_k\) be the size of the effective alphabet of stack \(k\) in \(E\) and \(\mathrm{dec}_k(n)\), for \(n < s_k\), its \(n\)-th effective symbol. For every \(i \in \mathbb{N}\), every stack \(k\) of \(M\) and every symbol \(x\) of the alphabet of stack \(k\): if \(x\) is among the symbols that the effect of situation \(i\) leaves pushed on stack \(k\), then \(x = \mathrm{dec}_k(n)\) for some \(n < s_k\).
theorem res_pushed (i : ℕ) (k : M.K) (x : M.Γ k) (hx : x ∈ (E.res i).2.2.1 k) :
∃ n, E.dec k n = xUses 7 · Used by 1
TheoremPushed codes are valid symbol codes#✓fully proved
Fix an encoding record \(E\) of a finite multi-stack machine. Let \(i\) be a situation, \(k\) a stack number, \(s\) the stack that the inverse stack numbering of \(E\) assigns to \(k\), \(n_s\) the size of the effective alphabet of \(s\), and \(j < \mathrm{pl}(i, k)\). Then there is a symbol \(x\) at position \(j\) from the top (counting from \(0\)) among the symbols the effect of situation \(i\) leaves pushed on \(s\), such that \(\mathrm{pu}(i, k, j)\) is the code of \(x\), \(1 \le \mathrm{pu}(i, k, j) \le n_s\), and decoding \(\mathrm{pu}(i, k, j)\) on stack \(s\) gives \(x\).
theorem pu_valid (i k j : ℕ) (hj : j < E.pl i k) :
∃ x, ((E.res i).2.2.1 (E.kd k))[j]? = some x ∧ E.pu i k j = E.enc (E.kd k) x ∧
1 ≤ E.pu i k j ∧ E.pu i k j ≤ E.sz (E.kd k) ∧ E.decO (E.kd k) (E.pu i k j) = some xUses 6 · Used by 2
TheoremThe transition tables of a machine are well formed#✓fully proved
Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(E\) be an encoding of \(M\) with \(A_0\) label/state codes, \(K\) stacks, \(g\) symbol codes and \(N\) situations, and let \(H \ge d\). For every \(i \in \mathbb{N}\), the current-code table \(\mathrm{la}\), the next-code table \(\mathrm{na}\) and the window table \(\mathrm{wa}\) of \(E\) are well formed for the transition clauses of the layout of \(E\) at situation \(i\) and height \(H\): that is, \(\mathrm{la}(i) < A_0 + N\), \(\mathrm{na}(i) < A_0 + N\), \(\mathrm{wa}(i, k, j) < g\) for all \(k < K\) and \(j < d\), and \(d \le H\).
theorem wf_upd {H : ℕ} (hH : depth M ≤ H) (i : ℕ) : Family.WF E.layout E.la E.na E.wa H idef depth (M : FinTM2) : ℕ :=
letI := M.ΛFin
Finset.univ.sup fun l => ops (M.m l)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231
structure WF (H i : ℕ) : Prop where
la_lt : la i < L.A
na_lt : na i < L.A
wa_lt : ∀ k < L.KK, ∀ j < L.d, wa i k j < L.g
d_le : L.d ≤ HCSLibExt/Computability/Complexity/CookLevin/Family.lean:261
Uses 13 · Used by 3
TheoremThe situation-definition tables of a machine are well formed#✓fully proved
Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(E\) be an encoding of \(M\) with \(A_0\) label/state codes, \(K\) stacks, \(g\) symbol codes and \(N\) situations, and let \(H \ge d\). For every situation \(i < N\), the current-code table \(\mathrm{la}\) of \(E\), the table \(\mathrm{sa}(i) = A_0 + i\) as next-code table and the window table \(\mathrm{wa}\) of \(E\) are well formed for the transition clauses of the layout of \(E\) at situation \(i\) and height \(H\): that is, \(\mathrm{la}(i) < A_0 + N\), \(\mathrm{sa}(i) < A_0 + N\), \(\mathrm{wa}(i, k, j) < g\) for all \(k < K\) and \(j < d\), and \(d \le H\).
theorem wf_sdef {H : ℕ} (hH : depth M ≤ H) (i : ℕ) (hi : i < E.N) :
Family.WF E.layout E.la E.sa E.wa H idef depth (M : FinTM2) : ℕ :=
letI := M.ΛFin
Finset.univ.sup fun l => ops (M.m l)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231
structure WF (H i : ℕ) : Prop where
la_lt : la i < L.A
na_lt : na i < L.A
wa_lt : ∀ k < L.KK, ∀ j < L.d, wa i k j < L.g
d_le : L.d ≤ HCSLibExt/Computability/Complexity/CookLevin/Family.lean:261
Uses 12 · Used by 3
TheoremThe cell-shift tables of a machine are well formed#✓fully proved
Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(E\) be an encoding of \(M\) with \(A_0\) label/state codes, \(K\) stacks, \(g\) symbol codes and \(N\) situations, and let \(H \ge d\). Then the table \(\mathrm{sa}(i) = A_0 + i\), the push counts \(\mathrm{pl}\), the consumption counts \(\mathrm{cn}\) and the pushed codes \(\mathrm{pu}\) of \(E\) are well formed for the cell-shift clauses of the layout of \(E\) with \(N\) situations at height \(H\): that is, \(0 < g\), \(d \le H\), \(\mathrm{sa}(i) < A_0 + N\) for all \(i < N\), and for all \(i < N\) and \(k < K\) we have \(\mathrm{pl}(i, k) \le d\), \(\mathrm{cn}(i, k) \le d\) and \(\mathrm{pu}(i, k, j) < g\) for all \(j < \mathrm{pl}(i, k)\).
theorem wf_sh {H : ℕ} (hH : depth M ≤ H) : Shift.WF E.layout E.sa E.pl E.cn E.pu E.N Hdef depth (M : FinTM2) : ℕ :=
letI := M.ΛFin
Finset.univ.sup fun l => ops (M.m l)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231
structure WF (N H : ℕ) : Prop where
g_pos : 0 < L.g
d_le : L.d ≤ H
sa_lt : ∀ i < N, sa i < L.A
pl_le : ∀ i < N, ∀ k < L.KK, pl i k ≤ L.d
cn_le : ∀ i < N, ∀ k < L.KK, cn i k ≤ L.d
pu_lt : ∀ i < N, ∀ k < L.KK, ∀ j < pl i k, pu i k j < L.gCSLibExt/Computability/Complexity/CookLevin/Shift.lean:105
Uses 21 · Used by 3
TheoremHalted situations stay fixed#✓fully proved
If the (label, state) pair decoded from the code \(\mathrm{la}(i)\) of situation \(i\) has no label, so the machine has halted, then for every stack number \(k\) the next code equals the current one, \(\mathrm{na}(i) = \mathrm{la}(i)\), and \(\mathrm{pl}(i, k) = 0\) and \(\mathrm{cn}(i, k) = 0\): nothing is left pushed and nothing is consumed.
theorem halted (i : ℕ) (h : (E.ld (E.la i)).1 = none) (k : ℕ) :
E.na i = E.la i ∧ E.pl i k = 0 ∧ E.cn i k = 0DefinitionMixed-radix number#✓fully proved
For a base \(b\), a top digit \(c\), a length \(m\) and digits \(D : \mathbb{N} \to \mathbb{N}\), \(\mathrm{mix}(b, c, 0, D) = c\) and \(\mathrm{mix}(b, c, m + 1, D) = D(0) + b \cdot \mathrm{mix}(b, c, m, n \mapsto D(n + 1))\); that is, \(D(0) + b\,(D(1) + b\,(\cdots + b\,(D(m - 1) + b\,c)))\), least significant digit first.
def mix (b c : ℕ) : ℕ → (ℕ → ℕ) → ℕ
| 0, _ => c
| m + 1, D => D 0 + b * mix b c m (fun n => D (n + 1))Used by 3
TheoremMixed-radix index of a situation#✓fully proved
Fix an encoding record \(E\) of a finite multi-stack machine \(M\). Let \(K\) be the number of stacks of \(E\), \(d\) the window depth of \(M\), \(A_0\) the number of (label, state) codes of \(E\), \(g\) the symbol-code bound of \(E\) and \(N\) the number of situations. For a code \(c < A_0\) and window contents \(w(k, j)\) with \(w(k, j) < g\) for all \(k < K\) and \(j < d\), let \(i = \mathrm{mix}(g, c, K d, D)\) with digits \(D(n) = w(\lfloor n / d \rfloor, n \bmod d)\). Then \(i < N\), \(\mathrm{la}(i) = c\), and \(\mathrm{wa}(i, k, j) = w(k, j)\) for all \(k < K\) and \(j < d\).
theorem mix_sit (c : ℕ) (hc : c < E.A0) (w : ℕ → ℕ → ℕ)
(hw : ∀ k < E.KK, ∀ j < depth M, w k j < E.g) :
mix E.g c (E.KK * depth M) (fun n => w (n / depth M) (n % depth M)) < E.N ∧
E.la (mix E.g c (E.KK * depth M) (fun n => w (n / depth M) (n % depth M))) = c ∧
∀ k < E.KK, ∀ j < depth M,
E.wa (mix E.g c (E.KK * depth M) (fun n => w (n / depth M) (n % depth M))) k j = w k jdef depth (M : FinTM2) : ℕ :=
letI := M.ΛFin
Finset.univ.sup fun l => ops (M.m l)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231
def mix (b c : ℕ) : ℕ → (ℕ → ℕ) → ℕ
| 0, _ => c
| m + 1, D => D 0 + b * mix b c m (fun n => D (n + 1))CSLibExt/Computability/Complexity/CookLevin/Situation.lean:399
Uses 8 · Used by 2
TheoremSituation surjectivity#✓fully proved
Let \(E\) be an encoding of a finite multi-stack Turing machine \(M\) with \(A_0\) label/state codes, \(K\) stacks, \(g\) symbol codes, window depth \(d\) and \(N\) situations. For every \(c < A_0\) and every \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\) with \(w(k, j) < g\) for all \(k < K\) and \(j < d\), there is a situation \(i < N\) whose label/state code \(\mathrm{la}(i)\) equals \(c\) and whose window codes satisfy \(\mathrm{wa}(i, k, j) = w(k, j)\) for all \(k < K\) and \(j < d\).
theorem sit_surj (c : ℕ) (hc : c < E.A0) (w : ℕ → ℕ → ℕ)
(hw : ∀ k < E.KK, ∀ j < depth M, w k j < E.g) :
∃ i < E.N, E.la i = c ∧ ∀ k < E.KK, ∀ j < depth M, E.wa i k j = w k jdef depth (M : FinTM2) : ℕ :=
letI := M.ΛFin
Finset.univ.sup fun l => ops (M.m l)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231
DefinitionFinite set of pushable symbols#✓fully proved
For a stack \(k\) and a statement tree \(q\) of a multi-stack machine with a finite set of states, the finite set of symbols of stack \(k\) that some push instruction of \(q\) on stack \(k\) pushes for some state: the union, over all push instructions on \(k\) in all branches of \(q\), of the images of their push functions over all states.
noncomputable def pushFS (k : K) : TM2.Stmt Γ Λ σ → Finset (Γ k)
| .push k' f q =>
(if h : k' = k then Finset.univ.image fun v => cast (congrArg Γ h) (f v) else ∅) ∪
pushFS k q
| .peek _ _ q => pushFS k q
| .pop _ _ q => pushFS k q
| .load _ q => pushFS k q
| .branch _ q₁ q₂ => pushFS k q₁ ∪ pushFS k q₂
| .goto _ => ∅
| .halt => ∅DefinitionPushable and input symbols of a stack#✓fully proved
For a finite multi-stack Turing machine \(M\) and a stack \(k\) of \(M\), this is the finite set of symbols of stack \(k\) consisting of every symbol that some push node on stack \(k\) in the statement of some label of \(M\) pushes in some state, together with, when \(k\) is the input stack \(k_0\), every symbol of the alphabet of \(k_0\).
noncomputable def symSet (M : FinTM2) (k : M.K) : Finset (M.Γ k) :=
letI := M.ΛFin; letI := M.σFin; letI := M.Γk₀Fin
(Finset.univ.biUnion fun l => pushFS k (M.m l)) ∪
(if h : M.k₀ = k then Finset.univ.image fun x : M.Γ M.k₀ => cast (congrArg M.Γ h) x else ∅)noncomputable def pushFS (k : K) : TM2.Stmt Γ Λ σ → Finset (Γ k)
| .push k' f q =>
(if h : k' = k then Finset.univ.image fun v => cast (congrArg Γ h) (f v) else ∅) ∪
pushFS k q
| .peek _ _ q => pushFS k q
| .pop _ _ q => pushFS k q
| .load _ q => pushFS k q
| .branch _ q₁ q₂ => pushFS k q₁ ∪ pushFS k q₂
| .goto _ => ∅
| .halt => ∅CSLibExt/Computability/Complexity/CookLevin/Situation.lean:478
DefinitionThe classical encoding record of a finite multi-stack machine#✓fully proved
For every finite multi-stack Turing machine \(M\), an encoding record of \(M\), built with classical choice. If \(M\) has \(K\) stacks, they are numbered \(0, \dots, K - 1\) by a bijection, and numbers \(n \ge K\) decode to the input stack. The pairs of an optional label and a state are numbered \(0, \dots, A_0 - 1\) by a bijection, where \(A_0\) is the number of such pairs, and numbers \(c \ge A_0\) decode to the pair of no label and the initial state. The effective alphabet of stack \(k\) is the finite set of symbols that some statement of \(M\) can push on \(k\), together with the whole input alphabet when \(k\) is the input stack; its \(s_k\) elements are listed by a bijection with \(\{0, \dots, s_k - 1\}\), a symbol in it gets code its position in that list plus \(1\), and a symbol outside it gets code \(0\).
Only the existence of this record is used later.
Cslib.Complexity.CookLevin.Situation.Enc.ofFinTM2 · 21 lines
noncomputable def Enc.ofFinTM2 (M : FinTM2) : Enc M :=
letI := M.kFin; letI := M.ΛFin; letI := M.σFin
{ KK := Fintype.card M.K
kc := fun k => Fintype.equivFin M.K k
kd := fun n => if h : n < Fintype.card M.K then (Fintype.equivFin M.K).symm ⟨n, h⟩ else M.k₀
kc_lt := fun k => (Fintype.equivFin M.K k).2
kd_kc := fun k => by simp
kc_kd := fun n hn => by simp [hn]
A0 := Fintype.card (Option M.Λ × M.σ)
lc := fun x => Fintype.equivFin _ x
ld := fun c => if h : c < Fintype.card (Option M.Λ × M.σ) then
(Fintype.equivFin _).symm ⟨c, h⟩ else (none, M.initialState)
lc_lt := fun x => (Fintype.equivFin _ x).2
ld_lc := fun x => by rw [dite_eq_left (Fintype.equivFin _ x).2]; simp
lc_ld := fun c hc => by rw [dite_eq_left hc]; simp
sz := fun k => (symSet M k).card
dec := fun k i => ((symSet M k).equivFin.symm i).1
enc := fun k x => if h : x ∈ symSet M k then (symSet M k).equivFin ⟨x, h⟩ + 1 else 0
enc_dec := fun k i => by simp
push_mem := fun l k x h => ⟨(symSet M k).equivFin ⟨x, push_mem_symSet M l k x h⟩, by simp⟩
input_mem := fun x => ⟨(symSet M M.k₀).equivFin ⟨x, input_mem_symSet M x⟩, by simp⟩ }structure Enc (M : FinTM2) where
/-- Number of stacks. -/
KK : ℕ
/-- Stack numbering. -/
kc : M.K → ℕ
/-- Inverse of the stack numbering. -/
kd : ℕ → M.K
kc_lt : ∀ k, kc k < KK
kd_kc : ∀ k, kd (kc k) = k
kc_kd : ∀ n < KK, kc (kd n) = n
/-- Number of (label, state) codes. -/
A0 : ℕ
⋯CSLibExt/Computability/Complexity/CookLevin/Situation.lean:201
TheoremTime bound of the transition-clause generator on the tables of a machine#✓fully proved
Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(E\) be an encoding of \(M\) with \(N\) situations, and let \(H \ge d\) and \(T \in \mathbb{N}\). Run the transition-clause generator for the layout of \(E\), the current-code table \(\mathrm{la}\), the next-code table \(\mathrm{na}\) and the window table \(\mathrm{wa}\) of \(E\) and \(N\) situations, started at its first precomputation stage, in state false, with \(T\) on the time counter and \(H\) on the height counter in unary, all other counters empty, and an arbitrary list \(o\) of bits on the output stack. Then within \(c\,(T + H + 1)^5\) steps, where \(c\) is the constant of the generator's time bound for this layout and \(N\), it reaches its final label \(\mathsf{done}\), in some state, with stacks whose output stack holds the encoding of the transition clause family for this layout, \(\mathrm{la}\), \(\mathrm{na}\), \(\mathrm{wa}\), \(T\), \(H\) and \(N\), followed by \(o\).
theorem upd_time (T : ℕ) (o : List Bool) :
∃ (v : Bool) (S : ∀ k, List (GΓ k)),
TM2Program.RunLe (prog E.layout E.la E.na E.wa E.N) (genC E.layout E.N * (T + H + 1) ^ 5)
⟨some (.pre .eg), false, st (initF T H) o⟩ ⟨some .done, v, S⟩ ∧
S .out = DenseSAT.encodeCNF (family E.layout E.la E.na E.wa T H E.N) ++ oabbrev GΓ := SΓ CKCSLibExt/Computability/Complexity/CookLevin/Family.lean:360
def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
∃ n, n ≤ B ∧ Run M n c dMathlibExt/Computability/TuringMachine/Program.lean:901
def prog : GL N L.nLits → TM2.Stmt GΓ (GL N L.nLits) Bool
| .pre .eg => emitR (.c .Gc) (List.replicate L.g ()) (.pre (.hg .head))
| .pre (.hg s) => mulS .Hs .md .Gc .HG .tmp (fun s => .pre (.hg s)) (.pre .ew) s
| .pre .ew => emitR (.c .Wc) (List.replicate L.A ()) (.pre .ek)
| .pre .ek => emitR (.c .Ka) (List.replicate L.KK ()) (.pre (.w .head))
| .pre (.w s) => mulS .Ka .md .HG .Wc .tmp (fun s => .pre (.w s)) (.pre .dk) s
| .pre .dk => xfer (.c .Ka) [] (.pre .dk) (.pre .cp1)
| .pre .cp1 => xfer (.c .Tn) [⟨.c .Ka, ()⟩, ⟨.c .tmp, ()⟩] (.pre .cp1) (.pre .cp2)
| .pre .cp2 => xfer (.c .tmp) [⟨.c .Tn, ()⟩] (.pre .cp2) (.pre .inc)
| .pre .inc => incr (.c .Ka) () (.pre (.v .head))
| .pre (.v s) => mulS .Ka .md .Wc .Vc .tmp (fun s => .pre (.v s)) (.pre .dk2) s
| .pre .dk2 => xfer (.c .Ka) [] (.pre .dk2) .tHead
⋯CSLibExt/Computability/Complexity/CookLevin/Family.lean:448
def genC (L : Layout) (N : ℕ) : ℕ := 323 * (L.A + L.KK + L.g + L.d + N + 1) ^ 5CSLibExt/Computability/Complexity/CookLevin/Family.lean:1051
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)CSLibExt/Computability/Complexity/CookLevin/CounterView.lean:72
def initF (T H : ℕ) : CK → ℕ
| .Tn => T
| .Hs => H
| _ => 0CSLibExt/Computability/Complexity/CookLevin/Family.lean:912
def encodeCNF (φ : CNF) : List Bool := φ.flatMap encodeClauseCSLibExt/Computability/Complexity/DenseSAT.lean:90
def family (T H N : ℕ) : CNF :=
(List.range T).flatMap fun t =>
(List.range N).map fun i => denseClause (L.numVars T H) (lits L la na wa H t i)CSLibExt/Computability/Complexity/CookLevin/Family.lean:132
Uses 22 · Used by 1
TheoremTime bound of the situation-definition generator on the tables of a machine#✓fully proved
Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(E\) be an encoding of \(M\) with \(A_0\) label/state codes and \(N\) situations, and let \(H \ge d\) and \(T \in \mathbb{N}\). Run the transition-clause generator for the layout of \(E\), the current-code table \(\mathrm{la}\) of \(E\), the table \(\mathrm{sa}(i) = A_0 + i\) (the position of the variable of situation \(i\)) in place of the next-code table, the window table \(\mathrm{wa}\) of \(E\) and \(N\) situations, started at its first precomputation stage, in state false, with \(T\) on the time counter and \(H\) on the height counter in unary, all other counters empty, and an arbitrary list \(o\) of bits on the output stack. Then within \(c\,(T + H + 1)^5\) steps, where \(c\) is the constant of the generator's time bound for this layout and \(N\), it reaches its final label \(\mathsf{done}\), in some state, with stacks whose output stack holds the encoding of the transition clause family for this layout, \(\mathrm{la}\), \(\mathrm{sa}\), \(\mathrm{wa}\), \(T\), \(H\) and \(N\), followed by \(o\).
theorem sdef_time (T : ℕ) (o : List Bool) :
∃ (v : Bool) (S : ∀ k, List (GΓ k)),
TM2Program.RunLe (prog E.layout E.la E.sa E.wa E.N) (genC E.layout E.N * (T + H + 1) ^ 5)
⟨some (.pre .eg), false, st (initF T H) o⟩ ⟨some .done, v, S⟩ ∧
S .out = DenseSAT.encodeCNF (family E.layout E.la E.sa E.wa T H E.N) ++ oabbrev GΓ := SΓ CKCSLibExt/Computability/Complexity/CookLevin/Family.lean:360
def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
∃ n, n ≤ B ∧ Run M n c dMathlibExt/Computability/TuringMachine/Program.lean:901
def prog : GL N L.nLits → TM2.Stmt GΓ (GL N L.nLits) Bool
| .pre .eg => emitR (.c .Gc) (List.replicate L.g ()) (.pre (.hg .head))
| .pre (.hg s) => mulS .Hs .md .Gc .HG .tmp (fun s => .pre (.hg s)) (.pre .ew) s
| .pre .ew => emitR (.c .Wc) (List.replicate L.A ()) (.pre .ek)
| .pre .ek => emitR (.c .Ka) (List.replicate L.KK ()) (.pre (.w .head))
| .pre (.w s) => mulS .Ka .md .HG .Wc .tmp (fun s => .pre (.w s)) (.pre .dk) s
| .pre .dk => xfer (.c .Ka) [] (.pre .dk) (.pre .cp1)
| .pre .cp1 => xfer (.c .Tn) [⟨.c .Ka, ()⟩, ⟨.c .tmp, ()⟩] (.pre .cp1) (.pre .cp2)
| .pre .cp2 => xfer (.c .tmp) [⟨.c .Tn, ()⟩] (.pre .cp2) (.pre .inc)
| .pre .inc => incr (.c .Ka) () (.pre (.v .head))
| .pre (.v s) => mulS .Ka .md .Wc .Vc .tmp (fun s => .pre (.v s)) (.pre .dk2) s
| .pre .dk2 => xfer (.c .Ka) [] (.pre .dk2) .tHead
⋯CSLibExt/Computability/Complexity/CookLevin/Family.lean:448
def genC (L : Layout) (N : ℕ) : ℕ := 323 * (L.A + L.KK + L.g + L.d + N + 1) ^ 5CSLibExt/Computability/Complexity/CookLevin/Family.lean:1051
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)CSLibExt/Computability/Complexity/CookLevin/CounterView.lean:72
def initF (T H : ℕ) : CK → ℕ
| .Tn => T
| .Hs => H
| _ => 0CSLibExt/Computability/Complexity/CookLevin/Family.lean:912
def encodeCNF (φ : CNF) : List Bool := φ.flatMap encodeClauseCSLibExt/Computability/Complexity/DenseSAT.lean:90
def family (T H N : ℕ) : CNF :=
(List.range T).flatMap fun t =>
(List.range N).map fun i => denseClause (L.numVars T H) (lits L la na wa H t i)CSLibExt/Computability/Complexity/CookLevin/Family.lean:132
Uses 22 · Used by 1
TheoremTime bound of the shift generator on the tables of a machine#✓fully proved
Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(E\) be an encoding of \(M\) with \(A_0\) label/state codes and \(N\) situations, and let \(H \ge d\) and \(T \in \mathbb{N}\). Run the cell-shift generator for the layout of \(E\), the table \(\mathrm{sa}(i) = A_0 + i\) (the position of the variable of situation \(i\)), the push counts \(\mathrm{pl}\), the consumption counts \(\mathrm{cn}\) and the pushed codes \(\mathrm{pu}\) of \(E\) and \(N\) situations, started at its first precomputation stage, in state false, with \(T\) on the time counter and \(H\) on the height counter in unary, all other counters empty, and an arbitrary list \(o\) of bits on the output stack. Then within \(c\,(T + H + 1)^6\) steps, where \(c\) is the constant of the shift-generator time bound for this layout and \(N\), it reaches its final label \(\mathsf{done}\), in some state, with stacks whose output stack holds the encoding of the cell-shift clause family for this layout, \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\), \(N\), \(T\) and \(H\), followed by \(o\).
theorem shift_time (T : ℕ) (o : List Bool) :
∃ (v : Bool) (S : ∀ k, List (SΓ Shift.CK k)),
TM2Program.RunLe (Shift.prog E.layout E.sa E.pl E.cn E.pu E.N) (shC E.layout E.N * (T + H + 1) ^ 6)
⟨some (.pre .eg), false, CounterView.st (Shift.initF T H) o⟩ ⟨some .done, v, S⟩ ∧
S .out = DenseSAT.encodeCNF (shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) ++ oabbrev SΓ (C : Type) : SK C → Type
| .out => Bool
| .c _ => UnitCSLibExt/Computability/Complexity/CookLevin/CounterView.lean:63
inductive CK
| Tn | Ti | Hs | Gc | HG | Wc | Vc | TW | TW1 | KB | U | Ui | R | Ri | CB | CW | P | Q | tmp | md | Ka
| c1 | c2
deriving DecidableEqCSLibExt/Computability/Complexity/CookLevin/Shift.lean:136
def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
∃ n, n ≤ B ∧ Run M n c dMathlibExt/Computability/TuringMachine/Program.lean:901
def prog : Lab L N → TM2.Stmt (SΓ CK) (Lab L N) Bool
| .pre .eg => emitR (.c .Gc) (List.replicate L.g ()) (.pre (.hg .head))
| .pre (.hg s) => mulS .Hs .md .Gc .HG .tmp (fun s => .pre (.hg s)) (.pre .ew) s
| .pre .ew => emitR (.c .Wc) (List.replicate L.A ()) (.pre .ek)
| .pre .ek => emitR (.c .Ka) (List.replicate L.KK ()) (.pre (.w .head))
| .pre (.w s) => mulS .Ka .md .HG .Wc .tmp (fun s => .pre (.w s)) (.pre .dk) s
| .pre .dk => xfer (.c .Ka) [] (.pre .dk) (.pre (.v .head))
| .pre (.v s) => mulS .Tn .md .Wc .Vc .tmp (fun s => .pre (.v s)) (.pre .vw1) s
| .pre .vw1 => xfer (.c .Wc) [⟨.c .Vc, ()⟩, ⟨.c .tmp, ()⟩] (.pre .vw1) (.pre .vw2)
| .pre .vw2 => xfer (.c .tmp) [⟨.c .Wc, ()⟩] (.pre .vw2) .tHead
| .tHead => forHead (.c .Tn) (.c .Ti) () (.tw .head) .tRest
| .tRest => xfer (.c .Ti) [⟨.c .Tn, ()⟩] .tRest .done
⋯CSLibExt/Computability/Complexity/CookLevin/Shift.lean:389
def shC (L : Layout) (N : ℕ) : ℕ := 828 * (L.A + L.KK + L.g + L.d + N + 1) ^ 7CSLibExt/Computability/Complexity/CookLevin/Shift.lean:1380
def st (f : C → ℕ) (o : List Bool) : ∀ k, List (SΓ C k)
| .out => o
| .c x => cnt () (f x)CSLibExt/Computability/Complexity/CookLevin/CounterView.lean:72
def initF (T H : ℕ) : CK → ℕ
| .Tn => T
| .Hs => H
| _ => 0CSLibExt/Computability/Complexity/CookLevin/Shift.lean:1251
def encodeCNF (φ : CNF) : List Bool := φ.flatMap encodeClauseCSLibExt/Computability/Complexity/DenseSAT.lean:90
def shFamily (N T H : ℕ) : CNF :=
(List.range T).flatMap fun t => (List.range N).flatMap fun i =>
(List.range L.KK).flatMap fun k => shBlk L sa pl cn pu T H t i kCSLibExt/Computability/Complexity/CookLevin/Shift.lean:100
Uses 24 · Used by 1
DefinitionTop window of a stack#✓fully proved
For \(d \in \mathbb{N}\) and a list \(L = [x_0, x_1, \dots]\) over a type \(\alpha\) (a stack, top first), the window of depth \(d\) of \(L\) is the list of length \(d\) over \(\alpha\) extended by the empty cell \(\bot\) whose entry \(j\) is \(x_j\) if \(j\) is less than the length of \(L\) and \(\bot\) otherwise.
def window {α : Type} (d : ℕ) (L : List α) : List (Option α) :=
(List.range d).map fun j => L[j]?Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.