let IAlph, OAlph be non empty set ; for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic holds
tfsm1,tfsm2 -are_equivalent
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph; ( tfsm1,tfsm2 -are_isomorphic implies tfsm1,tfsm2 -are_equivalent )
assume
tfsm1,tfsm2 -are_isomorphic
; tfsm1,tfsm2 -are_equivalent
then consider Tf being Function of the carrier of tfsm1, the carrier of tfsm2 such that
Tf is bijective
and
A1:
Tf . the InitS of tfsm1 = the InitS of tfsm2
and
A2:
for q being Element 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) )
;
now for w1 being FinSequence of IAlph holds ( the InitS of tfsm1,w1) -response = ( the InitS of tfsm2,w1) -response let w1 be
FinSequence of
IAlph;
( the InitS of tfsm1,w1) -response = ( the InitS of tfsm2,w1) -response set rw1 = ( the
InitS of
tfsm1,
w1)
-response ;
set rw2 = ( the
InitS of
tfsm2,
w1)
-response ;
set aw1 = ( the
InitS of
tfsm1,
w1)
-admissible ;
set aw2 = ( the
InitS of
tfsm2,
w1)
-admissible ;
A3:
for
k being
Nat st 1
<= k &
k <= (len w1) + 1 holds
Tf . ((( the InitS of tfsm1,w1) -admissible) . k) = (( the InitS of tfsm2,w1) -admissible) . k
proof
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= (len w1) + 1 implies
Tf . ((( the InitS of tfsm1,w1) -admissible) . $1) = (( the InitS of tfsm2,w1) -admissible) . $1 );
A4:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
( 1
<= k &
k <= (len w1) + 1 implies
Tf . ((( the InitS of tfsm1,w1) -admissible) . k) = (( the InitS of tfsm2,w1) -admissible) . k )
;
S1[k + 1]
assume that
1
<= k + 1
and A6:
k + 1
<= (len w1) + 1
;
Tf . ((( the InitS of tfsm1,w1) -admissible) . (k + 1)) = (( the InitS of tfsm2,w1) -admissible) . (k + 1)
A7:
(
0 = k or (
0 < k &
0 + 1
= 1 ) )
;
per cases
( 0 = k or 1 <= k )
by A7, NAT_1:13;
suppose A9:
1
<= k
;
Tf . ((( the InitS of tfsm1,w1) -admissible) . (k + 1)) = (( the InitS of tfsm2,w1) -admissible) . (k + 1)A10:
len w1 <= (len w1) + 1
by NAT_1:11;
A11:
k <= len w1
by A6, XREAL_1:6;
then consider w1k being
Element of
IAlph,
qk,
qk1 being
Element of
tfsm1 such that A12:
(
w1k = w1 . k &
qk = (( the InitS of tfsm1,w1) -admissible) . k )
and A13:
(
qk1 = (( the InitS of tfsm1,w1) -admissible) . (k + 1) &
w1k -succ_of qk = qk1 )
by A9, Def2;
consider w2k being
Element of
IAlph,
q2k,
q2k1 being
Element of
tfsm2 such that A14:
(
w2k = w1 . k &
q2k = (( the InitS of tfsm2,w1) -admissible) . k )
and A15:
(
q2k1 = (( the InitS of tfsm2,w1) -admissible) . (k + 1) &
w2k -succ_of q2k = q2k1 )
by A9, A11, Def2;
thus Tf . ((( the InitS of tfsm1,w1) -admissible) . (k + 1)) =
Tf . ( the Tran of tfsm1 . (qk,w1k))
by A13
.=
the
Tran of
tfsm2 . (
q2k,
w2k)
by A2, A5, A9, A11, A12, A14, A10, XXREAL_0:2
.=
(( the InitS of tfsm2,w1) -admissible) . (k + 1)
by A15
;
verum end;
end;
A16:
S1[
0 ]
;
thus
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A16, A4); verum
end; A17:
now for k being Nat st 1 <= k & k <= len (( the InitS of tfsm1,w1) -response) holds
(( the InitS of tfsm2,w1) -response) . k = (( the InitS of tfsm1,w1) -response) . klet k be
Nat;
( 1 <= k & k <= len (( the InitS of tfsm1,w1) -response) implies (( the InitS of tfsm2,w1) -response) . k = (( the InitS of tfsm1,w1) -response) . k )assume that A18:
1
<= k
and A19:
k <= len (( the InitS of tfsm1,w1) -response)
;
(( the InitS of tfsm2,w1) -response) . k = (( the InitS of tfsm1,w1) -response) . k
k <= len w1
by A19, Def6;
then A20:
k in dom w1
by A18, FINSEQ_3:25;
then A21:
w1 . k is
Element of
IAlph
by FINSEQ_2:11;
k in Seg (len w1)
by A20, FINSEQ_1:def 3;
then
k in Seg ((len w1) + 1)
by FINSEQ_2:8;
then
k in Seg (len (( the InitS of tfsm1,w1) -admissible))
by Def2;
then A22:
k in dom (( the InitS of tfsm1,w1) -admissible)
by FINSEQ_1:def 3;
then A23:
1
<= k
by FINSEQ_3:25;
k <= len (( the InitS of tfsm1,w1) -admissible)
by A22, FINSEQ_3:25;
then A24:
k <= (len w1) + 1
by Def2;
A25:
(( the InitS of tfsm1,w1) -admissible) . k is
Element of
tfsm1
by A22, FINSEQ_2:11;
thus (( the InitS of tfsm2,w1) -response) . k =
the
OFun of
tfsm2 . [((( the InitS of tfsm2,w1) -admissible) . k),(w1 . k)]
by A20, Def6
.=
the
OFun of
tfsm2 . (
(Tf . ((( the InitS of tfsm1,w1) -admissible) . k)),
(w1 . k))
by A3, A23, A24
.=
the
OFun of
tfsm1 . (
((( the InitS of tfsm1,w1) -admissible) . k),
(w1 . k))
by A2, A25, A21
.=
(( the InitS of tfsm1,w1) -response) . k
by A20, Def6
;
verum end; len (( the InitS of tfsm1,w1) -response) =
len w1
by Def6
.=
len (( the InitS of tfsm2,w1) -response)
by Def6
;
hence
( the
InitS of
tfsm1,
w1)
-response = ( the
InitS of
tfsm2,
w1)
-response
by A17, FINSEQ_1:14;
verum end;
hence
tfsm1,tfsm2 -are_equivalent
; verum