read-acl2-oracle - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "update-acl2-oracle"))

in-theory

(in-theory (disable read-acl2-oracle))

state-p1-of-mv-nth-2-of-read-acl2-oracletheorem

(defthm state-p1-of-mv-nth-2-of-read-acl2-oracle
  (implies (state-p1 state)
    (state-p1 (mv-nth 2 (read-acl2-oracle state))))
  :hints (("Goal" :in-theory (enable read-acl2-oracle state-p1 open-output-channels))))

open-input-channels-of-mv-nth-2-of-read-acl2-oracletheorem

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

w-of-mv-nth-2-of-read-acl2-oracletheorem

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