PrintForm
Definitions
automata
4
Sections
AutomataTheory
Doc
At:
auto
iso
sym
1
1
1
1
1
1.
Alph:
Type
2.
S1:
Type
3.
S2:
Type
4.
A1:
Automata(Alph;S1)
5.
A2:
Automata(Alph;S2)
6.
f:
S1
S2
7.
Bij(S1; S2; f)
8.
s:S1, a:Alph. f(
A1(s,a)) =
A2(f(s),a)
9.
f(InitialState(A1)) = InitialState(A2)
10.
s:S1. FinalState(A1)(s) = FinalState(A2)(f(s))
11.
g:
S2
S1
12.
InvFuns(S1; S2; f; g)
Bij(S2; S1; g)
By:
Inst Thm*
f:(A
B), g:(B
A). InvFuns(A; B; f; g)
InvFuns(B; A; g; f) [S1;S2;f;g]
Generated subgoal:
1
13.
InvFuns(S2; S1; g; f)
Bij(S2; S1; g)
About: