[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

array/array_of_nat/Extension is used by REFINE-example,
array/array_of_nat/Put-other is used by REFINE-example,
array/array_of_nat/Size-mkarray is used by REFINE-example,
array/array_of_nat/Size-put is used by REFINE-example,
array/array_of_nat/cgetput is used by REFINE-example,
array/array_of_nat/cngetput-num is used by REFINE-example,
array/array_of_nat/cputput is used by REFINE-example,

Used from specification list-del

list-del/partition/get-numrec is used by REFINE-example,
list-del/partition/get-zero-01 is used by REFINE-example,
list-del/partition/one-03 is used by REFINE-example,
list-del/partition/put-one-01 is used by REFINE-example,
list-del/partition/put-zero is used by REFINE-example,

Used from specification nat-basic1

nat-basic1/f is used by REFINE-example,
nat-basic1/one is used by NEWPARTS-example,

Used from specification partelem

partelem/sel-03 is used by REFINE-example, NEWPARTS-example,
partelem/sel-04 is used by NEWPARTS-example,
partelem/sel-05 is used by REFINE-example, NEWPARTS-example,
partelem/upd-03 is used by REFINE-example,

Used from specification nat-basic2

nat-basic2/a is used by REFINE-example, NEWPARTS-example,
nat-basic2/c is used by REFINE-example, NEWPARTS-example,

Used from specification list

list/partition/Last is used by NEWPARTS-example,
list/partition/Nil is used by NEWPARTS-example,
list/list_of_nat/a is used by REFINE-example, MAIN-example,
list/partition/a is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/list_of_nat/app is used by REFINE-example, MAIN-example,
list/partition/app is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/partition/app-01 is used by MAIN-example,
list/list_of_nat/app-01 is used by MAIN-example,
list/list_of_nat/app-02-ant is used by REFINE-example,
list/list_of_nat/c is used by REFINE-example, MAIN-example,
list/partition/c is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/list_of_nat/c-03 is used by REFINE-example,
list/list_of_nat/c-06 is used by REFINE-example,
list/partition/c-07 is used by NEWPARTS-example,
list/list_of_nat/c-07 is used by REFINE-example,
list/partition/c-08 is used by NEWPARTS-example,
list/list_of_nat/e is used by REFINE-example,
list/partition/e is used by NEWPARTS-example,
list/list_of_nat/e-01 is used by REFINE-example,
list/partition/e-01 is used by NEWPARTS-example,
list/partition/first is used by NEWPARTS-example,
list/partition/in-14 is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/list_of_nat/in-14 is used by REFINE-example,
list/list_of_nat/in-15 is used by REFINE-example,
list/partition/in-15 is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/partition/in-17 is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/list_of_nat/in-17 is used by REFINE-example,
list/partition/in-append is used by REFINE-example, NEWPARTS-example, MAIN-example,
list/list_of_nat/in-append is used by REFINE-example,
list/partition/len is used by NEWPARTS-example,
list/partition/len-02 is used by NEWPARTS-example,
list/list_of_nat/rest is used by REFINE-example,
list/partition/rest is used by NEWPARTS-example,

Used from specification partition-refinement

partition-refinement/updF-get is used by updF-get-strong,
partition-refinement/updF-member is used by NEWPARTS-example,

Used from specification list-data

list-data/list_of_nat/elim-list-c is used by REFINE-example,
list-data/partition/size-01 is used by NEWPARTS-example,

Used from specification store

store/map_nat_nat/k-Extension is used by REFINE-example, NEWPARTS-example,
store/map_nat_nat/At-other is used by At-other-strong,
store/map_nat_nat/At-other-num is used by REFINE-example, NEWPARTS-example,
store/map_nat_nat/At-same is used by At-other-strong,
store/map_nat_nat/In-empty is used by REFINE-example, NEWPARTS-example,
store/map_nat_nat/In-insert is used by in-insert-strong,
store/map_nat_nat/insins is used by REFINE-example,

Used from specification nat

nat/anti is used by NEWPARTS-example,
nat/lels-02 is used by NEWPARTS-example,
nat/pred-03 is used by NEWPARTS-example,