let IAlph, OAlph be non empty set ; :: thesis: for sfsm being non empty finite Moore-FSM of IAlph,OAlph ex tfsm being non empty finite Mealy-FSM of IAlph,OAlph st tfsm is_similar_to sfsm
let sfsm be non empty finite Moore-FSM of IAlph,OAlph; :: thesis: ex tfsm being non empty finite Mealy-FSM of IAlph,OAlph st tfsm is_similar_to sfsm
set S = the carrier of sfsm;
set T = the Tran of sfsm;
set sOF = the OFun of sfsm;
set IS = the InitS of sfsm;
deffunc H1( Element of the carrier of sfsm, Element of IAlph) -> Element of OAlph = the OFun of sfsm . (the Tran of sfsm . [$1,$2]);
consider tOF being Function of [:the carrier of sfsm,IAlph:],OAlph such that
A1: for q being Element of the carrier of sfsm
for s being Element of IAlph holds tOF . q,s = H1(q,s) from BINOP_1:sch 4();
 take tfsm = Mealy-FSM(# the carrier of sfsm,the Tran of sfsm,tOF,the InitS of sfsm #); :: thesis: tfsm is_similar_to sfsm
let tw be FinSequence of IAlph; :: according to FSM_1:def 8 :: thesis: <*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response ) = the InitS of sfsm,tw -response
set tIS = the InitS of tfsm;
set twa = the InitS of tfsm,tw -admissible ;
set swa = the InitS of sfsm,tw -admissible ;
defpred S1[ Element of NAT ] means ( $1 in Seg ((len tw) + 1) implies (the InitS of tfsm,tw -admissible ) . $1 = (the InitS of sfsm,tw -admissible ) . $1 );
A2: S1[ 0 ] by FINSEQ_1:3;
A3: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: ( i in Seg ((len tw) + 1) implies (the InitS of tfsm,tw -admissible ) . i = (the InitS of sfsm,tw -admissible ) . i ) ; :: thesis: S1[i + 1]
assume i + 1 in Seg ((len tw) + 1) ; :: thesis: (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1)
then A5: i + 1 <= (len tw) + 1 by FINSEQ_1:3;
per cases ( i = 0 or ( i > 0 & i <= len tw ) ) by A5, XREAL_1:8;
suppose A6: i = 0 ; :: thesis: (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1)
( (the InitS of tfsm,tw -admissible ) . 1 = the InitS of tfsm & (the InitS of sfsm,tw -admissible ) . 1 = the InitS of sfsm ) by Def2;
hence (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1) by A6; :: thesis: verum
end;
suppose ( i > 0 & i <= len tw ) ; :: thesis: (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1)
then A7: ( 0 + 1 = 1 implies ( 1 <= i & i <= len tw ) ) by NAT_1:13;
then A8: ( 1 <= i & i <= (len tw) + 1 ) by NAT_1:12;
consider twi being Element of IAlph, tqi, tqi1 being Element of tfsm such that
A9: ( twi = tw . i & tqi = (the InitS of tfsm,tw -admissible ) . i & tqi1 = (the InitS of tfsm,tw -admissible ) . (i + 1) & twi -succ_of tqi = tqi1 ) by A7, Def2;
ex swi being Element of IAlph ex sqi, sqi1 being Element of sfsm st
( swi = tw . i & sqi = (the InitS of sfsm,tw -admissible ) . i & sqi1 = (the InitS of sfsm,tw -admissible ) . (i + 1) & swi -succ_of sqi = sqi1 ) by A7, Def2;
hence (the InitS of tfsm,tw -admissible ) . (i + 1) = (the InitS of sfsm,tw -admissible ) . (i + 1) by A4, A8, A9, FINSEQ_1:3; :: thesis: verum
end;
end;
end;
A10: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A2, A3);
now
thus K: len (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) = (len <*(the OFun of sfsm . the InitS of sfsm)*>) + (len (the InitS of tfsm,tw -response )) by FINSEQ_1:35
.= 1 + (len (the InitS of tfsm,tw -response )) by FINSEQ_1:57
.= (len tw) + 1 by Def6 ; :: thesis: ( len (the InitS of sfsm,tw -response ) = (len tw) + 1 & ( for i being Nat st i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) holds
(<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b2 = (the InitS of sfsm,tw -response ) . b2 ) )
thus len (the InitS of sfsm,tw -response ) = (len tw) + 1 by Def7; :: thesis: for i being Nat st i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) holds
(<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b2 = (the InitS of sfsm,tw -response ) . b2
X: dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) = Seg ((len tw) + 1) by K, FINSEQ_1:def 3;
let i be Nat; :: thesis: ( i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) implies (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b1 = (the InitS of sfsm,tw -response ) . b1 )
assume A11: i in dom (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) ; :: thesis: (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b1 = (the InitS of sfsm,tw -response ) . b1
then A12: ( 1 <= i & i <= (len tw) + 1 ) by X, FINSEQ_1:3;
per cases ( i = 1 or 1 < i ) by A12, XXREAL_0:1;
suppose A13: i = 1 ; :: thesis: (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b1 = (the InitS of sfsm,tw -response ) . b1
then i in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
then i in dom <*(the OFun of sfsm . the InitS of sfsm)*> by FINSEQ_1:55;
hence (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . i = <*(the OFun of sfsm . the InitS of sfsm)*> . i by FINSEQ_1:def 7
.= the OFun of sfsm . the InitS of sfsm by A13, FINSEQ_1:57
.= (the InitS of sfsm,tw -response ) . i by A13, Th25 ;
:: thesis: verum
end;
suppose 1 < i ; :: thesis: (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . b1 = (the InitS of sfsm,tw -response ) . b1
then consider j being Element of NAT such that
A14: ( j = i - 1 & 1 <= j ) by INT_1:78;
A15: i = j + 1 by A14;
A16: len <*(the OFun of sfsm . the InitS of sfsm)*> = 1 by FINSEQ_1:57;
A17: j <= len tw by A12, A15, XREAL_1:8;
then A18: j in Seg (len tw) by A14, FINSEQ_1:3;
( 1 <= j & j <= (len tw) + 1 ) by A14, A17, NAT_1:12;
then A19: j in Seg ((len tw) + 1) by FINSEQ_1:3;
len (the InitS of tfsm,tw -response ) = len tw by Def6;
then A20: j in dom (the InitS of tfsm,tw -response ) by A18, FINSEQ_1:def 3;
consider swj being Element of IAlph, swaj, swai being Element of sfsm such that
A21: ( swj = tw . j & swaj = (the InitS of sfsm,tw -admissible ) . j & swai = (the InitS of sfsm,tw -admissible ) . (j + 1) & swj -succ_of swaj = swai ) by A14, A17, Def2;
A22: j in dom tw by A18, FINSEQ_1:def 3;
(<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . i = (the InitS of tfsm,tw -response ) . j by A15, A16, A20, FINSEQ_1:def 7
.= the OFun of tfsm . [((the InitS of tfsm,tw -admissible ) . j),(tw . j)] by A22, Def6
.= tOF . ((the InitS of sfsm,tw -admissible ) . j),(tw . j) by A10, A19
.= the OFun of sfsm . (the Tran of sfsm . swaj,swj) by A1, A21
.= (the InitS of sfsm,tw -response ) . i by A11, A14, A21, Def7, X ;
hence (<*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response )) . i = (the InitS of sfsm,tw -response ) . i ; :: thesis: verum
end;
end;
end;
hence <*(the OFun of sfsm . the InitS of sfsm)*> ^ (the InitS of tfsm,tw -response ) = the InitS of sfsm,tw -response by FINSEQ_2:10; :: thesis: verum