		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-annop

Filepath-transunit-map-annop

Signature
(filepath-transunit-map-annop 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-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__))
  (or (not (mbt (filepath-transunit-mapp filepath-transunit-map)))
      (omap::emptyp filepath-transunit-map)
      (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*
    ((yes/no (filepath-transunit-map-annop filepath-transunit-map)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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)