PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem1
1
2
1
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*
x < ||nil||
firstn(x+1;nil) = (firstn(x;nil) @ [nil[x]])
T*
By:
Reduce 0
Generated subgoals:
None
About:
as:T*. x-1 < ||as|| 
firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]])
x < ||nil|| firstn(x+1;nil) = (firstn(x;nil) @ [nil[x]]) 
T*
