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: |
|---|
| delta-write-same | proved | all subs proved
| ecs-write,
ecs-write-same,
delta-01,
|
| delta-atomic-leb-change | proved | all subs proved
| ecs-write-same,
delta-01,
|
| ecs-write-same | proved | all subs proved
| in-ecs,
ecs-write,
|
| delta-write | proved | all subs proved
| in-ecs,
sum-of-differences-rem,
ecs-empty,
bag-rem-eq-empty-elim,
sum-of-differences-base,
sum-of-differences-rec,
ecs-write,
delta-01,
|
| ecs-write | proved | all subs proved
| ecs-n-write,
ecs,
|
| in-delta | proved | all subs proved
| in-ecs,
sum-of-differences-in,
delta-01,
|
| ecs-n-write | proved | all subs proved
| in-ecs-n,
ecs-n-rec,
ecs-n-base,
|
| ecs-empty | proved | all subs proved
| ecs-n-empty,
ecs,
|
| sum-of-differences-rem | proved | all subs proved
| sum-of-differences-in,
sum-of-differences-rec,
sum-of-differences-base,
|
| in-ecs | proved | all subs proved
| in-ecs-n,
ecs,
|
| sum-of-differences-in | proved | all subs proved
| sum-of-differences-rec,
|
| in-ecs-n | proved | all subs proved
| ecs-n-rec,
ecs-n-base,
|
| ecs-n-empty | proved | all subs proved
| ecs-n-rec,
ecs-n-base,
|
| ecs-n-base | axiom | | |
| ecs-n-rec | axiom | | |
| ecs | axiom | | |
| sum-of-differences-rec | axiom | | |
| sum-of-differences-base | axiom | | |
| bag-rem-eq-empty-elim | proved | all subs proved
| |
| delta-01 | axiom | | |