[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/sep is used by embed-split,
heap-sep/heap-aux-inst/sep is used by embed-split,
heap-sep/heap-aux-inst/split-union is used by embed-split,
heap-sep/and is used by embed-and,
heap-sep/heap-aux-inst/and is used by lift-prop, embed-and, and-split,
heap-sep/and-ass is used by embed-and,
heap-sep/heap-aux-inst/and-ass is used by lift-prop, embed-and, and-split,
heap-sep/and-com is used by embed-and,
heap-sep/heap-aux-inst/and-com is used by lift-prop, embed-and, and-split,
heap-sep/emp is used by lift-emp,
heap-sep/heap-aux-inst/emp is used by lift-emp, lift-prop,
heap-sep/false-rev is used by write-known,
heap-sep/falseH is used by lift-false, write-known,
heap-sep/heap-aux-inst/prop is used by lift-prop,
heap-sep/prop is used by lift-prop,
heap-sep/heap-aux-inst/sep-ass is used by write-other-true, write-unknown, mod-other-hp, map-owner-unknown, map-owner-known, map-same, mod-other-aux1, mod-other-aux, merge-owned-rewrite, lift-unknown, aux-unknown, get-unknown, split-owned2, mod-f-known,
heap-sep/heap-aux-inst/sep-com is used by write-other-true, write-unknown, mod-other-hp, map-owner-unknown, map-owner-known, map-same, mod-other-aux1, mod-other-aux, merge-owned-rewrite, lift-unknown, aux-unknown, get-unknown, split-owned2, mod-f-known,
heap-sep/heap-aux-inst/true-and is used by lift-prop,
heap-sep/heap-aux-inst/true-rev is used by lift-prop,
heap-sep/trueH is used by lift-true,

Used from specification set-union

set-union/refset/subdef is used by merge-owned,
set-union/refset/subset-is-union is used by merge-owned,
set-union/refset/int-a is used by merge-owned, map-same, aux-known, embed-split, mod-other-hp2, write-known,
set-union/refset/int-c is used by merge-owned, map-same, aux-known, embed-split, mod-other-hp2, write-known,
set-union/refset/int-empty-02 is used by map-same, aux-known, write-known,
set-union/refset/intu-empty is used by merge-owned, mod-other-hp2,
set-union/refset/una is used by merge-owned, embed-split, map-in, mod-other-hp2,
set-union/refset/unc is used by merge-owned, embed-split, map-in, mod-other-hp2,
set-union/refset/unin is used by merge-owned,
set-union/refset/unin-01 is used by merge-owned, embed-split, map-in,

Used from specification maplet

maplet/mapex is used by write-unknown, lift-unknown, aux-unknown, get-unknown,
maplet/maplet is used by map-unique, aux-known, lift-unknown, get-known, map-in0, write-known,
maplet/ex1 is used by lift-ex-r,
maplet/ex3 is used by lift-ex-o, lift-unknown,
maplet/map-null is used by write-known,
maplet/maplet-singleton-heap is used by aux-known, write-known,

Used from specification set-basic

set-basic/refset/Extension is used by merge-owned,
set-basic/refset/ne-01 is used by lift-emp, lift-ex-o, lift-ex-r, lift-unknown, embed-split, write-known,
set-basic/refset/size-zero-01 is used by lift-emp, lift-ex-o, lift-ex-r, lift-unknown, embed-split, write-known,

Used from specification heap-fun

heap-fun/apply is used by embed-split,
heap-fun/sep is used by embed-split,
heap-fun/at-mk is used by map-unique, aux-known, lift-unknown, embed-split, get-known, map-in0, mod-other-hp2, write-known, mod-other-both,
heap-fun/at-unil is used by embed-split,
heap-fun/at-unir is used by embed-split,
heap-fun/disj is used by embed-split,
heap-fun/in-mk is used by lift-emp, map-unique, aux-known, lift-unknown, embed-split, get-known, map-in0, mod-other-hp2, write-known, mod-other-both,

Used from specification heap

heap/heap-aux-inst/ext is used by lift-emp,
heap/ext is used by lift-emp, map-unique, aux-known, lift-unknown, embed-split, get-known, map-in0, mod-other-hp2, write-known, mod-other-both,
heap/in-uni is used by embed-split,
heap/at-write is used by map-unique, aux-known, lift-unknown, get-known, map-in0, write-known,
heap/heap-aux-inst/in-alloc is used by lift-unknown,
heap/in-alloc is used by map-unique, aux-known, lift-unknown, get-known, map-in0, write-known,
heap/heap-aux-inst/in-emp is used by lift-emp, lift-prop, lift-unknown,
heap/in-emp is used by lift-emp, map-unique, aux-known, lift-unknown, get-known, map-in0, write-known,
heap/in-write is used by map-unique, aux-known, lift-unknown, get-known, map-in0, write-known,

Used from specification heap-aux

heap-aux/apply is used by lift-emp, write-other-true, lift-true, switch-aux, merge-owned, switch-obj, lift-ex-o, map-unique, lift-prop, aux-known, lift-unknown, embed-split, embed-and, and-split, lift-false, get-known, map-in0, mod-other-hp2, write-known, mod-other-both,
heap-aux/ex3-03 is used by lift-ex-o,
heap-aux/ext is used by write-other-true, switch-aux, switch-obj, lift-prop, lift-unknown, embed-split,
heap-aux/in-uni is used by embed-split,
heap-aux/mapex is used by lift-unknown,
heap-aux/mapex-new is used by alloc,
heap-aux/maplet is used by lift-unknown,
heap-aux/mk-exists is used by lift-ex-r, embed-split,
heap-aux/mk-ext is used by lift-emp, lift-ex-o, lift-prop, embed-split, embed-and, lift-false,
heap-aux/sep is used by write-other-true, merge-owned, map-same, map-unique, aux-known, lift-unknown, map-in, get-known, mod-other-hp2, write-known, mod-other-both,
heap-aux/split-uni is used by write-other-true, merge-owned, aux-known, lift-unknown, mod-other-hp2, write-known, mod-other-both,
heap-aux/uni is used by embed-split,
heap-aux/at-mk-M01 is used by write-other-true, switch-aux, switch-obj, lift-unknown, embed-split,
heap-aux/at-mk-M02 is used by write-other-true, switch-aux, switch-obj, lift-unknown, embed-split,
heap-aux/at-unil-M01 is used by embed-split,
heap-aux/at-unil-M02 is used by embed-split,
heap-aux/at-unir-M01 is used by embed-split,
heap-aux/at-unir-M02 is used by embed-split,
heap-aux/at-write-M01 is used by lift-unknown,
heap-aux/at-write-M02 is used by lift-unknown,
heap-aux/disj is used by embed-split,
heap-aux/ex1 is used by lift-ex-r,
heap-aux/ex3-03 is used by lift-unknown,
heap-aux/ex3-shift-01 is used by write-unknown, lift-unknown, aux-unknown, get-unknown,
heap-aux/in-mk is used by lift-emp, write-other-true, switch-aux, switch-obj, lift-prop, lift-unknown, embed-split,
heap-aux/in-write is used by lift-unknown,
heap-aux/prop-false is used by lift-false,
heap-aux/prop-true is used by write-other-true, merge-owned, mod-other-hp2, mod-other-both,
heap-aux/true-elim is used by merge-owned-rewrite, split-owned2,