let OAlph, IAlph be non empty set ; for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11, q12 being State of tfsm1
for Tf being Function of the carrier of tfsm1,the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s ) ) holds
( q11,q12 -are_equivalent iff Tf . q11,Tf . q12 -are_equivalent )
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; for q11, q12 being State of tfsm1
for Tf being Function of the carrier of tfsm1,the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s ) ) holds
( q11,q12 -are_equivalent iff Tf . q11,Tf . q12 -are_equivalent )
let q11, q12 be State of tfsm1; for Tf being Function of the carrier of tfsm1,the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s ) ) holds
( q11,q12 -are_equivalent iff Tf . q11,Tf . q12 -are_equivalent )
let Tf be Function of the carrier of tfsm1,the carrier of tfsm2; ( ( for q being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s ) ) implies ( q11,q12 -are_equivalent iff Tf . q11,Tf . q12 -are_equivalent ) )
set Stfsm1 = the carrier of tfsm1;
set Stfsm2 = the carrier of tfsm2;
set OF1 = the OFun of tfsm1;
set OF2 = the OFun of tfsm2;
assume A1:
for q being Element of the carrier of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q,s) = the Tran of tfsm2 . (Tf . q),s & the OFun of tfsm1 . q,s = the OFun of tfsm2 . (Tf . q),s )
; ( q11,q12 -are_equivalent iff Tf . q11,Tf . q12 -are_equivalent )
hereby ( Tf . q11,Tf . q12 -are_equivalent implies q11,q12 -are_equivalent )
reconsider Tq2 =
Tf . q12 as
Element of the
carrier of
tfsm2 ;
reconsider Tq1 =
Tf . q11 as
Element of the
carrier of
tfsm2 ;
assume A2:
q11,
q12 -are_equivalent
;
Tf . q11,Tf . q12 -are_equivalent now let w be
FinSequence of
IAlph;
Tq1,w -response = Tq2,w -response A3:
now let k be
Nat;
( 1 <= k & k <= len (Tq1,w -response ) implies (Tq1,w -response ) . k = (Tq2,w -response ) . k )assume that A4:
1
<= k
and A5:
k <= len (Tq1,w -response )
;
(Tq1,w -response ) . k = (Tq2,w -response ) . k
len (Tq1,w -response ) = len w
by Def6;
then A6:
k in Seg (len w)
by A4, A5, FINSEQ_1:3;
then A7:
k in Seg ((len w) + 1)
by FINSEQ_2:9;
then A8:
k <= (len w) + 1
by FINSEQ_1:3;
len (q11,w -admissible ) = (len w) + 1
by Def2;
then
k in dom (q11,w -admissible )
by A7, FINSEQ_1:def 3;
then reconsider q1a =
(q11,w -admissible ) . k as
Element of the
carrier of
tfsm1 by FINSEQ_2:13;
A9:
k in NAT
by ORDINAL1:def 13;
len (q12,w -admissible ) = (len w) + 1
by Def2;
then
k in dom (q12,w -admissible )
by A7, FINSEQ_1:def 3;
then reconsider q2a =
(q12,w -admissible ) . k as
Element of the
carrier of
tfsm1 by FINSEQ_2:13;
A10:
k in dom w
by A6, FINSEQ_1:def 3;
then reconsider wk =
w . k as
Element of
IAlph by FINSEQ_2:13;
thus (Tq1,w -response ) . k =
the
OFun of
tfsm2 . [((Tq1,w -admissible ) . k),(w . k)]
by A10, Def6
.=
the
OFun of
tfsm2 . (Tf . q1a),
wk
by A1, A4, A8, A9, Th60
.=
the
OFun of
tfsm1 . q1a,
wk
by A1
.=
(q11,w -response ) . k
by A10, Def6
.=
(q12,w -response ) . k
by A2, Def10
.=
the
OFun of
tfsm1 . q2a,
wk
by A10, Def6
.=
the
OFun of
tfsm2 . (Tf . q2a),
wk
by A1
.=
the
OFun of
tfsm2 . [((Tq2,w -admissible ) . k),(w . k)]
by A1, A4, A8, A9, Th60
.=
(Tq2,w -response ) . k
by A10, Def6
;
verum end; len (Tq1,w -response ) =
len w
by Def6
.=
len (Tq2,w -response )
by Def6
;
hence
Tq1,
w -response = Tq2,
w -response
by A3, FINSEQ_1:18;
verum end; hence
Tf . q11,
Tf . q12 -are_equivalent
by Def10;
verum
end;
assume A11:
Tf . q11,Tf . q12 -are_equivalent
; q11,q12 -are_equivalent
now let w be
FinSequence of
IAlph;
q11,w -response = q12,w -response A12:
now let k be
Nat;
( 1 <= k & k <= len (q11,w -response ) implies (q11,w -response ) . k = (q12,w -response ) . k )assume that A13:
1
<= k
and A14:
k <= len (q11,w -response )
;
(q11,w -response ) . k = (q12,w -response ) . k
len (q11,w -response ) = len w
by Def6;
then A15:
k in Seg (len w)
by A13, A14, FINSEQ_1:3;
then A16:
k in Seg ((len w) + 1)
by FINSEQ_2:9;
then A17:
(
k in NAT &
k <= (len w) + 1 )
by FINSEQ_1:3, ORDINAL1:def 13;
len (q12,w -admissible ) = (len w) + 1
by Def2;
then
k in dom (q12,w -admissible )
by A16, FINSEQ_1:def 3;
then reconsider q2a =
(q12,w -admissible ) . k as
Element of the
carrier of
tfsm1 by FINSEQ_2:13;
len (q11,w -admissible ) = (len w) + 1
by Def2;
then
k in dom (q11,w -admissible )
by A16, FINSEQ_1:def 3;
then reconsider q1a =
(q11,w -admissible ) . k as
Element of the
carrier of
tfsm1 by FINSEQ_2:13;
A18:
k in dom w
by A15, FINSEQ_1:def 3;
then reconsider wk =
w . k as
Element of
IAlph by FINSEQ_2:13;
thus (q11,w -response ) . k =
the
OFun of
tfsm1 . ((q11,w -admissible ) . k),
(w . k)
by A18, Def6
.=
the
OFun of
tfsm2 . (Tf . q1a),
wk
by A1
.=
the
OFun of
tfsm2 . [(((Tf . q11),w -admissible ) . k),wk]
by A1, A13, A17, Th60
.=
((Tf . q11),w -response ) . k
by A18, Def6
.=
((Tf . q12),w -response ) . k
by A11, Def10
.=
the
OFun of
tfsm2 . [(((Tf . q12),w -admissible ) . k),(w . k)]
by A18, Def6
.=
the
OFun of
tfsm2 . (Tf . q2a),
wk
by A1, A13, A17, Th60
.=
the
OFun of
tfsm1 . q2a,
(w . k)
by A1
.=
(q12,w -response ) . k
by A18, Def6
;
verum end; len (q11,w -response ) =
len w
by Def6
.=
len (q12,w -response )
by Def6
;
hence
q11,
w -response = q12,
w -response
by A12, FINSEQ_1:18;
verum end;
hence
q11,q12 -are_equivalent
by Def10; verum