		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-nonempty-fix

Signature
(svstack-nonempty-fix x) → new-x
Arguments: x — Guard (svstack-p x).
Returns: new-x — Type (svstack-p new-x).

Definitions and Theorems

Function: svstack-nonempty-fix

(defun svstack-nonempty-fix (x)
  (declare (xargs :guard (svstack-p x)))
  (let ((__function__ 'svstack-nonempty-fix))
    (declare (ignorable __function__))
    (b* ((x (svstack-fix x)))
      (if (atom x) (list nil) x))))

Theorem: svstack-p-of-svstack-nonempty-fix

(defthm svstack-p-of-svstack-nonempty-fix
  (b* ((new-x (svstack-nonempty-fix x)))
    (svstack-p new-x))
  :rule-classes :rewrite)

Theorem: consp-of-svstack-nonempty-fix

(defthm consp-of-svstack-nonempty-fix
  (b* ((?new-x (svstack-nonempty-fix x)))
    (consp new-x)))

Theorem: svstack-nonempty-fix-when-consp

(defthm svstack-nonempty-fix-when-consp
  (b* nil
    (implies (consp x)
             (equal (svstack-nonempty-fix x)
                    (svstack-fix x)))))

Theorem: svstack-nonempty-fix-of-svstack-fix-x

(defthm svstack-nonempty-fix-of-svstack-fix-x
  (equal (svstack-nonempty-fix (svstack-fix x))
         (svstack-nonempty-fix x)))

Theorem: svstack-nonempty-fix-svstack-equiv-congruence-on-x

(defthm svstack-nonempty-fix-svstack-equiv-congruence-on-x
  (implies (svstack-equiv x x-equiv)
           (equal (svstack-nonempty-fix x)
                  (svstack-nonempty-fix x-equiv)))
  :rule-classes :congruence)