[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,

Lemma dependency for Specification PLIB

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
plibStep-lemprovedall subs proved inj-mkPLIBgs, sel-mkPLIBgs-doth, sel-mkPLIBgs-dotpm, upd-mkPLIBgs-doth, upd-mkPLIBgs-dotvm, gen-PLIBGState, ACrash, disj-globalACrash-globalAPersist, plibStep,
not-pre-global-crashprovedall subs proved disj-ARetWrite-globalACrash, pre-resWrite, disj-ARetRead-globalACrash, pre-resRead, disj-AInvRead-globalACrash, disj-AInvWrite-globalACrash, disj-callTSync-globalACrash, pre-ready, disj-ADoWrite-globalACrash, pre-invWrite, disj-ADoRead-globalACrash, pre-invRead, disj-callARun-globalACrash, pre-idle, pre-crashed, gen-PLIBPC, gen-PLIBGState,
plib-inv-allReadsOKprovedall subs proved sel-mkPLIBgs-doth, sel-mkPLIBgs-dotpm, sel-mkPLIBgs-dotvm, PLIBGInv, PLIBInv,
not-pre-global-persistprovedall subs proved disj-ARetWrite-globalAPersist, pre-resWrite, disj-ARetRead-globalAPersist, pre-resRead, disj-AInvRead-globalAPersist, disj-AInvWrite-globalAPersist, disj-callTSync-globalAPersist, pre-ready, disj-ADoWrite-globalAPersist, pre-invWrite, disj-ADoRead-globalAPersist, pre-invRead, disj-callARun-globalAPersist, pre-idle, pre-crashed, gen-PLIBPC, gen-PLIBGState,
disj-callARun-globalAPersistaxiom
disj-ADoRead-globalAPersistaxiom
disj-ADoWrite-globalAPersistaxiom
disj-callTSync-globalAPersistaxiom
disj-AInvWrite-globalAPersistaxiom
disj-AInvRead-globalAPersistaxiom
disj-ARetRead-globalAPersistaxiom
disj-ARetWrite-globalAPersistaxiom
PLIBInvaxiom
PLIBGInvaxiom
sel-mkPLIBgs-dotvmaxiom
gen-PLIBPCaxiom
pre-crashedaxiom
pre-idleaxiom
disj-callARun-globalACrashaxiom
pre-invReadaxiom
disj-ADoRead-globalACrashaxiom
pre-invWriteaxiom
disj-ADoWrite-globalACrashaxiom
pre-readyaxiom
disj-callTSync-globalACrashaxiom
disj-AInvWrite-globalACrashaxiom
disj-AInvRead-globalACrashaxiom
pre-resReadaxiom
disj-ARetRead-globalACrashaxiom
pre-resWriteaxiom
disj-ARetWrite-globalACrashaxiom
plibStepaxiom
disj-globalACrash-globalAPersistaxiom
ACrashaxiom
gen-PLIBGStateaxiom
upd-mkPLIBgs-dotvmaxiom
upd-mkPLIBgs-dothaxiom
sel-mkPLIBgs-dotpmaxiom
sel-mkPLIBgs-dothaxiom
inj-mkPLIBgsaxiom