Theorems · Theorem · logic and foundations

Turing.TM0.map_init

∀ {Γ : Type u_1} [inst : Inhabited Γ] {Γ' : Type u_2} [inst_1 : Inhabited Γ'] {Λ : Type u_3} [inst_2 : Inhabited Λ]
  {Λ' : Type u_4} [inst_3 : Inhabited Λ'] (f₁ : Turing.PointedMap Γ Γ') (g₁ : Turing.PointedMap Λ Λ') (l : List Γ),
  Turing.TM0.Cfg.map f₁ g₁.f (Turing.TM0.init l) = Turing.TM0.init (List.map f₁.f l)

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

InhabitedInhabitedInhabitedInhabited