382def x86NativeIncrementUnsigned32 :
383 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeUnsigned32Result)) =
384 (lambda unrestricted value : (family X86NativeUnsigned32) .
385 (eliminate
386 X86NativeUnsigned32
387 (lambda unrestricted current : (family X86NativeUnsigned32) .
388 (family X86NativeUnsigned32Result))
389 value
390 (branch
391 X86NativeUnsigned32Value
392 byte0
393 byte1
394 byte2
395 byte3
396 .
397 (nat-eliminate
398 (lambda unrestricted carry0 : Nat . (family X86NativeUnsigned32Result))
399 (constructor
400 X86NativeUnsigned32Result
401 X86NativeUnsigned32Success
402 (constructor
403 X86NativeUnsigned32
404 X86NativeUnsigned32Value
405 (x86NativeIncrementByte byte0)
406 byte1
407 byte2
408 byte3))
409 (lambda unrestricted predecessor0 : Nat .
410 (lambda unrestricted induction0 : (family X86NativeUnsigned32Result) .
411 (nat-eliminate
412 (lambda unrestricted carry1 : Nat . (family X86NativeUnsigned32Result))
413 (constructor
414 X86NativeUnsigned32Result
415 X86NativeUnsigned32Success
416 (constructor
417 X86NativeUnsigned32
418 X86NativeUnsigned32Value
419 (byte 0)
420 (x86NativeIncrementByte byte1)
421 byte2
422 byte3))
423 (lambda unrestricted predecessor1 : Nat .
424 (lambda unrestricted induction1 : (family X86NativeUnsigned32Result) .
425 (nat-eliminate
426 (lambda unrestricted carry2 : Nat . (family X86NativeUnsigned32Result))
427 (constructor
428 X86NativeUnsigned32Result
429 X86NativeUnsigned32Success
430 (constructor
431 X86NativeUnsigned32
432 X86NativeUnsigned32Value
433 (byte 0)
434 (byte 0)
435 (x86NativeIncrementByte byte2)
436 byte3))
437 (lambda unrestricted predecessor2 : Nat .
438 (lambda unrestricted induction2 : (family X86NativeUnsigned32Result) .
439 (nat-eliminate
440 (lambda unrestricted carry3 : Nat . (family X86NativeUnsigned32Result))
441 (constructor
442 X86NativeUnsigned32Result
443 X86NativeUnsigned32Success
444 (constructor
445 X86NativeUnsigned32
446 X86NativeUnsigned32Value
447 (byte 0)
448 (byte 0)
449 (byte 0)
450 (x86NativeIncrementByte byte3)))
451 (lambda unrestricted predecessor3 : Nat .
452 (lambda unrestricted induction3 : (family X86NativeUnsigned32Result) .
453 (constructor X86NativeUnsigned32Result X86NativeUnsigned32Overflow)))
454 (byte-equal byte3 (byte 255)))))
455 (byte-equal byte2 (byte 255)))))
456 (byte-equal byte1 (byte 255)))))
457 (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.