The size of the simulated configurations

After j steps, the configuration of the simulation is bounded in the length of the encoded description, the length of the input and j: the state and all symbols on the work tapes and the output are numbers from the description, the input head stays on the input, every head moves by at most one cell per step, and every zipper grows by at most two cells per step.

Main definitions

• Turing.MultiTapeTM.Universal.cfgBound: the bound on the configurations.
• Turing.MultiTapeTM.Universal.stepBound: Turing.MultiTapeTM.Universal.stepTime at the largest sizes the invariant allows.

Main results

• Turing.MultiTapeTM.Universal.length_eCfg_iterate_le: the size of the configuration after j steps.
• Turing.MultiTapeTM.Universal.stepTime_iterate_le: the time of the step after j steps.

Numbers in the description

theorem Turing.MultiTapeTM.Universal.length_eSym_le {o : Option ℕ} {b : ℕ} (h : o.getD 0 ≤ b) : (eSym o).length ≤ b + 1

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.descLen (d : Desc) : ℕ

The length of the encoded description, which bounds all numbers in it.

The invariant

structure Turing.MultiTapeTM.Universal.TapeInv (D j : ℕ) (t : Tape) : Prop

A work tape after at most j steps, with symbols at most D: the head is within [-j, j] and the zipper holds at most 2 * j cells.

• head : t.head.natAbs ≤ j
• length : t.left.length + t.right.length ≤ 2 * j
• val (o : Option ℕ) : o ∈ t.left ++ t.right → o.getD 0 ≤ D

structure Turing.MultiTapeTM.Universal.Inv (D X j : ℕ) (c : SCfg) : Prop

A configuration after at most j steps, for a description of length D and an input of length X.

• state : c.state.getD 0 ≤ D
• inputPos : c.inputPos ≤ X + 1
• tapes : c.workTapes.length ≤ D
• workTapes (t : Tape) : t ∈ c.workTapes → TapeInv D j t

theorem Turing.MultiTapeTM.Universal.length_applyTapes_eq (ts : List Tape) (as : List TapeAct) : (applyTapes ts as).length = ts.length

theorem Turing.MultiTapeTM.Universal.inv_iterate (d : Desc) (x : List ℕ) (j : ℕ) : Inv (descLen d) x.length j ((stepOut d x)^[j] (init d, [])).1 ∧ ((stepOut d x)^[j] (init d, [])).2.length ≤ j ∧ ∀ o ∈ ((stepOut d x)^[j] (init d, [])).2, o ≤ descLen d

The configuration and the output after j steps.

The size bound

theorem Turing.MultiTapeTM.Universal.length_encInt_le (z : ℤ) : (encInt z).length ≤ z.natAbs + 1

theorem Turing.MultiTapeTM.Universal.length_encNat_le (n : ℕ) : (encNat n).length ≤ n

theorem Turing.MultiTapeTM.Universal.length_cells_le {D : ℕ} {l : List (Option ℕ)} (h : ∀ o ∈ l, o.getD 0 ≤ D) : ((encList eSym) l).length ≤ l.length * (2 * D + 3)

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.tapeBound (D j : ℕ) : ℕ

The bound on the encoded work tapes.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.cfgBound (D X j : ℕ) : ℕ

The bound on the encoded configurations, after j steps.

theorem Turing.MultiTapeTM.Universal.length_eCfg_iterate_le (d : Desc) (x : List ℕ) (j : ℕ) : (eCfg ((stepOut d x)^[j] (init d, [])).1).length ≤ cfgBound (descLen d) x.length j

The size of the simulated configurations after j steps.

The time of a step

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.ctxBound (D N j : ℕ) : ℕ

The bound on the context of a step after j steps, for a description of length D and an input of encoded length N.

def Turing.MultiTapeTM.Universal.stepBound (D N j : ℕ) : ℕ

The bound on the time of a step after j steps, for a description of length D and an input of encoded length N: Turing.MultiTapeTM.Universal.stepTime at the largest sizes the invariant allows.

theorem Turing.MultiTapeTM.Universal.stepBound_mono {D N j D' N' j' : ℕ} (hD : D ≤ D') (hN : N ≤ N') (hj : j ≤ j') : stepBound D N j ≤ stepBound D' N' j'

theorem Turing.MultiTapeTM.Universal.length_eCtx_le (d : Desc) (x : List ℕ) {j : ℕ} {c : SCfg} (h : Inv (descLen d) x.length j c) : (eCtx ((d, x), c)).length ≤ ctxBound (descLen d) ((encList encUnary) x).length j

theorem Turing.MultiTapeTM.Universal.stepTime_iterate_le (d : Desc) (x : List ℕ) (j : ℕ) : stepTime ((d, x), ((stepOut d x)^[j] (init d, [])).1) ≤ stepBound (descLen d) ((encList encUnary) x).length j

The time of a step after j steps, in the length of the description, the length of the encoded input and j.