let IAlph, OAlph be non empty set ; for tfsm being non empty finite Mealy-FSM over 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 over IAlph,OAlph; 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
by Th48;
then
[:(accessibleStates tfsm),IAlph:] c= [: the carrier of tfsm,IAlph:]
by ZFMISC_1:96;
then
the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:], the carrier of tfsm
by FUNCT_2:32;
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
set I = the
InitS of
tfsm;
let x be
object ;
TARSKI:def 3 ( 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:])
;
x in accessibleStates tfsm
then consider d being
object such that A4:
d in dom ( the Tran of tfsm | [:(accessibleStates tfsm),IAlph:])
and A5:
x = ( the Tran of tfsm | [:(accessibleStates tfsm),IAlph:]) . d
by FUNCT_1:def 3;
A6:
d `1 in accessibleStates tfsm
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 qsa = (
q,
<*s*>)
-admissible ;
A7:
(
((q,<*s*>) -admissible) . 1
= q &
<*s*> . 1
= s )
by Def2, FINSEQ_1:40;
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;
1
<= len <*s*>
by FINSEQ_1:39;
then A8:
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, A5, FUNCT_1:49;
then A9:
((q,<*s*>) -admissible) . (1 + 1) = q1
by A4, A7, A8, MCART_1:21;
1
+ 1
= 2
;
then A10:
2
<= (len <*s*>) + 1
by FINSEQ_1:39;
q is
accessible
by A6, Th48;
then consider w being
FinSequence of
IAlph such that A11:
the
InitS of
tfsm,
w -leads_to q
;
len (w ^ <*s*>) = (len w) + (len <*s*>)
by FINSEQ_1:22;
then (len (w ^ <*s*>)) + 1 =
((len w) + 1) + 1
by FINSEQ_1:39
.=
(len w) + (1 + 1)
;
then
(( the InitS of tfsm,(w ^ <*s*>)) -admissible) . ((len (w ^ <*s*>)) + 1) = q1
by A11, A9, A10, Th7;
then
the
InitS of
tfsm,
w ^ <*s*> -leads_to q1
;
then
q1 is
accessible
;
hence
x in accessibleStates tfsm
;
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:4; verum