Used simplifier rules/spec theorems by specification

Used from specification forall-indexWhere

• forall-indexWhere/indexWhere-rec1 is used by first-vol-write-size, first-vol-write-rec-write-unpersisted, take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• forall-indexWhere/indexWhere-rec2 is used by first-vol-write-size, first-vol-write-rec-read, first-vol-write-rec-write-other, first-vol-write-rec-write-persisted, take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• forall-indexWhere/filter-forall2 is used by restrict-b-idem,
• forall-indexWhere/forall-base is used by restrict-b-idem,
• forall-indexWhere/forall-rec is used by restrict-b-idem,
• forall-indexWhere/indexWhere-base is used by first-vol-write-size, take-first-vol-write-no-unpersisted-writes,
• forall-indexWhere/indexWhere-length-ls is used by first-vol-write-size3,
• forall-indexWhere/indexWhere-one is used by first-vol-write-split,

Used from specification nat

• nat/lels is used by first-vol-write-size2,
• nat/le-def is used by allwritesOK-ind-at-most-one-write,
• nat/lels is used by first-vol-write-size, first-vol-write-split,
• nat/lels-02 is used by first-vol-write-size2,
• nat/lez is used by first-vol-write-split,
• nat/lez-01 is used by first-vol-write-split,
• nat/succ-01 is used by first-vol-write-size, first-vol-write-split,

Used from specification list-set

• list-set/subset-app-03 is used by rely-unpersisted-subset,
• list-set/subset-append-01 is used by rely-unpersisted-subset,
• list-set/subset-empty-01 is used by rely-unpersisted-subset,

Used from specification memory

• memory/emptymem is used by allReadsOK-firstreadpersisted, allReadsOK-tailread, allReadsOK-one,

Used from specification list-data

• list-data/elim-add is used by first-vol-write-head-restricted,
• list-data/l is used by first-vol-write-size, hist-more-persisted-size-eq, first-vol-write-split,
• list-data/size-nil is used by first-vol-write-size, hist-more-persisted-size-eq, first-vol-write-split,

Used from specification filter-count

• filter-count/count-zero-filter-nil is used by allwritesOK-ind-at-most-one-write,
• filter-count/filter-swap is used by restrict-t-b-swap, restrict-l-b-swap, restrict-w-t-swap, restrict-w-b-swap, restrict-l-t-swap, restrict-w-l-swap,
• filter-count/count-append is used by allwritesOK-ind-at-most-one-write,
• filter-count/count-base is used by allwritesOK-ind-at-most-one-write,
• filter-count/count-single is used by allwritesOK-ind-at-most-one-write,
• filter-count/count-sizefilter is used by allwritesOK-ind-at-most-one-write,
• filter-count/filter-append is used by restrict-read-attach-W, nowrites-lastPersistedtrue, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, restrict-b-append, restrict-true-false-empty, rely-unpersisted-subset, allReadsOK-ind-no-initial-unpersisted-read, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W, restrict-t-append, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, restrict-W-append, rely-stable-write-one, restrict-l-append, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-at-most-one-write,
• filter-count/filter-base is used by restrict-R-empty, allWritesOK-ind-filter-persisted, rely-persist, persist-dependent-reads-unchanged-writes, nowrites-lastPersistedtrue, allWritesOK-ind-filter-persisted-upd-true, restrict-t-empty, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, overwrite-persist-dependent-reads-restrict-true, allreadsOK-ind-filter-persisted, restrict-true-false-empty, rely-unpersisted-subset, persistDependentReads-restrict-same-loc, restrict-W-empty, allReadsOK-ind-no-initial-unpersisted-read, restrict-b-idem, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, allreadsOK-ind-filter-persisted-upd-false, persistDependentReads-restrict-single-W, allwritesOK-ind-persist-one-write, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, rely-stable-write-one, rely-refl, persistDependentReads-restrict-other-loc, restrict-b-empty, take-first-vol-write-no-unpersisted-writes, restrict-l-empty, allwritesOK-ind-at-most-one-write,
• filter-count/filter-in is used by restrict-t-b-empty-expand-loc, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, allwritesOK-ind-pending-not-in, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-at-most-one-write,
• filter-count/filter-one is used by restrict-read-attach-W, nowrites-lastPersistedtrue, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, restrict-bool-one, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, restrict-t-one, restrict-write-one, restrict-l-one, restrict-true-false-empty, rely-attach, rely-unpersisted-subset, allReadsOK-ind-no-initial-unpersisted-read, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W, restrict-read-one, allwritesOK-ind-persist-one-write, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, rely-stable-write-one, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-at-most-one-write,
• filter-count/filter-rec is used by allWritesOK-ind-filter-persisted, persist-dependent-reads-unchanged-writes, nowrites-lastPersistedtrue, allWritesOK-ind-filter-persisted-upd-true, allwritesOK-ind-add-write, first-vol-write-size, restrict-read-R, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, overwrite-persist-dependent-reads-restrict-true, allreadsOK-ind-filter-persisted, restrict-true-false-empty, rely-unpersisted-subset, persistDependentReads-restrict-same-loc, allReadsOK-ind-no-initial-unpersisted-read, restrict-b-idem, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, allreadsOK-ind-filter-persisted-upd-false, persistDependentReads-restrict-single-W, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, rely-stable-write-one, persistDependentReads-restrict-other-loc, restrict-read-W, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-at-most-one-write,

