324def x86NativeIncrementUnsigned32Wrapping :
325 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeUnsigned32)) =
326 (lambda unrestricted value : (family X86NativeUnsigned32) .
327 (eliminate
328 X86NativeUnsigned32
329 (lambda unrestricted current : (family X86NativeUnsigned32) . (family X86NativeUnsigned32))
330 value
331 (branch
332 X86NativeUnsigned32Value
333 byte0
334 byte1
335 byte2
336 byte3
337 .
338 (nat-eliminate
339 (lambda unrestricted carry0 : Nat . (family X86NativeUnsigned32))
340 (constructor
341 X86NativeUnsigned32
342 X86NativeUnsigned32Value
343 (x86NativeIncrementByte byte0)
344 byte1
345 byte2
346 byte3)
347 (lambda unrestricted predecessor0 : Nat .
348 (lambda unrestricted induction0 : (family X86NativeUnsigned32) .
349 (nat-eliminate
350 (lambda unrestricted carry1 : Nat . (family X86NativeUnsigned32))
351 (constructor
352 X86NativeUnsigned32
353 X86NativeUnsigned32Value
354 (byte 0)
355 (x86NativeIncrementByte byte1)
356 byte2
357 byte3)
358 (lambda unrestricted predecessor1 : Nat .
359 (lambda unrestricted induction1 : (family X86NativeUnsigned32) .
360 (nat-eliminate
361 (lambda unrestricted carry2 : Nat . (family X86NativeUnsigned32))
362 (constructor
363 X86NativeUnsigned32
364 X86NativeUnsigned32Value
365 (byte 0)
366 (byte 0)
367 (x86NativeIncrementByte byte2)
368 byte3)
369 (lambda unrestricted predecessor2 : Nat .
370 (lambda unrestricted induction2 : (family X86NativeUnsigned32) .
371 (constructor
372 X86NativeUnsigned32
373 X86NativeUnsigned32Value
374 (byte 0)
375 (byte 0)
376 (byte 0)
377 (x86NativeIncrementByte byte3))))
378 (byte-equal byte2 (byte 255)))))
379 (byte-equal byte1 (byte 255)))))
380 (byte-equal byte0 (byte 255))))))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.