[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. 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,

Theorem search_tree_delete_min

search_tree_delete_min(; a, r, H) {let r0 = H[r].left in if r0 = null then {a := H[r].val; r := H[r].right, H := H -- r} else let r1 = r, r2 = H[r0].left in {while r2 ≠ null do {r1 := r0; r0 := r2; r2 := H[r0].left}; a := H[r0].val; r2 := H[r0].right; H := H -- r0; H := H[r1, H[r1].left:= r2]} }