---

Step * 2 2 1 3 of Lemma lastn-as-accum


1. A : Type
2. n : ℤ
3. u : A
4. v : A List
5. ¬(n ≤ 0)
6. 0 < n
7. ∀L,as:A List. ∀n:ℤ.
     ((||as|| ≤ n)
     ⇒ (lastn(n;as @ L) ~ accumulate (with value b and list item x):
                            if ||b|| <z n then b @ [x] else tl(b @ [x]) fi 
                           over list:
                             L
                           with starting value:
                            as)))
⊢ lastn(n;[u / v]) ~ accumulate (with value b and list item x):
                      if ||b|| <z n then b @ [x] else tl(b @ [x]) fi 
                     over list:
                       v
                     with starting value:
                      [u])
BY
{ ((InstHyp [⌜v⌝;⌜[u]⌝;⌜n⌝] (-1)⋅ THENA (Reduce 0 THEN Auto)) THEN RWO "-1<" 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbZ{}
3.  u  :  A
4.  v  :  A  List
5.  \mneg{}(n  \mleq{}  0)
6.  0  <  n
7.  \mforall{}L,as:A  List.  \mforall{}n:\mBbbZ{}.
          ((||as||  \mleq{}  n)
          {}\mRightarrow{}  (lastn(n;as  @  L)  \msim{}  accumulate  (with  value  b  and  list  item  x):
                                                        if  ||b||  <z  n  then  b  @  [x]  else  tl(b  @  [x])  fi 
                                                      over  list:
                                                          L
                                                      with  starting  value:
                                                        as)))
\mvdash{}  lastn(n;[u  /  v])  \msim{}  accumulate  (with  value  b  and  list  item  x):
                                            if  ||b||  <z  n  then  b  @  [x]  else  tl(b  @  [x])  fi 
                                          over  list:
                                              v
                                          with  starting  value:
                                            [u])


By

---

Latex:
((InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}[u]\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  RWO  "-1<"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index