---

Step * 1 2 of Lemma remove-nat-missing_wf


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)} 
BY
{ ((MemCD THEN Auto)
   THEN MemTypeCD
   THEN Auto
   THEN skip{((RWO "eqff_to_assert" (-2) THENA Auto) THEN (RW assert_pushdownC (-2) THENA Auto))}) }

1
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 ∈ ℤ
10. l-ordered(ℕ;x,y.x < y;s1)
⊢ (∀x∈s1.x < m - 1)

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}
2.  m  :  \mBbbZ{}
3.  (-1)  \mleq{}  m
4.  s1  :  \mBbbN{}  List
5.  last(s1)  \mneq{}  m  -  1
6.  \mneg{}(s1  =  [])
7.  l-ordered(\mBbbN{};x,y.x  <  y;s1)
8.  (\mforall{}x\mmember{}s1.x  <  m)
9.  i  =  m
\mvdash{}  <m  -  1,  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)\} 


By

---

Latex:
((MemCD  THEN  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  skip\{((RWO  "eqff\_to\_assert"  (-2)  THENA  Auto)  THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto))\})

---

Home Index