{K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        {motive : Turing.TM2.Stmt Γ Λ σ → Sort u} →
          (t : Turing.TM2.Stmt Γ Λ σ) →
            ((k : K) → (a : σ → Γ k) → (a_1 : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a a_1)) →
              ((k : K) →
                  (a : σ → Option (Γ k) → σ) → (a_1 : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a a_1)) →
                ((k : K) →
                    (a : σ → Option (Γ k) → σ) → (a_1 : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a a_1)) →
                  ((a : σ → σ) → (a_1 : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a a_1)) →
                    ((a : σ → Bool) → (a_1 a_2 : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a a_1 a_2)) →
                      ((a : σ → Λ) → motive (Turing.TM2.Stmt.goto a)) → motive Turing.TM2.Stmt.halt → motive t