[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,
Used simplifier rules/spec theorems by specification
Used from specification nat
Used from specification list-data
Used from specification pair
Used from specification list
- list/assoclista/In
is used by
ex,
- list/assoclista/c
is used by
cons,
- list/assoclista/Nil
is used by
unique-add,
unique,
nuni-01,
lookup-append-01,
lookup-append,
lookup-01,
lookup,
lastoccurrence-key,
insnotin,
insfirst,
firstoccurrence-key,
firstoc,
app,
- list/assoclista/a
is used by
uniquelen,
unique-put,
unique-del,
unique-add,
unique-04,
unique-03,
unique-02,
unique-01,
unique,
put-one-01,
put-one,
put-in,
perm-unique,
one-01,
one,
nuni-01,
nuni,
not,
lookup-one,
lookup-append-01,
lookup-append,
lookup-02,
lookup-01,
lookup,
lenle,
lenequal,
lastoccurrence-key,
insnotin,
insfirst,
inrec,
inkeys-nc,
inkeys-n,
infirst,
incons,
inapp,
in-put,
in-assoclist-01,
in-assoclist,
in-append,
in-04,
in-03,
in-02,
in,
firstoccurrence-key,
firstoc,
ex,
at-put-01,
at-put,
app,
- list/assoclista/app
is used by
put-one-01,
put-one,
one-01,
one,
lookup-one,
- list/assoclista/app-01
is used by
lastoccurrence-key,
insnotin,
insfirst,
firstoccurrence-key,
firstoc,
- list/assoclista/c
is used by
uniquelen,
unique-put,
unique-del,
unique-add,
unique-02,
unique-01,
unique,
put-in,
perm-unique,
one,
nuni-01,
nuni,
lookup-append-01,
lookup-append,
lookup-02,
lookup-01,
lookup,
lenle,
lenequal,
lastoccurrence-key,
insnotin,
insfirst,
inrec,
in-put,
in-assoclist-01,
in-assoclist,
firstoccurrence-key,
firstoc,
ex,
at-put-01,
at-put,
app,
- list/assoclista/c-04
is used by
insnotin,
- list/assoclista/e-01
is used by
uniquelen,
lenle,
- list/assoclista/in-01
is used by
put-in,
- list/assoclista/in-06
is used by
put-in,
inrec,
inkeys-n,
incons,
in-assoclist-01,
in-assoclist,
- list/assoclista/in-13
is used by
uniquelen,
firstoc,
- list/assoclista/in-17
is used by
uniquelen,
unique-02,
put-in,
lookup-02,
inrec,
inone,
inkeys-n,
firstoc,
- list/assoclista/in-append
is used by
uniquelen,
unique-02,
lookup-02,
inrec,
inkeys-n,
inapp,
firstoc,
- list/assoclista/in-empty
is used by
unique-02,
lookup-02,
inrec,
empty,
- list/assoclista/len
is used by
uniquelen,
lenle,
lenequal,
- list/assoclista/len-02
is used by
uniquelen,
lenle,
lenequal,
Used from specification nat-basic2
- nat-basic2/a
is used by
uniquelen,
lenle,
lenequal,
- nat-basic2/add-base
is used by
uniquelen,
lenle,
lenequal,
- nat-basic2/c
is used by
uniquelen,
lenle,
lenequal,
- nat-basic2/eq-01
is used by
uniquelen,
lenequal,
- nat-basic2/s
is used by
lenle,
- nat-basic2/succ
is used by
uniquelen,
lenle,
lenequal,
Used from specification list-perm
- list-perm/assoclista/del-01
is used by
perm-unique,
- list-perm/assoclista/app
is used by
perm-unique,
- list-perm/assoclista/empty
is used by
perm-unique,
- list-perm/assoclista/empty-01
is used by
perm-unique,
- list-perm/assoclista/in
is used by
perm-unique,
perm-eq,
- list-perm/assoclista/ref
is used by
perm-unique,
perm-eq,
- list-perm/assoclista/sym-01
is used by
perm-unique,
perm-eq,
- list-perm/assoclista/trans
is used by
perm-unique,
perm-eq,
Used from specification nat-basic1
Used from specification list-del