---

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


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 )
BY
{ (RWO "-4<" 0 THENA Auto) }

1
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
⊢ ||if ||as|| <z n1 then as @ [u1] else tl(as @ [u1]) fi || ≤ n1

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]) ~ lastn(n1;if ||as|| <z n1 then as @ [u1] else tl(as @ [u1]) fi  @ v1)

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbZ{}
3.  u  :  A
4.  v  :  A  List
5.  \mneg{}(n  \mleq{}  0)
6.  0  <  n
7.  u1  :  A
8.  v1  :  A  List
9.  \mforall{}as:A  List.  \mforall{}n:\mBbbZ{}.
          ((||as||  \mleq{}  n)
          {}\mRightarrow{}  (lastn(n;as  @  v1)  \msim{}  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  :  \mBbbZ{}
12.  ||as||  \mleq{}  n1
\mvdash{}  lastn(n1;as  @  [u1  /  v1])  \msim{}  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  )


By

---

Latex:
(RWO  "-4<"  0  THENA  Auto)

---

Home Index