[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/a is used by Uniform-heap, size-alloc,
nat-basic/c is used by Uniform-heap, size-alloc,
nat-basic/eq-01 is used by size-alloc,
nat-basic/refl-Nat is used by Uniform-heap,
nat-basic/s-04 is used by Uniform-heap,

Used from specification heapmap

heapmap/add-get is used by at-alloc,
heapmap/put-def is used by Uniform-heap, in-write,
heapmap/add-in is used by Uniform-heap, in-alloc, Decl-allocjsiz,
heapmap/add-size is used by size-alloc,
heapmap/add-update-is-alloc is used by Uniform-heap,
heapmap/del-def is used by in-del, at-del,
heapmap/get-def is used by at-write, at-del, at-alloc, ext,
heapmap/put-def is used by at-write, size-write,
heapmap/put-undef is used by Uniform-heap, at-write, in-write,

Used from specification map

map/Extension is used by Uniform-heap, ext,
map/exin is used by Uniform-heap,
map/notmemlookup is used by Uniform-heap, ext,
map/At-other is used by at-write,
map/Del-at is used by at-del,
map/Del-in is used by in-del,
map/In-empty is used by Uniform-heap, in-emp, Term-jemp,
map/In-insert is used by Uniform-heap, in-write,
map/Size-empty is used by size-emp,
map/Size-insert is used by Uniform-heap,
map/k-At-same is used by at-write,
map/size-in is used by size-write,