		Search-engine friendly clone of the ACL2 documentation.

4v-nsexpr-p

(4v-nsexpr-p x) recognizes s-expressions where every variable is a natural number.

We can develop a faster version of 4v-sexpr-vars by requiring all of the variables in an s-expression to be natural numbers; see 4v-nsexpr-vars.

Memoized. You should probably clear its table when you clear the tables for 4v-nsexpr-vars-nonsparse or 4v-nsexpr-vars-sparse.

We typically leave these disabled and reason about, e.g.,

(nat-listp (4v-sexpr-vars x))

Function: 4v-nsexpr-p

(defun 4v-nsexpr-p (x)
  (declare (xargs :guard t))
  (if (atom x)
      (or (not x) (natp x))
    (4v-nsexpr-list-p (cdr x))))

Function: 4v-nsexpr-list-p

(defun 4v-nsexpr-list-p (x)
  (declare (xargs :guard t))
  (if (atom x)
      t
    (and (4v-nsexpr-p (car x))
         (4v-nsexpr-list-p (cdr x)))))

Function: 4v-nsexpr-p-memoize-condition

(defun 4v-nsexpr-p-memoize-condition (x)
  (declare (ignorable x)
           (xargs :guard 't))
  (and (consp x) (consp (cdr x))))

Theorem: 4v-nsexpr-p-when-nat-listp-4v-sexpr-vars

(defthm 4v-nsexpr-p-when-nat-listp-4v-sexpr-vars
  (equal (4v-nsexpr-p x)
         (nat-listp (4v-sexpr-vars x))))

Theorem: 4v-nsexpr-list-p-when-nat-listp-4v-sexpr-vars-list

(defthm 4v-nsexpr-list-p-when-nat-listp-4v-sexpr-vars-list
  (equal (4v-nsexpr-list-p x)
         (nat-listp (4v-sexpr-vars-list x))))

4v-nsexpr-alist-p: (4v-nsexpr-p x) recognizes an alist where every value is an 4v-nsexpr-p.
4v-nsexpr-p-4v-sexpr-compose
4v-nsexpr-p-4v-sexpr-restrict