---

Step * of Lemma member-insert-combine

∀T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x,z:T. ∀v:T List.
  ((z ∈ insert-combine(cmp;f;x;v)) ⇒ ((z ∈ v) ∨ (z = x ∈ T) ∨ (∃y∈v. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T))))
BY
{ (InductionOnList THEN RepUR ``insert-combine`` 0 THEN Try (Fold `insert-combine` 0)) }

1
1. T : Type
2. cmp : comparison(T)
3. f : T ⟶ T ⟶ T
4. x : T
5. z : T
⊢ (z ∈ [x]) ⇒ ((z ∈ []) ∨ (z = x ∈ T) ∨ (∃y∈[]. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T)))

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)) ⇒ ((z ∈ v) ∨ (z = x ∈ T) ∨ (∃y∈v. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T)))
⊢ (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 )
⇒ ((z ∈ [u / v]) ∨ (z = x ∈ T) ∨ (∃y∈[u / v]. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T)))

---

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))  {}\mRightarrow{}  ((z  \mmember{}  v)  \mvee{}  (z  =  x)  \mvee{}  (\mexists{}y\mmember{}v.  ((cmp  x  y)  =  0)  \mwedge{}  (z  =  (f  x  y)))))


By

---

Latex:
(InductionOnList  THEN  RepUR  ``insert-combine``  0  THEN  Try  (Fold  `insert-combine`  0))

---

Home Index