[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-basic
- nat-basic/a
is used by
lenle,
lenequal,
uniquelen,
- nat-basic/c
is used by
lenle,
lenequal,
uniquelen,
- nat-basic/eq-01
is used by
lenequal,
uniquelen,
- nat-basic/f
is used by
lenle,
- nat-basic/s-04
is used by
lenle,
- nat-basic/succ
is used by
lenle,
lenequal,
uniquelen,
Used from specification nat
Used from specification list-data
Used from specification pair
Used from specification list
- list/assoclist/c
is used by
cons,
- list/assoclist/in-def
is used by
ex,
- list/assoclist/Nil
is used by
app,
insnotin,
firstoc,
insfirst,
unique,
nuni-01,
- list/assoclist/a
is used by
infirst,
inkeys-n,
in-put,
in-03,
ex,
unique-03,
one-01,
inkeys-nc,
unique-04,
incons,
app,
unique-01,
lenle,
in,
insnotin,
k-unique-r,
inapp,
lenequal,
firstoc,
uniquelen,
insfirst,
unique,
in-02,
unique-02,
not,
inrec,
one,
put-one,
nuni-01,
nuni,
- list/assoclist/app
is used by
one-01,
one,
put-one,
- list/assoclist/c
is used by
in-put,
ex,
app,
unique-01,
lenle,
insnotin,
k-unique-r,
lenequal,
firstoc,
uniquelen,
insfirst,
unique,
unique-02,
one,
nuni-01,
nuni,
- list/assoclist/c-04
is used by
insnotin,
- list/assoclist/e-01
is used by
lenle,
k-unique-r,
uniquelen,
- list/assoclist/in-17
is used by
ex,
inone,
- list/assoclist/in-append
is used by
ex,
inapp,
- list/assoclist/in-empty
is used by
empty,
unique-02,
- list/assoclist/in-rec
is used by
unique-02,
- list/assoclist/len
is used by
lenle,
lenequal,
uniquelen,
- list/assoclist/len-01
is used by
insnotin,
firstoc,
insfirst,
- list/assoclist/len-05
is used by
lenle,
lenequal,
uniquelen,