Used simplifier rules/spec theorems by specification

Used from specification forall-indexWhere

• forall-indexWhere/indexWhere-base is used by absloc-persist-firstPersistW,

Used from specification nat

• nat/lels is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO,
• nat/lez is used by abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO,
• nat/succ-01 is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO,

Used from specification FLITPSC-preds

• FLITPSC-preds/ctrok-def is used by counterzero,
• FLITPSC-preds/filtertid-def is used by counterzero,
• FLITPSC-preds/filterwrites-def is used by counterzero, abs-leading-write-h-restricted-non-empty,
• FLITPSC-preds/noPendingW is used by abs-single-FO-no-pending, abs-leading-last-FO-one-pending, abs-single-FO-one-pending, abs-leading-last-FO-no-pending,
• FLITPSC-preds/onePendingW is used by abs-leading-last-FO-one-pending, abs-single-FO-one-pending,
• FLITPSC-preds/writersOk is used by counterzero,
• FLITPSC-preds/filter-W-append is used by absloc-nowritesp-nowritesh, abs-loc-no-w-last-firstfo-then-no-pending, absloc-addReadFO, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-addWrite, absloc-no-W-leading-W, absloc-addWriteFO,
• FLITPSC-preds/filter-W-one-fo is used by absloc-nowritesp-nowritesh, abs-loc-no-w-last-firstfo-then-no-pending, absloc-addReadFO, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-addWrite, absloc-no-W-leading-W, absloc-addWriteFO,
• FLITPSC-preds/filter-W-one-w is used by absloc-nowritesp-nowritesh, abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-addWrite, absloc-no-W-leading-W,
• FLITPSC-preds/filter-t-append is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-no-W-leading-W,
• FLITPSC-preds/filter-t-one is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-no-W-leading-W,
• FLITPSC-preds/filter-tid-empty is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-no-W-leading-W,
• FLITPSC-preds/filter-w-empty is used by absloc-nowritesp-nowritesh, abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-recW-W-one3, absloc-addWrite, absloc-no-W-leading-W,
• FLITPSC-preds/filter-w-fo is used by abs-leading-last-FO-one-pending, abs-leading-last-FO-no-pending, absloc-prepend-FO, absloc-persistfirstFO,
• FLITPSC-preds/filter-w-write is used by abs-firstVolWrite-head,
• FLITPSC-preds/in-filter-W is used by counterzero,
• FLITPSC-preds/one-pending-no-fo-no-pending is used by abs-leading-last-FO-one-pending,
• FLITPSC-preds/oplus-same-writes-eq is used by abs-apply-firstPersistW, abs-apply-persist-FO,
• FLITPSC-preds/oplus-v-append is used by abs-apply-firstPersistW, abs-apply-persist-FO,
• FLITPSC-preds/oplus-v-one-FO is used by abs-apply-firstPersistW, abs-apply-persist-FO,
• FLITPSC-preds/oplus-v-one-W is used by abs-apply-firstPersistW, abs-apply-persist-FO,
• FLITPSC-preds/overwrite-def is used by abs-apply-firstPersistW,
• FLITPSC-preds/overwrite-rec1 is used by abs-apply-firstPersistW,

Used from specification PLIB-preds

