[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 array-copy

array-copy/suffix-array-base/at-subarray is used by sar-elems-bagle-twice-same,
array-copy/suffix-array-base/subarray-subarray-elim is used by sar-elems-bagle-twice-same,
array-copy/suffix-array-base/size-subarray is used by sar-elems-bagle-twice-same,
array-copy/suffix-array-base/subarray-elim is used by sar-elems-bagle-twice-same,

Used from specification bag-basic

bag-basic/suffix-array-base/count-insert is used by bagle-count,
bag-basic/suffix-array-base/count-empty is used by bagle-count,
bag-basic/suffix-array-base/count-same is used by sar-elems-bagle-twice-same,

Used from specification bag-union

bag-union/suffix-array-base/in is used by bagle-in,
bag-union/suffix-array-base/size-empty is used by bagle-size,
bag-union/suffix-array-base/size-rec is used by bagle-size,
bag-union/suffix-array-base/union-ass is used by sar-elems-bagle-twice-same,
bag-union/suffix-array-base/union-com is used by sar-elems-bagle-twice-same,
bag-union/suffix-array-base/union-rec is used by sar-elems-bagle-twice-same,

Used from specification nat-basic1

nat-basic1/f is used by valid-suffix-ls, valid-sar-twice-same, valid-sar-index-exists, valid-sar-at-ls, valid-sar-at-le, sar-elems-bagle-twice-same, sar-elems-bagle-ls, bagle-count,
nat-basic1/lf is used by valid-sar-at-le, sar-elems-bagle-twice-same,
nat-basic1/lf-01 is used by valid-suffix-ls, valid-sar-twice-same, valid-sar-index-exists, valid-sar-at-ls, valid-sar-at-le, sar-elems-bagle-twice-same,
nat-basic1/lf-02 is used by valid-sar-at-le, sar-elems-bagle-twice-same,
nat-basic1/ls-02 is used by valid-sar-at-le, sar-elems-bagle-twice-same, bagle-count,
nat-basic1/neq-01 is used by sar-elems-bagle-twice-same, bagle-count,
nat-basic1/one is used by sar-elems-bagle-twice-same,
nat-basic1/ref-1 is used by valid-sar-at-ls, valid-sar-at-le, sar-elems-bagle-twice-same, bagle-count,
nat-basic1/trans-1 is used by valid-sar-at-le, sar-elems-bagle-twice-same,
nat-basic1/zero-01 is used by bagle-count,

Used from specification nat

nat/add-num-03 is used by sar-elems-bagle-twice-same,
nat/elim-pred-c is used by sar-elems-bagle-twice-same,
nat/elim-sub is used by sar-elems-bagle-twice-same,
nat/eq-02 is used by sar-elems-bagle-twice-same,
nat/fle is used by valid-sar-at-ls, valid-sar-at-le, sar-elems-bagle-twice-same, sar-elems-bagle-ls,
nat/fle-01 is used by valid-sar-at-ls, valid-sar-at-le,
nat/ge is used by sar-elems-bagle-twice-same,
nat/le-ls-simp is used by valid-sar-at-ls, sar-elems-bagle-twice-same, sar-elems-bagle-ls,
nat/le-num-01 is used by sar-elems-bagle-twice-same,
nat/lels is used by valid-sar-index-exists, valid-sar-at-ls, valid-sar-at-le, sar-elems-bagle-twice-same, sar-elems-bagle-ls,
nat/lels-01 is used by valid-sar-at-le, sar-elems-bagle-twice-same,
nat/lels-03 is used by sar-elems-bagle-twice-same,
nat/lep is used by sar-elems-bagle-twice-same,
nat/lep-02 is used by sar-elems-bagle-twice-same,
nat/ler is used by sar-elems-bagle-twice-same,
nat/ls-01 is used by sar-elems-bagle-twice-same,
nat/ls-02 is used by sar-elems-bagle-twice-same,
nat/ls-03 is used by sar-elems-bagle-twice-same,
nat/ls-le-simp is used by valid-sar-index-exists,
nat/not-zero is used by sar-elems-bagle-twice-same,
nat/prop-07 is used by sar-elems-bagle-twice-same,
nat/succ-01 is used by sar-elems-bagle-twice-same,
nat/zero-01 is used by sar-elems-bagle-twice-same,

Used from specification nat-basic2

nat-basic2/a is used by valid-sar-twice-same1, sar-elems-bagle-twice-same, bagle-size, bagle-count,
nat-basic2/ax-08 is used by sar-elems-bagle-twice-same, bagle-count,
nat-basic2/c is used by valid-sar-twice-same1, sar-elems-bagle-twice-same, bagle-size, bagle-count,
nat-basic2/eq is used by valid-sar-twice-same1, sar-elems-bagle-twice-same,
nat-basic2/eq-01 is used by sar-elems-bagle-twice-same, bagle-size,
nat-basic2/l is used by sar-elems-bagle-twice-same,
nat-basic2/l-01 is used by sar-elems-bagle-twice-same,
nat-basic2/l-02 is used by sar-elems-bagle-twice-same,
nat-basic2/neq-01 is used by sar-elems-bagle-twice-same,
nat-basic2/nls-fst is used by valid-sar-twice-same1,
nat-basic2/one is used by sar-elems-bagle-twice-same, bagle-count,
nat-basic2/one-03 is used by sar-elems-bagle-twice-same,
nat-basic2/oz is used by sar-elems-bagle-twice-same,
nat-basic2/s is used by sar-elems-bagle-twice-same, bagle-count,
nat-basic2/succ is used by valid-sar-at-le, sar-elems-bagle-twice-same, bagle-size, bagle-count,
nat-basic2/succ-03 is used by sar-elems-bagle-twice-same,

Used from specification bag-array

bag-array/suffix-array-base/ar-elems-extract1 is used by sar-elems-bagle-twice-same,
bag-array/suffix-array-base/ar-elems-in is used by sar-elems-bagle-ls,
bag-array/suffix-array-base/ar-elems-in-exists is used by valid-sar-index-exists,
bag-array/suffix-array-base/ar-elems-size is used by sar-elems-bagle-size,