Method try_reduce_bitvec_lt_prop

crates/kernel/src/whnf.rs:2537–2558

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

    }
    if !self.is_nat_succ_ih_step(step)? {
      return Ok(None);
    }

    let base = base.clone();
    let base_whnf = self.whnf(&base)?;
    let Some(base_val) = extract_nat_value(&base_whnf, &self.prims) else {
      // Symbolic base: collapse `succ^offset(Nat.rec base succ-step (Lit n))`
      // to the compact offset `Nat.add base (Lit (n + offset))` rather than
      // declining into n iota steps that materialize succ^n(base). Keeps the
      // value in the same `base + k` form a literal already has, so def-eq
      // converges instead of descending n unary succ layers. Conservative:
      // only when the recursor application carries no post-major arguments.
      // Mirrors IxVM dbc4177.
      if parts.spine.len() != parts.major_idx + 1 {
        return Ok(None);
      }
      let total = Nat(&parts.major.0 + offset);
      let lit = self.nat_expr_from_value(total);
      let result = self.mk_nat_add(base_whnf, lit);
      return Ok(Some(result));
    };

    let mut total = base_val.0;
    total += parts.major.0;
    total += offset;