[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/cell-heap/Eq-P is used by dls-split, dls-last,
heap-sep/cell-heap/and is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/and-ass is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/and-com is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/emp-sep is used by dls-split, dls-one, dls-last,
heap-sep/cell-heap/false-and is used by dls-length,
heap-sep/cell-heap/false-rev is used by dls-length,
heap-sep/cell-heap/false-sep is used by dls-length,
heap-sep/cell-heap/falseH is used by dls-length,
heap-sep/cell-heap/prop is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/prop-shift is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/sep-ass is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/sep-com is used by dls-split, dls-one, dls-length, dls-last,
heap-sep/cell-heap/true-and is used by dls-split, dls-one, dls-last,
heap-sep/cell-heap/true-rev is used by dls-split, dls-one, dls-last,

Used from specification maplet

maplet/cell-heap/eq-objs is used by dls-split, dls-last,
maplet/cell-heap/ex1 is used by dls-one,
maplet/cell-heap/ex1-shift is used by dls-split, dls-length, dls-last,
maplet/cell-heap/ex2-shift is used by dls-split,

Used from specification list-data

list-data/reflist/elim-list-c is used by dls-split, dls-length,
list-data/reflist/l is used by dls-split, dls-length, dls-last,
list-data/reflist/size-01 is used by dls-split, dls-last,
list-data/size-01 is used by dls-split, dls-length, dls-last,

Used from specification list

list/reflist/Nil is used by dls-split, dls-last,
list/Nil is used by dls-split, dls-last,
list/reflist/a is used by dls-split, dls-length, dls-last,
list/a is used by dls-split, dls-one, dls-length, dls-last,
list/reflist/app is used by dls-split,
list/app is used by dls-split, dls-one,
list/c is used by dls-split, dls-length, dls-last,
list/reflist/c is used by dls-split, dls-length, dls-last,
list/reflist/c-07 is used by dls-split, dls-last,
list/reflist/c-08 is used by dls-split, dls-last,
list/reflist/e is used by dls-one,
list/e-01 is used by dls-split,
list/reflist/e-01 is used by dls-split, dls-length, dls-last,
list/reflist/first is used by dls-one,
list/len is used by dls-split, dls-length, dls-last,
list/reflist/len is used by dls-split, dls-length, dls-last,
list/len-02 is used by dls-split, dls-length, dls-last,
list/reflist/len-02 is used by dls-split, dls-length, dls-last,
list/reflist/rest is used by dls-one,

Used from specification nat-basic2

nat-basic2/a is used by dls-split, dls-length, dls-last,
nat-basic2/c is used by dls-split, dls-length, dls-last,
nat-basic2/eq-01 is used by dls-split, dls-length, dls-last,
nat-basic2/oz is used by dls-split, dls-last,