---

Step * of Lemma remove-nat-missing-prop

∀s:nat-missing-type(). ∀x,y:ℕ.
  (↑member-nat-missing(x;remove-nat-missing(y;s)) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;s)))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``remove-nat-missing`` 0 THEN DVar `s' THEN Reduce 0 THEN RepeatFor 2 (AutoSplit)) }

1
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. y = m ∈ ℤ
6. s1 = [] ∈ (ℕ List)
⊢ ↑member-nat-missing(x;<m - 1, []>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;<m, s1>))

2
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>))

3
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. y ≠ m
6. m < y
⊢ ↑member-nat-missing(x;<m, s1>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;<m, s1>))

4
1. m : {m:ℤ| (-1) ≤ m} @i
2. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} @i
3. x : ℕ@i
4. y : ℕ@i
5. ¬m < y
6. y ≠ m
⊢ ↑member-nat-missing(x;<m, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;y;s1)>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-\000Cnat-missing(x;<m, s1>))

---

Latex:


\mforall{}s:nat-missing-type().  \mforall{}x,y:\mBbbN{}.
    (\muparrow{}member-nat-missing(x;remove-nat-missing(y;s))  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}member-nat-missing(x;s)))


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``remove-nat-missing``  0
  THEN  DVar  `s'
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index