{motive : Turing.PartrecToTM2.Cont' → Sort u} →
  (t : Turing.PartrecToTM2.Cont') →
    motive Turing.PartrecToTM2.Cont'.halt →
      ((a : Turing.ToPartrec.Code) →
          (a_1 : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ a a_1)) →
        ((a : Turing.PartrecToTM2.Cont') → motive a.cons₂) →
          ((a : Turing.ToPartrec.Code) →
              (a_1 : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp a a_1)) →
            ((a : Turing.ToPartrec.Code) →
                (a_1 : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix a a_1)) →
              motive t