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