• 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
            • 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
              • Ulong-list-fix
              • Ulong-list-equiv
              • Ulong-listp
            • 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

• Ulong-list

Ulong-list-equiv

Basic equivalence relation for ulong-list structures.

Definitions and Theorems

Function: ulong-list-equiv$inline

(defun ulong-list-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (ulong-listp acl2::x)
                              (ulong-listp acl2::y))))
  (equal (ulong-list-fix acl2::x)
         (ulong-list-fix acl2::y)))

Theorem: ulong-list-equiv-is-an-equivalence

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

Theorem: ulong-list-equiv-implies-equal-ulong-list-fix-1

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

Theorem: ulong-list-fix-under-ulong-list-equiv

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

Theorem: equal-of-ulong-list-fix-1-forward-to-ulong-list-equiv

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

Theorem: equal-of-ulong-list-fix-2-forward-to-ulong-list-equiv

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

Theorem: ulong-list-equiv-of-ulong-list-fix-1-forward

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

Theorem: ulong-list-equiv-of-ulong-list-fix-2-forward

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