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

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

Used from specification heapfuns-map

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

Used from specification refmap-maplet

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

Used from specification cell

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

Used from specification list

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

Used from specification map

map/Extension is used by precise-ls,
map/In-empty is used by precise-ls,
map/notin-del-notin is used by ls-union,