PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem1
1
1
2
1
1.
T:
Type
2.
as:
T*
3.
u:
T
4.
v:
T*
5.
0 < ||v||+1
u.firstn(0;v) = [u]
By:
Analyze
Generated subgoal:
1
firstn(0;v) = nil
About:
u.firstn(0;v) = [u] firstn(0;v) = nil
