PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 2 2
1. T: Type
2. x:
3. 0 < x
4. as:T*. x-1 < ||as|| firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]])
5. as: T*
6. u: T
7. v: T*
8. x < ||v|| firstn(x+1;v) = (firstn(x;v) @ [v[x]])

x < ||u.v|| firstn(x+1;u.v) = (firstn(x;u.v) @ [(u.v)[x]])
By:
Thin -1
THEN
Reduce 0
THEN
Analyze 0
Generated subgoal:

18. x < ||v||+1
firstn(x+1;u.v) = (firstn(x;u.v) @ [(u.v)[x]])

About:
impliesless_thanconsequallistadd
natural_numberniluniverseintallsubtract