---

Step * of Lemma merge-int-comm

∀[T:Type]
  ∀[as,bs:T List].  merge-int(as;bs) = merge-int(bs;as) ∈ (T List) supposing sorted(as) ∧ sorted(bs) supposing T ⊆r ℤ
BY
{ (InductionOnList
   THEN Unfold `merge-int` 0
   THEN Reduce 0
   THEN Try (Fold `merge-int` 0)
   THEN Auto
   THEN ∀h:hyp. (FLemma `sorted-cons` [h] THENA Auto) 
   THEN ThinTrivial) }

1
1. T : Type
2. T ⊆r ℤ
3. bs : T List
4. sorted([])
5. sorted(bs)
⊢ merge-int([];bs) = bs ∈ (T List)

2
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. bs : T List
7. sorted([u / v])
8. sorted(bs)
9. sorted(v)
⊢ merge-int([u / v];bs) = insert-int(u;merge-int(bs;v)) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[as,bs:T  List].    merge-int(as;bs)  =  merge-int(bs;as)  supposing  sorted(as)  \mwedge{}  sorted(bs) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(InductionOnList
  THEN  Unfold  `merge-int`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `merge-int`  0)
  THEN  Auto
  THEN  \mforall{}h:hyp.  (FLemma  `sorted-cons`  [h]  THENA  Auto) 
  THEN  ThinTrivial)

---

Home Index