let OAlph, IAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
set cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:];
A1:
( accessibleStates tfsm c= the carrier of tfsm & IAlph c= IAlph )
by Th67;
then
[:(accessibleStates tfsm),IAlph:] c= [:the carrier of tfsm,IAlph:]
by ZFMISC_1:119;
then
the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:],the carrier of tfsm
by FUNCT_2:38;
then A2:
dom (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) = [:(accessibleStates tfsm),IAlph:]
by FUNCT_2:def 1;
rng (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) c= accessibleStates tfsm
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) or x in accessibleStates tfsm )
assume A3:
x in rng (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:])
;
:: thesis: x in accessibleStates tfsm
rng (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) c= the
carrier of
tfsm
by RELAT_1:def 19;
then reconsider q1 =
x as
State of
tfsm by A3;
consider d being
set such that A4:
(
d in dom (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) &
x = (the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) . d )
by A3, FUNCT_1:def 5;
A5:
(
d `1 in accessibleStates tfsm &
d `2 in IAlph )
by A2, A4, MCART_1:10;
then reconsider q =
d `1 as
State of
tfsm by A1;
reconsider s =
d `2 as
Element of
IAlph by A2, A4, MCART_1:10;
set I = the
InitS of
tfsm;
q is
accessible
by A5, Th67;
then consider w being
FinSequence of
IAlph such that A6:
the
InitS of
tfsm,
w -leads_to q
by Def21;
A7:
len (w ^ <*s*>) = (len w) + (len <*s*>)
by FINSEQ_1:35;
set qsa =
q,
<*s*> -admissible ;
A8:
(q,<*s*> -admissible ) . 1
= q
by Def2;
A9:
<*s*> . 1
= s
by FINSEQ_1:57;
1
<= len <*s*>
by FINSEQ_1:56;
then A10:
ex
wi being
Element of
IAlph ex
qi,
qi1 being
State of
tfsm st
(
wi = <*s*> . 1 &
qi = (q,<*s*> -admissible ) . 1 &
qi1 = (q,<*s*> -admissible ) . (1 + 1) &
wi -succ_of qi = qi1 )
by Def2;
the
Tran of
tfsm . d = q1
by A2, A4, FUNCT_1:72;
then A11:
(q,<*s*> -admissible ) . (1 + 1) = q1
by A2, A4, A8, A9, A10, MCART_1:23;
A12:
(len (w ^ <*s*>)) + 1 =
((len w) + 1) + 1
by A7, FINSEQ_1:56
.=
(len w) + (1 + 1)
;
1
+ 1
= 2
;
then
( 1
<= 2 & 2
<= (len <*s*>) + 1 )
by FINSEQ_1:56;
then
(the InitS of tfsm,(w ^ <*s*>) -admissible ) . ((len (w ^ <*s*>)) + 1) = q1
by A6, A11, A12, Th22;
then
the
InitS of
tfsm,
w ^ <*s*> -leads_to q1
by Def3;
then
q1 is
accessible
by Def21;
hence
x in accessibleStates tfsm
;
:: thesis: verum
end;
hence
the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum