PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
action
append
1
1.
T:
Type
2.
S:
ActionSet(T)
3.
s:
S.car
4.
tl1:
T*
5.
tl2:
T*
(S:tl1 @ tl2
s) = (S:tl1
(S:tl2
s))
By:
ListInd -2
THEN
RecUnfold `maction` 0
THEN
Reduce 0
THEN
RecFold `maction` 0
Generated subgoal:
1
6.
u:
T
7.
v:
T*
8.
(S:v @ tl2
s) = (S:v
(S:tl2
s))
S.act(u,(S:v @ tl2
s)) = S.act(u,(S:v
(S:tl2
s)))
About:
s) = (S:v(S:tl2s))
S.act(u,(S:v @ tl2s)) = S.act(u,(S:v(S:tl2s))) (S:tl1 @ tl2s) = (S:tl1(S:tl2s))s) = (S:v(S:tl2s)) S.act(u,(S:v @ tl2s)) = S.act(u,(S:v(S:tl2s)))
