[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 heap-sep

heap-sep/false-rev is used by cf-map-unknown,
heap-sep/falseH is used by cf-map-unknown,
heap-sep/heap-aux-inst/sep-ass is used by cf-map-unknown,
heap-sep/heap-aux-inst/sep-com is used by cf-map-unknown,

Used from specification maplet

maplet/cell-heap-aux/mapex is used by cf-map-unknown,
maplet/cell-heap-aux/maplet is used by cf-map-unknown,
maplet/cell-heap-aux/map-null is used by cf-map-unknown,

Used from specification heap-fun

heap-fun/cell-heap-aux/at-mk is used by cf-map-unknown,
heap-fun/cell-heap-aux/in-mk is used by cf-map-unknown,

Used from specification embed-aux

embed-aux/cell-heap-aux/lift-aux is used by cf-map-unknown,
embed-aux/cell-heap-aux/lift-ex-o is used by cf-map-unknown,

Used from specification heap

heap/cell-heap-aux/ext is used by cf-map-unknown,
heap/cell-heap-aux/at-write is used by cf-map-unknown,
heap/cell-heap-aux/in-alloc is used by cf-map-unknown,
heap/cell-heap-aux/in-emp is used by cf-map-unknown,
heap/cell-heap-aux/in-write is used by cf-map-unknown,

Used from specification heap-aux

heap-aux/cell-heap-aux/apply is used by cf-map-unknown,
heap-aux/cell-heap-aux/sep is used by cf-map-unknown,
heap-aux/cell-heap-aux/split-uni is used by cf-map-unknown,
heap-aux/cell-heap-aux/ex3-shift-01 is used by cf-map-unknown,

Used from specification cell

cell/elim-tim is used by cf-write-val, cf-write-nxt,
cell/upd-tim-dotnxt is used by cf-write-nxt,
cell/upd-tim-dotval is used by cf-write-val,