		Search-engine friendly clone of the ACL2 documentation.

States32i

Stat32i-iso

Isomorphism between stat-rv32i-p and stat32i.

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

Definitions and Theorems

Theorem: stat32i-iso.alpha-image

(defthm stat32i-iso.alpha-image
  (implies (stat-rv32i-p stat)
           (stat32ip (stat32i-from-stat stat))))

Theorem: stat32i-iso.beta-image

(defthm stat32i-iso.beta-image
  (implies (stat32ip stat32i)
           (stat-rv32i-p (stat-from-stat32i stat32i))))

Theorem: stat-from-stat32i-of-stat32i-from-stat

(defthm stat-from-stat32i-of-stat32i-from-stat
  (implies (stat-rv32i-p stat)
           (equal (stat-from-stat32i (stat32i-from-stat stat))
                  stat)))

Theorem: stat32i-from-stat-of-stat-from-stat32i

(defthm stat32i-from-stat-of-stat-from-stat32i
  (implies (stat32ip stat32i)
           (equal (stat32i-from-stat (stat-from-stat32i stat32i))
                  stat32i)))

Theorem: stat32i-iso.doma-guard

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

Theorem: stat32i-iso.domb-guard

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

Theorem: stat32i-iso.alpha-guard

(defthm stat32i-iso.alpha-guard
  (implies (stat-rv32i-p stat)
           (stat-rv32i-p stat)))

Theorem: stat32i-iso.beta-guard

(defthm stat32i-iso.beta-guard
  (implies (stat32ip stat32i)
           (stat32ip stat32i)))

Theorem: stat32i-from-stat-injective

(defthm stat32i-from-stat-injective
  (implies (and (stat-rv32i-p stat)
                (stat-rv32i-p stat$))
           (equal (equal (stat32i-from-stat stat)
                         (stat32i-from-stat stat$))
                  (equal stat stat$))))

Theorem: stat-from-stat32i-injective

(defthm stat-from-stat32i-injective
  (implies (and (stat32ip stat32i)
                (stat32ip stat32i$))
           (equal (equal (stat-from-stat32i stat32i)
                         (stat-from-stat32i stat32i$))
                  (equal stat32i stat32i$))))