---

Step * 1 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
{ ((RWO "primrec-unroll-1" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit
   THEN (All(RWO "assert-in-missing-nat-iff") THENA Auto)
   THEN Try (Complete ((MemTypeCD 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 ∈ missing)
⊢ 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)
     ∧ ((0 ≤ x) ⇒ (¬(x ∈ missing)))
     ∧ (∀y:ℕ. ((¬(y ∈ missing)) ⇒ y < max ⇒ (y ≤ x)))
     ∧ (∀y:ℕ. (y < max ⇒ x < y ⇒ (y ∈ missing)))} 

---

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

((RWO  "primrec-unroll-1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (All(RWO  "assert-in-missing-nat-iff")  THENA  Auto)
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto))))

---

Home Index