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