---

Step * 1 of Lemma add-nat-missing_wf

.....subterm..... T:t
2:n
1. i : ℕ
2. m : {m:ℤ| (-1) ≤ m} 
3. s1 : {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < m)} 
4. m <z i ∈ 𝔹
5. m < i
⊢ s1 @ [m + 1, i) ∈ {L:ℕ List| l-ordered(ℕ;x,y.x < y;L) ∧ (∀x∈L.x < i)} 
BY
{ (DVarSets
   THEN MemTypeCD
   THEN Auto
   THEN Try (Complete ((Repeat ((RW ListC 0 THEN Auto))
                        THEN (RW ListC (-1) THENA Auto)
                        THEN (RWO "l_all_iff" (-9) THENA Auto)
                        THEN InstHyp [⌈x⌉] (-9)⋅
                        THEN Auto)))
   THEN Using [`T',⌈ℕ⌉] (BLemma `l_all_append`)⋅
   THEN Auto
   THEN All(RWO "l_all_iff")
   THEN Auto
   THEN OnSomeHyp(\i.InstHyp [⌈x⌉] i THEN CpltAuto)⋅) }

---

Latex:


.....subterm.....  T:t
2:n
1.  i  :  \mBbbN{}
2.  m  :  \{m:\mBbbZ{}|  (-1)  \mleq{}  m\} 
3.  s1  :  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  m)\} 
4.  m  <z  i  \mmember{}  \mBbbB{}
5.  m  <  i
\mvdash{}  s1  @  [m  +  1,  i)  \mmember{}  \{L:\mBbbN{}  List|  l-ordered(\mBbbN{};x,y.x  <  y;L)  \mwedge{}  (\mforall{}x\mmember{}L.x  <  i)\} 


By

(DVarSets
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  (Complete  ((Repeat  ((RW  ListC  0  THEN  Auto))
                                            THEN  (RW  ListC  (-1)  THENA  Auto)
                                            THEN  (RWO  "l\_all\_iff"  (-9)  THENA  Auto)
                                            THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-9)\mcdot{}
                                            THEN  Auto)))
  THEN  Using  [`T',\mkleeneopen{}\mBbbN{}\mkleeneclose{}]  (BLemma  `l\_all\_append`)\mcdot{}
  THEN  Auto
  THEN  All(RWO  "l\_all\_iff")
  THEN  Auto
  THEN  OnSomeHyp(\mbackslash{}i.InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  i  THEN  CpltAuto)\mcdot{})

---

Home Index