let OAlph, IAlph be non empty set ; 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; 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: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
;
the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent now 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 Th35;
qa,
(<*s*> ^ w) -response = qb,
(<*s*> ^ w) -response
by A1, Def10;
hence
(the Tran of tfsm . [qa,s]),
w -response = (the Tran of tfsm . [qb,s]),
w -response
by A3, A4, FINSEQ_1:46;
verum end; hence
the
Tran of
tfsm . [qa,s],the
Tran of
tfsm . [qb,s] -are_equivalent
by Def10;
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:111;
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
by Def10;
thus qa,
w -response =
<*(the OFun of tfsm . [qa,s])*> ^ ((the Tran of tfsm . [qa,s]),wt -response )
by A7, Th35
.=
<*(the OFun of tfsm . [qb,s])*> ^ ((the Tran of tfsm . [qb,s]),wt -response )
by A5, A8
.=
qb,
w -response
by A7, Th35
;
verum end;