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();
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();
consider r0 being Element of OAlphf;
set sSs = [:the carrier of tfsmf,OAlphf:];
set sTs = sT;
reconsider sOFs = sOF as Function of [:the carrier of tfsmf,OAlphf:],OAlphf ;
set sI = [the InitS of tfsmf,r0];
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: verumproof
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:
S1[
0 ]
by FINSEQ_1:3;
A4:
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 A5:
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 A6:
i + 1
<= (len tw) + 1
by FINSEQ_1:3;
per cases
( i = 0 or ( i > 0 & i <= len tw ) )
by A6, XREAL_1:8;
suppose
(
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:
(
0 + 1
= 1 implies ( 1
<= i &
i <= len tw ) )
by NAT_1:13;
then A9:
( 1
<= i &
i <= (len tw) + 1 )
by NAT_1:12;
consider twi being
Element of
IAlph,
tqi,
tqi1 being
Element of
tfsmf such that A10:
(
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 A8, 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) &
swi -succ_of sqi = sqi1 )
by A8, Def2;
sqi1 =
sT . sqi,
swi
by A11
.=
[(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 A5, A9, A10, A11, FINSEQ_1:3, MCART_1:def 1;
:: thesis: verum end;
end;
A12:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A3, A4);
now thus K:
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 ) )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 ) . b2X:
dom (<*(sOF . [the InitS of tfsmf,r0])*> ^ (the InitS of tfsmf,tw -response )) = Seg ((len tw) + 1)
by K, FINSEQ_1:def 3;
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 A13:
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 ) . b1then A14:
( 1
<= i &
i <= (len tw) + 1 )
by X, FINSEQ_1:3;
per cases
( i = 1 or 1 < i )
by A14, XXREAL_0:1;
suppose
1
< i
;
:: thesis: (<*(sOF . [the InitS of tfsmf,r0])*> ^ (the InitS of tfsmf,tw -response )) . b1 = (SI,tw -response ) . b1then consider j being
Element of
NAT such that A16:
(
j = i - 1 & 1
<= j )
by INT_1:78;
A17:
i = j + 1
by A16;
A18:
len <*(sOF . [the InitS of tfsmf,r0])*> = 1
by FINSEQ_1:57;
A19:
j <= len tw
by A14, A17, XREAL_1:8;
then A20:
j in Seg (len tw)
by A16, FINSEQ_1:3;
j <= (len tw) + 1
by A19, NAT_1:12;
then A21:
j in Seg ((len tw) + 1)
by A16, FINSEQ_1:3;
len (the InitS of tfsmf,tw -response ) = len tw
by Def6;
then A22:
j in dom (the InitS of tfsmf,tw -response )
by A20, FINSEQ_1:def 3;
consider swj being
Element of
IAlph,
swaj,
swai being
Element of
sfsmf such that A23:
(
swj = tw . j &
swaj = (the InitS of sfsmf,tw -admissible ) . j &
swai = (the InitS of sfsmf,tw -admissible ) . (j + 1) &
swj -succ_of swaj = swai )
by A16, A19, Def2;
reconsider swaj =
swaj as
Element of
[:the carrier of tfsmf,OAlphf:] ;
A24:
j in dom tw
by A20, FINSEQ_1:def 3;
thus (<*(sOF . [the InitS of tfsmf,r0])*> ^ (the InitS of tfsmf,tw -response )) . i =
(the InitS of tfsmf,tw -response ) . j
by A17, A18, A22, FINSEQ_1:def 7
.=
the
OFun of
tfsmf . ((the InitS of tfsmf,tw -admissible ) . j),
(tw . j)
by A24, Def6
.=
the
OFun of
tfsmf . (swaj `1 ),
(tw . j)
by A12, A21, A23
.=
sOF . (the Tran of tfsmf . (swaj `1 ),swj),
(the OFun of tfsmf . (swaj `1 ),swj)
by A2, A23
.=
sOF . (sT . swaj,swj)
by A1
.=
(SI,tw -response ) . i
by A13, A16, A23, Def7, X
;
:: thesis: verum 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;