		Search-engine friendly clone of the ACL2 documentation.

Atc-pointed-integer-rules

Rules about pointed-to integers.

Theorem: schar-read-when-scharp

(defthm schar-read-when-scharp
  (implies (scharp x)
           (equal (schar-read x) x)))

Theorem: uchar-read-when-ucharp

(defthm uchar-read-when-ucharp
  (implies (ucharp x)
           (equal (uchar-read x) x)))

Theorem: sshort-read-when-sshortp

(defthm sshort-read-when-sshortp
  (implies (sshortp x)
           (equal (sshort-read x) x)))

Theorem: ushort-read-when-ushortp

(defthm ushort-read-when-ushortp
  (implies (ushortp x)
           (equal (ushort-read x) x)))

Theorem: sint-read-when-sintp

(defthm sint-read-when-sintp
  (implies (sintp x)
           (equal (sint-read x) x)))

Theorem: uint-read-when-uintp

(defthm uint-read-when-uintp
  (implies (uintp x)
           (equal (uint-read x) x)))

Theorem: slong-read-when-slongp

(defthm slong-read-when-slongp
  (implies (slongp x)
           (equal (slong-read x) x)))

Theorem: ulong-read-when-ulongp

(defthm ulong-read-when-ulongp
  (implies (ulongp x)
           (equal (ulong-read x) x)))

Theorem: sllong-read-when-sllongp

(defthm sllong-read-when-sllongp
  (implies (sllongp x)
           (equal (sllong-read x) x)))

Theorem: ullong-read-when-ullongp

(defthm ullong-read-when-ullongp
  (implies (ullongp x)
           (equal (ullong-read x) x)))

Theorem: schar-write-when-scharp

(defthm schar-write-when-scharp
  (implies (scharp x)
           (equal (schar-write x) x)))

Theorem: uchar-write-when-ucharp

(defthm uchar-write-when-ucharp
  (implies (ucharp x)
           (equal (uchar-write x) x)))

Theorem: sshort-write-when-sshortp

(defthm sshort-write-when-sshortp
  (implies (sshortp x)
           (equal (sshort-write x) x)))

Theorem: ushort-write-when-ushortp

(defthm ushort-write-when-ushortp
  (implies (ushortp x)
           (equal (ushort-write x) x)))

Theorem: sint-write-when-sintp

(defthm sint-write-when-sintp
  (implies (sintp x)
           (equal (sint-write x) x)))

Theorem: uint-write-when-uintp

(defthm uint-write-when-uintp
  (implies (uintp x)
           (equal (uint-write x) x)))

Theorem: slong-write-when-slongp

(defthm slong-write-when-slongp
  (implies (slongp x)
           (equal (slong-write x) x)))

Theorem: ulong-write-when-ulongp

(defthm ulong-write-when-ulongp
  (implies (ulongp x)
           (equal (ulong-write x) x)))

Theorem: sllong-write-when-sllongp

(defthm sllong-write-when-sllongp
  (implies (sllongp x)
           (equal (sllong-write x) x)))

Theorem: ullong-write-when-ullongp

(defthm ullong-write-when-ullongp
  (implies (ullongp x)
           (equal (ullong-write x) x)))