• 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
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
          • Representation-of-integer-operations
          • Atc-arrays
          • Representation-of-integers
            • Def-integer-values
            • Ushort-list-from-integer-list
            • Ullong-list-from-integer-list
            • Sshort-list-from-integer-list
            • Sllong-list-from-integer-list
            • Integer-list-from-ushort-list
            • Integer-list-from-ullong-list
            • Integer-list-from-sshort-list
            • Integer-list-from-sllong-list
            • Ulong-list-from-integer-list
            • Uchar-list-from-integer-list
            • Slong-list-from-integer-list
            • Schar-list-from-integer-list
            • Integer-list-from-ulong-list
            • Integer-list-from-uchar-list
            • Integer-list-from-slong-list
            • Integer-list-from-schar-list
            • Uint-list-from-integer-list
            • Sint-list-from-integer-list
            • Integer-list-from-uint-list
            • Integer-list-from-sint-list
            • Cinteger
              • Cintegerp
              • Cinteger-fix
              • Cinteger-equiv
              • Cinteger-ushort
              • Cinteger-ulong
              • Cinteger-ullong
              • Cinteger-uint
              • Cinteger-uchar
              • Cinteger-sshort
              • Cinteger-slong
              • Cinteger-sllong
              • Cinteger-sint
              • Cinteger-schar
              • Cinteger-kind
            • Ullongp
            • Ucharp
            • Sintp
            • Ushortp
            • Ulongp
            • Uintp
            • Sllongp
            • Slongp
            • Sshortp
            • Scharp
            • Integer-from-sshort
            • Integer-from-sllong
            • Integer-from-sint
            • Integer-from-slong
            • Integer-from-schar
            • Integer-type-to-fixtype
            • Integer-from-ushort
            • Integer-from-ullong
            • Integer-from-uchar
            • Integer-from-cinteger
            • Integer-from-ulong
            • Integer-from-uint
            • Def-integer-values-loop
            • Sint-from-integer
            • Sint
            • Fixtype-to-integer-type
            • Uchar-from-integer
            • Ushort-from-integer-mod
            • Ushort-from-integer
            • Ulong-from-integer-mod
            • Ulong-from-integer
            • Ullong-from-integer-mod
            • Ullong-from-integer
            • Uchar-from-integer-mod
            • Sshort-from-integer
            • Slong-from-integer
            • Sllong-from-integer
            • Schar-from-integer
            • Uint-from-integer-mod
            • Uint-from-integer
            • Uchar
            • Schar
            • Ushort
            • Ulong
            • Ullong
            • Sshort
            • Slong
            • Sllong
            • Ullong-fix
            • Uint
            • Uchar-fix
            • Sint-fix
            • Ushort-fix
            • Ulong-fix
            • Uint-fix
            • Sshort-fix
            • Slong-fix
            • Sllong-fix
            • Schar-fix
            • Ushort-list
            • Ulong-list
            • Ullong-list
            • Uint-list
            • Uchar-list
            • Sshort-list
            • Slong-list
            • Sllong-list
            • Sint-list
            • Schar-list
            • Integer-type-to/from-fixtype-theorems
            • *nonchar-integer-fixtypes*
          • Representation-of-integer-conversions
          • Pointed-integers
        • Transformation-tools
        • Pack
      • 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

• Cinteger

Cinteger-equiv

Basic equivalence relation for cinteger structures.

Definitions and Theorems

Function: cinteger-equiv$inline

(defun cinteger-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (cintegerp acl2::x)
                              (cintegerp acl2::y))))
  (equal (cinteger-fix acl2::x)
         (cinteger-fix acl2::y)))

Theorem: cinteger-equiv-is-an-equivalence

(defthm cinteger-equiv-is-an-equivalence
  (and (booleanp (cinteger-equiv x y))
       (cinteger-equiv x x)
       (implies (cinteger-equiv x y)
                (cinteger-equiv y x))
       (implies (and (cinteger-equiv x y)
                     (cinteger-equiv y z))
                (cinteger-equiv x z)))
  :rule-classes (:equivalence))

Theorem: cinteger-equiv-implies-equal-cinteger-fix-1

(defthm cinteger-equiv-implies-equal-cinteger-fix-1
  (implies (cinteger-equiv acl2::x x-equiv)
           (equal (cinteger-fix acl2::x)
                  (cinteger-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: cinteger-fix-under-cinteger-equiv

(defthm cinteger-fix-under-cinteger-equiv
  (cinteger-equiv (cinteger-fix acl2::x)
                  acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-cinteger-fix-1-forward-to-cinteger-equiv

(defthm equal-of-cinteger-fix-1-forward-to-cinteger-equiv
  (implies (equal (cinteger-fix acl2::x) acl2::y)
           (cinteger-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-cinteger-fix-2-forward-to-cinteger-equiv

(defthm equal-of-cinteger-fix-2-forward-to-cinteger-equiv
  (implies (equal acl2::x (cinteger-fix acl2::y))
           (cinteger-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: cinteger-equiv-of-cinteger-fix-1-forward

(defthm cinteger-equiv-of-cinteger-fix-1-forward
  (implies (cinteger-equiv (cinteger-fix acl2::x)
                           acl2::y)
           (cinteger-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: cinteger-equiv-of-cinteger-fix-2-forward

(defthm cinteger-equiv-of-cinteger-fix-2-forward
  (implies (cinteger-equiv acl2::x (cinteger-fix acl2::y))
           (cinteger-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)