Used from specification nat-basic

• nat-basic/a is used by lastwrite-to-update, first-vol-write-size, first-vol-write-head-restricted, hist-more-persisted-size-eq, take-first-vol-write-no-unpersisted-writes, first-vol-write-split, allwritesOK-ind-at-most-one-write,
• nat-basic/add-base is used by allwritesOK-ind-at-most-one-write,
• nat-basic/c is used by lastwrite-to-update, first-vol-write-size, first-vol-write-rec-read, first-vol-write-head-restricted, first-vol-write-rec-write-other, hist-more-persisted-size-eq, first-vol-write-rec-write-persisted, take-first-vol-write-no-unpersisted-writes, first-vol-write-split, allwritesOK-ind-at-most-one-write,
• nat-basic/eq-01 is used by hist-more-persisted-size-eq,
• nat-basic/f is used by first-vol-write-size, first-vol-write-split,
• nat-basic/less-zero is used by first-vol-write-size,
• nat-basic/lf is used by first-vol-write-size,
• nat-basic/one is used by allwritesOK-ind-at-most-one-write,
• nat-basic/one-03 is used by allwritesOK-ind-at-most-one-write,
• nat-basic/oz is used by hist-more-persisted-size-eq, allwritesOK-ind-at-most-one-write,
• nat-basic/refl-Nat is used by lastwrite-to-update, first-vol-write-size, first-vol-write-size2,
• nat-basic/s-04 is used by lastwrite-to-update, first-vol-write-size, first-vol-write-split,
• nat-basic/succ is used by first-vol-write-size, hist-more-persisted-size-eq, first-vol-write-split,
• nat-basic/trans-Nat is used by first-vol-write-size,

Used from specification list

