[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification list-perm

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-delprovedall subs proved del1-01, perm-rec, del, ocs-mklist, perm-mklist, empty,
perm-recprovedall subs proved perm-last-rec, perm-shift-in2, sym-02, del-01, shift-03, ref, app-beg-beg, sym-01, trans,
perm-shift-in2provedall subs proved perm-one, app-beg-end, ref, app-beg-beg, sym-01, trans, sym-02, perm-last-rec,
perm-last-recprovedall subs proved del, perm-one, empty, perm-e,
shift-01provedall subs proved perm-one, app-beg-end, app-end-end,
perm-mklistprovedall subs proved del-01, del, ref, sym-01, trans, perm-e, empty,
perm-oneprovedall subs proved ref, empty, del-01, empty-01,
rec-01provedall subs proved del-01, shift-03,
app-end-allprovedall subs proved app-all-end, sym-01, ref,
in-02provedall subs proved rec,
app-in-inprovedall subs proved app-beg-in, shift-02,
in-03provedall subs proved rec,
app-beg-inprovedall subs proved app-in-beg, sym-02, sym-01, c,
recprovedall subs proved del, del-01,
app-all-endprovedall subs proved delapp, del-01, del, ref, app-end-end, sym-01, trans,
shift-03provedall subs proved in, ref, del-02, app-beg-beg, sym-01, trans, del-01,
emptyprovedall subs proved empty-01, sym-01, perm-e,
adjoinprovedall subs proved del-01, in, ref, sym-01, trans, sym-02,
papp-02provedall subs proved papp-03, app-beg-end, shift-02, ref, app-beg-beg, sym-01, trans, sym-02,
perm-rprovedall subs proved empty-01,
perm-rmdup-revprovedall subs proved del-01, perm-e, empty-01,
papp-03provedall subs proved papp, app-end-end, neq, app-beg-beg, sym-02, ref, sym-01, trans,
app-in-begprovedall subs proved c, app-end-in, shift-02, ref, app-beg-beg, sym-01, trans, sym-02,
empty-01provedall subs proved del, ref, perm-e, sym-01, trans,
del-01provedall subs proved sym-02, del, sym,
perm-rev-02provedall subs proved sym-02, perm-rev-01, sym,
perm-putprovedall subs proved del-02, perm-put-del1, perm-del, sym-02, in, ref, sym-01, trans,
papp-01provedall subs proved subapp-01, perm,
subapp-01provedall subs proved subdel-01, subrec, subapp-02, subempty,
perm-delprovedall subs proved del-04, sym-02, neq, ref, sym-01, trans,
app-end-inprovedall subs proved app-in-end, sym-02, sym-01,
perm-rev-01provedall subs proved sym, ref, sym-01, sym-02, trans, perm-rev,
pappprovedall subs proved subapp, perm,
delprovedall subs proved in-01, del1, msubset, in-05, subrec-01, subrec, perm,
perm-dups-02provedall subs proved perm-dups-01, ref, app-beg-beg, sym-01, trans,
perm-switchprovedall subs proved ocs-sw, perm-all,
perm-del-01provedall subs proved in-05, notin, perm-del-in, oc-zero, ocs-del, ocs-del-length, perm-all, ref, sym-01, trans, sym-02, neq,
consprovedall subs proved a, app-beg-beg,
perm-common-prefixprovedall subs proved a, sym-02, ref, app-beg-beg, sym-01, trans,
perm-rmv-inprovedall subs proved perm-rmv-in-list,
perm-rmcommon-beg-begprovedall subs proved a, app-beg-beg,
perm-same-prefixprovedall subs proved ref, sym-01, trans, a,
perm-dups-03provedall subs proved perm-dups-01, ref, app-beg-beg, sym-01, trans,
del-inprovedall subs proved del-04, del-02,
perm-swapprovedall subs proved ocs-sw, perm-all,
ocs-same-length-allprovedall subs proved ocs-same-length-mklist,
ocs-same-length-mklistprovedall subs proved ocs-not-more, one-01, one, ocappend, oc-e,
app-in-endprovedall subs proved app-beg-end, shift-02,
subdel-01provedall subs proved del1-01, in-05, del1, oc-del-01, ocappend, oc-zero, msubset,
subrec-01provedall subs proved del1-01, one-01, oc, one, ocappend, subrec, subempty, oc-e,
subappprovedall subs proved subrec, subapp-03, subempty,
perm-revprovedall subs proved sym-01, neq, app-beg-end, perm-e, sym-02,
perm-put-del1provedall subs proved ocs-put-01, ocs-put, ocs-put-02, in-05, oc-zero, notin, del1, del1-01, perm-all, sym-02,
perm-rmv-in-listprovedall subs proved app-beg-beg, sym, shift-02,
aprovedall subs proved sym-02, sym-01, neq, app-beg-beg,
perm-del-inprovedall subs proved in, ref, sym-01, trans,
del-04provedall subs proved in, in-05, oc-zero, notin, del1, del1-01, perm-all, ref, sym-01, trans, sym-02,
ocs-swprovedall subs proved oc-zero, ocs-put, ocs-put-02, ocs-put-01,
perm-dups-01provedall subs proved perm-dups, ref, sym-01, trans,
adprovedall subs proved in-05, oc-zero, del1, oc-del-01, del1-01, ocappend, msubset, perm,
app-end-begprovedall subs proved app-beg-end, sym-02, sym-01,
filterprovedall subs proved notin, oc-filt-01, oc-zero, oc-filt, sym-02, msubset, perm,
perm-rmcommon-end-endprovedall subs proved app-end-end,
perm-rmcommon-beg-endprovedall subs proved app-beg-end,
diffprovedall subs proved notin, oc-zero, oc-diff-01, oc-diff, sym-02, msubset, perm,
perm-com2provedall subs proved shift-02, ref, app-beg-beg, sym-01, trans, sym-02,
subdel-02provedall subs proved in-05, del1, oc, oc-zero, sub-del,
subdelprovedall subs proved oc-del, oc-zero, msubset,
app-attachprovedall subs proved app-end-end,
app-beg-allprovedall subs proved app-all-beg, sym-01, ref,
subperm-01provedall subs proved in, ref, sym-01, trans,
perm-com1provedall subs proved shift-02, ref, app-beg-beg, sym-01, trans, sym-02, neq,
size-permprovedall subs proved oc-zero, oc-dups, msubset, perm,
perm-shift-out2provedall subs proved app-beg-end, ref, app-beg-beg, sym-01, trans, sym-02,
nodupsprovedall subs proved in-05, notin, oc-dups, msubset, perm,
del-05provedall subs proved in-05, del1, perm-all, ref, del-02, sym-01, trans,
subpermprovedall subs proved in, ref, sym-01, trans,
shiftprovedall subs proved ref, app-beg-end,
subdel-03provedall subs proved in-05, notin, del1, oc-zero, oc, sub-del,
perm-common-postfixprovedall subs proved app-end-end, sym-02, ref, app-beg-beg, sym-01, trans,
subapp-02provedall subs proved oc-zero, ocappend, msubset,
subapp-03provedall subs proved oc-zero, ocappend, msubset,
subrecprovedall subs proved del1-01, one-01, del1, in-05, oc-zero, notin, one, ocappend, msubset,
delappprovedall subs proved in-05, notin, del1-01, one, oc-zero, del1, oc-e, ocappend, msubset, perm,
ocs-not-moreprovedall subs proved in-05, one-01, one, ocappend, oc-e, oc-zero,
ocs-put-02provedall subs proved one-01, oc-zero, oc-n, one, ocappend, oc-e,
cprovedall subs proved oc-zero, ocappend, msubset, perm,
perm-dupsprovedall subs proved ocnodups, one, ocappend, msubset, perm,
oc-dupsprovedall subs proved in-05, one-01, one, notin, ocappend, oc-e, oc-zero,
app-all-begprovedall subs proved one, oc-zero, oc-e, ocappend, msubset, perm,
oc-delprovedall subs proved del1, del1-01, oc-zero,
sub-delprovedall subs proved in-05, ocs-del-length, oc-zero, msubset,
ocs-delprovedall subs proved oc-zero,
oc-diffprovedall subs proved oc-zero,
del-02provedall subs proved del1, del1-01, oc-zero, msubset, perm,
app-end-endprovedall subs proved oc-zero, ocappend, msubset, perm,
oc-filt-01provedall subs proved oc-zero,
perm-eprovedall subs proved ref,
perm-allprovedall subs proved notin, oc-zero, msubset, perm,
transprovedall subs proved oc-zero, sym-02, msubset, perm,
app-beg-begprovedall subs proved oc-zero, ocappend, msubset, perm,
app-beg-endprovedall subs proved oc-zero, ocappend, msubset, perm,
oc-del-01provedall subs proved del1, oc-zero, ocappend,
ocs-dups-exprovedall subs proved oc-zero, oc-e, one, ocappend, in-05,
ocs-del1provedall subs proved one, ocappend, oc-e, oc-zero,
ocs-del1-ifprovedall subs proved del1, del1-01,
ocs-del-del1provedall subs proved one-01, oc-zero, one, ocappend, oc-e,
in-04provedall subs proved in, sym-01,
oc-del-02provedall subs proved del1, del1-01, oc-zero,
in-symprovedall subs proved in, sym,
lprovedall subs proved subsize, msubset, perm,
in-putprovedall subs proved one-01, one, oc-zero, ocappend, oc-e,
in-01provedall subs proved notin, oc-y, msubset, perm,
subsizeprovedall subs proved notin, one, oc-e, ocappend, msubset,
ocnodupsprovedall subs proved one-01, notin, one, ocappend, oc-e,
inprovedall subs proved in-05, notin, msubset, perm,
neqprovedall subs proved sym-02, sym-01,
refprovedall subs proved msubset, perm, sym-02,
del1provedall subs proved oc-n, one-01, one, ocappend, oc-e, in-05,
oc-zeroprovedall subs proved notin, in-05,
oconeprovedall subs proved in-05,
ocnodups-01provedall subs proved in-05, notin,
ocs-mklistprovedall subs proved one-01, one, ocappend, oc-e,
ocs-putprovedall subs proved one-01, one, ocappend,
ocs-put-01provedall subs proved one-01, one, ocappend,
oc-diff-01provedall subs proved oc-n, one-01, one, ocappend, oc-e,
ocs-del-lengthprovedall subs proved one-01, one, ocappend, oc-e,
shift-02provedall subs proved ocappend, msubset, perm,
oc-filtprovedall subs proved oc-n, one-01, one, ocappend, oc-e,
sym-01provedall subs proved sym,
sym-02provedall subs proved sym,
notinprovedall subs proved one-01, ocappend, oc-e,
del1-01provedall subs proved oc-n, one-01, one, ocappend, oc-e,
in-05provedall subs proved one-01, one, ocappend, oc-e,
restprovedall subs proved one-01, one, ocappend, msubset,
subemptyprovedall subs proved oc-e, msubset,
ocprovedall subs proved msubset,
symprovedall subs proved perm,
oneprovedall subs proved oc-e, oc-y,
one-01provedall subs proved oc-e, oc-n,
ocappendprovedall subs proved oc-n, oc-y, oc-e,
oc-adjoinprovedall subs proved oc-n,
oc-yaxiom
oc-eaxiom
oc-naxiom
permaxiom
msubsetaxiom