let OAlph, IAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm holds
( qa,qb -are_equivalent iff for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent ) )
let tfsm be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for qa, qb being State of tfsm holds
( qa,qb -are_equivalent iff for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent ) )
let qa, qb be State of tfsm; :: thesis: ( qa,qb -are_equivalent iff for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent ) )
set OF = the OFun of tfsm;
hereby :: thesis: ( ( for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent ) ) implies qa,qb -are_equivalent )
assume A1:
qa,
qb -are_equivalent
;
:: thesis: for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent )let s be
Element of
IAlph;
:: thesis: ( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent )
len <*s*> = 1
by FINSEQ_1:57;
then A2:
1
in dom <*s*>
by FINSEQ_3:27;
thus A3: the
OFun of
tfsm . [qa,s] =
the
OFun of
tfsm . [((qa,<*s*> -admissible ) . 1),s]
by Def2
.=
the
OFun of
tfsm . [((qa,<*s*> -admissible ) . 1),(<*s*> . 1)]
by FINSEQ_1:57
.=
(qa,<*s*> -response ) . 1
by A2, Def6
.=
(qb,<*s*> -response ) . 1
by A1, Def10
.=
the
OFun of
tfsm . [((qb,<*s*> -admissible ) . 1),(<*s*> . 1)]
by A2, Def6
.=
the
OFun of
tfsm . [((qb,<*s*> -admissible ) . 1),s]
by FINSEQ_1:57
.=
the
OFun of
tfsm . [qb,s]
by Def2
;
:: thesis: the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent set qa' = the
Tran of
tfsm . [qa,s];
set qb' = the
Tran of
tfsm . [qb,s];
now let w be
FinSequence of
IAlph;
:: thesis: (the Tran of tfsm . [qa,s]),w -response = (the Tran of tfsm . [qb,s]),w -response
(
qa,
(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ ((the Tran of tfsm . [qa,s]),w -response ) &
qb,
(<*s*> ^ w) -response = <*(the OFun of tfsm . [qb,s])*> ^ ((the Tran of tfsm . [qb,s]),w -response ) &
qa,
(<*s*> ^ w) -response = qb,
(<*s*> ^ w) -response )
by A1, Def10, Th35;
hence
(the Tran of tfsm . [qa,s]),
w -response = (the Tran of tfsm . [qb,s]),
w -response
by A3, FINSEQ_1:46;
:: thesis: verum end; hence
the
Tran of
tfsm . [qa,s],the
Tran of
tfsm . [qb,s] -are_equivalent
by Def10;
:: thesis: verum
end;
assume A4:
for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent )
; :: thesis: qa,qb -are_equivalent
let w be FinSequence of IAlph; :: according to FSM_1:def 10 :: thesis: qa,w -response = qb,w -response
per cases
( w = <*> IAlph or w <> {} )
;
suppose
w <> {}
;
:: thesis: qa,w -response = qb,w -response then consider s being
Element of
IAlph,
wt being
FinSequence of
IAlph such that A6:
(
s = w . 1 &
w = <*s*> ^ wt )
by FINSEQ_3:111;
set qa' = the
Tran of
tfsm . [qa,s];
set qb' = the
Tran of
tfsm . [qb,s];
the
Tran of
tfsm . [qa,s],the
Tran of
tfsm . [qb,s] -are_equivalent
by A4;
then A7:
(the Tran of tfsm . [qa,s]),
wt -response = (the Tran of tfsm . [qb,s]),
wt -response
by Def10;
set asresp = the
OFun of
tfsm . [qa,s];
set bsresp = the
OFun of
tfsm . [qb,s];
thus qa,
w -response =
<*(the OFun of tfsm . [qa,s])*> ^ ((the Tran of tfsm . [qa,s]),wt -response )
by A6, Th35
.=
<*(the OFun of tfsm . [qb,s])*> ^ ((the Tran of tfsm . [qb,s]),wt -response )
by A4, A7
.=
qb,
w -response
by A6, Th35
;
:: thesis: verum end;