• PLIB-preds/allReadsOK-def is used by abs-single-FO-no-pending, abs-leading-last-FO-one-pending, abs-single-FO-one-pending, abs-leading-last-FO-no-pending,
• PLIB-preds/allReadsOK-nowrites-allpersisted is used by abs-h-p-nowritesh-allpersisted-aux, pofl-empty-all-l-persisted,
• PLIB-preds/first-vol-write-rec-write-other is used by absloc-persist-firstPersistW,
• PLIB-preds/first-vol-write-split is used by abs-persist-firstPersistW, abs-persistWrite,
• PLIB-preds/firstVolWrite-def is used by absloc-persist-firstPersistW,
• PLIB-preds/nowrites-lastPersistedtrue is used by abs-h-p-nowritesh-lastPersisted,
• PLIB-preds/restrict-R is used by abs-addWriteFO,
• PLIB-preds/restrict-events is used by abs-addWriteFO,
• PLIB-preds/restrict-loc is used by abs-addWriteFO,
• PLIB-preds/restrict-t-b-swap is used by abs-h-p-nowritesh-allpersisted-aux,
• PLIB-preds/restrict-thread is used by abs-addWriteFO,
• PLIB-preds/restrict-vp is used by abs-addWriteFO,
• PLIB-preds/restrict-w-b-swap is used by abs-h-p-nowritesh-lastPersisted,
• PLIB-preds/restrict-w-l-swap is used by abs-h-p-nowritesh-lastPersisted,
• PLIB-preds/allReadsOK-ind-no-initial-unpersisted-read is used by abs-loc-no-w-last-fo-then-no-pending,
• PLIB-preds/allReadsOK-no-initial-unpersisted-read is used by abs-persistFO-weak, abs-persistFO,
• PLIB-preds/allReadsOKInd-recR is used by abs-loc-no-w-last-firstfo-then-no-pending,
• PLIB-preds/allReadsOKInd-recW is used by abs-loc-no-w-last-firstfo-then-no-pending,
• PLIB-preds/events-append is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/events-empty is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-h-p-nowritesh-allpersisted-aux, abs-noReadFO, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/events-one is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/first-vol-write-rec-read is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, absloc-persist-firstPersistW, abs-firstVolWrite-head,
• PLIB-preds/first-vol-write-rec-write-other is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-firstVolWrite-head,
• PLIB-preds/first-vol-write-rec-write-persisted is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, absloc-persist-firstPersistW, abs-firstVolWrite-head,
• PLIB-preds/first-vol-write-rec-write-unpersisted is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, absloc-persist-firstPersistW, abs-firstVolWrite-head,
• PLIB-preds/first-vol-write-size is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-persist-firstPersistW, abs-persistWrite,
• PLIB-preds/persistDependentReads-base is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/persistDependentReads-nextwrite is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/persistDependentReads-otherread is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/persistDependentReads-otherwrite is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/persistDependentReads-read is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/persistDependentReads-restrict-other-loc is used by abs-persist-firstPersistW, abs-persistWrite,
• PLIB-preds/restrict-W-append is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-W-empty is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-h-p-nowritesh-lastPersisted, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-b-append is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-b-empty is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-bool-one is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-false-false is used by absloc-persist-DependentReads, abs-persistWrite,
• PLIB-preds/restrict-false-true is used by absloc-persist-firstPersistW, absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/restrict-l-R-other is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/restrict-l-R-same is used by absloc-persist-DependentReads, absloc-persistWrite,
• PLIB-preds/restrict-l-W-other is used by absloc-persist-firstPersistW, absloc-persist-DependentReads, absloc-persistWrite, abs-persistWrite,
• PLIB-preds/restrict-l-W-same is used by absloc-persist-firstPersistW, absloc-persist-DependentReads, absloc-persistWrite, abs-persistWrite,
• PLIB-preds/restrict-l-append is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-l-empty is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-loc-no-w-no-fo-then-no-pending, abs-firstVolWrite-head, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-l-one is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• PLIB-preds/restrict-t-append is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending,
• PLIB-preds/restrict-t-empty is used by abs-h-p-nowritesh-allpersisted-aux, abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending,
• PLIB-preds/restrict-t-one is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending,
• PLIB-preds/restrict-write-one is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-firstPersistW-is-in-hist,
• PLIB-preds/take-first-vol-write-no-unpersisted-writes is used by abs-persistWrite,

Used from specification set-basic

