---

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

.....truecase..... 
1. A : Type
2. n : ℤ
3. u : A
4. v : A List
5. ¬(n ≤ 0)
6. 0 < n
⊢ 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
{ (Assert ∀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))) BY
         (InductionOnList THEN Reduce 0 THEN (UnivCD THENA Auto))) }

1
1. A : Type
2. n : ℤ
3. u : A
4. v : A List
5. ¬(n ≤ 0)
6. 0 < n
7. as : A List
8. n1 : ℤ
9. ||as|| ≤ n1
⊢ lastn(n1;as @ []) ~ as

2
1. A : Type
2. n : ℤ
3. u : A
4. v : A List
5. ¬(n ≤ 0)
6. 0 < n
7. u1 : A
8. v1 : A List
9. ∀as:A List. ∀n:ℤ.
     ((||as|| ≤ n)
     ⇒ (lastn(n;as @ v1) ~ accumulate (with value b and list item x):
                             if ||b|| <z n then b @ [x] else tl(b @ [x]) fi 
                            over list:
                              v1
                            with starting value:
                             as)))
10. as : A List
11. n1 : ℤ
12. ||as|| ≤ n1
⊢ lastn(n1;as @ [u1 / v1]) ~ accumulate (with value b and list item x):
                              if ||b|| <z n1 then b @ [x] else tl(b @ [x]) fi 
                             over list:
                               v1
                             with starting value:
                              if ||as|| <z n1 then as @ [u1] else tl(as @ [u1]) fi )

3
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])

---

Latex:

---

Latex:
.....truecase..... 
1.  A  :  Type
2.  n  :  \mBbbZ{}
3.  u  :  A
4.  v  :  A  List
5.  \mneg{}(n  \mleq{}  0)
6.  0  <  n
\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:
(Assert  \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)))  BY
              (InductionOnList  THEN  Reduce  0  THEN  (UnivCD  THENA  Auto)))

---

Home Index