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: |
|---|
| cmp-fill-full | proved | all subs proved
| at-fill-h0,
Cmp,
Fill-all,
|
| copy-other | proved | all subs proved
| copy-other-weak,
|
| at-fill-mkarray | proved | all subs proved
| at-fill-h0,
Fill-all,
|
| copy-other-weak | proved | all subs proved
| Copy-succ,
Copy-zero,
at-copy,
|
| at-fill-h0 | proved | all subs proved
| at-fill-h,
|
| at-fill | proved | all subs proved
| at-fill-h,
Fill-all,
|
| cmp-write-same | proved | all subs proved
| cmp-full-at,
|
| at-fill-other | proved | all subs proved
| at-fill-h,
|
| cmp-fill | proved | all subs proved
| at-fill-h,
Cmp-elem,
Fill-all,
|
| idexcept-n-fill-other | proved | all subs proved
| at-fill-h,
Idexcept-n,
|
| copy-self | proved | all subs proved
| at-copy,
|
| copy-exact | proved | all subs proved
| at-copy,
|
| idexcpt-n-copy-hole | proved | all subs proved
| Idexcept-n,
at-copy,
|
| idexcept-n-copy-other | proved | all subs proved
| Idexcept-n,
at-copy,
|
| copy-coalesce | proved | all subs proved
| at-copy,
|
| copy-append | proved | all subs proved
| at-copy,
|
| copy-rec | proved | all subs proved
| at-copy,
Copy-zero,
Copy-succ,
|
| cmp-full-at | proved | all subs proved
| Cmp,
|
| at-copy | proved | all subs proved
| Copy-succ,
Copy-zero,
|
| at-fill-h | proved | all subs proved
| Fill-succ,
Fill-zero,
|
| idexcept-trans | proved | all subs proved
| Idexcept,
|
| idexcept-refl | 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-comm-simp | proved | all subs proved
| Idexcept,
|
| idexcept-write-at-right | proved | all subs proved
| Idexcept,
|
| idexcept-write-at | proved | all subs proved
| Idexcept,
|
| idexcept-comm | proved | all subs proved
| Idexcept,
|
| idexcept-eq-below | proved | all subs proved
| Idexcept-n,
|
| idexcept-n-shorter | proved | all subs proved
| Idexcept-n,
|
| idexcept-n-trans-successive | proved | all subs proved
| Idexcept-n,
|
| cmp-full-write | proved | all subs proved
| Cmp,
|
| cmp-at | proved | all subs proved
| Cmp-elem,
|
| idexcept-write-at0 | proved | all subs proved
| Idexcept,
|
| cmp-write-above | proved | all subs proved
| Cmp-elem,
|
| cmp-write-value | proved | all subs proved
| Cmp-elem,
|
| cmp-move-1 | proved | all subs proved
| Cmp-elem,
|
| cmp-0 | proved | all subs proved
| Cmp-elem,
|
| cmp-cmp-eq | proved | all subs proved
| Cmp,
|
| idexcept-write-at0-right | proved | all subs proved
| Idexcept,
|
| idexcept-n-trans | proved | all subs proved
| Idexcept-n,
|
| idexcept-extract-left | proved | all subs proved
| Idexcept,
|
| cmp-at-0 | proved | all subs proved
| Cmp-elem,
|
| idexcept-eq-above | proved | all subs proved
| Idexcept-n,
|
| idexcept-extract-right | proved | all subs proved
| Idexcept,
|
| idexcept-same | proved | all subs proved
| Idexcept,
|
| cmp-cmp | proved | all subs proved
| Cmp-elem,
Cmp,
|
| idexcept-n-widden | proved | all subs proved
| Idexcept-n,
|
| Cmp | axiom | | |
| Cmp-elem | axiom | | |
| Fill-zero | axiom | | |
| Fill-succ | axiom | | |
| Copy-zero | axiom | | |
| Copy-succ | axiom | | |
| Idexcept-n | axiom | | |
| Fill-all | axiom | | |
| Idexcept | axiom | | |