---

Step * 1 1 of Lemma add-nat-missing-prop

.....wf..... 
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. x ≤ y
6. ¬↑in-missing(x;s1 @ [m + 1, y))
7. m < y
8. (x ∈ s1 @ [m + 1, y))@i
⊢ s1 @ [m + 1, y) ∈ {l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} 
BY
{ (DVarSets
   THEN (MemTypeCD THEN Auto)
   THEN (RW ListC 0 THEN Auto)
   THEN Try ((RW ListC 0 THEN Auto))
   THEN (RW ListC (-1) THENA Auto)
   THEN (All(RWO "l_all_iff") THEN Auto)
   THEN OnSomeHyp(\i.InstHyp [⌈x1⌉] i THEN CpltAuto)⋅) }

---

Latex:


.....wf..... 
1.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\}  @i
2.  s1  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\}  @i
3.  x  :  \mBbbN{}@i
4.  y  :  \mBbbN{}@i
5.  x  \mleq{}  y
6.  \mneg{}\muparrow{}in-missing(x;s1  @  [m  +  1,  y))
7.  m  <  y
8.  (x  \mmember{}  s1  @  [m  +  1,  y))@i
\mvdash{}  s1  @  [m  +  1,  y)  \mmember{}  \{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\} 


By

(DVarSets
  THEN  (MemTypeCD  THEN  Auto)
  THEN  (RW  ListC  0  THEN  Auto)
  THEN  Try  ((RW  ListC  0  THEN  Auto))
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  (All(RWO  "l\_all\_iff")  THEN  Auto)
  THEN  OnSomeHyp(\mbackslash{}i.InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  i  THEN  CpltAuto)\mcdot{})

---

Home Index