PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
length
reverse
1
2
1.
T:
Type
2.
l:
T*
3.
u:
T
4.
v:
T*
5.
||rev(v)|| = ||v||
||rev(u.v)|| = ||u.v||
By:
RecUnfold `reverse` 0
THEN
Reduce 0
Generated subgoal:
1
||rev(v) @ [u]|| = ||v||+1
About:
||rev(v) @ [u]|| = ||v||+1
||rev(u.v)|| = ||u.v|| ||rev(v) @ [u]|| = ||v||+1
