PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem1
1
2
2
1
1
1
1
2
2
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
11.
firstn(x;v) = (firstn(-1+x;v) @ [v[(-1+x)]])
(firstn(-1+x;v) @ [v[(-1+x)]]) = (firstn(-1+x;v) @ [(u.v)[x]])
By:
Analyze
Generated subgoal:
1
[v[(-1+x)]] = [(u.v)[x]]
About:
[v[(-1+x)]] = [(u.v)[x]]
as:T*. -1+x < ||as|| 
firstn(x;as) = (firstn(-1+x;as) @ [as[(-1+x)]]) (firstn(-1+x;v) @ [v[(-1+x)]]) = (firstn(-1+x;v) @ [(u.v)[x]]) [v[(-1+x)]] = [(u.v)[x]]
