PrintForm
Definitions
automata
7
Sections
AutomataTheory
Doc
At:
empty
lang
dec
1
1
1
1
1
1
1
1
1
1
2
1
1.
Alph:
Type
2.
St:
Type
3.
Auto:
Automata(Alph;St)
4.
Fin(Alph)
5.
n:
6.
f:(
n
St). Bij(
n; St; f)
7.
l:
Alph*
8.
FinalState(Auto)((Action(Auto):l
InitialState(Auto)))
St ~
n
By:
Unfold `one_one_corr` 0
Generated subgoal:
1
f:(St
n), g:(
n
St). InvFuns(St;
n; f; g)
About:
f:(St
n), g:(nSt). InvFuns(St; n; f; g)f:(nSt). Bij(n; St; f)
InitialState(Auto))) St ~ n f:(Stn), g:(nSt). InvFuns(St; n; f; g)
