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: |
|---|
| map-path | proved | all subs proved
| reachable-one,
reachset-succ,
closed-succ,
at-apply-succ,
in-apply-succ,
at-apply,
path-rec,
reachable-eq,
reachset,
inj-eq,
in-apply,
path-emp,
path-first-in,
|
| reachable-eq | proved | all subs proved
| path-emp,
path-last-in,
reachable,
|
| reachable-one | proved | all subs proved
| path-emp,
path-rec,
path-last-in,
reachable,
|
| path-last-in | proved | all subs proved
| path-rec,
path-emp,
path-first-in,
|
| reachset-succ | proved | all subs proved
| path-rec,
path-first-in,
reachable,
reachset,
|
| reachable-closed | proved | all subs proved
| closed-succ,
path-rec,
path-emp,
reachable,
|
| hom-empty | proved | all subs proved
| apply-empty,
hom,
|
| path-first-in | proved | all subs proved
| path-rec,
path-emp,
|
| inj-eq | proved | all subs proved
| inj,
|
| closed-succ | proved | all subs proved
| closeds,
closed,
|
| apply-empty | proved | all subs proved
| in-apply,
|
| ran-put-new | proved | all subs proved
| ran,
|
| ran-in-heap-eq | proved | all subs proved
| dom,
ran,
|
| ran-empty | proved | all subs proved
| ran,
|
| inj-empty | proved | all subs proved
| inj,
|
| dom-write | proved | all subs proved
| dom,
|
| dom-empty | proved | all subs proved
| dom,
|
| dom-alloc | proved | all subs proved
| dom,
|
| closeds-subset | proved | all subs proved
| dom,
closeds,
|
| closeds-empty | proved | all subs proved
| closeds,
|
| closed-succ-rm | proved | all subs proved
| closeds,
|
| closed-succ-in-subheap | proved | all subs proved
| closeds,
|
| closed-succ-in | proved | all subs proved
| closeds,
|
| closed-empty | proved | all subs proved
| closed,
|
| apply-succ-empty | proved | all subs proved
| in-apply-succ,
|
| H-dom-subset | proved | all subs proved
| dom,
|
| reachable | axiom | | |
| ran | axiom | | |
| path-emp | axiom | | |
| reachset | axiom | | |
| path-rec | axiom | | |
| at-apply | axiom | | |
| at-apply-succ | axiom | | |
| inj | axiom | | |
| hom | axiom | | |
| closeds | axiom | | |
| closed | axiom | | |
| in-apply-succ | axiom | | |
| in-apply | axiom | | |
| dom | axiom | | |