[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 ring-buffer

ring-buffer/elim is used by push-corr, pop-corr, clear-corr,
ring-buffer/sel-01 is used by test, push-corr, pop-corr, create-corr, clear-corr,
ring-buffer/sel-02 is used by test, push-corr, pop-corr, create-corr, clear-corr,
ring-buffer/sel-03 is used by test, push-corr, pop-corr, create-corr, clear-corr,
ring-buffer/sel-04 is used by test, push-corr, pop-corr, create-corr, clear-corr,
ring-buffer/upd-01 is used by test, push-corr,
ring-buffer/upd-03 is used by test, pop-corr,
ring-buffer/upd-04 is used by test, push-corr, pop-corr,
ring-buffer/updsel-01 is used by push-corr,
ring-buffer/updsel-03 is used by pop-corr,
ring-buffer/updsel-04 is used by push-corr, pop-corr, clear-corr,
ring-buffer/updsel-05 is used by push-corr,
ring-buffer/updsel-07 is used by pop-corr,
ring-buffer/updsel-08 is used by push-corr, pop-corr, clear-corr,
ring-buffer/updsel-09 is used by push-corr,
ring-buffer/updsel-11 is used by pop-corr,
ring-buffer/updsel-12 is used by push-corr, pop-corr, clear-corr,
ring-buffer/updsel-13 is used by push-corr,
ring-buffer/updsel-15 is used by pop-corr,
ring-buffer/updsel-16 is used by push-corr, pop-corr, clear-corr,

Used from specification nat-mult

nat-mult/mult-a is used by push-corr,
nat-mult/mult-c is used by push-corr,
nat-mult/numeral-26 is used by push-corr,
nat-mult/numeral-36 is used by push-corr,
nat-mult/one is used by push-corr,
nat-mult/two-02 is used by push-corr,
nat-mult/two-zero-01 is used by push-corr,

Used from specification list

list/queue/Last is used by tolist-size, tolist-rec-inv, tolist-at, push-corr,
list/queue/a is used by tolist-size, tolist-rec-inv, tolist-at, push-corr, pop-corr, head-corr,
list/queue/app-01 is used by tolist-rec-inv,
list/queue/app-03 is used by push-corr,
list/queue/c is used by pop-corr, head-corr,
list/queue/in-14 is used by pop-corr, head-corr,
list/queue/in-17 is used by pop-corr, head-corr,
list/queue/in-append is used by pop-corr, head-corr,
list/queue/len is used by tolist-size, push-corr, pop-corr, head-corr,
list/queue/len-02 is used by tolist-size, push-corr, pop-corr, head-corr,

Used from specification int-basic2

int-basic2/add-c is used by push-corr,
int-basic2/add-a is used by push-corr, pop-corr, head-corr,
int-basic2/add-c is used by push-corr, pop-corr, head-corr,
int-basic2/add-in is used by push-corr, pop-corr,
int-basic2/mone-03 is used by head-corr,

Used from specification int-div

int-div/mod-ls-zero is used by pop-corr,
int-div/div-elim is used by push-corr,
int-div/mod-les is used by pop-corr,
int-div/mod-less-01 is used by push-corr, pop-corr,
int-div/mod-zero-04 is used by push-corr,

Used from specification intnat

intnat/add-01 is used by push-corr,
intnat/i2n-mod is used by push-corr, pop-corr, int-mod-distr,
intnat/num-i2n-le is used by push-corr,
intnat/num-i2n-le-02 is used by push-corr,
intnat/num-i2n-ls-02 is used by push-corr,
intnat/num-n2i-ls-02 is used by push-corr,
intnat/abs-02 is used by pop-corr,
intnat/abs-eq is used by push-corr,
intnat/abs-zero is used by tolist-rec-inv, push-corr, head-corr,
intnat/add-nonneg-int-to-nat is used by pop-corr,
intnat/i2i-pos is used by create-corr,
intnat/i2i-pos-01 is used by push-corr,
intnat/ini2-abs is used by push-corr,
intnat/inj is used by pop-corr,
intnat/labs is used by push-corr, pop-corr, at-first-mod,
intnat/le is used by pop-corr,
intnat/le-int-le-nat is used by pop-corr,
intnat/n2i-add is used by push-corr, pop-corr, head-corr,
intnat/n2n is used by tolist-rec-inv, push-corr, pop-corr,
intnat/nat2int is used by push-corr, pop-corr, clear-corr,
intnat/nat2int-02 is used by tolist-rec-inv, push-corr, pop-corr, clear-corr,
intnat/nat2int-04 is used by pop-corr,
intnat/nat2int-07 is used by head-corr,
intnat/nat2int-08 is used by clear-corr,
intnat/num-n2i-ls-02 is used by push-corr, pop-corr, head-corr, clear-corr,
intnat/num-n2i-ls-07 is used by pop-corr,
intnat/rax-04 is used by push-corr, pop-corr,

Used from specification int-abs

int-abs/abs-16 is used by push-corr, at-first-mod,
int-abs/abs-18 is used by push-corr,
int-abs/absle is used by push-corr, pop-corr, at-first-mod,
int-abs/anti is used by push-corr,
int-abs/elim-sub is used by pop-corr,
int-abs/forward-le-01 is used by tolist-rec-inv, push-corr, pop-corr, head-corr, clear-corr, at-first-mod,
int-abs/forward-le-02 is used by push-corr, pop-corr,
int-abs/forward-le-04 is used by push-corr,
int-abs/forward-le-05 is used by tolist-rec-inv, push-corr, pop-corr, head-corr, create-corr, clear-corr, at-first-mod,
int-abs/forward-lele is used by push-corr, pop-corr, head-corr,
int-abs/forward-lels is used by push-corr, pop-corr, head-corr, at-first-mod,
int-abs/forward-lsle is used by push-corr, pop-corr, head-corr,
int-abs/lels is used by push-corr, pop-corr, head-corr, clear-corr, at-first-mod,
int-abs/lels-01 is used by push-corr, pop-corr,
int-abs/lels-02 is used by tolist-rec-inv, push-corr, pop-corr, create-corr, clear-corr,
int-abs/lels-03 is used by push-corr,
int-abs/lenls is used by push-corr,
int-abs/lep-01 is used by push-corr,
int-abs/numle-02 is used by push-corr, pop-corr,
int-abs/numleledel-01 is used by push-corr, pop-corr,
int-abs/succ-01 is used by push-corr,
int-abs/zero-gels-01 is used by push-corr, pop-corr,
int-abs/zero-gels-04 is used by push-corr, pop-corr, int-mod-distr, head-corr, clear-corr,
int-abs/zero-gs is used by push-corr, pop-corr,

Used from specification nat-basic1

nat-basic1/f is used by tolist-at, push-corr, pop-corr,
nat-basic1/lf is used by push-corr, pop-corr,
nat-basic1/lf-01 is used by push-corr,
nat-basic1/lf-02 is used by push-corr,
nat-basic1/ls-02 is used by push-corr, pop-corr,
nat-basic1/one is used by push-corr, pop-corr,
nat-basic1/ref-1 is used by pop-corr,
nat-basic1/trans-1 is used by push-corr, pop-corr,
nat-basic1/zero is used by push-corr, pop-corr, head-corr, clear-corr,
nat-basic1/zero-01 is used by tolist-at,

Used from specification nat-div

nat-div/mod-eq is used by push-corr, pop-corr,
nat-div/mod-le-02 is used by tolist-rec-inv,
nat-div/mod-rec is used by push-corr, mod-twice,
nat-div/mod-eq is used by push-corr, mod-twice, at-n-mod,
nat-div/mod-le-03 is used by tolist-rec-inv,
nat-div/mod-ls is used by push-corr,
nat-div/mod-once is used by mod-twice,

Used from specification int-basic1

int-basic1/forward-pos is used by push-corr, pop-corr,
int-basic1/irref is used by push-corr, pop-corr, head-corr, at-first-mod,
int-basic1/ls-01 is used by push-corr,

Used from specification list-data

list-data/queue/l is used by pop-corr,
list-data/queue/size-01 is used by tolist-size, create-corr, clear-corr,

Used from specification list-del

list-del/queue/extension is used by push-corr, pop-corr,
list-del/queue/get-butlast is used by tolist-at,
list-del/queue/get-last is used by tolist-at,
list-del/queue/get-append-grt is used by tolist-at,
list-del/queue/get-succ is used by pop-corr,
list-del/queue/get-zero-01 is used by pop-corr, head-corr,
list-del/queue/one-03 is used by tolist-at,

Used from specification array

array/cngetput is used by push-corr,
array/Size-mkarray is used by test, create-corr,
array/Size-put is used by test, push-corr,
array/cgetput is used by test, push-corr,
array/ngp is used by test,
array/ngp-01 is used by test,

Used from specification nat

nat/pls is used by push-corr,
nat/anti is used by tolist-at, push-corr,
nat/elim-sub is used by push-corr, mod-twice,
nat/fle is used by push-corr,
nat/fle-01 is used by push-corr,
nat/le-add is used by mod-twice,
nat/le-ls-simp is used by push-corr,
nat/lels is used by tolist-rec-inv, tolist-ext-one, tolist-at, push-corr, pop-corr, mod-twice,
nat/lels-01 is used by push-corr, mod-twice,
nat/lels-03 is used by push-corr,
nat/lep is used by push-corr, mod-twice,
nat/ler is used by tolist-rec-inv, tolist-at, push-corr,
nat/let is used by tolist-rec-inv,
nat/ls-le-simp is used by tolist-ext-one, push-corr, pop-corr,
nat/succ-01 is used by pop-corr,
nat/zero is used by tolist-at,

Used from specification nat-basic2

nat-basic2/a is used by tolist-size, tolist-at, push-corr, pop-corr, mod-twice, head-corr,
nat-basic2/c is used by tolist-size, tolist-rec-inv, tolist-ext-one, tolist-at, push-corr, pop-corr, mod-twice, head-corr,
nat-basic2/eq-01 is used by tolist-size, push-corr,
nat-basic2/eqs is used by push-corr,
nat-basic2/l is used by push-corr, pop-corr,
nat-basic2/l-01 is used by push-corr,
nat-basic2/l-02 is used by push-corr,
nat-basic2/oz is used by pop-corr,
nat-basic2/s is used by tolist-at,
nat-basic2/succ is used by tolist-size, tolist-at, push-corr, pop-corr,
nat-basic2/z is used by pop-corr, head-corr,

Used from specification ring-buffer-inv

ring-buffer-inv/inv is used by tolist-rec-inv, push-corr, pop-corr, head-corr, create-corr, clear-corr, at-first-mod,