[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification nat-basic

nat-basic/f is used by extension,
nat-basic/lf-01 is used by extension,

Used from specification matrix+array

matrix+array/selcol-get is used by selrow-get,
matrix+array/selcol-size is used by selrow-size,
matrix+array/selrow-get is used by selcol-get,
matrix+array/selrow-size is used by selcol-size,

Used from specification matrix-revops

matrix-revops/revput-def is used by put-otherrow, Uniform-matrix, colno-put, revput-def, put-othercol, put-same, rowno-put,
matrix-revops/revselect-def is used by put-otherrow, selcol-get, put-othercol, put-same, extension, updrow-sel, get-mkmatrix, selrow-get, revselect-def, updcol-sel,

Used from specification rowcol-upd

rowcol-upd/colno-updcol is used by rowno-updrow,
rowcol-upd/colno-updrow is used by rowno-updcol,
rowcol-upd/rowno-updcol is used by colno-updrow,
rowcol-upd/rowno-updrow is used by colno-updcol,
rowcol-upd/updcol-sel is used by updrow-sel,
rowcol-upd/updrow-sel is used by updcol-sel,

Used from specification matrix

matrix/extension is used by extension,
matrix/colno-mkmatrix is used by rowno-mkmatrix,
matrix/colno-put is used by rowno-put,
matrix/eq-write-1 is used by revput-def,
matrix/get-mkmatrix is used by get-mkmatrix,
matrix/put-othercol is used by put-otherrow,
matrix/put-otherrow is used by put-othercol,
matrix/put-same is used by put-same,
matrix/rowno-mkmatrix is used by colno-mkmatrix,
matrix/rowno-put is used by colno-put,