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