Called only after proving remaining > 0. Borrow visits at most four bytes;
it never runs bitwise XOR to subtract a single unit.
295def normalizationWordPredecessor =
296 (lambda unrestricted word : (family ModelWord32) .
297 (eliminate
298 ModelWord32
299 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
300 word
301 (branch
302 ModelWord32Value
303 b0
304 b1
305 b2
306 b3
307 .
308 (normalizationWordChoose
309 (byte-equal b0 (byte 0))
310 (lambda unrestricted force : Nat .
311 (normalizationWordChoose
312 (byte-equal b1 (byte 0))
313 (lambda unrestricted force : Nat .
314 (normalizationWordChoose
315 (byte-equal b2 (byte 0))
316 (lambda unrestricted force : Nat .
317 (constructor
318 ModelWord32
319 ModelWord32Value
320 (byte 255)
321 (byte 255)
322 (byte 255)
323 (normalizationBytePredecessor b3)))
324 (lambda unrestricted force : Nat .
325 (constructor
326 ModelWord32
327 ModelWord32Value
328 (byte 255)
329 (byte 255)
330 (normalizationBytePredecessor b2)
331 b3))))
332 (lambda unrestricted force : Nat .
333 (constructor
334 ModelWord32
335 ModelWord32Value
336 (byte 255)
337 (normalizationBytePredecessor b1)
338 b2
339 b3))))
340 (lambda unrestricted force : Nat .
341 (constructor ModelWord32 ModelWord32Value (normalizationBytePredecessor b0) b1 b2 b3))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.