---

Step * of Lemma member-merge-int

∀bs,as:ℤ List. ∀x:ℤ.  ((x ∈ merge-int(as;bs)) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
BY
{ (Unfold `merge-int` 0 THEN InductionOnList THEN Reduce 0) }

1
∀as:ℤ List. ∀x:ℤ.  ((x ∈ as) ⇐⇒ (x ∈ as) ∨ (x ∈ []))

2
1. u : ℤ
2. v : ℤ List
3. ∀as:ℤ List. ∀x:ℤ.  ((x ∈ reduce(λb,l. insert-int(b;l);as;v)) ⇐⇒ (x ∈ as) ∨ (x ∈ v))
⊢ ∀as:ℤ List. ∀x:ℤ.  ((x ∈ insert-int(u;reduce(λb,l. insert-int(b;l);as;v))) ⇐⇒ (x ∈ as) ∨ (x ∈ [u / v]))

---

Latex:

---

Latex:
\mforall{}bs,as:\mBbbZ{}  List.  \mforall{}x:\mBbbZ{}.    ((x  \mmember{}  merge-int(as;bs))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  as)  \mvee{}  (x  \mmember{}  bs))


By

---

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

---

Home Index