		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-aidentp

Filepath-transunit-map-aidentp

Signature
(filepath-transunit-map-aidentp filepath-transunit-map gcc) → fty::result
Arguments: filepath-transunit-map — Guard (filepath-transunit-mapp filepath-transunit-map).; gcc — Guard (booleanp gcc).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: filepath-transunit-map-aidentp

(defun filepath-transunit-map-aidentp (filepath-transunit-map gcc)
 (declare
   (xargs
        :guard (and (filepath-transunit-mapp filepath-transunit-map)
                    (booleanp gcc))))
 (let ((__function__ 'filepath-transunit-map-aidentp))
  (declare (ignorable __function__))
  (cond
   ((not (mbt (filepath-transunit-mapp filepath-transunit-map)))
    t)
   ((omap::emptyp filepath-transunit-map)
    t)
   (t
     (and (transunit-aidentp (omap::head-val filepath-transunit-map)
                             gcc)
          (filepath-transunit-map-aidentp
               (omap::tail filepath-transunit-map)
               gcc))))))

Theorem: booleanp-of-filepath-transunit-map-aidentp

(defthm booleanp-of-filepath-transunit-map-aidentp
 (b*
  ((fty::result
       (filepath-transunit-map-aidentp filepath-transunit-map gcc)))
  (booleanp fty::result))
 :rule-classes :rewrite)

Theorem: filepath-transunit-map-aidentp-when-emptyp

(defthm filepath-transunit-map-aidentp-when-emptyp
 (implies
  (omap::emptyp filepath-transunit-map)
  (equal (filepath-transunit-map-aidentp filepath-transunit-map gcc)
         t)))

Theorem: filepath-transunit-map-aidentp-of-filepath-transunit-map-fix-filepath-transunit-map

(defthm
 filepath-transunit-map-aidentp-of-filepath-transunit-map-fix-filepath-transunit-map
 (equal
      (filepath-transunit-map-aidentp
           (filepath-transunit-map-fix filepath-transunit-map)
           gcc)
      (filepath-transunit-map-aidentp filepath-transunit-map gcc)))

Theorem: filepath-transunit-map-aidentp-filepath-transunit-map-equiv-congruence-on-filepath-transunit-map

(defthm
 filepath-transunit-map-aidentp-filepath-transunit-map-equiv-congruence-on-filepath-transunit-map
 (implies
  (filepath-transunit-map-equiv filepath-transunit-map
                                filepath-transunit-map-equiv)
  (equal (filepath-transunit-map-aidentp filepath-transunit-map gcc)
         (filepath-transunit-map-aidentp
              filepath-transunit-map-equiv gcc)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-aidentp-of-bool-fix-gcc

(defthm filepath-transunit-map-aidentp-of-bool-fix-gcc
  (equal
       (filepath-transunit-map-aidentp
            filepath-transunit-map (bool-fix gcc))
       (filepath-transunit-map-aidentp filepath-transunit-map gcc)))

Theorem: filepath-transunit-map-aidentp-iff-congruence-on-gcc

(defthm filepath-transunit-map-aidentp-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal (filepath-transunit-map-aidentp filepath-transunit-map gcc)
         (filepath-transunit-map-aidentp
              filepath-transunit-map gcc-equiv)))
 :rule-classes :congruence)