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