---

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


1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. ¬(s1 = [] ∈ (ℕ List))
4. x : ℕ@i
5. y : ℕ@i
6. y = m ∈ ℤ
⊢ ↑member-nat-missing(x;eval x = last(s1) in
                        if (x =z m - 1) then eval n = select-last-in-nat-missing(x;s1) in <n, filter(λx.x <z n;s1)> else\000C <m - 1, s1> fi )
⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;<m, s1>))
BY
{ (DVarSets THEN (CallByValueReduce 0 THENA ProveHasValue) THEN SimpleSplit) }

1
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) ∈ ℤ
⊢ ↑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>))

2
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
⊢ ↑member-nat-missing(x;<m - 1, s1>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;<m, s1>))

---

Latex:



1.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\}  @i
2.  s1  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\}  @i
3.  \mneg{}(s1  =  [])
4.  x  :  \mBbbN{}@i
5.  y  :  \mBbbN{}@i
6.  y  =  m
\mvdash{}  \muparrow{}member-nat-missing(x;eval  x  =  last(s1)  in
                                                if  (x  =\msubz{}  m  -  1)
                                                then  eval  n  =  select-last-in-nat-missing(x;s1)  in
                                                          <n,  filter(\mlambda{}x.x  <z  n;s1)>
                                                else  <m  -  1,  s1>
                                                fi  )
\mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}member-nat-missing(x;<m,  s1>))


By

(DVarSets  THEN  (CallByValueReduce  0  THENA  ProveHasValue)  THEN  SimpleSplit)

---

Home Index