Recognizer for tag-env.
(tag-envp x) → *
Function:
(defun tag-envp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (consp (car x)) (identp (caar x)) (tag-infop (cdar x)) (or (null (cdr x)) (and (consp (cdr x)) (consp (cadr x)) (acl2::fast-<< (caar x) (caadr x)) (tag-envp (cdr x)))))))
Theorem:
(defthm booleanp-of-tag-envp (booleanp (tag-envp x)))
Theorem:
(defthm mapp-when-tag-envp (implies (tag-envp x) (omap::mapp x)) :rule-classes (:rewrite :forward-chaining))
Theorem:
(defthm tag-envp-of-tail (implies (tag-envp x) (tag-envp (omap::tail x))))
Theorem:
(defthm identp-of-head-key-when-tag-envp (implies (and (tag-envp x) (not (omap::emptyp x))) (identp (mv-nth 0 (omap::head x)))))
Theorem:
(defthm tag-infop-of-head-val-when-tag-envp (implies (and (tag-envp x) (not (omap::emptyp x))) (tag-infop (mv-nth 1 (omap::head x)))))
Theorem:
(defthm tag-envp-of-update (implies (and (tag-envp x) (identp k) (tag-infop v)) (tag-envp (omap::update k v x))))
Theorem:
(defthm tag-envp-of-update* (implies (and (tag-envp x) (tag-envp y)) (tag-envp (omap::update* x y))))
Theorem:
(defthm tag-envp-of-delete (implies (tag-envp x) (tag-envp (omap::delete k x))))
Theorem:
(defthm tag-envp-of-delete* (implies (tag-envp x) (tag-envp (omap::delete* k x))))
Theorem:
(defthm identp-when-in-tag-envp-binds-free-x (implies (and (omap::assoc k x) (tag-envp x)) (identp k)))
Theorem:
(defthm identp-of-car-of-in-tag-envp (implies (and (tag-envp x) (omap::assoc k x)) (identp (car (omap::assoc k x)))))
Theorem:
(defthm tag-infop-of-cdr-of-in-tag-envp (implies (and (tag-envp x) (omap::assoc k x)) (tag-infop (cdr (omap::assoc k x)))))
Theorem:
(defthm tag-infop-of-lookup-when-tag-envp (implies (and (tag-envp x) (omap::assoc k x)) (tag-infop (omap::lookup k x))))