PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem1
1
2
2
1
1
1
1
2
1.
T:
Type
2.
x:
3.
0 < x
4.
as:T*. -1+x < ||as||
firstn(x;as) = (firstn(-1+x;as) @ [as[(-1+x)]])
5.
as:
T*
6.
u:
T
7.
v:
T*
8.
x < ||v||+1
9.
0 < x+1
10.
0 < x
u.firstn(x;v) = ((u.firstn(-1+x;v)) @ [(u.v)[x]])
By:
Reduce 0
THEN
Analyze
Generated subgoals:
1
u = u
2
firstn(x;v) = (firstn(-1+x;v) @ [(u.v)[x]])
About:
u = u firstn(x;v) = (firstn(-1+x;v) @ [(u.v)[x]])
as:T*. -1+x < ||as|| 
firstn(x;as) = (firstn(-1+x;as) @ [as[(-1+x)]]) u.firstn(x;v) = ((u.firstn(-1+x;v)) @ [(u.v)[x]]) u = u firstn(x;v) = (firstn(-1+x;v) @ [(u.v)[x]])
