---

Step * 2 1 1 1 of Lemma merge-int-comm


1. T : Type
2. T ⊆r ℤ
3. u : T
4. v : T List
5. ∀[bs:T List]. merge-int(v;bs) = merge-int(bs;v) ∈ (T List) supposing sorted(v) ∧ sorted(bs)
6. sorted(v) ∧ (∀z∈v.u ≤ z)
7. sorted(v)
⊢ [u / v] = insert-int(u;v) ∈ (T List)
BY
{ (DVar `v' THEN Reduce 0 THEN Try ((Fold `member` 0 THEN Auto))) }

1
1. T : Type
2. T ⊆r ℤ
3. u : T
4. u1 : T
5. v : T List
6. ∀[bs:T List]. merge-int([u1 / v];bs) = merge-int(bs;[u1 / v]) ∈ (T List) supposing sorted([u1 / v]) ∧ sorted(bs)
7. sorted([u1 / v]) ∧ (∀z∈[u1 / v].u ≤ z)
8. sorted([u1 / v])
⊢ [u; [u1 / v]] = insert-int(u;[u1 / v]) ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  \mBbbZ{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[bs:T  List].  merge-int(v;bs)  =  merge-int(bs;v)  supposing  sorted(v)  \mwedge{}  sorted(bs)
6.  sorted(v)  \mwedge{}  (\mforall{}z\mmember{}v.u  \mleq{}  z)
7.  sorted(v)
\mvdash{}  [u  /  v]  =  insert-int(u;v)


By

---

Latex:
(DVar  `v'  THEN  Reduce  0  THEN  Try  ((Fold  `member`  0  THEN  Auto)))

---

Home Index