PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
tl
append
front
1
2
1.
T:
Type
2.
l:
T*
3.
m:
T*
4.
u:
T
5.
v:
T*
6.
||v|| > 0
tl((v @ m)) = (tl(v) @ m)
||u.v|| > 0
tl(((u.v) @ m)) = (tl((u.v)) @ m)
By:
Analyze 0
Generated subgoal:
1
7.
||u.v|| > 0
tl(((u.v) @ m)) = (tl((u.v)) @ m)
About:
tl(((u.v) @ m)) = (tl((u.v)) @ m)
tl((v @ m)) = (tl(v) @ m) ||u.v|| > 0 tl(((u.v) @ m)) = (tl((u.v)) @ m) tl(((u.v) @ m)) = (tl((u.v)) @ m)
