PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
append
back
1
2
1.
T:
Type
2.
l:
T*
3.
m:
T*
4.
||m|| > 0
5.
u:
T
6.
v:
T*
7.
||v|| = 0
hd((v @ m)) = hd(m)
||u.v|| = 0
hd(((u.v) @ m)) = hd(m)
By:
Reduce 0
Generated subgoals:
None
About:
hd((v @ m)) = hd(m)
||u.v|| = 0 hd(((u.v) @ m)) = hd(m)
