Theorems · Theorem · logic and foundations

Turing.TM1.SupportsStmt.eq_def

∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (x : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.SupportsStmt S x =
    match x with
    | Turing.TM1.Stmt.move a q => Turing.TM1.SupportsStmt S q
    | Turing.TM1.Stmt.write a q => Turing.TM1.SupportsStmt S q
    | Turing.TM1.Stmt.load a q => Turing.TM1.SupportsStmt S q
    | Turing.TM1.Stmt.branch a q₁ q₂ => Turing.TM1.SupportsStmt S q₁ ∧ Turing.TM1.SupportsStmt S q₂
    | Turing.TM1.Stmt.goto l => ∀ (a : Γ) (v : σ), l a v ∈ S
    | Turing.TM1.Stmt.halt => True

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

1 results in Mathlib

Foundations

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