PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
tl
append
back
T:Type, l,m:T*. ||l|| = 0
||m|| > 0
tl((l @ m)) = tl(m)
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
l:
T*
3.
m:
T*
4.
||l|| = 0
5.
||m|| > 0
tl((l @ m)) = tl(m)
About:
tl((l @ m)) = tl(m) 
T:Type, l,m:T*. ||l|| = 0 
||m|| > 0 tl((l @ m)) = tl(m) tl((l @ m)) = tl(m)
