PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem0
1
1.
T:
Type
2.
as:
T*
firstn(||as||;as) = as
By:
ListInd 2
THEN
RecUnfold `firstn` 0
THEN
Reduce 0
Generated subgoal:
1
3.
u:
T
4.
v:
T*
5.
firstn(||v||;v) = v
if 0 <
||v||+1
u.firstn(||v||+1-1;v) else nil fi = u.v
About:
if 0 < 
||v||+1
u.firstn(||v||+1-1;v) else nil fi = u.v firstn(||as||;as) = as if 0 < ||v||+1 u.firstn(||v||+1-1;v) else nil fi = u.v
