---

Step * 8 3 of Lemma member-insert-combine2


1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. ¬0 < cmp x u
8. cmp x u ≠ 0
9. v : T List
10. ((∃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))
11. l : T List
12. l' : T List
13. a : T
14. (l @ [a / l']) = [u / v] ∈ (T List)
15. (∀y∈l.cmp x y < 0)
16. 0 < cmp x a
17. (z = x ∈ T) ∨ (z = a ∈ T) ∨ (z ∈ l')
⊢ (z = u ∈ T) ∨ (z ∈ insert-combine(cmp;f;x;v))
BY
{ (DVar `l' THEN AllReduce THEN AutoSimpHyp Auto (-4) THEN SpList (-3)) }

1
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. ¬0 < cmp x u
8. cmp x u ≠ 0
9. v : T List
10. ((∃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))
11. l' : T List
12. a : T
13. a = u ∈ T
14. l' = v ∈ (T List)
15. True
16. 0 < cmp x a
17. (z = x ∈ T) ∨ (z = a ∈ T) ∨ (z ∈ l')
⊢ (z = u ∈ T) ∨ (z ∈ insert-combine(cmp;f;x;v))

2
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
6. u : T
7. ¬0 < cmp x u
8. cmp x u ≠ 0
9. v : T List
10. ((∃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))
11. u1 : T
12. v1 : T List
13. l' : T List
14. a : T
15. u1 = u ∈ T
16. (v1 @ [a / l']) = v ∈ (T List)
17. cmp x u1 < 0 ∧ (∀y∈v1.cmp x y < 0)
18. 0 < cmp x a
19. (z = x ∈ T) ∨ (z = a ∈ T) ∨ (z ∈ l')
⊢ (z = u ∈ T) ∨ (z ∈ insert-combine(cmp;f;x;v))

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  f  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  x  :  T
5.  z  :  T
6.  u  :  T
7.  \mneg{}0  <  cmp  x  u
8.  cmp  x  u  \mneq{}  0
9.  v  :  T  List
10.  ((\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)))
{}\mRightarrow{}  (z  \mmember{}  insert-combine(cmp;f;x;v))
11.  l  :  T  List
12.  l'  :  T  List
13.  a  :  T
14.  (l  @  [a  /  l'])  =  [u  /  v]
15.  (\mforall{}y\mmember{}l.cmp  x  y  <  0)
16.  0  <  cmp  x  a
17.  (z  =  x)  \mvee{}  (z  =  a)  \mvee{}  (z  \mmember{}  l')
\mvdash{}  (z  =  u)  \mvee{}  (z  \mmember{}  insert-combine(cmp;f;x;v))


By

---

Latex:
(DVar  `l'  THEN  AllReduce  THEN  AutoSimpHyp  Auto  (-4)  THEN  SpList  (-3))

---

Home Index