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: |
|---|
| perm-updcol | proved | all subs proved
| perm-toArr-toArc,
perm-updcol-aux,
|
| perm-toArr-toArc | proved | all subs proved
| oc-toArr-toArc,
|
| oc-toArr-toArc | proved | all subs proved
| oc-put-toArc,
oc-put-toAr,
put-outside-id,
init-toArc,
init-toArr,
|
| perm-updcol-aux | proved | all subs proved
| perm-updcol-ind,
colno-updcol,
toArc-def,
|
| perm-updrow | proved | all subs proved
| perm-updrow-ind,
rowno-updrow,
toArr-def,
|
| perm-updcol-ind | proved | all subs proved
| putcol-getcol,
toArc-rec,
toArc-base,
toArc-outside-gen,
|
| perm-updrow-ind | proved | all subs proved
| putrow-getrow,
toArr-rec,
toArr-base,
toArr-outside-gen,
|
| oc-put-toAr | proved | all subs proved
| oc-put-toArr-rec,
toArr-def,
|
| oc-put-toArc | proved | all subs proved
| oc-put-toArc-rec,
toArc-def,
|
| toArc-outside | proved | all subs proved
| toArc-outside-gen,
|
| toArr-outside | proved | all subs proved
| toArr-outside-gen,
|
| getmx-inmx | proved | all subs proved
| in-toArr,
|
| in-toArr | proved | all subs proved
| in-toArr-ind,
toArr-def,
|
| oc-put-toArr-rec | proved | all subs proved
| oc-toArr-positive,
getrow-putsame,
put-selrow,
toArr-rec,
toArr-base,
|
| toArr-outside-gen | proved | all subs proved
| putrow-getrow,
toArr-rec,
toArr-base,
|
| oc-put-toArc-rec | proved | all subs proved
| oc-toArc-positive,
getcol-putsame,
put-selcol,
toArc-rec,
toArc-base,
|
| init-toArr | proved | all subs proved
| init-toArr-rec,
toArr-def,
|
| init-toArc | proved | all subs proved
| init-toArc-rec,
toArc-def,
|
| toArc-outside-gen | proved | all subs proved
| putcol-getcol,
toArc-rec,
toArc-base,
|
| putcol-getcol-same | proved | all subs proved
| putcol-getcol,
|
| putrow-getrow-same | proved | all subs proved
| putrow-getrow,
|
| putrow-getrow-other | proved | all subs proved
| putrow-getrow,
|
| putcol-getcol-ls | proved | all subs proved
| putcol-getcol,
|
| putrow-getrow-ls | proved | all subs proved
| putrow-getrow,
|
| putcol-getcol-gr | proved | all subs proved
| putcol-getcol,
|
| putrow-getrow-gr | proved | all subs proved
| putrow-getrow,
|
| putcol-getcol-other | proved | all subs proved
| putcol-getcol,
|
| in-toArr-ind | proved | all subs proved
| toArr-rec,
toArr-base,
|
| oc-toArc-positive | proved | all subs proved
| toArc-rec,
|
| oc-toArr-positive | proved | all subs proved
| toArr-rec,
|
| init-toArc-rec | proved | all subs proved
| selcol-mkmatrix,
toArc-rec,
toArc-base,
|
| init-toArr-rec | proved | all subs proved
| selrow-mkmatrix,
toArr-rec,
toArr-base,
|
| putrow-getrow | proved | all subs proved
| updrow-sel,
colno-updrow,
|
| putcol-getcol | proved | all subs proved
| updcol-sel,
rowno-updcol,
|
| size-toAr | proved | all subs proved
| toArr-rec,
toArr-base,
|
| putrow-outside-id | proved | all subs proved
| updrow-sel,
colno-updrow,
rowno-updrow,
|
| putcol-id | proved | all subs proved
| updcol-sel,
colno-updcol,
rowno-updcol,
|
| putrow-id | proved | all subs proved
| updrow-sel,
colno-updrow,
rowno-updrow,
|
| size-toArc | proved | all subs proved
| toArc-rec,
toArc-base,
|
| putcol-outside-id | proved | all subs proved
| updcol-sel,
colno-updcol,
rowno-updcol,
|
| put-selcol | proved | all subs proved
| |
| getcol-putsame | proved | all subs proved
| |
| rowno-updcol | axiom | | |
| updcol-sel | axiom | | |
| put-selrow | proved | all subs proved
| |
| getrow-putsame | proved | all subs proved
| |
| colno-updcol | axiom | | |
| selcol-mkmatrix | proved | all subs proved
| |
| rowno-updrow | axiom | | |
| selrow-mkmatrix | proved | all subs proved
| |
| toArc-def | axiom | | |
| colno-updrow | axiom | | |
| updrow-sel | axiom | | |
| toArr-def | axiom | | |
| put-outside-id | proved | all subs proved
| |
| toArr-base | axiom | | |
| toArr-rec | axiom | | |
| toArc-base | axiom | | |
| toArc-rec | axiom | | |