PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
append
front
1
1
1.
T:
Type
2.
l:
T*
3.
m:
T*
4.
||l|| > 0
(l @ m)[0] = l[0]
By:
RWH (LemmaC
Thm*
as,bs:T*, i:
||as||. (as @ bs)[i] = as[i]) 0
Generated subgoals:
None
About:
(l @ m)[0] = l[0]
as,bs:T*, i:
||as||. (as @ bs)[i] = as[i])
0
