---

Step * 2 of Lemma bs_tree_insert_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_insert(cmp;x;tr))
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN (BLemma `bs_tree-induction` THENW Auto)
   THEN (UnivCD THENA Auto)
   THEN (RepUR ``bs_tree_insert`` 0 THEN Try (Fold `bs_tree_insert` 0))
   THEN Try (((CallByValueReduce 0 THENA Auto) THEN Repeat (AutoSplit)))
   THEN RepUR ``bs_tree_ordered`` 0
   THEN Try (Fold `bs_tree_ordered` 0)
   THEN RepUR ``member_bs_tree`` 0
   THEN Try (Fold `member_bs_tree` 0)
   THEN Try (Trivial)
   THEN Try (OnSomeHyp (\h. (RepUR ``bs_tree_ordered`` h THEN Fold `bs_tree_ordered` h) THEN Auto)⋅)
   THEN Auto) }

1
1. E : Type
2. cmp : comparison(E)
3. x : E
4. value : E
5. ¬0 < cmp value x
6. bs_tree_ordered(E;cmp;bst_leaf(value))
7. cmp value x < 0
8. True
9. True
10. ∀x@0:E. (False ⇒ 0 < cmp x@0 x)
11. x@0 : E
12. value = x@0 ∈ E
⊢ 0 < cmp x x@0

2
1. E : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. right : bs_tree(E)
7. bs_tree_ordered(E;cmp;left)
8. bs_tree_ordered(E;cmp;right)
9. ∀x:E. (x ∈ left ⇒ 0 < cmp x value)
10. ∀x:E. (x ∈ right ⇒ 0 < cmp value x)
11. 0 < cmp value x
12. bs_tree_ordered(E;cmp;left)
13. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;right))
14. ∀x:E. (x ∈ left ⇒ 0 < cmp x value)
15. x@0 : E
16. x@0 ∈ bs_tree_insert(cmp;x;right)
17. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;right))
18. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;left))
⊢ 0 < cmp value x@0

3
1. E : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. ¬0 < cmp value x
7. right : bs_tree(E)
8. bs_tree_ordered(E;cmp;left)
9. bs_tree_ordered(E;cmp;right)
10. ∀x:E. (x ∈ left ⇒ 0 < cmp x value)
11. ∀x:E. (x ∈ right ⇒ 0 < cmp value x)
12. cmp value x < 0
13. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;left))
14. bs_tree_ordered(E;cmp;right)
15. x@0 : E
16. x@0 ∈ bs_tree_insert(cmp;x;left)
17. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;right))
18. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;left))
⊢ 0 < cmp x@0 value

4
1. E : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. ¬cmp value x < 0
7. ¬0 < cmp value x
8. right : bs_tree(E)
9. bs_tree_ordered(E;cmp;left)
10. bs_tree_ordered(E;cmp;right)
11. ∀x:E. (x ∈ left ⇒ 0 < cmp x value)
12. ∀x:E. (x ∈ right ⇒ 0 < cmp value x)
13. bs_tree_ordered(E;cmp;left)
14. bs_tree_ordered(E;cmp;right)
15. x@0 : E
16. x@0 ∈ left
17. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;right))
18. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;left))
⊢ 0 < cmp x@0 x

5
1. E : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. ¬cmp value x < 0
7. ¬0 < cmp value x
8. right : bs_tree(E)
9. bs_tree_ordered(E;cmp;left)
10. bs_tree_ordered(E;cmp;right)
11. ∀x:E. (x ∈ left ⇒ 0 < cmp x value)
12. ∀x:E. (x ∈ right ⇒ 0 < cmp value x)
13. bs_tree_ordered(E;cmp;left)
14. bs_tree_ordered(E;cmp;right)
15. ∀x@0:E. (x@0 ∈ left ⇒ 0 < cmp x@0 x)
16. x@0 : E
17. x@0 ∈ right
18. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;right))
19. bs_tree_ordered(E;cmp;bs_tree_insert(cmp;x;left))
⊢ 0 < cmp x x@0

---

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\_insert(cmp;x;tr))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (BLemma  `bs\_tree-induction`  THENW  Auto)
  THEN  (UnivCD  THENA  Auto)
  THEN  (RepUR  ``bs\_tree\_insert``  0  THEN  Try  (Fold  `bs\_tree\_insert`  0))
  THEN  Try  (((CallByValueReduce  0  THENA  Auto)  THEN  Repeat  (AutoSplit)))
  THEN  RepUR  ``bs\_tree\_ordered``  0
  THEN  Try  (Fold  `bs\_tree\_ordered`  0)
  THEN  RepUR  ``member\_bs\_tree``  0
  THEN  Try  (Fold  `member\_bs\_tree`  0)
  THEN  Try  (Trivial)
  THEN  Try  (OnSomeHyp  (\mbackslash{}h.  (RepUR  ``bs\_tree\_ordered``  h  THEN  Fold  `bs\_tree\_ordered`  h)  THEN  Auto)\mcdot{})
  THEN  Auto)

---

Home Index