[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/and is used by tr-fold-singleton,
heap-sep/and-ass is used by tr-unfold, tr-branch, tr-fold-singleton, tr-null,
heap-sep/and-com is used by tr-unfold, tr-branch, tr-fold-singleton, tr-null,
heap-sep/emp-sep is used by tr-fold-singleton,
heap-sep/false-and is used by tr-unfold, tr-branch, tr-null,
heap-sep/false-rev is used by tr-unfold, tr-branch, tr-fold-singleton, tr-null,
heap-sep/false-sep is used by tr-unfold, tr-branch, tr-null,
heap-sep/falseH is used by tr-unfold, tr-branch, tr-fold-singleton, tr-null,
heap-sep/prop is used by tr-fold-singleton,
heap-sep/prop-shift is used by tr-fold-singleton,
heap-sep/sep-ass is used by tr-fold, tr-unfold, tr-fold-t, tr-branch, tr-fold-singleton, tr-null,
heap-sep/sep-com is used by tr-fold, tr-unfold, tr-fold-t, tr-branch, tr-fold-singleton, tr-null,
heap-sep/true-and is used by tr-null,
heap-sep/true-elim is used by tr-fold-t,
heap-sep/true-rev is used by tr-null,

Used from specification maplet

maplet/node-heap/ex2 is used by tr-fold-singleton, tr-null,
maplet/node-heap/ex2-shift is used by tr-fold, tr-unfold, tr-fold-t,
maplet/node-heap/map-null is used by tr-null,

Used from specification tree

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