• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
          • Defbyte
            • Defbytelist
            • Defbyte-standard-instances
              • Ubyte5
              • Ubyte8
              • Ubyte32
              • Ubyte12
              • Ubyte64
              • Ubyte16
                • Ubyte16p
                • Ubyte16-fix
                • Ubyte16-ihs-theorems
                • Ubyte128
                • Sbyte8
                • Sbyte64
                • Sbyte32
                • Sbyte16
                • Sbyte128
                • Ubyte20
                • Ubyte11
                • Ubyte4
                • Ubyte256
                • Sbyte256
                • Ubyte7
                • Ubyte6
                • Ubyte3
                • Ubyte2
                • Ubyte1
                • Sbyte4
                • Sbyte3
                • Sbyte2
                • Sbyte1
                • Defbyte-standard-instances-ihs-theorems
                • Defubyte
                • Defsbyte
              • Defbyte-ihs-theorems
              • Defbyte-implementation
            • Defresult
            • Defsubtype
            • Defset
            • Specific-types
            • Defflatsum
            • Deflist-of-len
            • Pos-list
            • Defbytelist
            • Defbyte-standard-instances
              • Ubyte5
              • Ubyte8
              • Ubyte32
              • Ubyte12
              • Ubyte64
              • Ubyte16
                • Ubyte16p
                • Ubyte16-fix
                • Ubyte16-ihs-theorems
                • Ubyte128
                • Sbyte8
                • Sbyte64
                • Sbyte32
                • Sbyte16
                • Sbyte128
                • Ubyte20
                • Ubyte11
                • Ubyte4
                • Ubyte256
                • Sbyte256
                • Ubyte7
                • Ubyte6
                • Ubyte3
                • Ubyte2
                • Ubyte1
                • Sbyte4
                • Sbyte3
                • Sbyte2
                • Sbyte1
                • Defbyte-standard-instances-ihs-theorems
                • Defubyte
                • Defsbyte
              • Defomap
              • Deffixtype-alias
              • Defbytelist-standard-instances
              • Defunit
              • Byte-list
              • Byte
              • Pos-option
              • Nibble
              • Nat-option
              • String-option
              • Byte-list20
              • Byte-list32
              • Byte-list64
              • Pseudo-event-form
              • Natoption/natoptionlist
              • Nati
              • Character-list
              • Nat/natlist
              • Maybe-string
              • Nibble-list
              • Natoption/natoptionlist-result
              • Nat/natlist-result
              • Nat-option-list-result
              • Set
              • String-result
              • String-list-result
              • Nat-result
              • Nat-option-result
              • Nat-list-result
              • Maybe-string-result
              • Integer-result
              • Character-result
              • Character-list-result
              • Boolean-result
              • Map
              • Bag
              • Pos-set
              • Hex-digit-char-list
              • Dec-digit-char-list
              • Nat-option-list
              • Symbol-set
              • String-set
              • Pseudo-event-form-list
              • Nat-set
              • Oct-digit-char-list
              • Bin-digit-char-list
              • Bit-list
            • Isar
            • Kestrel-utilities
            • Soft
            • Bv
            • Imp-language
            • C
            • Event-macros
            • Java
            • Bitcoin
            • Ethereum
            • Yul
            • Zcash
            • ACL2-programming-language
            • Prime-fields
            • Json
            • Syntheto
            • File-io-light
            • Number-theory
            • Cryptography
            • Lists-light
            • Builtins
            • Axe
            • Solidity
            • Helpers
            • Htclient
            • Typed-lists-light
            • Arithmetic-light
          • X86isa
          • Axe
          • Execloader
        • Math
        • Testing-utilities
      • Ubyte16
      • Defbyte-standard-instances-ihs-theorems

      Ubyte16-ihs-theorems

      Theorems about ubyte16 and IHS functions.

      Definitions and Theorems

      Theorem: ubyte16p-of-loghead-of-16

      (defthm ubyte16p-of-loghead-of-16
  (ubyte16p (loghead 16 x)))