• set-basic/In-empty is used by counterzero,
• set-basic/In-insert is used by absloc-addReader, absloc-addReadReader,
• set-basic/Size-empty is used by counterzero,
• set-basic/ne-01 is used by abs-noReadFO, absloc-addRead, absloc-addReadFO, counterzero, abs-addReadFO, absloc-addWrite, abs-addRead,
• set-basic/size-zero-01 is used by abs-noReadFO, absloc-addRead, absloc-addReadFO, abs-addReadFO, absloc-addWrite, abs-addRead,
• set-basic/size-zero-02 is used by counterzero,

Used from specification nat-basic

• nat-basic/a is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, absloc-persist-leading-firstPersistW, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persist-firstPersistW, absloc-persistFO, abs-persist-firstPersistW, abs-loc-no-w-last-fo-then-no-pending, abs-firstVolWrite-head,
• nat-basic/c is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, absloc-persist-leading-firstPersistW, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persist-firstPersistW, absloc-persistFO, abs-persist-firstPersistW, abs-loc-no-w-last-fo-then-no-pending, abs-firstVolWrite-head,
• nat-basic/f is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persist-firstPersistW, abs-persist-firstPersistW, abs-firstPersistW-is-in-hist,
• nat-basic/less-zero is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h,
• nat-basic/refl-Nat is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-firstPersistW-is-in-hist,
• nat-basic/s-04 is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO,
• nat-basic/succ is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending,

Used from specification list

• list/some-element is used by abs-addWriteFO, counterzero,
• list/Nil is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, absloc-addRead, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-addReadFO, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, absloc-addWrite, abs-firstVolWrite-head, absloc-addWriteFO, absloc-addReadReader, abs-firstPersistW-is-in-hist,
• list/a is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, absloc-persist-leading-firstPersistW, absloc-addRead, abs-apply-firstPersistW, absloc-recW-FO-one3, abs-apply-persist-FO, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, abs-addWriteFO, absloc-recW-W-one2, absloc-addReader, absloc-addReadFO, absloc-recR-one, absloc-recW-W-one, absloc-recW-empty-one, absloc-persist-DependentReads, absloc-persistFO, abs-persist-firstPersistW, abs-loc-no-w-last-fo-then-no-pending, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-addReadFO, abs-loc-no-w-no-fo-then-no-pending, abs-persistFO-weak, abs-leading-last-FO-one-pending, absloc-recW-FO-one, absloc-recW-W-one3, absloc-addWrite, abs-addReadReader, abs-firstVolWrite-head, absloc-recW-FO-one2, abs-addRead, absloc-no-W-leading-W, absloc-addWriteFO, abs-leading-last-FO-no-pending, abs-persistFO, absloc-prepend-FO, absloc-addReadReader, abs-firstPersistW-is-in-hist, absloc-persistfirstFO,
• list/app is used by absloc-recW-FO-one3, absloc-recW-W-one2, absloc-addReadFO, absloc-recR-one, absloc-recW-W-one, absloc-recW-empty-one, abs-addWrite, absloc-recW-FO-one, absloc-recW-W-one3, abs-addReadReader, absloc-recW-FO-one2, abs-addRead, absloc-addWriteFO,
• list/app-02 is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-loc-no-w-no-fo-then-no-pending, abs-persistFO-weak, absloc-addWrite, abs-firstVolWrite-head, absloc-no-W-leading-W, abs-persistFO, abs-firstPersistW-is-in-hist, absloc-persistfirstFO,
• list/c is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, absloc-persist-leading-firstPersistW, absloc-addRead, abs-apply-firstPersistW, abs-apply-persist-FO, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, absloc-addReader, absloc-addReadFO, absloc-persist-DependentReads, absloc-persistFO, abs-persist-firstPersistW, abs-loc-no-w-last-fo-then-no-pending, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-persistFO-weak, absloc-addWrite, abs-firstVolWrite-head, absloc-no-W-leading-W, absloc-addWriteFO, abs-persistFO, absloc-prepend-FO, absloc-addReadReader, abs-firstPersistW-is-in-hist, absloc-persistfirstFO,
• list/c-08 is used by absloc-persistFO, absloc-persistfirstFO,
• list/e is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-loc-no-w-no-fo-then-no-pending, abs-persistFO-weak, absloc-addWrite, abs-firstVolWrite-head, absloc-no-W-leading-W, abs-persistFO, absloc-persistfirstFO,
• list/in-06 is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending,
• list/in-14 is used by abs-loc-no-w-last-fo-then-no-pending, abs-leading-write-h-restricted-non-empty, abs-persistWrite, abs-persistFO-weak, abs-leading-last-FO-one-pending, abs-firstVolWrite-head, abs-leading-last-FO-no-pending, abs-persistFO,
• list/in-17 is used by absloc-addReadFO, absloc-addWrite, absloc-addWriteFO,
• list/in-append is used by absloc-addReadFO, absloc-addWrite, absloc-addWriteFO,
• list/in-empty is used by abs-loc-no-w-last-fo-then-no-pending, absloc-addWrite,
• list/in-rec is used by abs-loc-no-w-last-fo-then-no-pending, absloc-persistWrite, abs-persistFO-weak, abs-firstVolWrite-head, absloc-addWriteFO, abs-persistFO, absloc-prepend-FO, absloc-persistfirstFO,
• list/len-05 is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW, abs-apply-persist-FO,
• list/map-in is used by abs-addWriteFO,

