Theorem restrict-vp

• Type: An axiom
• Validity: The proof is valid.
• Features: ls,
• Comment:
• Used by: allReadsOK-ind-no-initial-unpersisted-read, allReadsOK-no-initial-unpersisted-read, allReadsOK-nowrites-allpersisted, allReadsOK-nowrites-allpersisted-ind, allreadsOK-filter-persisted, allwritesOK-add-write, allwritesOK-filter-persisted, allwritesOK-ind-add-write, allwritesOK-ind-at-most-one-write, allwritesOK-ind-one-unpersisted-write-no-persisted-after, allwritesOK-ind-pending-not-in, allwritesOK-ind-pending-zero-write, allwritesOK-ind-persist-one-write, allwritesOK-one-unpersisted-write-no-persisted-after, allwritesOK-persist-one-write, first-vol-write-head-restricted, first-vol-write-size, first-vol-write-size2, lastwrite-to-update, nowrites-lastPersistedtrue, overwrite-persist-dependent-reads-restrict-true, overwrite-persist-one-write-restrict-true, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W, rely-stable-write-empty, rely-stable-write-one, rely-unpersisted-subset, restrict-b-append, restrict-b-empty, restrict-b-idem, restrict-bool-one, restrict-false-attach-false, restrict-false-attach-true, restrict-false-false, restrict-false-true, restrict-l-b-swap, restrict-t-b-empty-expand-loc, restrict-t-b-swap, restrict-true-attach-false, restrict-true-attach-true, restrict-true-false, restrict-true-false-empty, restrict-true-true, restrict-w-b-swap, take-first-vol-write-no-unpersisted-writes,
• Used by units in proved state: abs-FLITPSCweak-PLIB,
• Proof exists?: No