Tape transformations given by equations

TransformsWords tm ws ws' e t s: started on the words ws, the machine tm leaves the words ws' and emits e, within t steps and s work-tape cells. Most specifications of the parts of a composed machine are of this form; for them, sequential composition is a plain chain of words, and adapting a specification to other spellings of the words is rewriting.

Main definitions

• Turing.MultiTapeTM.TransformsWords: tape transformations given by equations.

Main results

• Turing.MultiTapeTM.TransformsTapes.words: a specification read on given words.
• Turing.MultiTapeTM.TransformsWords.seq: sequential composition.

@[reducible, inline]

abbrev Turing.MultiTapeTM.TransformsWords {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (ws ws' : Fin k → List Symbol) (e : List Symbol) (t s : ℕ) : Prop

TransformsWords tm ws ws' e t s: started on the words ws, the machine tm leaves the words ws' and emits e, within t steps and s work-tape cells.

theorem Turing.MultiTapeTM.TransformsTapes.words {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapes P Q t s) {ws ws' : Fin k → List Symbol} {e : List Symbol} (hP : ∀ (input : List Symbol), P input ws) (hQ : ∀ (input : List Symbol) (v : Fin k → List Symbol) (e' : List Symbol), Q input ws v e' → v = ws' ∧ e' = e) : tm.TransformsWords ws ws' e t s

A specification read on given words: the words satisfy the precondition, and the postcondition determines the result.

theorem Turing.MultiTapeTM.TransformsWords.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {ws ws' : Fin k → List Symbol} {e : List Symbol} {t s t' s' : ℕ} (h : tm.TransformsWords ws ws' e t s) (ht : t ≤ t') (hs : s ≤ s') : tm.TransformsWords ws ws' e t' s'

theorem Turing.MultiTapeTM.TransformsWords.congr {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {ws ws' ws₂ ws₂' : Fin k → List Symbol} {e e₂ : List Symbol} {t s : ℕ} (h : tm.TransformsWords ws ws' e t s) (hws : ws₂ = ws) (hws' : ws' = ws₂') (he : e = e₂) : tm.TransformsWords ws₂ ws₂' e₂ t s

Other spellings of the words and of the emitted word.

theorem Turing.MultiTapeTM.TransformsWords.seq {k : ℕ} {Symbol : Type u_1} {State₀ : Type u_3} {State₁ : Type u_4} {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} {ws₀ ws₁ ws₂ : Fin k → List Symbol} {e₀ e₁ : List Symbol} {t₀ s₀ t₁ s₁ : ℕ} (h₀ : tm₀.TransformsWords ws₀ ws₁ e₀ t₀ s₀) (h₁ : tm₁.TransformsWords ws₁ ws₂ e₁ t₁ s₁) : (tm₀.seq tm₁).TransformsWords ws₀ ws₂ (e₀ ++ e₁) (t₀ + t₁) (s₀ + s₁)

Sequential composition: the words left by the first machine are those the second one starts on, and the emitted words are concatenated.