[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/add-subset is used by precise-tr,
heapfuns/subset is used by precise-tr, inj-tr-gen,
heapfuns/disj-distr-uni is used by inj-tr-gen,
heapfuns/disj-emp-r is used by inj-tr-gen,
heapfuns/disj-singleton-write is used by precise-tr,
heapfuns/disj-write is used by inj-tr-gen,
heapfuns/emp-subset is used by inj-tr-gen,
heapfuns/in-uni is used by precise-tr,
heapfuns/subset-refl is used by inj-tr,
heapfuns/union-add-singleton-left is used by precise-tr,
heapfuns/union-subset is used by precise-tr, inj-tr-gen,

Used from specification node

node/inj-mknode is used by precise-tr, inj-tr-gen,

Used from specification maplet

maplet/maplet is used by precise-tr, inj-tr-gen,
maplet/ex2 is used by tr-null, precise-tr, tr-fold-singleton, inj-tr-gen,
maplet/ex2-shift is used by tr-fold, tr-unfold, tr-fold-t,
maplet/map-null is used by tr-null,

Used from specification tree

tree/inj-branch is used by inj-tr-gen,
tree/disj-leaf-branch is used by tr-null, inj-tr-gen,

Used from specification heap-sep

heap-sep/precise-alt-def is used by precise-tr,
heap-sep/sep is used by precise-tr, inj-tr-gen,
heap-sep/and is used by precise-tr, tr-fold-singleton, inj-tr-gen,
heap-sep/and-ass is used by tr-null, tr-branch, precise-tr, tr-unfold, tr-fold-singleton, inj-tr-gen,
heap-sep/and-com is used by tr-null, tr-branch, precise-tr, tr-unfold, tr-fold-singleton, inj-tr-gen,
heap-sep/emp is used by precise-tr, inj-tr-gen,
heap-sep/emp-sep is used by tr-fold-singleton,
heap-sep/false-and is used by tr-null, tr-branch, tr-unfold, inj-tr-gen,
heap-sep/false-rev is used by tr-null, tr-branch, tr-unfold, tr-fold-singleton, inj-tr-gen,
heap-sep/false-sep is used by tr-null, tr-branch, tr-unfold,
heap-sep/falseH is used by tr-null, tr-branch, tr-unfold, tr-fold-singleton, inj-tr-gen,
heap-sep/prop is used by precise-tr, tr-fold-singleton, inj-tr-gen,
heap-sep/prop-shift is used by tr-fold-singleton,
heap-sep/sep-ass is used by tr-null, tr-branch, precise-tr, tr-fold, tr-unfold, tr-fold-t, tr-fold-singleton, inj-tr-gen,
heap-sep/sep-com is used by tr-null, tr-branch, precise-tr, tr-fold, tr-unfold, tr-fold-t, tr-fold-singleton, inj-tr-gen,
heap-sep/true-and is used by tr-null, precise-tr,
heap-sep/true-elim is used by tr-fold-t,
heap-sep/true-rev is used by tr-null, precise-tr,

Used from specification heap

heap/at-write is used by precise-tr, inj-tr-gen,
heap/in-alloc is used by precise-tr, inj-tr-gen,
heap/in-emp is used by inj-tr-gen,
heap/in-write is used by precise-tr, inj-tr-gen,
heap/nonnull is used by precise-tr, inj-tr-gen,