[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
,
Theorem base summary for Specification maplet
Status:
Proved!
Axioms: 4, User Theorems: 32 (Proved: 32, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 252, Interactions: 111
at-eq(3,1)
ex(0,0)
ex2(0,0)
ex3(0,0)
map-del(8,4)
map-same(5,2)
at-eq-sharing(12,5)
ex1-shift(10,4)
ex2-shift(10,4)
ex3-shift(10,4)
map-del-sharing(47,27)
map-write(7,2)
at-rw(3,1)
ex1-shiftw(14,7)
ex2-shiftw(14,7)
ex3-shiftw(14,7)
map-in(3,1)
maplet(0,0)
at-rw-sharing(2,0)
ex1-shiftw-inst(8,3)
ex2-shiftw-inst(8,3)
ex3-shiftw-inst(8,3)
map-in0(2,0)
maplet-singleton-heap(2,0)
at-rw-singleton(2,0)
ex1-shiftwr(7,3)
ex2-shiftwr(7,2)
ex3-shiftwr(7,3)
map-null(2,1)
maplet-unique(7,3)
eq-objs(5,2)
ex1-shiftwr-impl(4,2)
ex2-shiftwr-impl(4,2)
ex3-shiftwr-impl(4,2)
map-put-rw(11,5)
precise-map(2,1)