---

Step * of Lemma select-last-in-nat-missing_wf

∀[max:ℕ]. ∀[missing:{l:ℕ List| l-ordered(ℕ;x,y.x < y;l)} ].
  (select-last-in-nat-missing(max;missing) ∈ {x:ℤ| 
                                              ((-1) ≤ x)
                                              ∧ (x ≤ max)
                                              ∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
                                              ∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < max ⇒ (y ≤ x)))
                                              ∧ (∀y:ℕ. (y < max ⇒ x < y ⇒ (y ∈ missing)))} )
BY
{ ((UnivCD THENA Auto) THEN DVarSets THEN UnfoldAtAddr [2] 0 THEN NatInd 1 THEN Reduce 0) }

1
1. max : ℤ
2. missing : ℕ List
3. l-ordered(ℕ;x,y.x < y;missing)
⊢ if in-missing(0;missing) then -1 else 0 fi  ∈ {x:ℤ| 
                                                 ((-1) ≤ x)
                                                 ∧ (x ≤ 0)
                                                 ∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
                                                 ∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < 0 ⇒ (y ≤ x)))
                                                 ∧ (∀y:ℕ. (y < 0 ⇒ x < y ⇒ (y ∈ missing)))} 

2
.....upcase..... 
1. missing : ℕ List
2. l-ordered(ℕ;x,y.x < y;missing)
3. max : ℤ
4. 0 < max
5. primrec(max - 1;if in-missing(0;missing) then -1 else 0 fi ;λm,r. if in-missing(m;missing) then r else m fi )
   ∈ {x:ℤ| 
      ((-1) ≤ x)
      ∧ (x ≤ (max - 1))
      ∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
      ∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < max - 1 ⇒ (y ≤ x)))
      ∧ (∀y:ℕ. (y < max - 1 ⇒ x < y ⇒ (y ∈ missing)))} 
⊢ primrec(max;if in-missing(0;missing) then -1 else 0 fi ;λm,r. if in-missing(m;missing) then r else m fi )
  ∈ {x:ℤ| 
     ((-1) ≤ x)
     ∧ (x ≤ max)
     ∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
     ∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < max ⇒ (y ≤ x)))
     ∧ (∀y:ℕ. (y < max ⇒ x < y ⇒ (y ∈ missing)))} 

---

Latex:

---

Latex:
\mforall{}[max:\mBbbN{}].  \mforall{}[missing:\{l:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;l)\}  ].
    (select-last-in-nat-missing(max;missing)  \mmember{}  \{x:\mBbbZ{}| 
                                                                                            ((-1)  \mleq{}  x)
                                                                                            \mwedge{}  (x  \mleq{}  max)
                                                                                            \mwedge{}  ((0  \mleq{}  x)  {}\mRightarrow{}  (\mneg{}(x  \mmember{}  missing)))
                                                                                            \mwedge{}  (\mforall{}y:\mBbbN{}.  ((\mneg{}(y  \mmember{}  missing))  {}\mRightarrow{}  y  <  max  {}\mRightarrow{}  (y  \mleq{}  x)))
                                                                                            \mwedge{}  (\mforall{}y:\mBbbN{}.  (y  <  max  {}\mRightarrow{}  x  <  y  {}\mRightarrow{}  (y  \mmember{}  missing)))\}  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  DVarSets  THEN  UnfoldAtAddr  [2]  0  THEN  NatInd  1  THEN  Reduce  0)

---

Home Index