[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 store-access
Status:
Proved!
Axioms: 13, User Theorems: 76 (Proved: 76, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 268, Interactions: 83
At-in-out(4,1)
Data-in-putdel(4,1)
Dom(0,0)
del-empty(1,1)
dom-ins(1,1)
indef(5,0)
insert(3,2)
put-neq-01(3,2)
subset-elem-eq-01(2,0)
subset-put-strong-03(4,1)
At-other(0,0)
Data-in-putdelput(6,1)
Extension(0,0)
del-exists(19,9)
dom-isemp(2,1)
indef-01(5,0)
insin(1,0)
put-same(1,0)
subset-elem-eq-02(1,0)
subset-put-strong-04(6,1)
At-other-num(2,0)
Data-in-puteq(1,0)
In-data-in(1,1)
del-notin(4,1)
empty(13,8)
inex(6,3)
insins(2,0)
rew(6,1)
subset-empty(1,0)
subset-put-strong-05(8,1)
At-other-strong(1,0)
Data-in-putsame(2,1)
In-empty(0,0)
del-put(2,0)
eq-shift-put(9,4)
inj-put(2,1)
k-Extension(8,4)
sub-ref(1,0)
subset-empty-01(8,2)
superset-elem-eq(1,0)
At-same(0,0)
Data-notin-other(4,2)
In-insert(0,0)
del-putsame(2,0)
exin(5,2)
inj-put-01(1,0)
lookupisempty(1,1)
sub-trans(3,2)
subset-put(2,0)
superset-elem-in(2,0)
Data-in(0,0)
Data-notin-other-2(2,1)
Ran(0,0)
deldel(2,1)
exnotempty(9,5)
ins(2,0)
neq(2,0)
subset-delete(1,0)
subset-put-01(2,0)
superset-elem-in-01(2,0)
Data-in-del(2,1)
Data-notin-other-3(2,1)
Size-empty(0,0)
delete-put-rew(6,1)
exputin(5,3)
ins-same(2,0)
notin-emp(3,1)
subset-delete-01(6,0)
subset-put-strong(1,0)
sw(2,1)
Data-in-delput(4,1)
Del-at(0,0)
Size-insert(0,0)
dom-del(1,1)
in-neq(1,0)
ins-same-01(2,0)
notmemlookup(4,1)
subset-delete-02(6,0)
subset-put-strong-01(1,0)
sw-01(6,3)
Data-in-delput-2(6,1)
Del-in(0,0)
Subset(0,0)
dom-emp(2,1)
in-notemp(1,0)
ins3(6,1)
put-neq(8,4)
subset-elem-eq(2,0)
subset-put-strong-02(1,0)