---

Step * 1 1 1 of Lemma last_index_append


1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
⊢ (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:
        <0, 0>)))
= ||as||
∈ ℤ
BY
{ xxx(Assert ⌜∀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||)⌝⋅
THENM (RWO "-1" 0 THEN Auto)
)xxx }

1
.....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||)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  (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:
                ɘ,  0>)))
=  ||as||


By

---

Latex:
xxx(Assert  \mkleeneopen{}\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||)\mkleeneclose{}\mcdot{}
THENM  (RWO  "-1"  0  THEN  Auto)
)xxx

---

Home Index