Method cleanup_nat_offset_major

crates/kernel/src/whnf.rs:1125–1147

Lean's `cleanupNatOffsetMajor` for recursor reduction. If the major premise is definitionally an offset `base + k` with `k > 0`, expose exactly one constructor layer as `Nat.succ (base + (k-1))`. This prevents `Nat.rec ... (x + huge)` from delta-unfolding `Nat.add` and allocating one intermediate literal per predecessor. Closed Nat arithmetic is left alone so the primitive Nat reducer can compute

(
    &mut self,
    e: &KExpr<M>,
  )

      // and may leave the Prj head stuck; `try_proj_app_reduce` gives it
      // one more attempt with the same projection policy.
      if let Some((proj_result, args)) =
        self.try_proj_app_reduce(&cur, flags)?
      {
        let mut result = proj_result;
        for arg in &args {
          result = self.intern(KExpr::app(result, arg.clone()));
        }
        cur = result;
        continue;
      }

      // Primitive reduction, dispatched by memoized head family (see the
      // main WHNF loop) — family head sets are disjoint, so dispatching
      // replaces probe-everything without changing semantics.
      let family = self.head_prim_family(&cur);

      // BitVec.toNat/ult reductions are definitional wrappers around Nat.
      if family == PrimFamily::BitVec
        && let Some(reduced) = self.try_reduce_bitvec(&cur)?
      {
        cur = reduced;
        continue;
      }

      // Nat primitive reduction
      if family == PrimFamily::Nat