[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-dll-prev,
heapfuns/disj is used by dll-union,
heapfuns/in-uni is used by precise-dll-prev,
heapfuns/subset is used by inj-dll-gen,
heapfuns/uni-ass is used by precise-dll-prev,
heapfuns/at-uni is used by precise-dll-prev, dll-union,
heapfuns/del-uni is used by dll-union,
heapfuns/disj-com-rw is used by precise-dll-prev,
heapfuns/disj-distr-uni is used by precise-dll-prev,
heapfuns/disj-distr-uni-com is used by precise-dll-prev,
heapfuns/disj-emp-l is used by dll-union,
heapfuns/disj-emp-r is used by precise-dll-prev,
heapfuns/disj-rem is used by dll-union,
heapfuns/disj-singleton-write is used by inj-dll-gen, precise-dll-prev,
heapfuns/disj-write is used by precise-dll-prev,
heapfuns/emp-subset is used by inj-dll-gen,
heapfuns/in-uni is used by precise-dll-prev, dll-union,
heapfuns/subset-refl is used by inj-dll,
heapfuns/uni-emp-l is used by dll-union,
heapfuns/uni-inj is used by precise-dll-prev,
heapfuns/union-subset is used by inj-dll-gen,

Used from specification node

node/inj-mknode is used by inj-dll-gen, precise-dll-prev, dll-union,

Used from specification maplet

maplet/map-del is used by dll-union,
maplet/maplet is used by inj-dll-gen, precise-dll-prev,
maplet/at-rw is used by dll-union,
maplet/at-rw-singleton is used by precise-dll-prev,
maplet/ex is used by inj-dll-gen, precise-dll-prev, dll-union, dll-prev-one, dll-prev-null,
maplet/ex1-shift is used by ls-unfold1, ls-unfold2, dll-union, dll-fold,
maplet/map-in is used by dll-union,
maplet/map-in0 is used by precise-dll-prev,
maplet/map-null is used by inj-dll-gen, dll-union, dll-prev-null,
maplet/precise-map is used by precise-dll-prev,

Used from specification heap-sep

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

Used from specification heap

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

Used from specification list

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