PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
reverse
1
2
2
1
1
1
1
1.
T:
Type
2.
l:
T*
3.
u:
T
4.
v:
T*
5.
||v|| = 0
6.
hd(rev(v)) = v[(||v||-1)]
||v||+1 > 0
hd(rev(v)) = v[(||v||+1-1-1)]
By:
RWH (HypC 6) 0
Generated subgoal:
1
||v||+1 > 0
v[(||v||-1)] = v[(||v||+1-1-1)]
About:
||v||+1 > 0 
v[(||v||-1)] = v[(||v||+1-1-1)]
||v|| = 0 ||v||+1 > 0 hd(rev(v)) = v[(||v||+1-1-1)] ||v||+1 > 0 v[(||v||-1)] = v[(||v||+1-1-1)]
