---

Step * 2 2 1 of Lemma remove-nat-missing-prop

.....assertion..... 
1. m : ℤ@i
2. [%18] : (-1) ≤ m@i
3. s1 : ℕ List@i
4. [%17] : l-ordered(ℕ;x,y.x < y;s1) ∧ (∀x∈s1.x < m)@i
5. ¬(s1 = [] ∈ (ℕ List))
6. x : ℕ@i
7. y : ℕ@i
8. y = m ∈ ℤ
9. last(s1) ≠ m - 1
⊢ s1 ∈ {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m - 1)} 
BY
{ (MemTypeCD THEN Auto THEN RepeatFor 2 (ParallelOp 5) THEN (Decide ⌜s1[i] = (m - 1) ∈ ℕ⌝⋅ THENA Auto)) }

1
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. l-ordered(ℕ;x,y.x < y;s1)@i
5. ∀i:ℕ||s1||. s1[i] < m@i
6. ¬(s1 = [] ∈ (ℕ List))
7. x : ℕ@i
8. y : ℕ@i
9. y = m ∈ ℤ
10. last(s1) ≠ m - 1
11. l-ordered(ℕ;x,y.x < y;s1)
12. i : ℕ||s1||@i
13. s1[i] < m
14. s1[i] = (m - 1) ∈ ℕ
⊢ s1[i] < m - 1

2
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. l-ordered(ℕ;x,y.x < y;s1)@i
5. ∀i:ℕ||s1||. s1[i] < m@i
6. ¬(s1 = [] ∈ (ℕ List))
7. x : ℕ@i
8. y : ℕ@i
9. y = m ∈ ℤ
10. last(s1) ≠ m - 1
11. l-ordered(ℕ;x,y.x < y;s1)
12. i : ℕ||s1||@i
13. s1[i] < m
14. ¬(s1[i] = (m - 1) ∈ ℕ)
⊢ s1[i] < m - 1

---

Latex:

---

Latex:
.....assertion..... 
1.  m  :  \mBbbZ{}@i
2.  [\%18]  :  (-1)  \mleq{}  m@i
3.  s1  :  \mBbbN{}  List@i
4.  [\%17]  :  l-ordered(\mBbbN{};x,y.x  <  y;s1)  \mwedge{}  (\mforall{}x\mmember{}s1.x  <  m)@i
5.  \mneg{}(s1  =  [])
6.  x  :  \mBbbN{}@i
7.  y  :  \mBbbN{}@i
8.  y  =  m
9.  last(s1)  \mneq{}  m  -  1
\mvdash{}  s1  \mmember{}  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m  -  1)\} 


By

---

Latex:
(MemTypeCD  THEN  Auto  THEN  RepeatFor  2  (ParallelOp  5)  THEN  (Decide  \mkleeneopen{}s1[i]  =  (m  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index