[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. 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
,
Theorem embed-split
⊦ a[hP0 * hP1] = a[hP0] * a[hP1]
Type: A user defined theorem
Validity: The proof is valid.
Features: s,
Comment:
Used by:
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 36
Proof steps: 64
Used lemmas:
lift-aux
,
Used spec theorems:
heap-aux
/
mk-ext
heap-aux
/
apply
heap-fun
/
apply
heap-fun
/
sep
heap-aux
/
uni
heap-sep
/heap-aux-inst/
split-union
heap-sep
/heap-aux-inst/
sep
heap-aux
/
mk-exists
heap-sep
/
sep
heap
/
ext
heap-aux
/
ext
heap
/
in-uni
heap-aux
/
in-uni
Used simplifier rules:
heap-aux
/
disj
set-union
/refset/
unin-01
set-union
/refset/
una
set-union
/refset/
unc
heap-fun
/
disj
heap-fun
/
at-mk
heap-fun
/
in-mk
heap-aux
/
at-mk-M02
heap-aux
/
at-mk-M01
heap-aux
/
in-mk
set-union
/refset/
int-a
set-union
/refset/
int-c
heap-aux
/
at-unil-M01
heap-aux
/
at-unil-M02
heap-fun
/
at-unil
heap-aux
/
at-unir-M01
heap-aux
/
at-unir-M02
heap-fun
/
at-unir
set-basic
/refset/
size-zero-01
set-basic
/refset/
ne-01