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: |
|---|
| oplus-addFO | proved | all subs proved
| oplus-same-writes-eq,
oplus-addFO-aux,
overwrite-def,
|
| oplus-addFO-aux | proved | all subs proved
| oplus-same-writes-eq,
oplus-v-append,
overwrite-base,
oplus-v-one-FO,
|
| onemember-nowriter-contra | proved | all subs proved
| notMember-onewriter-contra,
|
| oplus-addW-aux | proved | all subs proved
| oplus-v-append,
oplus-v-one-W,
|
| oplus-addW | proved | all subs proved
| oplus-same-writes-eq,
oplus-v-one-W,
oplus-v-append,
overwrite-def,
|
| notMember-onewriter-contra | proved | all subs proved
| notMember-not-in,
oneWriter,
|
| oplus-v-append | proved | all subs proved
| overwrite-rec2,
overwrite-rec1,
oplus-same-writes-eq,
overwrite-base,
|
| oplus-recW | proved | all subs proved
| oplus-same-writes-eq,
overwrite-rec2,
overwrite-def,
|
| filter-t-split | proved | all subs proved
| filtertid-def,
filter-t-one,
filter-t-append,
|
| at-filter-FO-not-W | proved | all subs proved
| filter-FO-one-W,
filter-FO-one-FO,
filter-FO-append,
filter-FO-empty,
|
| filter-FO-empty | proved | all subs proved
| filterfos-def,
|
| filter-FO-append | proved | all subs proved
| filterfos-def,
|
| filter-FO-one-FO | proved | all subs proved
| filterfos-def,
|
| filter-FO-one-W | proved | all subs proved
| filterfos-def,
|
| oplus-v-one-W | proved | all subs proved
| overwrite-base,
overwrite-rec2,
|
| filter-t-append | proved | all subs proved
| filtertid-def,
|
| filter-t-one | proved | all subs proved
| filtertid-def,
|
| notMember-not-in | proved | all subs proved
| noWriter,
|
| oplus-v-one-FO | proved | all subs proved
| overwrite-base,
overwrite-rec1,
|
| oplus-same-writes-eq | proved | all subs proved
| overwrite-rec2,
overwrite-rec1,
overwrite-base,
filterwrites-def,
|
| relyp-persist | proved | all subs proved
| filtertid-def,
relyp-def,
allrelyp-def,
|
| filter-tid-empty | proved | all subs proved
| filtertid-def,
|
| in-filter-W | proved | all subs proved
| filterwrites-def,
|
| ctrok-size-writers-eq-ctr | proved | all subs proved
| ctrok-def,
|
| relyp-no-pending-w-stable | proved | all subs proved
| relyp-def,
allrelyp-def,
filtertid-def,
filterwrites-def,
noPendingW,
|
| relyp-refl | proved | all subs proved
| filtertid-def,
relyp-def,
allrelyp-def,
|
| one-pending-no-fo-no-pending | proved | all subs proved
| FOFollowsW-def,
filtertid-def,
filterwrites-def,
noPendingW,
onePendingW,
|
| relyp-no-event-added-by-other | proved | all subs proved
| filtertid-def,
relyp-def,
allrelyp-def,
|
| filter-FO-idx | proved | all subs proved
| filterfos-def,
|
| filter-w-fo | proved | all subs proved
| filterwrites-def,
|
| pending-ok-persist | proved | all subs proved
| filtertid-def,
filterwrites-def,
pendingOk,
|
| filter-w-empty | proved | all subs proved
| filterwrites-def,
|
| get-filter-t-rev | proved | all subs proved
| filtertid-def,
|
| get-filter-t | proved | all subs proved
| filtertid-def,
|
| relyws-refl | proved | all subs proved
| relyws-def,
allrelyws-def,
|
| in-filter-t | proved | all subs proved
| filtertid-def,
|
| relyws-rm-other-writer | proved | all subs proved
| relyws-def,
allrelyws-def,
|
| filter-W-one-fo | proved | all subs proved
| filterwrites-def,
|
| fo-follows-last | proved | all subs proved
| FOFollowsW-def,
|
| relyp-fo-follows-w-stable | proved | all subs proved
| FOFollowsW-def,
filtertid-def,
relyp-def,
allrelyp-def,
|
| relyws-noWriter-stable | proved | all subs proved
| relyws-def,
allrelyws-def,
noWriter,
|
| filter-W-one-w | proved | all subs proved
| filterwrites-def,
|
| add-pending-fo-ok | proved | all subs proved
| filterwrites-def,
filtertid-def,
pendingOk,
|
| relyws-oneWriter-stable | proved | all subs proved
| relyws-def,
allrelyws-def,
oneWriter,
|
| filter-W-append | proved | all subs proved
| filterwrites-def,
|
| add-pending-w-ok | proved | all subs proved
| filterwrites-def,
filtertid-def,
pendingOk,
noPending,
|
| onemember-to-nomember | proved | all subs proved
| noWriter,
oneWriter,
|
| add-pending-w-one-pending | proved | all subs proved
| filtertid-def,
filterwrites-def,
onePendingW,
noPending,
|
| writersok-rm-writer | proved | all subs proved
| filterwrites-def,
filtertid-def,
writersOk,
noPending,
oneWriter,
|
| filter-W-t-swap | proved | all subs proved
| filterwrites-def,
filtertid-def,
|
| relyp-add-other-fo | proved | all subs proved
| filtertid-def,
relyp-def,
allrelyp-def,
|
| writersok-add-writer | proved | all subs proved
| filtertid-def,
filterwrites-def,
writersOk,
noWriter,
|
| writersok-del-pos | proved | all subs proved
| filtertid-def,
filterwrites-def,
writersOk,
|
| writersok-persist | proved | all subs proved
| filtertid-def,
filterwrites-def,
writersOk,
|
| writersok-add-fo | proved | all subs proved
| filtertid-def,
filterwrites-def,
writersOk,
|
| no-pending-w-no-pending | proved | all subs proved
| filterwrites-def,
filtertid-def,
noPendingW,
noPending,
|
| in-filter-FO | proved | all subs proved
| filterfos-def,
|
| onewriter-ctrok-nonzero | proved | all subs proved
| ctrok-def,
oneWriter,
|
| ctrok-rm-writer | proved | all subs proved
| ctrok-def,
oneWriter,
|
| one-pending-add-stable | proved | all subs proved
| filtertid-def,
filterwrites-def,
onePendingW,
|
| no-pending-w-add-fo-stable | proved | all subs proved
| filterwrites-def,
noPendingW,
|
| ctrok-add-writer | proved | all subs proved
| ctrok-def,
noWriter,
|
| filter-w-write | proved | all subs proved
| filterwrites-def,
|
| relyp-no-pending-stable | proved | all subs proved
| relyp-def,
allrelyp-def,
filtertid-def,
noPending,
|
| onemember-eq | proved | all subs proved
| oneWriter,
|
| writersok-add-pending | proved | all subs proved
| filterwrites-def,
filtertid-def,
writersOk,
noPending,
oneWriter,
|
| relyp-add-other-w | proved | all subs proved
| filtertid-def,
relyp-def,
allrelyp-def,
|
| nomember-to-onemember | proved | all subs proved
| oneWriter,
noWriter,
|
| pendingsok-del-pos | proved | all subs proved
| filtertid-def,
filterwrites-def,
pendingOk,
|
| relyws-add-other-writer | proved | all subs proved
| relyws-def,
allrelyws-def,
|
| relyp-one-pending-stable | proved | all subs proved
| relyp-def,
allrelyp-def,
filtertid-def,
filterwrites-def,
onePendingW,
pendingOk,
|
| writersOk | axiom | | |
| noPending | axiom | | |
| overwrite-def | axiom | | |
| noWriter | axiom | | |
| allrelyws-def | axiom | | |
| relyws-def | axiom | | |
| pendingOk | axiom | | |
| oneWriter | axiom | | |
| onePendingW | axiom | | |
| FOFollowsW-def | axiom | | |
| filterfos-def | axiom | | |
| noPendingW | axiom | | |
| ctrok-def | axiom | | |
| filterwrites-def | axiom | | |
| allrelyp-def | axiom | | |
| relyp-def | axiom | | |
| filtertid-def | axiom | | |
| overwrite-base | axiom | | |
| overwrite-rec1 | axiom | | |
| overwrite-rec2 | axiom | | |