		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-aidentp

Ext-declon-list-aidentp

Signature
(ext-declon-list-aidentp ext-declon-list gcc) → fty::result
Arguments: ext-declon-list — Guard (ext-declon-listp ext-declon-list).; gcc — Guard (booleanp gcc).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: ext-declon-list-aidentp

(defun ext-declon-list-aidentp (ext-declon-list gcc)
  (declare (xargs :guard (and (ext-declon-listp ext-declon-list)
                              (booleanp gcc))))
  (let ((__function__ 'ext-declon-list-aidentp))
    (declare (ignorable __function__))
    (cond ((endp ext-declon-list) t)
          (t (and (ext-declon-aidentp (car ext-declon-list)
                                      gcc)
                  (ext-declon-list-aidentp (cdr ext-declon-list)
                                           gcc))))))

Theorem: booleanp-of-ext-declon-list-aidentp

(defthm booleanp-of-ext-declon-list-aidentp
  (b* ((fty::result (ext-declon-list-aidentp ext-declon-list gcc)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: ext-declon-list-aidentp-of-ext-declon-list-fix-ext-declon-list

(defthm
     ext-declon-list-aidentp-of-ext-declon-list-fix-ext-declon-list
 (equal
      (ext-declon-list-aidentp (ext-declon-list-fix ext-declon-list)
                               gcc)
      (ext-declon-list-aidentp ext-declon-list gcc)))

Theorem: ext-declon-list-aidentp-ext-declon-list-equiv-congruence-on-ext-declon-list

(defthm
 ext-declon-list-aidentp-ext-declon-list-equiv-congruence-on-ext-declon-list
 (implies
      (ext-declon-list-equiv ext-declon-list ext-declon-list-equiv)
      (equal (ext-declon-list-aidentp ext-declon-list gcc)
             (ext-declon-list-aidentp ext-declon-list-equiv gcc)))
 :rule-classes :congruence)

Theorem: ext-declon-list-aidentp-of-bool-fix-gcc

(defthm ext-declon-list-aidentp-of-bool-fix-gcc
  (equal (ext-declon-list-aidentp ext-declon-list (bool-fix gcc))
         (ext-declon-list-aidentp ext-declon-list gcc)))

Theorem: ext-declon-list-aidentp-iff-congruence-on-gcc

(defthm ext-declon-list-aidentp-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (ext-declon-list-aidentp ext-declon-list gcc)
              (ext-declon-list-aidentp ext-declon-list gcc-equiv)))
  :rule-classes :congruence)