		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstates-compatible

Signature
(svstates-compatible x y) → *
Arguments: x — Guard (svstate-p x).; y — Guard (svstate-p y).

Definitions and Theorems

Function: svstates-compatible

(defun svstates-compatible (x y)
  (declare (xargs :guard (and (svstate-p x) (svstate-p y))))
  (let ((__function__ 'svstates-compatible))
    (declare (ignorable __function__))
    (svstacks-compatible (svstate->blkst x)
                         (svstate->blkst y))))

Theorem: svstates-compatible-is-an-equivalence

(defthm svstates-compatible-is-an-equivalence
  (and (booleanp (svstates-compatible x y))
       (svstates-compatible x x)
       (implies (svstates-compatible x y)
                (svstates-compatible y x))
       (implies (and (svstates-compatible x y)
                     (svstates-compatible y z))
                (svstates-compatible x z)))
  :rule-classes (:equivalence))

Theorem: svstates-compatible-implies-svstacks-compatible-svstate->blkst-1

(defthm
   svstates-compatible-implies-svstacks-compatible-svstate->blkst-1
  (implies (svstates-compatible x x-equiv)
           (svstacks-compatible (svstate->blkst x)
                                (svstate->blkst x-equiv)))
  :rule-classes (:congruence))

Theorem: svstacks-compatible-implies-svstates-compatible-svstate-1

(defthm svstacks-compatible-implies-svstates-compatible-svstate-1
  (implies (svstacks-compatible blkst blkst-equiv)
           (svstates-compatible (svstate blkst nonblkst)
                                (svstate blkst-equiv nonblkst)))
  :rule-classes (:congruence))

Theorem: svstate-normalize-nonblkst-under-svstates-compatible

(defthm svstate-normalize-nonblkst-under-svstates-compatible
  (implies (syntaxp (not (and (equal nonblkst ''nil))))
           (svstates-compatible (svstate blkst nonblkst)
                                (svstate blkst nil))))

Theorem: svstate-reconstruct-under-svstates-compatible

(defthm svstate-reconstruct-under-svstates-compatible
  (svstates-compatible (svstate (svstate->blkst st) nonblkst)
                       st))

Theorem: svstates-compatible-blkst-of-svstate-fork

(defthm svstates-compatible-blkst-of-svstate-fork
  (svstates-compatible (svstate-fork x)
                       (double-rewrite x)))

Theorem: svstates-compatible-of-svstate-fix-x

(defthm svstates-compatible-of-svstate-fix-x
  (equal (svstates-compatible (svstate-fix x) y)
         (svstates-compatible x y)))

Theorem: svstates-compatible-svstate-equiv-congruence-on-x

(defthm svstates-compatible-svstate-equiv-congruence-on-x
  (implies (svstate-equiv x x-equiv)
           (equal (svstates-compatible x y)
                  (svstates-compatible x-equiv y)))
  :rule-classes :congruence)

Theorem: svstates-compatible-of-svstate-fix-y

(defthm svstates-compatible-of-svstate-fix-y
  (equal (svstates-compatible x (svstate-fix y))
         (svstates-compatible x y)))

Theorem: svstates-compatible-svstate-equiv-congruence-on-y

(defthm svstates-compatible-svstate-equiv-congruence-on-y
  (implies (svstate-equiv y y-equiv)
           (equal (svstates-compatible x y)
                  (svstates-compatible x y-equiv)))
  :rule-classes :congruence)