A 26-bit branch field at bit 0.
862def aarch64Branch26Word =
863 (lambda unrestricted base3 : Nat .
864 (lambda unrestricted direction : (family AArch64Direction) .
865 (lambda unrestricted distance : Nat .
866 (nat-eliminate
867 (lambda unrestricted aligned : Nat . (family AArch64EncodeResult))
868 (constructor AArch64EncodeResult AArch64MisalignedOffset distance)
869 (lambda unrestricted predecessorAligned : Nat .
870 (lambda unrestricted inductionAligned : (family AArch64EncodeResult) .
871 (nat-eliminate
872 (lambda unrestricted accepted : Nat . (family AArch64EncodeResult))
873 (constructor AArch64EncodeResult AArch64DisplacementOutOfRange distance)
874 (lambda unrestricted predecessor : Nat .
875 (lambda unrestricted induction : (family AArch64EncodeResult) .
876 (app
877 (lambda unrestricted field : Nat .
878 (aarch64ByteWord
879 (naturalModuloUnchecked field aarch64TwoHundredFiftySix)
880 (naturalModuloUnchecked
881 (naturalDivideUnchecked field aarch64TwoHundredFiftySix)
882 aarch64TwoHundredFiftySix)
883 (naturalModuloUnchecked
884 (naturalDivideUnchecked
885 field
886 (naturalMultiply aarch64TwoHundredFiftySix aarch64TwoHundredFiftySix))
887 aarch64TwoHundredFiftySix)
888 (naturalAdd
889 base3
890 (naturalModuloUnchecked
891 (naturalDivideUnchecked
892 field
893 (naturalMultiply
894 (naturalMultiply
895 aarch64TwoHundredFiftySix
896 aarch64TwoHundredFiftySix)
897 aarch64TwoHundredFiftySix))
898 aarch64Four))))
899 (aarch64SignedField
900 direction
901 (naturalDivideUnchecked distance aarch64Four)
902 aarch64Modulus26))))
903 (aarch64DistanceAccepted
904 direction
905 (naturalDivideUnchecked distance aarch64Four)
906 (naturalDivideUnchecked aarch64Modulus26 aarch64Two)))))
907 (naturalIsZero (naturalModuloUnchecked distance aarch64Four))))))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.