PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
maction
lemma
1
2
1
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 = (S:u.(v @ L2)
s)
By:
AbReduce 11
Generated subgoal:
1
11.
u.(v @ L1) = nil
s = (S:u.(v @ L2)
s)
About:
s = (S:u.(v @ L2)
s)s) = (S:L2s)s) = (S:v @ L2s) s = (S:u.(v @ L2)s) s = (S:u.(v @ L2)s)
