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