Proof of Nuprl Lemma : member_bs_tree

Step * 3 of Lemma member_bs_tree_insert

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)
     ⇒ (∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))))
    ⇒ (bs_tree_ordered(E;cmp;right)
       ⇒ (∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ (∀y:E
          (y ∈ bs_tree_insert(cmp;x;bst_node(left;value;right))
          ⇐⇒ (y = x ∈ E) ∨ (y ∈ bst_node(left;value;right) ∧ (¬((cmp x y) = 0 ∈ ℤ))))))
BY
{ ((Intros THEN RepUR ``bs_tree_ordered`` -2 THEN Fold `bs_tree_ordered` (-2))
   THEN (RepUR ``bs_tree_insert`` 0 THEN Fold `bs_tree_insert` 0)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (AutoSplit)
   THEN RepUR ``member_bs_tree`` 0
   THEN Fold `member_bs_tree` 0
   THEN (RWW  "7 8" 0 THENA Auto)
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

1
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. y : E
12. 0 < cmp value x
13. value = y ∈ E
14. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (y = x ∈ E) ∨ (((value = y ∈ E) ∨ y ∈ left ∨ y ∈ right) ∧ (¬((cmp x y) = 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. y : E
12. 0 < cmp value x
13. y ∈ left
14. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (y = x ∈ E) ∨ (((value = y ∈ E) ∨ y ∈ left ∨ y ∈ right) ∧ (¬((cmp x y) = 0 ∈ ℤ)))

3
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. y : E
12. 0 < cmp value x
13. (value = y ∈ E) ∨ y ∈ left ∨ y ∈ right
14. ¬((cmp x y) = 0 ∈ ℤ)
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (value = y ∈ E) ∨ y ∈ left ∨ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ)))

4
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. y : E
13. cmp value x < 0
14. value = y ∈ E
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (y = x ∈ E) ∨ (((value = y ∈ E) ∨ y ∈ left ∨ y ∈ right) ∧ (¬((cmp x y) = 0 ∈ ℤ)))

5
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. y : E
13. cmp value x < 0
14. y ∈ right
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (y = x ∈ E) ∨ (((value = y ∈ E) ∨ y ∈ left ∨ y ∈ right) ∧ (¬((cmp x y) = 0 ∈ ℤ)))

6
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. y : E
13. cmp value x < 0
14. (value = y ∈ E) ∨ y ∈ left ∨ y ∈ right
15. ¬((cmp x y) = 0 ∈ ℤ)
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
17. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (value = y ∈ E) ∨ ((y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ)))) ∨ y ∈ right

7
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. y : E
14. y ∈ left
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (y = x ∈ E) ∨ (((value = y ∈ E) ∨ y ∈ left ∨ y ∈ right) ∧ (¬((cmp x y) = 0 ∈ ℤ)))

8
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. y : E
14. y ∈ right
15. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))

⊢ (y = x ∈ E) ∨ (((value = y ∈ E) ∨ y ∈ left ∨ y ∈ right) ∧ (¬((cmp x y) = 0 ∈ ℤ)))

9
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. y : E
14. (value = y ∈ E) ∨ y ∈ left ∨ y ∈ right
15. ¬((cmp x y) = 0 ∈ ℤ)
16. ∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))
17. ∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))
⊢ (x = y ∈ E) ∨ y ∈ left ∨ y ∈ right

Latex:

Latex:
1. [E] : Type 2. cmp : comparison(E) 3. x : E \mvdash{} \mforall{}left:bs\_tree(E). \mforall{}value:E. \mforall{}right:bs\_tree(E). ((bs\_tree\_ordered(E;cmp;left) {}\mRightarrow{} (\mforall{}y:E. (y \mmember{} bs\_tree\_insert(cmp;x;left) \mLeftarrow{}{}\mRightarrow{} (y = x) \mvee{} (y \mmember{} left \mwedge{} (\mneg{}((cmp x y) = 0)))))) {}\mRightarrow{} (bs\_tree\_ordered(E;cmp;right) {}\mRightarrow{} (\mforall{}y:E. (y \mmember{} bs\_tree\_insert(cmp;x;right) \mLeftarrow{}{}\mRightarrow{} (y = x) \mvee{} (y \mmember{} right \mwedge{} (\mneg{}((cmp x y) = 0)))))) {}\mRightarrow{} bs\_tree\_ordered(E;cmp;bst\_node(left;value;right)) {}\mRightarrow{} (\mforall{}y:E (y \mmember{} bs\_tree\_insert(cmp;x;bst\_node(left;value;right)) \mLeftarrow{}{}\mRightarrow{} (y = x) \mvee{} (y \mmember{} bst\_node(left;value;right) \mwedge{} (\mneg{}((cmp x y) = 0)))))) By Latex: ((Intros THEN RepUR ``bs\_tree\_ordered`` -2 THEN Fold `bs\_tree\_ordered` (-2)) THEN (RepUR ``bs\_tree\_insert`` 0 THEN Fold `bs\_tree\_insert` 0) THEN (CallByValueReduce 0 THENA Auto) THEN Repeat (AutoSplit) THEN RepUR ``member\_bs\_tree`` 0 THEN Fold `member\_bs\_tree` 0 THEN (RWW "7 8" 0 THENA Auto) THEN Auto THEN SplitOrHyps THEN Auto) Home Index