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

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

Used from specification list

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

Used from specification cell

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

Used from specification heap-sep

heap-sep/cell-heap-aux/precise is used by precise-ls,
heap-sep/cell-heap-aux/sep is used by precise-ls, owner-lst1, owner-ls1, lst-in-hp,
heap-sep/cell-heap-aux-heap-aux/and is used by ls-unique,
heap-sep/cell-heap-aux/and is used by precise-ls, ls-one,
heap-sep/cell-heap-aux/and-ass is used by precise-ls, owner-lst1, owner-ls1, lst-null, lst-in-hp, ls-unique-strng, ls-unique, ls-unfold1, ls-push, ls-one, ls-null,
heap-sep/cell-heap-aux-heap-aux/and-ass is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux-heap-aux/and-com is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux/and-com is used by precise-ls, owner-lst1, owner-ls1, lst-null, lst-in-hp, ls-unique-strng, ls-unique, ls-unfold1, ls-push, ls-one, ls-null,
heap-sep/cell-heap-aux/emp is used by precise-ls,
heap-sep/cell-heap-aux-heap-aux/emp is used by lst-null,
heap-sep/cell-heap-aux/emp-sep is used by ls-one,
heap-sep/cell-heap-aux-heap-aux/emp-sep is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux/false-and is used by owner-lst1, owner-ls1, lst-in-hp, ls-unique-strng, ls-unique, ls-unfold1, ls-null,
heap-sep/cell-heap-aux/false-rev is used by owner-lst1, owner-ls1, lst-in-hp, ls-unique-strng, ls-unique, ls-unfold1, ls-push, ls-one, ls-null,
heap-sep/cell-heap-aux-heap-aux/false-sep is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux/false-sep is used by ls-unfold1, ls-null,
heap-sep/cell-heap-aux/falseH is used by owner-lst1, owner-ls1, lst-in-hp, ls-unfold1, ls-one, ls-null,
heap-sep/cell-heap-aux/precise-emp is used by precise-ls,
heap-sep/cell-heap-aux/precise-same is used by precise-ls,
heap-sep/cell-heap-aux-heap-aux/prop is used by ls-unique,
heap-sep/cell-heap-aux/prop is used by precise-ls, ls-one,
heap-sep/cell-heap-aux-heap-aux/prop-shift is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux/prop-shift is used by ls-one,
heap-sep/cell-heap-aux/sep-ass is used by ls-unique-strng, ls-unique, ls-unfold2, ls-unfold1, ls-push, ls-one, ls-null, ls-fold1,
heap-sep/cell-heap-aux-heap-aux/sep-ass is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux/sep-com is used by ls-unique-strng, ls-unique, ls-unfold2, ls-unfold1, ls-push, ls-one, ls-null, ls-fold1,
heap-sep/cell-heap-aux-heap-aux/sep-com is used by ls-unique-strng, ls-unique, ls-push,
heap-sep/cell-heap-aux-heap-aux/true-and is used by ls-push,
heap-sep/cell-heap-aux/true-and is used by precise-ls, lst-null, ls-null,
heap-sep/cell-heap-aux/true-rev is used by precise-ls, lst-null, ls-null,

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-unique-strng, ls-unique, ls-push,
embed-aux/cell-heap-aux/embed-split is used by ls-unique-strng, ls-unique, ls-push,
embed-aux/cell-heap-aux/lift-emp is used by lst-null, ls-unique-strng, ls-unique, ls-push,
embed-aux/cell-heap-aux/lift-ex-r is used by ls-unique-strng, ls-unique, ls-push,
embed-aux/cell-heap-aux/lift-false is used by ls-unique-strng, ls-unique, ls-push,
embed-aux/cell-heap-aux/lift-prop is used by ls-unique-strng, ls-unique, ls-push,
embed-aux/cell-heap-aux/map2 is used by ls-unique-strng, ls-unique, ls-push,
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 precise-ls, owner-lst1, owner-ls1, 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-uni is used by precise-ls, lst-in-hp,
heap/cell-heap-aux/at-write 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-swap is used by precise-ls,
heap/cell-heap-aux/disj-write is used by precise-ls,
heap/cell-heap-aux/in-alloc is used by precise-ls, lst-in-hp,
heap/cell-heap-aux/in-emp is used by precise-ls, lst-in-hp,
heap/cell-heap-aux/in-uni is used by precise-ls, owner-lst1, owner-ls1, lst-in-hp,
heap/cell-heap-aux/in-write-strong is used by lst-in-hp,
heap/cell-heap-aux/nonnull is used by precise-ls,

Used from specification heap-fun

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

Used from specification set-union

set-union/refset/Union is used by lst-in-hp,
set-union/refset/int-a is used by owner-lst1, owner-ls1, lst-in-hp, ex-lst-shift,
set-union/refset/int-c is used by owner-lst1, owner-ls1, lst-in-hp, ex-lst-shift,
set-union/refset/una is used by lst-in-hp,
set-union/refset/unc is used by lst-in-hp,