		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-unambp

Filepath-transunit-map-unambp

Signature
(filepath-transunit-map-unambp filepath-transunit-map) → yes/no
Arguments: filepath-transunit-map — Guard (filepath-transunit-mapp filepath-transunit-map).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: filepath-transunit-map-unambp

(defun filepath-transunit-map-unambp (filepath-transunit-map)
 (declare
    (xargs :guard (filepath-transunit-mapp filepath-transunit-map)))
 (let ((__function__ 'filepath-transunit-map-unambp))
  (declare (ignorable __function__))
  (or
     (not (mbt (filepath-transunit-mapp filepath-transunit-map)))
     (omap::emptyp filepath-transunit-map)
     (and (transunit-unambp (omap::head-val filepath-transunit-map))
          (filepath-transunit-map-unambp
               (omap::tail filepath-transunit-map))))))

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

(defthm booleanp-of-filepath-transunit-map-unambp
  (b*
   ((yes/no (filepath-transunit-map-unambp filepath-transunit-map)))
   (booleanp yes/no))
  :rule-classes :rewrite)

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

(defthm filepath-transunit-map-unambp-when-emptyp
  (implies (omap::emptyp filepath-transunit-map)
           (filepath-transunit-map-unambp filepath-transunit-map)))

Theorem: filepath-transunit-map-unambp-of-update

(defthm filepath-transunit-map-unambp-of-update
  (implies
       (and (filepath-transunit-mapp filepath-transunit-map)
            (transunit-unambp transunit)
            (filepath-transunit-map-unambp filepath-transunit-map))
       (filepath-transunit-map-unambp
            (omap::update filepath
                          transunit filepath-transunit-map))))

Theorem: transunit-of-head-when-filepath-transunit-map-unambp

(defthm transunit-of-head-when-filepath-transunit-map-unambp
 (implies
   (and (filepath-transunit-mapp filepath-transunit-map)
        (filepath-transunit-map-unambp filepath-transunit-map)
        (not (omap::emptyp filepath-transunit-map)))
   (transunit-unambp (mv-nth 1
                             (omap::head filepath-transunit-map)))))

Theorem: filepath-transunit-map-unambp-of-tail

(defthm filepath-transunit-map-unambp-of-tail
  (implies
       (and (filepath-transunit-mapp filepath-transunit-map)
            (filepath-transunit-map-unambp filepath-transunit-map))
       (filepath-transunit-map-unambp
            (omap::tail filepath-transunit-map))))

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

(defthm
 filepath-transunit-map-unambp-of-filepath-transunit-map-fix-filepath-transunit-map
 (equal (filepath-transunit-map-unambp
             (filepath-transunit-map-fix filepath-transunit-map))
        (filepath-transunit-map-unambp filepath-transunit-map)))

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

(defthm
 filepath-transunit-map-unambp-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-unambp filepath-transunit-map)
      (filepath-transunit-map-unambp filepath-transunit-map-equiv)))
 :rule-classes :congruence)