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: |
|---|
| perm-shift-two | proved | all subs proved
| in-mkbag-del-two,
bag-swap-add,
bag-del-add,
in-mkbag-del,
bag-swap-del,
mkbag-del-add-content-two,
mkbag-del-add-content,
mkbag-update-out-of-bound,
mkbag-update,
perm,
|
| mkbag-del-add-content-two | proved | all subs proved
| mkbag-del-add-content,
bag-del-add,
in-mkbag-del,
bag-swap-del,
|
| in-mkbag-del-two | proved | all subs proved
| count-del-other,
count-mkbag-greater-two,
count-mkbag-greater-one,
count-mkbag-non-zero,
count-del-same,
|
| perm-shift-one | proved | all subs proved
| bag-del-add,
in-mkbag-del,
bag-swap-del,
mkbag-del-add-content,
mkbag-update,
perm,
|
| in-mkbag-del | proved | all subs proved
| count-del-other,
count-mkbag-greater-one,
count-mkbag-non-zero,
count-del-same,
|
| count-mkbag-greater-two | proved | all subs proved
| mkbag-rec,
mkbag-base,
count-mkbag-greater-one,
|
| perm-swap | proved | all subs proved
| mkbag-del-add-content,
mkbag-update,
perm,
|
| mkbag-update | proved | all subs proved
| bag-del-add,
index-in-mkbag,
mkbag-update-out-of-bound,
mkbag-rec,
mkbag-base,
|
| mkbag-del-add-content | proved | all subs proved
| bag-del-add,
index-in-mkbag,
|
| count-mkbag-greater-one | proved | all subs proved
| mkbag-rec,
mkbag-base,
count-mkbag-non-zero,
|
| perm-size | proved | all subs proved
| mkbag-size,
bag-eq-size,
perm,
|
| mkbag-size | proved | all subs proved
| mkbag-rec,
mkbag-base,
|
| mkbag-update-out-of-bound | proved | all subs proved
| mkbag-rec,
mkbag-base,
|
| bag-swap-del | proved | all subs proved
| count-del-other,
count-del-same,
|
| index-in-mkbag | proved | all subs proved
| mkbag-rec,
|
| count-mkbag-non-zero | proved | all subs proved
| mkbag-rec,
mkbag-base,
|
| perm-trans | proved | all subs proved
| perm,
|
| perm-ident | proved | all subs proved
| perm,
|
| bag-eq-size | proved | all subs proved
| |
| bag-swap-add | proved | all subs proved
| |
| perm | axiom | | |
| bag-del-add | proved | all subs proved
| |
| mkbag-base | axiom | | |
| mkbag-rec | axiom | | |
| count-del-same | proved | all subs proved
| |
| count-del-other | proved | all subs proved
| |