---

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

.....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)))
BY
{ (RepUR ``union-nat-missing-pos`` 0
   THEN AutoSplit
   THEN Try ((RWO "add-nat-missing-prop" 0 THENA Auto))
   THEN (RWO "assert-member-nat-missing" 0 THENA (Auto THEN GenConclAtAddr [2;1] THEN Auto))
   THEN (All(RWO "assert-in-missing-nat-iff") THENA Auto)
   THEN Auto
   THEN DProdsAndUnions
   THEN Auto
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN D (-1)
   THEN Assert ⌈x = 0 ∈ ℕ⌉⋅
   THEN Auto) }

---

Latex:


.....basecase..... 
1.  s1  :  nat-missing-type()@i
2.  missing  :  \{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  @i
3.  x  :  \mBbbN{}@i
\mvdash{}  \muparrow{}member-nat-missing(x;union-nat-missing-pos(s1;0;missing))
\mLeftarrow{}{}\mRightarrow{}  (\muparrow{}member-nat-missing(x;s1))  \mvee{}  ((x  \mleq{}  0)  \mwedge{}  (\mneg{}(x  \mmember{}  missing)))


By

(RepUR  ``union-nat-missing-pos``  0
  THEN  AutoSplit
  THEN  Try  ((RWO  "add-nat-missing-prop"  0  THENA  Auto))
  THEN  (RWO  "assert-member-nat-missing"  0  THENA  (Auto  THEN  GenConclAtAddr  [2;1]  THEN  Auto))
  THEN  (All(RWO  "assert-in-missing-nat-iff")  THENA  Auto)
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  Auto
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  D  (-1)
  THEN  Assert  \mkleeneopen{}x  =  0\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index