[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 app, nuni-01, nuni, ex, inone, cons, inapp, empty, unique-e,
unique-01provedall subs proved inone, cons, inapp, copied-empty, unique,
unique-03provedall subs proved nuni-01, nuni,
firstocprovedall subs proved inkeys-n, inone, inapp, copied-empty,
unique-04provedall subs proved nuni-01, nuni,
inkeys-ncprovedall subs proved inkeys-n,
lenequalprovedall subs proved app, nuni-01, nuni, inkeys-n, ex, inone, cons, inapp,
in-putprovedall subs proved put-yes, inkeys-n, put-no, inapp, inone, put-empty, copied-empty,
inkeys-nprovedall subs proved incons, copied-inrec,
uniqueprovedall subs proved cons, inone, inapp, unique-e, one,
nuniprovedall subs proved inone, cons, inapp, copied-empty, nuni-01,
infirstprovedall subs proved copied-inrec,
oneprovedall subs proved unique-e, copied-empty, unique-r,
inconsprovedall subs proved inapp,
copied-inrecprovedall subs proved inone, inapp,
nuni-01provedall subs proved not, cons,
appprovedall subs proved inapp, cons, not,
insnotinprovedall subs proved put-no, inone, inapp, put-empty,
in-02provedall subs proved inone, inapp,
in-03provedall subs proved inapp,
insfirstprovedall subs proved put-no, inone, inapp, put-yes,
unique-02provedall subs proved in-01, cons,
inprovedall subs proved in-01, cons,
lenleprovedall subs proved ex, copied-empty, unique-e, inone, cons, inapp,
notprovedall subs proved cons,
in-01provedall subs proved inassoc,
copied-emptyprovedall subs proved inassoc,
exprovedall subs proved inassoc,
inappprovedall subs proved inassoc,
inoneprovedall subs proved inassoc,
k-unique-rprovedall subs proved cons, unique-e,
inassocprovedall subs proved inrec, empty,
consprovedall subs proved unique-r,
one-01provedall subs proved assoc-yes,
put-oneprovedall subs proved put-yes,
assoc-yesaxiom
inrecaxiom
unique-raxiom
put-yesaxiom
unique-eaxiom
emptyaxiom
put-emptyaxiom
put-noaxiom