Input-tape lookups

Lemmas for reading Turing.inputAt. Position 0 is the left end cell and position q + 1 holds x[q], so the lookup is blank exactly at 0 and beyond x.length.

Main results

• Turing.inputAt_zero, Turing.inputAt_succ: the lookup at the left end cell and at a data cell.
• Turing.inputAt_eq_none_iff, Turing.inputAt_eq_some_iff: when the lookup is blank, and which symbols it reads.

@[simp]

theorem Turing.inputAt_zero {Symbol : Type u_1} (x : List Symbol) : inputAt x 0 = none

Position 0 is the blank left end cell.

@[simp]

theorem Turing.inputAt_succ {Symbol : Type u_1} (x : List Symbol) (q : ℕ) : inputAt x (q + 1) = x[q]?

Position q + 1 holds the q-th input symbol.

theorem Turing.inputAt_eq_none_iff {Symbol : Type u_1} (x : List Symbol) (j : ℕ) : inputAt x j = none ↔ j = 0 ∨ x.length < j

The input tape is blank at the left end cell and beyond the input.

theorem Turing.inputAt_eq_some_iff {Symbol : Type u_1} (x : List Symbol) {s : Symbol} (j : ℕ) : inputAt x j = some s ↔ ∃ (q : ℕ), j = q + 1 ∧ x[q]? = some s

The input tape holds s at j exactly when j = q + 1 with x[q] = s.