let IAlph be non empty set ; :: thesis: for OAlphf being non empty finite set
for tfsmf being non empty finite Mealy-FSM over IAlph,OAlphf ex sfsmf being non empty finite Moore-FSM over IAlph,OAlphf st tfsmf is_similar_to sfsmf
let OAlphf be non empty finite set ; :: thesis: for tfsmf being non empty finite Mealy-FSM over IAlph,OAlphf ex sfsmf being non empty finite Moore-FSM over IAlph,OAlphf st tfsmf is_similar_to sfsmf
let tfsmf be non empty finite Mealy-FSM over IAlph,OAlphf; :: thesis: ex sfsmf being non empty finite Moore-FSM over 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 H₁( 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) = H₁(q,s) from BINOP_1:sch 4();
set sSs = [: the carrier of tfsmf,OAlphf:];
set sTs = sT;
set r0 = the Element of OAlphf;
deffunc H₂( 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) = H₂(q,r) from BINOP_1:sch 4();
set sI = [ the InitS of tfsmf, the Element of OAlphf];
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, the Element of OAlphf] #) as non empty finite Moore-FSM over IAlph,OAlphf ;
take sfsmf ; :: thesis: tfsmf is_similar_to sfsmf
reconsider SI = [ the InitS of tfsmf, the Element of OAlphf] 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 S₁[ 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 S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[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:1;

per cases ( i = 0 or ( i > 0 & i <= len tw ) ) by A5, XREAL_1:6;

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, the Element of OAlphf] `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;
A13: [( the Tran of tfsmf . [(sqi `1),swi]),( the OFun of tfsmf . [(sqi `1),swi])] `1 = the Tran of tfsmf . [(sqi `1),swi] ;
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:1, A13; :: thesis: verum

end;

end;

end;

A14: S₁[ 0 ] by FINSEQ_1:1;
A15: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A14, A3);

now :: thesis: ( len (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) = (len tw) + 1 & len ((SI,tw) -response) = (len tw) + 1 & ( for i being Nat st i in dom (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) holds
(<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . i = ((SI,tw) -response) . i ) )

thus len (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) = (len <*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*>) + (len (( the InitS of tfsmf,tw) -response)) by FINSEQ_1:22
.= 1 + (len (( the InitS of tfsmf,tw) -response)) by FINSEQ_1:40
.= (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, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) holds
(<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . b₂ = ((SI,tw) -response) . b₂ ) )
then A16: dom (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( 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, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) holds
(<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . b₂ = ((SI,tw) -response) . b₂
let i be Nat; :: thesis: ( i in dom (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) implies (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . b₁ = ((SI,tw) -response) . b₁ )
assume A17: i in dom (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) ; :: thesis: (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . b₁ = ((SI,tw) -response) . b₁
then A18: 1 <= i by A16, FINSEQ_1:1;
A19: i <= (len tw) + 1 by A16, A17, FINSEQ_1:1;

per cases ( i = 1 or 1 < i ) by A18, XXREAL_0:1;

suppose A20: i = 1 ; :: thesis: (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . b₁ = ((SI,tw) -response) . b₁

then i in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then i in dom <*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> by FINSEQ_1:38;
hence (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . i = <*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> . i by FINSEQ_1:def 7
.= sOF . [ the InitS of tfsmf, the Element of OAlphf] by A20, FINSEQ_1:40
.= ((SI,tw) -response) . i by A20, Th10 ;
:: thesis: verum

end;

suppose 1 < i ; :: thesis: (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . b₁ = ((SI,tw) -response) . b₁

then consider j being Element of NAT such that
A21: j = i - 1 and
A22: 1 <= j by INT_1:51;
A23: i = j + 1 by A21;
then A24: j <= len tw by A19, XREAL_1:6;
then consider swj being Element of IAlph, swaj, swai being Element of sfsmf such that
A25: swj = tw . j and
A26: swaj = (( the InitS of sfsmf,tw) -admissible) . j and
A27: ( swai = (( the InitS of sfsmf,tw) -admissible) . (j + 1) & swj -succ_of swaj = swai ) by A22, Def2;
j <= (len tw) + 1 by A24, NAT_1:12;
then A28: j in Seg ((len tw) + 1) by A22, FINSEQ_1:1;
reconsider swaj = swaj as Element of [: the carrier of tfsmf,OAlphf:] ;
A29: j in Seg (len tw) by A22, A24, FINSEQ_1:1;
then A30: 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, the Element of OAlphf])*> = 1 & j in dom (( the InitS of tfsmf,tw) -response) ) by A29, FINSEQ_1:40, FINSEQ_1:def 3;
hence (<*(sOF . [ the InitS of tfsmf, the Element of OAlphf])*> ^ (( the InitS of tfsmf,tw) -response)) . i = (( the InitS of tfsmf,tw) -response) . j by A23, FINSEQ_1:def 7
.= the OFun of tfsmf . (((( the InitS of tfsmf,tw) -admissible) . j),(tw . j)) by A30, Def6
.= the OFun of tfsmf . ((swaj `1),(tw . j)) by A15, A28, A26
.= sOF . (( the Tran of tfsmf . ((swaj `1),swj)),( the OFun of tfsmf . ((swaj `1),swj))) by A2, A25
.= sOF . (sT . (swaj,swj)) by A1
.= ((SI,tw) -response) . i by A16, A17, A21, A27, 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:9; :: thesis: verum

end;