---

Step * of Lemma union-nat-missing-prop

∀s1,s2:nat-missing-type(). ∀x:ℕ.
  (↑member-nat-missing(x;union-nat-missing(s1;s2)) ⇐⇒ (↑member-nat-missing(x;s1)) ∨ (↑member-nat-missing(x;s2)))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``union-nat-missing`` 0 THEN D (-2) THEN Reduce 0 THEN AutoSplit) }

1
1. s1 : nat-missing-type()@i
2. m : {m:ℤ| (-1) ≤ m} @i
3. s3 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
4. x : ℕ@i
5. 0 ≤ m
⊢ ↑member-nat-missing(x;union-nat-missing-pos(s1;m;s3)) ⇐⇒ (↑member-nat-missing(x;s1)) ∨ (↑member-nat-missing(x;<m, s3>\000C))

2
1. s1 : nat-missing-type()@i
2. m : {m:ℤ| (-1) ≤ m} @i
3. ¬(0 ≤ m)
4. s3 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
5. x : ℕ@i
⊢ ↑member-nat-missing(x;s1) ⇐⇒ (↑member-nat-missing(x;s1)) ∨ (↑member-nat-missing(x;<m, s3>))

---

Latex:


\mforall{}s1,s2:nat-missing-type().  \mforall{}x:\mBbbN{}.
    (\muparrow{}member-nat-missing(x;union-nat-missing(s1;s2))
    \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}member-nat-missing(x;s1))  \mvee{}  (\muparrow{}member-nat-missing(x;s2)))


By

((UnivCD  THENA  Auto)  THEN  RepUR  ``union-nat-missing``  0  THEN  D  (-2)  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index