[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 heapfuns

heapfuns/at-uni is used by precise-ls,
heapfuns/disj is used by ls-union,
heapfuns/subset is used by inj-ls-gen,
heapfuns/uni-ass is used by precise-ls,
heapfuns/at-uni is used by precise-ls, ls-union,
heapfuns/del-uni is used by ls-union,
heapfuns/disj-com-rw is used by precise-ls,
heapfuns/disj-distr-uni is used by precise-ls,
heapfuns/disj-distr-uni-com is used by precise-ls,
heapfuns/disj-emp-l is used by ls-union,
heapfuns/disj-emp-r is used by precise-ls,
heapfuns/disj-rem is used by ls-union,
heapfuns/disj-singleton-write is used by precise-ls, inj-ls-gen,
heapfuns/disj-write is used by precise-ls,
heapfuns/in-uni is used by precise-ls, ls-union,
heapfuns/subset-refl is used by inj-ls,
heapfuns/uni-emp-l is used by ls-union,
heapfuns/uni-inj is used by precise-ls,
heapfuns/union-subset is used by inj-ls-gen,

Used from specification maplet

maplet/map-del is used by ls-union,
maplet/maplet is used by precise-ls, inj-ls-gen,
maplet/at-rw is used by ls-union,
maplet/at-rw-singleton is used by precise-ls,
maplet/eq-objs is used by inj-ls-gen-sep,
maplet/ex is used by precise-ls, ls-union, ls-one, ls-null, inj-ls-gen,
maplet/ex1-shift is used by ls-union, ls-unfold2, ls-unfold1, ls-fold1, inj-ls-gen-sep,
maplet/map-in is used by ls-union,
maplet/map-in0 is used by precise-ls,
maplet/map-null is used by ls-union, ls-null, inj-ls-gen-sep, inj-ls-gen,
maplet/precise-map is used by precise-ls,

Used from specification heap-sep

heap-sep/precise is used by precise-ls,
heap-sep/sep is used by precise-ls, inj-ls-gen,
heap-sep/and is used by precise-ls, ls-union, ls-one, inj-ls-gen-sep, inj-ls-gen,
heap-sep/and-ass is used by precise-ls, ls-union, ls-unfold1, ls-one, ls-null, inj-ls-gen-sep, inj-ls-gen,
heap-sep/and-com is used by precise-ls, ls-union, ls-unfold1, ls-one, ls-null, inj-ls-gen-sep, inj-ls-gen,
heap-sep/emp is used by precise-ls, ls-union, inj-ls-gen,
heap-sep/emp-sep is used by ls-union, ls-one, inj-ls-gen-sep,
heap-sep/false-and is used by ls-unfold1, ls-null, inj-ls-gen-sep, inj-ls-gen,
heap-sep/false-rev is used by ls-union, ls-unfold1, ls-one, ls-null, inj-ls-gen-sep, inj-ls-gen,
heap-sep/false-sep is used by ls-union, ls-unfold1, ls-null, inj-ls-gen-sep, inj-ls-gen,
heap-sep/falseH is used by ls-union, ls-unfold1, ls-one, ls-null, inj-ls-gen-sep, inj-ls-gen,
heap-sep/precise-emp is used by precise-ls,
heap-sep/precise-same is used by precise-ls,
heap-sep/prop is used by precise-ls, ls-union, ls-one, inj-ls-gen-sep, inj-ls-gen,
heap-sep/prop-shift is used by ls-union, ls-one, inj-ls-gen-sep,
heap-sep/sep-ass is used by ls-union, ls-unfold2, ls-unfold1, ls-one, ls-null, ls-fold1, inj-ls-gen-sep, inj-ls-gen,
heap-sep/sep-com is used by ls-union, ls-unfold2, ls-unfold1, ls-one, ls-null, ls-fold1, inj-ls-gen-sep, inj-ls-gen,
heap-sep/split-union is used by ls-union,
heap-sep/true-and is used by precise-ls, ls-null,
heap-sep/true-rev is used by precise-ls, ls-null,

Used from specification cell

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

Used from specification heap

heap/ext is used by precise-ls,
heap/at-write is used by inj-ls-gen,
heap/del-notin is used by ls-union,
heap/in-alloc is used by inj-ls-gen,
heap/in-emp is used by precise-ls, inj-ls-gen,
heap/in-write is used by inj-ls-gen,
heap/nonnull is used by inj-ls-gen,

Used from specification list

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