let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for cTran being Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: for cTran being Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
set M = tfsm;
let cTran be Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm); :: thesis: for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let cOFun be Function of [:(accessibleStates tfsm),IAlph:],OAlph; :: thesis: for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let cInitS be Element of accessibleStates tfsm; :: thesis: ( cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm implies tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent )
assume that
A1: cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] and
A2: cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] and
A3: cInitS = the InitS of tfsm ; :: thesis: tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
let w be FinSequence of IAlph; :: according to FSM_1:def 9 :: thesis: ( the InitS of tfsm,w) -response = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response
set cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #);
set ma = ( the InitS of tfsm,w) -admissible ;
set cma = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible ;
set mr = ( the InitS of tfsm,w) -response ;
set cmr = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response ;

A4: now :: thesis: ( len (( the InitS of tfsm,w) -admissible) = (len w) + 1 & len (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) = (len w) + 1 & ( for j being Nat holds S₁[j] ) )

defpred S₁[ Nat] means ( $1 in dom (( the InitS of tfsm,w) -admissible) implies (( the InitS of tfsm,w) -admissible) . $1 = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . $1 );
thus ( len (( the InitS of tfsm,w) -admissible) = (len w) + 1 & len (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) = (len w) + 1 ) by Def2; :: thesis: for j being Nat holds S₁[j]
then A5: dom (( the InitS of tfsm,w) -admissible) = Seg ((len w) + 1) by FINSEQ_1:def 3;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A7: ( j in dom (( the InitS of tfsm,w) -admissible) implies (( the InitS of tfsm,w) -admissible) . j = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . j ) ; :: thesis: S₁[j + 1]
A8: ( 0 = j or ( 0 < j & 0 + 1 = 1 ) ) ;
assume j + 1 in dom (( the InitS of tfsm,w) -admissible) ; :: thesis: (( the InitS of tfsm,w) -admissible) . (j + 1) = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . (j + 1)
then A9: j + 1 <= (len w) + 1 by A5, FINSEQ_1:1;
then A10: j <= len w by XREAL_1:6;
A11: j < (len w) + 1 by A9, NAT_1:13;

per cases ( 0 = j or 1 <= j ) by A8, NAT_1:13;

suppose A12: 0 = j ; :: thesis: (( the InitS of tfsm,w) -admissible) . (j + 1) = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . (j + 1)

hence (( the InitS of tfsm,w) -admissible) . (j + 1) = the InitS of tfsm by Def2
.= (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . (j + 1) by A3, A12, Def2 ;
:: thesis: verum

end;

suppose A13: 1 <= j ; :: thesis: (( the InitS of tfsm,w) -admissible) . (j + 1) = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . (j + 1)

then ( ex mwj being Element of IAlph ex mqj, mqj1 being State of tfsm st
( mwj = w . j & mqj = (( the InitS of tfsm,w) -admissible) . j & mqj1 = (( the InitS of tfsm,w) -admissible) . (j + 1) & mwj -succ_of mqj = mqj1 ) & ex cmwj being Element of IAlph ex cmqj, cmqj1 being State of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) st
( cmwj = w . j & cmqj = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . j & cmqj1 = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . (j + 1) & cmwj -succ_of cmqj = cmqj1 ) ) by A10, Def2;
hence (( the InitS of tfsm,w) -admissible) . (j + 1) = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . (j + 1) by A1, A5, A7, A11, A13, FINSEQ_1:1, FUNCT_1:49; :: thesis: verum

end;

end;

end;

A14: S₁[ 0 ] by A5, FINSEQ_1:1;
thus for j being Nat holds S₁[j] from NAT_1:sch 2(A14, A6); :: thesis: verum

end;

then A15: ( the InitS of tfsm,w) -admissible = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible by FINSEQ_2:9;

now :: thesis: ( len (( the InitS of tfsm,w) -response) = len w & len (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) = len w & ( for j being Nat st j in dom (( the InitS of tfsm,w) -response) holds
(( the InitS of tfsm,w) -response) . j = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) . j ) )

thus ( len (( the InitS of tfsm,w) -response) = len w & len (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) = len w ) by Def6; :: thesis: for j being Nat st j in dom (( the InitS of tfsm,w) -response) holds
(( the InitS of tfsm,w) -response) . j = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) . j
then A16: dom (( the InitS of tfsm,w) -response) = Seg (len w) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in dom (( the InitS of tfsm,w) -response) implies (( the InitS of tfsm,w) -response) . j = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) . j )
assume A17: j in dom (( the InitS of tfsm,w) -response) ; :: thesis: (( the InitS of tfsm,w) -response) . j = (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) . j
then A18: j in dom w by A16, FINSEQ_1:def 3;
j in Seg ((len w) + 1) by A16, A17, FINSEQ_2:8;
then j in dom (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) by A4, FINSEQ_1:def 3;
then A19: (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . j in accessibleStates tfsm by FINSEQ_2:11;
w . j in IAlph by A18, FINSEQ_2:11;
then A20: [((( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . j),(w . j)] in [:(accessibleStates tfsm),IAlph:] by A19, ZFMISC_1:87;
thus (( the InitS of tfsm,w) -response) . j = the OFun of tfsm . [((( the InitS of tfsm,w) -admissible) . j),(w . j)] by A18, Def6
.= cOFun . [((( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . j),(w . j)] by A2, A15, A20, FUNCT_1:49
.= (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response) . j by A18, Def6 ; :: thesis: verum

end;

hence ( the InitS of tfsm,w) -response = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -response by FINSEQ_2:9; :: thesis: verum