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: |
|---|
| getbar-putbar-01 | proved | all subs proved
| getbar-putbar-same-01,
putByteArray-all,
getByteArray-all,
putbar-len,
|
| getbar-putbar-same-01 | proved | all subs proved
| getbar-put-lower,
putBar-rec,
getbar-rec,
bar-empty-01,
putBar-empty,
|
| putbar-getbar-le | proved | all subs proved
| getbar-put-lower,
getbar-rec,
putBar-rec,
bar-empty-01,
putBar-empty,
|
| getintarray-put-upper-02 | proved | all subs proved
| getintarray-put-upper,
|
| getintarray-put-upper-01 | proved | all subs proved
| getintarray-put-upper,
|
| getintarray-put-other-03 | proved | all subs proved
| getintarray-put-upper,
getintarray-put-lower,
|
| getintarray-put-other-02 | proved | all subs proved
| getintarray-put-upper,
getintarray-put-lower,
getintarray-def,
|
| getbar-put | proved | all subs proved
| getbar-put-other,
getbar-put-lower,
get-put-01,
getbar-ref,
|
| getintarray-put-upper | proved | all subs proved
| getarray-put-05,
getintarray,
|
| getbar-put-lower | proved | all subs proved
| getbar-put-other,
|
| getbar-put-02 | proved | all subs proved
| getbar-put-other,
|
| getbar-putbar-same | proved | all subs proved
| putbar-getbar,
putBar-at-len,
putByteArray-all,
getByteArray-all,
|
| getbyte-putbyte | proved | all subs proved
| putbar-getbar,
putBar-at-len,
getByteArray-all,
|
| getbar-put-other | proved | all subs proved
| getarray-put-01,
getarray-put,
getarray-put-02,
getByteArray,
|
| putbar-len | proved | all subs proved
| putbar-len-01,
putByteArray-all,
|
| putbar-getbar | proved | all subs proved
| putar-getar,
putByteArray,
getByteArray,
|
| getintarray-put-lower | proved | all subs proved
| getarray-put,
getintarray,
|
| getarray-put-05 | proved | all subs proved
| getarray-put-01,
getarray-put,
getarray-put-02,
|
| sublist-getbar | proved | all subs proved
| bar-sublist,
getByteArray-all,
|
| getbar-union-02 | proved | all subs proved
| getbar-union-03,
|
| getbar-union | proved | all subs proved
| getbar-union-01,
|
| bar-firstn | proved | all subs proved
| bar-sublist,
|
| bar-eq-sub | proved | all subs proved
| bar-neq-soffset,
|
| putbar-len-01 | proved | all subs proved
| putBar-at-len,
|
| putar-getar | proved | all subs proved
| getarray-put-01,
getarray-offset-02,
putar-at,
getArray-one,
getArray-rec,
putArray-rec,
get-zero,
putArray-empty,
|
| getbar-union-03 | proved | all subs proved
| getarray-union,
getByteArray,
|
| getbar-union-01 | proved | all subs proved
| getarray-union,
getByteArray,
getByteArray-all,
|
| getarray-put | proved | all subs proved
| getarray-put-01,
|
| bar-sublist | proved | all subs proved
| bar-len-03,
getbar-anyrec,
|
| bar-neq-soffset | proved | all subs proved
| bar-neq-same,
bar-len-02,
bar-empty,
getbar-anyrec,
|
| getarray-put=set | proved | all subs proved
| getarray-put-01,
get-length,
get-zero,
getArray-one,
getArray-rec,
|
| getbar-appeq-01 | proved | all subs proved
| getbar-appeq,
|
| getbar-length-01 | proved | all subs proved
| getbar-len-02,
|
| getbar-restn-01 | proved | all subs proved
| bar-len-03,
getbar-anyrec,
getByteArray-all,
|
| getbytearray-put-index-length | proved | all subs proved
| getbar-len-03,
bar-zero,
getbar-len-01,
bar-length,
|
| getbytearray-putbar-length | proved | all subs proved
| get-length-02,
get-length-01,
getByteArray,
putBar-at-len,
getByteArray-all,
|
| putBar-lastrec | proved | all subs proved
| putBar-rec,
putBar-empty,
putBar-one,
putBar-rew,
|
| putbar-put-mode | proved | all subs proved
| putBar-at-mode,
putByteArray-all,
|
| bar-neq-same | proved | all subs proved
| bar-neq,
|
| getbar-appeq | proved | all subs proved
| bar-len-02,
|
| getbar-len-02 | proved | all subs proved
| bar-len-02,
|
| bar-len-03 | proved | all subs proved
| bar-len-02,
|
| getarray-union | proved | all subs proved
| getArray-zero,
getarray-offset-02,
|
| getbar-len-03 | proved | all subs proved
| getbar-len-01,
bar-length,
|
| putBar-rew | proved | all subs proved
| putBar-at-fskey,
putBar-at,
putbar-atref-01,
putbar-byte,
putbar-atother-01,
putBar-in,
|
| getarray-put-01 | proved | all subs proved
| getarray-offset-02,
getArray-zero,
get-rec-01,
|
| putBar-at-len | proved | all subs proved
| putBar-at-fskey,
|
| putBar-at-mode | proved | all subs proved
| putBar-at-fskey,
|
| putbytearray-subset-new | proved | all subs proved
| putbytearray-subset-new-01,
putByteArray-all,
|
| putbar-override | proved | all subs proved
| putbar-put-override,
putBar-rec,
putBar-empty,
|
| putBar-at-type | proved | all subs proved
| putBar-at-fskey,
|
| getintarray-zero | proved | all subs proved
| getintarray-empty-02,
getintarray-def,
|
| getintarray-max-rec-01 | proved | all subs proved
| getintarray-empty-02,
getintarray-rec-last,
|
| getintarray-max-rec | proved | all subs proved
| getintarray-empty-02,
getintarray-rec-last,
|
| getintarray-length-01 | proved | all subs proved
| getintarray-length,
getintarray-def,
|
| getintarray-at | proved | all subs proved
| get-get,
get-length,
getintarray,
getintarray-empty-02,
|
| getbytearray-subset | proved | all subs proved
| bar-at,
bar-empty,
bar-len-02,
is_arrayref,
|
| getbytearray-one | proved | all subs proved
| getbar-one,
getByteArray-all,
|
| getbytearray-length-zero | proved | all subs proved
| bar-zero,
|
| getbar-restn-04 | proved | all subs proved
| bar-restn,
bar-len-02,
|
| getbar-restn-02 | proved | all subs proved
| bar-len-02,
bar-restn,
getByteArray-all,
|
| getbar-restn | proved | all subs proved
| getbar-len-01,
bar-length,
|
| getbar-mod | proved | all subs proved
| getbar-mod-01,
getByteArray-all,
|
| getbar-length | proved | all subs proved
| getbar-len-01,
bar-length,
|
| getbar-5rec | proved | all subs proved
| getarray-offset-02,
getByteArray,
|
| getbar-3rec | proved | all subs proved
| getarray-offset-02,
getByteArray,
|
| getbar-2rec | proved | all subs proved
| getarray-offset-02,
getByteArray,
|
| getba-neq | proved | all subs proved
| getba-neq-01,
getByteArray-all,
|
| getarray-in | proved | all subs proved
| get-empty,
getArray-all,
getarray-length,
getarray-get,
|
| comp-copy | proved | all subs proved
| copy-between,
copy-at,
get-alleq,
Comp-get-02,
|
| arrayComp-08 | proved | all subs proved
| get-alleq,
Comp-get-02,
|
| arrayComp-05 | proved | all subs proved
| get-alleq,
Comp-get-02,
|
| putbytearray-subset-new-01 | proved | all subs proved
| putarray-subset-new-01,
putByteArray,
|
| putbar-put-override | proved | all subs proved
| putByteArray-put-switch-01,
putBar-empty,
putBar-rec,
|
| putbar-byte | proved | all subs proved
| putar-at,
putByteArray,
|
| putBar-at-fskey | proved | all subs proved
| putBar-at,
putbar-atref-01,
|
| getintarray-length | proved | all subs proved
| get-length-01,
getintarray,
|
| getintarray-empty-02 | proved | all subs proved
| getintarray-empty,
getintarray-empty-01,
getintarray-rec-first,
|
| getbar-one | proved | all subs proved
| bar-empty-01,
getbar-rec,
|
| bar-zero | proved | all subs proved
| bar-empty-01,
bar-empty,
getbar-rec,
getByteArray-all,
|
| getbar-mod-01 | proved | all subs proved
| extension,
|
| bar-length | proved | all subs proved
| get-length-01,
getByteArray,
getByteArray-all,
|
| getba-neq-01 | proved | all subs proved
| bar-empty-01,
getbar-rec,
|
| getarray-offset-02 | proved | all subs proved
| getArray-one,
getarray-offset,
|
| getarray-length | proved | all subs proved
| get-length-01,
getArray-all,
|
| getbar-anyrec | proved | all subs proved
| bytevalues,
getarray-offset,
getByteArray,
|
| bar-neq | proved | all subs proved
| get-length-01,
bytevalues,
getarray-offset,
getByteArray,
|
| bar-len-02 | proved | all subs proved
| get-length-01,
getByteArray,
|
| Comp-get-02 | proved | all subs proved
| Comp-get,
arrayComp,
Comp-get-01,
|
| bar-at-01 | proved | all subs proved
| bar-at,
getByteArray-all,
|
| copy-succ | proved | all subs proved
| copy-in-upper,
copy-in-upper-01,
copy-in-lower,
copy-in-between,
copy-in,
copy-upper,
copy-lower,
copy-between,
copy-at,
copy-upper-01,
copy-infs,
copy-atfield,
arrayCopy-rec,
|
| extension-01 | proved | all subs proved
| extension,
getByteArray-all,
|
| get-eqex | proved | all subs proved
| get-eqex-01,
|
| get-sublist | proved | all subs proved
| get-rec-01,
get-rest,
get-first,
get-empty,
get-zero,
|
| getByteArray-put-01 | proved | all subs proved
| getByteArray-put,
|
| getar-putbar | proved | all subs proved
| getar-putbar-01,
putBar-empty,
putByteArray-all,
|
| getarray-length-01 | proved | all subs proved
| get-length-01,
|
| getarray-offset-01 | proved | all subs proved
| getArray-zero,
getArray-one,
getarray-offset,
|
| getarray-put-07 | proved | all subs proved
| getarray-put-06,
getarray-put-other,
|
| getarray-union-01 | proved | all subs proved
| getarray-union-02,
|
| getba-eq | proved | all subs proved
| bar-empty,
bar-empty-01,
getbar-rec,
|
| getbar-len | proved | all subs proved
| get-length-01,
getByteArray,
getByteArray-all,
|
| getbar-mode | proved | all subs proved
| get-put-02,
|
| getbar-put-03 | proved | all subs proved
| getbar-put-01,
|
| getbar-put-04 | proved | all subs proved
| get-put-02,
|
| getbar-putbar | proved | all subs proved
| putbar-getbar-03,
putBar-empty,
putByteArray-all,
|
| getbytearray-put | proved | all subs proved
| get-put,
getByteArray-put,
|
| getintarray-in-01 | proved | all subs proved
| getintarray-in,
|
| getintarray-in-02 | proved | all subs proved
| getintarray-empty,
getintarray-empty-01,
getintarray-rec-last,
|
| getintarray-one | proved | all subs proved
| getintarray-empty,
getintarray-rec-last,
|
| getintarray-subset | proved | all subs proved
| getintarray-subset-01,
getintarray-def,
is_arrayref,
|
| putArray-at-in | proved | all subs proved
| putar-at,
|
| putarray-length | proved | all subs proved
| putarray-field,
|
| putarray-mode | proved | all subs proved
| putarray-field,
|
| putarray-subset-new | proved | all subs proved
| putarray-subset-new-01,
putArray-all,
|
| putarray-type | proved | all subs proved
| putarray-field,
|
| putbytearray-in | proved | all subs proved
| putBar-in,
|
| Comp-get | proved | all subs proved
| get-get,
arrayComp,
|
| copy-in-lower | proved | all subs proved
| copy-in-between,
arrayCopy-base,
arrayCopy-rec,
|
| copy-lower | proved | all subs proved
| copy-between,
arrayCopy-base,
arrayCopy-rec,
|
| get-eqex-01 | proved | all subs proved
| get-del,
|
| get-first | proved | all subs proved
| get-zero,
get-empty,
getArray-one,
getArray-rec,
|
| getar-putbar-01 | proved | all subs proved
| getarray-put-other,
putBar-rec,
putBar-empty,
|
| getarray-get | proved | all subs proved
| get-get,
get-length,
get-empty,
getArray-all,
|
| getarray-put-06 | proved | all subs proved
| getarray-put-03,
getArray-all,
getarray-put-other,
|
| getarray-union-02 | proved | all subs proved
| getarray-union-03,
|
| getarray-offset | proved | all subs proved
| get-empty,
get-zero,
getArray-one,
getArray-zero,
getArray-rec,
|
| extension | proved | all subs proved
| get-zero,
get-empty,
getArray-zero,
get-rec-01,
getByteArray,
|
| getbar-put-01 | proved | all subs proved
| get-put,
|
| get-put-02 | proved | all subs proved
| get-put,
|
| putbar-getbar-03 | proved | all subs proved
| putar-getar-02,
getByteArray,
putar-atref,
getByteArray-all,
putByteArray,
|
| getByteArray-put | proved | all subs proved
| getbar-ref,
getByteArray-all,
|
| bar-at | proved | all subs proved
| get-get,
get-length,
getByteArray,
|
| getintarray-in | proved | all subs proved
| get-get,
get-length,
get-empty,
getintarray,
getintarray-def,
|
| get-length-01 | proved | all subs proved
| get-zero,
get-length,
|
| getintarray-empty | proved | all subs proved
| get-zero,
getintarray,
|
| getintarray-rec-last | proved | all subs proved
| get-zero,
getArray-one,
getArray-rec,
getintarray,
|
| getintarray-subset-01 | proved | all subs proved
| getarray-subset,
getintarray,
is_arrayref,
|
| putBar-at | proved | all subs proved
| putArray-at,
putByteArray,
|
| putbar-atother-01 | proved | all subs proved
| putar-atother,
putByteArray,
|
| putarray-field | proved | all subs proved
| putar-atref,
putArray-at,
putArray-rec,
putArray-empty,
|
| putar-at | proved | all subs proved
| putar-atother,
putArray-rec,
putArray-empty,
|
| bar-empty-01 | proved | all subs proved
| get-zero,
getByteArray,
|
| putByteArray-put-switch-01 | proved | all subs proved
| putByteArray-put-switch,
putBar-rec,
|
| putBar-in | proved | all subs proved
| putArray-in,
putByteArray,
|
| putarray-subset-new-01 | proved | all subs proved
| putArray-in,
putar-inref,
putar-atref,
|
| stsub-copy | proved | all subs proved
| copy-in-01,
copy-in,
copy-at,
|
| putbytearray-init | proved | all subs proved
| pubBar-init,
|
| putbar-inref-01 | proved | all subs proved
| putbar-inref,
putByteArray-all,
|
| putbar-inother-01 | proved | all subs proved
| putar-inother,
putByteArray,
putByteArray-all,
|
| putbar-inother | proved | all subs proved
| putar-inother,
putByteArray,
|
| putbar-infs-01 | proved | all subs proved
| putbar-infs,
putByteArray-all,
|
| putbar-getbar-02 | proved | all subs proved
| putar-getar-02,
putByteArray,
getByteArray,
|
| putbar-getbar-01 | proved | all subs proved
| putar-getar-01,
putByteArray,
getByteArray,
|
| putbar-atother | proved | all subs proved
| putar-atother,
putByteArray,
putByteArray-all,
|
| putByteArray-append | proved | all subs proved
| putByteArray-put-switch,
putBar-rec,
putBar-empty,
|
| putArray-put | proved | all subs proved
| putArray-put-switch,
putAr-lastrec,
putArray-rec,
putArray-one,
putArray-empty,
|
| isarrayref-putbar-other | proved | all subs proved
| putbar-inref,
is_arrayref,
|
| getintarray-put-other-01 | proved | all subs proved
| getintarray-put-other,
getintarray-def,
|
| getbar-restn-03 | proved | all subs proved
| bar-restn,
getByteArray-all,
|
| getbar-lastrec | proved | all subs proved
| bytevalues,
get-zero,
getArray-one,
getArray-rec,
getByteArray,
|
| getarray-superset | proved | all subs proved
| is_arrayref,
getarray-subset,
|
| getarray-putbar | proved | all subs proved
| getarray-putbar-01,
getarray-put-02,
putBar-rec,
putBar-empty,
putByteArray-all,
|
| getarray-copy-01 | proved | all subs proved
| getarray-copy-02,
|
| getarray-copy | proved | all subs proved
| getarray-copy-02,
copy-length,
getArray-all,
|
| getar-at | proved | all subs proved
| get-length,
getByteArray,
get-get,
|
| getArray-rec-01 | proved | all subs proved
| get-zero,
getArray-one,
getArray-rec,
|
| get-rest-01 | proved | all subs proved
| get-rest,
|
| get-put-05 | proved | all subs proved
| get-put,
|
| get-eqex-02 | proved | all subs proved
| get-eqex-03,
|
| get-ateq-01 | proved | all subs proved
| get-ateq,
|
| copy-ref | proved | all subs proved
| copy-in-01,
|
| copy-bet-bet | proved | all subs proved
| copy-bet-up,
copy-upper,
arrayCopy-rec,
|
| copy-at-01 | proved | all subs proved
| copy-ident,
copy-between,
|
| copy-arref | proved | all subs proved
| copy-in,
is_arrayref,
|
| bar-len-01 | proved | all subs proved
| get-zero,
getArray-one,
getByteArray,
|
| at=get-offset | proved | all subs proved
| get-zero,
get-length,
getArray-one,
getArray-rec,
|
| pubBar-init | proved | all subs proved
| putBar-rec,
putBar-empty,
|
| putar-inother | proved | all subs proved
| putar-inref,
putArray-rec,
putArray-empty,
|
| putbar-infs | proved | all subs proved
| putar-infs,
putByteArray,
|
| putar-getar-02 | proved | all subs proved
| getarray-put-02,
putArray-rec,
putArray-empty,
|
| putar-getar-01 | proved | all subs proved
| getarray-put-02,
putar-atref,
getArray-zero,
get-rec-01,
putArray-rec,
putArray-empty,
|
| putar-atother | proved | all subs proved
| putar-atref,
putArray-rec,
putArray-empty,
|
| putByteArray-put-switch | proved | all subs proved
| putBar-rec,
putBar-empty,
|
| putBar-one | proved | all subs proved
| putBar-empty,
putBar-rec,
|
| putArray-in | proved | all subs proved
| putar-inref,
putar-rew,
putArray-rec,
putArray-empty,
|
| putbar-atref-01 | proved | all subs proved
| putar-atref,
putByteArray,
|
| putArray-at | proved | all subs proved
| putar-atfs,
|
| putAr-lastrec | proved | all subs proved
| putArray-rec,
putArray-empty,
putar-rew,
|
| putbar-inref | proved | all subs proved
| putar-inref,
putByteArray,
|
| getintarray-put-other | proved | all subs proved
| getarray-put-02,
getintarray,
|
| getintarray-rec-first | proved | all subs proved
| get-rec-01,
getintarray,
|
| getintarray-empty-01 | proved | all subs proved
| get-empty,
getintarray,
|
| get-length-02 | proved | all subs proved
| get-empty,
|
| bar-restn | proved | all subs proved
| get-rec-01,
getByteArray,
|
| getbar-len-01 | proved | all subs proved
| get-empty,
getByteArray,
getByteArray-all,
|
| getarray-union-03 | proved | all subs proved
| getArray-zero,
get-rec-01,
|
| getarray-subset | proved | all subs proved
| get-alleq,
is_arrayref,
|
| getarray-putbar-01 | proved | all subs proved
| getarray-put-02,
putBar-rec,
putBar-empty,
|
| copy-length | proved | all subs proved
| copy-atfield,
|
| getarray-copy-02 | proved | all subs proved
| copy-at,
get-alleq,
|
| getarray-put-other | proved | all subs proved
| getarray-put-02,
getArray-all,
|
| getbar-ref | proved | all subs proved
| getarray-put-02,
getByteArray,
|
| get-rest | proved | all subs proved
| get-empty,
getArray-one,
getArray-zero,
getArray-rec,
|
| get-put | proved | all subs proved
| getByteArray,
get-put-01,
getByteArray-all,
|
| get-eqex-03 | proved | all subs proved
| get-alleq,
|
| get-del | proved | all subs proved
| get-del-01,
getArray-all,
|
| get-ateq | proved | all subs proved
| get-alleq,
|
| copy-upper-01 | proved | all subs proved
| copy-upper,
|
| copy-in-upper-01 | proved | all subs proved
| copy-in-upper,
|
| copy-in-01 | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
copy-in-02,
|
| copy-in-between | proved | all subs proved
| copy-zero,
copy-in-upper,
arrayCopy-rec,
|
| copy-bet-up | proved | all subs proved
| copy-upper,
arrayCopy-rec,
|
| copy-in | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
copy-infs,
|
| copy-between | proved | all subs proved
| copy-upper,
arrayCopy-rec,
|
| getbar-rec | proved | all subs proved
| get-rec-01,
getByteArray,
|
| bar-empty | proved | all subs proved
| get-empty,
getByteArray,
|
| get-zero | proved | all subs proved
| get-empty,
|
| get-get | proved | all subs proved
| get-length,
getArray-one,
getArray-rec,
|
| at=get | proved | all subs proved
| get-length,
getArray-one,
getArray-rec,
|
| copy-bet-low | proved | all subs proved
| copy-ident,
copy-upper,
arrayCopy-rec,
|
| copy-length-02 | proved | all subs proved
| copy-infs,
|
| copy-mode | proved | all subs proved
| copy-atfield,
|
| copy-mode-01 | proved | all subs proved
| copy-infs,
|
| copy-type | proved | all subs proved
| copy-infs,
|
| copy-type-01 | proved | all subs proved
| copy-atfield,
|
| get-length-04 | proved | all subs proved
| get-length,
|
| get-put-03 | proved | all subs proved
| getByteArray,
get-put-01,
|
| get-put-04 | proved | all subs proved
| getByteArray,
get-put-01,
|
| get-puteq | proved | all subs proved
| get-alleq,
|
| getarray-put-04 | proved | all subs proved
| getarray-put-03,
|
| isarrayref-put | proved | all subs proved
| is_arrayref,
arrayref-02,
|
| putAr-get-other-01 | proved | all subs proved
| putar-atref,
putArray-rec,
putArray-empty,
|
| putBar-rew-01 | proved | all subs proved
| putBar-rec,
putBar-empty,
|
| putBar-unrec | proved | all subs proved
| putBar-rec,
|
| putbar-atfs | proved | all subs proved
| putar-atfs,
putByteArray,
putByteArray-all,
|
| putbar-atfs-01 | proved | all subs proved
| putar-atfs,
putByteArray,
|
| putbar-atref | proved | all subs proved
| putar-atref,
putByteArray,
putByteArray-all,
|
| putbar-in | proved | all subs proved
| putar-in,
putByteArray,
|
| putbar-in-01 | proved | all subs proved
| putar-in-01,
putByteArray,
|
| putbar-in-02 | proved | all subs proved
| putar-in-02,
putByteArray,
|
| putbar-refval | proved | all subs proved
| putBar-rec,
putBar-empty,
|
| Comp-get-01 | proved | all subs proved
| getArray-one,
getArray-zero,
getArray-rec,
arrayComp,
|
| copy-ident | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-in-02 | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-zero | proved | all subs proved
| arrayCopy-base,
|
| copy-in-upper | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-infs | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-atfield | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-upper | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| get-del-01 | proved | all subs proved
| getArray-one,
getArray-rec,
getArray-zero,
|
| getarray-put-03 | proved | all subs proved
| getArray-one,
getArray-zero,
getArray-rec,
|
| get-alleq | proved | all subs proved
| getArray-one,
getArray-zero,
getArray-rec,
|
| get-put-01 | proved | all subs proved
| bytevalues,
getArray-one,
getArray-zero,
getArray-rec,
getByteArray,
|
| get-length | proved | all subs proved
| getArray-one,
getArray-rec,
|
| get-empty | proved | all subs proved
| getArray-one,
getArray-rec,
getArray-zero,
|
| arrayref-02 | proved | all subs proved
| is_arrayref,
|
| putar-rew | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putArray-put-switch | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putArray-one | proved | all subs proved
| putArray-empty,
putArray-rec,
|
| get-rec-01 | proved | all subs proved
| getArray-one,
getArray-zero,
getArray-rec,
|
| getarray-put-02 | proved | all subs proved
| getArray-one,
getArray-zero,
getArray-rec,
|
| putar-atfs | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putar-atref | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putar-in | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putar-in-01 | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putar-in-02 | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putar-infs | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putar-inref | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putBar-rec | proved | all subs proved
| putArray-rec,
putByteArray,
|
| putBar-empty | proved | all subs proved
| putArray-empty,
putByteArray,
|
| copy-at | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| putArray-put-switch-02 | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putArray-put-switch-01 | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putArray-append | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| putAr-get-other | proved | all subs proved
| putArray-rec,
putArray-empty,
|
| isarrayref-mod | proved | all subs proved
| is_arrayref,
|
| isarrayref-del | proved | all subs proved
| is_arrayref,
|
| isarray-03 | proved | all subs proved
| is_arrayref,
|
| isarray-02 | proved | all subs proved
| is_arrayref,
|
| isarray-01 | proved | all subs proved
| is_arrayref,
|
| isarray | proved | all subs proved
| is_arrayref,
|
| is_arrayref-03 | proved | all subs proved
| is_arrayref,
|
| is_arrayref-02 | proved | all subs proved
| is_arrayref,
|
| is_arrayref-01 | proved | all subs proved
| is_arrayref,
|
| getintarray-max-len | proved | all subs proved
| getintarray-def,
|
| getintarray-length-rew | proved | all subs proved
| getintarray-def,
|
| getarray=getbytearray | proved | all subs proved
| getByteArray,
|
| getarray-in-01 | proved | all subs proved
| getArray-one,
getArray-rec,
|
| get-length-03 | proved | all subs proved
| getArray-zero,
|
| copy-new | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-init-02 | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-init-01 | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| copy-init | proved | all subs proved
| arrayCopy-base,
arrayCopy-rec,
|
| comp-next | proved | all subs proved
| arrayComp,
|
| comp-negative | proved | all subs proved
| arrayComp,
|
| bar-len | proved | all subs proved
| getArray-one,
getArray-zero,
getByteArray,
|
| arrayref-01 | proved | all subs proved
| is_arrayref,
|
| arrayref | proved | all subs proved
| is_arrayref,
|
| arrayComp-07 | proved | all subs proved
| arrayComp,
|
| arrayComp-06 | proved | all subs proved
| arrayComp,
|
| arrayComp-04 | proved | all subs proved
| arrayComp,
|
| arrayComp-03 | proved | all subs proved
| arrayComp,
|
| arrayComp-02 | proved | all subs proved
| arrayComp,
|
| arrayComp-01 | proved | all subs proved
| arrayComp,
|
| putArray-all | axiom | | |
| putByteArray | axiom | | |
| putArray-empty | axiom | | |
| putArray-rec | axiom | | |
| getintarray-def | axiom | | |
| getintarray | axiom | | |
| putByteArray-all | axiom | | |
| getArray-all | axiom | | |
| arrayCopy-rec | axiom | | |
| arrayCopy-base | axiom | | |
| bytevalues | proved | all subs proved
| |
| getByteArray-all | axiom | | |
| getByteArray | axiom | | |
| is_arrayref | axiom | | |
| getArray-rec | axiom | | |
| getArray-zero | axiom | | |
| getArray-one | axiom | | |
| arrayComp | axiom | | |