---

Step * of Lemma merge-int-1-1

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

1
1. T : Type
2. T ⊆r ℤ
3. u : T
4. v : T List
5. ∀[as,bs:T List].
     (as = bs ∈ (T List)) supposing ((merge-int(as;v) = merge-int(bs;v) ∈ (T List)) and sorted(bs) and sorted(as))
6. as : T List
7. bs : T List
8. sorted(as)
9. sorted(bs)
10. insert-int(u;merge-int(as;v)) = insert-int(u;merge-int(bs;v)) ∈ (T List)
⊢ as = bs ∈ (T List)

---

Latex:

---

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


By

---

Latex:
(InductionOnList  THEN  Unfold  `merge-int`  0  THEN  Reduce  0  THEN  Try  (Fold  `merge-int`  0)  THEN  Auto)

---

Home Index