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: |
|---|
| removed-stays-reachable | proved | all subs proved
| rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
endnotinH-notreachable,
changenonnxt-reachable,
reach-reachnext,
rem-stays-reachable-aux,
reach-alloc,
|
| rem-stays-reachable-aux1 | proved | all subs proved
| path-split-last,
linearity-path,
path-postfix,
path-butlast,
reachable-def,
path-two,
null-not-start-of-path,
path-first-in-H,
self-reachable,
path-cons,
reachable-nodups-def,
|
| rem-stays-reachable-aux2 | proved | all subs proved
| path-butlast,
path-prefix,
path-cons,
path-two,
path-one,
linearity-path,
reachable-nodups-def,
path-last-nxt,
path-postfix,
path-split-last,
reachable-def,
|
| path-prelast | proved | all subs proved
| path-butlast,
path-last,
|
| rem-stays-reachable-aux | proved | all subs proved
| path-last-not-null,
path-trans,
path-first-in-H,
reachable-def,
path-postfix,
path-prefix,
path-modify-strong,
path-two,
path-modify,
path-cons,
path-one,
reachable-nodups-def,
reach-alloc,
|
| path-butlast | proved | all subs proved
| path-prefix,
path-cons,
path-one,
path-two,
|
| add-preserves-reachable-rev | proved | all subs proved
| fromnext-reachable-rev,
startnotinH-notreachable,
fromnext-reachable,
path-two,
reach-reachnext,
reachnext,
path-cons,
self-reachable,
path-one,
reachable-def,
reach-alloc,
|
| reachable-split-first | proved | all subs proved
| path-first-in-H,
path-cons,
reachable-def,
id-reachable,
startnotinH-notreachable,
notnull-reachable,
fromnext-reachable-rev,
fromnext-reachable,
|
| reachable-addnew-rev | proved | all subs proved
| null-not-reachable,
reachable-notnullinH,
path-two,
reach-reachnext,
reachable-addnew,
reachable-trans,
path-prefix,
path-postfix,
startnotinH-notreachable,
path-cons,
reachable-def,
path-last,
path-new-irrelevant-strong,
path-split-last,
path-one,
reachable-nodups-def,
endnotinH-notreachable,
reach-alloc,
|
| add-preserves-reachable | proved | all subs proved
| fromnext-reachable,
fromnext-reachable-rev,
reachable-notnullinH,
reach-alloc,
modnotreachable-reachable,
path-cons,
self-reachable,
path-one,
reachable-def,
|
| reachable-n-rec-rev2 | proved | all subs proved
| reachable-1-def,
reachable-n-rec,
reachable-n-rec-rev,
|
| acyclic-rem-not-reachable | proved | all subs proved
| path-split-last,
linearity-path,
path-postfix,
reachable-def,
path-modify,
path-cons,
self-reachable,
path-two,
reach-alloc,
path-one,
reachable-nodups-def,
|
| reachable-trans-simp | proved | all subs proved
| reachable-trans,
|
| rem-reachable-rev | proved | all subs proved
| rem-reachable,
path-cons,
self-reachable,
path-one,
reachable-def,
|
| rem-reachable | proved | all subs proved
| fromnext-reachable,
fromnext-reachable-rev,
path-cons,
self-reachable,
path-one,
reachable-def,
|
| reachable-n-rec-rev | proved | all subs proved
| reachable-n-1,
reachable-n-trans,
reachable-1-def,
reachable-n-rec,
reach-n-split,
|
| modnotreachable-reachable | proved | all subs proved
| fromnext-reachable-rev,
self-reachable,
path-cons,
path-one,
reachable-def,
|
| endnotinH-notreachable | proved | all subs proved
| reach-alloc,
|
| path-new-irrelevant-strong | proved | all subs proved
| path-first-in-H,
path-cons,
path-one,
|
| reachable-trans | proved | all subs proved
| self-reachable,
fromnext-reachable-rev,
path-cons,
path-one,
reachable-def,
|
| reachable-addnew | proved | all subs proved
| path-cons,
self-reachable,
path-one,
reachable-def,
|
| reachable-notnullinH | proved | all subs proved
| reach-alloc,
|
| reachable-nodups-def | proved | all subs proved
| path-postfix,
path-cons,
path-one,
reachable-def,
|
| notnull-reachable | proved | all subs proved
| null-not-start-of-path,
reachable-def,
|
| id-reachable | proved | all subs proved
| null-not-start-of-path,
path-cons,
path-one,
reachable-def,
null-not-reachable,
self-reachable,
|
| path-prefix | proved | all subs proved
| path-cons,
null-not-start-of-path,
path-first-in-H,
path-one,
|
| reachnext | proved | all subs proved
| path-two,
path-cons,
path-one,
null-not-start-of-path,
path-first-in-H,
reachable-def,
|
| frommodified | proved | all subs proved
| path-two,
self-reachable,
path-one,
path-cons,
reachable-def,
|
| reachable-n-rec2 | proved | all subs proved
| reachable-1-def,
reachable-n-1,
reachable-n-rec,
|
| modified-stays-reachable-rev | proved | all subs proved
| modified-stays-reachable,
|
| k-reachable-def | proved | all subs proved
| path-two,
reachable-n-rec,
reachable-1-def,
reachable-n-1,
path-cons,
reachable-n-base,
path-one,
null-not-start-of-path,
path-first-in-H,
reachable-star-def,
reachable-def,
|
| reachable-addnewtonull-rev | proved | all subs proved
| null-not-start-of-path,
path-cons,
path-one,
reachable-def,
|
| changenonnxt-reachable-rev | proved | all subs proved
| changenonnxt-reachable,
|
| reachable-n-rec-strong2 | proved | all subs proved
| reachable-n-rec-strong,
reachable-n-rec,
|
| linearity | proved | all subs proved
| fromnext-reachable,
reach-reachnext,
path-split-last,
path-one,
reachable-def,
|
| reach-n-path-n | proved | all subs proved
| k-path,
path-one,
path-cons,
null-not-start-of-path,
path-first-in-H,
path-two,
reachable-1-def,
reachable-n-base,
reachable-n-rec,
|
| reachable-split-last | proved | all subs proved
| reach-reachnext,
path-split-last,
path-last-nxt,
reachable-def,
|
| modnotreachable-reachable-rev | proved | all subs proved
| fromnext-reachable-rev,
path-cons,
self-reachable,
path-one,
reachable-def,
|
| reach-n-split-le | proved | all subs proved
| reachable-n-base,
reach-n-split,
|
| k-path | proved | all subs proved
| path-cons,
path-one,
path-empty,
|
| reachable-n-rec-strong | proved | all subs proved
| reachable-1-def,
reachable-n-rec,
|
| changenonnxt-reachable | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| path-last-nxt | proved | all subs proved
| path-cons,
path-two,
|
| linearity-path | proved | all subs proved
| path-cons,
path-one,
|
| modified-stays-reachable | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| path-split-last | proved | all subs proved
| path-cons,
path-two,
path-one,
|
| null-not-reachable | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| path-modify | proved | all subs proved
| path-cons,
path-one,
path-empty,
|
| path-modify-strong | proved | all subs proved
| path-cons,
path-two,
path-one,
|
| path-postfix | proved | all subs proved
| path-cons,
|
| path-trans | proved | all subs proved
| path-cons,
path-one,
path-empty,
|
| path-last-not-null | proved | all subs proved
| path-cons,
path-two,
|
| path-last | proved | all subs proved
| path-cons,
path-one,
|
| path-first-in-H | proved | all subs proved
| path-cons,
path-one,
|
| null-not-start-of-path | proved | all subs proved
| path-cons,
path-one,
|
| reach-n-split | proved | all subs proved
| reachable-n-rec,
reachable-1-def,
reachable-n-base,
|
| reachable-n-trans | proved | all subs proved
| reachable-n-rec,
reachable-1-def,
reachable-n-base,
|
| reachable-n-1 | proved | all subs proved
| reachable-n-base,
reachable-n-rec,
|
| reach-alloc | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| self-reachable | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| reach-reachnext | proved | all subs proved
| path-two,
path-cons,
path-one,
reachable-def,
|
| fromnext-reachable | proved | all subs proved
| path-cons,
reachable-def,
|
| startnotinH-notreachable | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| fromnext-reachable-rev | proved | all subs proved
| path-cons,
reachable-def,
|
| reach-n-unique | proved | all subs proved
| reachable-1-def,
reachable-n-rec,
reachable-n-base,
|
| path-delnonmember | proved | all subs proved
| path-cons,
path-one,
path-empty,
|
| reachable-modbehind | proved | all subs proved
| path-cons,
path-one,
reachable-def,
|
| reachable-star-def | axiom | | |
| path-empty | axiom | | |
| reachable-n-base | axiom | | |
| reachable-1-def | axiom | | |
| reachable-n-rec | axiom | | |
| reachable-def | axiom | | |
| path-one | axiom | | |
| path-cons | axiom | | |
| path-two | axiom | | |