[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 owner-lst1, owner-ls1, lst-in-hp, precise-ls,
heap-sep/and is used by ls-one, precise-ls,
heap-sep/and-ass is used by owner-lst1, ls-null, ls-one, owner-ls1, lst-in-hp, ls-push, ls-unfold1, precise-ls, lst-null, ls-unique-strng,
heap-sep/heap-aux-inst/and-ass is used by ls-push, ls-unique-strng,
heap-sep/and-com is used by owner-lst1, ls-null, ls-one, owner-ls1, lst-in-hp, ls-push, ls-unfold1, precise-ls, lst-null, ls-unique-strng,
heap-sep/heap-aux-inst/and-com is used by ls-push, ls-unique-strng,
heap-sep/emp is used by precise-ls,
heap-sep/heap-aux-inst/emp is used by lst-null,
heap-sep/emp-sep is used by ls-one,
heap-sep/heap-aux-inst/emp-sep is used by ls-push, ls-unique-strng,
heap-sep/false-and is used by owner-lst1, ls-null, owner-ls1, lst-in-hp, ls-unfold1, ls-unique-strng,
heap-sep/false-rev is used by owner-lst1, ls-null, ls-one, owner-ls1, lst-in-hp, ls-push, ls-unfold1, ls-unique-strng,
heap-sep/false-sep is used by ls-null, ls-unfold1,
heap-sep/heap-aux-inst/false-sep is used by ls-push, ls-unique-strng,
heap-sep/falseH is used by owner-lst1, ls-null, ls-one, owner-ls1, lst-in-hp, ls-unfold1,
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, precise-ls,
heap-sep/prop-shift is used by ls-one,
heap-sep/heap-aux-inst/prop-shift is used by ls-push, ls-unique-strng,
heap-sep/heap-aux-inst/sep-ass is used by ls-unique, ls-push, ls-unique-strng,
heap-sep/sep-ass is used by ls-null, ls-one, ls-push, ls-unfold1, ls-fold1, ls-unique-strng, ls-unfold2,
heap-sep/heap-aux-inst/sep-com is used by ls-unique, ls-push, ls-unique-strng,
heap-sep/sep-com is used by ls-null, ls-one, ls-push, ls-unfold1, ls-fold1, ls-unique-strng, ls-unfold2,
heap-sep/heap-aux-inst/true-and is used by ls-push,
heap-sep/true-and is used by ls-null, precise-ls, lst-null,
heap-sep/true-rev is used by ls-null, precise-ls, lst-null,

Used from specification set-union

set-union/refset/una is used by lst-in-hp,
set-union/refset/unc is used by lst-in-hp,
set-union/refset/unin-01 is used by lst-in-hp,

Used from specification maplet

maplet/cell-heap-aux/maplet is used by lst-in-hp, precise-ls,
maplet/cell-heap-aux/ex1 is used by owner-lst1, ls-null, ls-one, owner-ls1, lst-in-hp, precise-ls,
maplet/cell-heap-aux/ex1-shift is used by ls-unfold1, ls-fold1, ls-unfold2,
maplet/cell-heap-aux/map-in0 is used by owner-lst1, owner-ls1, precise-ls,
maplet/cell-heap-aux/map-null is used by ls-null, ls-push, ls-unique-strng,
maplet/cell-heap-aux/precise-map is used by precise-ls,

Used from specification set-basic

set-basic/refset/ne-01 is used by ex-lst-shift,
set-basic/refset/size-zero-01 is used by ex-lst-shift,

Used from specification heap-fun

heap-fun/cell-heap-aux/at-mk is used by owner-lst1, owner-ls1, lst-in-hp,
heap-fun/cell-heap-aux/in-mk is used by owner-lst1, owner-ls1, lst-in-hp,

Used from specification list

list/firsteq-01 is used by ls-push,
list/Nil is used by ls-push,
list/a is used by owner-lst1, ls-null, ls-one, owner-ls1, lst-in-hp, ls-push, ls-unfold1, ls-fold1, precise-ls, ls-unique-strng, ls-unfold2,
list/app is used by ls-one,
list/c is used by owner-lst1, ls-null, owner-ls1, lst-in-hp, ls-push, ls-unfold1, precise-ls, ls-unique-strng,
list/c-06 is used by ls-unfold1, ls-unique-strng,
list/e is used by ls-push,
list/e-01 is used by ls-null, ls-push, ls-unfold1, ls-unique-strng,
list/first is used by ls-push,
list/rest is used by ls-push,

Used from specification embed-aux

embed-aux/cell-heap-aux/aux-known is used by ls-push,
embed-aux/cell-heap-aux/lift-aux is used by owner-lst1, owner-ls1, lst-in-hp, ex-lst-shift,
embed-aux/cell-heap-aux/and-split is used by ls-unique-strng,
embed-aux/cell-heap-aux/embed-and is used by ls-push, ls-unique-strng,
embed-aux/cell-heap-aux/embed-split is used by ls-push, ls-unique-strng,
embed-aux/cell-heap-aux/lift-emp is used by ls-push, lst-null, ls-unique-strng,
embed-aux/cell-heap-aux/lift-ex-r is used by ls-push, ls-unique-strng,
embed-aux/cell-heap-aux/lift-false is used by ls-push, ls-unique-strng,
embed-aux/cell-heap-aux/lift-prop is used by ls-push, ls-unique-strng,
embed-aux/cell-heap-aux/map2 is used by ls-push, ls-unique-strng,
embed-aux/cell-heap-aux/merge-owned-rewrite is used by ls-push,

Used from specification heap

heap/cell-heap-aux/at-uni is used by precise-ls,
heap/cell-heap-aux/disj-distr-uni is used by precise-ls,
heap/cell-heap-aux/ext is used by owner-lst1, owner-ls1, lst-in-hp, precise-ls,
heap/cell-heap-aux/in-uni is used by lst-in-hp,
heap/cell-heap-aux/uni-ass is used by precise-ls,
heap/cell-heap-aux/uni-inj is used by precise-ls,
heap/cell-heap-aux/at-write is used by precise-ls,
heap/cell-heap-aux/disj-com-rw is used by precise-ls,
heap/cell-heap-aux/disj-distr-uni-com is used by precise-ls,
heap/cell-heap-aux/disj-emp-r is used by precise-ls,
heap/cell-heap-aux/disj-singleton-write is used by lst-in-hp, precise-ls,
heap/cell-heap-aux/disj-write is used by precise-ls,
heap/cell-heap-aux/in-alloc is used by lst-in-hp, precise-ls,
heap/cell-heap-aux/in-emp is used by lst-in-hp, precise-ls,
heap/cell-heap-aux/in-uni is used by owner-lst1, owner-ls1, precise-ls,
heap/cell-heap-aux/in-write is used by lst-in-hp,
heap/cell-heap-aux/nonnull is used by precise-ls,

Used from specification cell

cell/inj-tim is used by ls-push, precise-ls, ls-unique-strng,

Used from specification heap-aux

heap-aux/cell-heap-aux/apply is used by owner-lst1, owner-ls1, lst-in-hp, ex-lst-shift, lst-null,
heap-aux/cell-heap-aux/ex1-shift is used by ls-unique-strng,
heap-aux/cell-heap-aux/sep is used by owner-lst1, owner-ls1, lst-in-hp, ex-lst-shift,
heap-aux/cell-heap-aux/split-uni is used by ex-lst-shift,
heap-aux/cell-heap-aux/emp is used by lst-null,
heap-aux/cell-heap-aux/ex1-shift is used by ls-push, ls-unique-strng,
heap-aux/cell-heap-aux/prop is used by ls-push, ls-unique-strng,
heap-aux/cell-heap-aux/prop-false is used by ls-push, ls-unique-strng,
heap-aux/cell-heap-aux/true-elim is used by ls-push,