PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
maction
lemma
1
2
2
1.
Alph:
Type
2.
S:
ActionSet(Alph)
3.
s:
S.car
4.
L1:
Alph*
5.
L2:
Alph*
6.
L:
Alph*
7.
(S:L1
s) = (S:L2
s)
8.
u:
Alph
9.
v:
Alph*
10.
(S:v @ L1
s) = (S:v @ L2
s)
11.
((u.v) @ L1) = nil
S.act(u,(S:v @ L1
s)) = (S:u.(v @ L2)
s)
By:
RW (LowerC (HypC 10)) 0
Generated subgoal:
1
S.act(u,(S:v @ L2
s)) = (S:u.(v @ L2)
s)
About:
S.act(u,(S:v @ L2
s)) = (S:u.(v @ L2)s)s) = (S:L2s)s) = (S:v @ L2s)
((u.v) @ L1) = nil S.act(u,(S:v @ L1s)) = (S:u.(v @ L2)s) S.act(u,(S:v @ L2s)) = (S:u.(v @ L2)s)
