PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
maction
wf
2
1.
Alph:
Type
2.
S:
ActionSet(Alph)
3.
L:
Alph*
4.
s:
S.car
5.
u:
Alph
6.
v:
Alph*
7.
(S:v
s)
S.car
(S:u.v
s)
S.car
By:
RecCaseSplit `maction`
Generated subgoals:
1
8.
u.v = nil
s
S.car
2
8.
u.v = nil
S.act(u,(S:v
s))
S.car
About:
s 
S.car
u.v = nil S.act(u,(S:v
s)) S.cars) S.car (S:u.vs) S.car s S.caru.v = nil S.act(u,(S:vs)) S.car
