PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem0
1
1
1
1.
T:
Type
2.
as:
T*
3.
u:
T
4.
v:
T*
5.
firstn(||v||;v) = v
6.
0 < 1+||v||
u.firstn(||v||;v) = u.v
By:
Analyze
Generated subgoals:
None
About:
u.firstn(||v||;v) = u.v
