[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/precise is used by precise-ls,
heap-sep/sep is used by precise-ls,
heap-sep/and is used by ls-one, ls-union, precise-ls,
heap-sep/and-ass is used by ls-null, ls-one, ls-unfold1, ls-union, precise-ls,
heap-sep/and-com is used by ls-null, ls-one, ls-unfold1, ls-union, precise-ls,
heap-sep/emp is used by ls-union, precise-ls,
heap-sep/emp-sep is used by ls-one, ls-union,
heap-sep/false-and is used by ls-null, ls-unfold1,
heap-sep/false-rev is used by ls-null, ls-one, ls-unfold1, ls-union,
heap-sep/false-sep is used by ls-null, ls-unfold1, ls-union,
heap-sep/falseH is used by ls-null, ls-one, ls-unfold1, ls-union,
heap-sep/precise-emp is used by precise-ls,
heap-sep/precise-same is used by precise-ls,
heap-sep/prop is used by ls-one, ls-union, precise-ls,
heap-sep/prop-shift is used by ls-one, ls-union,
heap-sep/sep-ass is used by ls-null, ls-one, ls-unfold1, ls-union, ls-fold1, ls-unfold2,
heap-sep/sep-com is used by ls-null, ls-one, ls-unfold1, ls-union, ls-fold1, ls-unfold2,
heap-sep/split-union is used by ls-union,
heap-sep/true-and is used by ls-null, precise-ls,
heap-sep/true-rev is used by ls-null, precise-ls,

Used from specification maplet

maplet/cell-heap/map-del is used by ls-union,
maplet/cell-heap/maplet is used by precise-ls,
maplet/cell-heap/at-eq is used by ls-union,
maplet/cell-heap/ex1 is used by ls-null, ls-one, ls-union, precise-ls,
maplet/cell-heap/ex1-shift is used by ls-unfold1, ls-union, ls-fold1, ls-unfold2,
maplet/cell-heap/map-in is used by ls-union,
maplet/cell-heap/map-in0 is used by precise-ls,
maplet/cell-heap/map-null is used by ls-null, ls-union,
maplet/cell-heap/precise-map is used by precise-ls,

Used from specification list

list/a is used by ls-null, ls-one, ls-unfold1, ls-union, ls-fold1, precise-ls, ls-unfold2,
list/app is used by ls-one,
list/c is used by ls-null, ls-unfold1, ls-union, precise-ls,
list/c-06 is used by ls-unfold1, ls-union,
list/e-01 is used by ls-null, ls-unfold1, ls-union,

Used from specification cell

cell/inj-tim is used by ls-union, precise-ls,

Used from specification heap

heap/cell-heap/at-uni is used by precise-ls,
heap/cell-heap/disj is used by ls-union,
heap/cell-heap/disj-distr-uni is used by precise-ls,
heap/cell-heap/ext is used by precise-ls,
heap/cell-heap/uni-ass is used by precise-ls,
heap/cell-heap/uni-inj is used by precise-ls,
heap/cell-heap/at-uni is used by ls-union, precise-ls,
heap/cell-heap/at-write is used by precise-ls,
heap/cell-heap/del-notin is used by ls-union,
heap/cell-heap/del-uni is used by ls-union,
heap/cell-heap/disj-com-rw is used by precise-ls,
heap/cell-heap/disj-distr-uni-com is used by precise-ls,
heap/cell-heap/disj-emp-l is used by ls-union,
heap/cell-heap/disj-emp-r is used by precise-ls,
heap/cell-heap/disj-l is used by ls-union,
heap/cell-heap/disj-singleton-write is used by precise-ls,
heap/cell-heap/disj-write is used by precise-ls,
heap/cell-heap/in-alloc is used by precise-ls,
heap/cell-heap/in-del is used by ls-union,
heap/cell-heap/in-emp is used by precise-ls,
heap/cell-heap/in-uni is used by ls-union, precise-ls,
heap/cell-heap/nonnull is used by precise-ls,
heap/cell-heap/uni-emp-l is used by ls-union,