PrintForm Definitions grammar 1 Sections AutomataTheory Doc

At: derive trans 1 1
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

a:((V+T)* List). l = a[0] & (i:(||a||-1). a[i] a[(i+1)]) & a[(||a||-1)] = n
By: Witness firstn(||a1||-1;a1) @ a
Generated subgoals:

18. ||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
(firstn(||a1||-1;a1) @ a) ((V+T)* List)
2 l = (firstn(||a1||-1;a1) @ a)[0] & (i:(||firstn(||a1||-1;a1) @ a||-1). (firstn(||a1||-1;a1) @ a)[i] (firstn(||a1||-1;a1) @ a)[(i+1)]) & (firstn(||a1||-1;a1) @ a)[(||firstn(||a1||-1;a1) @ a||-1)] = n
38. ||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. a2: (V+T)* List
(l = a2[0] & (i:(||a2||-1). a2[i] a2[(i+1)]) & a2[(||a2||-1)] = n) Prop

About:
existslistunionandequalnatural_number
allsubtractadduniversememberprop