---

Step * of Lemma last_index_append

∀[T:Type]. ∀[as,bs:T List]. ∀[P:T ⟶ 𝔹].
  (last_index(as @ bs;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(Intros
      THEN Subst' last_index(as @ bs;x.P[x]) ~ 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])>)) 0
      )xxx }

1
.....equality..... 
1. T : Type
2. as : T List
3. bs : T List
4. P : T ⟶ 𝔹
⊢ last_index(as @ bs;x.P[x]) ~ 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])>))

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    ...


By

---

Latex:
xxx(Intros
        THEN  Subst'  last\_index(as  @  bs;x.P[x])  \msim{}  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])>))  0
        )xxx

---

Home Index