---

Step * 2 1 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) ∈ ℤ
⊢ <select-last-in-nat-missing(last(s1);s1), filter(λx.x <z select-last-in-nat-missing(last(s1);s1);s1)>
  ∈ nat-missing-type()
BY
{ (Unfold `nat-missing-type` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. 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) ∈ ℤ
⊢ select-last-in-nat-missing(last(s1);s1) ∈ {m:ℤ| (-1) ≤ m} 

2
.....subterm..... T:t
2:n
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. 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) ∈ ℤ
⊢ filter(λx.x <z select-last-in-nat-missing(last(s1);s1);s1) ∈ {L:ℕ List| 
                                                                l-ordered(ℕ;x,y.x < y;L)
                                                                ∧ (∀x∈L.x < select-last-in-nat-missing(last(s1);s1))} 

3
.....eq aux..... 
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. 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) ∈ ℤ
10. m1 : {m:ℤ| (-1) ≤ m} 
⊢ {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m1)}  ∈ Type

---

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)  =  (m  -  1)
\mvdash{}  <select-last-in-nat-missing(last(s1);s1)
    ,  filter(\mlambda{}x.x  <z  select-last-in-nat-missing(last(s1);s1);s1)
    >  \mmember{}  nat-missing-type()


By

---

Latex:
(Unfold  `nat-missing-type`  0  THEN  MemCD)

---

Home Index