		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-scopestack-subscope-p

Determine if scopestack a occurs within scopestack b.

Signature
(vl-lucid-scopestack-subscope-p a b) → *
Arguments: a — Guard (vl-scopestack-p a).; b — Guard (vl-scopestack-p b).

Definitions and Theorems

Function: vl-lucid-scopestack-subscope-p

(defun vl-lucid-scopestack-subscope-p (a b)
 (declare (xargs :guard (and (vl-scopestack-p a)
                             (vl-scopestack-p b))))
 (let ((__function__ 'vl-lucid-scopestack-subscope-p))
   (declare (ignorable __function__))
   (b* ((a (vl-scopestack-fix a))
        (b (vl-scopestack-fix b)))
     (or (hons-equal a b)
         (vl-scopestack-case
              b
              :null nil
              :global nil
              :local (vl-lucid-scopestack-subscope-p a b.super))))))

Theorem: vl-lucid-scopestack-subscope-p-of-vl-scopestack-fix-a

(defthm vl-lucid-scopestack-subscope-p-of-vl-scopestack-fix-a
  (equal (vl-lucid-scopestack-subscope-p (vl-scopestack-fix a)
                                         b)
         (vl-lucid-scopestack-subscope-p a b)))

Theorem: vl-lucid-scopestack-subscope-p-vl-scopestack-equiv-congruence-on-a

(defthm
 vl-lucid-scopestack-subscope-p-vl-scopestack-equiv-congruence-on-a
 (implies (vl-scopestack-equiv a a-equiv)
          (equal (vl-lucid-scopestack-subscope-p a b)
                 (vl-lucid-scopestack-subscope-p a-equiv b)))
 :rule-classes :congruence)

Theorem: vl-lucid-scopestack-subscope-p-of-vl-scopestack-fix-b

(defthm vl-lucid-scopestack-subscope-p-of-vl-scopestack-fix-b
  (equal (vl-lucid-scopestack-subscope-p a (vl-scopestack-fix b))
         (vl-lucid-scopestack-subscope-p a b)))

Theorem: vl-lucid-scopestack-subscope-p-vl-scopestack-equiv-congruence-on-b

(defthm
 vl-lucid-scopestack-subscope-p-vl-scopestack-equiv-congruence-on-b
 (implies (vl-scopestack-equiv b b-equiv)
          (equal (vl-lucid-scopestack-subscope-p a b)
                 (vl-lucid-scopestack-subscope-p a b-equiv)))
 :rule-classes :congruence)