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

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:
eq-objsprovedall subs proved at-eq, at-rw,
map-delprovedall subs proved maplet, at-eq, map-in,
at-eqprovedall subs proved at-rw,
at-rwprovedall subs proved maplet, map-in0,
at-rw-sharingprovedall subs proved at-eq-sharing,
map-put-rwprovedall subs proved maplet, map-write, map-in,
ex1-shiftwr-implprovedall subs proved ex1-shiftwr,
ex3-shiftwr-implprovedall subs proved ex3-shiftwr,
ex2-shiftwr-implprovedall subs proved ex2-shiftwr,
ex1-shiftw-instprovedall subs proved ex1-shiftw,
ex2-shiftw-instprovedall subs proved ex2-shiftw,
ex3-shiftw-instprovedall subs proved ex3-shiftw,
ex3-shiftwprovedall subs proved ex3,
ex2-shiftwprovedall subs proved ex2,
ex1-shiftwprovedall subs proved ex,
ex2-shiftwrprovedall subs proved ex2,
ex3-shiftwrprovedall subs proved ex3,
ex1-shiftwrprovedall subs proved ex,
map-writeprovedall subs proved maplet,
map-inprovedall subs proved maplet,
map-in0provedall subs proved maplet,
at-eq-sharingprovedall subs proved maplet,
ex2-shiftprovedall subs proved ex2,
precise-mapprovedall subs proved maplet,
maplet-uniqueprovedall subs proved maplet,
maplet-singleton-heapprovedall subs proved maplet,
map-sameprovedall subs proved maplet,
map-del-sharingprovedall subs proved maplet,
ex3-shiftprovedall subs proved ex3,
map-nullprovedall subs proved maplet,
at-rw-singletonprovedall subs proved maplet,
ex1-shiftprovedall subs proved ex,
mapletaxiom
ex3axiom
ex2axiom
exaxiom