[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 natset

natset/range-recend is used by singletonmxvec-get-sum-aux,
natset/range-def is used by distrmxmx-r, distrmxmx-l, distrvevecmx, singletonmxvec-get-sum-aux, distrvecmxmx, mult-assoc, distrmxmxvec, distrmxvecvec,
natset/range-empty is used by singletonmxvec-get-sum-aux,

Used from specification nat-basic

nat-basic/a is used by singletonmxvec-get-sum-aux,
nat-basic/add-base is used by singletonmxvec-get-sum-aux,
nat-basic/c is used by singletonmxvec-get-sum-aux,
nat-basic/f is used by distrmxmx-r, distrmxmx-l, addmx-com, distrvevecmx, singletonmxvec-get-sum-aux, singletonmxvec-get, distrvecmxmx, multmx-row, mult-assoc, distrmxmxvec, addvec-assoc, distrmxvecvec, addvec-com, addmx-assoc, multmx-column,
nat-basic/less-zero is used by singletonmxvec-get-sum-aux,
nat-basic/lf is used by distrvecmxmx,
nat-basic/lf-01 is used by distrmxmx-r, distrmxmx-l, addmx-com, distrvevecmx, distrvecmxmx, mult-assoc, distrmxmxvec, addvec-assoc, distrmxvecvec, addvec-com, addmx-assoc,
nat-basic/lf-02 is used by distrvecmxmx,
nat-basic/ls-02 is used by singletonmxvec-get-sum-aux, distrvecmxmx,
nat-basic/neq-01 is used by singletonmxvec-get-sum-aux,
nat-basic/oz is used by singletonmxvec-get-sum-aux,
nat-basic/refl-nat is used by distrmxmx-r, distrmxmx-l, singletonmxvec-get-sum-aux, distrmxmxvec, addvec-assoc,
nat-basic/s-04 is used by singletonmxvec-get-sum-aux,
nat-basic/succ is used by singletonmxvec-get-sum-aux,
nat-basic/trans-nat is used by distrvecmxmx,
nat-basic/zero is used by singletonmxvec-get-sum-aux,

Used from specification matrix+array

matrix+array/matrixops/selcol-get is used by multmx-column,
matrix+array/matrixops/selcol-size is used by multmx-column,
matrix+array/matrixops/selrow-get is used by multmx-row,
matrix+array/matrixops/selrow-size is used by multmx-row,

Used from specification set-union

set-union/natset/Difference is used by sum-union,
set-union/natset/diff-del-plus-1 is used by sum-union,
set-union/natset/diff-del-plus-2 is used by sum-union,
set-union/natset/diff-e-01 is used by sum-union,
set-union/natset/una is used by sum-union,
set-union/natset/unadd is used by sum-union,
set-union/natset/unc is used by sum-union,
set-union/natset/une is used by sum-union,
set-union/natset/unin is used by sum-union,
set-union/natset/unin-01 is used by sum-union,

Used from specification nat

nat/add-01 is used by singletonmxvec-get-sum-aux,
nat/fle is used by distrmxmx-r, distrmxmx-l, distrvecmxmx, distrmxmxvec, addvec-assoc,
nat/fle-01 is used by distrmxmx-r, distrmxmx-l, distrvevecmx, distrvecmxmx, distrmxmxvec, addvec-assoc, distrmxvecvec,
nat/lels is used by distrmxmx-r, distrmxmx-l, distrvevecmx, distrvecmxmx, distrmxmxvec, addvec-assoc, distrmxvecvec,
nat/lels-03 is used by singletonmxvec-get-sum-aux,
nat/ler is used by singletonmxvec-get,
nat/lez is used by distrmxmx-r, distrmxmx-l, distrvevecmx, singletonmxvec-get-sum-aux, distrvecmxmx, mult-assoc, distrmxmxvec, distrmxvecvec,
nat/ls-le-simp is used by distrvevecmx, distrmxvecvec,
nat/succ-01 is used by singletonmxvec-get-sum-aux,

Used from specification set-basic

set-basic/natset/eq is used by sum-red, sum-multr, singletonmxvec-get-sum-aux, sum-switch, sum-multl, sum-union, sum-add,
set-basic/natset/In-insert is used by sum-red,
set-basic/natset/ne-01 is used by sum-red, sum-multr, sum-switch, sum-multl, sum-union, sum-add,
set-basic/natset/size-zero-01 is used by sum-red, sum-multr, sum-switch, sum-multl, sum-union, sum-add,

Used from specification matrix

matrix/cngetput-c is used by singletonmxvec-get-sum-aux,
matrix/cngetput-num-r is used by singletonmxvec-get-sum-aux,
matrix/extension is used by distrmxmx-r, distrmxmx-l, addmx-com, mult-assoc, addmx-assoc,
matrix/cgetput is used by singletonmxvec-get-sum-aux,
matrix/colno-mkmatrix is used by singletonmxvec-get-sum-aux, singletonmxvec-get,
matrix/colno-put is used by singletonmxvec-get,
matrix/get-mkmatrix is used by singletonmxvec-get-sum-aux,
matrix/put-otherrow is used by singletonmxvec-get-sum-aux,
matrix/rowno-mkmatrix is used by singletonmxvec-get-sum-aux, singletonmxvec-get,
matrix/rowno-put is used by singletonmxvec-get,

Used from specification ring

ring/distr-l is used by distrmxmx-l, sum-multr, distrvevecmx, distrmxmxvec,
ring/distr-r is used by distrmxmx-r, sum-multl, distrvecmxmx, distrmxvecvec,
ring/addassoc is used by singletonmxvec-get-sum-aux, sum-switch, sum-union, addvec-assoc, addmx-assoc, sum-add,
ring/addcom is used by addmx-com, singletonmxvec-get-sum-aux, sum-switch, sum-union, addvec-assoc, addvec-com, addmx-assoc, sum-add,
ring/addzero-r is used by singletonmxvec-get-sum-aux, sum-switch, sum-union, sum-add,
ring/multassoc is used by sum-multr, singletonmxvec-get-sum-aux, sum-multl, mult-assoc,
ring/multzero-l is used by sum-multr, singletonmxvec-get-sum-aux,
ring/multzero-r is used by sum-multl,

Used from specification array

array/matrixops/Extension is used by distrvevecmx, distrvecmxmx, multmx-row, distrmxmxvec, addvec-assoc, distrmxvecvec, addvec-com, multmx-column,