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: |
|---|
| nonnullrefs-dups-firstoc | proved | all subs proved
| nonnullrefs-one,
nonnullrefs-append,
nonnullrefs-in-firstoc,
nonnullrefs-yes,
nonnullrefs-no,
nonnullrefs-empty,
|
| nonnullrefs-in-firstoc | proved | all subs proved
| nonnullrefs-one-yes,
nonnullrefs-one-no,
nonnullrefs-empty,
nonnullrefs-one,
nonnullrefs-append,
|
| nonnullrefs-null | proved | all subs proved
| nonnullrefs-one-yes,
nonnullrefs-one-no,
nonnullrefs-append,
nonnullrefs-empty,
|
| nonnullrefs-one-yes | proved | all subs proved
| nonnullrefs-one,
|
| javavalues-is-bytevalue | proved | all subs proved
| is_bytes-vals,
isbytelist-all,
|
| nonnullrefs-one | proved | all subs proved
| nonnullrefs-append,
nonnullrefs-yes,
|
| is_bytes-vals | proved | all subs proved
| is_bytelist,
mkvalsb-rec,
is_bytelist-empty,
mkvalsb-empty,
|
| bytevalues-eq | proved | all subs proved
| bytevalues-rec,
bytevalues-empty-01,
bytevalues-empty,
|
| ints2bytes-butlast | proved | all subs proved
| ints2bytes-empty-01,
ints2bytes-empty,
ints2bytes-rec,
|
| intvalues-mklist | proved | all subs proved
| intvalues-one,
intvalues-append,
intvalues-empty,
|
| mkjavavalues-byte-lastrec | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
mkvals-single,
|
| mkjavavalues-byte-lastrec-01 | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
mkvals-single,
|
| mkvalues-butlast | proved | all subs proved
| mkjava-empty,
mkvalsb-empty,
mkvalsb-rec,
|
| mkvalues-last | proved | all subs proved
| mkjava-empty,
mkvalsb-empty,
mkvalsb-rec,
|
| nonnullrefs-dups | proved | all subs proved
| nonnullrefs-in,
nonnullrefs-yes,
nonnullrefs-no,
nonnullrefs-empty,
|
| bytevalues-empty-01 | proved | all subs proved
| bytevalues-rec,
bytevalues-empty,
|
| ints2bytes-empty-01 | proved | all subs proved
| ints2bytes-rec,
ints2bytes-empty,
|
| intvalues-one | proved | all subs proved
| intvalues-empty,
intvalues-rec,
|
| intvalues-append | proved | all subs proved
| intvalues-rec,
intvalues-empty,
|
| is_bytelist | proved | all subs proved
| is_bytelist-rec,
|
| isbytelist-all | proved | all subs proved
| is_bytelist-rec,
is_bytelist-empty,
|
| mkvals-single | proved | all subs proved
| mkvalsb-empty,
mkvalsb-rec,
|
| mkjava-empty | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
|
| nonnullrefs-in | proved | all subs proved
| nonnullrefs-yes,
nonnullrefs-no,
nonnullrefs-empty,
|
| nonnullrefs-one-no | proved | all subs proved
| nonnullrefs-empty,
nonnullrefs-no,
|
| nonnullrefs-append | proved | all subs proved
| nonnullrefs-yes,
nonnullrefs-no,
nonnullrefs-empty,
|
| vals2val-single | proved | all subs proved
| vals2val-empty,
vals2val-rec,
|
| vals2ints-len | proved | all subs proved
| vals2ints-rec,
vals2ints-empty,
|
| vals2ints-empty-01 | proved | all subs proved
| vals2ints-rec,
vals2ints-empty,
|
| vals2int-one | proved | all subs proved
| vals2ints-empty,
vals2ints-rec,
|
| vals-at | proved | all subs proved
| mkvalsb-rec,
|
| val-inj-01 | proved | all subs proved
| vals-rec,
vals2val-rec,
vals-empty,
vals2val-empty,
|
| posints-rec-02 | proved | all subs proved
| posints-rec,
|
| posints-rec-01 | proved | all subs proved
| posints-rec,
|
| posints-one | proved | all subs proved
| posints-empty,
posints-rec,
|
| nonnullrefs-ok | proved | all subs proved
| nonnullrefs-yes,
|
| mkvalsr-one | proved | all subs proved
| mkvalsr-empty,
mkvalsr-rec,
|
| mkvalsr-len | proved | all subs proved
| mkvalsr-rec,
mkvalsr-empty,
|
| mkvalsr-at | proved | all subs proved
| mkvalsr-rec,
mkvalsr-empty,
|
| mkjavavalues-restn | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
|
| mkjavavalues-rec | proved | all subs proved
| mkvalsr-rec,
|
| mkjavavalues-empty | proved | all subs proved
| mkvalsr-rec,
mkvalsr-empty,
|
| mkjavavalues-append-01 | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
|
| mkjavavalues-append | proved | all subs proved
| mkvalsr-rec,
mkvalsr-empty,
|
| mkjavavalues | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
|
| mkjava-len | proved | all subs proved
| mkvalsb-rec,
mkvalsb-empty,
|
| mkjava-bvs | proved | all subs proved
| bytevalues-rec,
mkvalsb-rec,
bytevalues-empty,
mkvalsb-empty,
|
| javavalues-in | proved | all subs proved
| mkvalsr-rec,
mkvalsr-empty,
|
| is_bytelist-one | proved | all subs proved
| is_bytelist-empty,
is_bytelist-rec,
|
| intvalues-put-sw | proved | all subs proved
| intvalues-rec,
intvalues-empty,
|
| intvalues-len | proved | all subs proved
| intvalues-rec,
intvalues-empty,
|
| intvalues-empty-01 | proved | all subs proved
| intvalues-rec,
intvalues-empty,
|
| intvalues-at | proved | all subs proved
| intvalues-rec,
intvalues-empty,
|
| ints2bytes-one | proved | all subs proved
| ints2bytes-empty,
ints2bytes-rec,
|
| ints2bytes-len | proved | all subs proved
| ints2bytes-rec,
ints2bytes-empty,
|
| ints2bytes-at | proved | all subs proved
| ints2bytes-rec,
|
| ibbis | proved | all subs proved
| ints2bytes-rec,
bytes2ints-rec,
ints2bytes-empty,
bytes2ints-empty,
|
| bytevalues-one | proved | all subs proved
| bytevalues-empty,
bytevalues-rec,
|
| bytevalues-len | proved | all subs proved
| bytevalues-rec,
bytevalues-empty,
|
| bytevals-inj | proved | all subs proved
| is_bytelist-rec,
mkvalsb-rec,
bytevalues-rec,
mkvalsb-empty,
bytevalues-empty,
|
| bytevals-at | proved | all subs proved
| bytevalues-rec,
bytevalues-empty,
|
| bytes2ints-one | proved | all subs proved
| bytes2ints-empty,
bytes2ints-rec,
|
| vals2ints-rec | axiom | | |
| vals2ints-empty | axiom | | |
| vals2val-empty | axiom | | |
| vals-empty | axiom | | |
| vals2val-rec | axiom | | |
| vals-rec | axiom | | |
| posints-rec | axiom | | |
| posints-empty | axiom | | |
| nonnullrefs-empty | axiom | | |
| nonnullrefs-no | axiom | | |
| nonnullrefs-yes | axiom | | |
| mkvalsr-empty | axiom | | |
| mkvalsr-rec | axiom | | |
| is_bytelist-empty | axiom | | |
| intvalues-empty | axiom | | |
| intvalues-rec | axiom | | |
| ints2bytes-empty | axiom | | |
| ints2bytes-rec | axiom | | |
| mkvalsb-empty | axiom | | |
| mkvalsb-rec | axiom | | |
| is_bytelist-rec | axiom | | |
| bytevalues-empty | axiom | | |
| bytevalues-rec | axiom | | |
| bytes2ints-rec | axiom | | |
| bytes2ints-empty | axiom | | |