At: derive trans 1 1 2 2 1 3
1. V: Type
2. T: Type
3. G: Grammar(V;T)
4. l: (V+T)*
5. m: (V+T)*
6. n: (V+T)*
7. a1: ((V+T)*)*
8. ||a1|| > 0
9. l = a1[0]
10. 
i:
(||a1||-1). a1[i] 
a1[(i+1)]
11. a1[(||a1||-1)] = m
12. a: ((V+T)*)*
13. ||a|| > 0
14. m = a[0]
15. i:(||a||-1). a[i] a[(i+1)]
16. a[(||a||-1)] = n
17. i: (||firstn(||a1||-1;a1) @ a||-1)
18. i < ||a1||-2
firstn(||a1||-1;a1)[i] firstn(||a1||-1;a1)[(i+1)]
By: RWH
(LemmaC
Thm* as:T*, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i])
0
Generated subgoal:
About:
