read-acl2-oracle

(in-package "OSLIB")

(local (in-theory (enable read-acl2-oracle)))

(defthm booleanp-of-read-acl2-oracle
  (booleanp (mv-nth 0 (read-acl2-oracle state)))
  :rule-classes :type-prescription)

(defthm state-p1-of-read-acl2-oracle
  (implies (force (state-p1 state))
    (state-p1 (mv-nth 2 (read-acl2-oracle state)))))

(defthm w-state-of-read-acl2-oracle
  (equal (w (mv-nth 2 (read-acl2-oracle state)))
    (w state))
  :hints (("Goal" :in-theory (enable update-acl2-oracle))))