---

Step * 1 of Lemma sort-int-trivial


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index