• list/lastdiv-rew is used by lastwrite-to-update,
• list/len-01 is used by rely-attach,
• list/some-element is used by restrict-t-b-empty-expand-loc, overwrite-persist-one-write-restrict-true, allwritesOK-ind-pending-not-in, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-at-most-one-write,
• list/Nil is used by allwritesOK-ind-add-read, allWritesOK-ind-filter-persisted, persist-dependent-reads-unchanged-writes, restrict-write-R, allWritesOK-ind-filter-persisted-upd-true, allwritesOK-ind-add-write, first-vol-write-size, overwrite-attach-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, allwritesOK-ind-persist-dependent-reads, restrict-l-R-other, overwrite-persist-dependent-reads-restrict-true, allreadsOK-ind-filter-persisted, hist-more-persisted-append, rely-unpersisted-subset, persistDependentReads-restrict-same-loc, overwrite-persist-dependent-reads, restrict-false-true, allReadsOK-ind-no-initial-unpersisted-read, restrict-b-idem, allwritesOK-ind-one-unpersisted-write-no-persisted-after, allreadsok-ind-add-write, allreadsok-ind-add-read, persistDependentReads-restrict-empty, allreadsOK-ind-filter-persisted-upd-false, persistDependentReads-restrict-single-W, allreadsok-ind-persist, allwritesOK-ind-persist-one-write, overwrite-attach-read, rely-stable-write-one, restrict-true-false, overwrite-persist-one-write, persistDependentReads-restrict-other-loc, restrict-l-W-other, restrict-read-W, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-unpersisted-one-write, first-vol-write-split,
• list/a is used by allwritesOK-ind-add-read, allwritesOK-ind-one, allWritesOK-ind-filter-persisted, lastPersisted-false-ex-persisted-write, rely-persist, allwritesOK-ind-swap-to-non-pending, restrict-true-attach-false, allReadsOK-firstreadpersisted, restrict-false-attach-false, restrict-read-attach-W, persist-dependent-reads-unchanged-writes, restrict-write-R, nowrites-lastPersistedtrue, restrict-true-true, allWritesOK-ind-filter-persisted-upd-true, allreadsok-ind-one, restrict-true-attach-true, hist-more-persisted-persistDependetReads, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allreadsok-add-write, allwritesOK-add-write, restrict-read-R, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-attach-write, restrict-l-R-same, overwrite-persist-one-write-restrict-true, first-vol-write-rec-read, first-vol-write-head-restricted, restrict-l-W-same, allwritesOK-ind-persist-dependent-reads, restrict-l-R-other, restrict-false-attach-true, overwrite-persist-dependent-reads-restrict-true, allreadsOK-ind-filter-persisted, hist-more-persisted-append, restrict-b-append, event-persistDependentReads, at-overwrite-mem-update-other, hist-more-persisted-trans, restrict-true-false-empty, rely-attach, hist-more-persisted-size-eq, rely-unpersisted-subset, allwritesOK-persist-one-write, persistDependentReads-restrict-same-loc, allReadsOK-no-initial-unpersisted-read, overwrite-persist-dependent-reads, restrict-false-true, allReadsOK-ind-no-initial-unpersisted-read, restrict-b-idem, allreadsok-persist, events-append, restrict-write-attach-R, allwritesOK-ind-one-unpersisted-write-no-persisted-after, allreadsok-ind-add-write, allwritesOK-add-read, allreadsok-ind-add-read, persistDependentReads-restrict-empty, allreadsOK-ind-filter-persisted-upd-false, first-vol-write-rec-write-unpersisted, allwritesOK-ind-swap-flags-persist-one-write, persistDependentReads-restrict-single-W, allreadsok-ind-persist, first-vol-write-rec-write-persisted, allReadsOK-tailread, allwritesOK-persist-dependent-reads, allwritesOK-ind-persist-one-write, overwrite-attach-read, restrict-t-append, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, allwritesOK-one-unpersisted-write-no-persisted-after, overwrite-one-read, restrict-W-append, rely-stable-write-one, overwrite-one-write, hist-more-persisted-refl, rely-refl, restrict-true-false, restrict-write-W, overwrite-persist-one-write, restrict-l-append, persistDependentReads-restrict-other-loc, restrict-l-W-other, restrict-read-W, restrict-false-false, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-unpersisted-one-write, first-vol-write-split, allwritesOK-ind-at-most-one-write,
• list/app is used by allwritesOK-ind-one, rely-persist, restrict-true-attach-false, restrict-read-attach-W, allreadsok-ind-one, lastwrite-to-update, restrict-false-attach-true, rely-unpersisted-subset, restrict-write-attach-R, overwrite-one-read, rely-stable-write-one, overwrite-one-write, rely-refl, first-vol-write-split,
• list/app-02 is used by nowrites-lastPersistedtrue, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, restrict-true-false-empty, allReadsOK-ind-no-initial-unpersisted-read, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, allwritesOK-ind-persist-one-write, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, rely-stable-write-one, take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• list/c is used by allwritesOK-ind-add-read, allWritesOK-ind-filter-persisted, lastPersisted-false-ex-persisted-write, allwritesOK-ind-swap-to-non-pending, persist-dependent-reads-unchanged-writes, nowrites-lastPersistedtrue, allWritesOK-ind-filter-persisted-upd-true, hist-more-persisted-persistDependetReads, allwritesOK-ind-add-write, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, hist-ind, allwritesOK-ind-persist-dependent-reads, overwrite-persist-dependent-reads-restrict-true, allreadsOK-ind-filter-persisted, hist-more-persisted-append, event-persistDependentReads, at-overwrite-mem-update-other, hist-more-persisted-trans, restrict-true-false-empty, hist-more-persisted-size-eq, rely-unpersisted-subset, persistDependentReads-restrict-same-loc, overwrite-persist-dependent-reads, allReadsOK-ind-no-initial-unpersisted-read, restrict-b-idem, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, allreadsOK-ind-filter-persisted-upd-false, allwritesOK-ind-swap-flags-persist-one-write, persistDependentReads-restrict-single-W, allreadsok-ind-persist, allwritesOK-ind-persist-one-write, overwrite-attach-read, rely-stable-write-empty, allwritesOK-ind-pending-zero-write, rely-stable-write-one, hist-more-persisted-refl, overwrite-persist-one-write, persistDependentReads-restrict-other-loc, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-unpersisted-one-write, first-vol-write-split, allwritesOK-ind-at-most-one-write,
• list/c-03 is used by persistDependentReads-restrict-single-W, rely-stable-write-one,
• list/c-04 is used by restrict-read-one, events-one, first-vol-write-split,
• list/c-06 is used by first-vol-write-head-restricted, allReadsOK-ind-no-initial-unpersisted-read,
• list/e is used by nowrites-lastPersistedtrue, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, rely-attach, allReadsOK-ind-no-initial-unpersisted-read, allwritesOK-ind-one-unpersisted-write-no-persisted-after, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W, restrict-read-one, allwritesOK-ind-persist-one-write, rely-stable-write-empty, rely-stable-write-one, first-vol-write-split,
• list/in-14 is used by first-vol-write-head-restricted, allReadsOK-ind-no-initial-unpersisted-read,
• list/in-15 is used by rely-attach,
• list/in-17 is used by allReadsOK-ind-no-initial-unpersisted-read,
• list/in-append is used by first-vol-write-head-restricted, rely-attach, allReadsOK-ind-no-initial-unpersisted-read,
• list/in-empty is used by first-vol-write-head-restricted, allReadsOK-ind-no-initial-unpersisted-read,
• list/in-rec is used by lastPersisted-false-ex-persisted-write, first-vol-write-head-restricted, allReadsOK-ind-no-initial-unpersisted-read,
• list/len is used by lastwrite-to-update,
• list/len-01 is used by rely-persist, restrict-false-attach-false, persist-dependent-reads-unchanged-writes, restrict-true-true, restrict-true-attach-true, restrict-read-R, restrict-l-R-same, restrict-l-W-same, restrict-b-append, event-persistDependentReads, persistDependentReads-restrict-same-loc, events-append, restrict-t-append, restrict-W-append, restrict-write-W, restrict-l-append, persistDependentReads-restrict-other-loc, restrict-false-false, first-vol-write-split,
• list/len-02 is used by lastwrite-to-update,
• list/len-05 is used by first-vol-write-size, hist-more-persisted-size-eq, first-vol-write-split,
• list/len-06 is used by first-vol-write-split,
• list/map-append is used by allReadsOK-ind-no-initial-unpersisted-read, events-append,
• list/map-base is used by event-persistDependentReads, allReadsOK-ind-no-initial-unpersisted-read, events-empty,
• list/map-one is used by allReadsOK-ind-no-initial-unpersisted-read, events-one,
• list/map-rec is used by event-persistDependentReads,
• list/one-01 is used by rely-stable-write-one,

