[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 nat
- FLITPSC-preds/FOFollowsW-def
is used by
step-W5-W6,
- FLITPSC-preds/ctrok-def
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSC-preds/filtertid-def
is used by
step-W1-W2,
- FLITPSC-preds/filterwrites-def
is used by
step-W1-W2,
- FLITPSC-preds/noPending
is used by
step-PSCCRASH,
init-state-inv,
step-W1-W2,
step-W5-W6,
- FLITPSC-preds/noPendingW
is used by
step-W1-W2,
- FLITPSC-preds/noWriter
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSC-preds/onePendingW
is used by
step-W5-W6,
- FLITPSC-preds/pendingOk
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSC-preds/writersOk
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSC-preds/add-pending-fo-ok
is used by
step-W4-W5,
step-R3-R4,
- FLITPSC-preds/add-pending-w-ok
is used by
step-W3-W4,
- FLITPSC-preds/add-pending-w-one-pending
is used by
step-W3-W4,
- FLITPSC-preds/ctrok-add-writer
is used by
step-W2-W3,
- FLITPSC-preds/ctrok-rm-writer
is used by
step-W6-W7,
- FLITPSC-preds/filter-tid-empty
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSC-preds/filter-w-empty
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSC-preds/fo-follows-last
is used by
step-W4-W5,
- FLITPSC-preds/in-filter-W
is used by
step-W5-W6,
- FLITPSC-preds/in-filter-t
is used by
step-W1-W2,
step-W5-W6,
- FLITPSC-preds/no-pending-w-add-fo-stable
is used by
step-R3-R4,
- FLITPSC-preds/no-pending-w-no-pending
is used by
step-idle-ready,
step-PSCCRASH,
step-W7-ready,
init-state-inv,
- FLITPSC-preds/nomember-to-onemember
is used by
step-R1-R2,
step-W2-W3,
- FLITPSC-preds/one-pending-add-stable
is used by
step-W4-W5,
- 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/pendingsok-del-pos
is used by
step-PSCPERSIST_FO,
step-PSCPERSIST_W,
- FLITPSC-preds/relyws-add-other-writer
is used by
rely-W2-W3,
rely-R1-R2,
- FLITPSC-preds/relyws-noWriter-stable
is used by
stable-W4,
stable-W1,
stable-W7,
stable-R1,
stable-W5,
stable-W2,
stable-R2,
stable-W3,
stable-idle,
- FLITPSC-preds/relyws-oneWriter-stable
is used by
stable-W4,
stable-W5,
stable-R2,
stable-W3,
- FLITPSC-preds/relyws-refl
is used by
rely-W3-W4,
rely-W2-W3,
rely-R3-R4,
rely-W6-W7,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
rely-R2-R3,
rely-R1-R2,
rely-reflexive,
rely-W4-W5,
rely-R2-R4,
- FLITPSC-preds/relyws-rm-other-writer
is used by
rely-R3-R4,
rely-W6-W7,
rely-R2-R4,
- FLITPSC-preds/writersok-add-fo
is used by
step-W4-W5,
step-R3-R4,
- FLITPSC-preds/writersok-add-pending
is used by
step-W3-W4,
- FLITPSC-preds/writersok-add-writer
is used by
step-W2-W3,
- FLITPSC-preds/writersok-del-pos
is used by
step-PSCPERSIST_FO,
step-PSCPERSIST_W,
- FLITPSC-preds/writersok-rm-writer
is used by
step-W6-W7,
Used from specification set-basic
- FLITPSCweak-preds/at-firstPersistW-is-W
is used by
definedness-PSCPERSIST_W,
- FLITPSCweak-preds/rely-add-other-fo
is used by
rely-R3-R4,
rely-W4-W5,
- FLITPSCweak-preds/rely-add-other-w
is used by
rely-W3-W4,
- FLITPSCweak-preds/rely-fo-follows-w-stable
is used by
stable-W5,
- FLITPSCweak-preds/rely-no-pending-stable
is used by
stable-W7,
stable-W2,
stable-W3,
stable-idle,
- FLITPSCweak-preds/rely-no-pending-w-stable
is used by
stable-W1,
stable-R1,
stable-W2,
stable-R2,
stable-idle,
- FLITPSCweak-preds/rely-one-pending-stable
is used by
stable-W4,
stable-W5,
- FLITPSCweak-preds/rely-persist-FO-weak
is used by
rely-PSCPERSIST_FO,
- FLITPSCweak-preds/rely-persist-W-weak
is used by
rely-PSCPERSIST_W,
- FLITPSCweak-preds/rely-refl
is used by
rely-W2-W3,
rely-W6-W7,
rely-PSCPERSIST_FO,
rely-R2-R3,
rely-R1-R2,
rely-reflexive,
rely-R2-R4,
Used from specification list-data
Used from specification nat-basic
Used from specification list
- list/some-element
is used by
step-W1-W2,
step-W5-W6,
- list/Last
is used by
step-W4-W5,
rely-W3-W4,
step-W3-W4,
rely-R3-R4,
step-R3-R4,
rely-W4-W5,
- list/a
is used by
step-W4-W5,
rely-W3-W4,
step-W3-W4,
rely-R3-R4,
step-R3-R4,
rely-W4-W5,
Used from specification FLITPSCweak
- FLITPSCweak/FLITPSCGInv
is used by
init-state-inv,
- FLITPSCweak/FLITPSCInv
is used by
init-state-inv,
- FLITPSCweak/FLITPSCLInv
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-R1-W1
is used by
step-ready-W1,
step-ready-R1,
- FLITPSCweak/disj-R1-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-R1-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-R1-ready
is used by
step-ready-ready,
step-ready-R1,
- FLITPSCweak/disj-R2-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-R2-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-R3-R4
is used by
step-R2-R4,
rely-R2-R3,
step-R2-R3,
rely-R2-R4,
- FLITPSCweak/disj-R3-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-R3-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-R4-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-R4-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W1-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W1-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W1-ready
is used by
step-ready-ready,
step-ready-W1,
- FLITPSCweak/disj-W2-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W2-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W3-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W3-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W4-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W4-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W5-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W5-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W6-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W6-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-W7-crashed
is used by
step-PSCCRASH,
- FLITPSCweak/disj-W7-idle
is used by
step-PSCCRASH,
init-state-inv,
- FLITPSCweak/disj-callPSCCOMPLETE-invFLITPSCREAD
is used by
step-ready-ready,
- FLITPSCweak/disj-callPSCCOMPLETE-invFLITPSCWRITE
is used by
step-ready-ready,
- FLITPSCweak/disj-crashed-idle
is used by
step-PSCCRASH,
- FLITPSCweak/disj-crashed-ready
is used by
step-PSCCRASH,
- FLITPSCweak/disj-invFLITPSCREAD-invFLITPSCWRITE
is used by
step-ready-W1,
step-ready-R1,
- FLITPSCweak/elim-mkFLITPSCgs
is used by
step-W1-W2,
step-W6-W7,
step-W5-W6,
- FLITPSCweak/elim-mkFLITPSCls
is used by
step-W1-W2,
step-W6-W7,
step-W5-W6,
- FLITPSCweak/gstepf-R1
is used by
step-R1-R2,
rely-R1-R2,
- FLITPSCweak/gstepf-R2
is used by
step-R2-R4,
rely-R2-R3,
step-R2-R3,
rely-R2-R4,
- FLITPSCweak/gstepf-R3
is used by
rely-R3-R4,
step-R3-R4,
- FLITPSCweak/gstepf-R4
is used by
step-R4-ready,
- FLITPSCweak/gstepf-W1
is used by
step-W1-W2,
- FLITPSCweak/gstepf-W2
is used by
rely-W2-W3,
step-W2-W3,
- FLITPSCweak/gstepf-W3
is used by
rely-W3-W4,
step-W3-W4,
- FLITPSCweak/gstepf-W4
is used by
step-W4-W5,
rely-W4-W5,
- FLITPSCweak/gstepf-W5
is used by
step-W5-W6,
- FLITPSCweak/gstepf-W6
is used by
rely-W6-W7,
step-W6-W7,
- FLITPSCweak/gstepf-W7
is used by
step-W7-ready,
- FLITPSCweak/gstepf-idle-PSCRUN
is used by
step-idle-ready,
- FLITPSCweak/gstepf-ready
is used by
step-ready-ready,
step-ready-W1,
step-ready-R1,
- FLITPSCweak/lstepf-R1
is used by
step-R1-R2,
- FLITPSCweak/lstepf-R2
is used by
step-R2-R4,
step-R2-R3,
- FLITPSCweak/lstepf-R3
is used by
step-R3-R4,
- FLITPSCweak/lstepf-R4
is used by
step-R4-ready,
- FLITPSCweak/lstepf-W1
is used by
step-W1-W2,
- FLITPSCweak/lstepf-W2
is used by
step-W2-W3,
- FLITPSCweak/lstepf-W3
is used by
step-W3-W4,
- FLITPSCweak/lstepf-W4
is used by
step-W4-W5,
- FLITPSCweak/lstepf-W5
is used by
step-W5-W6,
- FLITPSCweak/lstepf-W6
is used by
step-W6-W7,
- FLITPSCweak/lstepf-W7
is used by
step-W7-ready,
- FLITPSCweak/lstepf-idle-PSCRUN
is used by
step-idle-ready,
- FLITPSCweak/lstepf-ready-FLITPSCREAD
is used by
step-ready-R1,
- FLITPSCweak/lstepf-ready-FLITPSCWRITE
is used by
step-ready-W1,
- FLITPSCweak/lstepf-ready-PSCCOMPLETE
is used by
step-ready-ready,
- FLITPSCweak/pcstepf-R1
is used by
step-R1-R2,
rely-R1-R2,
- FLITPSCweak/pcstepf-R2
is used by
step-R2-R4,
rely-R2-R3,
step-R2-R3,
rely-R2-R4,
- FLITPSCweak/pcstepf-R3
is used by
rely-R3-R4,
step-R3-R4,
- FLITPSCweak/pcstepf-R4
is used by
step-R4-ready,
- FLITPSCweak/pcstepf-W1
is used by
step-W1-W2,
- FLITPSCweak/pcstepf-W2
is used by
rely-W2-W3,
step-W2-W3,
- FLITPSCweak/pcstepf-W3
is used by
rely-W3-W4,
step-W3-W4,
- FLITPSCweak/pcstepf-W4
is used by
step-W4-W5,
rely-W4-W5,
- FLITPSCweak/pcstepf-W5
is used by
step-W5-W6,
- FLITPSCweak/pcstepf-W6
is used by
rely-W6-W7,
step-W6-W7,
- FLITPSCweak/pcstepf-W7
is used by
step-W7-ready,
- FLITPSCweak/pcstepf-idle-PSCRUN
is used by
step-idle-ready,
- FLITPSCweak/pcstepf-ready-FLITPSCREAD
is used by
step-ready-ready,
step-ready-W1,
step-ready-R1,
- FLITPSCweak/pcstepf-ready-FLITPSCWRITE
is used by
step-ready-ready,
step-ready-W1,
step-ready-R1,
- FLITPSCweak/pcstepf-ready-PSCCOMPLETE
is used by
step-ready-ready,
step-ready-W1,
step-ready-R1,
- FLITPSCweak/pre-R1
is used by
step-R1-R2,
rely-R1-R2,
- FLITPSCweak/pre-R2
is used by
step-R2-R4,
definedness-R2,
rely-R2-R3,
step-R2-R3,
rely-R2-R4,
- FLITPSCweak/pre-R3
is used by
rely-R3-R4,
step-R3-R4,
- FLITPSCweak/pre-R4
is used by
step-R4-ready,
- FLITPSCweak/pre-W1
is used by
step-W1-W2,
- FLITPSCweak/pre-W2
is used by
rely-W2-W3,
step-W2-W3,
- FLITPSCweak/pre-W3
is used by
rely-W3-W4,
step-W3-W4,
- FLITPSCweak/pre-W4
is used by
step-W4-W5,
rely-W4-W5,
- FLITPSCweak/pre-W5
is used by
step-W5-W6,
- FLITPSCweak/pre-W6
is used by
rely-W6-W7,
definedness-W6,
step-W6-W7,
- FLITPSCweak/pre-W7
is used by
step-W7-ready,
- FLITPSCweak/pre-idle
is used by
step-idle-ready,
- FLITPSCweak/pre-ready
is used by
step-ready-ready,
step-ready-W1,
step-ready-R1,
- FLITPSCweak/updsel--dotctr-dotctr
is used by
step-W2-W3,
step-PSCCRASH,
step-W6-W7,
- FLITPSCweak/updsel--dotctr-dotp
is used by
rely-W2-W3,
step-W2-W3,
step-PSCCRASH,
rely-W6-W7,
step-W6-W7,
- FLITPSCweak/updsel--dotctr-dotreaders
is used by
rely-W2-W3,
step-W2-W3,
rely-W6-W7,
step-W6-W7,
- FLITPSCweak/updsel--dotl-dott
is used by
step-ready-W1,
step-ready-R1,
- FLITPSCweak/updsel--dotmem-dotctr
is used by
step-PSCPERSIST_W,
- FLITPSCweak/updsel--dotmem-dotreaders
is used by
rely-PSCPERSIST_W,
- FLITPSCweak/updsel--dotmem-dotwriters
is used by
rely-PSCPERSIST_W,
step-PSCPERSIST_W,
- FLITPSCweak/updsel--dotp-dotctr
is used by
step-W4-W5,
step-PSCPERSIST_FO,
step-W3-W4,
step-PSCPERSIST_W,
step-R3-R4,
- FLITPSCweak/updsel--dotp-dotp
is used by
step-W4-W5,
rely-W3-W4,
step-PSCPERSIST_FO,
step-W3-W4,
step-PSCCRASH,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
step-PSCPERSIST_W,
step-R3-R4,
rely-W4-W5,
- FLITPSCweak/updsel--dotp-dotreaders
is used by
step-W4-W5,
rely-W3-W4,
step-W3-W4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
rely-W4-W5,
- FLITPSCweak/updsel--dotp-dotwriters
is used by
step-W4-W5,
rely-W3-W4,
step-PSCPERSIST_FO,
step-W3-W4,
rely-R3-R4,
rely-PSCPERSIST_W,
rely-PSCPERSIST_FO,
step-PSCPERSIST_W,
step-R3-R4,
rely-W4-W5,
- FLITPSCweak/updsel--dotreaders-dotctr
is used by
step-R1-R2,
step-R2-R4,
step-PSCCRASH,
step-R3-R4,
- FLITPSCweak/updsel--dotreaders-dotp
is used by
step-R1-R2,
step-R2-R4,
step-PSCCRASH,
rely-R3-R4,
rely-R1-R2,
step-R3-R4,
rely-R2-R4,
- FLITPSCweak/updsel--dotreaders-dotreaders
is used by
step-R1-R2,
step-R2-R4,
step-PSCCRASH,
rely-R3-R4,
rely-R1-R2,
step-R3-R4,
rely-R2-R4,
- FLITPSCweak/updsel--dotreaders-dotwriters
is used by
step-R1-R2,
step-R2-R4,
step-PSCCRASH,
rely-R3-R4,
rely-R1-R2,
step-R3-R4,
rely-R2-R4,
- FLITPSCweak/updsel--dotv-dotl
is used by
step-R1-R2,
- FLITPSCweak/updsel--dotv-dott
is used by
step-R1-R2,
step-ready-W1,
- FLITPSCweak/updsel--dotwriters-dotctr
is used by
step-W2-W3,
step-PSCCRASH,
step-W6-W7,
- FLITPSCweak/updsel--dotwriters-dotp
is used by
rely-W2-W3,
step-W2-W3,
step-PSCCRASH,
rely-W6-W7,
step-W6-W7,
- FLITPSCweak/updsel--dotwriters-dotreaders
is used by
rely-W2-W3,
step-W2-W3,
rely-W6-W7,
step-W6-W7,
- FLITPSCweak/updsel--dotwriters-dotwriters
is used by
rely-W2-W3,
step-W2-W3,
step-PSCCRASH,
rely-W6-W7,
step-W6-W7,
Used from specification FOW
Used from specification list-del