[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,

Lemma dependency for Specification assoclist

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
uniquelenprovedall subs proved nuni, app, nuni-01, ex, inone, cons, inapp, empty, unique-e,
unique-addprovedall subs proved inone, cons, not, in-append, one, empty, unique-e, unique, unique-01,
unique-04provedall subs proved nuni-01, nuni,
unique-03provedall subs proved nuni-01, nuni,
perm-eqprovedall subs proved lookup-02, unique-02, inassoc, perm-unique,
lenequalprovedall subs proved app, nuni-01, nuni, ex, inone, cons, inapp, empty, unique-e,
infirstprovedall subs proved inrec,
unique-01provedall subs proved inone, cons, inapp, empty, unique,
perm-uniqueprovedall subs proved unique-02, inassoc, unique-del, cons, unique-e,
nuniprovedall subs proved inone, cons, inapp, empty, nuni-01,
inrecprovedall subs proved in-01, inassoc, inkeys-nc,
unique-putprovedall subs proved in-put, cons, put-yes, put-no, unique-e, one, put-empty,
in-putprovedall subs proved inapp, put-yes, put-no, in-append, empty, inone, put-empty,
uniqueprovedall subs proved inone, inapp, cons, unique-e, one,
unique-delprovedall subs proved unique-02, inassoc, inone, inapp, cons, empty, unique-e,
lookup-02provedall subs proved not, in-01, assoc-no, cons, assoc-yes, unique-e, unique-02,
nuni-01provedall subs proved not, cons,
appprovedall subs proved inapp, cons, not,
inkeys-ncprovedall subs proved in-01, inassoc, inkeys-n,
lookup-append-01provedall subs proved assoc-no, inone, in-append,
lenleprovedall subs proved ex, empty, unique-e, inone, cons, inapp,
lastoccurrence-keyprovedall subs proved inapp, empty, inone, in-append,
firstoccurrence-keyprovedall subs proved inapp, empty, inone, in-append,
oneprovedall subs proved unique-e, empty, unique-r,
unique-02provedall subs proved in-01, cons,
exprovedall subs proved inassoc, inone, inapp,
inkeys-nprovedall subs proved in-01, inassoc,
in-appendprovedall subs proved inapp,
notprovedall subs proved cons,
not-inprovedall subs proved in-01,
lookup-appendprovedall subs proved assoc-no, assoc-yes, inone, inapp, empty,
lookup-01provedall subs proved assoc-no, inone, inapp, one-01,
lookupprovedall subs proved assoc-no, inone, inapp, assoc-yes,
insnotinprovedall subs proved put-no, inone, inapp, put-empty,
insfirstprovedall subs proved put-no, inone, inapp, put-yes,
in-assoclist-01provedall subs proved assoc-no, assoc-yes, inone, inapp, empty,
in-assoclistprovedall subs proved assoc-no, assoc-yes, inone, inapp, empty,
in-04provedall subs proved inone, inapp,
in-03provedall subs proved inapp,
in-02provedall subs proved inone, inapp,
inprovedall subs proved in-01, cons,
firstocprovedall subs proved inone, inapp, empty,
at-put-01provedall subs proved assoc-no, assoc-yes, put-yes, put-no, one-01, put-empty,
at-putprovedall subs proved assoc-yes, assoc-no, put-yes, put-no, lookup-one, put-empty,
in-01provedall subs proved inassoc,
emptyprovedall subs proved inassoc,
inoneprovedall subs proved inassoc,
one-01provedall subs proved assoc-yes,
lookup-oneprovedall subs proved assoc-no,
consprovedall subs proved unique-r,
inappprovedall subs proved inassoc,
put-one-01provedall subs proved put-empty, put-no,
put-oneprovedall subs proved put-yes,
put-inprovedall subs proved put-yes, put-no, put-empty,
inconsprovedall subs proved inassoc,
unique-eaxiom
inassocaxiom
unique-raxiom
put-emptyaxiom
put-noaxiom
put-yesaxiom
assoc-noaxiom
assoc-yesaxiom