[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 array-copy

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:
subarray-elim-simpprovedall subs proved subarray-elim,
subarray-elimprovedall subs proved copy-exact, Subarray,
subarray-up-sameprovedall subs proved copy-exact, at-copy, size-copy, Subarray,
subarray-copy-elim-exactprovedall subs proved Subarray, subarray-copy-elim,
rev-revprovedall subs proved rev-at, rev-size,
copy-otherprovedall subs proved copy-other-weak,
copy-exactprovedall subs proved at-copy, size-copy,
subarray-copy-elimprovedall subs proved at-copy, size-copy, Subarray,
rev-atprovedall subs proved rev-at-h, rev,
copy-other-weakprovedall subs proved Copy-succ, Copy-zero, at-copy, size-copy,
subarray-write-belowprovedall subs proved at-copy, size-copy, Subarray,
subarray-subarray-elimprovedall subs proved at-copy, size-copy, Subarray,
subarray-copy-lowerprovedall subs proved at-copy, size-copy, Subarray,
subarray-copy-higherprovedall subs proved at-copy, size-copy, Subarray,
subarray-copyprovedall subs proved at-copy, size-copy, Subarray,
subarray-atprovedall subs proved at-copy, Subarray,
copy-subarray2provedall subs proved at-copy, size-copy, Subarray,
copy-subarray1-elimprovedall subs proved at-copy, size-copy, Subarray,
copy-selfprovedall subs proved at-copy, size-copy,
copy-recprovedall subs proved at-copy, Copy-zero, size-copy, Copy-succ,
copy-is-subarrayprovedall subs proved at-copy, size-copy, Subarray,
copy-coalesceprovedall subs proved at-copy, size-copy,
copy-appendprovedall subs proved at-copy, size-copy,
at-subarrayprovedall subs proved at-copy, Subarray,
at-fill-mkarrayprovedall subs proved at-fill-h, Fill-all,
at-fillprovedall subs proved at-fill-h0, Fill-all,
rev-sizeprovedall subs proved rev-size-h, rev,
rev-at-hprovedall subs proved rev-size-h, rev-rec,
at-copyprovedall subs proved size-copy, Copy-succ, Copy-zero,
at-fill-hprovedall subs proved size-fill-h, Fill-succ, Fill-zero,
at-fill-h0provedall subs proved size-fill-h, Fill-succ,
size-subarrayprovedall subs proved size-copy, Subarray,
size-fillprovedall subs proved size-fill-h, Fill-all,
idexcept-write-at-rightprovedall subs proved Idexcept, idexcept-write-at0-right,
idexcept-write-atprovedall subs proved Idexcept, idexcept-write-at0,
rev-size-hprovedall subs proved rev-rec, rev-base,
idexcept-write-at0-rightprovedall subs proved Idexcept,
idexcept-write-at0provedall subs proved Idexcept,
size-fill-hprovedall subs proved Fill-succ, Fill-zero,
size-copyprovedall subs proved Copy-succ, Copy-zero,
subarray-zeroprovedall subs proved Copy-zero, Subarray,
in-atprovedall subs proved in,
idexcept-transprovedall subs proved Idexcept,
idexcept-sizeprovedall subs proved Idexcept,
idexcept-sameprovedall subs proved Idexcept,
idexcept-reflprovedall subs proved Idexcept,
idexcept-extract-rightprovedall subs proved Idexcept,
idexcept-extract-leftprovedall subs proved Idexcept,
idexcept-comm-simpprovedall subs proved Idexcept,
idexcept-commprovedall subs proved Idexcept,
at-fill-otherprovedall subs proved Fill-succ, Fill-zero,
rev-baseaxiom
rev-recaxiom
revaxiom
inaxiom
Idexceptaxiom
Subarrayaxiom
Fill-zeroaxiom
Fill-succaxiom
Fill-allaxiom
Copy-zeroaxiom
Copy-succaxiom