Used from specification RWevent

• RWevent/disj-R-W is used by absloc-addWriteFO,
• RWevent/elim-R is used by absloc-addWriteFO,
• RWevent/elim-W is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-leading-write-h-restricted-non-empty, abs-firstPersistW-is-in-hist,
• RWevent/inj-R is used by absloc-addWriteFO,
• RWevent/sel-R-dotl is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-firstPersistW, abs-addWriteFO, absloc-persist-DependentReads, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-loc-no-w-no-fo-then-no-pending, abs-addReadReader, abs-firstVolWrite-head, abs-addRead, abs-firstPersistW-is-in-hist,
• RWevent/sel-R-dott is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-addWriteFO, abs-loc-no-w-no-fo-then-no-pending, absloc-addWriteFO,
• RWevent/sel-W-dotl is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-loc-no-w-last-firstfo-then-no-pending, absloc-persist-DependentReads, abs-persist-firstPersistW, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-addWrite, abs-persistWrite, abs-loc-no-w-no-fo-then-no-pending, abs-firstVolWrite-head, abs-firstPersistW-is-in-hist,
• RWevent/sel-W-dott is used by abs-loc-no-w-last-firstfo-then-no-pending, abs-addWriteFO, abs-loc-no-w-no-fo-then-no-pending,
• RWevent/sel-W-dotv is used by abs-firstPersistW-is-firstVolWrite, abs-apply-firstPersistW,
• RWevent/test-dotRque-R is used by abs-addWriteFO, absloc-persistFO, absloc-addWriteFO, absloc-persistfirstFO,
• RWevent/test-dotRque-W is used by abs-addWriteFO, absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending, abs-persistFO-weak, abs-persistFO, absloc-persistfirstFO,
• RWevent/test-dotWque-R is used by absloc-nowritesp-nowritesh, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-firstPersistW-is-in-hist,
• RWevent/test-dotWque-W is used by absloc-nowritesp-nowritesh, abs-firstPersistW-in-p-when-firstVolWrite-in-h, absloc-persistWrite, abs-leading-write-h-restricted-non-empty, abs-firstPersistW-is-in-hist,

Used from specification FOW

