let IAlph, OAlph be non empty set ; for tfsm1, tfsm2 being non empty Mealy-FSM over 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 over 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 for w being FinSequence of IAlph holds (Tq1,w) -response = (Tq2,w) -response let w be
FinSequence of
IAlph;
(Tq1,w) -response = (Tq2,w) -response A3:
now for k being Nat st 1 <= k & k <= len ((Tq1,w) -response) holds
((Tq1,w) -response) . k = ((Tq2,w) -response) . klet 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:1;
then A7:
k in Seg ((len w) + 1)
by FINSEQ_2:8;
then A8:
k <= (len w) + 1
by FINSEQ_1:1;
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:11;
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:11;
A9:
k in dom w
by A6, FINSEQ_1:def 3;
then reconsider wk =
w . k as
Element of
IAlph by FINSEQ_2:11;
thus ((Tq1,w) -response) . k =
the
OFun of
tfsm2 . [(((Tq1,w) -admissible) . k),(w . k)]
by A9, Def6
.=
the
OFun of
tfsm2 . (
(Tf . q1a),
wk)
by A1, A4, A8, Th43
.=
the
OFun of
tfsm1 . (
q1a,
wk)
by A1
.=
((q11,w) -response) . k
by A9, Def6
.=
((q12,w) -response) . k
by A2
.=
the
OFun of
tfsm1 . (
q2a,
wk)
by A9, Def6
.=
the
OFun of
tfsm2 . (
(Tf . q2a),
wk)
by A1
.=
the
OFun of
tfsm2 . [(((Tq2,w) -admissible) . k),(w . k)]
by A1, A4, A8, Th43
.=
((Tq2,w) -response) . k
by A9, 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:14;
verum end; hence
Tf . q11,
Tf . q12 -are_equivalent
;
verum
end;
assume A10:
Tf . q11,Tf . q12 -are_equivalent
; q11,q12 -are_equivalent
now for w being FinSequence of IAlph holds (q11,w) -response = (q12,w) -response let w be
FinSequence of
IAlph;
(q11,w) -response = (q12,w) -response A11:
now for k being Nat st 1 <= k & k <= len ((q11,w) -response) holds
((q11,w) -response) . k = ((q12,w) -response) . klet k be
Nat;
( 1 <= k & k <= len ((q11,w) -response) implies ((q11,w) -response) . k = ((q12,w) -response) . k )assume that A12:
1
<= k
and A13:
k <= len ((q11,w) -response)
;
((q11,w) -response) . k = ((q12,w) -response) . k
len ((q11,w) -response) = len w
by Def6;
then A14:
k in Seg (len w)
by A12, A13, FINSEQ_1:1;
then A15:
k in Seg ((len w) + 1)
by FINSEQ_2:8;
then A16:
(
k in NAT &
k <= (len w) + 1 )
by FINSEQ_1:1;
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:11;
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:11;
A17:
k in dom w
by A14, FINSEQ_1:def 3;
then reconsider wk =
w . k as
Element of
IAlph by FINSEQ_2:11;
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, A12, A16, Th43
.=
(((Tf . q11),w) -response) . k
by A17, Def6
.=
(((Tf . q12),w) -response) . k
by A10
.=
the
OFun of
tfsm2 . [((((Tf . q12),w) -admissible) . k),(w . k)]
by A17, Def6
.=
the
OFun of
tfsm2 . (
(Tf . q2a),
wk)
by A1, A12, A16, Th43
.=
the
OFun of
tfsm1 . (
q2a,
(w . k))
by A1
.=
((q12,w) -response) . k
by A17, 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 A11, FINSEQ_1:14;
verum end;
hence
q11,q12 -are_equivalent
; verum