---

Step * 2 of Lemma remove-nat-missing_wf


1. i : ℕ
2. m : ℤ
3. ¬m < i
4. i ≠ m
5. (-1) ≤ m
6. s1 : ℕ List
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
⊢ <m, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1)> ∈ m:{m:ℤ| (-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x <\000C y;L) ∧ (∀x∈L.x < m)} 
BY
{ (MemCD THEN Auto THEN MemTypeCD THEN Auto) }

1
1. i : ℕ
2. m : ℤ
3. ¬m < i
4. i ≠ m
5. (-1) ≤ m
6. s1 : ℕ List
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
⊢ l-ordered(ℕ;x,y.x < y;insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1))

2
1. i : ℕ
2. m : ℤ
3. ¬m < i
4. i ≠ m
5. (-1) ≤ m
6. s1 : ℕ List
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
9. l-ordered(ℕ;x,y.x < y;insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1))
⊢ (∀x∈insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1).x < m)

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}
2.  m  :  \mBbbZ{}
3.  \mneg{}m  <  i
4.  i  \mneq{}  m
5.  (-1)  \mleq{}  m
6.  s1  :  \mBbbN{}  List
7.  l-ordered(\mBbbN{};x,y.x  <  y;s1)
8.  (\mforall{}x\mmember{}s1.x  <  m)
\mvdash{}  <m,  insert-combine(int-minus-comparison-inc(\mlambda{}x.x);\mlambda{}i,a.  i;i;s1)>  \mmember{}  m:\{m:\mBbbZ{}|  (-1)  \mleq{}  m\}    \mtimes{}  \{L:\mBbbN{}  List|\000C  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\} 


By

---

Latex:
(MemCD  THEN  Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index