---

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

.....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)))
BY
{ (RepUR ``union-nat-missing-pos`` 0
   THEN (RWO "primrec-unroll-1" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌈(max + 1) - 1 ~ (max - 1) + 1⌉ 0⋅ THENA Auto)
   THEN Fold `union-nat-missing-pos` 0
   THEN (Subst ⌈(max - 1) + 1 ~ max⌉ 0⋅ THENA Auto)
   THEN AutoSplit
   THEN (All(RWO "assert-in-missing-nat-iff") THENA Auto)
   THEN Try ((RWO "add-nat-missing-prop" 0 THENA Auto))
   THEN Try ((RWO "-1" 0 THENA Auto))
   THEN Try ((RWO "-2" 0 THENA Auto))
   THEN (RWO "assert-member-nat-missing" 0 THENA Auto)
   THEN Auto
   THEN DProdsAndUnions
   THEN Auto
   THEN Try (Complete (((OrRight THEN Auto) THEN (Decide ⌈x = max ∈ ℤ⌉⋅ THEN Auto) THEN D (-2) THEN Auto)))
   THEN (Decide ⌈x = max ∈ ℤ⌉⋅ THEN Auto)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN RepeatFor 2 ((OrRight THEN Auto))) }

---

Latex:


.....upcase..... 
1.  s1  :  nat-missing-type()@i
2.  missing  :  \{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  @i
3.  x  :  \mBbbN{}@i
4.  max  :  \mBbbZ{}@i
5.  \mbackslash{}\mbackslash{}\%1  :  0  <  max@i
6.  \muparrow{}member-nat-missing(x;union-nat-missing-pos(s1;max  -  1;missing))
\mLeftarrow{}{}\mRightarrow{}  (\muparrow{}member-nat-missing(x;s1))  \mvee{}  ((x  \mleq{}  (max  -  1))  \mwedge{}  (\mneg{}(x  \mmember{}  missing)))@i
\mvdash{}  \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

(RepUR  ``union-nat-missing-pos``  0
  THEN  (RWO  "primrec-unroll-1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}(max  +  1)  -  1  \msim{}  (max  -  1)  +  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Fold  `union-nat-missing-pos`  0
  THEN  (Subst  \mkleeneopen{}(max  -  1)  +  1  \msim{}  max\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  (All(RWO  "assert-in-missing-nat-iff")  THENA  Auto)
  THEN  Try  ((RWO  "add-nat-missing-prop"  0  THENA  Auto))
  THEN  Try  ((RWO  "-1"  0  THENA  Auto))
  THEN  Try  ((RWO  "-2"  0  THENA  Auto))
  THEN  (RWO  "assert-member-nat-missing"  0  THENA  Auto)
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  Auto
  THEN  Try  (Complete  (((OrRight  THEN  Auto)
                                            THEN  (Decide  \mkleeneopen{}x  =  max\mkleeneclose{}\mcdot{}  THEN  Auto)
                                            THEN  D  (-2)
                                            THEN  Auto)))
  THEN  (Decide  \mkleeneopen{}x  =  max\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  RepeatFor  2  ((OrRight  THEN  Auto)))

---

Home Index