PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
length
reverse
1
1
1.
T:
Type
2.
l:
T*
||rev(nil)|| = ||nil||
By:
RecUnfold `reverse` 0
THEN
RecUnfold `length` 0
THEN
Reduce 0
Generated subgoals:
None
About:
||rev(nil)|| = ||nil|| 
