[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 FLIT-proofs

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:
FLITInv-thmaxiominit-state-inv, step-ready-W1, step-ready-R1, step-ready-ready, step-W1-W2, step-W2-W3, step-W3-W4, step-W4-W5, step-W5-W6, step-W6-W7, step-W7-ready, step-R1-R2, step-R2-R3, step-R2-R4, step-R3-R4, step-R4-ready, step-idle-ready, step-PROP_W, step-PROP_FO, step-PROP_SF, step-PERSIST_W, step-PERSIST_FO, step-CRASH, rely-reflexive, rely-W1-W2, rely-W2-W3, rely-W3-W4, rely-W4-W5, rely-W5-W6, rely-W6-W7, rely-R1-R2, rely-R2-R3, rely-R2-R4, rely-R3-R4, rely-PROP_W, rely-PROP_FO, rely-PROP_SF, rely-PERSIST_W, rely-PERSIST_FO, stable-R1, stable-R2, stable-W1, stable-W2, stable-W3, stable-W4, stable-W5, stable-W6, stable-W7, stable-crashed, stable-ready, definedness-W6, definedness-R2, definedness-PROP_W, definedness-PROP_SF, definedness-PERSIST_W, definedness-PERSIST_FO,
other-FLITLInvaxiominit-state-inv, step-ready-W1, step-ready-R1, step-ready-ready, step-W1-W2, step-W2-W3, step-W3-W4, step-W4-W5, step-W5-W6, step-W6-W7, step-W7-ready, step-R1-R2, step-R2-R3, step-R2-R4, step-R3-R4, step-R4-ready, step-idle-ready, step-PROP_W, step-PROP_FO, step-PROP_SF, step-PERSIST_W, step-PERSIST_FO, step-CRASH, rely-reflexive, rely-W1-W2, rely-W2-W3, rely-W3-W4, rely-W4-W5, rely-W5-W6, rely-W6-W7, rely-R1-R2, rely-R2-R3, rely-R2-R4, rely-R3-R4, rely-PROP_W, rely-PROP_FO, rely-PROP_SF, rely-PERSIST_W, rely-PERSIST_FO, stable-R1, stable-R2, stable-W1, stable-W2, stable-W3, stable-W4, stable-W5, stable-W6, stable-W7, stable-crashed, stable-ready, definedness-W6, definedness-R2, definedness-PROP_W, definedness-PROP_SF, definedness-PERSIST_W, definedness-PERSIST_FO,
stable-FLITLInvaxiominit-state-inv, step-ready-W1, step-ready-R1, step-ready-ready, step-W1-W2, step-W2-W3, step-W3-W4, step-W4-W5, step-W5-W6, step-W6-W7, step-W7-ready, step-R1-R2, step-R2-R3, step-R2-R4, step-R3-R4, step-R4-ready, step-idle-ready, step-PROP_W, step-PROP_FO, step-PROP_SF, step-PERSIST_W, step-PERSIST_FO, step-CRASH, rely-reflexive, rely-W1-W2, rely-W2-W3, rely-W3-W4, rely-W4-W5, rely-W5-W6, rely-W6-W7, rely-R1-R2, rely-R2-R3, rely-R2-R4, rely-R3-R4, rely-PROP_W, rely-PROP_FO, rely-PROP_SF, rely-PERSIST_W, rely-PERSIST_FO, stable-R1, stable-R2, stable-W1, stable-W2, stable-W3, stable-W4, stable-W5, stable-W6, stable-W7, stable-crashed, stable-ready, definedness-W6, definedness-R2, definedness-PROP_W, definedness-PROP_SF, definedness-PERSIST_W, definedness-PERSIST_FO,
rely-FLITLInvaxiominit-state-inv, step-ready-W1, step-ready-R1, step-ready-ready, step-W1-W2, step-W2-W3, step-W3-W4, step-W4-W5, step-W5-W6, step-W6-W7, step-W7-ready, step-R1-R2, step-R2-R3, step-R2-R4, step-R3-R4, step-R4-ready, step-idle-ready, step-PROP_W, step-PROP_FO, step-PROP_SF, step-PERSIST_W, step-PERSIST_FO, step-CRASH, rely-reflexive, rely-W1-W2, rely-W2-W3, rely-W3-W4, rely-W4-W5, rely-W5-W6, rely-W6-W7, rely-R1-R2, rely-R2-R3, rely-R2-R4, rely-R3-R4, rely-PROP_W, rely-PROP_FO, rely-PROP_SF, rely-PERSIST_W, rely-PERSIST_FO, stable-R1, stable-R2, stable-W1, stable-W2, stable-W3, stable-W4, stable-W5, stable-W6, stable-W7, stable-crashed, stable-ready, definedness-W6, definedness-R2, definedness-PROP_W, definedness-PROP_SF, definedness-PERSIST_W, definedness-PERSIST_FO,
step-FLITLInvaxiominit-state-inv, step-ready-W1, step-ready-R1, step-ready-ready, step-W1-W2, step-W2-W3, step-W3-W4, step-W4-W5, step-W5-W6, step-W6-W7, step-W7-ready, step-R1-R2, step-R2-R3, step-R2-R4, step-R3-R4, step-R4-ready, step-idle-ready, step-PROP_W, step-PROP_FO, step-PROP_SF, step-PERSIST_W, step-PERSIST_FO, step-CRASH, rely-reflexive, rely-W1-W2, rely-W2-W3, rely-W3-W4, rely-W4-W5, rely-W5-W6, rely-W6-W7, rely-R1-R2, rely-R2-R3, rely-R2-R4, rely-R3-R4, rely-PROP_W, rely-PROP_FO, rely-PROP_SF, rely-PERSIST_W, rely-PERSIST_FO, stable-R1, stable-R2, stable-W1, stable-W2, stable-W3, stable-W4, stable-W5, stable-W6, stable-W7, stable-crashed, stable-ready, definedness-W6, definedness-R2, definedness-PROP_W, definedness-PROP_SF, definedness-PERSIST_W, definedness-PERSIST_FO,
definedness-PERSIST_FOprovedall subs proved
definedness-PERSIST_Wprovedall subs proved
definedness-PROP_SFprovedall subs proved
definedness-PROP_Wprovedall subs proved
definedness-R2provedall subs proved
definedness-W6provedall subs proved
stable-readyprovedall subs proved
stable-crashedprovedall subs proved
stable-W7provedall subs proved
stable-W6provedall subs proved
stable-W5provedall subs proved
stable-W4provedall subs proved
stable-W3provedall subs proved
stable-W2provedall subs proved
stable-W1provedall subs proved
stable-R2provedall subs proved
stable-R1provedall subs proved
rely-PERSIST_FOprovedall subs proved
rely-PERSIST_Wprovedall subs proved
rely-PROP_SFprovedall subs proved
rely-PROP_FOprovedall subs proved
rely-PROP_Wprovedall subs proved
rely-R3-R4provedall subs proved
rely-R2-R4provedall subs proved
rely-R2-R3provedall subs proved
rely-R1-R2provedall subs proved
rely-W6-W7provedall subs proved
rely-W5-W6provedall subs proved
rely-W4-W5provedall subs proved
rely-W3-W4provedall subs proved
rely-W2-W3provedall subs proved
rely-W1-W2provedall subs proved
rely-reflexiveprovedall subs proved
step-CRASHprovedall subs proved
step-PERSIST_FOprovedall subs proved
step-PERSIST_Wprovedall subs proved
step-PROP_SFprovedall subs proved
step-PROP_FOprovedall subs proved
step-PROP_Wprovedall subs proved
step-idle-readyprovedall subs proved
step-R4-readyprovedall subs proved
step-R3-R4provedall subs proved
step-R2-R4provedall subs proved
step-R2-R3provedall subs proved
step-R1-R2provedall subs proved
step-W7-readyprovedall subs proved
step-W6-W7provedall subs proved
step-W5-W6provedall subs proved
step-W4-W5provedall subs proved
step-W3-W4provedall subs proved
step-W2-W3provedall subs proved
step-W1-W2provedall subs proved
step-ready-readyprovedall subs proved
step-ready-R1provedall subs proved
step-ready-W1provedall subs proved
init-state-invprovedall subs proved