Step
*
2
2
1
2
2
2
2
2
1
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
13. n1 ≤ ||as||
14. n1 < ||as @ [u1 / v1]||
15. 0 < n1
⊢ tl(as @ [u1 / v1]) ~ tl(as @ [u1]) @ v1
BY
{ (DVar `as' THEN Reduce 0 THEN Try (Trivial)) }
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. u2 : A
11. v2 : A List
12. n1 : ℤ
13. ||[u2 / v2]|| ≤ n1
14. n1 ≤ ||[u2 / v2]||
15. n1 < ||[u2 / v2] @ [u1 / v1]||
16. 0 < n1
⊢ v2 @ [u1 / v1] ~ (v2 @ [u1]) @ 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
13.  n1  \mleq{}  ||as||
14.  n1  <  ||as  @  [u1  /  v1]||
15.  0  <  n1
\mvdash{}  tl(as  @  [u1  /  v1])  \msim{}  tl(as  @  [u1])  @  v1
By
Latex:
(DVar  `as'  THEN  Reduce  0  THEN  Try  (Trivial))
Home
Index