		Search-engine friendly clone of the ACL2 documentation.

Hex-prefix

Hp-encoding-p

Check if a byte array is a hex-prefix encoding.

This is a declarative, non-executable definition, which essentially characterizes the image of hp-encode.

Definitions and Theorems

Theorem: hp-encoding-p-suff

(defthm hp-encoding-p-suff
  (implies (and (nibble-listp nibbles)
                (booleanp flag)
                (equal (hp-encode nibbles flag)
                       (byte-list-fix encoding)))
           (hp-encoding-p encoding)))

Theorem: booleanp-of-hp-encoding-p

(defthm booleanp-of-hp-encoding-p
  (b* ((yes/no (hp-encoding-p encoding)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: hp-encoding-p-of-byte-list-fix-encoding

(defthm hp-encoding-p-of-byte-list-fix-encoding
  (equal (hp-encoding-p (byte-list-fix encoding))
         (hp-encoding-p encoding)))

Theorem: hp-encoding-p-byte-list-equiv-congruence-on-encoding

(defthm hp-encoding-p-byte-list-equiv-congruence-on-encoding
  (implies (byte-list-equiv encoding encoding-equiv)
           (equal (hp-encoding-p encoding)
                  (hp-encoding-p encoding-equiv)))
  :rule-classes :congruence)