Used simplifier rules/spec theorems by specification

Used from specification forall-indexWhere

• forall-indexWhere/forall-1l is used by reorder-same-thread-events,

Used from specification nat

• nat/le-ls-simp is used by reorder-firstPersistW-valid-lifted,
• nat/lels is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-valid-lifted, reorder-firstPersistW-valid,
• nat/lez is used by isPropFO-delpos-eq-delfirst,
• nat/succ-01 is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-valid,

Used from specification FLITPSC-preds

• FLITPSC-preds/noPending is used by reorder-step-propW-lifted,
• FLITPSC-preds/filter-W-append is used by reorder-same-writes,
• FLITPSC-preds/filter-W-one-fo is used by reorder-same-writes,
• FLITPSC-preds/filter-W-one-w is used by reorder-same-writes,
• FLITPSC-preds/filter-t-append is used by reorder-same-thread-events, reorder-del-other-FO, reorder-step-readPWB, reorder-firstPersistW-eq, reorder-step-read-propFO, reorder-isPersistFO-exists, reorder-step-readPWB-other, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• FLITPSC-preds/filter-t-one is used by reorder-same-thread-events, reorder-del-other-FO, reorder-step-readPWB, reorder-firstPersistW-eq, reorder-step-read-propFO, reorder-isPersistFO-exists, reorder-step-readPWB-other, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• FLITPSC-preds/filter-tid-empty is used by reorder-same-thread-events, reorder-step-readPWB, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• FLITPSC-preds/filter-w-empty is used by reorder-same-writes,
• FLITPSC-preds/filter-w-fo is used by reorder-same-writes,
• FLITPSC-preds/filter-w-write is used by reorder-same-writes,
• FLITPSC-preds/oplus-same-writes-eq is used by reorder-overwrite-p-eq-lifted,
• FLITPSC-preds/oplus-v-append is used by reorder-overwrite-p-eq,
• FLITPSC-preds/oplus-v-one-FO is used by reorder-overwrite-p-eq,
• FLITPSC-preds/oplus-v-one-W is used by reorder-overwrite-p-eq,
• FLITPSC-preds/overwrite-base is used by reorder-overwrite-p-eq,
• FLITPSC-preds/overwrite-rec1 is used by reorder-overwrite-p-eq,
• FLITPSC-preds/overwrite-rec2 is used by reorder-overwrite-p-eq,

Used from specification FLITPSCweak-preds

• FLITPSCweak-preds/isPersistFO is used by reorder-isPersistFO-exists,
• FLITPSCweak-preds/firstPersistW-base is used by reorder-firstPersistW-eq, reorder-firstPersistW-valid,
• FLITPSCweak-preds/firstPersistW-rec-FO is used by reorder-firstPersistW-eq, reorder-step-persistW, reorder-firstPersistW-valid,
• FLITPSCweak-preds/firstPersistW-rec-W is used by reorder-firstPersistW-eq, reorder-step-persistW, reorder-firstPersistW-valid,
• FLITPSCweak-preds/isPersistFO-rec is used by reorder-isPersistFO-exists, reorder-step-persistFO,

Used from specification list-data

• list-data/elim-add is used by reorder-same-thread-events, reorder-del-other-FO, reorder-step-readPWB, reorder-fo-in-p, reorder-overwrite-p-eq, reorder-step-read-propFO, reorder-same-writes, reorder-step-readPWB-other, reorder-step-propW, reorder-step-propFO,
• list-data/l is used by isPropFO-delpos-eq-delfirst, isPropFO-in-bq, reorder-step-read-propFO,
• list-data/size-nil is used by reorder-firstPersistW-valid,

Used from specification nat-basic

• nat-basic/a is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-step-persistFO, reorder-firstPersistW-valid,
• nat-basic/c is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-step-persistFO, reorder-firstPersistW-valid,
• nat-basic/f is used by isPropFO-delpos-eq-delfirst, isPropFO-in-bq, reorder-step-read-propFO, reorder-firstPersistW-valid,
• nat-basic/less-zero is used by isPropFO-delpos-eq-delfirst, reorder-isPersistFO-exists, reorder-firstPersistW-valid,
• nat-basic/lf is used by isPropFO-delpos-eq-delfirst,
• nat-basic/oz is used by reorder-isPersistFO-exists,
• nat-basic/s-04 is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-valid,
• nat-basic/succ is used by isPropFO-delpos-eq-delfirst, reorder-isPersistFO-exists, reorder-step-persistFO, reorder-firstPersistW-valid,
• nat-basic/trans-Nat is used by isPropFO-delpos-eq-delfirst,
• nat-basic/zero is used by reorder-isPersistFO-exists,

