---

Step * 1 1 of Lemma remove-nat-missing_wf


1. i : ℕ
2. m : ℤ
3. (-1) ≤ m
4. s1 : ℕ List
5. ¬(s1 = [] ∈ (ℕ List))
6. l-ordered(ℕ;x,y.x < y;s1)
7. (∀x∈s1.x < m)
8. i = m ∈ ℤ
9. last(s1) = (m - 1) ∈ ℤ
⊢ eval n = select-last-in-nat-missing(last(s1);s1) in
  <n, filter(λx.x <z n;s1)> ∈ m:{m:ℤ| (-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
BY
{ ((CallByValueReduce 0 THENA ProveHasValue)
   THEN MemCD
   THEN Auto
   THEN GenConclAtAddr [2;1;1;2]
   THEN DVarSets
   THEN MemTypeCD
   THEN Auto
   THEN Try (Complete ((BLemma `l-ordered-filter` THEN Auto)))
   THEN RWO "l_all_iff" 0
   THEN Auto
   THEN RW ListC (-1)
   THEN AllReduce
   THEN Auto
   THEN RW assert_pushdownC (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}
2.  m  :  \mBbbZ{}
3.  (-1)  \mleq{}  m
4.  s1  :  \mBbbN{}  List
5.  \mneg{}(s1  =  [])
6.  l-ordered(\mBbbN{};x,y.x  <  y;s1)
7.  (\mforall{}x\mmember{}s1.x  <  m)
8.  i  =  m
9.  last(s1)  =  (m  -  1)
\mvdash{}  eval  n  =  select-last-in-nat-missing(last(s1);s1)  in
    <n,  filter(\mlambda{}x.x  <z  n;s1)>  \mmember{}  m:\{m:\mBbbZ{}|  (-1)  \mleq{}  m\}    \mtimes{}  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m\000C)\} 


By

---

Latex:
((CallByValueReduce  0  THENA  ProveHasValue)
  THEN  MemCD
  THEN  Auto
  THEN  GenConclAtAddr  [2;1;1;2]
  THEN  DVarSets
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `l-ordered-filter`  THEN  Auto)))
  THEN  RWO  "l\_all\_iff"  0
  THEN  Auto
  THEN  RW  ListC  (-1)
  THEN  AllReduce
  THEN  Auto
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)

---

Home Index