{Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) →
        (x : Turing.TM1.Stmt Γ Λ σ) →
          ((Q : Turing.TM1.Stmt Γ Λ σ) →
              (a : Turing.Dir) →
                (q : Turing.TM1.Stmt Γ Λ σ) →
                  (h : Q = Turing.TM1.Stmt.move a q) → motive (namedPattern Q (Turing.TM1.Stmt.move a q) h)) →
            ((Q : Turing.TM1.Stmt Γ Λ σ) →
                (a : Γ → σ → Γ) →
                  (q : Turing.TM1.Stmt Γ Λ σ) →
                    (h : Q = Turing.TM1.Stmt.write a q) → motive (namedPattern Q (Turing.TM1.Stmt.write a q) h)) →
              ((Q : Turing.TM1.Stmt Γ Λ σ) →
                  (a : Γ → σ → σ) →
                    (q : Turing.TM1.Stmt Γ Λ σ) →
                      (h : Q = Turing.TM1.Stmt.load a q) → motive (namedPattern Q (Turing.TM1.Stmt.load a q) h)) →
                ((Q : Turing.TM1.Stmt Γ Λ σ) →
                    (a : Γ → σ → Bool) →
                      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) →
                        (h : Q = Turing.TM1.Stmt.branch a q₁ q₂) →
                          motive (namedPattern Q (Turing.TM1.Stmt.branch a q₁ q₂) h)) →
                  ((Q : Turing.TM1.Stmt Γ Λ σ) → motive Q) → motive x