let IAlph, OAlph be non empty set ; for tfsm being non empty Mealy-FSM over 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 over 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 qa, qb be State of tfsm; ( 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 ( ( 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
;
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;
( 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 qa9 = the
Tran of
tfsm . [qa,s];
set qb9 = the
Tran of
tfsm . [qb,s];
len <*s*> = 1
by FINSEQ_1:40;
then A2:
1
in dom <*s*>
by FINSEQ_3:25;
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)]
.=
((qa,<*s*>) -response) . 1
by A2, Def6
.=
((qb,<*s*>) -response) . 1
by A1
.=
the
OFun of
tfsm . [(((qb,<*s*>) -admissible) . 1),(<*s*> . 1)]
by A2, Def6
.=
the
OFun of
tfsm . [(((qb,<*s*>) -admissible) . 1),s]
.=
the
OFun of
tfsm . [qb,s]
by Def2
;
the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] -are_equivalent now for w being FinSequence of IAlph holds (( the Tran of tfsm . [qa,s]),w) -response = (( the Tran of tfsm . [qb,s]),w) -response let w be
FinSequence of
IAlph;
(( the Tran of tfsm . [qa,s]),w) -response = (( the Tran of tfsm . [qb,s]),w) -response A4:
( (
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) )
by Th18;
(
qa,
(<*s*> ^ w))
-response = (
qb,
(<*s*> ^ w))
-response
by A1;
hence
(
( the Tran of tfsm . [qa,s]),
w)
-response = (
( the Tran of tfsm . [qb,s]),
w)
-response
by A3, A4, FINSEQ_1:33;
verum end; hence
the
Tran of
tfsm . [qa,s], the
Tran of
tfsm . [qb,s] -are_equivalent
;
verum
end;
assume A5:
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 )
; qa,qb -are_equivalent
let w be FinSequence of IAlph; FSM_1:def 10 (qa,w) -response = (qb,w) -response
per cases
( w = <*> IAlph or w <> {} )
;
suppose
w <> {}
;
(qa,w) -response = (qb,w) -response then consider s being
Element of
IAlph,
wt being
FinSequence of
IAlph such that
s = w . 1
and A7:
w = <*s*> ^ wt
by FINSEQ_3:102;
set bsresp = the
OFun of
tfsm . [qb,s];
set asresp = the
OFun of
tfsm . [qa,s];
set qb9 = the
Tran of
tfsm . [qb,s];
set qa9 = the
Tran of
tfsm . [qa,s];
the
Tran of
tfsm . [qa,s], the
Tran of
tfsm . [qb,s] -are_equivalent
by A5;
then A8:
(
( the Tran of tfsm . [qa,s]),
wt)
-response = (
( the Tran of tfsm . [qb,s]),
wt)
-response
;
thus (
qa,
w)
-response =
<*( the OFun of tfsm . [qa,s])*> ^ ((( the Tran of tfsm . [qa,s]),wt) -response)
by A7, Th18
.=
<*( the OFun of tfsm . [qb,s])*> ^ ((( the Tran of tfsm . [qb,s]),wt) -response)
by A5, A8
.=
(
qb,
w)
-response
by A7, Th18
;
verum end;