[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 linked-list

linked-list/ls-rec is used by refine-add,
linked-list/ls-base is used by refine-add,
linked-list/ls-null is used by process-one, refine-get, refine-add, initialization,
linked-list/ls-unfold1 is used by process-one, refine-get,

Used from specification nat-basic

nat-basic/a is used by size-del-0, size-del, process-queue, process-one, refine-get, refine-add, initialization,
nat-basic/add-base is used by size-del, process-queue, refine-get, refine-add,
nat-basic/c is used by size-del-0, size-del, process-queue, process-one, refine-get, refine-add, initialization,
nat-basic/eq-01 is used by refine-get, refine-add,
nat-basic/f is used by process-one, refine-get, refine-add,
nat-basic/l is used by refine-get, refine-add,
nat-basic/l-01 is used by refine-get, refine-add,
nat-basic/lf-01 is used by refine-get,
nat-basic/lf-02 is used by refine-get, refine-add,
nat-basic/nls-fst is used by refine-get,
nat-basic/one is used by process-one, refine-add,
nat-basic/one-01 is used by process-queue,
nat-basic/one-06 is used by process-queue,
nat-basic/oz is used by process-queue, process-one,
nat-basic/ref is used by refine-get, refine-add,
nat-basic/s-04 is used by process-one, refine-get, refine-add,
nat-basic/succ is used by process-one, refine-get, refine-add,
nat-basic/succ-03 is used by refine-add,
nat-basic/twols-02 is used by process-queue,
nat-basic/z-01 is used by size-del-0,
nat-basic/zero is used by process-one, initialization,

Used from specification heap-sep

heap-sep/and is used by process-one, refine-get, refine-add, initialization,
heap-sep/and-ass is used by process-queue, process-one, refine-get, refine-add, initialization,
heap-sep/and-com is used by process-queue, process-one, refine-get, refine-add, initialization,
heap-sep/emp is used by initialization,
heap-sep/emp-sep is used by process-queue, process-one, refine-get, refine-add, initialization,
heap-sep/false-and is used by refine-get, refine-add,
heap-sep/false-rev is used by refine-get, refine-add,
heap-sep/false-sep is used by refine-get, refine-add,
heap-sep/falseH is used by refine-get, refine-add,
heap-sep/prop is used by process-one, refine-get, refine-add, initialization,
heap-sep/prop-shift is used by process-one, refine-get, refine-add, initialization,
heap-sep/sep-ass is used by process-queue, process-one, refine-get, refine-add, initialization,
heap-sep/sep-com is used by process-queue, process-one, refine-get, refine-add, initialization,
heap-sep/true-and is used by process-queue, process-one, refine-get, refine-add,
heap-sep/true-rev is used by process-queue, process-one, refine-get, refine-add,

Used from specification nat

nat/add-01 is used by size-del, process-queue,
nat/add-num-03 is used by refine-add,
nat/anti is used by refine-get,
nat/cancel-01 is used by process-one,
nat/elim-pred-c is used by process-queue, process-one,
nat/elim-sub is used by process-one, refine-get, refine-add,
nat/eq-01 is used by process-one,
nat/fle is used by refine-add,
nat/ge is used by process-queue, process-one, refine-add,
nat/gr-def is used by initialization,
nat/le-add is used by refine-add,
nat/le-def is used by process-queue, refine-get, refine-add,
nat/le-ls-simp is used by refine-get, refine-add,
nat/le-num-04 is used by process-queue,
nat/lels is used by process-one, refine-get, refine-add,
nat/lels-02 is used by process-one, refine-get,
nat/lels-03 is used by refine-get,
nat/lels-04 is used by refine-add,
nat/lep is used by process-queue, process-one, refine-add,
nat/lep-02 is used by refine-get, refine-add,
nat/ler is used by refine-add,
nat/let is used by refine-add,
nat/lez is used by refine-add, initialization,
nat/ls-01 is used by refine-get,
nat/ls-02 is used by refine-get,
nat/ls-03 is used by refine-get,
nat/ls-le-simp is used by refine-get, refine-add,
nat/not-zero is used by process-queue, process-one, refine-add,
nat/prop-07 is used by refine-get,
nat/succ-01 is used by process-one, refine-get, refine-add,
nat/zero-02 is used by process-one, refine-get,

Used from specification maplet

maplet/cell-heap/map-del is used by process-one,
maplet/cell-heap/at-eq is used by process-one, refine-get,
maplet/cell-heap/ex1 is used by refine-add,
maplet/cell-heap/ex1-shift is used by refine-get, refine-add,
maplet/cell-heap/map-putex is used by refine-add,
maplet/cell-heap/mapex-new-rw is used by refine-add,

Used from specification del-lists

del-lists/del-list-rec is used by process-one,
del-lists/del-list-base is used by process-queue, process-one, refine-add, initialization,
del-lists/del-lists-1 is used by refine-add,
del-lists/ex-p is used by process-one, refine-add,

Used from specification list-prefixn

list-prefixn/prefixn-shift-right is used by refine-get,
list-prefixn/prefixn-append-left is used by refine-get,
list-prefixn/prefixn-eq-empty is used by refine-get,
list-prefixn/prefixn-fulln is used by refine-get,

Used from specification list-data

list-data/reflist/elim-list-c is used by process-one,
list-data/l is used by refine-get, refine-add,
list-data/size-01 is used by process-one, refine-get, refine-add, initialization,

Used from specification list

list/Last is used by refine-get,
list/Nil is used by refine-get,
list/reflist/a is used by process-one, refine-add,
list/a is used by process-one, refine-get, refine-add,
list/reflist/app is used by refine-add,
list/app is used by refine-get,
list/app-01 is used by refine-get,
list/app-04 is used by refine-get,
list/app-08 is used by refine-get,
list/reflist/c is used by process-one, refine-add,
list/c is used by refine-add,
list/reflist/e-01 is used by process-one,
list/e-03 is used by refine-get,
list/in-14 is used by process-one, refine-get,
list/in-rec is used by process-one, refine-get,
list/len is used by refine-get,
list/len-02 is used by refine-get,
list/len-05 is used by process-one, refine-get, refine-add,

Used from specification cell

cell/elim is used by process-one, refine-get,
cell/inj is used by process-one, refine-get,
cell/set-val-nxt is used by refine-add,

Used from specification heap

heap/cell-heap/exin is used by size-del-0, size-del,
heap/cell-heap/at-write is used by refine-add,
heap/cell-heap/del-new is used by size-del,
heap/cell-heap/in-alloc is used by size-del-0, size-del, refine-add,
heap/cell-heap/nonnull is used by size-del-0, size-del,
heap/cell-heap/overwrite is used by refine-add,
heap/cell-heap/sanity is used by size-del-0, size-del,
heap/cell-heap/size-alloc is used by size-del-0, size-del,
heap/cell-heap/size-write is used by size-del-0, size-del,
heap/cell-heap/write-del is used by size-del,

Used from specification linked-list-seg

linked-list-seg/lls-base is used by refine-get,
linked-list-seg/lls-unfold-tail is used by refine-get,

Used from specification implementation-asm

implementation-asm/infinite-memory is used by refine-add,