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₁[ 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 Nat st S₁[i] holds
S₁[i + 1]

proof

let i be 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;
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; :: thesis: verum

end;

end;

end;

A13: S₁[ 0 ] by FINSEQ_1:1;
A14: for i being Nat holds S₁[i] from NAT_1:sch 2(A13, 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 A15: 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 A16: 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 A17: 1 <= i by A15, FINSEQ_1:1;
A18: i <= (len tw) + 1 by A15, A16, FINSEQ_1:1;

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

suppose A19: 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 A19
.= ((SI,tw) -response) . i by A19, 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
A20: j = i - 1 and
A21: 1 <= j by INT_1:51;
A22: i = j + 1 by A20;
then A23: j <= len tw by A18, XREAL_1:6;
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:1;
reconsider swaj = swaj as Element of [: the carrier of tfsmf,OAlphf:] ;
A28: j in Seg (len tw) by A21, A23, FINSEQ_1:1;
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, the Element of OAlphf])*> = 1 & j in dom (( the InitS of tfsmf,tw) -response) ) by A28, 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 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:9; :: thesis: verum

end;