Theorem restrict-loc

• 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, allwritesOK-ind-one-unpersisted-write-no-persisted-after, allwritesOK-ind-persist-one-write, allwritesOK-one-unpersisted-write-no-persisted-after, allwritesOK-persist-one-write, at-overwrite-no-write, first-vol-write-head-restricted, first-vol-write-size, first-vol-write-size2, lastwrite-to-update, nowrites-lastPersistedtrue, overwrite-persist-one-write-restrict-true, persistDependentReads-restrict-empty, persistDependentReads-restrict-other-loc, persistDependentReads-restrict-same-loc, persistDependentReads-restrict-single-W, restrict-l-R-other, restrict-l-R-same, restrict-l-W-other, restrict-l-W-same, restrict-l-append, restrict-l-b-swap, restrict-l-empty, restrict-l-one, restrict-l-t-swap, restrict-t-b-empty-expand-loc, restrict-w-l-swap, take-first-vol-write-no-unpersisted-writes,
• Used by units in proved state: abs-FLITPSCweak-PLIB,
• Proof exists?: No