---

Step * 2 of Lemma add-nat-missing_wf

.....subterm..... T:t
2:n
1. i : ℕ
2. m : {m:ℤ| (-1) ≤ m} 
3. m ≠ i
4. ¬m < i
5. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
6. ff ∈ 𝔹
7. ff ∈ 𝔹
⊢ remove-combine(λx.(x - i);s1) ∈ {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
BY
{ (DVarSets
   THEN MemTypeCD
   THEN Auto
   THEN Try ((BLemma `l-ordered-remove-combine` THEN Auto))
   THEN RWO "l_all_iff" 0
   THEN Auto
   THEN (FLemma `remove-combine-implies-member` [-1] THENA Auto)
   THEN All(RWO "l_all_iff")
   THEN Auto) }

---

Latex:


.....subterm.....  T:t
2:n
1.  i  :  \mBbbN{}
2.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\} 
3.  m  \mneq{}  i
4.  \mneg{}m  <  i
5.  s1  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\} 
6.  ff  \mmember{}  \mBbbB{}
7.  ff  \mmember{}  \mBbbB{}
\mvdash{}  remove-combine(\mlambda{}x.(x  -  i);s1)  \mmember{}  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\} 


By

(DVarSets
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((BLemma  `l-ordered-remove-combine`  THEN  Auto))
  THEN  RWO  "l\_all\_iff"  0
  THEN  Auto
  THEN  (FLemma  `remove-combine-implies-member`  [-1]  THENA  Auto)
  THEN  All(RWO  "l\_all\_iff")
  THEN  Auto)

---

Home Index