		Search-engine friendly clone of the ACL2 documentation.

Omaps

Mapp

Recognize omaps.

Signature
(mapp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

This is similar to the definition of setp, but each element of the list is checked to be a cons pair and the ordering comparison is performed on the cars.

Definitions and Theorems

Function: mapp

(defun mapp (x)
       (declare (xargs :guard t))
       (let ((__function__ 'mapp))
            (declare (ignorable __function__))
            (if (atom x)
                (null x)
                (and (consp (car x))
                     (or (null (cdr x))
                         (and (consp (cdr x))
                              (consp (cadr x))
                              (fast-<< (caar x) (caadr x))
                              (mapp (cdr x))))))))

Theorem: booleanp-of-mapp

(defthm booleanp-of-mapp
        (b* ((yes/no (mapp x)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Theorem: setp-when-mapp

(defthm setp-when-mapp
        (implies (mapp x) (setp x))
        :rule-classes (:rewrite :forward-chaining))

Theorem: alistp-when-mapp

(defthm alistp-when-mapp
        (implies (mapp x) (alistp x))
        :rule-classes (:rewrite :forward-chaining))

Theorem: consp-car-when-non-empty-mapp

(defthm consp-car-when-non-empty-mapp
        (implies (and map (mapp map))
                 (consp (car map))))