		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat1-iso

Isomorphism between stat and stat1.

The stat1-from-stat and stat-from-stat1 functions are the isomorphic conversions.

We prove a local lemma to prove stat1-from-stat-of-stat-from-stat1.

Definitions and Theorems

Theorem: stat-stat1-iso.alpha-image

(defthm stat-stat1-iso.alpha-image
  (implies (statp stat)
           (stat1p (stat1-from-stat stat))))

Theorem: stat-stat1-iso.beta-image

(defthm stat-stat1-iso.beta-image
  (implies (stat1p stat1)
           (statp (stat-from-stat1 stat1))))

Theorem: stat-from-stat1-of-stat1-from-stat

(defthm stat-from-stat1-of-stat1-from-stat
  (implies (statp stat)
           (equal (stat-from-stat1 (stat1-from-stat stat))
                  stat)))

Theorem: stat1-from-stat-of-stat-from-stat1

(defthm stat1-from-stat-of-stat-from-stat1
  (implies (stat1p stat1)
           (equal (stat1-from-stat (stat-from-stat1 stat1))
                  stat1)))

Theorem: stat-stat1-iso.doma-guard

(defthm stat-stat1-iso.doma-guard
  t
  :rule-classes nil)

Theorem: stat-stat1-iso.domb-guard

(defthm stat-stat1-iso.domb-guard
  t
  :rule-classes nil)

Theorem: stat-stat1-iso.alpha-guard

(defthm stat-stat1-iso.alpha-guard
  (implies (statp stat) (statp stat)))

Theorem: stat-stat1-iso.beta-guard

(defthm stat-stat1-iso.beta-guard
  (implies (stat1p stat1)
           (and (stat1p stat1) (stat1p stat1))))

Theorem: stat1-from-stat-injective

(defthm stat1-from-stat-injective
  (implies (and (statp stat) (statp stat$))
           (equal (equal (stat1-from-stat stat)
                         (stat1-from-stat stat$))
                  (equal stat stat$))))

Theorem: stat-from-stat1-injective

(defthm stat-from-stat1-injective
  (implies (and (stat1p stat1) (stat1p stat1$))
           (equal (equal (stat-from-stat1 stat1)
                         (stat-from-stat1 stat1$))
                  (equal stat1 stat1$))))