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-split-at | proved | all subs proved
| append-at2,
append-at1,
append-len,
append-a,
append-prefix-left,
|
| subarray-append-shift-right | proved | all subs proved
| append-at,
append-a,
append-len,
|
| subarray-append-consec0 | proved | all subs proved
| subarray-append-consec,
|
| same-size-append | proved | all subs proved
| append-zero-right,
append-a,
append-len,
|
| mkemparray0-append-right | proved | all subs proved
| append-a,
emparray-len,
append-prefix-left,
|
| mkemparray0-append-left | proved | all subs proved
| emparray-len,
append-left-size0,
|
| copy2append00 | proved | all subs proved
| append-eq-left,
append-zero-left,
append-a,
append-prefix-left,
copy2append0,
|
| append-right-size0 | proved | all subs proved
| append-a,
append-prefix-left,
|
| append-eq-emptyar | proved | all subs proved
| append-len,
append-a,
append-zero-left,
|
| append-at | proved | all subs proved
| append-at2,
append-a,
append-at1,
|
| subarray-append-consec | proved | all subs proved
| append-at2,
append-at1,
append-a,
append-len,
|
| append-zero-right | proved | all subs proved
| append-at1,
append-a,
append-len,
|
| append-left-size0 | proved | all subs proved
| append-at1,
append-at2,
append-a,
append-len,
|
| copy2append0 | proved | all subs proved
| append-at2,
append-at1,
append-len,
append-a,
|
| append-eq-left | proved | all subs proved
| append-at2,
append-atp2,
append-a,
append-len,
|
| append-prefix-left | proved | all subs proved
| append-at1,
append-a,
append-len,
|
| append-zero-left | proved | all subs proved
| resize-len,
append,
append-a,
append-len,
|
| subarray-split-first | proved | all subs proved
| append-at2,
append-at1,
append-a,
append-len,
|
| subarray-append-left-01 | proved | all subs proved
| append-at1,
append-a,
append-len,
|
| subarray-append-left | proved | all subs proved
| append-at1,
append-a,
append-len,
|
| subarray-append-elim-left0 | proved | all subs proved
| append-atp2,
append-a,
append-len,
|
| subarray-append-elim-left | proved | all subs proved
| append-at2,
append-a,
append-len,
|
| subarray-append-elim | proved | all subs proved
| append-atp2,
append-a,
append-len,
|
| mkemparray-append | proved | all subs proved
| append-at2,
append-at1,
emparray-at,
append-a,
emparray-len,
append-len,
|
| fill2append | proved | all subs proved
| append-at2,
append-at1,
append-a,
append-len,
|
| copy2append | proved | all subs proved
| append-at2,
append-at1,
append-len,
append-a,
|
| copy-shift-append | proved | all subs proved
| append-a,
copy-append,
|
| copy-exact-append | proved | all subs proved
| append-a,
append-at1,
|
| append-inj | proved | all subs proved
| append-at2,
append-atp2,
append-at1,
append-a,
append-len,
|
| append-eq-right | proved | all subs proved
| append-at1,
append-a,
append-len,
|
| copy-append | proved | all subs proved
| append-at2,
|
| append-a | proved | all subs proved
| append-atp2,
append-at2,
append-at1,
append-len,
|
| range-extend | proved | all subs proved
| range-eq-ext,
range-eq-append,
|
| range-eq-append | proved | all subs proved
| range-eq-rec,
range-eq-bounds,
range-eq-0,
|
| append-at2 | proved | all subs proved
| append-atp2,
|
| splice-resize-less | proved | all subs proved
| splice-copy,
splice-resize,
splice-0,
splice-len,
resize-at,
resize-len,
|
| resize-exact-n | proved | all subs proved
| resize-exact,
|
| range-eq-trans | proved | all subs proved
| range-eq-ext,
|
| range-eq-sym | proved | all subs proved
| range-eq-ext,
|
| range-eq-subarrays | proved | all subs proved
| range-eq-ext,
|
| range-eq-splice-less | proved | all subs proved
| resize-at,
splice-copy,
splice-len,
resize-len,
range-eq-ext,
splice-resize,
|
| range-eq-resize | proved | all subs proved
| resize-at,
resize-len,
range-eq-ext,
|
| range-eq-refl | proved | all subs proved
| range-eq-ext,
|
| range-eq-cut | proved | all subs proved
| resize-at,
resize-len,
range-eq-ext,
|
| range-copy-upper | proved | all subs proved
| range-eq-ext,
|
| range-copy-outer | proved | all subs proved
| range-eq-ext,
|
| range-copy-lower | proved | all subs proved
| range-eq-ext,
|
| range-copy-inner | proved | all subs proved
| range-eq-ext,
|
| range-copy-drop | proved | all subs proved
| range-eq-ext,
|
| resize-exact | proved | all subs proved
| resize-at,
resize-len,
|
| splice-len | proved | all subs proved
| resize-len,
splice-resize,
splice-copy,
|
| range-eq-bounds | proved | all subs proved
| range-eq-rec,
range-eq-0,
|
| range-eq-ext | proved | all subs proved
| range-eq-rec,
range-eq-0,
|
| append-len | proved | all subs proved
| resize-len,
append,
|
| append-at1 | proved | all subs proved
| resize-at,
resize-len,
append,
|
| append-atp2 | proved | all subs proved
| resize-len,
append,
|
| resize-twice | proved | all subs proved
| resize-at,
resize-len,
|
| mkemparray-eq | proved | all subs proved
| emparray-len,
|
| splice-0 | axiom | | |
| splice-resize | axiom | | |
| splice-copy | axiom | | |
| range-eq-0 | axiom | | |
| range-eq-rec | axiom | | |
| emparray-len | axiom | | |
| emparray-at | axiom | | |
| append | axiom | | |
| resize-len | axiom | | |
| resize-at | axiom | | |