---

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

.....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)))} 
BY
{ (Assert max - 1 ∈ ℕ BY
         (Lemmaize [4] THEN Auto)) }

1
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)))} 
6. max - 1 ∈ ℕ
⊢ 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:
.....upcase..... 
1.  missing  :  \mBbbN{}  List
2.  l-ordered(\mBbbN{};x,y.x  <  y;missing)
3.  max  :  \mBbbZ{}
4.  0  <  max
5.  primrec(max  -  1;if  in-missing(0;missing)  then  -1  else  0  fi  ;\mlambda{}m,r.  if  in-missing(m;missing)
                                                                                                                                        then  r
                                                                                                                                        else  m
                                                                                                                                        fi  )  \mmember{}  \{x:\mBbbZ{}| 
                                                                                                                                                ((-1)  \mleq{}  x)
                                                                                                                                                \mwedge{}  (x  \mleq{}  (max  -  1))
                                                                                                                                                \mwedge{}  ((0  \mleq{}  x)
                                                                                                                                                    {}\mRightarrow{}  (\mneg{}(x  \mmember{}  missing)))
                                                                                                                                                \mwedge{}  (\mforall{}y:\mBbbN{}
                                                                                                                                                          ((\mneg{}(y  \mmember{}  missing))
                                                                                                                                                          {}\mRightarrow{}  y  <  max  -  1
                                                                                                                                                          {}\mRightarrow{}  (y  \mleq{}  x)))
                                                                                                                                                \mwedge{}  (\mforall{}y:\mBbbN{}
                                                                                                                                                          (y  <  max  -  1
                                                                                                                                                          {}\mRightarrow{}  x  <  y
                                                                                                                                                          {}\mRightarrow{}  (y  \mmember{}  missing)))\} 
\mvdash{}  primrec(max;if  in-missing(0;missing)  then  -1  else  0  fi  ;\mlambda{}m,r.  if  in-missing(m;missing)
                                                                                                                              then  r
                                                                                                                              else  m
                                                                                                                              fi  )  \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:
(Assert  max  -  1  \mmember{}  \mBbbN{}  BY
              (Lemmaize  [4]  THEN  Auto))

---

Home Index