		Search-engine friendly clone of the ACL2 documentation.

Match-cons-nest

Match-cons-nest-aux

Signature
(match-cons-nest-aux x acc) → (mv matchp acc)
Arguments: x — Guard (ute-term-p x).; acc — Guard (ute-termlist-p acc).
Returns: matchp — Type (booleanp matchp).; acc — Type (ute-termlist-p acc), given the guard.

Definitions and Theorems

Function: match-cons-nest-aux

(defun match-cons-nest-aux (x acc)
  (declare (xargs :guard (and (ute-term-p x)
                              (ute-termlist-p acc))))
  (let ((__function__ 'match-cons-nest-aux))
    (declare (ignorable __function__))
    (cond ((atom x) (mv nil acc))
          ((equal x ''nil) (mv t acc))
          ((and (eq (car x) 'cons)
                (equal (length x) 3))
           (match-cons-nest-aux (third x)
                                (cons (second x) acc)))
          (t (mv nil acc)))))

Theorem: booleanp-of-match-cons-nest-aux.matchp

(defthm booleanp-of-match-cons-nest-aux.matchp
  (b* (((mv ?matchp ?acc)
        (match-cons-nest-aux x acc)))
    (booleanp matchp))
  :rule-classes :type-prescription)

Theorem: ute-termlist-p-of-match-cons-nest-aux.acc

(defthm ute-termlist-p-of-match-cons-nest-aux.acc
  (implies (and (ute-term-p x)
                (ute-termlist-p acc))
           (b* (((mv ?matchp ?acc)
                 (match-cons-nest-aux x acc)))
             (ute-termlist-p acc)))
  :rule-classes :rewrite)

Theorem: true-listp-of-match-cons-nest-aux

(defthm true-listp-of-match-cons-nest-aux
  (implies (true-listp acc)
           (true-listp (mv-nth 1 (match-cons-nest-aux x acc)))))