591def sm86EncodeIntegerMultiplyAddWideConstant =
592 (lambda unrestricted guard : (family SM86InstructionGuard) .
593 (lambda unrestricted destination : (family SM86Register) .
594 (lambda unrestricted left : (family SM86Register) .
595 (lambda unrestricted right : (family SM86Register) .
596 (lambda unrestricted bank : Byte .
597 (lambda unrestricted offset : (family SM86Unsigned32) .
598 (lambda unrestricted control : (family SM86Control) .
599 (nat-eliminate
600 (lambda unrestricted destinationIsZero : Nat .
601 (family SM86InstructionEncodingResult))
602 (sm86EncodeInstructionFields
603 sm86OpcodeIntegerMultiplyAddWideConstant
604 guard
605 control
606 (sm86InstructionPrependField
607 sm86InstructionNaturalSixteen
608 sm86InstructionNaturalEight
609 (sm86RegisterNatural destination)
610 (sm86InstructionPrependField
611 sm86InstructionNaturalTwentyFour
612 sm86InstructionNaturalEight
613 (sm86RegisterNatural left)
614 (sm86InstructionPrependField
615 sm86InstructionNaturalThirtyEight
616 sm86InstructionNaturalSixteen
617 (sm86Unsigned32Natural offset)
618 (sm86InstructionPrependField
619 sm86InstructionNaturalFiftyFour
620 sm86InstructionNaturalFive
621 (byte-to-nat bank)
622 (sm86InstructionPrependField
623 sm86InstructionNaturalSixtyFour
624 sm86InstructionNaturalEight
625 (sm86RegisterNatural right)
626 (sm86InstructionOneWord24Field
627 sm86InstructionNaturalSeventyTwo
628 (byte 0)
629 (byte 142)
630 (byte 7))))))))
631 (lambda unrestricted invalidPredecessor : Nat .
632 (lambda unrestricted invalidInduction : (family SM86InstructionEncodingResult) .
633 (sm86InstructionUnsupported (byte-to-nat (byte 6)))))
634 (byte-equal (nat-to-byte (sm86RegisterNatural destination)) (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.