		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-globalp

Signature
(svstack-globalp k stack) → *
Arguments: k — Guard (svar-p k).; stack — Guard (svstack-p stack).

Definitions and Theorems

Function: svstack-globalp

(defun svstack-globalp (k stack)
  (declare (xargs :guard (and (svar-p k) (svstack-p stack))))
  (declare (xargs :guard (consp stack)))
  (let ((__function__ 'svstack-globalp))
    (declare (ignorable __function__))
    (if (atom (cdr stack))
        t
      (and (not (svex-fastlookup k (car stack)))
           (svstack-globalp k (cdr stack))))))

Theorem: svstack-globalp-of-svar-fix-k

(defthm svstack-globalp-of-svar-fix-k
  (equal (svstack-globalp (svar-fix k) stack)
         (svstack-globalp k stack)))

Theorem: svstack-globalp-svar-equiv-congruence-on-k

(defthm svstack-globalp-svar-equiv-congruence-on-k
  (implies (svar-equiv k k-equiv)
           (equal (svstack-globalp k stack)
                  (svstack-globalp k-equiv stack)))
  :rule-classes :congruence)

Theorem: svstack-globalp-of-svstack-fix-stack

(defthm svstack-globalp-of-svstack-fix-stack
  (equal (svstack-globalp k (svstack-fix stack))
         (svstack-globalp k stack)))

Theorem: svstack-globalp-svstack-equiv-congruence-on-stack

(defthm svstack-globalp-svstack-equiv-congruence-on-stack
  (implies (svstack-equiv stack stack-equiv)
           (equal (svstack-globalp k stack)
                  (svstack-globalp k stack-equiv)))
  :rule-classes :congruence)