---

Step * of Lemma member-insert-no-combine

∀T:Type. ∀cmp:comparison(T). ∀x,z:T. ∀v:T List.  ((z ∈ insert-no-combine(cmp;x;v)) ⇐⇒ (z ∈ [x / v]))
BY
{ (InductionOnList THEN RepUR ``insert-no-combine`` 0 THEN Try (Fold `insert-no-combine` 0)) }

1
1. T : Type
2. cmp : comparison(T)
3. x : T
4. z : T
⊢ (z ∈ [x]) ⇐⇒ (z ∈ [x])

2
1. T : Type
2. cmp : comparison(T)
3. x : T
4. z : T
5. u : T
6. v : T List
7. (z ∈ insert-no-combine(cmp;x;v)) ⇐⇒ (z ∈ [x / v])
⊢ (z ∈ if 0 ≤z cmp x u then [x; [u / v]] else [u / insert-no-combine(cmp;x;v)] fi ) ⇐⇒ (z ∈ [x; [u / v]])

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}cmp:comparison(T).  \mforall{}x,z:T.  \mforall{}v:T  List.
    ((z  \mmember{}  insert-no-combine(cmp;x;v))  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  [x  /  v]))


By

---

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

---

Home Index