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: |
|---|
| union-size-01 | proved | all subs proved
| unc,
una,
union-sizele-01,
|
| union-sizele-01 | proved | all subs proved
| union-sizele,
unadd-01,
|
| union-sizele | proved | all subs proved
| union-sub,
union-size,
unc,
una,
union-sizeeq,
|
| disjoint-notempty-01 | proved | all subs proved
| disjoint-all,
disjoint-02,
Delete,
|
| disjoint-sym | proved | all subs proved
| disjoint-02,
disjoint-all,
|
| union-size-ls-in | proved | all subs proved
| int-c,
int-a,
Intersect,
intersection-size,
union-size-03,
|
| union-sizeeq | proved | all subs proved
| union-sub,
unc,
una,
Union,
|
| union-size-03 | proved | all subs proved
| uninsert,
Intersect,
intersection-shift,
intersection-size,
intersection-insert,
Union,
unadd,
int-c,
int-a,
int-e,
unc,
una,
une,
|
| disjoint-02 | proved | all subs proved
| disjoint-01,
|
| disjoint-rem | proved | all subs proved
| int-c,
int-a,
disjoint-01,
Delete,
disjoint-all,
Disjoint,
|
| int-inse | proved | all subs proved
| int-c,
int-a,
disjoint-all,
Disjoint,
disjoint-rec,
|
| int-inserte | proved | all subs proved
| int-c,
int-a,
disjoint-all,
disjoint-rec,
Disjoint,
|
| subset-disjoint-union | proved | all subs proved
| Difference,
union-difference,
unc,
una,
unsub,
disjoint-all,
|
| union-rem-unchdg | proved | all subs proved
| del-in,
unc,
una,
undel,
unin,
del-in-03,
undel-03,
|
| union-size-02 | proved | all subs proved
| del-in,
une-01,
Union,
del-size,
unc,
una,
undel-03,
|
| union-size-not-less-02 | proved | all subs proved
| union-size-not-less-01,
|
| union-sub-rem-disjoint | proved | all subs proved
| unc,
una,
disjoint-diff-subset,
unsub-union-01,
|
| unsubdel-01 | proved | all subs proved
| unc,
una,
union-sub,
undel-03,
|
| disjoint-diff-subset | proved | all subs proved
| Difference,
diff-sub,
disjoint-all,
|
| union-sub | proved | all subs proved
| unc,
una,
union-sub-01,
|
| union-size-not-less-01 | proved | all subs proved
| union-size-le,
|
| intersection-size | proved | all subs proved
| Intersect,
intersection-insert,
intersection-shift,
int-c,
int-a,
int-e,
|
| undel-03 | proved | all subs proved
| unc,
una,
undel-01,
|
| union-difference | proved | all subs proved
| unc,
una,
Difference,
Union,
diff-union-01,
|
| disjoint-rec | proved | all subs proved
| disjoint-all,
|
| disjoint-01 | proved | all subs proved
| disjoint-all,
|
| add-inter-rem | proved | all subs proved
| intersection-insert,
Delete,
del-in,
int-c,
int-a,
Intersect,
del-neq,
|
| del-three-01 | proved | all subs proved
| del-size-02,
|
| disjoint-diff | proved | all subs proved
| Difference,
disjoint-all,
|
| disjoint-diff1 | proved | all subs proved
| Difference,
disjoint-all,
|
| disjoint-diff2 | proved | all subs proved
| Difference,
disjoint-all,
|
| disjoint-empty | proved | all subs proved
| disjoint-all,
|
| disjoint-empty2 | proved | all subs proved
| disjoint-all,
|
| disjoint-rec2 | proved | all subs proved
| disjoint-all,
|
| disjointu-empty | proved | all subs proved
| disjoint-all,
unc,
una,
Union,
|
| disjointu-empty2 | proved | all subs proved
| disjoint-all,
unc,
una,
Union,
|
| rem-disjoint | proved | all subs proved
| Difference,
disjoint-all,
int-c,
int-a,
Disjoint,
|
| subseteq-disjoint-empty | proved | all subs proved
| disjoint-all,
|
| union-diff-union-same | proved | all subs proved
| unc,
una,
union-diff,
Union,
Difference,
|
| union-size-not-less | proved | all subs proved
| union-size-le,
|
| union-subset | proved | all subs proved
| union-subset-01,
unc,
una,
|
| union-subset-01 | proved | all subs proved
| unc,
una,
Union,
|
| union-sub-01 | proved | all subs proved
| unc,
una,
uneq,
|
| union-size | proved | all subs proved
| unc,
una,
Union,
|
| union-size-le | proved | all subs proved
| uninsert,
Union,
unadd,
unc,
una,
une,
|
| diff-union-01 | proved | all subs proved
| Difference,
unc,
una,
Union,
|
| union-diff | proved | all subs proved
| Difference,
unc,
una,
Union,
|
| undel-01 | proved | all subs proved
| unc,
una,
Union,
Delete,
del-in-03,
undel,
|
| intersection-shift | proved | all subs proved
| int-c,
int-a,
Intersect,
|
| disjoint-all | proved | all subs proved
| int-c,
int-a,
Intersect,
Disjoint,
|
| del-size-02 | proved | all subs proved
| Delete,
del-in,
del-size,
|
| intersection-insert | proved | all subs proved
| int-c,
int-a,
Intersect,
|
| del-del-one | proved | all subs proved
| del-in-03,
|
| del-size-01 | proved | all subs proved
| del-size,
|
| del-size-le | proved | all subs proved
| del-in,
del-size,
|
| del-three | proved | all subs proved
| del-in,
Delete,
del-size,
|
| diff-add-del-01 | proved | all subs proved
| Difference,
del-in-03,
diff-add-del,
|
| diff-int | proved | all subs proved
| Difference,
int-c,
int-a,
Intersect,
|
| diff-int-01 | proved | all subs proved
| unc,
una,
Union,
Difference,
int-c,
int-a,
Intersect,
|
| diff-sub-size | proved | all subs proved
| del-in,
Difference,
del-size,
diff-add-del,
diff-e,
|
| diff-subset | proved | all subs proved
| unc,
una,
Union,
Difference,
|
| diff-supset-empty | proved | all subs proved
| unc,
una,
Union,
Difference,
|
| diff-union | proved | all subs proved
| Difference,
unc,
una,
Union,
|
| diff-union-02 | proved | all subs proved
| unin,
Difference,
unc,
una,
Union,
|
| diff-union-03 | proved | all subs proved
| Difference,
unc,
una,
Union,
|
| filter-union | proved | all subs proved
| unc,
una,
filter-in,
Union,
|
| int-del-rew | proved | all subs proved
| int-c,
int-a,
Delete,
Intersect,
|
| int-subs01 | proved | all subs proved
| int-c,
int-a,
Intersect,
|
| intdel-empty | proved | all subs proved
| Delete,
int-c,
int-a,
Intersect,
|
| intersect-add-rem | proved | all subs proved
| int-c,
int-a,
Delete,
Intersect,
|
| k-intersect-base | proved | all subs proved
| int-c,
int-a,
int-e,
|
| k-intersect-rec1 | proved | all subs proved
| int-c,
int-a,
Intersect,
Delete,
|
| k-intersect-rec2 | proved | all subs proved
| del-in,
Delete,
int-c,
int-a,
Intersect,
|
| k-union-base | proved | all subs proved
| unc,
una,
une,
|
| k-union-rec1 | proved | all subs proved
| unc,
una,
uninsert,
unadd,
|
| k-union-rec2 | proved | all subs proved
| unc,
una,
unadd,
|
| rem-union-ins | proved | all subs proved
| del-in,
Delete,
Union,
unindel,
unc,
una,
uninsert,
|
| size-del-leq | proved | all subs proved
| del-in,
del-size,
|
| size-union | proved | all subs proved
| Union,
unadd-01,
unc,
una,
une,
int-c,
int-a,
Intersect,
|
| sub-rem-inter-rem | proved | all subs proved
| Difference,
int-c,
int-a,
Intersect,
Delete,
|
| sub-union | proved | all subs proved
| unc,
una,
Union,
|
| sub-union-01 | proved | all subs proved
| unc,
una,
Union,
|
| sub-union-02 | proved | all subs proved
| unc,
una,
Union,
|
| sub-union-03 | proved | all subs proved
| unc,
una,
Union,
|
| sub-union-04 | proved | all subs proved
| unc,
una,
Union,
|
| sub-union-05 | proved | all subs proved
| unc,
una,
Union,
|
| subset-union-left-rem | proved | all subs proved
| unc,
una,
unsub-union-01,
unsub,
|
| union-inter-inter-union | proved | all subs proved
| int-c,
int-a,
unc,
una,
Union,
Intersect,
|
| union-one | proved | all subs proved
| unc,
una,
une,
unadd,
One,
|
| union-rem-add | proved | all subs proved
| unc,
una,
Delete,
Union,
unindel,
|
| union-rewone | proved | all subs proved
| unc,
una,
une,
unadd,
One,
|
| union-size-insert | proved | all subs proved
| unc,
una,
Union,
|
| union-subset-02 | proved | all subs proved
| unc,
una,
Union,
|
| union-subset-03 | proved | all subs proved
| unc,
una,
Union,
|
| union-subset-04 | proved | all subs proved
| unc,
una,
Union,
|
| union-subset-05 | proved | all subs proved
| unc,
una,
Union,
|
| unsubdel | proved | all subs proved
| unc,
una,
unin,
unsubsub,
sub-del-04,
undel-04,
|
| undel-04 | proved | all subs proved
| una,
Delete,
Union,
|
| unsubsub | proved | all subs proved
| una,
Union,
|
| uneq | proved | all subs proved
| una,
Union,
|
| une-01 | proved | all subs proved
| una,
Union,
|
| undel | proved | all subs proved
| una,
Delete,
Union,
|
| unsub-union-01 | proved | all subs proved
| una,
Union,
|
| unsub | proved | all subs proved
| una,
Union,
|
| unadd-01 | proved | all subs proved
| una,
Union,
|
| unadd | proved | all subs proved
| una,
Union,
|
| uninsert | proved | all subs proved
| unin-01,
|
| une | proved | all subs proved
| una,
Union,
|
| int-e | proved | all subs proved
| int-a,
Intersect,
|
| unc | proved | all subs proved
| una,
Union,
|
| del-size | proved | all subs proved
| del-in,
del-addeq-05,
|
| del-in-03 | proved | all subs proved
| del-in,
Delete,
|
| int-c | proved | all subs proved
| int-a,
Intersect,
|
| add-rem-sub | proved | all subs proved
| diff-del-plus-2,
del-in,
Delete,
Difference,
|
| del-addeq-02 | proved | all subs proved
| Delete,
del-addin-01,
|
| del-addin | proved | all subs proved
| del-addin-01,
|
| del-e | proved | all subs proved
| del-addeq-04,
del-neq-01,
del-e-01,
del-addeq-05,
|
| delsw-suc | proved | all subs proved
| delsw,
|
| diff-del | proved | all subs proved
| Delete,
del-in,
diff-del-minus-3,
Difference,
diff-del-minus,
|
| int-eq | proved | all subs proved
| int-a,
Intersect,
|
| int-idem | proved | all subs proved
| int-a,
Intersect,
|
| intexin | proved | all subs proved
| int-a,
Intersect,
|
| k-diff-rec2 | proved | all subs proved
| diff-del-minus-3,
diff-del-minus,
|
| one-min | proved | all subs proved
| del-e-01,
del-addeq-05,
|
| subset-del | proved | all subs proved
| sub-del-04,
del-in,
|
| unall | proved | all subs proved
| una,
Union,
|
| undel-02 | proved | all subs proved
| una,
Union,
Delete,
|
| undel-05 | proved | all subs proved
| del-in,
|
| undel-06 | proved | all subs proved
| una,
Delete,
Union,
|
| unidem | proved | all subs proved
| una,
Union,
|
| unsubins | proved | all subs proved
| una,
Union,
|
| unsubins-01 | proved | all subs proved
| una,
Union,
|
| unin-01 | proved | all subs proved
| Union,
|
| sub-del-04 | proved | all subs proved
| Delete,
|
| unindel | proved | all subs proved
| Delete,
Union,
|
| diff-sub | proved | all subs proved
| Difference,
|
| unin | proved | all subs proved
| Union,
|
| diff-e | proved | all subs proved
| Difference,
|
| una | proved | all subs proved
| Union,
|
| diff-del-minus | proved | all subs proved
| Delete,
Difference,
|
| diff-del-minus-3 | proved | all subs proved
| Delete,
Difference,
|
| diff-add-del | proved | all subs proved
| Difference,
Delete,
|
| delsw | proved | all subs proved
| Delete,
|
| del-addeq-05 | proved | all subs proved
| Delete,
|
| del-e-01 | proved | all subs proved
| Delete,
|
| del-neq-01 | proved | all subs proved
| Delete,
|
| del-addeq-04 | proved | all subs proved
| Delete,
|
| del-addin-01 | proved | all subs proved
| Delete,
|
| diff-del-plus-2 | proved | all subs proved
| Difference,
|
| int-a | proved | all subs proved
| Intersect,
|
| del-in | proved | all subs proved
| Delete,
|
| del-addeq | proved | all subs proved
| Delete,
|
| del-addeq-01 | proved | all subs proved
| Delete,
|
| del-addeq-03 | proved | all subs proved
| Delete,
|
| del-addeq-06 | proved | all subs proved
| Delete,
|
| del-d | proved | all subs proved
| Delete,
|
| del-d-01 | proved | all subs proved
| Delete,
|
| del-e-02 | proved | all subs proved
| Delete,
|
| del-eq | proved | all subs proved
| Delete,
|
| del-feq | proved | all subs proved
| Delete,
|
| del-feq-01 | proved | all subs proved
| Delete,
|
| del-feq-02 | proved | all subs proved
| Delete,
|
| del-in-01 | proved | all subs proved
| Delete,
|
| del-in-02 | proved | all subs proved
| Delete,
|
| del-ne | proved | all subs proved
| Delete,
|
| del-neq-02 | proved | all subs proved
| Delete,
|
| del-notin | proved | all subs proved
| Delete,
|
| del-two | proved | all subs proved
| Delete,
|
| delete-insert | proved | all subs proved
| Delete,
|
| delete-shift | proved | all subs proved
| Delete,
|
| delete-subset | proved | all subs proved
| Delete,
|
| delsw-01 | proved | all subs proved
| Delete,
|
| delsw-02 | proved | all subs proved
| Delete,
|
| diff-del-01 | proved | all subs proved
| Difference,
Delete,
|
| diff-del-02 | proved | all subs proved
| Difference,
Delete,
|
| diff-del-minus-2 | proved | all subs proved
| Delete,
Difference,
|
| diff-del-plus-1 | proved | all subs proved
| Difference,
|
| diff-diff-right | proved | all subs proved
| Difference,
|
| diff-e-01 | proved | all subs proved
| Difference,
|
| diff-empty | proved | all subs proved
| Difference,
|
| diff-idem | proved | all subs proved
| Difference,
|
| diff-nin | proved | all subs proved
| Difference,
|
| diff-one | proved | all subs proved
| Difference,
|
| diff-rc | proved | all subs proved
| Difference,
|
| diff-subset-01 | proved | all subs proved
| Delete,
Difference,
|
| equal-add-in | proved | all subs proved
| Delete,
|
| filter-add | proved | all subs proved
| filter-in,
|
| filter-empty | proved | all subs proved
| filter-in,
|
| insdel-sub | proved | all subs proved
| Delete,
|
| k-delete-rec | proved | all subs proved
| Delete,
|
| k-diff-rec1 | proved | all subs proved
| Delete,
Difference,
|
| one-in | proved | all subs proved
| One,
|
| selsub-diff | proved | all subs proved
| Difference,
|
| size-eq-ext | proved | all subs proved
| size-eq,
|
| sub-ade | proved | all subs proved
| Delete,
|
| sub-ade-01 | proved | all subs proved
| Delete,
|
| sub-ade-02 | proved | all subs proved
| Delete,
|
| sub-ade-03 | proved | all subs proved
| Delete,
|
| sub-del | proved | all subs proved
| Delete,
|
| sub-del-01 | proved | all subs proved
| Delete,
|
| sub-del-02 | proved | all subs proved
| Delete,
|
| sub-del-03 | proved | all subs proved
| Delete,
|
| sub-del-05 | proved | all subs proved
| Delete,
|
| subseteq-rem-del | proved | all subs proved
| Delete,
Difference,
|
| subsub-del | proved | all subs proved
| Delete,
|
| uninsubdel | proved | all subs proved
| Delete,
Union,
|
| union-del | proved | all subs proved
| Delete,
Union,
|
| size-eq | proved | all subs proved
| |
| One | axiom | | |
| filter-in | axiom | | |
| Disjoint | axiom | | |
| Union | axiom | | |
| Difference | axiom | | |
| del-neq | proved | all subs proved
| |
| Intersect | axiom | | |
| Delete | axiom | | |