PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
firstn
lem1
T:Type, x:
, as:T*. x < ||as||
firstn(x+1;as) = (firstn(x;as) @ [as[x]])
By:
Analyze 0
THEN
Analyze 0
Generated subgoal:
1
1.
T:
Type
2.
x:
as:T*. x < ||as||
firstn(x+1;as) = (firstn(x;as) @ [as[x]])
About:
as:T*. x < ||as|| 
firstn(x+1;as) = (firstn(x;as) @ [as[x]]) T:Type, x:, as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]]) as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]])
