---

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

.....falsecase..... 
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
13. n1 ≤ ||as||
⊢ lastn(n1;as @ [u1 / v1]) ~ lastn(n1;tl(as @ [u1]) @ v1)
BY
{ ((RW (AddrC [1] (LemmaC `lastn-cases`)) 0 THENA Auto) THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
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
13. n1 ≤ ||as||
14. ||as @ [u1 / v1]|| ≤ n1
⊢ as @ [u1 / v1] ~ lastn(n1;tl(as @ [u1]) @ v1)

2
.....falsecase..... 
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
13. n1 ≤ ||as||
14. n1 < ||as @ [u1 / v1]||
⊢ if n1 ≤z 0 then [] else lastn(n1;tl(as @ [u1 / v1])) fi  ~ lastn(n1;tl(as @ [u1]) @ v1)

---

Latex:

---

Latex:
.....falsecase..... 
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
13.  n1  \mleq{}  ||as||
\mvdash{}  lastn(n1;as  @  [u1  /  v1])  \msim{}  lastn(n1;tl(as  @  [u1])  @  v1)


By

---

Latex:
((RW  (AddrC  [1]  (LemmaC  `lastn-cases`))  0  THENA  Auto)  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index