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

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:
rely-FOFollowsW-stableprovedall subs proved FOWs-W, FOWs-W-split, FOWs-FO-split, FO-in-FOWs, FOWs-FO, FOWs-append, B-postfix-weak-FOWs-postfix, FOFollowsW-def, rely-local-def, rely-def, B-restrict-SF-l, B-postfix-weak,
B-postfix-weak-FOWs-postfixprovedall subs proved FOWs-one-SF, restrict-SF-eq-FOWs-eq, FOWs-one-FO, FOWs-one-W, FOWs-append, FOWs-base, B-restrict-SF-l, B-postfix-weak,
rely-noPendingW-stableprovedall subs proved W-in-FOWs, BrestrictL-def, FOWs-loc-empty, noPendingW, rely-local-def, rely-def,
rely-prop-FOprovedall subs proved isPropFO-FOWs-delpos-other, isPropFO-cons-leading-FO, isPropFO-FOWs-delpos-tail, rely-local-def, rely-def,
B-postfix-weak-delpos-propFOprovedall subs proved isPropFO-def, isPropFO-restrict-SF-l-head, B-restrict-SF-l, B-postfix-weak,
writersOk-prop-FOprovedall subs proved isPropFO-restrict-delpos, writersOk,
pendingOk-prop-FOprovedall subs proved isPropFO-restrict-delpos, pendingOk,
FO-in-FOWsprovedall subs proved FOWs-one-FO, FOWs-one-W, FOWs-one-SF, FOWs-append, FOWs-base,
FOWs-FO-splitprovedall subs proved FOWs-one-FO, FOWs-W, FOWs-one-W, FOWs-SF, FOWs-one-SF, FOWs-base, FOWs-FO, FOWs-append,
FOWs-W-splitprovedall subs proved FOWs-FO, FOWs-one-FO, FOWs-one-W, FOWs-SF, FOWs-one-SF, FOWs-base, FOWs-W, FOWs-append,
isPropFO-restrict-delposprovedall subs proved isPropFO-not-leading-FO, isPropFO-not-leading-W, isPropFO-leading-SF, isPropFO-rec, restrict-l-FO, isPropFO-def, restrict-l-append, restrict-l-empty,
isPropFO-restrict-SF-l-headprovedall subs proved isPropFO-rec, isPropFO-def, isPropFO-leading-SF, isPropFO-empty, B-restrict-SF-l,
restrict-SF-eq-FOWs-eqprovedall subs proved FOWs-one-FO, FOWs-one-W, FOWs-append, FOWs-base, B-restrict-SF-l,
isPropFO-FOWs-delpos-tailprovedall subs proved isPropFO-not-leading-FO, isPropFO-rec, isPropFO-not-leading-W, FOWs-one-W, isPropFO-leading-SF, FOWs-one-SF, FOWs-one-FO, isPropFO-def, FOWs-append, isPropFO-empty, FOWs-base,
isPropFO-cons-leading-FOprovedall subs proved FOWs-one-FO, isPropFO-rec, isPropFO-def, isPropFO-not-leading-W, FOWs-one-W, isPropFO-leading-SF, FOWs-one-SF, FOWs-append, isPropFO-empty, FOWs-base,
isPropFO-FOWs-delpos-otherprovedall subs proved isPropFO-not-leading-FO, isPropFO-not-leading-W, isPropFO-leading-SF, isPropFO-rec, FOWs-one-FO, isPropFO-def, FOWs-one-W, FOWs-one-SF, FOWs-append, FOWs-base,
FOWs-loc-emptyprovedall subs proved FOWs-one-FO, restrict-l-FO, restrict-l-W-other, restrict-l-W-same, FOWs-one-W, FOWs-one-SF, restrict-l-SF, FOWs-append, restrict-l-append, FOWs-base, restrict-l-empty,
W-in-FOWsprovedall subs proved FOWs-one-FO, FOWs-one-W, FOWs-one-SF, FOWs-append, FOWs-base,
writersOk-prop-Wprovedall subs proved restrict-l-W-same, restrict-l-append, writersOk,
pendingOk-empty-bqprovedall subs proved restrict-l-empty, pendingOk,
pendingOk-add-pendingprovedall subs proved restrict-l-W-same, restrict-l-W-other, restrict-l-empty, restrict-l-append, pendingOk, noPending,
pendingOk-prop-Wprovedall subs proved restrict-l-W-other, restrict-l-W-same, restrict-l-append, pendingOk,
noPendingW-add-FOprovedall subs proved restrict-l-FO, restrict-l-append, noPendingW,
writersOk-empty-bqprovedall subs proved restrict-l-empty, writersOk,
B-postfix-weak-same-loc-postfixprovedall subs proved B-postfix-weak-same-loc, B-restrict-SF-l, B-postfix-weak,
noPendingW-add-SFprovedall subs proved restrict-l-SF, restrict-l-append, noPendingW,
rely-prop-SFprovedall subs proved FOWs-one-SF, FOWs-base, rely-local-def, rely-def,
writersok-rm-writerprovedall subs proved restrict-l-empty, writersOk, noPending,
writersOk-add-FOprovedall subs proved restrict-l-FO, restrict-l-append, writersOk,
SFTrainling-prop-FOprovedall subs proved isPropFO-def, isPropFO-SF-in-delpos, SFTrailing,
B-postfix-weak-of-emptyprovedall subs proved B-postfix-weak-empty, B-restrict-SF-l, B-postfix-weak,
pendingOk-add-FOprovedall subs proved restrict-l-FO, restrict-l-append, pendingOk,
noPendingW-no-leading-bq-Wprovedall subs proved restrict-l-W-same, restrict-l-append, noPendingW,
writersOk-add-SFprovedall subs proved restrict-l-SF, restrict-l-append, writersOk,
pendingOk-no-two-buffered-Wsprovedall subs proved restrict-l-W-same, restrict-l-append, pendingOk,
writersok-add-pendingprovedall subs proved restrict-l-empty, restrict-l-W-other, restrict-l-append, writersOk, noPending,
pendingOk-add-SFprovedall subs proved restrict-l-SF, restrict-l-append, pendingOk,
B-postfix-weak-one-wsprovedall subs proved B-postfix-weak-one, B-postfix-weak-empty,
B-postfix-weak-oneprovedall subs proved B-restrict-SF-l, B-postfix-weak,
B-postfix-weak-emptyprovedall subs proved B-restrict-SF-l, B-postfix-weak,
isPropFO-SF-in-delposprovedall subs proved isPropFO-def,
restrict-l-SFprovedall subs proved BrestrictL-def,
B-postfix-weak-same-locprovedall subs proved B-restrict-SF-l, B-postfix-weak,
isPropFO-emptyprovedall subs proved isPropFO-def,
restrict-l-FOprovedall subs proved BrestrictL-def,
restrict-l-W-otherprovedall subs proved BrestrictL-def,
restrict-l-emptyprovedall subs proved BrestrictL-def,
restrict-l-appendprovedall subs proved BrestrictL-def,
restrict-l-W-sameprovedall subs proved BrestrictL-def,
isPropFO-recprovedall subs proved isPropFO-def,
isPropFO-leading-SFprovedall subs proved isPropFO-def,
isPropFO-not-leading-Wprovedall subs proved isPropFO-def,
isPropFO-not-leading-FOprovedall subs proved isPropFO-def,
FOWs-appendprovedall subs proved FOWs-FO, FOWs-W, FOWs-SF, FOWs-base,
FOWs-one-SFprovedall subs proved FOWs-base, FOWs-SF,
FOWs-one-Wprovedall subs proved FOWs-base, FOWs-W,
FOWs-one-FOprovedall subs proved FOWs-base, FOWs-FO,
readFOsOk-not-one-Wprovedall subs proved FOs, readFOsOk,
oplus-v-appendprovedall subs proved overwrite-rec-FO, overwrite-rec-W, overwrite-rec-SF, overwrite-base,
oplus-v-one-Wprovedall subs proved overwrite-base, overwrite-rec-W,
FOs-not-one-SFprovedall subs proved FOs,
SFTrailing-attachprovedall subs proved SFTrailing,
SFTrailing-tailprovedall subs proved SFTrailing,
rely-reflprovedall subs proved rely-local-def, rely-def,
rely-update-other-bqprovedall subs proved rely-local-def, rely-def,
oplus-v-one-FOprovedall subs proved overwrite-base, overwrite-rec-FO,
readFOsOk-empty-rfo-while-writingprovedall subs proved FOs, readFOsOk,
B-postfix-weak-not-in-stableprovedall subs proved B-restrict-SF-l, B-postfix-weak,
isPropFO-W-in-delposprovedall subs proved isPropFO-def,
rely-noPending-stableprovedall subs proved FOWs-base, noPending, rely-local-def, rely-def,
readFOsOk-not-one-SFprovedall subs proved FOs, readFOsOk,
noPending-then-noPendingWprovedall subs proved BrestrictL-def, noPendingW, noPending,
readFOsOk-add-writerprovedall subs proved FOs, readFOsOk,
oplus-v-one-SFprovedall subs proved overwrite-base, overwrite-rec-SF,
readFOsOk-not-leading-Wprovedall subs proved FOs, readFOsOk,
writersok-add-writerprovedall subs proved writersOk,
readFOsOk-rm-writerprovedall subs proved FOs, readFOsOk,
readFOsOk-prop-FOprovedall subs proved FOs, readFOsOk,
rely-prop-Wprovedall subs proved FOWs-W, rely-local-def, rely-def,
B-postfix-weak-appendprovedall subs proved B-restrict-SF-l, B-postfix-weak,
writersOk-persistprovedall subs proved writersOk,
FOs-not-one-Wprovedall subs proved FOs,
rely-noPending-stable-strongprovedall subs proved FOWs-FO, FOWs-W, FOWs-SF, FOWs-base, noPending, rely-local-def, rely-def, B-restrict-SF-l, B-postfix-weak,
FOs-not-leading-Wprovedall subs proved FOs,
oplus-noPendingWprovedall subs proved overwrite-base, overwrite-def, noPendingW,
noPending-no-leading-bq-Wprovedall subs proved noPending,
isPropFO-delpos-last-SFprovedall subs proved isPropFO-def,
pendingOk-persistprovedall subs proved pendingOk,
SFTrailing-leading-SFprovedall subs proved SFTrailing,
readFOsOk-add-FOprovedall subs proved FOs, readFOsOk,
isPropFO-other-FO-in-delposprovedall subs proved isPropFO-def,
B-postfix-weak-reflprovedall subs proved B-restrict-SF-l, B-postfix-weak,
isPropFO-drop-last-SFprovedall subs proved isPropFO-def,
rely-persistprovedall subs proved rely-local-def, rely-def,
FOFollowsW-defaxiom
overwrite-defaxiom
B-postfix-weakaxiom
B-restrict-SF-laxiom
SFTrailingaxiom
noPendingaxiom
pendingOkaxiom
writersOkaxiom
overwrite-baseaxiom
overwrite-rec-SFaxiom
overwrite-rec-Waxiom
overwrite-rec-FOaxiom
rely-defaxiom
rely-local-defaxiom
noPendingWaxiom
BrestrictL-defaxiom
isPropFO-defaxiom
readFOsOkaxiom
FOsaxiom
FOWs-FOaxiom
FOWs-SFaxiom
FOWs-Waxiom
FOWs-baseaxiom