[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
- heap/disj-com
is used by
precise-sep,
- heap/disj-distr-uni
is used by
wand-flatten,
precise-sep,
- heap/disj-distr-uni-com
is used by
sep-partial-mp,
- heap/ext
is used by
sharing-emp,
- heap/subset-uni
is used by
precise-alt-def,
- heap/uni-ass
is used by
wand-shift,
wand-flatten,
sharing-com,
sep-partial-mp,
sep-ass,
precise-sep,
precise-disj,
- heap/uni-com
is used by
wand-shift,
wand-flatten,
sharing-com,
sep-partial-mp,
sep-com,
sep-ass,
precise-split-r,
precise-disj,
introduce-sharing,
and-combine,
- heap/uni-inj
is used by
precise-sep,
- heap/disj-com-rw
is used by
wand-shift,
wand-flatten,
sharing-com,
sep-partial-mp,
sep-com,
sep-ass,
precise-split-r,
precise-sep,
precise-disj,
precise-alt-def,
introduce-sharing,
and-combine,
adjunction,
- heap/disj-distr-uni
is used by
wand-shift,
wand-flatten,
sep-partial-mp,
sep-ass,
precise-disj,
introduce-sharing,
- heap/disj-distr-uni-com
is used by
wand-shift,
wand-flatten,
sep-ass,
precise-sep,
- heap/disj-emp-l
is used by
wand-same-emp-p,
sharing-emp,
emp-sep,
- heap/disj-emp-r
is used by
wand-same-emp,
sharing-emp,
- heap/in-emp
is used by
sharing-emp,
- heap/in-uni
is used by
sharing-emp,
- heap/uni-com
is used by
adjunction,
- heap/uni-emp
is used by
wand-same-emp,
sharing-emp,
- heap/uni-emp-l
is used by
wand-same-emp-p,
sharing-emp,
emp-sep,
- heap/uni-inj
is used by
precise-split-l,
precise-same,