[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-splice

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-eq-elimprovedall subs proved subarray-append-elim-left0, subarray-append-consec, subarray-append-consec0, append-prefix-left, append-eq-left, append-zero-right, subarray-elim-right, append-zero-left, subarray-split-at, append-a, append-len,
subarray-elimprovedall subs proved subarray-append-elim-left0, subarray-elim-right, append-len, append-prefix-left, append-a, subarray-append-consec0,
subarray-append-elim-left0provedall subs proved append-a, copy-shift-append,
subarray-append-shift-right-simp-0provedall subs proved append-a, append-eq-left, subarray-append-shift-right,
array-split2provedall subs proved append-prefix-left, append-a, subarray-append-consec0,
array-split1provedall subs proved append-a, append-prefix-left, subarray-append-consec0,
array-split-elim-sizeprovedall subs proved append-prefix-left, subarray-append-consec0, append-a, append-len,
subarray-split-atprovedall subs proved append-at2, append-at1, append-len, append-a, append-prefix-left,
subarray-append-shift-rightprovedall subs proved append-atp2, append-at1, append-at, append-a, append-len,
copy-shift-appendprovedall subs proved append-a, copy-append,
subarray-append-consec0provedall subs proved subarray-append-consec,
subarray-split-sizeprovedall subs proved append-at, append-a, append-len,
subarray-append-shift-leftprovedall subs proved append-at, append-a, append-len,
subarray-append-elim-leftprovedall subs proved append-a, copy-append,
same-size-appendprovedall subs proved append-zero-right, append-a, append-len,
range-eq-append-shiftprovedall subs proved append-a, range-eq-shift-right,
mkemparray0-append-rightprovedall subs proved append-a, append-prefix-left, emparray,
mkemparray0-append-leftprovedall subs proved emparray, append-left-size0,
mkemparray-appendprovedall subs proved append-at, append-a, append-len, emparray,
fill-append-shiftprovedall subs proved append-at, append-at2, append-at1, append-a, append-len,
copy2append00provedall subs proved append-eq-left, append-zero-left, append-a, append-prefix-left, copy2append0,
copy-shift-rightprovedall subs proved append-at2, append-at1, append-at, append-a, append-len,
append-right-size0provedall subs proved append-a, append-prefix-left,
append-eq-emptyarprovedall subs proved append-len, append-a, append-zero-left,
subarray-append-consecprovedall subs proved append-at2, append-at1, append-a, append-len,
append-zero-rightprovedall subs proved append-at1, append-a, append-len,
range-eq-shift-rightprovedall subs proved append-atp2, append-a, append-len, range-eq-ext,
append-left-size0provedall subs proved append-at2, append-a, append-len,
copy2append0provedall subs proved append-at2, append-at1, append-len, append-a,
append-eq-leftprovedall subs proved append-atp2, append-a, append-len,
append-atprovedall subs proved append-at2, append-a, append-at1,
copy-appendprovedall subs proved append-a, append-atp2,
append-prefix-leftprovedall subs proved append-at1, append-a, append-len,
append-zero-leftprovedall subs proved resize-len, append, append-a, append-len,
subarray-split-firstprovedall subs proved append-at2, append-at1, append-a, append-len,
subarray-append-left-01provedall subs proved append-a, subarray-elim-right,
subarray-append-leftprovedall subs proved append-a, subarray-elim-right,
subarray-append-elim-left0-simpprovedall subs proved append-a, append-atp2,
subarray-append-elimprovedall subs proved append-a, append-atp2,
fill2appendprovedall subs proved append-at2, append-at1, append-a, append-len,
copy2appendprovedall subs proved append-at2, append-at1, append-len, append-a,
copy-exact-appendprovedall subs proved append-a, append-at1,
append-injprovedall subs proved append-atp2, append-at1, append-a, append-len,
append-eq-rightprovedall subs proved append-at1, append-a, append-len,
append-aprovedall subs proved append-atp2, append-at2, append-at1, append-len,
range-extendprovedall subs proved range-eq-ext, range-eq-append,
range-eq-cutprovedall subs proved range-eq-resize,
subarray-elim-rightprovedall subs proved append-at1,
range-eq-appendprovedall subs proved range-eq-rec, range-eq-ext, range-eq-0,
range-eq-resizeprovedall subs proved resize-at, resize-len, range-eq-ext,
append-at2provedall subs proved append-atp2,
splice-resize-lessprovedall subs proved splice-copy, splice-resize, splice-0, splice-len, resize-at, resize-len,
resize-exact-nprovedall subs proved resize-exact,
rangeeq-write-left-belowprovedall subs proved range-eq-ext,
rangeeq-write-left-aboveprovedall subs proved range-eq-ext,
range-eq-transprovedall subs proved range-eq-ext,
range-eq-symprovedall subs proved range-eq-ext,
range-eq-subarraysprovedall subs proved range-eq-ext,
range-eq-splice-lessprovedall subs proved resize-at, splice-0, splice-len, resize-len, range-eq-ext, splice-resize,
range-eq-refl-simpprovedall subs proved range-eq-ext,
range-eq-reflprovedall subs proved range-eq-ext,
range-eq-extractprovedall subs proved range-eq-ext,
range-copy-upperprovedall subs proved range-eq-ext,
range-copy-outerprovedall subs proved range-eq-ext,
range-copy-lowerprovedall subs proved range-eq-ext,
range-copy-innerprovedall subs proved range-eq-ext,
range-copy-dropprovedall subs proved range-eq-ext,
append-at1-simp2provedall subs proved append-at1,
append-at1-simp1provedall subs proved append-at1,
resize-exactprovedall subs proved resize-at, resize-len,
splice-lenprovedall subs proved resize-len, splice-resize, splice-copy,
range-eq-extprovedall subs proved range-eq-rec, range-eq-0,
append-lenprovedall subs proved resize-len, append,
append-at1provedall subs proved resize-at, resize-len, append,
append-atp2provedall subs proved resize-len, append,
zarray-lenprovedall subs proved zarray,
zarray-atprovedall subs proved zarray,
subarray-emparrayprovedall subs proved emparray,
resize-twiceprovedall subs proved resize-at, resize-len,
range-eq-boundsprovedall subs proved range-eq-rec, range-eq-0,
mkemparray-eqprovedall subs proved emparray,
emparray-lenprovedall subs proved emparray,
emparray-atprovedall subs proved emparray,
zarrayaxiom
splice-copyaxiom
splice-resizeaxiom
splice-0axiom
range-eq-0axiom
range-eq-recaxiom
emparrayaxiom
appendaxiom
resize-lenaxiom
resize-ataxiom