---

Step * of Lemma bs_tree_delete_wf1

∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_delete(cmp;x;tr) ∈ bs_tree(E))
BY
{ (Auto
   THEN Unfold `bs_tree_delete` 0
   THEN MemCD
   THEN Try (Complete (Auto))
   THEN InstLemma `bs_tree_max_wf1` [⌜E⌝;⌜a⌝;⌜v⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}[cmp:comparison(E)].  \mforall{}[x:E].  \mforall{}[tr:bs\_tree(E)].    (bs\_tree\_delete(cmp;x;tr)  \mmember{}  bs\_tree(E))


By

---

Latex:
(Auto
  THEN  Unfold  `bs\_tree\_delete`  0
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  InstLemma  `bs\_tree\_max\_wf1`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index