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