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: |
|---|
| subset-exdiff | proved | all subs proved
| union-diff-cancel,
union-diff-distr,
union-com,
union-ass,
union,
count-subset,
|
| union-diff-distr | proved | all subs proved
| count-subset,
union-com,
union-ass,
union,
difference,
count-diff-subset,
|
| union-diff-cancel | proved | all subs proved
| union-com,
union-ass,
union,
difference,
|
| diff-size | proved | all subs proved
| size-rec,
del-rec,
count-subset,
subset-plus,
diff-rec,
size-empty,
diff-empty,
|
| in-union | proved | all subs proved
| union-com,
union-ass,
union,
in,
|
| subset-size | proved | all subs proved
| size-rec,
subset-plus,
size-empty,
count-subset,
|
| subset-smaller | proved | all subs proved
| count-subset,
subset-plus,
|
| union-inj | proved | all subs proved
| union-com,
union-ass,
union,
|
| union-size | proved | all subs proved
| size-rec,
union-rec,
size-empty,
union-com,
union-ass,
union-empty,
|
| union-subset | proved | all subs proved
| union-com,
union-ass,
union,
count-subset,
|
| union-subset-inj | proved | all subs proved
| union-com,
union-ass,
union,
count-subset,
|
| count-diff-subset | proved | all subs proved
| count-subset,
difference,
|
| union-com | proved | all subs proved
| union-ass,
union,
|
| subset-plus | proved | all subs proved
| subset-in,
in,
exin,
subset-plusplus,
|
| del-size | proved | all subs proved
| del-notin,
size-rec,
del-rec,
exin,
in,
|
| diff-add-sw | proved | all subs proved
| difference,
in,
|
| diff-swap | proved | all subs proved
| difference,
|
| difference-notin | proved | all subs proved
| in,
difference,
|
| in-diff-notfirst | proved | all subs proved
| in,
difference,
|
| still-in-diff | proved | all subs proved
| difference,
in,
|
| union-ass | proved | all subs proved
| union,
|
| exin | proved | all subs proved
| count-del,
in,
|
| difference | proved | all subs proved
| count-del,
del-notin,
diff-rec,
diff-empty,
|
| bag-rm-add-eq | proved | all subs proved
| in,
count-del,
|
| in-at | proved | all subs proved
| in,
in-add,
|
| in-one | proved | all subs proved
| in-emp,
in-add,
one,
|
| in-rem-notrem | proved | all subs proved
| count-del,
in,
|
| some | proved | all subs proved
| in,
in-emp,
|
| still-in-rem | proved | all subs proved
| count-del,
in,
|
| subset-antisym | proved | all subs proved
| count-subset,
subset-refl,
subset-trans,
|
| subset-empty-size | proved | all subs proved
| size-empty,
subset-emp,
|
| subset-plusminus | proved | all subs proved
| count-del,
count-subset,
|
| subset-plusplus | proved | all subs proved
| count-subset,
|
| subset-in | proved | all subs proved
| count-subset,
|
| subset-emp | proved | all subs proved
| count-subset,
|
| subset-trans | proved | all subs proved
| count-subset,
|
| subset-refl | proved | all subs proved
| count-subset,
|
| union | proved | all subs proved
| union-rec,
union-empty,
|
| in-emp | proved | all subs proved
| in,
|
| in-add | proved | all subs proved
| in,
|
| del-notin | proved | all subs proved
| del-rec,
del-empty,
|
| count-del | proved | all subs proved
| del-rec,
del-empty,
|
| count-one | proved | all subs proved
| one,
|
| diff-empty1 | proved | all subs proved
| del-empty,
diff-rec,
diff-empty,
|
| subset-elem | proved | all subs proved
| in,
count-subset,
|
| subset-one | proved | all subs proved
| in,
count-subset,
|
| union-empty | axiom | | |
| union-rec | axiom | | |
| size-empty | axiom | | |
| diff-empty | axiom | | |
| diff-rec | axiom | | |
| size-rec | axiom | | |
| one | axiom | | |
| count-subset | axiom | | |
| del-empty | axiom | | |
| del-rec | axiom | | |
| in | axiom | | |