PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
length
reverse
1
2
1
1.
T:
Type
2.
l:
T*
3.
u:
T
4.
v:
T*
5.
||rev(v)|| = ||v||
||rev(v) @ [u]|| = ||v||+1
By:
RWH (LemmaC
Thm*
as,bs:T*. ||as @ bs|| = ||as||+||bs||) 0
Generated subgoal:
1
||rev(v)||+||[u]|| = ||v||+1
About:
||rev(v)||+||[u]|| = ||v||+1
||rev(v) @ [u]|| = ||v||+1
as,bs:T*. ||as @ bs|| = ||as||+||bs||)
0 ||rev(v)||+||[u]|| = ||v||+1