• FOW/ex-dotFOque is used by abs-apply-persist-FO,
• FOW/disj-FO-W is used by abs-loc-no-w-last-firstfo-then-no-pending, absloc-persistWrite, abs-loc-no-w-no-fo-then-no-pending, absloc-addWrite, abs-firstVolWrite-head,
• FOW/elim-FO is used by abs-loc-no-w-last-fo-then-no-pending,
• FOW/inj-FO is used by abs-loc-no-w-last-firstfo-then-no-pending, absloc-addReadFO, abs-loc-no-w-last-fo-then-no-pending, abs-loc-no-w-no-fo-then-no-pending, absloc-addWriteFO, absloc-prepend-FO, absloc-persistfirstFO,
• FOW/sel-FO-dottid is used by absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending,
• FOW/sel-W-dottid is used by abs-loc-no-w-last-firstfo-then-no-pending, counterzero, abs-loc-no-w-no-fo-then-no-pending, absloc-no-W-leading-W,
• FOW/sel-W-dotval is used by abs-firstPersistW-is-firstVolWrite,
• FOW/test-dotFOque-FO is used by absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending,
• FOW/test-dotWque-FO is used by counterzero,
• FOW/test-dotWque-W is used by counterzero, abs-leading-write-h-restricted-non-empty,

Used from specification set-union

• set-union/Delete is used by absloc-addReadFO,

Used from specification FLITPSCweak-preds

• FLITPSCweak-preds/firstPersistW-base is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h,
• FLITPSCweak-preds/firstPersistW-lt-filter-W-empty is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-firstPersistW-is-in-hist,
• FLITPSCweak-preds/firstPersistW-rec-FO is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, absloc-persist-leading-firstPersistW, abs-apply-firstPersistW,
• FLITPSCweak-preds/firstPersistW-rec-W is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h, abs-firstPersistW-is-firstVolWrite, absloc-persist-leading-firstPersistW, abs-apply-firstPersistW,
• FLITPSCweak-preds/fo-in-del-firstPersistW is used by absloc-persist-firstPersistW,
• FLITPSCweak-preds/isPersistFO-del-no-W-stable is used by absloc-persistFO, abs-single-FO-no-pending, abs-loc-no-w-last-fo-then-no-pending, abs-single-FO-one-pending,
• FLITPSCweak-preds/isPersistFO-leading-W is used by absloc-persistFO,
• FLITPSCweak-preds/isPersistFO-rec is used by absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending,
• FLITPSCweak-preds/one-pending-del-persist-FO-no-pending is used by abs-single-FO-one-pending,

Used from specification list-data

• list-data/elim-add is used by abs-loc-no-w-last-fo-then-no-pending, abs-persistFO-weak, abs-persistFO,
• list-data/l is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persist-firstPersistW, abs-persist-firstPersistW, abs-firstPersistW-is-in-hist,
• list-data/size-nil is used by abs-firstPersistW-in-p-when-firstVolWrite-in-h,

Used from specification filter-count

• filter-count/filter-in is used by abs-addWriteFO, counterzero,
• filter-count/filter-rec is used by abs-leading-write-h-restricted-non-empty,

Used from specification list-del

• list-del/delpos-atsizeid is used by abs-apply-firstPersistW,
• list-del/delpos-base is used by absloc-persist-leading-firstPersistW, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending,
• list-del/delpos-get-fw is used by abs-loc-no-w-last-fo-then-no-pending, abs-single-FO-one-pending,
• list-del/delpos-rec is used by absloc-persist-leading-firstPersistW, abs-apply-firstPersistW, abs-apply-persist-FO, absloc-persistFO, abs-loc-no-w-last-fo-then-no-pending,
• list-del/firstN-zero is used by absloc-persist-firstPersistW,
• list-del/get-succ is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-apply-persist-FO, abs-loc-no-w-last-fo-then-no-pending, abs-firstVolWrite-head,
• list-del/get-zero is used by abs-firstPersistW-is-firstVolWrite, abs-firstPersistW-firstVolWrite-correct-loc, abs-apply-firstPersistW, abs-apply-persist-FO, abs-loc-no-w-last-fo-then-no-pending, abs-firstVolWrite-head,
• list-del/restN-zero is used by absloc-persist-firstPersistW,
• list-del/weak-firstN-rec is used by absloc-persist-firstPersistW,
• list-del/weak-restN-rec is used by absloc-persist-firstPersistW,