Used from specification list

• list/elim-first is used by reorder-same-thread-events,
• list/firstoc-rew is used by reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-step-persistFO, reorder-firstPersistW-valid,
• list/in-def is used by reorder-step-readPWB, reorder-fo-in-p,
• list/Nil is used by propFOs-append, reorder-same-thread-events, reorder-step-readPWB, reorder-firstPersistW-eq, reorder-same-writes, reorder-isPersistFO-exists, buffered-1l-expand, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• list/a is used by propFOs-append, reorder-same-thread-events, isPropFO-delpos-eq-delfirst, reorder-del-other-FO, reorder-step-readPWB, reorder-step-persistFO-lifted, w-in-propFOs, reorder-fo-in-p, propFOs-one-w, reorder-overwrite-p-eq, reorder-firstPersistW-valid-lifted, reorder-firstPersistW-eq, reorder-step-propFO-lifted, reorder-step-read-propFO, propFOs-one-fo-other, reorder-step-read-propFO-lifted, propFOs-one-fo-same, reorder-same-writes, reorder-isPersistFO-exists-lifted, reorder-isPersistFO-exists, reorder-step-propW-lifted, reorder-firstPersistW-eq-lifted, reorder-step-readPWB-other, buffered-1l-expand, reorder-step-persistW-lifted, reorder-step-persistW, reorder-step-persistFO, propFOs-one-sf, fo-in-propFOs, reorder-step-readPWB-lifted, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• list/app is used by reorder-step-readPWB, propFOs-one-w, reorder-step-read-propFO, propFOs-one-fo-other, reorder-step-readPWB-other, buffered-1l-expand, propFOs-one-sf, reorder-step-propW, reorder-step-propFO,
• list/app-02 is used by reorder-same-thread-events, isPropFO-delpos-eq-delfirst, reorder-del-other-FO, reorder-step-readPWB, reorder-fo-in-p, reorder-overwrite-p-eq, reorder-firstPersistW-eq, reorder-step-read-propFO, reorder-same-writes, reorder-isPersistFO-exists, reorder-step-readPWB-other, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• list/c is used by propFOs-append, reorder-same-thread-events, isPropFO-delpos-eq-delfirst, reorder-del-other-FO, reorder-step-readPWB, w-in-propFOs, reorder-fo-in-p, reorder-overwrite-p-eq, reorder-firstPersistW-eq, reorder-step-read-propFO, propFOs-one-fo-same, reorder-same-writes, reorder-isPersistFO-exists, reorder-step-readPWB-other, buffered-1l-expand, reorder-step-persistW, reorder-step-persistFO, fo-in-propFOs, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• list/c-04 is used by reorder-step-propFO,
• list/c-06 is used by reorder-step-persistFO,
• list/c-07 is used by reorder-step-persistW, reorder-firstPersistW-valid,
• list/c-08 is used by reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-firstPersistW-valid,
• list/e is used by reorder-same-thread-events, isPropFO-delpos-eq-delfirst, reorder-del-other-FO, reorder-step-readPWB, reorder-fo-in-p, reorder-overwrite-p-eq, reorder-firstPersistW-eq, reorder-step-read-propFO, reorder-same-writes, reorder-isPersistFO-exists, reorder-step-readPWB-other, buffered-1l-expand, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-firstPersistW-valid, reorder-step-propFO,
• list/first is used by reorder-step-propW,
• list/first-01 is used by reorder-step-read-propFO, reorder-step-propW, reorder-step-propFO,
• list/in-11 is used by reorder-step-readPWB, reorder-step-readPWB-other,
• list/in-14 is used by reorder-same-thread-events, reorder-step-persistFO-lifted, reorder-firstPersistW-valid-lifted, reorder-firstPersistW-eq, reorder-isPersistFO-exists-lifted, reorder-isPersistFO-exists, reorder-firstPersistW-eq-lifted, reorder-step-persistW-lifted, reorder-step-persistW, reorder-step-persistFO, reorder-firstPersistW-valid,
• list/in-17 is used by reorder-step-readPWB, w-in-propFOs, fo-in-propFOs,
• list/in-append is used by reorder-step-readPWB, w-in-propFOs, reorder-fo-in-p, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-step-persistFO, fo-in-propFOs, reorder-firstPersistW-valid,
• list/in-empty is used by w-in-propFOs, reorder-fo-in-p, reorder-firstPersistW-eq, reorder-isPersistFO-exists, buffered-1l-expand, reorder-step-persistW, reorder-step-persistFO, fo-in-propFOs, reorder-firstPersistW-valid, reorder-step-propFO,
• list/in-rec is used by reorder-fo-in-p, reorder-firstPersistW-eq, reorder-isPersistFO-exists, buffered-1l-expand, reorder-step-persistW, reorder-step-persistFO, fo-in-propFOs, reorder-firstPersistW-valid,
• list/inapp-02 is used by reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-step-persistFO, reorder-firstPersistW-valid,
• list/len-01 is used by propFOs-append, reorder-same-thread-events, isPropFO-delpos-eq-delfirst, reorder-step-readPWB, reorder-step-read-propFO, reorder-same-writes, reorder-step-readPWB-other, buffered-1l-expand, reorder-step-persistFO,
• list/len-05 is used by isPropFO-delpos-eq-delfirst, reorder-isPersistFO-exists, reorder-firstPersistW-valid,
• list/len-06 is used by propFOs-one-fo-same,
• list/rest is used by reorder-step-propW,
• list/rest-01 is used by reorder-step-read-propFO, reorder-step-propW, reorder-step-propFO,

Used from specification Bevent

• Bevent/disj-FO-SF is used by isPropFO-delpos-eq-delfirst, reorder-del-other-FO, buffered-1l-expand, fo-in-propFOs,
• Bevent/disj-W-FO is used by reorder-del-other-FO, buffered-1l-expand, fo-in-propFOs,
• Bevent/inj-FO is used by reorder-del-other-FO, buffered-1l-expand, fo-in-propFOs,
• Bevent/sel-FO-dotl is used by isPropFO-delpos-eq-delfirst,
• Bevent/test-dotFOque-FO is used by isPropFO-delpos-eq-delfirst,
• Bevent/test-dotWque-FO is used by isPropFO-delpos-eq-delfirst,

Used from specification FOW

• FOW/disj-FO-W is used by w-in-propFOs, reorder-fo-in-p, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistW, reorder-firstPersistW-valid,
• FOW/elim-FO is used by reorder-step-persistFO,
• FOW/inj-FO is used by reorder-fo-in-p, reorder-isPersistFO-exists, reorder-step-persistFO, fo-in-propFOs,
• FOW/inj-W is used by reorder-firstPersistW-eq-lifted, reorder-step-persistW, reorder-step-propW, reorder-firstPersistW-valid,
• FOW/sel-FO-dottid is used by reorder-same-thread-events, reorder-del-other-FO, reorder-step-readPWB, reorder-step-read-propFO, reorder-isPersistFO-exists, reorder-step-readPWB-other, reorder-step-persistW, reorder-step-persistFO, reorder-step-propW, reorder-step-propFO,
• FOW/sel-W-dottid is used by reorder-same-thread-events, reorder-firstPersistW-eq, reorder-step-persistW, reorder-step-propW, reorder-firstPersistW-valid,
• FOW/test-dotFOque-FO is used by reorder-isPersistFO-exists, reorder-step-persistFO,

Used from specification list-del

• list-del/app is used by reorder-step-readPWB,
• list-del/del1-n is used by isPropFO-delpos-eq-delfirst, reorder-del-other-FO,
• list-del/in-get is used by isPropFO-in-bq, reorder-step-read-propFO,
• list-del/sw-02 is used by reorder-del-other-FO,
• list-del/app is used by reorder-step-readPWB, reorder-step-readPWB-other,
• list-del/app-01 is used by reorder-step-readPWB,
• list-del/del1-e is used by reorder-del-other-FO, buffered-1l-expand, reorder-step-propFO,
• list-del/del1-n is used by buffered-1l-expand,
• list-del/del1-y is used by isPropFO-delpos-eq-delfirst, reorder-del-other-FO, buffered-1l-expand,
• list-del/delpos-base is used by isPropFO-delpos-eq-delfirst, reorder-step-persistW, reorder-step-persistFO,
• list-del/delpos-rec is used by isPropFO-delpos-eq-delfirst, reorder-step-persistW, reorder-step-persistFO,
• list-del/get-succ is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistFO,
• list-del/get-zero is used by isPropFO-delpos-eq-delfirst, reorder-firstPersistW-eq, reorder-isPersistFO-exists, reorder-step-persistFO,
• list-del/in-01-01 is used by reorder-del-other-FO,
• list-del/in-05 is used by reorder-del-other-FO,
• list-del/one-01 is used by reorder-step-readPWB,

Used from specification FLIT-preds

• FLIT-preds/isPropFO-def is used by isPropFO-delpos-eq-delfirst, isPropFO-in-bq, reorder-step-read-propFO,