[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 nat-basic

nat-basic/a is used by mk-exists,
nat-basic/c is used by mk-exists,
nat-basic/refl-nat is used by mk-exists,
nat-basic/s-04 is used by mk-exists,

Used from specification heap-sep

heap-sep/sep is used by at-rw, sep, map-in, mapex-in,
heap-sep/split-union is used by split-uni, sep,
heap-sep/and is used by prop-emp, prop-sep,
heap-sep/and-ass is used by prop-emp, prop-sep,
heap-sep/and-com is used by prop-emp, prop-sep,
heap-sep/emp-sep is used by mapex-in0, prop-emp, at-rw0, map-in0,
heap-sep/false-rev is used by prop, map-in0,
heap-sep/falseH is used by prop, prop-false, map-in0,
heap-sep/prop is used by prop-emp, prop-sep,
heap-sep/prop-shift is used by prop-emp, prop-sep,
heap-sep/sep-ass is used by true-elim, mapex-in0, prop-emp, ex1-shift, mapex-elim, ex2-shift, at-rw0, true-emp, mapex-put, ex3-shift, map-in0, prop-sep,
heap-sep/sep-com is used by true-elim, mapex-in0, prop-emp, ex1-shift, mapex-elim, ex2-shift, at-rw0, true-emp, mapex-put, ex3-shift, map-in0, prop-sep,
heap-sep/true-and is used by prop-emp, prop-sep,
heap-sep/true-elim is used by true-elim,
heap-sep/true-emp is used by true-emp,
heap-sep/true-rev is used by prop-emp, prop, prop-sep,
heap-sep/trueH is used by prop-true, prop,

Used from specification set-union

set-union/refset/Union is used by uni,
set-union/refset/Delete is used by del,
set-union/refset/Intersect is used by disj,
set-union/refset/del-in-01 is used by del,
set-union/refset/int-a is used by at-unil, split-uni, uni, sep, at-unir, disj,
set-union/refset/int-c is used by at-unil, split-uni, uni, sep, at-unir, disj,
set-union/refset/int-empty-02 is used by sep, at-unir, disj,
set-union/refset/una is used by split-uni, uni, sep,
set-union/refset/unc is used by split-uni, uni, sep,
set-union/refset/unin is used by uni, sep,
set-union/refset/unin-01 is used by sep,

Used from specification maplet

maplet/map-del is used by mapex-new, mapex-put, map-del,
maplet/map-put is used by mapex-new, map-put,
maplet/map-putex is used by map-putrev,
maplet/mapex is used by mapex-put, mapex-in,
maplet/mapex-del is used by mapex-del,
maplet/mapex-new is used by mapex-new,
maplet/maplet is used by at-rw, map-in0,
maplet/ex1-shift is used by ex1-shift,
maplet/ex2-shift is used by ex2-shift,
maplet/ex3 is used by mapex-in,
maplet/ex3-shift is used by mapex-put, ex3-shift,
maplet/map-in0 is used by at-rw, map-in, mapex-in,
maplet/map-null is used by map-in0,
maplet/map-putex is used by mapex-put,
maplet/mapex-elim is used by mapex-elim, mapex-put,
maplet/maplet-singleton-heap is used by map-in0,

Used from specification set-basic

set-basic/refset/Extension is used by sep, disj,
set-basic/refset/In-empty is used by emp, disj,
set-basic/refset/In-insert is used by mk-exists,
set-basic/refset/add is used by mk-exists,
set-basic/refset/in is used by mapex-new,
set-basic/refset/in-02 is used by mapex-new,
set-basic/refset/in-03 is used by mapex-new,

Used from specification heap

heap/at-del is used by mapex-new,
heap/at-uni is used by at-unil, at-unir,
heap/disj is used by disj,
heap/exin is used by mk-exists,
heap/ext is used by mk-exists, at-rw, del, uni, mapex-new, write, sep, emp, map-in, mapex-in,
heap/in-uni is used by in-uni,
heap/at-alloc is used by mk-exists,
heap/at-del is used by del,
heap/at-uni is used by at-rw,
heap/at-write is used by mk-exists, at-rw, mapex-new, write,
heap/del-new is used by mapex-new,
heap/in-alloc is used by mk-exists, at-rw, mapex-new,
heap/in-del is used by del, mapex-new,
heap/in-emp is used by mk-exists, at-rw, emp,
heap/in-uni is used by at-rw, map-in, mapex-in,
heap/in-write is used by mk-exists, mapex-new, write, mapex-put,
heap/sanity is used by mk-exists,
heap/size-alloc is used by mk-exists,
heap/size-write is used by mk-exists,
heap/write-del is used by mapex-new, mapex-put,