PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 1 2
1. T: Type
2. as: T*
3. u: T
4. v: T*
5. 0 < ||v|| (Case of v; nil nil ; a.as' a.firstn(0;as')) = ((Case of v; nil nil ; a.as' nil) @ [v[0]])

0 < ||u.v|| (Case of u.v; nil nil ; a.as' a.firstn(0;as')) = ((Case of u.v; nil nil ; a.as' nil) @ [(u.v)[0]])
By:
Thin -1
THEN
Reduce 0
THEN
Analyze 0
Generated subgoal:

15. 0 < ||v||+1
u.firstn(0;v) = [u]

About:
impliesless_thannatural_numberconsequal
listlist_indniluniverse