Theorems · Theorem · logic and foundations

Turing.TM1to1.trTape.congr_simp

∀ {Γ : Type u_1} {n : ℕ} {enc enc_1 : Γ → List.Vector Bool n} (e_enc : enc = enc_1) [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (T T_1 : Turing.Tape Γ),
  T = T_1 → Turing.TM1to1.trTape enc0 T = Turing.TM1to1.trTape ⋯ T_1

Defined in: Mathlib.Computability.TuringMachine.PostTuringMachine
Cited by: 0 results in Mathlib
Foundations: Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Inhabited

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

List.Vectorstatement and proof · cited by 270
Turing.Tapestatement and proof · cited by 50
List.Vector.replicatestatement and proof · cited by 14
Turing.TM1to1.trTapestatement and proof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.