---

Step * of Lemma lastn-as-accum

∀[A:Type]. ∀[n:ℤ]. ∀[L:A List].
  (lastn(n;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:
                 []))
BY
{ xxx((UnivCD THENA Auto) THEN (Decide n ≤ 0 THENA Auto))xxx }

1
1. A : Type
2. n : ℤ
3. L : A List
4. n ≤ 0
⊢ lastn(n;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:
                [])

2
1. A : Type
2. n : ℤ
3. L : A List
4. ¬(n ≤ 0)
⊢ lastn(n;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:
                [])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[n:\mBbbZ{}].  \mforall{}[L:A  List].
    (lastn(n;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:
                                  []))


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  (Decide  n  \mleq{}  0  THENA  Auto))xxx

---

Home Index