Theorems · Theorem · logic and foundations

Turing.TM2to1.addBottom_modifyNth

∀ {K : Type u_1} {Γ : K → Type u_2} (f : ((k : K) → Option (Γ k)) → (k : K) → Option (Γ k))
  (L : Turing.ListBlank ((k : K) → Option (Γ k))) (n : ℕ),
  Turing.ListBlank.modifyNth (fun a => (a.1, f a.2)) n (Turing.TM2to1.addBottom L) =
    Turing.TM2to1.addBottom (Turing.ListBlank.modifyNth f n L)

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

1 results in Mathlib

Foundations

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