[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

nat/le-def is used by rely-APersist,
nat/lels is used by step-APersist,
nat/lels-03 is used by definedness-APersist,
nat/lep is used by rely-APersist,
nat/ler is used by step-APersist,
nat/not-zero is used by rely-APersist,
nat/succ-01 is used by definedness-APersist,
nat/zero is used by step-APersist,

Used from specification PLIB

PLIB/PLIBGInv is used by init-state-inv,
PLIB/PLIBInv is used by init-state-inv,
PLIB/PLIBLInv is used by init-state-inv, step-ACrash,
PLIB/disj-crashed-resWrite is used by step-ACrash,
PLIB/disj-idle-resWrite is used by init-state-inv, step-ACrash,
PLIB/gstepf-idle-ARun is used by step-idle-ready,
PLIB/gstepf-invRead-ADOREAD is used by step-invRead-resRead, rely-invRead-resRead,
PLIB/gstepf-invWrite-DOWRITE is used by rely-invWrite-resWrite, step-invWrite-resWrite,
PLIB/gstepf-ready is used by step-ready-ready, step-ready-invWrite, step-ready-invRead,
PLIB/gstepf-resRead-ARETREAD is used by step-resRead-ready,
PLIB/gstepf-resWrite-RETWRITE is used by step-resWrite-ready,
PLIB/lstepf-invWrite-DOWRITE is used by step-invWrite-resWrite,
PLIB/pcstepf-idle-ARun is used by step-idle-ready,
PLIB/pcstepf-invRead-ADOREAD is used by step-invRead-resRead, rely-invRead-resRead,
PLIB/pcstepf-invWrite-DOWRITE is used by rely-invWrite-resWrite, step-invWrite-resWrite,
PLIB/pcstepf-resRead-ARETREAD is used by step-resRead-ready,
PLIB/pcstepf-resWrite-RETWRITE is used by step-resWrite-ready,
PLIB/pre-idle is used by step-idle-ready,
PLIB/pre-invRead is used by step-invRead-resRead, rely-invRead-resRead,
PLIB/pre-invWrite is used by rely-invWrite-resWrite, step-invWrite-resWrite,
PLIB/pre-ready is used by step-ready-ready, step-ready-invWrite, step-ready-invRead,
PLIB/pre-resRead is used by step-resRead-ready,
PLIB/pre-resWrite is used by step-resWrite-ready,
PLIB/updsel--doth-doth is used by rely-APersist, step-invRead-resRead, rely-invRead-resRead, rely-invWrite-resWrite, step-ACrash, step-invWrite-resWrite, step-APersist,
PLIB/updsel--doth-dotpm is used by step-invRead-resRead, step-ACrash, step-invWrite-resWrite, step-APersist,
PLIB/updsel--doth-dotvm is used by step-invRead-resRead, step-ACrash, step-invWrite-resWrite, step-APersist,
PLIB/updsel--dotpm-dotpm is used by step-APersist,
PLIB/updsel--dotpm-dotvm is used by step-APersist,
PLIB/updsel--dotvm-dotpm is used by step-ACrash, step-invWrite-resWrite,
PLIB/updsel--dotvm-dotvm is used by step-ACrash, step-invWrite-resWrite,

Used from specification PLIB-preds

PLIB-preds/allReadsOK-def is used by init-state-inv,
PLIB-preds/allWritesOK-def is used by init-state-inv,
PLIB-preds/allreadsok-add-read is used by step-invRead-resRead,
PLIB-preds/allreadsok-persist is used by step-APersist,
PLIB-preds/allwritesOK-one-unpersisted-write-no-persisted-after is used by step-APersist,
PLIB-preds/allwritesOK-persist-dependent-reads is used by step-APersist,
PLIB-preds/allwritesOK-persist-one-write is used by step-APersist,
PLIB-preds/first-vol-write-split is used by step-APersist,
PLIB-preds/lastwrite-to-update is used by step-APersist,
PLIB-preds/allReadsOKInd-base is used by init-state-inv,
PLIB-preds/allWritesOKInd-base is used by init-state-inv,
PLIB-preds/allreadsOK-filter-persisted is used by step-ACrash,
PLIB-preds/allreadsok-add-write is used by step-invWrite-resWrite,
PLIB-preds/allwritesOK-add-read is used by step-invRead-resRead,
PLIB-preds/allwritesOK-add-write is used by step-invWrite-resWrite,
PLIB-preds/allwritesOK-filter-persisted is used by step-ACrash,
PLIB-preds/first-vol-write-size is used by rely-APersist, definedness-APersist, step-APersist,
PLIB-preds/first-vol-write-size2 is used by rely-APersist,
PLIB-preds/first-vol-write-size3 is used by rely-APersist,
PLIB-preds/overwrite-attach-read is used by step-invRead-resRead,
PLIB-preds/overwrite-attach-write is used by step-invWrite-resWrite,
PLIB-preds/overwrite-base is used by init-state-inv,
PLIB-preds/overwrite-persist-dependent-reads is used by step-APersist,
PLIB-preds/overwrite-persist-dependent-reads-restrict-true is used by step-APersist,
PLIB-preds/overwrite-persist-one-write is used by step-APersist,
PLIB-preds/rely-attach is used by rely-invRead-resRead, rely-invWrite-resWrite,
PLIB-preds/rely-persist is used by rely-APersist,
PLIB-preds/rely-refl is used by rely-reflexive, rely-TSync,
PLIB-preds/rely-stable-write-empty is used by stable-resWrite,
PLIB-preds/rely-stable-write-one is used by stable-resWrite,
PLIB-preds/restrict-W-append is used by rely-APersist, step-APersist,
PLIB-preds/restrict-W-empty is used by rely-APersist,
PLIB-preds/restrict-b-append is used by rely-APersist, step-invRead-resRead, step-APersist,
PLIB-preds/restrict-b-empty is used by rely-APersist, init-state-inv,
PLIB-preds/restrict-b-idem is used by step-ACrash,
PLIB-preds/restrict-bool-one is used by rely-APersist, step-invRead-resRead,
PLIB-preds/restrict-false-attach-false is used by step-invWrite-resWrite,
PLIB-preds/restrict-false-false is used by step-APersist,
PLIB-preds/restrict-l-W-same is used by step-APersist,
PLIB-preds/restrict-l-append is used by rely-APersist, step-APersist,
PLIB-preds/restrict-l-empty is used by rely-APersist,
PLIB-preds/restrict-t-append is used by step-invWrite-resWrite,
PLIB-preds/restrict-t-one is used by step-invWrite-resWrite,
PLIB-preds/restrict-true-attach-false is used by step-invWrite-resWrite,
PLIB-preds/restrict-true-false is used by step-APersist,
PLIB-preds/restrict-true-true is used by step-APersist,
PLIB-preds/restrict-write-W is used by step-APersist,
PLIB-preds/restrict-write-one is used by rely-APersist,
PLIB-preds/take-first-vol-write-no-unpersisted-writes is used by step-APersist,

Used from specification list-data

list-data/elim-list-c is used by rely-APersist,
list-data/l is used by rely-APersist,
list-data/lf-01 is used by rely-APersist,

Used from specification nat-basic

nat-basic/a is used by rely-APersist, definedness-APersist,
nat-basic/c is used by rely-APersist, definedness-APersist,
nat-basic/f is used by step-APersist,
nat-basic/one-01 is used by rely-APersist,
nat-basic/oz is used by rely-APersist,
nat-basic/refl-Nat is used by step-APersist,
nat-basic/succ is used by rely-APersist,

Used from specification list

list/Last is used by step-invRead-resRead, rely-invRead-resRead, rely-invWrite-resWrite, step-invWrite-resWrite,
list/Nil is used by rely-APersist, step-APersist,
list/a is used by rely-APersist, step-invRead-resRead, rely-invRead-resRead, rely-invWrite-resWrite, step-invWrite-resWrite, step-APersist,
list/app is used by rely-APersist, step-invRead-resRead,
list/app-02 is used by rely-APersist, step-invWrite-resWrite, step-APersist,
list/c is used by rely-APersist, step-APersist,
list/c-03 is used by rely-APersist,
list/c-04 is used by stable-resWrite,
list/c-05 is used by step-invWrite-resWrite,
list/e is used by rely-APersist, step-invWrite-resWrite, step-APersist,
list/len is used by rely-APersist,
list/len-05 is used by rely-APersist,

Used from specification RWevent

RWevent/sel-R-dott is used by rely-invRead-resRead,
RWevent/sel-W-dott is used by rely-invWrite-resWrite, step-invWrite-resWrite,
RWevent/sel-W-dotv is used by step-APersist,

Used from specification list-del

list-del/get-append-grt is used by step-APersist,
list-del/elim-firstn-restn is used by rely-APersist,
list-del/first-length is used by step-APersist,
list-del/get-app is used by rely-APersist,
list-del/get-append-less is used by step-APersist,
list-del/get-zero is used by step-APersist,
list-del/restn-app is used by rely-APersist,