		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-annop

Filepath-transunit-map-annop

Signature
(filepath-transunit-map-annop 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-annop

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

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

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

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

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

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

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

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

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