---

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


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) ∈ ℤ
10. <select-last-in-nat-missing(last(s1);s1), filter(λx.x <z select-last-in-nat-missing(last(s1);s1);s1)>
    ∈ nat-missing-type()
⊢ ↑member-nat-missing(x;eval n = select-last-in-nat-missing(last(s1);s1) in <n, filter(λx.x <z n;s1)>) ⇐⇒ (¬(x = y ∈ ℕ)\000C) ∧ (↑member-nat-missing(x;<m, s1>))
BY
{ ((CallByValueReduce 0 THENA ProveHasValue)
   THEN (RWO "assert-member-nat-missing" 0 THENA (Reduce 0 THEN Auto))
   THEN Reduce 0
   THEN (GenConclTerm ⌜select-last-in-nat-missing(last(s1);s1)⌝⋅ THENA Auto)
   THEN D -2
   THEN (Unhide THENA Auto)
   THEN Thin (-1)
   THEN Auto) }

1
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. l-ordered(ℕ;x,y.x < y;s1)@i
5. (∀x∈s1.x < m)@i
6. ¬(s1 = [] ∈ (ℕ List))
7. x : ℕ@i
8. y : ℕ@i
9. y = m ∈ ℤ
10. last(s1) = (m - 1) ∈ ℤ
11. <select-last-in-nat-missing(last(s1);s1), filter(λx.x <z select-last-in-nat-missing(last(s1);s1);s1)>
    ∈ nat-missing-type()
12. v : ℤ@i
13. (-1) ≤ v@i
14. v ≤ last(s1)@i
15. (0 ≤ v) ⇒ (¬(v ∈ s1))@i
16. ∀y:ℕ. ((¬(y ∈ s1)) ⇒ y < last(s1) ⇒ (y ≤ v))@i
17. ∀y:ℕ. (y < last(s1) ⇒ v < y ⇒ (y ∈ s1))@i
18. x ≤ v@i
19. ¬(x ∈ filter(λx.x <z v;s1))@i
⊢ ¬(x ∈ s1)

2
1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. l-ordered(ℕ;x,y.x < y;s1)@i
5. (∀x∈s1.x < m)@i
6. ¬(s1 = [] ∈ (ℕ List))
7. x : ℕ@i
8. y : ℕ@i
9. y = m ∈ ℤ
10. last(s1) = (m - 1) ∈ ℤ
11. <select-last-in-nat-missing(last(s1);s1), filter(λx.x <z select-last-in-nat-missing(last(s1);s1);s1)>
    ∈ nat-missing-type()
12. v : ℤ@i
13. (-1) ≤ v@i
14. v ≤ last(s1)@i
15. (0 ≤ v) ⇒ (¬(v ∈ s1))@i
16. ∀y:ℕ. ((¬(y ∈ s1)) ⇒ y < last(s1) ⇒ (y ≤ v))@i
17. ∀y:ℕ. (y < last(s1) ⇒ v < y ⇒ (y ∈ s1))@i
18. ¬(x = y ∈ ℕ)@i
19. x ≤ m@i
20. ¬(x ∈ s1)@i
⊢ x ≤ v

---

Latex:

---

Latex:

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)
10.  <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()
\mvdash{}  \muparrow{}member-nat-missing(x;eval  n  =  select-last-in-nat-missing(last(s1);s1)  in
                                                <n,  filter(\mlambda{}x.x  <z  n;s1)>)
\mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}member-nat-missing(x;<m,  s1>))


By

---

Latex:
((CallByValueReduce  0  THENA  ProveHasValue)
  THEN  (RWO  "assert-member-nat-missing"  0  THENA  (Reduce  0  THEN  Auto))
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}select-last-in-nat-missing(last(s1);s1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  (Unhide  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index