---

Step * 1 of Lemma bs_tree_delete_wf

.....set predicate..... 
1. E : Type
2. cmp : comparison(E)
3. x : E
4. tr : bs_tree(E)
5. bs_tree_ordered(E;cmp;tr)
⊢ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;tr))
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN (BLemma `bs_tree-induction` THENA Auto)) }

1
1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ bs_tree_ordered(E;cmp;bst_null()) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;bst_null()))

2
1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀value:E. (bs_tree_ordered(E;cmp;bst_leaf(value)) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;bst_leaf(value))))

3
1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((bs_tree_ordered(E;cmp;left) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;left)))
    ⇒ (bs_tree_ordered(E;cmp;right) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;right)))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;bst_node(left;value;right))))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  E  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
4.  tr  :  bs\_tree(E)
5.  bs\_tree\_ordered(E;cmp;tr)
\mvdash{}  bs\_tree\_ordered(E;cmp;bs\_tree\_delete(cmp;x;tr))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  (BLemma  `bs\_tree-induction`  THENA  Auto))

---

Home Index