		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-unambp

Filepath-transunit-map-unambp

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

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__))
  (cond
   ((not (mbt (filepath-transunit-mapp filepath-transunit-map)))
    t)
   ((omap::emptyp filepath-transunit-map)
    t)
   (t
     (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* ((fty::result
            (filepath-transunit-map-unambp filepath-transunit-map)))
    (booleanp fty::result))
  :rule-classes :rewrite)

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)