let IAlph, OAlph be non empty set ; :: thesis: 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; :: thesis: ( tfsm1,tfsm2 -are_isomorphic implies tfsm1,tfsm2 -are_equivalent )
assume tfsm1,tfsm2 -are_isomorphic ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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 S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[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 ) ; :: thesis: S₁[k + 1]
assume that
1 <= k + 1 and
A6: k + 1 <= (len w1) + 1 ; :: thesis: 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 A8: 0 = k ; :: thesis: Tf . ((( the InitS of tfsm1,w1) -admissible) . (k + 1)) = (( the InitS of tfsm2,w1) -admissible) . (k + 1)

hence Tf . ((( the InitS of tfsm1,w1) -admissible) . (k + 1)) = the InitS of tfsm2 by A1, Def2
.= (( the InitS of tfsm2,w1) -admissible) . (k + 1) by A8, Def2 ;
:: thesis: verum

end;

suppose A9: 1 <= k ; :: thesis: 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 ; :: thesis: verum

end;

end;

end;

A16: S₁[ 0 ] ;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A16, A4); :: thesis: verum

end;

A17: now :: thesis: 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) . k

let k be Nat; :: thesis: ( 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) ; :: thesis: (( 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 ; :: thesis: 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; :: thesis: verum

end;

hence tfsm1,tfsm2 -are_equivalent ; :: thesis: verum