---

Step * of Lemma member-merge

∀[T:Type]. ∀bs,as:T List. ∀x:T.  ((x ∈ merge(as;bs)) ⇐⇒ (x ∈ as) ∨ (x ∈ bs)) supposing T ⊆r ℤ
BY
{ (((((InductionOnList THEN Unfold `merge` 0 THEN Reduce 0 THEN Try (Fold `merge` 0) THEN RWW "nil_member" 0)
      THENA Auto
      )
     THEN RWW "member-s-insert" 0
     )
    THENA Auto
    )
   THEN RWW "cons_member" 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto) }

1
1. [T] : Type
2. T ⊆r ℤ
3. u : T@i
4. v : T List@i
5. ∀as:T List. ∀x:T.  ((x ∈ merge(as;v)) ⇐⇒ (x ∈ as) ∨ (x ∈ v))@i
6. as : T List@i
7. x : T@i
8. (x ∈ merge(as;v))@i
⊢ (x ∈ as) ∨ (x = u ∈ T) ∨ (x ∈ v)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}bs,as:T  List.  \mforall{}x:T.    ((x  \mmember{}  merge(as;bs))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  as)  \mvee{}  (x  \mmember{}  bs))  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(((((InductionOnList
          THEN  Unfold  `merge`  0
          THEN  Reduce  0
          THEN  Try  (Fold  `merge`  0)
          THEN  RWW  "nil\_member"  0)
        THENA  Auto
        )
      THEN  RWW  "member-s-insert"  0
      )
    THENA  Auto
    )
  THEN  RWW  "cons\_member"  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index