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: |
|---|
| no-dups-keyset-size-simp | proved | all subs proved
| no-dups-keyset-size,
|
| no-dups-keyset-size | proved | all subs proved
| key-set-extract-index,
keyset-size-bound0,
keyset-rec,
keyset-base,
no-dups,
|
| keyset-xchg | proved | all subs proved
| keyset-overwrite-add,
keyset-rec,
keyset-base,
key-set-write-other,
|
| keyset-size-bound0 | proved | all subs proved
| keyset-size-bound,
|
| keyset-overwrite-add | proved | all subs proved
| keyset-rec,
keyset-base,
key-set-write-other,
|
| valid-idx-outofbounds | proved | all subs proved
| key-set-extract-index,
valid-idx,
|
| no-dups-idx-rec | proved | all subs proved
| key-set-extract-index,
no-dups-idx,
|
| keyset-subarray-eq-add | proved | all subs proved
| keyset-subarray-eq,
|
| key-set-write-nodups | proved | all subs proved
| key-set-extract-index,
keyset-rec,
keyset-base,
key-set-write-other,
no-dups-idx,
|
| key-set-write-last | proved | all subs proved
| key-set-write-other,
keyset-rec,
|
| key-index-in-keyset-array-extract | proved | all subs proved
| key-set-extract-index,
valid-idx,
|
| keyset-subarray-eq | proved | all subs proved
| keyset-rec,
keyset-base,
|
| keyset-size-bound | proved | all subs proved
| keyset-rec,
keyset-base,
|
| key-set-write-other | proved | all subs proved
| keyset-rec,
keyset-base,
|
| key-set-extract-index | proved | all subs proved
| keyset-rec,
keyset-base,
|
| valid-idx-xhg | proved | all subs proved
| valid-idx,
|
| valid-idx-update-key | proved | all subs proved
| valid-idx,
|
| valid-idx-remlast | proved | all subs proved
| valid-idx,
|
| valid-idx-rec | proved | all subs proved
| no-dups-idx,
valid-idx,
|
| valid-idx-move-last | proved | all subs proved
| valid-idx,
|
| valid-idx-last-valid | proved | all subs proved
| valid-idx,
|
| valid-idx-imp-1 | proved | all subs proved
| valid-idx,
|
| valid-idx-0 | proved | all subs proved
| valid-idx,
|
| no-dups-update-key | proved | all subs proved
| no-dups-idx,
|
| no-dups-shorter | proved | all subs proved
| no-dups,
|
| no-dups-idx-xchg | proved | all subs proved
| no-dups-idx,
|
| no-dups-idx-remlast | proved | all subs proved
| no-dups-idx,
|
| no-dups-idx-rem1 | proved | all subs proved
| no-dups-idx,
|
| no-dups-idx-mvlast | proved | all subs proved
| no-dups-idx,
|
| no-dups-idx-0 | proved | all subs proved
| no-dups-idx,
|
| no-dups-0 | proved | all subs proved
| no-dups,
|
| key-set-1 | proved | all subs proved
| keyset-base,
keyset-rec,
|
| heap-order-remove-last | proved | all subs proved
| heap-order,
|
| heap-order-pull-up-child | proved | all subs proved
| heap-order,
|
| heap-order-pull-down-parent | proved | all subs proved
| heap-order,
|
| heap-order-overwrite0 | proved | all subs proved
| heap-order,
|
| heap-order-overwrite-parent-ok | proved | all subs proved
| heap-order,
|
| heap-order-overwrite-children-ok | proved | all subs proved
| heap-order,
|
| heap-order-overwrite-children-at | proved | all subs proved
| heap-order,
|
| heap-order-min | proved | all subs proved
| heap-order,
|
| heap-order-add-smaller | proved | all subs proved
| heap-order,
|
| heap-order-add-parent-key | proved | all subs proved
| heap-order,
|
| heap-order-1 | proved | all subs proved
| heap-order,
|
| heap-order-0 | proved | all subs proved
| heap-order,
|
| 2exp-size-mult2 | proved | all subs proved
| 2exp-size,
|
| 2exp-size-1 | proved | all subs proved
| 2exp-size,
|
| 2exp-size-0 | proved | all subs proved
| 2exp-size,
|
| no-dups | axiom | | |
| no-dups-idx | axiom | | |
| keyset-rec | axiom | | |
| keyset-base | axiom | | |
| valid-idx | axiom | | |
| heap-order | axiom | | |
| 2exp-size | axiom | | |