[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 search-tree

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:
insert-bstprovedall subs proved insert-branch-same, insert-branch-right, bst-elem-order-right, bst-elem-order-left, insert-in, insert-branch-left, bst-branch-rec, bst-elem-in-branch, in-leaf, bst-branch, insert-leaf, bst-leaf,
delete-prepost-minprovedall subs proved delete-prepost, leftmost-ismin, bst-elem-order-left, butleftmost-in, leftmost-in, in-branch, bst-elem-order-right, in-leaf, bst-leaf, bst-branch-rec, bst-elem-in-branch, leftmost, butleftmost, butleftmost-bst, root-nonnull,
insert-inprovedall subs proved insert-branch-same, bst-elem-order-right, insert-branch-right, bst-elem-order-left, insert-branch-left, bst-branch-rec, bst-elem-in-branch, in-leaf, in-branch, insert-leaf,
butleftmost-bstprovedall subs proved butleftmost-in, bst-branch, bst-elem-in-branch, bst-branch-rec, butleftmost, in-branch, leftmost, leftmost-in,
leftmost-isminprovedall subs proved bst-elem-order-left, bst-elem-order-right, in-leaf, bst-leaf, bst-branch-rec, bst-elem-in-branch, in-branch, leftmost, leftmost-in,
bst-elem-order-leftprovedall subs proved bst-branch, bst-elem-in-branch, bst-branch-rec,
butleftmost-inprovedall subs proved in-leaf, bst-leaf, bst-branch, bst-elem-in-branch, bst-branch-rec, leftmost, in-branch, butleftmost, leftmost-in,
bst-branch-recprovedall subs proved bst-branch, bst-elem-in-branch,
bst-elem-in-branchprovedall subs proved bst-branch, bst-elem-order-right,
insert-prepostprovedall subs proved insert-branch-same, insert-branch-right, insert-branch-left, root-nonnull, mknode-prepost, insert-leaf, search_tree_insert,
mknode-prepostprovedall subs proved search_tree_mknode,
delete-prepostprovedall subs proved search_tree_delete_min, leftmost, butleftmost, root-nonnull,
leftmost-inprovedall subs proved in-branch, leftmost,
bst-elem-order-rightprovedall subs proved bst-branch,
delete-prepost-loopprovedall subs proved leftmost, butleftmost, search_tree_delete_min,
search_tree_mknodeaxiom
search_tree_insertaxiom
insert-leafaxiom
insert-branch-leftaxiom
insert-branch-rightaxiom
insert-branch-sameaxiom
root-nonnullprovedall subs proved
search_tree_delete_minaxiom
bst-leafaxiom
in-leafaxiom
leftmostaxiom
in-branchaxiom
butleftmostaxiom
bst-branchaxiom