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: |
|---|
| lastn-neq | proved | all subs proved
| lastN-in-01,
|
| firstN-dups-01 | proved | all subs proved
| firstN-dups-03,
|
| firstN-dups | proved | all subs proved
| firstN-dups-02,
|
| firstn-at-in-dups | proved | all subs proved
| get-firstn,
firstn-length-03,
in-get,
dups-def,
firstN-in-05,
|
| sublist-is-restn | proved | all subs proved
| rest-len,
first-all-01,
sublist-def,
sublist-append,
|
| sublist-mklist-01 | proved | all subs proved
| sublist-mklist,
sublist-append,
|
| sublist-append | proved | all subs proved
| sublist-def,
first-append-01,
rest-append,
|
| firstN-in-05 | proved | all subs proved
| firstN-in-01,
|
| firstN-dups-02 | proved | all subs proved
| firstN-in-04,
firstN-dups-04,
|
| firstN-dups-03 | proved | all subs proved
| firstN-in-04,
firstN-dups-04,
|
| lastN-in-01 | proved | all subs proved
| rest-in-01,
lastn-restn-01,
|
| firstn-restn-in | proved | all subs proved
| rest-in,
rest-in-01,
elim-firstn-restn,
firstN-in,
restN-rec,
firstN-rec,
restN-zero,
firstN-zero,
|
| lastN-in | proved | all subs proved
| rest-in-01,
lastn-restn-01,
|
| firstN-dups-05 | proved | all subs proved
| firstN-dups-04,
|
| sublist-move | proved | all subs proved
| first-append-01,
rest-append,
elim-firstn-restn,
restN-rec,
firstn-firstn,
firstN-rec,
first-num,
rest-rec,
firstN-zero,
restN-zero,
sublist-def,
|
| lastn-neq-01 | proved | all subs proved
| rest-in-01,
lastn-restn-01,
lastN-rec,
lastN-zero,
|
| first-append-01 | proved | all subs proved
| rest-len,
first-append,
|
| firstN-in-04 | proved | all subs proved
| firstN-in,
|
| firstN-dups-04 | proved | all subs proved
| firstN-in,
firstN-rec,
firstN-zero,
|
| rest-in-01 | proved | all subs proved
| rest-in,
|
| firstN-in-01 | proved | all subs proved
| firstN-in,
|
| sub-len-01 | proved | all subs proved
| firstn-length-04,
first-append,
restN-zero,
sublist-def,
|
| lastn-firstn-in-01 | proved | all subs proved
| firstN-lastN-in,
|
| firstN-in-02 | proved | all subs proved
| firstN-in,
|
| firstN-in-03 | proved | all subs proved
| firstN-in,
|
| lastn-firstn-in | proved | all subs proved
| firstN-lastN-in,
|
| firstN-lastN-in-01 | proved | all subs proved
| firstN-lastN-in,
lastn-restn-01,
|
| put-firstn-restn | proved | all subs proved
| first-all-01,
put-one,
firstN-len,
put-last,
put-app-right,
put-app-left,
first-append-02,
first-append,
put-succ,
firstN-zero,
put-zero,
firstN-rec-01,
elim-firstn-restn,
restN-rec,
|
| firstn-butlast-intro | proved | all subs proved
| first-append,
|
| lastn-restn | proved | all subs proved
| lastN-rec-02,
rest-rec,
lastN-zero,
restN-zero,
|
| lastn-mklist | proved | all subs proved
| lastn-mklist-03,
lastN-rec-02,
lastN-zero,
|
| sublist-append-04 | proved | all subs proved
| sublist-part,
rest-len,
restN-append,
firstN-empty,
first-append-02,
first-append,
elim-firstn-restn,
restN-rec,
firstN-rec,
first-num,
rest-rec,
firstN-zero,
restN-zero,
sublist-def,
|
| first-mklist-02 | proved | all subs proved
| first-mklist-04,
first-append,
|
| sublist-mklist | proved | all subs proved
| first-mklist,
rest-mklist-01,
sublist-def,
|
| lastn-mklist-03 | proved | all subs proved
| restN-zero,
lastn-restn-01,
lastN-all,
|
| lastN-rec-02 | proved | all subs proved
| lastN-rest,
|
| rest-in | proved | all subs proved
| elim-firstn-restn,
restN-rec,
restN-zero,
|
| firstN-in | proved | all subs proved
| elim-firstn-restn,
firstN-rec-01,
firstN-zero,
|
| firstN-lastN-in | proved | all subs proved
| firstN-lastN,
lastn-restn-01,
|
| first-append | proved | all subs proved
| firstN-len,
elim-firstn-restn,
firstN-rec,
firstN-zero,
|
| lastn-mklist-02 | proved | all subs proved
| lastN-append,
|
| del-rev-01 | proved | all subs proved
| del-rev,
|
| dups-first-last-split | proved | all subs proved
| firstn-last-eq,
|
| elim-lastn-butlastn | proved | all subs proved
| firstN-len,
blastN-firstN,
lastN-append,
lastn-length-01,
lastN-blastN,
|
| get-split-take-drop | proved | all subs proved
| firstN-len,
firstN-rec,
firstN-zero,
get-last-04,
elim-firstn-restn,
restN-rec,
|
| get-split | proved | all subs proved
| rest-len,
firstN-rec,
firstN-zero,
get-last-04,
elim-firstn-restn,
restN-rec,
firstn-length-03,
get-app,
|
| restn-less | proved | all subs proved
| restN-len,
get-last-04,
elim-firstn-restn,
get-succ,
restN-zero,
get-zero,
restN-rec,
|
| lastN-dups-01 | proved | all subs proved
| lastN-all,
lastN-dups,
|
| rmpos-take-drop | proved | all subs proved
| firstN-rec,
delpos-rec,
firstN-zero,
delpos-base,
elim-firstn-restn,
restN-rec,
|
| restn-less-2 | proved | all subs proved
| restN-len,
restN-zero,
get-last-04,
elim-firstn-restn,
restN-rec,
|
| firstn-last | proved | all subs proved
| get-last-04,
elim-firstn-restn,
get-succ,
get-zero,
firstN-zero,
firstN-rec,
|
| lastN-rest | proved | all subs proved
| restN-rec,
lastn-restn-01,
|
| rest-mklist-01 | proved | all subs proved
| rest-mklist,
|
| lastN-dups | proved | all subs proved
| restN-zero,
lastn-restn-01,
restN-rec,
|
| lastn-length-01 | proved | all subs proved
| rest-len,
lastn-restn-01,
|
| firstN-lastN | proved | all subs proved
| restN-rec,
firstN-zero,
firstN-rec-01,
restN-zero,
firstN-empty,
lastn-restn-01,
|
| firstn-last-eq | proved | all subs proved
| firstn-restn-eq,
lastn-restn-01,
|
| elim-firstn-restn | proved | all subs proved
| restN-len,
firstN-len,
firstn-length-04,
firstn-restn-eq,
|
| del-rev | proved | all subs proved
| del-one-simp-different,
in-03,
del-n,
one,
del-append,
del-y,
del-e,
|
| lastN-append | proved | all subs proved
| restN-len,
lastn-restn-01,
|
| lastN-all | proved | all subs proved
| restN-zero,
lastn-restn-01,
|
| lastn-mklist-01 | proved | all subs proved
| restN-len,
lastn-restn-01,
|
| sublist-last-01 | proved | all subs proved
| sublist-last,
|
| del-rmdup-01 | proved | all subs proved
| del-rmdup,
|
| lastN-rest-01 | proved | all subs proved
| rest-one,
lastn-restn-01,
|
| restn-size-last | proved | all subs proved
| restN-len,
restN-rec,
restN-zero,
|
| restn-prefix | proved | all subs proved
| restN-len,
|
| lastn-lastn-01 | proved | all subs proved
| lastn-rec,
lastn-length,
lastn-restn-01,
lastN-rec,
lastN-zero,
|
| sublist-at | proved | all subs proved
| get-restn,
rest-len,
get-firstn,
sublist-def,
|
| lastN-ex | proved | all subs proved
| first-length,
rest-empty,
firstrestex,
lastn-restn-01,
|
| sublist-append-01-01 | proved | all subs proved
| sublist-def,
sublist-append-01,
|
| lastN-append-01 | proved | all subs proved
| lastn-restn-01,
restn-app,
|
| sub-zero | proved | all subs proved
| sublist-all,
|
| put-sw-in | proved | all subs proved
| put-in,
get-in,
put-succ,
put-zero,
get-zero,
|
| put-del1-in | proved | all subs proved
| del1-n,
put-in-02,
put-in,
get-succ,
del1-y,
put-zero,
get-zero,
put-rec,
|
| sublist-two-num | proved | all subs proved
| sublist-def,
sublist-first-skip,
restN-zero,
|
| put-in-01 | proved | all subs proved
| del1-n,
put-in,
get-in,
get-succ,
put-zero,
get-zero,
put-rec,
del1-y,
put-in-02,
del1-e,
|
| del-rmdup-length-nle | proved | all subs proved
| in-03,
size-rmdup-del,
|
| lastn-lastn | proved | all subs proved
| lastN-rec,
restN-zero,
lastn-length,
lastn-restn-01,
lastN-rec-01,
lastN-zero,
|
| lastn-app | proved | all subs proved
| lastN-rec,
rest-empty,
lastn-restn-01,
lastn-rec,
|
| sublist-good | proved | all subs proved
| firstN-len,
restN-len,
sublist-def,
|
| size-rmdup-del | proved | all subs proved
| in-del-new,
del-n,
in-03,
del-y,
del-e,
|
| del-one-simp-different | proved | all subs proved
| del-one-simp,
|
| rest-mklist | proved | all subs proved
| rest-mklist-02,
|
| sublist-first-skip | proved | all subs proved
| rest-len,
firstn-firstn,
restn-firstn-better,
sublist-def,
|
| first-mklist-04 | proved | all subs proved
| first-all-01,
|
| put-in | proved | all subs proved
| get-succ,
put-zero,
get-zero,
put-rec,
put-in-02,
|
| sublist-all | proved | all subs proved
| first-all-01,
restN-zero,
sublist-def,
|
| sublist-part | proved | all subs proved
| restN-rec,
first-all-01,
firstN-rec,
restN-zero,
firstN-zero,
first-num,
firstN-empty,
|
| dups-def | proved | all subs proved
| get-in,
get-append-grt,
get-zero,
in-get,
get-succ,
get-nodups,
|
| sublist-append-01 | proved | all subs proved
| restn-app,
sublist-def,
|
| get-firstn | proved | all subs proved
| get-succ,
get-zero,
firstN-rec,
firstN-zero,
one-03,
firstn-one-02,
|
| lastN-blastN | proved | all subs proved
| num-lastN,
lastN-zero,
|
| first-append-02 | proved | all subs proved
| firstn-app-01,
|
| del-rmdup | proved | all subs proved
| in-del-new,
del-n,
in-03,
del-y,
del-e,
|
| sublist-last | proved | all subs proved
| get-succ,
restN-rec,
restn-apprec,
rest-rest1,
restn-first-get,
firstN-zero,
firstN-rec,
sublist-def,
|
| restN-len | proved | all subs proved
| rest-empty,
restN-append,
|
| lastn-restn-01 | proved | all subs proved
| restN-append,
lastN-rec,
rest-empty,
lastN-zero,
|
| rmdup-last | proved | all subs proved
| in-del-new,
del-n,
del-y,
del-e,
|
| in-del | proved | all subs proved
| in-del-new,
in-02,
|
| sublist-lenrec | proved | all subs proved
| get-succ,
sub-rec-01,
restN-zero,
sublist-def,
firstN-rec,
sublist-lenrec-01,
|
| firstn-prefix-02 | proved | all subs proved
| firstn-prefix,
|
| firstn-prefix-03 | proved | all subs proved
| firstn-prefix,
|
| put-butlast | proved | all subs proved
| put-app-left,
|
| firstn-prefix-04 | proved | all subs proved
| firstn-prefix,
firstN-rec,
|
| in-01 | proved | all subs proved
| in-del-new,
|
| sublist-one | proved | all subs proved
| firstN-zero,
restn-first-get,
first-num,
sublist-def,
|
| sublist-restn-02 | proved | all subs proved
| rest-len,
first-all-01,
sublist-def,
|
| dups | proved | all subs proved
| del1-in,
del1-n,
del1-y,
del1-e,
|
| sublist-append-02-01 | proved | all subs proved
| restN-zero,
sublist-def,
sublist-append-02,
|
| sw-01 | proved | all subs proved
| sw,
|
| pos-get-01 | proved | all subs proved
| pos-get,
|
| sublist-one-01 | proved | all subs proved
| firstn-one-02,
restN-zero,
sublist-num,
|
| firstn-two | proved | all subs proved
| firstn-one-02,
firstN-num-rec,
|
| rest-sub | proved | all subs proved
| restN-rec,
first-all-01,
restN-zero,
sublist-def,
|
| in | proved | all subs proved
| in-del-new,
|
| delete-dups | proved | all subs proved
| in-del-new,
del-n,
in-03,
del-y,
del-e,
|
| rmdup-del1-del | proved | all subs proved
| del1-n,
in-del-new,
del-n,
in-03,
del1-y,
del-y,
del-e,
del1-e,
|
| first-mklist-01 | proved | all subs proved
| first-mklist,
|
| first-mklist-03 | proved | all subs proved
| first-mklist,
|
| sub-len | proved | all subs proved
| firstn-length-04,
restN-zero,
sublist-def,
|
| sublist-prefix | proved | all subs proved
| restN-rec,
restn-apprec,
rest-rest1,
first-num,
firstN-zero,
firstN-rec,
sublist-def,
|
| rest-mklist-03 | proved | all subs proved
| rest-mklist-02,
|
| sublist-mklist-02 | proved | all subs proved
| first-mklist,
restN-zero,
sublist-def,
|
| restn-empty | proved | all subs proved
| rest-rec,
rest-empty,
restN-rec,
restN-zero,
|
| lastn-one-01 | proved | all subs proved
| lastn-one,
|
| lastn-one | proved | all subs proved
| lastN-zero,
lastn-rec,
|
| get-nodups | proved | all subs proved
| get-in,
get-append-grt,
get-zero,
get-numrec,
|
| rest-rest1 | proved | all subs proved
| restN-zero,
rest-rec,
|
| first-mklist | proved | all subs proved
| firstN-rec-01,
firstN-zero,
|
| rest-mklist-02 | proved | all subs proved
| rest-mklist-04,
restN-append,
|
| put-in-02 | proved | all subs proved
| put-zero,
put-rec,
|
| restn-app | proved | all subs proved
| rest-app,
|
| in-get | proved | all subs proved
| get-succ,
get-zero,
get-in,
|
| firstn-length-03 | proved | all subs proved
| first-length,
|
| del-one-simp | proved | all subs proved
| in-03,
|
| rest-append | proved | all subs proved
| restN-append,
|
| get-last-04 | proved | all subs proved
| get-last,
get-append-less,
get-numrec,
get-zero,
|
| blastN-firstN | proved | all subs proved
| firstN-rec-01,
firstN-zero,
|
| put-last | proved | all subs proved
| put-one,
put-app-right,
|
| firstn-one-02 | proved | all subs proved
| firstN-zero,
first-num,
|
| pos-get | proved | all subs proved
| get-in,
pos-n,
pos-y,
get-zero,
get-append-grt,
|
| sw | proved | all subs proved
| del-n,
del-del,
del-y,
del-e,
|
| sublist-append-02 | proved | all subs proved
| firstn-app,
restN-zero,
sublist-def,
|
| del1-in | proved | all subs proved
| in-01-01,
in-04,
|
| firstn-app-01 | proved | all subs proved
| firstn-app,
|
| restn-first-get | proved | all subs proved
| get-succ,
get-zero,
restN-zero,
rest-rec,
|
| put-app-left | proved | all subs proved
| put-succ,
put-zero,
put-rec-02,
|
| firstn-prefix | proved | all subs proved
| firstN-zero,
firstN-rec-01,
firstN-empty,
|
| sublist-lenrec-01 | proved | all subs proved
| get-succ,
firstN-rec,
get-zero,
firstN-zero,
restN-zero,
sublist-def,
sub-zerorec-01,
|
| num-lastN | proved | all subs proved
| lastN-rec-01,
|
| first-all-01 | proved | all subs proved
| first-all,
|
| firstn-length-04 | proved | all subs proved
| first-length,
|
| in-del-new | proved | all subs proved
| del-y,
del-n,
in-02,
del-e,
|
| firstn-firstn | proved | all subs proved
| firstN-rec-01,
firstN-empty,
firstN-rec,
firstN-zero,
|
| rest-empty | proved | all subs proved
| restN-all,
|
| rmpos-size | proved | all subs proved
| delpos-rec,
delpos-base,
delnr-one,
|
| sublist-restn | proved | all subs proved
| sublist-def,
restn-apprec,
|
| delete-one-le | proved | all subs proved
| delete-one-nls,
|
| len | proved | all subs proved
| len-01,
|
| firstn-butlast | proved | all subs proved
| firstN-zero,
firstN-rec-01,
firstN-rec,
firstN-empty,
|
| rmpos-get | proved | all subs proved
| get-zero,
get-append-grt,
delpos-rec,
delpos-base,
get-succ,
|
| restn-at | proved | all subs proved
| get-restn,
|
| firstn-allprefix | proved | all subs proved
| firstN-len,
|
| delpos-in | proved | all subs proved
| rmpos-not-in,
|
| firstn-twice | proved | all subs proved
| firstN-rec,
firstN-rec-01,
firstN-zero,
|
| get-last-nonempty | proved | all subs proved
| get-last2,
|
| sub-zerozero | proved | all subs proved
| firstN-zero,
restN-zero,
sublist-num,
|
| in-05 | proved | all subs proved
| in-04,
|
| rev-get | proved | all subs proved
| one-03,
get-butlast,
get-append-grt,
get-zero,
get-append-less,
|
| st | proved | all subs proved
| sw-02,
|
| firstn-append-01 | proved | all subs proved
| firstN-zero,
firstN-rec-01,
firstN-rec,
firstN-empty,
|
| sublist-restn-01 | proved | all subs proved
| sublist-def,
restn-apprec,
|
| firstn-first | proved | all subs proved
| firstN-rec-01,
firstN-empty,
|
| rmpos-in | proved | all subs proved
| delpos-get-fw,
rmpos-not-in,
get-in,
delpos-rec,
delpos-base,
get-zero,
get-append-grt,
one-03,
delnr-one,
delpos-empty,
|
| size-del-nodups | proved | all subs proved
| del-n,
in-03,
del-y,
del-e,
|
| sublist-length-02 | proved | all subs proved
| first-length,
sublist-def,
|
| sublist-length-03 | proved | all subs proved
| first-length,
sublist-def,
|
| sublist-length-01 | proved | all subs proved
| first-length,
restN-zero,
sublist-def,
|
| firstn-length-02 | proved | all subs proved
| first-length,
|
| restn-nonempty-2 | proved | all subs proved
| restN-zero,
rest-rec,
|
| firstn-length-01 | proved | all subs proved
| first-length,
|
| restN-dups | proved | all subs proved
| rest-rec,
restN-zero,
|
| put-one-01 | proved | all subs proved
| put-one,
put-rec,
|
| firstn-one | proved | all subs proved
| firstN-zero,
firstN-num-rec,
|
| inl-01 | proved | all subs proved
| inl,
pos-n,
pos-y,
|
| sublist-length | proved | all subs proved
| first-length,
sublist-def,
|
| firstn-length | proved | all subs proved
| first-length,
|
| get-last-03 | proved | all subs proved
| get-last,
|
| rest-two | proved | all subs proved
| rest-one,
rest-rec,
|
| nodups-rmposnodups | proved | all subs proved
| rmpos-not-in,
delpos-rec,
delpos-base,
delpos-empty,
|
| del1-empty | proved | all subs proved
| del1-n,
del1-y,
one-01,
|
| firstn-append | proved | all subs proved
| firstN-zero,
firstN-empty,
firstN-rec,
|
| firstn-app-02 | proved | all subs proved
| firstn-app,
|
| firstn-app-exact | proved | all subs proved
| firstN-len,
|
| l-02 | proved | all subs proved
| l,
del1-n,
del1-y,
del1-e,
in-02-01,
|
| sublist-empty | proved | all subs proved
| sub-zerolen,
firstN-empty,
sublist-def,
|
| l-01 | proved | all subs proved
| in-02-01,
l,
|
| sublist-append-03 | proved | all subs proved
| firstN-len,
restN-zero,
sublist-def,
|
| restn-restn | proved | all subs proved
| restn-apprec,
|
| restn-nonempty | proved | all subs proved
| rest-rec,
restN-zero,
|
| firstn-one-01 | proved | all subs proved
| firstN-zero,
first-num,
|
| get-append-grt-02 | proved | all subs proved
| get-append-grt,
|
| del-del1-nodups | proved | all subs proved
| del1-n,
del-n,
del1-y,
in-03,
del-y,
del1-e,
del-e,
|
| possize-notin | proved | all subs proved
| pos-equal,
pos-n,
pos-y,
pos-e,
notin-03,
|
| sublist-recstart | proved | all subs proved
| restN-rec,
get-succ,
restN-zero,
get-zero,
sublist-def,
sub-rec-01,
firstN-rec,
|
| lastn-neq-02 | proved | all subs proved
| lastn-length,
lastN-rec,
|
| sublist-firsteq | proved | all subs proved
| firstN-rec,
firstN-zero,
restN-zero,
sublist-def,
first-length,
|
| get-in1 | proved | all subs proved
| get-in,
|
| firstn-last-01 | proved | all subs proved
| firstN-zero,
firstN-rec,
firstN-empty,
|
| restn-last | proved | all subs proved
| rest-rec,
restN-zero,
|
| dups-01 | proved | all subs proved
| del1-n,
del1-y,
del1-e,
in-01-01,
|
| rest-two-01 | proved | all subs proved
| rest-one-01,
rest-rec,
|
| rest-one-01 | proved | all subs proved
| restN-zero,
restN-rec,
|
| del-append | proved | all subs proved
| del-n,
del-y,
del-e,
|
| one | proved | all subs proved
| del-e,
del-y,
|
| rest-mklist-04 | proved | all subs proved
| restN-rec,
restN-zero,
|
| notin-03 | proved | all subs proved
| pos-n,
pos-e,
|
| pos-equal | proved | all subs proved
| pos-n,
pos-y,
pos-e,
|
| first-all | proved | all subs proved
| firstN-rec,
firstN-zero,
|
| put-rec-02 | proved | all subs proved
| put-succ,
|
| rest-app | proved | all subs proved
| restN-rec,
|
| lastN-rec-01 | proved | all subs proved
| lastN-rec,
|
| sub-zerolen | proved | all subs proved
| firstN-zero,
sublist-def,
|
| in-02-01 | proved | all subs proved
| del1-n,
del1-e,
|
| l | proved | all subs proved
| del1-n,
del1-y,
del1-e,
|
| firstn-app | proved | all subs proved
| firstN-rec,
|
| one-01 | proved | all subs proved
| del1-y,
|
| get-app | proved | all subs proved
| get-succ,
get-zero,
|
| get-numrec | proved | all subs proved
| get-succ,
|
| get-last | proved | all subs proved
| get-succ,
one-03,
|
| firstrestex | proved | all subs proved
| restN-rec,
firstN-rec,
restN-zero,
firstN-zero,
|
| inl | proved | all subs proved
| pos-n,
pos-y,
|
| put-rec | proved | all subs proved
| put-succ,
|
| restN-all | proved | all subs proved
| restN-rec,
restN-zero,
|
| lastn-length | proved | all subs proved
| lastN-rec,
lastN-zero,
|
| lastn-rec | proved | all subs proved
| lastN-rec,
|
| firstN-num-rec | proved | all subs proved
| firstN-rec,
|
| in-01-01 | proved | all subs proved
| del1-n,
del1-y,
del1-e,
|
| rest-rec | proved | all subs proved
| restN-rec,
|
| put-app-right | proved | all subs proved
| put-succ,
|
| put-one | proved | all subs proved
| put-zero,
|
| first-length | proved | all subs proved
| firstN-rec,
firstN-zero,
|
| get-in | proved | all subs proved
| get-zero,
|
| delpos-get-fw | proved | all subs proved
| delpos-base,
delpos-rec,
get-succ,
get-zero,
|
| del-del | proved | all subs proved
| del-n,
del-y,
del-e,
|
| sw-02 | proved | all subs proved
| del1-y,
del1-n,
del1-e,
|
| firstn-restn-eq | proved | all subs proved
| restN-rec,
firstN-rec,
restN-zero,
firstN-zero,
|
| get-append-less | proved | all subs proved
| get-succ,
get-zero,
|
| get-butlast | proved | all subs proved
| get-succ,
one-03,
get-zero,
|
| in-04 | proved | all subs proved
| del1-y,
del1-n,
|
| sublist-num | proved | all subs proved
| sublist-def,
|
| sub-rec-01 | proved | all subs proved
| sublist-def,
restN-rec,
|
| get-last2 | proved | all subs proved
| get-succ,
one-03,
|
| in-03 | proved | all subs proved
| del-n,
del-e,
|
| rest-one | proved | all subs proved
| restN-zero,
restN-rec,
|
| first-num | proved | all subs proved
| firstN-rec,
|
| in-02 | proved | all subs proved
| del-n,
del-y,
del-e,
|
| rmpos-not-in | proved | all subs proved
| delpos-rec,
delpos-base,
delpos-empty,
|
| firstN-len | proved | all subs proved
| firstN-rec,
firstN-zero,
|
| get-restn | proved | all subs proved
| get-succ,
restN-rec,
restN-zero,
|
| get-append-grt | proved | all subs proved
| get-succ,
|
| firstN-empty | proved | all subs proved
| firstN-rec,
firstN-zero,
|
| firstN-rec-01 | proved | all subs proved
| firstN-rec,
|
| len-01 | proved | all subs proved
| pos-n,
pos-y,
pos-e,
|
| delete-one-nls | proved | all subs proved
| del1-n,
del1-y,
del1-e,
|
| restn-apprec | proved | all subs proved
| restN-rec,
restN-zero,
|
| delnr-one | proved | all subs proved
| delpos-base,
|
| restn-firstn-better | proved | all subs proved
| restN-rec,
firstN-rec,
restN-zero,
|
| rest-len | proved | all subs proved
| restN-rec,
restN-zero,
|
| sub-zerorec-01 | proved | all subs proved
| restN-zero,
sublist-def,
firstN-rec,
|
| restN-append | proved | all subs proved
| restN-rec,
restN-zero,
|
| rmtoobigpos | proved | all subs proved
| delpos-rec,
delpos-base,
delpos-empty,
|
| from-rest | proved | all subs proved
| restN-rec,
pos-n,
fromE-no,
pos-y,
fromE-yes,
restN-zero,
pos-e,
fromE-empty,
|
| app | proved | all subs proved
| del1-n,
del1-y,
del1-e,
|
| from-notin | proved | all subs proved
| fromE-no,
fromE-empty,
|
| at-last | proved | all subs proved
| one-03,
|
| restn-rest | proved | all subs proved
| restN-zero,
restN-rec,
|
| lastN-empty | proved | all subs proved
| lastN-rec,
lastN-zero,
|
| firstn-restn | proved | all subs proved
| sublist-def,
|
| first-sub | proved | all subs proved
| restN-zero,
sublist-def,
|
| sublist-rec-01 | proved | all subs proved
| firstN-rec,
restN-zero,
sublist-def,
|
| del1-del | proved | all subs proved
| del-n,
del1-n,
del-y,
del1-y,
del-e,
del1-e,
|
| weak-firstN-rec | proved | all subs proved
| firstN-rec,
|
| map-get | proved | all subs proved
| get-succ,
get-zero,
one-03,
|
| get-mklist | proved | all subs proved
| get-mklist-01,
one-03,
|
| firstn-last-rec | proved | all subs proved
| get-succ,
firstN-zero,
firstN-rec,
|
| app-01 | proved | all subs proved
| del1-n,
|
| app-05 | proved | all subs proved
| pos-n,
pos-y,
pos-e,
|
| get-last-01 | proved | all subs proved
| get-succ,
one-03,
|
| del-del1-switch | proved | all subs proved
| del-y,
del1-n,
del1-y,
del-n,
del1-e,
del-e,
|
| get-add-num | proved | all subs proved
| get-succ,
|
| del1-first | proved | all subs proved
| del1-y,
|
| list-select-not-first | proved | all subs proved
| get-succ,
|
| sub-rec | proved | all subs proved
| sublist-def,
restN-rec,
|
| del1-del-switch | proved | all subs proved
| del1-y,
del-n,
del-y,
del1-n,
del-e,
del1-e,
|
| put-zero-01 | proved | all subs proved
| put-zero,
|
| restn-firstn | proved | all subs proved
| restN-rec,
firstN-rec,
restN-zero,
|
| get | proved | all subs proved
| get-succ,
pos-n,
get-zero,
pos-y,
pos-e,
|
| app-05-neg | proved | all subs proved
| pos-n,
|
| weak-restN-rec | proved | all subs proved
| restN-rec,
|
| sublist-rec | proved | all subs proved
| firstN-rec,
restN-zero,
sublist-def,
|
| append-mod | proved | all subs proved
| put-succ,
|
| delpos-append-size-lt | proved | all subs proved
| delpos-rec,
delpos-base,
|
| sublist-num-01 | proved | all subs proved
| firstN-rec,
restN-zero,
sublist-def,
|
| del-length | proved | all subs proved
| del-n,
del-y,
del-e,
|
| pos-one | proved | all subs proved
| pos-y,
|
| one-01-01 | proved | all subs proved
| del1-e,
del1-n,
|
| delpos-atsizeid | proved | all subs proved
| delpos-rec,
delpos-empty,
|
| del-n-simp | proved | all subs proved
| del-n,
|
| sub-zerorec | proved | all subs proved
| restN-zero,
sublist-def,
firstN-rec,
|
| get-mklist-01 | proved | all subs proved
| |
| put-zero | proved | all subs proved
| |
| one-03 | proved | all subs proved
| |
| del1-e | axiom | | |
| del1-y | axiom | | |
| del1-n | axiom | | |
| fromE-empty | axiom | | |
| pos-e | axiom | | |
| fromE-yes | axiom | | |
| pos-y | axiom | | |
| fromE-no | axiom | | |
| pos-n | axiom | | |
| restN-rec | axiom | | |
| del-e | axiom | | |
| del-y | axiom | | |
| del-n | axiom | | |
| put-succ | proved | all subs proved
| |
| delpos-empty | axiom | | |
| delpos-base | axiom | | |
| delpos-rec | axiom | | |
| sublist-def | axiom | | |
| restN-zero | axiom | | |
| firstN-zero | axiom | | |
| get-zero | proved | all subs proved
| |
| firstN-rec | axiom | | |
| get-succ | proved | all subs proved
| |
| lastN-zero | axiom | | |
| lastN-rec | axiom | | |