iprint-oracle-updates

Included Books

other

(in-package "ACL2")

local

(local (include-book "kestrel/utilities/state" :dir :system))

local

(local (include-book "kestrel/utilities/read-acl2-oracle" :dir :system))

local

(local (include-book "channels"))

open-input-channels-of-iprint-oracle-updatestheorem

(defthm open-input-channels-of-iprint-oracle-updates
  (equal (open-input-channels (iprint-oracle-updates state))
    (open-input-channels state))
  :hints (("Goal" :in-theory (e/d (iprint-oracle-updates) (nfix)))))

state-p1-of-iprint-oracle-updatestheorem

(defthm state-p1-of-iprint-oracle-updates
  (implies (state-p1 state)
    (state-p1 (iprint-oracle-updates state)))
  :hints (("Goal" :in-theory (e/d (iprint-oracle-updates)
       (array1p iprint-last-index* nfix)))))

state-p-of-iprint-oracle-updatestheorem

(defthm state-p-of-iprint-oracle-updates
  (implies (state-p state)
    (state-p (iprint-oracle-updates state)))
  :hints (("Goal" :in-theory (e/d (iprint-oracle-updates)
       (array1p iprint-last-index* nfix)))))