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-mklist-del | proved | all subs proved
| del1-01,
perm-rec,
del,
ocs-mklist,
perm-mklist,
empty,
|
| perm-rec | proved | all subs proved
| perm-last-rec,
perm-shift-in2,
sym-02,
del-01,
shift-03,
ref,
app-beg-beg,
sym-01,
trans,
|
| perm-shift-in2 | proved | all subs proved
| perm-one,
app-beg-end,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
perm-last-rec,
|
| perm-last-rec | proved | all subs proved
| del,
perm-one,
empty,
perm-e,
|
| shift-01 | proved | all subs proved
| perm-one,
app-beg-end,
app-end-end,
|
| perm-mklist | proved | all subs proved
| del-01,
del,
ref,
sym-01,
trans,
perm-e,
empty,
|
| perm-one | proved | all subs proved
| ref,
empty,
del-01,
empty-01,
|
| rec-01 | proved | all subs proved
| del-01,
shift-03,
|
| perm-app-left-rev | proved | all subs proved
| perm-app-left-sym,
sym-02,
sym-01,
neq,
app-end-end,
trans,
|
| in-02 | proved | all subs proved
| rec,
|
| in-03 | proved | all subs proved
| rec,
|
| app-end-all | proved | all subs proved
| app-all-end,
sym-01,
ref,
|
| perm-app-right-rev-sym | proved | all subs proved
| perm-app-left-sym,
sym-02,
sym-01,
app-end-end,
trans,
|
| app-in-in | proved | all subs proved
| app-beg-in,
shift-02,
|
| app-beg-in | proved | all subs proved
| app-in-beg,
sym-02,
sym-01,
c,
|
| app-all-end | proved | all subs proved
| delapp,
del-01,
del,
ref,
app-end-end,
sym-01,
trans,
|
| rec | proved | all subs proved
| del,
del-01,
|
| empty | proved | all subs proved
| empty-01,
sym-01,
perm-e,
|
| perm-app-left-sym | proved | all subs proved
| perm-app-left,
sym-02,
sym-01,
app-end-end,
trans,
|
| shift-03 | proved | all subs proved
| in,
ref,
del-02,
app-beg-beg,
sym-01,
trans,
del-01,
|
| papp-02 | proved | all subs proved
| papp-03,
app-beg-end,
shift-02,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
|
| perm-app-left-rev-sym | proved | all subs proved
| perm-app-left,
sym-02,
sym-01,
app-end-end,
trans,
|
| perm-r | proved | all subs proved
| empty-01,
|
| perm-app-right-sym | proved | all subs proved
| sym-02,
perm-app-left,
|
| perm-app-right-rev | proved | all subs proved
| perm-app-left,
sym-02,
sym-01,
ref,
perm-app-right,
|
| perm-rmdup-rev | proved | all subs proved
| del-01,
perm-e,
empty-01,
|
| adjoin | proved | all subs proved
| del-01,
in,
ref,
sym-01,
trans,
sym-02,
|
| app-in-beg | proved | all subs proved
| c,
app-end-in,
shift-02,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
|
| empty-01 | proved | all subs proved
| del,
ref,
perm-e,
sym-01,
trans,
|
| del-01 | proved | all subs proved
| sym-02,
del,
sym,
|
| perm-app-left | proved | all subs proved
| perm-app-right,
sym-02,
sym-01,
neq,
app-end-end,
trans,
|
| papp-03 | proved | all subs proved
| papp,
app-end-end,
neq,
app-beg-beg,
sym-02,
ref,
sym-01,
trans,
|
| papp-01 | proved | all subs proved
| subapp-01,
perm,
|
| perm-put | proved | all subs proved
| del-02,
perm-put-del1,
perm-del,
sym-02,
in,
ref,
sym-01,
trans,
|
| perm-rev-02 | proved | all subs proved
| sym-02,
perm-rev-01,
sym,
|
| perm-rev-01 | proved | all subs proved
| sym,
ref,
sym-01,
sym-02,
trans,
perm-rev,
|
| perm-del | proved | all subs proved
| del-04,
sym-02,
neq,
ref,
sym-01,
trans,
|
| app-end-in | proved | all subs proved
| app-in-end,
sym-02,
sym-01,
|
| del | proved | all subs proved
| in-01,
del1,
msubset,
in-05,
subrec-01,
subrec,
perm,
|
| perm-app-right | proved | all subs proved
| app-end-end,
a,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
|
| papp | proved | all subs proved
| subapp,
perm,
|
| subapp-01 | proved | all subs proved
| subdel-01,
subrec,
subapp-02,
subempty,
|
| cons | proved | all subs proved
| a,
app-beg-beg,
|
| del-in | proved | all subs proved
| del-04,
del-02,
|
| ocs-same-length-all | proved | all subs proved
| ocs-same-length-mklist,
|
| perm-switch | proved | all subs proved
| ocs-sw,
perm-all,
|
| perm-dups-02 | proved | all subs proved
| perm-dups-01,
ref,
app-beg-beg,
sym-01,
trans,
|
| perm-dups-03 | proved | all subs proved
| perm-dups-01,
ref,
app-beg-beg,
sym-01,
trans,
|
| perm-rmv-in | proved | all subs proved
| perm-rmv-in-list,
|
| perm-common-prefix | proved | all subs proved
| a,
sym-02,
ref,
app-beg-beg,
sym-01,
trans,
|
| perm-swap | proved | all subs proved
| ocs-sw,
perm-all,
|
| perm-rmcommon-beg-beg | proved | all subs proved
| a,
app-beg-beg,
|
| perm-same-prefix | proved | all subs proved
| ref,
sym-01,
trans,
a,
|
| perm-del-01 | proved | all subs proved
| in-05,
notin,
perm-del-in,
oc-zero,
ocs-del,
ocs-del-length,
perm-all,
ref,
sym-01,
trans,
sym-02,
neq,
|
| app-in-end | proved | all subs proved
| app-beg-end,
shift-02,
|
| perm-rev | proved | all subs proved
| sym-01,
neq,
app-beg-end,
perm-e,
sym-02,
|
| subdel-01 | proved | all subs proved
| del1-01,
in-05,
del1,
oc-del-01,
ocappend,
oc-zero,
msubset,
|
| perm-del-in | proved | all subs proved
| in,
ref,
sym-01,
trans,
|
| perm-rmv-in-list | proved | all subs proved
| app-beg-beg,
sym,
shift-02,
|
| subapp | proved | all subs proved
| subrec,
subapp-03,
subempty,
|
| perm-dups-01 | proved | all subs proved
| perm-dups,
ref,
sym-01,
trans,
|
| ocs-sw | proved | all subs proved
| oc-zero,
ocs-put,
ocs-put-02,
ocs-put-01,
|
| ocs-same-length-mklist | proved | all subs proved
| ocs-not-more,
one-01,
one,
ocappend,
oc-e,
|
| perm-put-del1 | proved | all subs proved
| ocs-put-01,
ocs-put,
ocs-put-02,
in-05,
oc-zero,
notin,
del1,
del1-01,
perm-all,
sym-02,
|
| del-04 | proved | all subs proved
| in,
in-05,
oc-zero,
notin,
del1,
del1-01,
perm-all,
ref,
sym-01,
trans,
sym-02,
|
| a | proved | all subs proved
| sym-02,
sym-01,
neq,
app-beg-beg,
|
| subrec-01 | proved | all subs proved
| del1-01,
one-01,
oc,
one,
ocappend,
subrec,
subempty,
oc-e,
|
| shift | proved | all subs proved
| ref,
app-beg-end,
|
| subdel | proved | all subs proved
| oc-del,
oc-zero,
msubset,
|
| ad | proved | all subs proved
| in-05,
oc-zero,
del1,
oc-del-01,
del1-01,
ocappend,
msubset,
perm,
|
| diff | proved | all subs proved
| notin,
oc-zero,
oc-diff-01,
oc-diff,
sym-02,
msubset,
perm,
|
| perm-shift-out2 | proved | all subs proved
| app-beg-end,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
|
| del-05 | proved | all subs proved
| in-05,
del1,
perm-all,
ref,
del-02,
sym-01,
trans,
|
| subdel-03 | proved | all subs proved
| in-05,
notin,
del1,
oc-zero,
oc,
sub-del,
|
| subdel-02 | proved | all subs proved
| in-05,
del1,
oc,
oc-zero,
sub-del,
|
| perm-com2 | proved | all subs proved
| shift-02,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
|
| perm-com1 | proved | all subs proved
| shift-02,
ref,
app-beg-beg,
sym-01,
trans,
sym-02,
neq,
|
| nodups | proved | all subs proved
| in-05,
notin,
oc-dups,
msubset,
perm,
|
| perm-common-postfix | proved | all subs proved
| app-end-end,
sym-02,
ref,
app-beg-beg,
sym-01,
trans,
|
| app-end-beg | proved | all subs proved
| app-beg-end,
sym-02,
sym-01,
|
| subperm | proved | all subs proved
| in,
ref,
sym-01,
trans,
|
| app-beg-all | proved | all subs proved
| app-all-beg,
sym-01,
ref,
|
| app-attach | proved | all subs proved
| app-end-end,
|
| perm-rmcommon-end-end | proved | all subs proved
| app-end-end,
|
| subperm-01 | proved | all subs proved
| in,
ref,
sym-01,
trans,
|
| perm-rmcommon-beg-end | proved | all subs proved
| app-beg-end,
|
| intersect | proved | all subs proved
| notin,
oc-filt-01,
oc-zero,
oc-filt,
sym-02,
msubset,
perm,
|
| size-perm | proved | all subs proved
| oc-zero,
oc-dups,
msubset,
perm,
|
| oc-filt-01 | proved | all subs proved
| oc-zero,
|
| delapp | proved | all subs proved
| in-05,
notin,
del1-01,
one,
oc-zero,
del1,
oc-e,
ocappend,
msubset,
perm,
|
| ocs-not-more | proved | all subs proved
| in-05,
one-01,
one,
ocappend,
oc-e,
oc-zero,
|
| subapp-02 | proved | all subs proved
| oc-zero,
ocappend,
msubset,
|
| ocs-del | proved | all subs proved
| oc-zero,
|
| app-all-beg | proved | all subs proved
| one,
oc-zero,
oc-e,
ocappend,
msubset,
perm,
|
| oc-dups | proved | all subs proved
| in-05,
one-01,
one,
notin,
ocappend,
oc-e,
oc-zero,
|
| sub-del | proved | all subs proved
| in-05,
ocs-del-length,
oc-zero,
msubset,
|
| perm-dups | proved | all subs proved
| ocnodups,
one,
ocappend,
msubset,
perm,
|
| del-02 | proved | all subs proved
| del1,
del1-01,
oc-zero,
msubset,
perm,
|
| subapp-03 | proved | all subs proved
| oc-zero,
ocappend,
msubset,
|
| oc-diff | proved | all subs proved
| oc-zero,
|
| perm-all | proved | all subs proved
| notin,
oc-zero,
msubset,
perm,
|
| ocs-put-02 | proved | all subs proved
| one-01,
oc-zero,
oc-n,
one,
ocappend,
oc-e,
|
| oc-del-01 | proved | all subs proved
| del1,
oc-zero,
ocappend,
|
| c | proved | all subs proved
| oc-zero,
ocappend,
msubset,
perm,
|
| oc-del | proved | all subs proved
| del1,
del1-01,
oc-zero,
|
| perm-e | proved | all subs proved
| ref,
|
| subrec | proved | all subs proved
| del1-01,
one-01,
del1,
in-05,
oc-zero,
notin,
one,
ocappend,
msubset,
|
| app-beg-end | proved | all subs proved
| oc-zero,
ocappend,
msubset,
perm,
|
| trans | proved | all subs proved
| oc-zero,
sym-02,
msubset,
perm,
|
| app-beg-beg | proved | all subs proved
| oc-zero,
ocappend,
msubset,
perm,
|
| app-end-end | proved | all subs proved
| oc-zero,
ocappend,
msubset,
perm,
|
| ocs-del1-if | proved | all subs proved
| del1,
del1-01,
|
| in-put | proved | all subs proved
| one-01,
one,
oc-zero,
ocappend,
oc-e,
|
| in-sym | proved | all subs proved
| in,
sym,
|
| in-04 | proved | all subs proved
| in,
sym-01,
|
| l | proved | all subs proved
| subsize,
msubset,
perm,
|
| oc-del-02 | proved | all subs proved
| del1,
del1-01,
oc-zero,
|
| ocs-dups-ex | proved | all subs proved
| oc-zero,
oc-e,
one,
ocappend,
in-05,
|
| ocs-del-del1 | proved | all subs proved
| one-01,
oc-zero,
one,
ocappend,
oc-e,
|
| ocs-del1 | proved | all subs proved
| one,
ocappend,
oc-e,
oc-zero,
|
| ocnodups | proved | all subs proved
| one-01,
notin,
one,
ocappend,
oc-e,
|
| subsize | proved | all subs proved
| notin,
one,
oc-e,
ocappend,
msubset,
|
| in | proved | all subs proved
| in-05,
notin,
msubset,
perm,
|
| oc-zero | proved | all subs proved
| notin,
in-05,
|
| del1 | proved | all subs proved
| oc-n,
one-01,
one,
ocappend,
oc-e,
in-05,
|
| in-01 | proved | all subs proved
| notin,
oc-y,
msubset,
perm,
|
| ref | proved | all subs proved
| msubset,
perm,
sym-02,
|
| neq | proved | all subs proved
| sym-02,
sym-01,
|
| ocone | proved | all subs proved
| in-05,
|
| ocnodups-01 | proved | all subs proved
| in-05,
notin,
|
| oc-filt | proved | all subs proved
| oc-n,
one-01,
one,
ocappend,
oc-e,
|
| ocs-del-length | proved | all subs proved
| one-01,
one,
ocappend,
oc-e,
|
| ocs-mklist | proved | all subs proved
| one-01,
one,
ocappend,
oc-e,
|
| oc-diff-01 | proved | all subs proved
| oc-n,
one-01,
one,
ocappend,
oc-e,
|
| notin | proved | all subs proved
| one-01,
ocappend,
oc-e,
|
| ocs-put | proved | all subs proved
| one-01,
one,
ocappend,
|
| ocs-put-01 | proved | all subs proved
| one-01,
one,
ocappend,
|
| del1-01 | proved | all subs proved
| oc-n,
one-01,
one,
ocappend,
oc-e,
|
| in-05 | proved | all subs proved
| one-01,
one,
ocappend,
oc-e,
|
| shift-02 | proved | all subs proved
| ocappend,
msubset,
perm,
|
| sym-01 | proved | all subs proved
| sym,
|
| sym-02 | proved | all subs proved
| sym,
|
| rest | proved | all subs proved
| one-01,
one,
ocappend,
msubset,
|
| oc | proved | all subs proved
| msubset,
|
| sym | proved | all subs proved
| perm,
|
| subempty | proved | all subs proved
| oc-e,
msubset,
|
| ocappend | proved | all subs proved
| oc-n,
oc-y,
oc-e,
|
| one | proved | all subs proved
| oc-e,
oc-y,
|
| one-01 | proved | all subs proved
| oc-e,
oc-n,
|
| oc-adjoin | proved | all subs proved
| oc-n,
|
| oc-y | axiom | | |
| oc-e | axiom | | |
| oc-n | axiom | | |
| msubset | axiom | | |
| perm | axiom | | |