---

Step * 1 1 1 1 of Lemma last_index_append

.....assertion..... 
1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
⊢ ∀n,m:ℤ.
    (fst(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:
           as
         with starting value:
          <n, m>)) ~ n + ||as||)
BY
{ xxx(All Thin THEN ListInd 2 THEN Reduce 0 THEN Auto THEN RWO "-3" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mforall{}n,m:\mBbbZ{}.
        (fst(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:
                      as
                  with  starting  value:
                    <n,  m>))  \msim{}  n  +  ||as||)


By

---

Latex:
xxx(All  Thin  THEN  ListInd  2  THEN  Reduce  0  THEN  Auto  THEN  RWO  "-3"  0  THEN  Auto)xxx

---

Home Index