Data.JSON

First-order whitespace drop. The previous definition folded a FUNCTION accumulator (`pi input . Bytes`) and, inside each step, ran `bytes-eliminate` over the input. The runtime-graph evaluator forces a fold's induction (and a `bytes-eliminate`'s ignored tail-result) EAGERLY, so composing the two symbolically re-walked every suffix at every fuel level -- an exponential blow-up. This version folds a FIRST-ORDER value accumulator (the current byte string) with the O(1) native views `bytes-head` / `bytes-tail`: at each step it either peels one leading whitespace byte or keeps the string (idempotent once a non-whitespace byte is reached). `bytes-head` of the empty string is byte 0, which is not whitespace, so the empty input is a fixed point. The surviving bytes are identical to the original; only the cost changed.

323def jsonDropWhitespaceWithFuel =
324  (lambda unrestricted fuel : Nat .
325    (lambda unrestricted input : Bytes .
326      (nat-eliminate
327        (lambda unrestricted current : Nat . Bytes)
328        input
329        (lambda unrestricted predecessor : Nat .
330          (lambda unrestricted induction : Bytes .
331            (nat-eliminate
332              (lambda unrestricted whitespace : Nat . Bytes)
333              induction
334              (lambda unrestricted whitespacePredecessor : Nat .
335                (lambda unrestricted whitespaceInduction : Bytes . (bytes-tail induction)))
336              (jsonByteIsWhitespace (bytes-head induction)))))
337        fuel)))