PrintForm
Definitions
det
automata
Sections
AutomataTheory
Doc
At:
action
auto
1
2
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
l:
Alph*
5.
u:
Alph
6.
v:
Alph*
7.
( < St,
l,s.
Auto(s,l) > :v
InitialState(Auto)) = (Result(Auto)v)
Auto(( < St,
l,s.
Auto(s,l) > :v
InitialState(Auto)),u) =
Auto((Result(Auto)v),u)
By:
RWH (HypC 7) 0
Generated subgoals:
None
About:
l,s. 
Auto(s,l) > :v
InitialState(Auto)) = (Result(Auto)v)
Auto(( < St,l,s. Auto(s,l) > :vInitialState(Auto)),u) = Auto((Result(Auto)v),u)