[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 nat-basic

nat-basic/addex is used by bubblesort-correct,
nat-basic/a is used by bubblesort-correct,
nat-basic/add-base is used by bubblesort-correct,
nat-basic/between is used by bubblesort-correct,
nat-basic/c is used by bubblesort-correct,
nat-basic/eq-01 is used by bubblesort-correct,
nat-basic/eq-02 is used by bubblesort-correct,
nat-basic/f is used by bubblesort-correct,
nat-basic/l is used by bubblesort-correct,
nat-basic/l-01 is used by bubblesort-correct,
nat-basic/l-02 is used by bubblesort-correct,
nat-basic/l-05 is used by bubblesort-correct,
nat-basic/l-06 is used by bubblesort-correct,
nat-basic/l-08 is used by bubblesort-correct,
nat-basic/less-zero is used by bubblesort-correct,
nat-basic/lf is used by bubblesort-correct,
nat-basic/lf-01 is used by bubblesort-correct,
nat-basic/lf-02 is used by bubblesort-correct,
nat-basic/ls-02 is used by bubblesort-correct,
nat-basic/neq-04 is used by bubblesort-correct,
nat-basic/nls-fst is used by bubblesort-correct,
nat-basic/one is used by bubblesort-correct,
nat-basic/one-01 is used by bubblesort-correct,
nat-basic/one-03 is used by bubblesort-correct,
nat-basic/one-06 is used by bubblesort-correct,
nat-basic/oz is used by bubblesort-correct,
nat-basic/pred is used by bubblesort-correct,
nat-basic/refl-nat is used by bubblesort-correct,
nat-basic/s-04 is used by bubblesort-correct,
nat-basic/succ is used by bubblesort-correct,
nat-basic/trans-nat is used by bubblesort-correct,
nat-basic/z-01 is used by bubblesort-correct,
nat-basic/zero is used by bubblesort-correct,

Used from specification tord

tord/irreflexivity is used by bubblesort-correct,
tord/nll is used by bubblesort-correct,
tord/transitivity is used by bubblesort-correct,

Used from specification nat

nat/le-addex is used by bubblesort-correct,
nat/add-01 is used by bubblesort-correct,
nat/add-num-03 is used by bubblesort-correct,
nat/anti is used by bubblesort-correct,
nat/elim-pred-c is used by bubblesort-correct,
nat/elim-sub is used by bubblesort-correct,
nat/eq is used by bubblesort-correct,
nat/eq-01 is used by bubblesort-correct,
nat/eqle-one is used by bubblesort-correct,
nat/fle is used by bubblesort-correct,
nat/fle-01 is used by bubblesort-correct,
nat/ge is used by bubblesort-correct,
nat/gr-def is used by bubblesort-correct,
nat/l-num-01 is used by bubblesort-correct,
nat/le-add is used by bubblesort-correct,
nat/le-def is used by bubblesort-correct,
nat/le-ls-simp is used by bubblesort-correct,
nat/le-num-06 is used by bubblesort-correct,
nat/le-one is used by bubblesort-correct,
nat/lels is used by bubblesort-correct,
nat/lels-02 is used by bubblesort-correct,
nat/lels-03 is used by bubblesort-correct,
nat/lep is used by bubblesort-correct,
nat/lep-02 is used by bubblesort-correct,
nat/ler is used by bubblesort-correct,
nat/les is used by bubblesort-correct,
nat/let is used by bubblesort-correct,
nat/lez is used by bubblesort-correct,
nat/ls is used by bubblesort-correct,
nat/ls-01 is used by bubblesort-correct,
nat/ls-02 is used by bubblesort-correct,
nat/ls-03 is used by bubblesort-correct,
nat/ls-le-simp is used by bubblesort-correct,
nat/not-zero is used by bubblesort-correct,
nat/pred-03 is used by bubblesort-correct,
nat/prop-07 is used by bubblesort-correct,
nat/succ-01 is used by bubblesort-correct,
nat/zero is used by bubblesort-correct,

Used from specification list-last

list-last/list-as-arrayinstance/last-elim is used by bubblesort-correct,

Used from specification list-data

list-data/oarray-sort/elim-add is used by bubblesort-correct,
list-data/oarray-sort/elim-list-c is used by bubblesort-correct,
list-data/oarray-sort/l is used by bubblesort-correct,
list-data/oarray-sort/lf-01 is used by bubblesort-correct,
list-data/oarray-sort/size-nil is used by bubblesort-correct,

Used from specification list

list/list-as-arrayinstance/Last is used by bubblesort-correct,
list/list-as-arrayinstance/Nil is used by bubblesort-correct,
list/list-as-arrayinstance/a is used by bubblesort-correct,
list/list-as-arrayinstance/app is used by bubblesort-correct,
list/list-as-arrayinstance/app-02 is used by bubblesort-correct,
list/list-as-arrayinstance/c is used by bubblesort-correct,
list/list-as-arrayinstance/c-03 is used by bubblesort-correct,
list/list-as-arrayinstance/e is used by bubblesort-correct,
list/list-as-arrayinstance/len is used by bubblesort-correct,
list/list-as-arrayinstance/len-02 is used by bubblesort-correct,
list/list-as-arrayinstance/len-05 is used by bubblesort-correct,

Used from specification olist-min-max

olist-min-max/oarray-sort/allle-range-def is used by bubblesort-correct,
olist-min-max/oarray-sort/allle-empty is used by bubblesort-correct,
olist-min-max/oarray-sort/allle-numone is used by bubblesort-correct,

Used from specification list-perm

list-perm/list-as-arrayinstance/perm-switch is used by bubblesort-correct,
list-perm/list-as-arrayinstance/trans is used by bubblesort-correct,
list-perm/list-as-arrayinstance/app-end-end is used by bubblesort-correct,
list-perm/list-as-arrayinstance/perm-one is used by bubblesort-correct,
list-perm/list-as-arrayinstance/ref is used by bubblesort-correct,

Used from specification olist

olist/oarray-sort/ole-last-01 is used by bubblesort-correct,
olist/oarray-sort/orderedle-all is used by bubblesort-correct,
olist/oarray-sort/orderedle-append is used by bubblesort-correct,
olist/oarray-sort/le-e is used by bubblesort-correct,
olist/oarray-sort/le-o is used by bubblesort-correct,
olist/oarray-sort/le-r is used by bubblesort-correct,
olist/oarray-sort/orderedle-append2-split is used by bubblesort-correct,

Used from specification list-getput

list-getput/oarray-sort/get-zero-01 is used by bubblesort-correct,

Used from specification array

array/Put-other is used by bubblesort-correct,
array/Put-same is used by bubblesort-correct,
array/Size-put is used by bubblesort-correct,
array/cgetput is used by bubblesort-correct,
array/ngp-06 is used by bubblesort-correct,
array/ngp-08 is used by bubblesort-correct,

Used from specification list-del

list-del/list-as-arrayinstance/first-append is used by bubblesort-correct,
list-del/list-as-arrayinstance/firstn-last is used by bubblesort-correct,
list-del/list-as-arrayinstance/firstn-last-rec is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-append-grt is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-append-less is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-firstn is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-restn is used by bubblesort-correct,
list-del/list-as-arrayinstance/put-app-left is used by bubblesort-correct,
list-del/list-as-arrayinstance/rest-empty is used by bubblesort-correct,
list-del/list-as-arrayinstance/rest-len is used by bubblesort-correct,
list-del/list-as-arrayinstance/restN-append is used by bubblesort-correct,
list-del/list-as-arrayinstance/elim-firstn-restn is used by bubblesort-correct,
list-del/list-as-arrayinstance/first-length is used by bubblesort-correct,
list-del/list-as-arrayinstance/firstN-empty is used by bubblesort-correct,
list-del/list-as-arrayinstance/firstN-len is used by bubblesort-correct,
list-del/list-as-arrayinstance/firstN-zero is used by bubblesort-correct,
list-del/list-as-arrayinstance/firstn-one-01 is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-app is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-append-grt-02 is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-succ is used by bubblesort-correct,
list-del/list-as-arrayinstance/get-zero is used by bubblesort-correct,
list-del/list-as-arrayinstance/restN-all is used by bubblesort-correct,
list-del/list-as-arrayinstance/restN-zero is used by bubblesort-correct,
list-del/list-as-arrayinstance/restn-at is used by bubblesort-correct,