• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
        • Defbytelist
        • Defbyte-standard-instances
          • Ubyte5
          • Ubyte32
          • Ubyte12
          • Ubyte8
          • Defbyte-standard-instances-ihs-theorems
            • Ubyte128-ihs-theorems
            • Sbyte64-ihs-theorems
            • Sbyte32-ihs-theorems
            • Sbyte16-ihs-theorems
            • Sbyte128-ihs-theorems
            • Ubyte8-ihs-theorems
            • Ubyte7-ihs-theorems
            • Ubyte64-ihs-theorems
            • Ubyte6-ihs-theorems
            • Ubyte5-ihs-theorems
            • Ubyte32-ihs-theorems
            • Ubyte3-ihs-theorems
            • Ubyte20-ihs-theorems
            • Ubyte16-ihs-theorems
            • Ubyte12-ihs-theorems
            • Sbyte8-ihs-theorems
          • Ubyte20
          • Ubyte64
          • Ubyte16
          • Ubyte128
          • Sbyte8
          • Sbyte64
          • Sbyte32
          • Sbyte16
          • Sbyte128
          • Ubyte6
          • Ubyte7
          • Ubyte3
          • Ubyte11
          • Ubyte4
          • Ubyte256
          • Sbyte256
          • Ubyte2
          • Ubyte1
          • Sbyte4
          • Sbyte3
          • Sbyte2
          • Sbyte1
          • Defubyte
          • Defsbyte
        • Defbyte-ihs-theorems
        • Defbyte-implementation
      • Defresult
      • Deffixequiv
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defomap
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defbyte-standard-instances

Defbyte-standard-instances-ihs-theorems

Theorems about defbyte standard instances and IHS functions.

Subtopics

Ubyte128-ihs-theorems

Theorems about ubyte128 and IHS functions.

Sbyte64-ihs-theorems

Theorems about sbyte64 and IHS functions.

Sbyte32-ihs-theorems

Theorems about sbyte32 and IHS functions.

Sbyte16-ihs-theorems

Theorems about sbyte16 and IHS functions.

Sbyte128-ihs-theorems

Theorems about sbyte128 and IHS functions.

Ubyte8-ihs-theorems

Theorems about ubyte8 and IHS functions.

Ubyte7-ihs-theorems

Theorems about ubyte7 and IHS functions.

Ubyte64-ihs-theorems

Theorems about ubyte64 and IHS functions.

Ubyte6-ihs-theorems

Theorems about ubyte6 and IHS functions.

Ubyte5-ihs-theorems

Theorems about ubyte5 and IHS functions.

Ubyte32-ihs-theorems

Theorems about ubyte32 and IHS functions.

Ubyte3-ihs-theorems

Theorems about ubyte3 and IHS functions.

Ubyte20-ihs-theorems

Theorems about ubyte20 and IHS functions.

Ubyte16-ihs-theorems

Theorems about ubyte16 and IHS functions.

Ubyte12-ihs-theorems

Theorems about ubyte12 and IHS functions.

Sbyte8-ihs-theorems

Theorems about sbyte8 and IHS functions.