[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 store+set

store+set/sparsearray/Diff-ext is used by step-L2-L3,
store+set/sparsearray/Diff-get is used by step-L2-L3,
store+set/sparsearray/Dom is used by step-L2-L3,
store+set/sparsearray/diff-subset is used by rely-L2-L3,

Used from specification nat-basic

nat-basic/f is used by step-L6-L7,

Used from specification store

store/sparsearray/Del-at is used by step-L6-L7,
store/sparsearray/Extension is used by step-L6-L7, step-L2-L3, step-L4-L0, init,
store/sparsearray/Subset is used by step-L6-L7, step-L2-L3,
store/sparsearray/notmemlookup is used by step-L6-L7, step-L2-L3,
store/sparsearray/Del-at-strong is used by step-L6-L7,
store/sparsearray/Del-in is used by step-L6-L7,
store/sparsearray/In-empty is used by step-L2-L3, step-L4-L0, init,
store/sparsearray/lookupisempty is used by step-L6-L7,
store/sparsearray/notin-del-notin is used by step-L6-L7,
store/sparsearray/notmemlookup is used by step-L6-L7, step-L2-L3, step-L4-L0, init,
store/sparsearray/sub-ref is used by rely-L5-L6, rely-L6-L7, rely-L6-L3, rely-reflexive, rely-L2-L1, init,
store/sparsearray/sub-trans is used by stable-L1, stable-L4, stable-L8, stable-L7-01, stable-L5, stable-L3, step-L2-L3,
store/sparsearray/subset-empty is used by step-L1-L8, stable-L8,
store/sparsearray/subset-empty-01 is used by stable-L8,
store/sparsearray/superset-elem-in-01 is used by step-L2-L3,

Used from specification natpair

Used from specification VerifyThis3-sequential

VerifyThis3-sequential/addzero is used by init,
VerifyThis3-sequential/main-lemma is used by step-L6-L7,
VerifyThis3-sequential/okspmx-def is used by step-L6-L7,
VerifyThis3-sequential/toMatrix-colno is used by init,
VerifyThis3-sequential/toMatrix-rowno is used by init,

Used from specification tidset-npset

tidset-npset/alldisjointp-def is used by step-L6-L7, init,
tidset-npset/alldisjointp-reduce is used by step-L6-L7, step-L2-L3,
tidset-npset/bigunion-get is used by step-L6-L7, step-L2-L3,
tidset-npset/bigunion-in is used by init,
tidset-npset/disjointp-def is used by step-L6-L7, step-L2-L3,
tidset-npset/disjointp-reduce is used by step-L6-L7,
tidset-npset/in-union is used by step-L6-L7, step-L2-L3,
tidset-npset/bigunion-in is used by step-L6-L7, step-L2-L3,
tidset-npset/disjoint-empty-l is used by init,
tidset-npset/disjoint-empty-r is used by step-L1-L8, stable-L8,
tidset-npset/union-empty-l is used by init,
tidset-npset/union-empty-r is used by step-L1-L8, stable-L8,
tidset-npset/union-lookup is used by step-L6-L7, step-L2-L3,
tidset-npset/union-subset is used by rely-L5-L6, step-L1-L8, step-L6-L7, rely-L6-L7, rely-L6-L3, step-L7-L3, stable-L1, stable-L4, rely-reflexive, stable-L8, stable-L7-01, stable-L5, stable-L3, rely-L2-L1, step-L2-L1, rely-L2-L3, step-L2-L3, step-L3-L1, step-L3-L4, step-L6-L3, step-L4-L0, step-L4-L5, step-L5-L6, step-L1-L2,

Used from specification array

array/matrixops/Size-mkarray is used by init,
array/matrixops/Size-put is used by step-L6-L7,

Used from specification matrixops

matrixops/multmxvec-size is used by init,