[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
Status:
Proved!
Axioms: 12, User Theorems: 76 (Proved: 76, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 444, Interactions: 141
At-in-out(5,1)
Del-other-data(2,0)
del-exists(39,22)
exnotempty(9,5)
inj-put-01(7,3)
k-Del-rec1(2,0)
put-neq-01(2,0)
subset-delete(3,1)
subset-put(11,4)
subset-put-strong-04(7,1)
At-other(0,0)
Del-rec-other(6,1)
del-put(3,1)
exputin(5,3)
ins(3,0)
k-Del-rec2(7,1)
put-same(2,0)
subset-delete-01(6,3)
subset-put-01(21,8)
subset-put-strong-05(9,1)
At-other-num(2,0)
Del-rec-same(2,0)
del-putsame(2,0)
ext-rec(6,4)
ins-same(4,2)
k-Extension(4,2)
rew(5,0)
subset-delete-02(3,1)
subset-put-02(12,4)
subset-size(18,6)
At-same(0,0)
Extension(0,0)
deldel(3,1)
gen(0,0)
ins-same-01(2,0)
key-size(24,12)
size(6,2)
subset-elem-eq(4,2)
subset-put-03(2,0)
superset-elem-eq(2,0)
Del-at(12,3)
In-empty(0,0)
delete-put-rew(7,1)
in-neq(2,0)
ins3(6,1)
lookupisempty(1,1)
size-in(9,3)
subset-elem-eq-01(4,1)
subset-put-04(1,1)
superset-elem-in(4,1)
Del-at-strong(2,0)
In-insert(0,0)
empty(3,0)
indef(6,1)
ins4(1,1)
neq(3,0)
size-neq(2,0)
subset-elem-eq-02(2,0)
subset-put-strong(2,0)
superset-elem-in-01(4,1)
Del-empty(4,1)
Size-empty(0,0)
eq-shift-del(15,5)
indef-01(3,1)
insin(1,0)
notin-del-notin(5,1)
size-subset(3,1)
subset-empty(1,0)
subset-put-strong-01(2,0)
sw-01(6,0)
Del-in(7,5)
Size-insert(0,0)
eq-shift-put(19,7)
inex(4,1)
insins(2,0)
notmemlookup(5,1)
sub-ref(1,0)
subset-empty-01(4,1)
subset-put-strong-02(2,0)
Del-notin(8,2)
Subset(0,0)
exin(2,1)
inj-put(9,3)
k-At-same(2,0)
put-neq(5,1)
sub-trans(5,2)
subset-new(3,1)
subset-put-strong-03(5,1)