---

Step * 2 of Lemma filter-index_wf


1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀i:ℕ||v||. ((↑(P v[i])) ⇒ (filter-index(P;v) i ∈ {j:ℕ||filter(P;v)||| filter(P;v)[j] = v[i] ∈ T} ))
6. i : ℕ||v|| + 1
⊢ (↑(P [u / v][i]))
⇒ (filter-index(P;[u / v]) i ∈ {j:ℕ||if P u then [u / filter(P;v)] else filter(P;v) fi ||| 
                                 if P u then [u / filter(P;v)] else filter(P;v) fi [j] = [u / v][i] ∈ T} )
BY
{ ((SplitOnConclITE THENA Auto)
   THEN CaseNat 0 `i'
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN Try (Trivial)
   THEN ((RWO "select_cons_tl" (-1) THENA Auto) ORELSE (RepUR ``filter-index`` 0 THEN Auto))
   THEN (Assert filter-index(P;v) (i - 1) ∈ {j:ℕ||filter(P;v)||| filter(P;v)[j] = v[i - 1] ∈ T}  BY
               Auto)
   THEN Unfold `filter-index` 0
   THEN Reduce 0
   THEN Fold `filter-index` 0
   THEN (GenConclTerm ⌜filter-index(P;v) (i - 1)⌝⋅ THENA Auto)
   THEN D -2
   THEN (MemTypeCD THENW (All Thin THEN Auto))
   THEN Thin (-1)
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}i:\mBbbN{}||v||.  ((\muparrow{}(P  v[i]))  {}\mRightarrow{}  (filter-index(P;v)  i  \mmember{}  \{j:\mBbbN{}||filter(P;v)|||  filter(P;v)[j]  =  v[i]\}  ))
6.  i  :  \mBbbN{}||v||  +  1
\mvdash{}  (\muparrow{}(P  [u  /  v][i]))
{}\mRightarrow{}  (filter-index(P;[u  /  v])  i  \mmember{}  \{j:\mBbbN{}||if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi  ||| 
                                                                  if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi  [j]
                                                                  =  [u  /  v][i]\}  )


By

---

Latex:
((SplitOnConclITE  THENA  Auto)
  THEN  CaseNat  0  `i'
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  ((RWO  "select\_cons\_tl"  (-1)  THENA  Auto)  ORELSE  (RepUR  ``filter-index``  0  THEN  Auto))
  THEN  (Assert  filter-index(P;v)  (i  -  1)  \mmember{}  \{j:\mBbbN{}||filter(P;v)|||  filter(P;v)[j]  =  v[i  -  1]\}    BY
                          Auto)
  THEN  Unfold  `filter-index`  0
  THEN  Reduce  0
  THEN  Fold  `filter-index`  0
  THEN  (GenConclTerm  \mkleeneopen{}filter-index(P;v)  (i  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  (MemTypeCD  THENW  (All  Thin  THEN  Auto))
  THEN  Thin  (-1)
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index