w

(in-package "ACL2")

(defsection std/system/w
  :parents (std/system)
  :short "Theorems about @(tsee w)."
  (defthm plist-worldp-of-w-when-state-p
    (implies (state-p state) (plist-worldp (w state)))
    :hints (("Goal" :in-theory (enable state-p)))))