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: |
|---|
| cputput-reverse-r | proved | all subs proved
| eq-write-2-r,
|
| cputput-reverse-c | proved | all subs proved
| eq-write-2-c,
|
| eq-write-2-c | proved | all subs proved
| ngp-07-r,
cngetput-r,
ngp-07-c,
put-otherrow,
put-same,
put-othercol,
cgetput,
cngetput-c,
colno-put,
rowno-put,
extension,
|
| eq-write-2-r | proved | all subs proved
| ngp-07-r,
cngetput-r,
ngp-07-c,
put-othercol,
put-same,
cgetput,
put-otherrow,
cngetput-c,
colno-put,
rowno-put,
extension,
|
| size-0c | proved | all subs proved
| eq-write-left,
rowno-put,
colno-put,
gen,
rowno-mkmatrix,
colno-mkmatrix,
extension,
|
| eq-put2 | proved | all subs proved
| put-otherrow,
put-othercol,
cgetput,
cngetput-r,
put-same,
cngetput-c,
cputput,
colno-put,
rowno-put,
extension,
|
| size-0r | proved | all subs proved
| eq-write-left,
colno-put,
rowno-put,
gen,
rowno-mkmatrix,
colno-mkmatrix,
extension,
|
| cputput | proved | all subs proved
| put-otherrow,
put-othercol,
put-same,
cgetput,
colno-put,
rowno-put,
extension,
|
| ngp-07-c | proved | all subs proved
| cngetput-c,
|
| ngp-07-r | proved | all subs proved
| cngetput-r,
|
| eq-write-left | proved | all subs proved
| cngetput-r,
cngetput-c,
put-same,
putgetinv,
colno-put,
rowno-put,
extension,
|
| ngp-06-c | proved | all subs proved
| cngetput-c,
|
| ngp-08-c | proved | all subs proved
| cngetput-c,
|
| ngp-09-c | proved | all subs proved
| cngetput-c,
|
| ngp-10-rc | proved | all subs proved
| cngetput-c,
|
| ngp-10-r | proved | all subs proved
| cngetput-r,
|
| eq-write-1 | proved | all subs proved
| cngetput-r,
put-same,
cngetput-c,
colno-put,
rowno-put,
extension,
|
| ngp-08-r | proved | all subs proved
| cngetput-r,
|
| ngp-06-r | proved | all subs proved
| cngetput-r,
|
| ngp-09-r | proved | all subs proved
| cngetput-r,
|
| put-same-content | proved | all subs proved
| extension,
putgetinv,
|
| ngp-10-c | proved | all subs proved
| cngetput-c,
|
| write3 | proved | all subs proved
| put-otherrow,
put-same,
put-othercol,
cgetput,
colno-put,
rowno-put,
extension,
|
| putgetinv | proved | all subs proved
| put-otherrow,
put-othercol,
put-same,
colno-put,
rowno-put,
extension,
|
| cgetput | proved | all subs proved
| put-same,
|
| cngetput-r | proved | all subs proved
| put-otherrow,
|
| cngetput-c | proved | all subs proved
| put-othercol,
|
| cngetput-num-r | proved | all subs proved
| put-otherrow,
|
| ext-rec | proved | all subs proved
| put-otherrow,
put-othercol,
put-same,
colno-put,
rowno-put,
extension,
|
| cngetput-num-c | proved | all subs proved
| put-othercol,
|
| put-otherrow | axiom | | |
| put-same | axiom | | |
| put-othercol | axiom | | |
| extension | axiom | | |
| colno-mkmatrix | axiom | | |
| rowno-mkmatrix | axiom | | |
| gen | axiom | | |
| colno-put | axiom | | |
| rowno-put | axiom | | |