---

Step * 2 1 of Lemma last_index_append


1. T : Type
2. bs : T List
3. P : T ⟶ 𝔹
4. v : ℕ
5. n : ℤ
⊢ (snd(accumulate (with value p and list item x):
        let n,lst = p 
        in <n + 1, if P[x] then n + 1 else lst fi >
       over list:
         bs
       with starting value:
        <v, n>)))
= if 0 <z last_index(bs;x.P[x]) then v + last_index(bs;x.P[x]) else n fi 
∈ ℤ
BY
{ xxx(Unfold `last_index` 0
      THEN RepeatFor 2 (MoveToConcl (-1))
      THEN ListInd 2
      THEN Reduce 0
      THEN Auto
      THEN (RWO "-3" 0 THENA Auto)
      THEN Fold `last_index` 0
      THEN AutoSplit)xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  v  :  \mBbbN{}
5.  n  :  \mBbbZ{}
\mvdash{}  (snd(accumulate  (with  value  p  and  list  item  x):
                let  n,lst  =  p 
                in  <n  +  1,  if  P[x]  then  n  +  1  else  lst  fi  >
              over  list:
                  bs
              with  starting  value:
                <v,  n>)))
=  if  0  <z  last\_index(bs;x.P[x])  then  v  +  last\_index(bs;x.P[x])  else  n  fi 


By

---

Latex:
xxx(Unfold  `last\_index`  0
        THEN  RepeatFor  2  (MoveToConcl  (-1))
        THEN  ListInd  2
        THEN  Reduce  0
        THEN  Auto
        THEN  (RWO  "-3"  0  THENA  Auto)
        THEN  Fold  `last\_index`  0
        THEN  AutoSplit)xxx

---

Home Index