		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-operations

Lognot-ullong

Logical complement of a value of type unsigned long long [C17:6.5.3].

Definitions and Theorems

Function: lognot-ullong

(defun lognot-ullong (x)
  (declare (xargs :guard (and (ullongp x))))
  (sint-from-boolean (= (integer-from-ullong x) 0)))

Theorem: sintp-of-lognot-ullong

(defthm sintp-of-lognot-ullong
  (sintp (lognot-ullong x)))

Theorem: lognot-ullong-of-ullong-fix-x

(defthm lognot-ullong-of-ullong-fix-x
  (equal (lognot-ullong (ullong-fix x))
         (lognot-ullong x)))

Theorem: lognot-ullong-ullong-equiv-congruence-on-x

(defthm lognot-ullong-ullong-equiv-congruence-on-x
  (implies (ullong-equiv x x-equiv)
           (equal (lognot-ullong x)
                  (lognot-ullong x-equiv)))
  :rule-classes :congruence)