Theorems · Theorem · logic and foundations

Turing.TM1to1.tr_supports

∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ)
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst : Fintype Γ] [inst_1 : Inhabited Λ] {S : Finset Λ},
  Turing.TM1.Supports M S → Turing.TM1.Supports (Turing.TM1to1.tr enc dec M) (Turing.TM1to1.trSupp M S)

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeInhabited