PrintForm
Definitions
automata
4
Sections
AutomataTheory
Doc
At:
auto
iso
sym
1
1
1
1
2
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)
13.
s:
S2
14.
a:
Alph
g(
A2(s,a)) =
A1(g(s),a)
By:
Witness8 g(s)
Generated subgoal:
1
8.
f(InitialState(A1)) = InitialState(A2)
9.
s:S1. FinalState(A1)(s) = FinalState(A2)(f(s))
10.
g:
S2
S1
11.
InvFuns(S1; S2; f; g)
12.
s:
S2
13.
a:
Alph
14.
a:Alph. f(
A1(g(s),a)) =
A2(f(g(s)),a)
g(
A2(s,a)) =
A1(g(s),a)
About: