[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification list-last

list-last/postfix is used by stable-W5, stable-W6,
list-last/splitlasteq is used by rely-PROP_W,
list-last/bc is used by rely-PROP_W,
list-last/butlast-def is used by rely-PROP_W,
list-last/butlast-one is used by rely-PROP_W,
list-last/l-in is used by rely-PROP_W,
list-last/last-elim is used by rely-PROP_W,

Used from specification forall-indexWhere

forall-indexWhere/forall-base is used by step-CRASH, init-state-inv,
forall-indexWhere/forall-one is used by stable-W5, stable-W6,
forall-indexWhere/forall-rec is used by stable-W5, stable-W6,

Used from specification nat

nat/elim-pred-c is used by step-W6-W7,
nat/ge is used by definedness-W6,
nat/le-def is used by definedness-W6,

Used from specification FLITPSC-preds

FLITPSC-preds/ctrok-def is used by step-CRASH, init-state-inv,
FLITPSC-preds/filter-W-append is used by step-W6-W7,
FLITPSC-preds/filtertid-def is used by step-W2-W3,
FLITPSC-preds/filterwrites-def is used by step-W2-W3,
FLITPSC-preds/noWriter is used by step-CRASH, init-state-inv,
FLITPSC-preds/ctrok-add-writer is used by step-W2-W3,
FLITPSC-preds/ctrok-rm-writer is used by step-W6-W7,
FLITPSC-preds/ctrok-size-writers-eq-ctr is used by rely-PROP_FO, step-PROP_FO,
FLITPSC-preds/filter-t-append is used by step-W6-W7,
FLITPSC-preds/filter-t-one is used by step-W6-W7,
FLITPSC-preds/filter-tid-empty is used by step-CRASH, init-state-inv,
FLITPSC-preds/filter-w-empty is used by step-CRASH, init-state-inv,
FLITPSC-preds/filter-w-write is used by step-W6-W7,
FLITPSC-preds/in-filter-t is used by step-W2-W3, step-W6-W7,
FLITPSC-preds/nomember-to-onemember is used by step-R1-R2, step-W2-W3,
FLITPSC-preds/onemember-eq is used by step-W6-W7,
FLITPSC-preds/onemember-to-nomember is used by step-R2-R4, step-W6-W7, step-R3-R4,
FLITPSC-preds/onewriter-ctrok-nonzero is used by definedness-W6, step-W6-W7,
FLITPSC-preds/overwrite-def is used by step-R1-R2, rely-R1-R2,
FLITPSC-preds/relyws-add-other-writer is used by rely-W2-W3, rely-R1-R2,
FLITPSC-preds/relyws-noWriter-stable is used by stable-ready, stable-W4, stable-W1, stable-W7, stable-crashed, stable-R1, stable-W5, stable-W2, stable-R2, stable-W3, stable-W6,
FLITPSC-preds/relyws-oneWriter-stable is used by stable-W4, stable-W5, stable-R2, stable-W3, stable-W6,
FLITPSC-preds/relyws-refl is used by rely-W3-W4, rely-PERSIST_W, rely-PROP_FO, rely-W2-W3, rely-W1-W2, rely-R3-R4, rely-W6-W7, rely-PERSIST_FO, rely-W5-W6, rely-R2-R3, rely-R1-R2, rely-reflexive, rely-PROP_W, rely-W4-W5, rely-PROP_SF, rely-R2-R4,
FLITPSC-preds/relyws-rm-other-writer is used by rely-R3-R4, rely-W6-W7, rely-R2-R4,

Used from specification FLIT-preds

FLIT-preds/B-postfix-weak-same-loc-postfix is used by stable-W5, stable-W6,
FLIT-preds/FOFollowsW-def is used by step-W4-W5, step-W6-W7, step-W5-W6,
FLIT-preds/FOs is used by step-CRASH, init-state-inv,
FLIT-preds/SFTrailing is used by step-CRASH, init-state-inv,
FLIT-preds/isPropFO-delpos-last-SF is used by rely-PROP_FO,
FLIT-preds/noPending is used by step-CRASH, step-W2-W3, init-state-inv, step-W6-W7,
FLIT-preds/noPendingW is used by step-W2-W3,
FLIT-preds/pendingOk is used by step-CRASH, init-state-inv,
FLIT-preds/readFOsOk is used by step-CRASH, init-state-inv,
FLIT-preds/readFOsOk-prop-FO is used by step-PROP_FO,
FLIT-preds/writersOk is used by step-CRASH, init-state-inv, step-W6-W7,
FLIT-preds/B-postfix-weak-append is used by stable-W5, stable-W6, rely-PROP_W,
FLIT-preds/B-postfix-weak-delpos-propFO is used by rely-PROP_FO,
FLIT-preds/B-postfix-weak-empty is used by rely-PROP_SF,
FLIT-preds/B-postfix-weak-not-in-stable is used by stable-ready, stable-W4, stable-W1, stable-W7, stable-crashed, stable-R1, stable-W5, stable-R2, stable-W3,
FLIT-preds/B-postfix-weak-of-empty is used by stable-W3,
FLIT-preds/B-postfix-weak-one is used by stable-W4, stable-W5,
FLIT-preds/B-postfix-weak-one-ws is used by stable-W4, stable-W5,
FLIT-preds/B-postfix-weak-refl is used by rely-W3-W4, rely-PERSIST_W, rely-PROP_FO, rely-W2-W3, rely-W1-W2, rely-R3-R4, rely-W6-W7, rely-PERSIST_FO, rely-W5-W6, rely-R2-R3, rely-R1-R2, rely-reflexive, rely-PROP_W, rely-W4-W5, rely-PROP_SF, rely-R2-R4,
FLIT-preds/SFTrailing-attach is used by step-W4-W5, step-W3-W4, step-W1-W2, step-R3-R4, step-W5-W6,
FLIT-preds/SFTrailing-leading-SF is used by step-PROP_SF, rely-PROP_SF,
FLIT-preds/SFTrailing-tail is used by step-PROP_SF, step-PROP_W,
FLIT-preds/SFTrainling-prop-FO is used by step-PROP_FO,
FLIT-preds/noPending-then-noPendingW is used by step-idle-ready, step-CRASH, step-W7-ready, init-state-inv,
FLIT-preds/noPendingW-add-FO is used by step-R3-R4,
FLIT-preds/noPendingW-add-SF is used by step-W1-W2,
FLIT-preds/oplus-noPendingW is used by step-R1-R2,
FLIT-preds/pendingOk-add-FO is used by step-W4-W5, step-R3-R4,
FLIT-preds/pendingOk-add-SF is used by step-W1-W2, step-W5-W6,
FLIT-preds/pendingOk-add-pending is used by step-W3-W4,
FLIT-preds/pendingOk-empty-bq is used by step-PROP_SF,
FLIT-preds/pendingOk-persist is used by step-PERSIST_W, step-PERSIST_FO,
FLIT-preds/pendingOk-prop-FO is used by step-PROP_FO,
FLIT-preds/pendingOk-prop-W is used by step-PROP_W,
FLIT-preds/readFOsOk-add-FO is used by step-R3-R4,
FLIT-preds/readFOsOk-add-writer is used by step-W2-W3,
FLIT-preds/readFOsOk-empty-rfo-while-writing is used by rely-PROP_FO, step-PROP_FO,
FLIT-preds/readFOsOk-not-leading-W is used by rely-PROP_W,
FLIT-preds/readFOsOk-not-one-SF is used by rely-PROP_SF,
FLIT-preds/readFOsOk-rm-writer is used by step-W6-W7,
FLIT-preds/rely-FOFollowsW-stable is used by stable-W5, stable-W6,
FLIT-preds/rely-noPending-stable is used by stable-W3,
FLIT-preds/rely-noPending-stable-strong is used by stable-W7, stable-crashed,
FLIT-preds/rely-noPendingW-stable is used by stable-ready, stable-W1, stable-crashed, stable-R1, stable-W2, stable-R2,
FLIT-preds/rely-persist is used by rely-PERSIST_W, rely-PERSIST_FO,
FLIT-preds/rely-prop-FO is used by rely-PROP_FO,
FLIT-preds/rely-prop-SF is used by rely-PROP_SF,
FLIT-preds/rely-prop-W is used by rely-PROP_W,
FLIT-preds/rely-refl is used by rely-W2-W3, rely-W6-W7, rely-R2-R3, rely-R1-R2, rely-reflexive, rely-R2-R4,
FLIT-preds/rely-update-other-bq is used by rely-W3-W4, rely-W1-W2, rely-R3-R4, rely-W5-W6, rely-W4-W5,
FLIT-preds/restrict-l-empty is used by step-CRASH, step-W2-W3, init-state-inv, step-W6-W7,
FLIT-preds/writersOk-add-FO is used by step-W4-W5, step-R3-R4,
FLIT-preds/writersOk-add-SF is used by step-W1-W2, step-W5-W6,
FLIT-preds/writersOk-empty-bq is used by step-PROP_SF,
FLIT-preds/writersOk-persist is used by step-PERSIST_W, step-PERSIST_FO,
FLIT-preds/writersOk-prop-FO is used by step-PROP_FO,
FLIT-preds/writersOk-prop-W is used by step-PROP_W,
FLIT-preds/writersok-add-pending is used by step-W3-W4,
FLIT-preds/writersok-add-writer is used by step-W2-W3,
FLIT-preds/writersok-rm-writer is used by step-W6-W7,

Used from specification set-basic

set-basic/In-empty is used by step-CRASH, init-state-inv,
set-basic/Size-empty is used by step-CRASH, init-state-inv,
set-basic/ne-01 is used by rely-PROP_FO, step-PROP_FO,
set-basic/size-zero-01 is used by rely-PROP_FO, step-PROP_FO,

Used from specification nat-basic

nat-basic/a is used by step-CRASH, step-W2-W3, init-state-inv, step-W6-W7,
nat-basic/c is used by step-CRASH, step-W2-W3, init-state-inv, step-W6-W7,
nat-basic/f is used by rely-PROP_FO, step-PROP_FO,
nat-basic/one-01 is used by rely-PROP_FO, definedness-W6,
nat-basic/oz is used by step-W6-W7,

Used from specification list

list/in-def is used by step-W6-W7,
list/some-element is used by step-W2-W3, step-W6-W7,
list/Last is used by step-W4-W5, rely-W3-W4, step-W3-W4, rely-PROP_FO, rely-W1-W2, step-PROP_W, rely-R3-R4, rely-W5-W6, step-W1-W2, step-PROP_FO, step-R3-R4, rely-PROP_W, rely-W4-W5, step-W5-W6,
list/Nil is used by step-W4-W5, stable-W4, step-W3-W4, rely-PROP_FO, stable-W5, stable-W6, step-W5-W6,
list/a is used by step-W4-W5, stable-W4, rely-PERSIST_W, step-PERSIST_W, step-W3-W4, rely-PROP_FO, step-PROP_SF, step-W2-W3, step-PERSIST_FO, step-PROP_W, stable-W5, rely-PERSIST_FO, step-W1-W2, step-PROP_FO, step-W6-W7, step-R3-R4, stable-W6, rely-PROP_W, step-W5-W6, rely-PROP_SF,
list/app is used by step-W4-W5, stable-W4, step-PROP_SF, stable-W5, stable-W6, rely-PROP_W, step-W5-W6, rely-PROP_SF,
list/app-02 is used by step-W4-W5, stable-W4, step-W3-W4, step-W2-W3, stable-W5, step-W6-W7, stable-W6, rely-PROP_W, step-W5-W6, rely-PROP_SF,
list/app-05 is used by stable-W5, stable-W6, rely-PROP_W, rely-PROP_SF,
list/app-06 is used by step-W4-W5,
list/c is used by step-W4-W5, stable-W4, rely-PERSIST_W, step-PERSIST_W, step-PROP_SF, step-PERSIST_FO, step-PROP_W, stable-W5, rely-PERSIST_FO, step-W6-W7, stable-W6, rely-PROP_W, step-W5-W6, rely-PROP_SF,
list/c-03 is used by step-W4-W5, stable-W4, stable-W5, stable-W6, step-W5-W6,
list/c-05 is used by step-W4-W5, step-W3-W4, stable-W6, step-W5-W6,
list/c-06 is used by step-W4-W5, stable-W5, stable-W6, rely-PROP_W, step-W5-W6,
list/c-08 is used by step-W5-W6,
list/e is used by step-W4-W5, stable-W4, step-W3-W4, rely-PROP_FO, step-PROP_SF, stable-W5, step-W6-W7, stable-W6, rely-PROP_W, step-W5-W6, rely-PROP_SF,
list/eq-04 is used by step-W4-W5, stable-W5, stable-W6, step-W5-W6,
list/eq-05 is used by stable-W6,
list/first is used by step-W4-W5, step-W3-W4, step-W5-W6,
list/in-01 is used by stable-W5, stable-W6,
list/in-06 is used by stable-W4, stable-W5, step-W5-W6,
list/in-10 is used by step-W5-W6,
list/in-11 is used by stable-W6,
list/in-12 is used by step-W6-W7,
list/in-14 is used by step-W4-W5, stable-W4, step-PROP_SF, stable-W5, stable-W6, rely-PROP_W, step-W5-W6, rely-PROP_SF,
list/in-15 is used by step-W4-W5, rely-PROP_FO, stable-W5, stable-W6, rely-PROP_W, step-W5-W6,
list/in-16 is used by stable-W5, stable-W6,
list/in-17 is used by step-W4-W5, stable-W4, step-W3-W4, stable-W5, step-R3-R4, stable-W6, step-W5-W6, rely-PROP_SF,
list/in-append is used by step-W4-W5, step-W3-W4, stable-W5, step-R3-R4, stable-W6, step-W5-W6,
list/in-append0-not-left is used by stable-W5, stable-W6,
list/in-empty is used by step-ready-ready, step-W4-W5, rely-W3-W4, step-W3-W4, step-CRASH, step-W2-W3, step-W7-ready, init-state-inv, stable-W5, step-W6-W7, step-W5-W6,
list/in-rec is used by step-W4-W5, stable-W4, stable-W5, stable-W6, rely-PROP_W, step-W5-W6,
list/inapp-02 is used by stable-W5, stable-W6, step-W5-W6,
list/inapp-12 is used by stable-W5, stable-W6,
list/inex is used by stable-W5, stable-W6,
list/len-02 is used by rely-PROP_FO,
list/len-06 is used by step-W4-W5, stable-W5, step-W1-W2, step-R3-R4, stable-W6, step-W5-W6,
list/ni is used by step-W4-W5, stable-W5, stable-W6,
list/one-01 is used by stable-W5, stable-W6,
list/rest is used by rely-PROP_SF,

Used from specification FOW

FOW/sel-FO-dottid is used by step-W2-W3, step-W6-W7,
FOW/sel-W-dottid is used by step-W2-W3, step-W6-W7,
FOW/test-dotWque-W is used by step-W2-W3,

Used from specification FLIT

FLIT/FLITGInv is used by init-state-inv,
FLIT/FLITInv is used by init-state-inv,
FLIT/FLITLInv is used by step-CRASH, init-state-inv,
FLIT/disj-R1-W1 is used by step-ready-W1, step-ready-R1,
FLIT/disj-R1-crashed is used by step-CRASH,
FLIT/disj-R1-idle is used by step-CRASH, init-state-inv,
FLIT/disj-R1-ready is used by step-ready-ready, step-ready-R1,
FLIT/disj-R2-crashed is used by step-CRASH,
FLIT/disj-R2-idle is used by step-CRASH, init-state-inv,
FLIT/disj-R3-R4 is used by step-R2-R4, rely-R2-R3, step-R2-R3, rely-R2-R4,
FLIT/disj-R3-crashed is used by step-CRASH,
FLIT/disj-R3-idle is used by step-CRASH, init-state-inv,
FLIT/disj-R4-crashed is used by step-CRASH,
FLIT/disj-R4-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W1-crashed is used by step-CRASH,
FLIT/disj-W1-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W1-ready is used by step-ready-ready, step-ready-W1,
FLIT/disj-W2-crashed is used by step-CRASH,
FLIT/disj-W2-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W3-crashed is used by step-CRASH,
FLIT/disj-W3-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W4-crashed is used by step-CRASH,
FLIT/disj-W4-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W5-crashed is used by step-CRASH,
FLIT/disj-W5-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W6-crashed is used by step-CRASH,
FLIT/disj-W6-idle is used by step-CRASH, init-state-inv,
FLIT/disj-W7-crashed is used by step-CRASH,
FLIT/disj-W7-idle is used by step-CRASH, init-state-inv,
FLIT/disj-callFLITCOMPLETE-invFLITREAD is used by step-ready-ready,
FLIT/disj-callFLITCOMPLETE-invFLITWRITE is used by step-ready-ready,
FLIT/disj-crashed-idle is used by step-CRASH,
FLIT/disj-crashed-ready is used by step-CRASH,
FLIT/disj-invFLITREAD-invFLITWRITE is used by step-ready-W1, step-ready-R1,
FLIT/gstepf-R1 is used by step-R1-R2, rely-R1-R2,
FLIT/gstepf-R2 is used by step-R2-R4, rely-R2-R3, step-R2-R3, rely-R2-R4,
FLIT/gstepf-R3 is used by rely-R3-R4, step-R3-R4,
FLIT/gstepf-R4 is used by step-R4-ready,
FLIT/gstepf-W1 is used by rely-W1-W2, step-W1-W2,
FLIT/gstepf-W2 is used by rely-W2-W3, step-W2-W3,
FLIT/gstepf-W3 is used by rely-W3-W4, step-W3-W4,
FLIT/gstepf-W4 is used by step-W4-W5, rely-W4-W5,
FLIT/gstepf-W5 is used by rely-W5-W6, step-W5-W6,
FLIT/gstepf-W6 is used by rely-W6-W7, step-W6-W7,
FLIT/gstepf-W7 is used by step-W7-ready,
FLIT/gstepf-idle-RUN is used by step-idle-ready,
FLIT/gstepf-ready is used by step-ready-ready, step-ready-W1, step-ready-R1,
FLIT/lstepf-R1 is used by step-R1-R2,
FLIT/lstepf-R2 is used by step-R2-R4, step-R2-R3,
FLIT/lstepf-R3 is used by step-R3-R4,
FLIT/lstepf-R4 is used by step-R4-ready,
FLIT/lstepf-W1 is used by step-W1-W2,
FLIT/lstepf-W2 is used by step-W2-W3,
FLIT/lstepf-W3 is used by step-W3-W4,
FLIT/lstepf-W4 is used by step-W4-W5,
FLIT/lstepf-W5 is used by step-W5-W6,
FLIT/lstepf-W6 is used by step-W6-W7,
FLIT/lstepf-W7 is used by step-W7-ready,
FLIT/lstepf-idle-RUN is used by step-idle-ready,
FLIT/lstepf-ready-FLITCOMPLETE is used by step-ready-ready,
FLIT/lstepf-ready-FLITREAD is used by step-ready-R1,
FLIT/lstepf-ready-FLITWRITE is used by step-ready-W1,
FLIT/pcstepf-R1 is used by step-R1-R2, rely-R1-R2,
FLIT/pcstepf-R2 is used by step-R2-R4, rely-R2-R3, step-R2-R3, rely-R2-R4,
FLIT/pcstepf-R3 is used by rely-R3-R4, step-R3-R4,
FLIT/pcstepf-R4 is used by step-R4-ready,
FLIT/pcstepf-W1 is used by rely-W1-W2, step-W1-W2,
FLIT/pcstepf-W2 is used by rely-W2-W3, step-W2-W3,
FLIT/pcstepf-W3 is used by rely-W3-W4, step-W3-W4,
FLIT/pcstepf-W4 is used by step-W4-W5, rely-W4-W5,
FLIT/pcstepf-W5 is used by rely-W5-W6, step-W5-W6,
FLIT/pcstepf-W6 is used by rely-W6-W7, step-W6-W7,
FLIT/pcstepf-W7 is used by step-W7-ready,
FLIT/pcstepf-idle-RUN is used by step-idle-ready,
FLIT/pcstepf-ready-FLITCOMPLETE is used by step-ready-ready, step-ready-W1, step-ready-R1,
FLIT/pcstepf-ready-FLITREAD is used by step-ready-ready, step-ready-W1, step-ready-R1,
FLIT/pcstepf-ready-FLITWRITE is used by step-ready-ready, step-ready-W1, step-ready-R1,
FLIT/pre-R1 is used by step-R1-R2, rely-R1-R2,
FLIT/pre-R2 is used by step-R2-R4, definedness-R2, rely-R2-R3, step-R2-R3, rely-R2-R4,
FLIT/pre-R3 is used by rely-R3-R4, step-R3-R4,
FLIT/pre-R4 is used by step-R4-ready,
FLIT/pre-W1 is used by rely-W1-W2, step-W1-W2,
FLIT/pre-W2 is used by rely-W2-W3, step-W2-W3,
FLIT/pre-W3 is used by rely-W3-W4, step-W3-W4,
FLIT/pre-W4 is used by step-W4-W5, rely-W4-W5,
FLIT/pre-W5 is used by rely-W5-W6, step-W5-W6,
FLIT/pre-W6 is used by rely-W6-W7, definedness-W6, step-W6-W7,
FLIT/pre-W7 is used by step-W7-ready,
FLIT/pre-idle is used by step-idle-ready,
FLIT/pre-ready is used by step-ready-ready, step-ready-W1, step-ready-R1,
FLIT/updsel--dotbq-dotbq is used by step-W4-W5, rely-W3-W4, step-W3-W4, rely-PROP_FO, step-CRASH, step-PROP_SF, rely-W1-W2, step-PROP_W, rely-R3-R4, rely-W5-W6, step-W1-W2, step-PROP_FO, step-R3-R4, rely-PROP_W, rely-W4-W5, step-W5-W6, rely-PROP_SF,
FLIT/updsel--dotbq-dotfctr is used by step-W4-W5, step-W3-W4, step-CRASH, step-PROP_SF, step-PROP_W, step-W1-W2, step-PROP_FO, step-R3-R4, step-W5-W6,
FLIT/updsel--dotbq-dotfreaders is used by step-W4-W5, rely-W3-W4, step-W3-W4, rely-PROP_FO, rely-W1-W2, rely-W5-W6, step-W1-W2, rely-PROP_W, rely-W4-W5, step-W5-W6, rely-PROP_SF,
FLIT/updsel--dotbq-dotfwriters is used by step-W4-W5, rely-W3-W4, step-W3-W4, rely-PROP_FO, step-PROP_SF, rely-W1-W2, step-PROP_W, rely-R3-R4, rely-W5-W6, step-W1-W2, step-PROP_FO, step-R3-R4, rely-PROP_W, rely-W4-W5, step-W5-W6, rely-PROP_SF,
FLIT/updsel--dotbq-dotpq is used by step-W4-W5, rely-W3-W4, step-W3-W4, rely-PROP_FO, step-CRASH, step-PROP_SF, rely-W1-W2, step-PROP_W, rely-R3-R4, rely-W5-W6, step-W1-W2, step-PROP_FO, step-R3-R4, rely-PROP_W, rely-W4-W5, step-W5-W6, rely-PROP_SF,
FLIT/updsel--dotbq-dotrfo is used by step-W4-W5, rely-W3-W4, step-W3-W4, step-PROP_SF, rely-W1-W2, step-PROP_W, rely-W5-W6, step-W1-W2, rely-PROP_W, rely-W4-W5, step-W5-W6, rely-PROP_SF,
FLIT/updsel--dotfctr-dotbq is used by rely-W2-W3, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfctr-dotfctr is used by step-CRASH, step-W2-W3, step-W6-W7,
FLIT/updsel--dotfctr-dotfreaders is used by rely-W2-W3, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfctr-dotpq is used by rely-W2-W3, step-CRASH, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfctr-dotrfo is used by rely-W2-W3, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfreaders-dotbq is used by step-R1-R2, step-CRASH, step-R2-R4, rely-R3-R4, rely-R1-R2, step-R3-R4, rely-R2-R4,
FLIT/updsel--dotfreaders-dotfctr is used by step-R1-R2, step-CRASH, step-R2-R4, step-R3-R4,
FLIT/updsel--dotfreaders-dotfreaders is used by step-R1-R2, step-CRASH, step-R2-R4, rely-R3-R4, rely-R1-R2, step-R3-R4, rely-R2-R4,
FLIT/updsel--dotfreaders-dotfwriters is used by step-R1-R2, step-CRASH, step-R2-R4, rely-R3-R4, rely-R1-R2, step-R3-R4, rely-R2-R4,
FLIT/updsel--dotfreaders-dotpq is used by step-R1-R2, step-CRASH, step-R2-R4, rely-R3-R4, rely-R1-R2, step-R3-R4, rely-R2-R4,
FLIT/updsel--dotfreaders-dotrfo is used by step-R1-R2, step-R2-R4, rely-R3-R4, rely-R1-R2, step-R3-R4, rely-R2-R4,
FLIT/updsel--dotfwriters-dotbq is used by rely-W2-W3, step-CRASH, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfwriters-dotfctr is used by step-CRASH, step-W2-W3, step-W6-W7,
FLIT/updsel--dotfwriters-dotfreaders is used by rely-W2-W3, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfwriters-dotfwriters is used by rely-W2-W3, step-CRASH, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfwriters-dotpq is used by rely-W2-W3, step-CRASH, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotfwriters-dotrfo is used by rely-W2-W3, step-W2-W3, rely-W6-W7, step-W6-W7,
FLIT/updsel--dotloc-dott is used by step-ready-W1, step-ready-R1,
FLIT/updsel--dotpmem-dotbq is used by rely-PERSIST_W, step-PERSIST_W,
FLIT/updsel--dotpmem-dotfctr is used by step-PERSIST_W,
FLIT/updsel--dotpmem-dotfreaders is used by rely-PERSIST_W,
FLIT/updsel--dotpmem-dotfwriters is used by rely-PERSIST_W, step-PERSIST_W,
FLIT/updsel--dotpmem-dotrfo is used by rely-PERSIST_W, step-PERSIST_W,
FLIT/updsel--dotpq-dotbq is used by rely-PERSIST_W, step-PERSIST_W, step-PERSIST_FO, rely-PERSIST_FO,
FLIT/updsel--dotpq-dotfctr is used by step-PERSIST_W, step-PERSIST_FO, step-PROP_W, step-PROP_FO,
FLIT/updsel--dotpq-dotfreaders is used by rely-PERSIST_W, rely-PROP_FO, rely-PERSIST_FO, rely-PROP_W,
FLIT/updsel--dotpq-dotfwriters is used by rely-PERSIST_W, step-PERSIST_W, rely-PROP_FO, step-PERSIST_FO, step-PROP_W, rely-PERSIST_FO, step-PROP_FO, rely-PROP_W,
FLIT/updsel--dotpq-dotpq is used by rely-PERSIST_W, step-PERSIST_W, rely-PROP_FO, step-CRASH, step-PERSIST_FO, step-PROP_W, rely-PERSIST_FO, step-PROP_FO, rely-PROP_W,
FLIT/updsel--dotpq-dotrfo is used by rely-PERSIST_W, step-PERSIST_W, step-PERSIST_FO, step-PROP_W, rely-PERSIST_FO, rely-PROP_W,
FLIT/updsel--dotrfo-dotbq is used by rely-PROP_FO, step-CRASH, rely-R3-R4, step-PROP_FO, step-R3-R4,
FLIT/updsel--dotrfo-dotfctr is used by step-CRASH, step-PROP_FO, step-R3-R4,
FLIT/updsel--dotrfo-dotfreaders is used by rely-PROP_FO, step-CRASH,
FLIT/updsel--dotrfo-dotfwriters is used by rely-PROP_FO, step-CRASH, rely-R3-R4, step-PROP_FO, step-R3-R4,
FLIT/updsel--dotrfo-dotpq is used by rely-PROP_FO, step-CRASH, rely-R3-R4, step-PROP_FO, step-R3-R4,
FLIT/updsel--dotrfo-dotrfo is used by rely-PROP_FO, step-CRASH, rely-R3-R4, step-PROP_FO, step-R3-R4,
FLIT/updsel--dotval-dotloc is used by step-R1-R2,
FLIT/updsel--dotval-dott is used by step-R1-R2, step-ready-W1,

Used from specification list-data

list-data/elim-add is used by stable-W4, rely-PERSIST_W, step-PERSIST_W, step-PROP_SF, step-PERSIST_FO, step-PROP_W, stable-W5, rely-PERSIST_FO, stable-W6, rely-PROP_W, rely-PROP_SF,
list-data/elim-list-c is used by step-W4-W5, step-W5-W6,
list-data/l is used by rely-PROP_FO, step-PROP_FO,
list-data/size-nil is used by step-CRASH, init-state-inv,

Used from specification filter-count

filter-count/filter-in is used by step-W2-W3,

Used from specification Bevent

Bevent/disj-FO-SF is used by step-W4-W5, stable-W5, step-R3-R4, stable-W6, step-W5-W6,
Bevent/disj-W-FO is used by step-W4-W5, stable-W5, stable-W6, step-W5-W6,
Bevent/disj-W-SF is used by step-W4-W5, stable-W4, step-W3-W4, stable-W5, stable-W6, rely-PROP_W, step-W5-W6,
Bevent/elim-W is used by step-PROP_W, rely-PROP_W,
Bevent/inj-W is used by step-W3-W4, step-W5-W6,
Bevent/sel-FO-dotl is used by stable-W5, stable-W6,
Bevent/sel-W-dotl is used by stable-W5, stable-W6,
Bevent/test-dotWque-FO is used by step-W4-W5, stable-W5, stable-W6, step-W5-W6,
Bevent/test-dotWque-SF is used by stable-W6, step-W5-W6,
Bevent/test-dotWque-W is used by step-W4-W5, step-W3-W4, step-PROP_W, rely-PROP_W, step-W5-W6,

Used from specification list-del

list-del/delnr-one is used by rely-PROP_FO,
list-del/delpos-empty is used by rely-PROP_FO,