Used from specification RWevent

• RWevent/ex-dotWque is used by first-vol-write-split,
• RWevent/disj-R-W is used by first-vol-write-head-restricted, persistDependentReads-restrict-single-W,
• RWevent/elim-W is used by nowrites-lastPersistedtrue, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, allwritesOK-ind-one-unpersisted-write-no-persisted-after, allwritesOK-ind-pending-zero-write, take-first-vol-write-no-unpersisted-writes, allwritesOK-ind-at-most-one-write,
• RWevent/inj-R is used by hist-more-persisted-persistDependetReads,
• RWevent/inj-W is used by first-vol-write-head-restricted,
• RWevent/sel-R-dotl is used by allreadsok-ind-one, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, restrict-l-R-same, first-vol-write-rec-read, restrict-l-R-other, persistDependentReads-restrict-same-loc, allReadsOK-ind-no-initial-unpersisted-read, allreadsok-ind-add-read, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W, persistDependentReads-restrict-other-loc, take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• RWevent/sel-R-dott is used by allwritesOK-ind-add-write, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W,
• RWevent/sel-R-dotv is used by allreadsok-ind-one, allreadsok-ind-add-read, allReadsOK-one,
• RWevent/sel-W-dotl is used by allwritesOK-ind-one, lastPersisted-false-ex-persisted-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, restrict-l-W-same, first-vol-write-rec-write-other, persistDependentReads-restrict-same-loc, allReadsOK-ind-no-initial-unpersisted-read, persistDependentReads-restrict-empty, first-vol-write-rec-write-unpersisted, persistDependentReads-restrict-single-W, first-vol-write-rec-write-persisted, allwritesOK-ind-persist-one-write, persistDependentReads-restrict-other-loc, restrict-l-W-other, take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• RWevent/sel-W-dott is used by allwritesOK-ind-one, allwritesOK-ind-add-write, allwritesOK-ind-pending-not-in, persistDependentReads-restrict-empty, persistDependentReads-restrict-single-W, allwritesOK-ind-at-most-one-write,
• RWevent/sel-W-dotv is used by allReadsOK-one,
• RWevent/test-dotRque-R is used by allwritesOK-ind-add-read, allwritesOK-ind-one, allreadsok-ind-one, restrict-read-R, allwritesOK-one, allreadsok-ind-add-read, restrict-read-one, allReadsOK-one,
• RWevent/test-dotRque-W is used by allwritesOK-ind-one, restrict-read-attach-W, allwritesOK-ind-add-write, allwritesOK-one, restrict-read-one, allReadsOK-one, restrict-read-W,
• RWevent/test-dotWque-R is used by persist-dependent-reads-unchanged-writes, restrict-write-R, nowrites-lastPersistedtrue, allreadsok-ind-one, lastwrite-to-update, first-vol-write-size, at-overwrite-no-write, first-vol-write-rec-read, first-vol-write-head-restricted, restrict-write-attach-R, allreadsok-ind-add-read, restrict-read-one, allwritesOK-ind-persist-one-write, take-first-vol-write-no-unpersisted-writes, first-vol-write-split, allwritesOK-ind-at-most-one-write,
• RWevent/test-dotWque-W is used by allwritesOK-ind-one, persist-dependent-reads-unchanged-writes, nowrites-lastPersistedtrue, allreadsok-ind-one, allwritesOK-ind-add-write, lastwrite-to-update, first-vol-write-size, allReadsOK-nowrites-allpersisted-ind, at-overwrite-no-write, overwrite-persist-one-write-restrict-true, first-vol-write-head-restricted, allwritesOK-ind-pending-not-in, allwritesOK-one, allwritesOK-ind-one-unpersisted-write-no-persisted-after, allreadsok-ind-add-write, first-vol-write-rec-write-unpersisted, first-vol-write-rec-write-persisted, restrict-read-one, allwritesOK-ind-persist-one-write, restrict-write-W, allReadsOK-one, take-first-vol-write-no-unpersisted-writes, first-vol-write-split, allwritesOK-ind-at-most-one-write,

Used from specification list-del

• list-del/firstN-zero is used by take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• list-del/get-succ is used by first-vol-write-head-restricted,
• list-del/get-zero is used by first-vol-write-head-restricted,
• list-del/restN-zero is used by first-vol-write-split,
• list-del/weak-firstN-rec is used by take-first-vol-write-no-unpersisted-writes, first-vol-write-split,
• list-del/weak-restN-rec is used by first-vol-write-split,