Theorems · Definition · logic and foundations

Turing.TM2to1.TrCfg.casesOn

∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4}
  {motive :
    (a : Turing.TM2.Cfg Γ Λ σ) →
      (a_1 : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) → Turing.TM2to1.TrCfg a a_1 → Prop}
  {a : Turing.TM2.Cfg Γ Λ σ} {a_1 : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ}
  (t : Turing.TM2to1.TrCfg a a_1),
  (∀ {q : Option Λ} {v : σ} {S : (k : K) → List (Γ k)} (L : Turing.ListBlank ((k : K) → Option (Γ k)))
      (a : ∀ (k : K), Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some (S k)).reverse),
      motive { l := q, var := v, stk := S }
        { l := Option.map Turing.TM2to1.Λ'.normal q, var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
        ⋯) →
    motive a a_1 t

Defined in

Mathlib.Computability.TuringMachine.StackTuringMachine

Cited by

2 results in Mathlib

Foundations

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