Theorems · Theorem · logic and foundations

Turing.Tape.map_move

∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (T : Turing.Tape Γ) (d : Turing.Dir),
  Turing.Tape.map f (Turing.Tape.move d T) = Turing.Tape.move d (Turing.Tape.map f T)

Defined in

Mathlib.Computability.TuringMachine.Tape

Cited by

1 results in Mathlib

Foundations

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

Assumes

InhabitedInhabited