PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
length
reverse
1
1.
T:
Type
2.
l:
T*
||rev(l)|| = ||l||
By:
ListInd 2
Generated subgoals:
1
||rev(nil)|| = ||nil||
2
3.
u:
T
4.
v:
T*
5.
||rev(v)|| = ||v||
||rev(u.v)|| = ||u.v||
About:
||rev(nil)|| = ||nil|| 
||rev(u.v)|| = ||u.v|| ||rev(l)|| = ||l|| ||rev(nil)|| = ||nil|| ||rev(u.v)|| = ||u.v|| 
