PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
whole
segment
1
1.
T:
Type
2.
as:
T*
(as[0..||as||
]) = as
By:
Unfold `segment` 0
THEN
ArithSimp 0
Generated subgoal:
1
firstn(||as||;nth_tl(0;as)) = as
About:
firstn(||as||;nth_tl(0;as)) = as (as[0..||as||
]) = as firstn(||as||;nth_tl(0;as)) = as
