PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
whole
segment
1
1
1
1.
T:
Type
2.
as:
T*
firstn(||as||;as) = as
By:
ListInd 2
Generated subgoals:
1
firstn(||nil||;nil) = nil
T*
2
3.
u:
T
4.
v:
T*
5.
firstn(||v||;v) = v
firstn(||u.v||;u.v) = u.v
About:
firstn(||nil||;nil) = nil 
T* firstn(||u.v||;u.v) = u.v firstn(||as||;as) = as firstn(||nil||;nil) = nil T* firstn(||u.v||;u.v) = u.v
