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

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:
fliqtStep-lemprovedall subs proved PSCCRASH, disj-globalPSCCRASH-globalPSCPERSISTuscW, not-pre-global-crash, upd-mkFLITPSCgs-dotreaders, upd-mkFLITPSCgs-dotwriters, upd-mkFLITPSCgs-dotctr, sel-mkFLITPSCgs-dotctr, sel-mkFLITPSCgs-dotreaders, sel-mkFLITPSCgs-dotwriters, PSCPERSIST_FO, inj-mkFLITPSCgs, inj-globalPSCPERSISTuscFO, disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscW, not-pre-global-tsync, disj-globalPSCCRASH-globalPSCPERSISTuscFO, sel-mkFLITPSCgs-dotp, sel-mkFLITPSCgs-dotmem, flitpscStep, upd-mkFLITPSCgs-dotp, upd-mkFLITPSCgs-dotmem, elim-mkFLITPSCgs, lstep,
not-pre-global-tsyncprovedall subs proved disj-callPSCCOMPLETE-globalPSCPERSISTuscFO, disj-globalPSCPERSISTuscFO-invFLITPSCREAD, disj-globalPSCPERSISTuscFO-invFLITPSCWRITE, pre-ready, disj-callPSCRUN-globalPSCPERSISTuscFO, pre-idle, pre-crashed, disj-globalPSCPERSISTuscFO-retFLITPSCWRITE, pre-W7, disj-ctrDecPSC-globalPSCPERSISTuscFO, pre-W6, pre-W5, pre-W4, disj-doWritePSC-globalPSCPERSISTuscFO, pre-W3, disj-ctrIncPSC-globalPSCPERSISTuscFO, pre-W2, disj-globalPSCPERSISTuscFO-sfencePSC, pre-W1, disj-globalPSCPERSISTuscFO-retFLITPSCREAD, pre-R4, disj-globalPSCPERSISTuscFO-pwbPSC, pre-R3, disj-ctrReadPSC-globalPSCPERSISTuscFO, pre-R2, disj-doReadPSC-globalPSCPERSISTuscFO, pre-R1, gen-FLITPSCPC,
not-pre-global-crashprovedall subs proved disj-callPSCCOMPLETE-globalPSCCRASH, disj-globalPSCCRASH-invFLITPSCREAD, disj-globalPSCCRASH-invFLITPSCWRITE, pre-ready, disj-callPSCRUN-globalPSCCRASH, pre-idle, pre-crashed, disj-globalPSCCRASH-retFLITPSCWRITE, pre-W7, disj-ctrDecPSC-globalPSCCRASH, pre-W6, pre-W5, pre-W4, disj-doWritePSC-globalPSCCRASH, pre-W3, disj-ctrIncPSC-globalPSCCRASH, pre-W2, disj-globalPSCCRASH-sfencePSC, pre-W1, disj-globalPSCCRASH-retFLITPSCREAD, pre-R4, disj-globalPSCCRASH-pwbPSC, pre-R3, disj-ctrReadPSC-globalPSCCRASH, pre-R2, disj-doReadPSC-globalPSCCRASH, pre-R1, gen-FLITPSCPC,
not-pre-global-persistprovedall subs proved disj-callPSCCOMPLETE-globalPSCPERSISTuscW, disj-globalPSCPERSISTuscW-invFLITPSCREAD, disj-globalPSCPERSISTuscW-invFLITPSCWRITE, pre-ready, disj-callPSCRUN-globalPSCPERSISTuscW, pre-idle, pre-crashed, disj-globalPSCPERSISTuscW-retFLITPSCWRITE, pre-W7, disj-ctrDecPSC-globalPSCPERSISTuscW, pre-W6, pre-W5, pre-W4, disj-doWritePSC-globalPSCPERSISTuscW, pre-W3, disj-ctrIncPSC-globalPSCPERSISTuscW, pre-W2, disj-globalPSCPERSISTuscW-sfencePSC, pre-W1, disj-globalPSCPERSISTuscW-retFLITPSCREAD, pre-R4, disj-globalPSCPERSISTuscW-pwbPSC, pre-R3, disj-ctrReadPSC-globalPSCPERSISTuscW, pre-R2, disj-doReadPSC-globalPSCPERSISTuscW, pre-R1, gen-FLITPSCPC,
disj-doReadPSC-globalPSCPERSISTuscWaxiom
disj-ctrReadPSC-globalPSCPERSISTuscWaxiom
disj-globalPSCPERSISTuscW-pwbPSCaxiom
disj-globalPSCPERSISTuscW-retFLITPSCREADaxiom
disj-globalPSCPERSISTuscW-sfencePSCaxiom
disj-ctrIncPSC-globalPSCPERSISTuscWaxiom
disj-doWritePSC-globalPSCPERSISTuscWaxiom
disj-ctrDecPSC-globalPSCPERSISTuscWaxiom
disj-globalPSCPERSISTuscW-retFLITPSCWRITEaxiom
disj-callPSCRUN-globalPSCPERSISTuscWaxiom
disj-globalPSCPERSISTuscW-invFLITPSCWRITEaxiom
disj-globalPSCPERSISTuscW-invFLITPSCREADaxiom
disj-callPSCCOMPLETE-globalPSCPERSISTuscWaxiom
lstepaxiom
elim-mkFLITPSCgsaxiom
upd-mkFLITPSCgs-dotmemaxiom
upd-mkFLITPSCgs-dotpaxiom
flitpscStepaxiom
sel-mkFLITPSCgs-dotmemaxiom
sel-mkFLITPSCgs-dotpaxiom
disj-globalPSCCRASH-globalPSCPERSISTuscFOaxiom
disj-globalPSCPERSISTuscFO-globalPSCPERSISTuscWaxiom
inj-globalPSCPERSISTuscFOaxiom
inj-mkFLITPSCgsaxiom
PSCPERSIST_FOaxiom
sel-mkFLITPSCgs-dotwritersaxiom
sel-mkFLITPSCgs-dotreadersaxiom
sel-mkFLITPSCgs-dotctraxiom
upd-mkFLITPSCgs-dotctraxiom
upd-mkFLITPSCgs-dotwritersaxiom
upd-mkFLITPSCgs-dotreadersaxiom
disj-globalPSCCRASH-globalPSCPERSISTuscWaxiom
PSCCRASHaxiom
disj-doReadPSC-globalPSCPERSISTuscFOaxiom
disj-ctrReadPSC-globalPSCPERSISTuscFOaxiom
disj-globalPSCPERSISTuscFO-pwbPSCaxiom
disj-globalPSCPERSISTuscFO-retFLITPSCREADaxiom
disj-globalPSCPERSISTuscFO-sfencePSCaxiom
disj-ctrIncPSC-globalPSCPERSISTuscFOaxiom
disj-doWritePSC-globalPSCPERSISTuscFOaxiom
disj-ctrDecPSC-globalPSCPERSISTuscFOaxiom
disj-globalPSCPERSISTuscFO-retFLITPSCWRITEaxiom
disj-callPSCRUN-globalPSCPERSISTuscFOaxiom
disj-globalPSCPERSISTuscFO-invFLITPSCWRITEaxiom
disj-globalPSCPERSISTuscFO-invFLITPSCREADaxiom
disj-callPSCCOMPLETE-globalPSCPERSISTuscFOaxiom
gen-FLITPSCPCaxiom
pre-R1axiom
disj-doReadPSC-globalPSCCRASHaxiom
pre-R2axiom
disj-ctrReadPSC-globalPSCCRASHaxiom
pre-R3axiom
disj-globalPSCCRASH-pwbPSCaxiom
pre-R4axiom
disj-globalPSCCRASH-retFLITPSCREADaxiom
pre-W1axiom
disj-globalPSCCRASH-sfencePSCaxiom
pre-W2axiom
disj-ctrIncPSC-globalPSCCRASHaxiom
pre-W3axiom
disj-doWritePSC-globalPSCCRASHaxiom
pre-W4axiom
pre-W5axiom
pre-W6axiom
disj-ctrDecPSC-globalPSCCRASHaxiom
pre-W7axiom
disj-globalPSCCRASH-retFLITPSCWRITEaxiom
pre-crashedaxiom
pre-idleaxiom
disj-callPSCRUN-globalPSCCRASHaxiom
pre-readyaxiom
disj-globalPSCCRASH-invFLITPSCWRITEaxiom
disj-globalPSCCRASH-invFLITPSCREADaxiom
disj-callPSCCOMPLETE-globalPSCCRASHaxiom