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