(motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) →
  (x : Std.Tactic.BVDecide.BVUnOp) →
    (Unit → motive Std.Tactic.BVDecide.BVUnOp.not) →
      ((a : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft a)) →
        ((a : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight a)) →
          ((a : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst a)) →
            (Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) →
              (Unit → motive Std.Tactic.BVDecide.BVUnOp.clz) → motive x