		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-aidentp

Ident-list-list-aidentp

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

Definitions and Theorems

Function: ident-list-list-aidentp

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

Theorem: booleanp-of-ident-list-list-aidentp

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

Theorem: ident-list-list-aidentp-of-ident-list-list-fix-ident-list-list

(defthm
     ident-list-list-aidentp-of-ident-list-list-fix-ident-list-list
 (equal
      (ident-list-list-aidentp (ident-list-list-fix ident-list-list)
                               gcc)
      (ident-list-list-aidentp ident-list-list gcc)))

Theorem: ident-list-list-aidentp-ident-list-list-equiv-congruence-on-ident-list-list

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

Theorem: ident-list-list-aidentp-of-bool-fix-gcc

(defthm ident-list-list-aidentp-of-bool-fix-gcc
  (equal (ident-list-list-aidentp ident-list-list (bool-fix gcc))
         (ident-list-list-aidentp ident-list-list gcc)))

Theorem: ident-list-list-aidentp-iff-congruence-on-gcc

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