---

Step * 2 2 of Lemma remove-nat-missing-prop


1. m : ℤ@i
2. \\%18 : (-1) ≤ m@i
3. s1 : ℕ List@i
4. \\%17 : l-ordered(ℕ;x,y.x < y;s1) ∧ (∀x∈s1.x < m)@i
5. ¬(s1 = [] ∈ (ℕ List))
6. x : ℕ@i
7. y : ℕ@i
8. y = m ∈ ℤ
9. last(s1) ≠ m - 1
⊢ ↑member-nat-missing(x;<m - 1, s1>) ⇐⇒ (¬(x = y ∈ ℕ)) ∧ (↑member-nat-missing(x;<m, s1>))
BY
{ (RWO "assert-member-nat-missing" 0
   THEN Reduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN RepeatFor 2 (ParallelOp 5)
   THEN Decide ⌈s1[i] = (m - 1) ∈ ℕ⌉⋅
   THEN Auto
   THEN Assert ⌈s1[i] ≤ last(s1)⌉⋅
   THEN Try (Complete (((InstHyp [⌈||s1|| - 1⌉] 5⋅ THENA Auto) THEN Fold `last` (-1) THEN Auto)))
   THEN (Decide i = (||s1|| - 1) ∈ ℤ THENA Auto)
   THEN Try (Complete (((RWO "-1" 0 THENA Auto) THEN Fold `last` 0 THEN Auto)))
   THEN (Unfold `last` 0 THEN Using [`j',⌈i⌉;`i',⌈||s1|| - 1⌉] (FLemma `l-ordered-inst` [-5])⋅)
   THEN Auto) }

---

Latex:



1.  m  :  \mBbbZ{}@i
2.  \mbackslash{}\mbackslash{}\%18  :  (-1)  \mleq{}  m@i
3.  s1  :  \mBbbN{}  List@i
4.  \mbackslash{}\mbackslash{}\%17  :  l-ordered(\mBbbN{};x,y.x  <  y;s1)  \mwedge{}  (\mforall{}x\mmember{}s1.x  <  m)@i
5.  \mneg{}(s1  =  [])
6.  x  :  \mBbbN{}@i
7.  y  :  \mBbbN{}@i
8.  y  =  m
9.  last(s1)  \mneq{}  m  -  1
\mvdash{}  \muparrow{}member-nat-missing(x;<m  -  1,  s1>)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}member-nat-missing(x;<m,  s1>))


By

(RWO  "assert-member-nat-missing"  0
  THEN  Reduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  5)
  THEN  Decide  \mkleeneopen{}s1[i]  =  (m  -  1)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Assert  \mkleeneopen{}s1[i]  \mleq{}  last(s1)\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (((InstHyp  [\mkleeneopen{}||s1||  -  1\mkleeneclose{}]  5\mcdot{}  THENA  Auto)  THEN  Fold  `last`  (-1)  THEN  Auto)))
  THEN  (Decide  i  =  (||s1||  -  1)  THENA  Auto)
  THEN  Try  (Complete  (((RWO  "-1"  0  THENA  Auto)  THEN  Fold  `last`  0  THEN  Auto)))
  THEN  (Unfold  `last`  0  THEN  Using  [`j',\mkleeneopen{}i\mkleeneclose{};`i',\mkleeneopen{}||s1||  -  1\mkleeneclose{}]  (FLemma  `l-ordered-inst`  [-5])\mcdot{})
  THEN  Auto)

---

Home Index