[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 btree-inv

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:
btree-inv-remove-refsize0provedall subs proved btree-reset-root, btree-crash, btree-clean-fwd-strong, btree, btree-istore-reduce-refed, btree-root-in-heap, btree-null-or-clean-below, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs, btree-inv,
btree-reset-rootprovedall subs proved btree-reset-root-frame,
btree-ri-uniqueprovedall subs proved btree-remove-context, nat-le-eq, ri-range-ext, bnode, maplet-null, btree-root-in-heap, btree-leaf-adr, bleaf, btree, btree-clean-fwd, btree-clean-alladrs, btree-null-or-clean-below, btree-adrs, btree-refed-subseteq-alladrs,
btree-restrict-union-properprovedall subs proved btree-istore-reduce-refed, btree-adrs, btree-refed-subseteq-alladrs, btree-istore-restrict, btree-istore-restrict-to-as,
btree-inv-root-null-or-cleanprovedall subs proved btree-crash, btree-istore-reduce, btree-clean-fwd, btree-root-in-heap, btree-null-or-clean-below, btree-adrs, btree-refed-subseteq-alladrs, btree-inv,
btree-inv-root-nullinvalidall subs proved btree-istore-reduce, btree-crash, btree-clean-fwd, btree-null-or-clean-below, btree-adrs, btree-refed-subseteq-alladrs, btree-inv,
btree-inv-crashinvalidall subs proved btree-clean-alladrs, btree, btree-clean-fwd, btree-crash, btree-istore-reduce, btree-adrs, btree-refed-subseteq-alladrs, btree-inv,
btree-inv-clean-commitprovedall subs proved btree-clean-fwd, btree-crash, btree-istore-reduce, btree-root-in-heap, btree-null-or-clean-below, btree-adrs, btree-refed-subseteq-alladrs, btree-inv,
btree-as-emptyprovedall subs proved btree-as-empty-rev, btree-istore-restrict, btree-adrs, btree-refed-subseteq-alladrs,
btree-reset-root-frameprovedall subs proved maplet-null, btree, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs,
btree-clean-fwd-strongprovedall subs proved nat-le-eq, ri-range-ext, btree-remove-context, bnode, bleaf, btree, btree-leaf-adr, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs,
btree-clean-fwdprovedall subs proved btree-remove-context, nat-le-eq, ri-range-ext, bnode, bleaf, btree, btree-leaf-adr, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs,
btree-istore-restrictprovedall subs proved btree-istore-reduce, restrict-dom, btree-adrs, btree-refed-subseteq-alladrs,
btree-write-nodeprovedall subs proved btree-sub-clean, btree-root-in-heap, btree-null-or-clean-below, btree-istore-reduce, sep-forall-reduce, bnode, maplet-null, bleaf, btree, btree-leaf-adr, btree-dirty-adr-notin, btree-adrs, btree-refed-subseteq-alladrs,
btree-mark-dirtyprovedall subs proved btree-imp-dirty, sep-forall-reduce, bnode, maplet-null, bleaf, btree, btree-leaf-adr, btree-clean-adr-in, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs,
btree-inv-root-neq-null-fwdprovedall subs proved btree-root-in-heap, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs, btree-inv,
btree-inv-formatinvalidall subs proved infinite-memory, bleaf, btree, btree-crash, btree-adrs, btree-refed-subseteq-alladrs, btree-inv,
btree-inv-allocprovedall subs proved btree-crash, btree-istore-reduce-refed, btree-adrs, btree-refed-subseteq-alladrs, btree-clean-alladrs, btree-inv,
btree-istore-restrict-to-asprovedall subs proved btree-istore-reduce-refed, btree-adrs, btree-refed-subseteq-alladrs,
btree-istore-reduceprovedall subs proved subseteq-restrict, btree-istore-reduce-refed, btree-adrs, btree-refed-subseteq-alladrs,
btree-crashprovedall subs proved btree-null,
btree-clean-alladrsprovedall subs proved btree-remove-context, nat-le-eq, bnode, bleaf, btree, btree-adrs, btree-refed-subseteq-alladrs, btree-leaf-adr,
btree-as-empty-revprovedall subs proved btree-istore-reduce-refed, btree-adrs, btree-refed-subseteq-alladrs,
btree-repl-dirty-addressprovedall subs proved bleaf, maplet-null, btree, btree-dirty-adr-notin, btree-adrs, btree-refed-subseteq-alladrs,
btree-dirty-adr-notinprovedall subs proved bleaf, btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-clean-adr-inprovedall subs proved bleaf, btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-root-in-heapprovedall subs proved maplet-null, btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-nullprovedall subs proved btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-leaf-adrprovedall subs proved bleaf, btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-remove-contextprovedall subs proved congruent, btree-adrs, btree-refed-subseteq-alladrs,
btree-istore-reduce-refedprovedall subs proved maplet-null, restrict-further, sep-forall-reduce, bnode, restrict-add-at, restrict-add-in, restrict-add-subseteq-at, restrict-add-subseteq-in, bleaf, btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-write-otherinvalidall subs proved btree-imp-dirty, maplet-null, btree-adrs, btree-refed-subseteq-alladrs, sep-forall-reduce, bnode, bleaf, btree,
btree-leaf-fwdprovedall subs proved btree, btree-adrs, btree-refed-subseteq-alladrs,
btree-adrsprovedall subs proved nat-le-eq, bnode, btree-refed-subseteq-alladrs, maplet-null, bleaf, btree,
btree-refed-subseteq-alladrsprovedall subs proved nat-le-eq, btree-imp-dirty, maplet-null, bnode, bleaf, btree,
inter-subseteq-weakenprovedall subs proved inter-subseteq-simp,
inter-subseteq-simpprovedall subs proved subseteq-inter-same,
btree-imp-dirtyprovedall subs proved btree,
restrict-furtherprovedall subs proved restrict-add-in,
btree-null-or-clean-belowprovedall subs proved maplet-null, btree,
restrict-idemprovedall subs proved restrict-2,
btree-sub-clean-write-branchesprovedall subs proved btree-sub-clean,
btree-sub-clean-nextprovedall subs proved btree-sub-clean,
btree-sub-clean-leafprovedall subs proved btree-sub-clean,
btree-sub-clean-0provedall subs proved btree-sub-clean,
btree-inv-adr-lnum-inprovedall subs proved btree-inv,
restrict-2provedall subs proved
subseteq-inter-sameprovedall subs proved
btree-sub-cleanaxiom
congruentaxiom
restrict-domprovedall subs proved
restrict-add-subseteq-inprovedall subs proved
restrict-add-subseteq-atprovedall subs proved
restrict-add-inprovedall subs proved
restrict-add-atprovedall subs proved
sep-forall-reduceprovedall subs proved
subseteq-restrictprovedall subs proved
infinite-memoryaxiom
btree-invaxiom
ri-range-extprovedall subs proved
btreeaxiom
bleafaxiom
maplet-nullprovedall subs proved
bnodeaxiom
nat-le-eqprovedall subs proved