[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 ablock-store-refsize-cons
Status:
Proved!
Axioms: 5, User Theorems: 28 (Proved: 28, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 259, Interactions: 94
in-remove-refsize0-refsize-cons(27,11)
refsize-cons-emtpy(1,0)
remove-refsize0-subset-refed(31,12)
restrict-in(1,0)
size-eq-0(22,7)
size-rem(5,2)
inv-valid-adrs(18,8)
refsize-cons-remove-index(6,2)
restrict-add(9,4)
restrict-leb(0,0)
size-eq-0-alloc(2,1)
subseteq-dom-nodes-alloc-restrict-empty(5,1)
refsize-cons-alloc(8,3)
refsize-cons-remove-index-0(6,2)
restrict-add-other(9,3)
restrict-subseteq(1,1)
size-eq-sets(2,0)
valid-adrs(0,0)
refsize-cons-append(10,4)
refsize-cons-remove-refsize0(4,0)
restrict-del(3,2)
restrict-union(13,7)
size-rec(0,0)
refsize-cons-dealloc(4,0)
refsize-cons-write(22,1)
restrict-del-other(5,2)
restrict-union-inter-empty-left(9,5)
size-rec-rem(6,2)
refsize-cons-def(0,0)
remove-refsize0-refsize-cons(27,12)
restrict-empty(2,1)
size-emp(0,0)
size-rec-simp(1,1)