[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 mult-emptymx-ind,
natset/range-def is used by mult-emptymx-ind,
natset/range-empty is used by mult-emptymx-ind,

Used from specification nat-basic

nat-basic/a is used by mult-emptymx-ind, correct,
nat-basic/add-base is used by mult-emptymx-ind,
nat-basic/c is used by mult-emptymx-ind, correct,
nat-basic/f is used by toMatrix-add, multzero, mult-emptymx-ind, main-lemma, addzero, correct,
nat-basic/lf-02 is used by toMatrix-add,
nat-basic/one-01 is used by correct,
nat-basic/oz is used by mult-emptymx-ind,
nat-basic/ref is used by mult-emptymx-ind, correct,
nat-basic/s-04 is used by correct,
nat-basic/succ is used by mult-emptymx-ind,
nat-basic/zero is used by mult-emptymx-ind,

Used from specification nat

nat/add-01 is used by mult-emptymx-ind,
nat/fle-01 is used by main-lemma,
nat/le-def is used by correct,
nat/le-ls-simp is used by correct,
nat/lels is used by main-lemma, addzero, correct,
nat/lels-03 is used by mult-emptymx-ind,
nat/ler is used by multzero,
nat/lez is used by mult-emptymx-ind,
nat/ls-01 is used by correct,
nat/ls-le-simp is used by main-lemma, addzero,
nat/pred-03 is used by correct,
nat/succ-01 is used by mult-emptymx-ind,

Used from specification store

store/sparsearray/Extension is used by correct,
store/sparsearray/exin is used by main-lemma,
store/sparsearray/At-in-out is used by toMatrix-add,
store/sparsearray/Del-rec-same is used by main-lemma,
store/sparsearray/In-empty is used by mult-emptymx-ind, correct,
store/sparsearray/In-insert is used by toMatrix-add,
store/sparsearray/empty is used by correct,
store/sparsearray/k-At-same is used by toMatrix-add, main-lemma,
store/sparsearray/notin-del-notin is used by main-lemma,
store/sparsearray/notmemlookup is used by toMatrix-add, correct,
store/sparsearray/size is used by correct,
store/sparsearray/sub-ref is used by correct,
store/sparsearray/subset-delete-02 is used by correct,
store/sparsearray/subset-empty is used by correct,
store/sparsearray/superset-elem-in-01 is used by correct,

Used from specification natpair

natpair/elim is used by correct,
natpair/inj is used by toMatrix-add,
natpair/sel-01 is used by correct,
natpair/sel-02 is used by correct,

Used from specification set-basic

set-basic/natset/eq is used by mult-emptymx-ind,

Used from specification matrix

matrix/cngetput-c is used by toMatrix-add,
matrix/cngetput-num-r is used by toMatrix-add,
matrix/extension is used by toMatrix-add,
matrix/cgetput is used by toMatrix-add,
matrix/colno-mkmatrix is used by toMatrix-add, main-lemma,
matrix/colno-put is used by main-lemma,
matrix/get-mkmatrix is used by toMatrix-add,
matrix/put-otherrow is used by toMatrix-add,
matrix/rowno-mkmatrix is used by toMatrix-add, main-lemma,
matrix/rowno-put is used by main-lemma,

Used from specification ring

ring/addassoc is used by toMatrix-add, mult-emptymx-ind, main-lemma, addzero, correct,
ring/addcom is used by toMatrix-add, mult-emptymx-ind, main-lemma, addzero, correct,
ring/addzero-r is used by toMatrix-add, mult-emptymx-ind, main-lemma, addzero,
ring/multassoc is used by mult-emptymx-ind, correct,
ring/multzero-l is used by mult-emptymx-ind,

Used from specification matrixops

matrixops/addmvec-get is used by main-lemma, addzero,
matrixops/addmx-get is used by toMatrix-add,
matrixops/addvec-com is used by correct,
matrixops/distrmxmxvec is used by main-lemma,
matrixops/multmxvec-get is used by multzero,
matrixops/multmxvec-size is used by multzero, main-lemma, correct,
matrixops/singletonmxvec-get is used by main-lemma,
matrixops/sum-rec is used by mult-emptymx-ind,
matrixops/addmvec-get is used by main-lemma,
matrixops/addmx-colno is used by toMatrix-add,
matrixops/addmx-rowno is used by toMatrix-add,
matrixops/addvec-size is used by main-lemma, addzero,
matrixops/sum-base is used by mult-emptymx-ind,

Used from specification array

array/matrixops/Extension is used by multzero, main-lemma, addzero,
array/matrixops/Put-other is used by main-lemma,
array/matrixops/Put-same is used by main-lemma,
array/matrixops/Size-mkarray is used by multzero, addzero, correct,
array/matrixops/Size-put is used by main-lemma, correct,