Proof of Nuprl Lemma : member-insert-combine2

Step * of Lemma member-insert-combine2

∀T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x,z:T. ∀v:T List.
  ((z ∈ insert-combine(cmp;f;x;v))
  ⇐⇒ (∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
      ∨ (∃l,l':T List
          ∃a:T
           (((l @ [a / l']) = v ∈ (T List))
           ∧ (∀y∈l.cmp x y < 0)

           ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
BY

{ (Auto THEN MoveToConcl (-1) THEN ListInd (-1) THEN Reduce 0 THEN Auto THEN Try (DProdsAndUnions) THEN SpList (-1)) }

1
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. z = x ∈ T
⊢ (∃l:T List. (l @ [z] ≤ [] ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = [] ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)

     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈[].cmp x y < 0))

2
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. v : T List
8. (z ∈ insert-combine(cmp;f;x;v))
⇒ ((∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
   ∨ (∃l,l':T List
       ∃a:T
        (((l @ [a / l']) = v ∈ (T List))
        ∧ (∀y∈l.cmp x y < 0)

        ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

   ∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
9. (z ∈ eval tst = cmp x u in
        if (tst =_z 0) then [f x u / v]
        if 0 <z tst then [x; [u / v]]
        else [u / insert-combine(cmp;f;x;v)]
        fi )
⊢ (∃l:T List. (l @ [z] ≤ [u / v] ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = [u / v] ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)

     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈[u / v].cmp x y < 0))

3
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. l : T List
7. l @ [z] ≤ []
8. (∀y∈l.cmp x y < 0)
9. cmp x z < 0
⊢ (z ∈ insert-combine(cmp;f;x;[]))

4
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. l : T List
7. l' : T List
8. a : T
9. (l @ [a / l']) = [] ∈ (T List)
10. (∀y∈l.cmp x y < 0)
11. 0 < cmp x a
12. (z = x ∈ T) ∨ (z = a ∈ T) ∨ (z ∈ l')
⊢ (z ∈ insert-combine(cmp;f;x;[]))

5
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. l : T List
7. l' : T List
8. a : T
9. (l @ [a / l']) = [] ∈ (T List)
10. (∀y∈l.cmp x y < 0)
11. (cmp x a) = 0 ∈ ℤ
12. (z = (f x a) ∈ T) ∨ (z ∈ l')
⊢ (z ∈ insert-combine(cmp;f;x;[]))

6
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. z = x ∈ T
7. True
⊢ (z ∈ insert-combine(cmp;f;x;[]))

7
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. v : T List
8. ((∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = v ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)

     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
⇒ (z ∈ insert-combine(cmp;f;x;v))
9. l : T List
10. l @ [z] ≤ [u / v]
11. (∀y∈l.cmp x y < 0)
12. cmp x z < 0
⊢ (z ∈ insert-combine(cmp;f;x;[u / v]))

8
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. v : T List
8. ((∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = v ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)

     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
⇒ (z ∈ insert-combine(cmp;f;x;v))
9. l : T List
10. l' : T List
11. a : T
12. (l @ [a / l']) = [u / v] ∈ (T List)
13. (∀y∈l.cmp x y < 0)
14. 0 < cmp x a
15. (z = x ∈ T) ∨ (z = a ∈ T) ∨ (z ∈ l')
⊢ (z ∈ insert-combine(cmp;f;x;[u / v]))

9
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. v : T List
8. ((∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = v ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)

     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
⇒ (z ∈ insert-combine(cmp;f;x;v))
9. l : T List
10. l' : T List
11. a : T
12. (l @ [a / l']) = [u / v] ∈ (T List)
13. (∀y∈l.cmp x y < 0)
14. (cmp x a) = 0 ∈ ℤ
15. (z = (f x a) ∈ T) ∨ (z ∈ l')
⊢ (z ∈ insert-combine(cmp;f;x;[u / v]))

10
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. v : T List
8. ((∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
    ∃a:T
     (((l @ [a / l']) = v ∈ (T List))
     ∧ (∀y∈l.cmp x y < 0)

     ∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))

∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
⇒ (z ∈ insert-combine(cmp;f;x;v))
9. z = x ∈ T
10. cmp x u < 0 ∧ (∀y∈v.cmp x y < 0)
⊢ (z ∈ insert-combine(cmp;f;x;[u / v]))

Latex:

Latex:
\mforall{}T:Type. \mforall{}cmp:comparison(T). \mforall{}f:T {}\mrightarrow{} T {}\mrightarrow{} T. \mforall{}x,z:T. \mforall{}v:T List. ((z \mmember{} insert-combine(cmp;f;x;v)) \mLeftarrow{}{}\mRightarrow{} (\mexists{}l:T List. (l @ [z] \mleq{} v \mwedge{} (\mforall{}y\mmember{}l.cmp x y < 0) \mwedge{} cmp x z < 0)) \mvee{} (\mexists{}l,l':T List \mexists{}a:T (((l @ [a / l']) = v) \mwedge{} (\mforall{}y\mmember{}l.cmp x y < 0) \mwedge{} ((0 < cmp x a \mwedge{} (z \mmember{} [x; [a / l']])) \mvee{} (((cmp x a) = 0) \mwedge{} (z \mmember{} [f x a / l']))))) \mvee{} ((z = x) \mwedge{} (\mforall{}y\mmember{}v.cmp x y < 0))) By Latex: (Auto THEN MoveToConcl (-1) THEN ListInd (-1) THEN Reduce 0 THEN Auto THEN Try (DProdsAndUnions) THEN SpList (-1)) Home Index