		Search-engine friendly clone of the ACL2 documentation.

Utilities

Prefix-of-eachp

(prefix-of-eachp p x) returns true exactly when p is a prefix of every member of x.

Signature
(prefix-of-eachp p x) → std::bool

This is an ordinary deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: prefix-of-eachp

(defun prefix-of-eachp (p x)
  (declare (xargs :guard t))
  (let ((__function__ 'prefix-of-eachp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (prefixp p (car x))
             (prefix-of-eachp p (cdr x)))
      t)))

Theorem: prefix-of-eachp-when-prefixp

(defthm prefix-of-eachp-when-prefixp
  (implies (and (prefix-of-eachp a x)
                (prefixp b a))
           (prefix-of-eachp b x)))

Theorem: prefix-of-eachp-when-prefixp-alt

(defthm prefix-of-eachp-when-prefixp-alt
  (implies (and (prefixp b a)
                (prefix-of-eachp a x))
           (prefix-of-eachp b x)))

Subtopics

Prefix-of-eachp-basics: Basic theorems about prefix-of-eachp, generated by deflist.