---

Step * 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 ∈ ℤ
⊢ eval x = last(s1) in
  if (x =z m - 1) then eval n = select-last-in-nat-missing(x;s1) in <n, filter(λx.x <z n;s1)> else <m - 1, s1> fi  ∈ m:{\000Cm:ℤ| (-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
BY
{ ((CallByValueReduce 0 THENA ProveHasValue) THEN AutoSplit) }

1
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)} 

2
1. i : ℕ
2. m : ℤ
3. (-1) ≤ m
4. s1 : ℕ List
5. last(s1) ≠ m - 1
6. ¬(s1 = [] ∈ (ℕ List))
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
9. i = m ∈ ℤ
⊢ <m - 1, s1> ∈ m:{m:ℤ| (-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 

---

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
\mvdash{}  eval  x  =  last(s1)  in
    if  (x  =\msubz{}  m  -  1)  then  eval  n  =  select-last-in-nat-missing(x;s1)  in  <n,  filter(\mlambda{}x.x  <z  n;s1)>  else  <\000Cm  -  1,  s1>  fi    \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)\} 


By

---

Latex:
((CallByValueReduce  0  THENA  ProveHasValue)  THEN  AutoSplit)

---

Home Index