[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/at-uni is used by at-unil, at-unir,
heapfuns/disj is used by disj,
heapfuns/in-uni is used by in-uni,
heapfuns/at-uni is used by at-rw,
heapfuns/in-uni is used by map-in, mapex-in, at-rw,
heapfuns/size-alloc is used by mk-exists,
heapfuns/size-write is used by mk-exists,

Used from specification set-union

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

Used from specification maplet

maplet/map-del is used by mapex-put, mapex-new, map-del,
maplet/maplet is used by map-in0, at-rw,
maplet/ex is used by mapex-in,
maplet/ex1-shift is used by ex1-shift, ex3-shift, mapex-put,
maplet/ex2-shift is used by ex2-shift,
maplet/map-in0 is used by map-in, mapex-in, at-rw,
maplet/map-null is used by map-in0,
maplet/map-write is used by mapex-put,
maplet/maplet is used by map-in0,

Used from specification set-basic

set-basic/Extension is used by sep,
set-basic/In-empty is used by emp,
set-basic/In-insert is used by mk-exists,
set-basic/add is used by mk-exists,
set-basic/eq is used by mapex-new,
set-basic/in is used by mapex-new,
set-basic/in-02 is used by mk-exists, mapex-new,
set-basic/in-03 is used by mapex-new,
set-basic/ne-01 is used by mk-exists, disj, map-putrev, mapex-put, sep, write, mapex-new, at-rw, del, at-unil, at-unir,
set-basic/size-zero-01 is used by disj, map-putrev, mapex-put, sep, write, mapex-new, at-rw, del, at-unil, at-unir,

Used from specification ex-maplet

ex-maplet/map-put is used by mapex-new, map-put,
ex-maplet/map-putex is used by map-putrev,
ex-maplet/mapex is used by mapex-put, mapex-in,
ex-maplet/mapex-del is used by mapex-del,
ex-maplet/mapex-new is used by mapex-new,
ex-maplet/map-putex is used by mapex-put,
ex-maplet/mapex-elim is used by mapex-elim, mapex-put,

Used from specification heap-sep

heap-sep/sep is used by map-in, mapex-in, sep, at-rw,
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 map-in0, prop-emp, mapex-in0, at-rw0,
heap-sep/false-rev is used by map-in0, prop,
heap-sep/falseH is used by map-in0, prop-false, prop,
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 ex1-shift, map-in0, mapex-elim, ex3-shift, true-elim, prop-emp, mapex-put, mapex-in, mapex-in0, true-emp, at-rw0, ex2-shift, prop-sep,
heap-sep/sep-com is used by ex1-shift, map-in0, mapex-elim, ex3-shift, true-elim, prop-emp, mapex-put, mapex-in, mapex-in0, true-emp, at-rw0, ex2-shift, 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 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

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