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-simp-explicit | proved | all subs proved
| subarray-elim,
|
| subarray-subarray-elim-0 | proved | all subs proved
| Subarray,
subarray-copy-elim,
subarray-subarray-elim-0-weak,
|
| subarray-elim-simp | proved | all subs proved
| subarray-elim,
|
| subarray-subarray-elim-0-weak | proved | all subs proved
| Subarray,
subarray-copy-elim,
|
| subarray-elim | proved | all subs proved
| copy-exact,
Subarray,
|
| subarray-longer-eq-eq | proved | all subs proved
| copy-exact,
at-copy,
size-copy,
Subarray,
|
| idexcept-n-subarrays | proved | all subs proved
| copy-exact,
at-copy,
size-copy,
Subarray,
Idexcept-n,
|
| copy-other | proved | all subs proved
| copy-other-weak,
|
| subarray-copy-elim-exact | proved | all subs proved
| subarray-copy-elim,
|
| subarray-write-above | proved | all subs proved
| subarray-at,
size-subarray,
|
| subarray-up-same | proved | all subs proved
| copy-exact,
at-copy,
size-copy,
Subarray,
|
| subarray-at | proved | all subs proved
| at-copy,
Subarray,
|
| subarray-copy-elim | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| copy-other-weak | proved | all subs proved
| Copy-succ,
Copy-zero,
at-copy,
size-copy,
|
| copy-exact | proved | all subs proved
| at-copy,
size-copy,
|
| at-fill | proved | all subs proved
| at-fill-h0,
Fill-all,
|
| subarray-subarray-elim | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| subarray-copy | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| cmp-fill-full | proved | all subs proved
| at-fill-h0,
size-fill-h,
Cmp,
Fill-all,
|
| subarray-copy-higher | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| cmp-fill | proved | all subs proved
| at-fill-h,
Cmp-elem,
Fill-all,
|
| at-fill-mkarray | proved | all subs proved
| at-fill-h,
Fill-all,
|
| idexcept-n-fill-other | proved | all subs proved
| at-fill-h,
Idexcept-n,
size-fill-h,
|
| copy-self | proved | all subs proved
| at-copy,
size-copy,
|
| idexcpt-n-copy-hole | proved | all subs proved
| at-copy,
Idexcept-n,
size-copy,
|
| copy-subarray1-elim | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| at-subarray | proved | all subs proved
| at-copy,
Subarray,
|
| copy-append | proved | all subs proved
| at-copy,
size-copy,
|
| copy-is-subarray | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| at-fill-other | proved | all subs proved
| at-fill-h,
|
| idexcept-n-copy-other | proved | all subs proved
| at-copy,
Idexcept-n,
size-copy,
|
| copy-coalesce | proved | all subs proved
| at-copy,
size-copy,
|
| subarray-copy-lower | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| subarray-write-below | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| copy-subarray2 | proved | all subs proved
| at-copy,
size-copy,
Subarray,
|
| copy-rec | proved | all subs proved
| at-copy,
Copy-zero,
size-copy,
Copy-succ,
|
| size-subarray | proved | all subs proved
| size-copy,
Subarray,
|
| at-fill-h | proved | all subs proved
| size-fill-h,
Fill-succ,
Fill-zero,
|
| at-copy | proved | all subs proved
| size-copy,
Copy-succ,
Copy-zero,
|
| at-fill-h0 | proved | all subs proved
| size-fill-h,
Fill-succ,
Fill-zero,
|
| size-fill | proved | all subs proved
| size-fill-h,
Fill-all,
|
| idexcept-write-at-right | proved | all subs proved
| Idexcept,
idexcept-write-at0-right,
|
| idexcept-write-at | proved | all subs proved
| Idexcept,
idexcept-write-at0,
|
| cmp-write-same | proved | all subs proved
| cmp-full-at,
|
| cmp-full-at | proved | all subs proved
| Cmp,
|
| idexcept-write-at0 | proved | all subs proved
| Idexcept,
|
| idexcept-write-at0-right | proved | all subs proved
| Idexcept,
|
| size-copy | proved | all subs proved
| Copy-succ,
Copy-zero,
|
| size-fill-h | proved | all subs proved
| Fill-succ,
Fill-zero,
|
| idexcept-refl | proved | all subs proved
| Idexcept,
|
| idexcept-comm-simp | proved | all subs proved
| Idexcept,
|
| idexcept-comm | proved | all subs proved
| Idexcept,
|
| idexcept-n-trans-successive | proved | all subs proved
| Idexcept-n,
|
| cmp-at | proved | all subs proved
| Cmp-elem,
|
| cmp-write-above | proved | all subs proved
| Cmp-elem,
|
| cmp-move-1 | proved | all subs proved
| Cmp-elem,
|
| idexcept-size | proved | all subs proved
| Idexcept,
|
| subarray-zero | proved | all subs proved
| Copy-zero,
Subarray,
|
| cmp-cmp-eq | proved | all subs proved
| Cmp,
|
| idexcept-extract-left | proved | all subs proved
| Idexcept,
|
| idexcept-extract-right | proved | all subs proved
| Idexcept,
|
| cmp-cmp | proved | all subs proved
| Cmp-elem,
Cmp,
|
| idexcept-n-widden | proved | all subs proved
| Idexcept-n,
|
| idexcept-trans | proved | all subs proved
| Idexcept,
|
| idexcept-n-same | proved | all subs proved
| Idexcept-n,
|
| idexcept-n-trans-rev | proved | all subs proved
| Idexcept-n,
|
| cmp-write-below | proved | all subs proved
| Cmp-elem,
|
| idexcept-eq-below | proved | all subs proved
| Idexcept-n,
|
| idexcept-n-shorter | proved | all subs proved
| Idexcept-n,
|
| cmp-full-write | proved | all subs proved
| Cmp,
|
| cmp-write-value | proved | all subs proved
| Cmp-elem,
|
| cmp-0 | proved | all subs proved
| Cmp-elem,
|
| idexcept-n-trans | proved | all subs proved
| Idexcept-n,
|
| cmp-at-0 | proved | all subs proved
| Cmp-elem,
|
| idexcept-eq-above | proved | all subs proved
| Idexcept-n,
|
| idexcept-same | proved | all subs proved
| Idexcept,
|
| Cmp-elem | axiom | | |
| Idexcept-n | axiom | | |
| Cmp | axiom | | |
| Copy-zero | axiom | | |
| Copy-succ | axiom | | |
| Fill-zero | axiom | | |
| Fill-succ | axiom | | |
| Subarray | axiom | | |
| Fill-all | axiom | | |
| Idexcept | axiom | | |