---

Step * of Lemma remove-nat-missing_wf

∀[i:ℕ]. ∀[s:nat-missing-type()].  (remove-nat-missing(i;s) ∈ nat-missing-type())
BY
{ ((UnivCD THENA Auto)
   THEN All (RepUR ``nat-missing-type remove-nat-missing``)
   THEN DProdsAndUnions
   THEN DVarSets
   THEN Reduce 0
   THEN RepeatFor 2 (AutoSplit)) }

1
1. i : ℕ
2. m : ℤ
3. (-1) ≤ m
4. s1 : ℕ List
5. ¬(s1 = [] ∈ (ℕ List))
6. l-ordered(ℕ;x,y.x < y;s1)
7. (∀x∈s1.x < m)
8. i = m ∈ ℤ
⊢ 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 <m - 1, s1> fi  ∈ m:{\000Cm:ℤ| (-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 

2
1. i : ℕ
2. m : ℤ
3. ¬m < i
4. i ≠ m
5. (-1) ≤ m
6. s1 : ℕ List
7. l-ordered(ℕ;x,y.x < y;s1)
8. (∀x∈s1.x < m)
⊢ <m, insert-combine(int-minus-comparison-inc(λx.x);λi,a. i;i;s1)> ∈ m:{m:ℤ| (-1) ≤ m}  × {L:ℕ List| l-ordered(ℕ;x,y.x <\000C y;L) ∧ (∀x∈L.x < m)} 

---

Latex:


\mforall{}[i:\mBbbN{}].  \mforall{}[s:nat-missing-type()].    (remove-nat-missing(i;s)  \mmember{}  nat-missing-type())


By

((UnivCD  THENA  Auto)
  THEN  All  (RepUR  ``nat-missing-type  remove-nat-missing``)
  THEN  DProdsAndUnions
  THEN  DVarSets
  THEN  Reduce  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index