[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 assoclist
Status:
Proved!
Axioms: 10, User Theorems: 55 (Proved: 55, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 334, Interactions: 126
app(8,3)
firstoc(12,4)
in-assoclist(6,2)
inkeys-nc(1,0)
lookup(6,1)
nuni(6,2)
put-no(0,0)
unique-02(10,4)
uniquelen(19,8)
assoc-no(0,0)
firstoccurrence-key(14,7)
in-assoclist-01(6,2)
inone(2,0)
lookup-01(6,1)
nuni-01(4,0)
put-one(1,1)
unique-03(1,0)
assoc-yes(0,0)
in(1,0)
in-put(7,4)
inrec(11,1)
lookup-02(10,2)
one(2,1)
put-one-01(2,1)
unique-04(1,0)
at-put(10,4)
in-01(2,0)
inapp(14,6)
insfirst(6,2)
lookup-append(10,2)
one-01(1,1)
put-yes(0,0)
unique-add(11,4)
at-put-01(6,3)
in-02(1,0)
inassoc(0,0)
insnotin(6,2)
lookup-append-01(6,1)
perm-eq(6,3)
rassoc-no(0,0)
unique-del(14,8)
cons(2,2)
in-03(1,0)
incons(2,0)
lastoccurrence-key(12,5)
lookup-one(2,1)
perm-unique(15,8)
rassoc-yes(0,0)
unique-e(0,0)
empty(1,0)
in-04(1,0)
infirst(1,0)
lenequal(12,7)
not(2,0)
put-empty(0,0)
unique(8,3)
unique-put(8,5)
ex(6,2)
in-append(1,0)
inkeys-n(2,0)
lenle(14,6)
not-in(1,0)
put-in(8,5)
unique-01(6,2)
unique-r(0,0)