---

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
   THEN Try (Complete ((AutoSplit THEN MemTypeCD THEN Auto THEN All(RWO "assert-in-missing-nat-iff") THEN Auto)))) }

1
.....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:


\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

((UnivCD  THENA  Auto)
  THEN  DVarSets
  THEN  UnfoldAtAddr  [2]  0
  THEN  NatInd  1
  THEN  Reduce  0
  THEN  Try  (Complete  ((AutoSplit
                                            THEN  MemTypeCD
                                            THEN  Auto
                                            THEN  All(RWO  "assert-in-missing-nat-iff")
                                            THEN  Auto))))

---

Home Index