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: |
|---|
| reorder-same-thread-events-lifted | proved | all subs proved
| reorder-same-thread-events,
reorder-def,
|
| reorder-step-read-propFO-lifted | proved | all subs proved
| reorder-del-other-propFO,
reorder-step-read-propFO,
reorder-def,
|
| reorder-step-read-propFO | proved | all subs proved
| buffered-1l-expand,
reorder-rec-W,
reorder-rec-FO,
isPropFO-delpos-eq-delfirst,
reorder-base,
|
| reorder-del-other-propFO | proved | all subs proved
| reorder-del-other-FO,
isPropFO-delpos-eq-delfirst,
|
| reorder-same-thread-events | proved | all subs proved
| reorder-rec-W,
buffered-1l-expand,
reorder-rec-FO,
reorder-base,
|
| reorder-step-readPWB-lifted | proved | all subs proved
| reorder-step-readPWB-other,
reorder-step-readPWB,
reorder-def,
|
| reorder-fo-in-p-lifted | proved | all subs proved
| reorder-fo-in-p,
reorder-def,
|
| reorder-del-other-FO | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
propFOs-FO-other,
propFOs-one-fo-other,
propFOs-one-fo-same,
propFOs-W,
propFOs-one-w,
propFOs-SF,
propFOs-one-sf,
propFOs-append,
propFOs-base,
reorder-base,
|
| reorder-fo-in-p | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
propFOs-one-fo-same,
propFOs-append,
reorder-base,
|
| buffered-1l-expand | proved | all subs proved
| propFOs-one-fo-other,
propFOs-one-w,
propFOs-one-sf,
propFOs-append,
propFOs-one-fo-same,
propFOs-base,
|
| reorder-step-readPWB | proved | all subs proved
| reorder-rec-W,
propFOs-one-fo-same,
propFOs-append,
reorder-rec-FO,
reorder-base,
|
| fo-in-propFOs | proved | all subs proved
| propFOs-one-fo-other,
propFOs-one-fo-same,
propFOs-one-w,
propFOs-one-sf,
propFOs-append,
propFOs-base,
|
| w-in-propFOs | proved | all subs proved
| propFOs-one-fo-other,
propFOs-one-fo-same,
propFOs-one-w,
propFOs-one-sf,
propFOs-append,
propFOs-base,
|
| propFOs-one-fo-same | proved | all subs proved
| propFOs-append,
propFOs-FO-same,
|
| reorder-step-readPWB-other | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
propFOs-one-fo-other,
propFOs-append,
reorder-base,
|
| reorder-overwrite-p-eq-lifted | proved | all subs proved
| reorder-overwrite-p-eq,
reorder-def,
|
| reorder-step-persistW-lifted | proved | all subs proved
| reorder-step-persistW,
reorder-def,
|
| reorder-firstPersistW-eq-lifted | proved | all subs proved
| reorder-firstPersistW-eq,
reorder-def,
|
| reorder-step-propW-lifted | proved | all subs proved
| reorder-step-propW,
reorder-def,
|
| reorder-isPersistFO-exists-lifted | proved | all subs proved
| reorder-isPersistFO-exists,
reorder-def,
|
| reorder-same-writes-lifted | proved | all subs proved
| reorder-same-writes,
reorder-def,
|
| reorder-step-propFO-lifted | proved | all subs proved
| reorder-step-propFO,
reorder-def,
|
| reorder-firstPersistW-valid-lifted | proved | all subs proved
| reorder-firstPersistW-valid,
reorder-def,
|
| reorder-step-persistFO-lifted | proved | all subs proved
| reorder-step-persistFO,
reorder-def,
|
| reorder-step-persistFO | proved | all subs proved
| reorder-rec-FO,
reorder-base,
|
| reorder-firstPersistW-valid | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| reorder-step-propFO | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| reorder-same-writes | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| reorder-isPersistFO-exists | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| reorder-step-propW | proved | all subs proved
| reorder-rec-FO,
reorder-rec-W,
reorder-base,
|
| reorder-firstPersistW-eq | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| reorder-step-persistW | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| propFOs-append | proved | all subs proved
| propFOs-FO-other,
propFOs-FO-same,
propFOs-W,
propFOs-SF,
propFOs-base,
|
| propFOs-one-sf | proved | all subs proved
| propFOs-base,
propFOs-SF,
|
| propFOs-one-w | proved | all subs proved
| propFOs-base,
propFOs-W,
|
| propFOs-one-fo-other | proved | all subs proved
| propFOs-base,
propFOs-FO-other,
|
| reorder-overwrite-p-eq | proved | all subs proved
| reorder-rec-W,
reorder-rec-FO,
reorder-base,
|
| propFOs-W | axiom | | |
| isPropFO-delpos-eq-delfirst | proved | all subs proved
| |
| propFOs-FO-other | axiom | | |
| propFOs-FO-same | axiom | | |
| propFOs-SF | axiom | | |
| propFOs-base | axiom | | |
| reorder-def | axiom | | |
| reorder-base | axiom | | |
| reorder-rec-FO | axiom | | |
| reorder-rec-W | axiom | | |