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: |
|---|
| copy-term | proved | all subs proved
| copy-new-node,
copy-node-prepost-empty,
copy-01,
|
| copy-no-effects | proved | all subs proved
| copy-new-node,
copy-node-prepost-empty,
copy-01,
|
| copy-all-reachable-are-fresh | proved | all subs proved
| copy-node-prepost,
copy-node-prepost-empty,
copy-new-node,
copy-01,
|
| copy-new-node | proved | all subs proved
| smaller,
subset-smaller,
copy-edges-prepost,
copy-node-prepost,
copy-edges-nonempty-term,
in-propagate,
copy-node,
|
| copy-map | proved | all subs proved
| subset-trans,
copy-some-node,
copy-edges,
copy-some-edges,
strengthen-recursive-edges-property,
strengthen-recursive-node-property,
copy-monotone,
copy-node,
prove-recursion,
|
| copy-edges-nonempty-term | proved | all subs proved
| subset-trans,
copy-node-prepost,
copy-edges-prepost,
copy-visited-node,
copy-prepost-propagate,
copy-prepost-init,
subset-eq,
copy-edges,
|
| copy-monotone | proved | all subs proved
| subset-trans,
copy-some-node,
copy-edges,
copy-some-edges,
subset-eq,
copy-node,
prove-recursion,
|
| strengthen-recursive-node-property | proved | all subs proved
| copy-some-node,
recursive-property,
recursive-node-property,
|
| strengthen-recursive-edges-property | proved | all subs proved
| copy-some-edges,
recursive-edges-property,
recursive-property,
|
| in-propagate | proved | all subs proved
| copy-node-prepost,
|
| smaller | proved | all subs proved
| copy-node-prepost,
|
| prove-recursion | proved | all subs proved
| recursive-edges-property,
recursive-node-property,
recursive-property,
|
| copy-some-edges | proved | all subs proved
| recursive-edges-property,
|
| copy-some-node | proved | all subs proved
| recursive-node-property,
|
| copy-prepost-init | proved | all subs proved
| copy-edges-prepost,
copy-node-prepost,
|
| copy-prepost-propagate | proved | all subs proved
| copy-node-prepost,
copy-edges-prepost,
|
| copy-visited-node | proved | all subs proved
| copy-node,
|
| copy-node-prepost-empty | proved | all subs proved
| copy-node-prepost,
|
| copy-edges-empty-term | proved | all subs proved
| copy-edges,
|
| recursive-property | axiom | | |
| recursive-node-property | axiom | | |
| recursive-edges-property | axiom | | |
| subset-smaller | proved | all subs proved
| |
| copy-node | axiom | | |
| subset-eq | proved | all subs proved
| |
| copy-edges-prepost | axiom | | |
| subset-trans | proved | all subs proved
| |
| copy-edges | axiom | | |
| copy-01 | axiom | | |
| copy-node-prepost | axiom | | |