---

Step * 2 of Lemma last_index_append


1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
⊢ (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:
        <||as||, last_index(as;x.P[x])>)))
= if 0 <z last_index(bs;x.P[x]) then ||as|| + last_index(bs;x.P[x]) else last_index(as;x.P[x]) fi 
∈ ℤ
BY
{ xxx(((GenConclTerm ⌜||as||⌝⋅ THENA Auto) THEN (GenConcl ⌜last_index(as;x.P[x]) = n ∈ ℤ⌝⋅ THENA Auto))
      THEN All Thin
      )xxx }

1
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 
∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\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:
                <||as||,  last\_index(as;x.P[x])>)))
=  if  0  <z  last\_index(bs;x.P[x])  then  ||as||  +  last\_index(bs;x.P[x])  else  last\_index(as;x.P[x])  fi 


By

---

Latex:
xxx(((GenConclTerm  \mkleeneopen{}||as||\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}last\_index(as;x.P[x])  =  n\mkleeneclose{}\mcdot{}  THENA  Auto))
        THEN  All  Thin
        )xxx

---

Home Index