---

Step * of Lemma union-nat-missing-pos-prop

∀s1:nat-missing-type(). ∀max:ℕ. ∀missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} . ∀x:ℕ.
  (↑member-nat-missing(x;union-nat-missing-pos(s1;max;missing))
  ⇐⇒ (↑member-nat-missing(x;s1)) ∨ ((x ≤ max) ∧ (¬(x ∈ missing))))
BY
{ ((UnivCD THENA Auto) THEN NatInd (-3)) }

1
.....basecase..... 
1. s1 : nat-missing-type()@i
2. missing : {l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} @i
3. x : ℕ@i
⊢ ↑member-nat-missing(x;union-nat-missing-pos(s1;0;missing))
⇐⇒ (↑member-nat-missing(x;s1)) ∨ ((x ≤ 0) ∧ (¬(x ∈ missing)))

2
.....upcase..... 
1. s1 : nat-missing-type()@i
2. missing : {l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} @i
3. x : ℕ@i
4. max : ℤ@i
5. [%1] : 0 < max@i
6. ↑member-nat-missing(x;union-nat-missing-pos(s1;max - 1;missing))
⇐⇒ (↑member-nat-missing(x;s1)) ∨ ((x ≤ (max - 1)) ∧ (¬(x ∈ missing)))@i
⊢ ↑member-nat-missing(x;union-nat-missing-pos(s1;max;missing))
⇐⇒ (↑member-nat-missing(x;s1)) ∨ ((x ≤ max) ∧ (¬(x ∈ missing)))

---

Latex:

---

Latex:
\mforall{}s1:nat-missing-type().  \mforall{}max:\mBbbN{}.  \mforall{}missing:\{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  .  \mforall{}x:\mBbbN{}.
    (\muparrow{}member-nat-missing(x;union-nat-missing-pos(s1;max;missing))
    \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}member-nat-missing(x;s1))  \mvee{}  ((x  \mleq{}  max)  \mwedge{}  (\mneg{}(x  \mmember{}  missing))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  NatInd  (-3))

---

Home Index