let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph ex Ctfsm being non empty finite connected Mealy-FSM over IAlph,OAlph st
( the Tran of Ctfsm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm,Ctfsm -are_equivalent )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: ex Ctfsm being non empty finite connected Mealy-FSM over IAlph,OAlph st
( the Tran of Ctfsm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm,Ctfsm -are_equivalent )
set M = tfsm;
set I = the InitS of tfsm;
accessibleStates tfsm c= the carrier of tfsm by Th48;
then [:(accessibleStates tfsm),IAlph:] c= [: the carrier of tfsm,IAlph:] by ZFMISC_1:96;
then reconsider cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] as Function of [:(accessibleStates tfsm),IAlph:],OAlph by FUNCT_2:32;
the InitS of tfsm, <*> IAlph -leads_to the InitS of tfsm by Th2;
then the InitS of tfsm is accessible ;
then reconsider cInitS = the InitS of tfsm as Element of accessibleStates tfsm by Th48;
reconsider cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] as Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm) by Th49;
set cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #);
A1: now :: thesis: for w being FinSequence of IAlph holds ( the InitS of tfsm,w) -admissible = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible
let w be FinSequence of IAlph; :: thesis: ( the InitS of tfsm,w) -admissible = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible
set ma = ( the InitS of tfsm,w) -admissible ;
set cma = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible ;
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 S1[j] ) )
defpred S1[ 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 S1[j]
then A2: dom (( the InitS of tfsm,w) -admissible) = Seg ((len w) + 1) by FINSEQ_1:def 3;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let j be Nat; :: thesis: ( S1[j] implies S1[j + 1] )
assume A4: ( 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: S1[j + 1]
A5: ( 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 A6: j + 1 <= (len w) + 1 by A2, FINSEQ_1:1;
then A7: j <= len w by XREAL_1:6;
A8: j < (len w) + 1 by A6, NAT_1:13;
per cases ( 0 = j or 1 <= j ) by A5, NAT_1:13;
suppose A9: 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 A9, Def2 ;
:: thesis: verum
end;
suppose A10: 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 A7, 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 A2, A4, A8, A10, FINSEQ_1:1, FUNCT_1:49; :: thesis: verum
end;
end;
end;
A11: S1[ 0 ] by A2, FINSEQ_1:1;
thus for j being Nat holds S1[j] from NAT_1:sch 2(A11, A3); :: thesis: verum
end;
hence ( the InitS of tfsm,w) -admissible = ( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible by FINSEQ_2:9; :: thesis: verum
end;
now :: thesis: for q being State of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) holds q is accessible
let q be State of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #); :: thesis: q is accessible
( q in accessibleStates tfsm & accessibleStates tfsm c= the carrier of tfsm ) by Th48;
then reconsider q9 = q as State of tfsm ;
q9 is accessible by Th48;
then consider w being FinSequence of IAlph such that
A12: the InitS of tfsm,w -leads_to q9 ;
(( the InitS of tfsm,w) -admissible) . ((len w) + 1) = q9 by A12;
then (( the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w) -admissible) . ((len w) + 1) = q by A1;
then the InitS of Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #),w -leads_to q ;
hence q is accessible ; :: thesis: verum
end;
then reconsider cm = Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) as non empty finite connected Mealy-FSM over IAlph,OAlph by Def22;
take cm ; :: thesis: ( the Tran of cm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] & the OFun of cm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of cm = the InitS of tfsm & tfsm,cm -are_equivalent )
thus the Tran of cm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] ; :: thesis: ( the OFun of cm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of cm = the InitS of tfsm & tfsm,cm -are_equivalent )
thus the OFun of cm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] ; :: thesis: ( the InitS of cm = the InitS of tfsm & tfsm,cm -are_equivalent )
thus the InitS of cm = the InitS of tfsm ; :: thesis: tfsm,cm -are_equivalent
let w be FinSequence of IAlph; :: according to FSM_1:def 9 :: thesis: ( the InitS of tfsm,w) -response = ( the InitS of cm,w) -response
set ma = ( the InitS of tfsm,w) -admissible ;
set cma = ( the InitS of cm,w) -admissible ;
set mr = ( the InitS of tfsm,w) -response ;
set cmr = ( the InitS of cm,w) -response ;
A13: len (( the InitS of cm,w) -admissible) = (len w) + 1 by Def2;
now :: thesis: ( len (( the InitS of tfsm,w) -response) = len w & len (( the InitS of cm,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 cm,w) -response) . j ) )
thus ( len (( the InitS of tfsm,w) -response) = len w & len (( the InitS of cm,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 cm,w) -response) . j
then A14: 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 cm,w) -response) . j )
assume A15: j in dom (( the InitS of tfsm,w) -response) ; :: thesis: (( the InitS of tfsm,w) -response) . j = (( the InitS of cm,w) -response) . j
then A16: j in dom w by A14, FINSEQ_1:def 3;
j in Seg ((len w) + 1) by A14, A15, FINSEQ_2:8;
then j in dom (( the InitS of cm,w) -admissible) by A13, FINSEQ_1:def 3;
then A17: (( the InitS of cm,w) -admissible) . j in accessibleStates tfsm by FINSEQ_2:11;
w . j in IAlph by A16, FINSEQ_2:11;
then A18: [((( the InitS of cm,w) -admissible) . j),(w . j)] in [:(accessibleStates tfsm),IAlph:] by A17, ZFMISC_1:87;
A19: [((( the InitS of tfsm,w) -admissible) . j),(w . j)] = [((( the InitS of cm,w) -admissible) . j),(w . j)] by A1;
thus (( the InitS of tfsm,w) -response) . j = the OFun of tfsm . [((( the InitS of tfsm,w) -admissible) . j),(w . j)] by A16, Def6
.= cOFun . [((( the InitS of cm,w) -admissible) . j),(w . j)] by A19, A18, FUNCT_1:49
.= (( the InitS of cm,w) -response) . j by A16, Def6 ; :: thesis: verum
end;
hence ( the InitS of tfsm,w) -response = ( the InitS of cm,w) -response by FINSEQ_2:9; :: thesis: verum