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: |
|---|
| diffone-nodupssize | proved | all subs proved
| diff-n,
diff-y,
diff-onenonmember,
diff-firstofapp,
diff-e,
|
| diffone-nodupsget | proved | all subs proved
| diff-n,
diff-y,
diff-onenonmember,
diff-firstofapp,
|
| diff-firstofapp | proved | all subs proved
| diff-same,
diff-append,
|
| le | proved | all subs proved
| filt-n,
filter-empty-01,
del1-01,
filt-y,
filt-e,
|
| filter-empty-in-01 | proved | all subs proved
| filter-empty-in,
|
| filter-empty-append | proved | all subs proved
| filter-empty-app-02,
filter-empty-app,
filter-empty-app-03,
|
| filter-empty-01 | proved | all subs proved
| filter-empty-def,
|
| filter-empty-in | proved | all subs proved
| filter-empty-def,
|
| filter-empty-app-03 | proved | all subs proved
| filter-notempty,
filter-empty-def,
|
| filter-empty-app | proved | all subs proved
| filter-empty-def,
|
| filter-empty-app-02 | proved | all subs proved
| filter-empty-def,
|
| diff-same | proved | all subs proved
| subset-ref,
diff-empty-sub,
diff-app,
|
| filter-rev-empty | proved | all subs proved
| filter-notempty,
filter-empty-def,
|
| filter-empty-subset-01 | proved | all subs proved
| filter-notempty,
sub-in,
filter-empty-def,
|
| filter-empty-subset | proved | all subs proved
| filter-notempty,
sub-in,
filter-empty-def,
|
| filter-empty-one | proved | all subs proved
| filter-empty-def,
|
| filter-empty-cons | proved | all subs proved
| filter-notempty,
filter-empty-def,
|
| filter-empty-commutative | proved | all subs proved
| filter-notempty,
filter-empty-def,
|
| filter-empty-app-04 | proved | all subs proved
| filter-notempty,
filter-empty-def,
|
| filter-empty-app-01 | proved | all subs proved
| filter-empty-def,
|
| diff-consbothsame | proved | all subs proved
| diff-app,
diff-append,
|
| filter-empty-def | proved | all subs proved
| filt-n,
filt-y,
filt-e,
filter-notempty,
|
| diff-app | proved | all subs proved
| subset-app,
diff-empty-sub,
diff-app-02,
|
| filter-all | proved | all subs proved
| filter-notempty,
filt-n,
filt-y,
filt-e,
|
| filter-notempty | proved | all subs proved
| filter-one,
filter-empty,
filt-e,
|
| diff-app-02 | proved | all subs proved
| subset-app-02,
diff-empty-sub,
diff-e,
|
| union-twice | proved | all subs proved
| subset-ref,
subset-rmdup,
assoc,
union,
|
| subset-diff-union | proved | all subs proved
| sub-in,
diff-in,
sub-notin,
subset,
rmdup-01,
assoc,
union,
|
| size-le | proved | all subs proved
| firstsub,
subset,
assoc,
union,
|
| onein-diff | proved | all subs proved
| subset-one,
diff-empty-sub,
|
| in-05 | proved | all subs proved
| filt-in,
in-01-01,
|
| filter-rest | proved | all subs proved
| filter-one,
filter-empty,
|
| filter-empty-cons-01 | proved | all subs proved
| filter-one,
filter-empty,
filt-n,
|
| filt-dups | proved | all subs proved
| filt-n,
filt-in,
filt-y,
filt-e,
|
| f-rm | proved | all subs proved
| filt-n,
filt-in,
filt-y,
filt-e,
|
| diff-union | proved | all subs proved
| diff-in,
diff-y,
diff-n,
diff-e,
assoc,
union,
|
| diff-unchanged | proved | all subs proved
| diff-n,
diff-in,
diff-y,
diff-e,
|
| diff-in-one | proved | all subs proved
| diff-in,
|
| diff-dups | proved | all subs proved
| diff-in,
diff-n,
diff-y,
diff-e,
|
| diff-app-01 | proved | all subs proved
| subset-one,
subset-app-04,
diff-empty-sub,
diff-e,
|
| subset-rmdup | proved | all subs proved
| subset-rec,
|
| firstsub | proved | all subs proved
| subset,
assoc,
union,
|
| filter-one | proved | all subs proved
| filter-one-02,
filter-one-01,
|
| filt-in | proved | all subs proved
| notin-02,
in-01-01,
|
| diff-in | proved | all subs proved
| diff-n,
notin-01,
diff-y,
diff-e,
|
| diff-empty-sub | proved | all subs proved
| subset,
diff-empty-all,
|
| subsub-01 | proved | all subs proved
| rmdup-01,
assoc,
union,
subset,
|
| subsub | proved | all subs proved
| rmdup-01,
assoc,
union,
subset,
|
| subset-trans | proved | all subs proved
| sub-notin,
sub-in,
subset,
|
| subset-empty-01 | proved | all subs proved
| subset,
subset-empty,
|
| subset-01-01 | proved | all subs proved
| subset,
rmdup-01,
assoc,
union,
|
| subset-01 | proved | all subs proved
| subset,
rmdup-01,
assoc,
union,
|
| subonein | proved | all subs proved
| subset-rec,
rmdup,
assoc,
union,
|
| suband | proved | all subs proved
| subset,
rmdup,
assoc,
union,
|
| sub-size-02 | proved | all subs proved
| subset,
assoc,
union,
|
| sub-size-01 | proved | all subs proved
| sub-in,
|
| sub-size | proved | all subs proved
| sub-in,
|
| sub-07 | proved | all subs proved
| subset,
rmdup,
assoc,
union,
|
| sub-06 | proved | all subs proved
| subset,
rmdup,
assoc,
union,
|
| sub-05 | proved | all subs proved
| subset,
rmdup-01,
rmdup,
assoc,
union,
|
| sub-04 | proved | all subs proved
| subset,
rmdup-01,
rmdup,
assoc,
union,
|
| sub-03 | proved | all subs proved
| subset,
rmdup-01,
assoc,
union,
|
| sub-02 | proved | all subs proved
| subset,
rmdup-01,
assoc,
union,
|
| sub-01 | proved | all subs proved
| subset,
rmdup-01,
rmdup,
assoc,
union,
|
| sub | proved | all subs proved
| subset,
rmdup-01,
rmdup,
assoc,
union,
|
| size-nls-01 | proved | all subs proved
| assoc,
union,
|
| size-nls | proved | all subs proved
| assoc,
union,
|
| size-nle | proved | all subs proved
| subset,
rmdup-01,
assoc,
union,
|
| rotsize | proved | all subs proved
| assoc,
union,
|
| rmdup-size | proved | all subs proved
| assoc,
union,
|
| rmdup-02 | proved | all subs proved
| assoc,
union,
|
| onenotin-diff | proved | all subs proved
| diff-consnotin2,
diff-empty,
|
| notin | proved | all subs proved
| assoc,
union,
|
| nodups | proved | all subs proved
| assoc,
union,
|
| k-union-rec-y | proved | all subs proved
| assoc,
union,
|
| k-union-rec-n | proved | all subs proved
| assoc,
union,
|
| insub-01 | proved | all subs proved
| subset,
rmdup,
assoc,
union,
|
| insub | proved | all subs proved
| subset,
rmdup,
assoc,
union,
|
| in-06 | proved | all subs proved
| in-01-01,
|
| in-04 | proved | all subs proved
| assoc,
union,
|
| in-03 | proved | all subs proved
| assoc,
union,
|
| in-02 | proved | all subs proved
| assoc,
union,
|
| in-01 | proved | all subs proved
| assoc,
union,
|
| firstinsub | proved | all subs proved
| subset-rec,
rmdup-01,
assoc,
union,
|
| firstin | proved | all subs proved
| assoc,
union,
|
| emptyunion | proved | all subs proved
| assoc,
union,
|
| diffgetn-nodupssize | proved | all subs proved
| diff-e,
diff-n,
diff-onenonmember,
diff-y,
|
| diff-twice-union | proved | all subs proved
| diff-n,
diff-y,
diff-e,
assoc,
union,
|
| commsize | proved | all subs proved
| assoc,
union,
|
| assocsize | proved | all subs proved
| assoc,
|
| appsize | proved | all subs proved
| assoc,
union,
|
| app | proved | all subs proved
| assoc,
union,
|
| Noassoc | proved | all subs proved
| assoc,
union,
|
| subset-empty | proved | all subs proved
| subset,
|
| sub-notin | proved | all subs proved
| subset,
|
| diff-empty | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| diff-consnotin2 | proved | all subs proved
| diff-y,
diff-n,
diff-e,
|
| del1-01 | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| rmdup | proved | all subs proved
| subset,
|
| rmdup-01 | proved | all subs proved
| subset,
|
| subset-rec | proved | all subs proved
| subset,
|
| filter-one-01 | proved | all subs proved
| filt-e,
filt-y,
|
| filter-one-02 | proved | all subs proved
| filt-e,
filt-n,
|
| sub-in | proved | all subs proved
| subset,
|
| filter-empty | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| in-01-01 | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| notin-02 | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| diff-onenonmember | proved | all subs proved
| diff-y,
diff-n,
diff-e,
|
| subset-ref | proved | all subs proved
| subset,
|
| notin-01 | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| diff-empty-all | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| diff-append | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| subset-app-02 | proved | all subs proved
| subset,
|
| subset-app-04 | proved | all subs proved
| subset,
|
| subset-one | proved | all subs proved
| subset,
|
| subset-app | proved | all subs proved
| subset,
|
| assoc | proved | all subs proved
| union,
|
| subset-perm | proved | all subs proved
| subset,
|
| subset-insert | proved | all subs proved
| subset,
|
| subset-del | proved | all subs proved
| subset,
|
| subset-append-02 | proved | all subs proved
| subset,
|
| subset-append-01 | proved | all subs proved
| subset,
|
| subset-append | proved | all subs proved
| subset,
|
| subset-app-03 | proved | all subs proved
| subset,
|
| subset-app-01 | proved | all subs proved
| subset,
|
| size | proved | all subs proved
| subset,
|
| rax-01 | proved | all subs proved
| diff-n,
|
| filter-notin | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| filter-dups | proved | all subs proved
| filt-n,
filt-e,
|
| empty-01 | proved | all subs proved
| union,
|
| empty | proved | all subs proved
| union,
|
| dups-app | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| diff-wfrec | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| diff-twice-append-rev | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| diff-twice-append | proved | all subs proved
| diff-n,
diff-y,
diff-e,
|
| del1 | proved | all subs proved
| filt-n,
filt-y,
filt-e,
|
| subset | axiom | | |
| diff-y | axiom | | |
| diff-n | axiom | | |
| diff-e | axiom | | |
| filt-e | axiom | | |
| filt-y | axiom | | |
| filt-n | axiom | | |
| union | axiom | | |