set part = final_states_partition tfsm;
reconsider m = card the carrier of tfsm as Nat ;
set TR = the Tran of tfsm;
consider n being Nat such that
A1:
m = n + 1
by NAT_1:6;
reconsider n = n as Nat ;
set IS = Class ((n -eq_states_EqR tfsm), the InitS of tfsm);
final_states_partition tfsm = n -eq_states_partition tfsm
by A1, Th39;
then reconsider IS = Class ((n -eq_states_EqR tfsm), the InitS of tfsm) as Element of final_states_partition tfsm by EQREL_1:def 3;
deffunc H1( Element of final_states_partition tfsm, Element of IAlph) -> Element of final_states_partition tfsm = ($2,$1) -succ_class ;
consider Trf being Function of [:(final_states_partition tfsm),IAlph:],(final_states_partition tfsm) such that
A2:
for q being Element of final_states_partition tfsm
for i being Element of IAlph holds Trf . (q,i) = H1(q,i)
from BINOP_1:sch 4();
deffunc H2( Element of final_states_partition tfsm, Element of IAlph) -> Element of OAlph = ($1,$2) -class_response ;
consider OF being Function of [:(final_states_partition tfsm),IAlph:],OAlph such that
A3:
for q being Element of final_states_partition tfsm
for i being Element of IAlph holds OF . (q,i) = H2(q,i)
from BINOP_1:sch 4();
take IT = Mealy-FSM(# (final_states_partition tfsm),Trf,OF,IS #); ( the carrier of IT = final_states_partition tfsm & ( for Q being State of IT
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of IT . (Q,s) & the OFun of tfsm . (q,s) = the OFun of IT . (Q,s) ) ) & the InitS of tfsm in the InitS of IT )
now for Q being Element of IT
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . [q,s] in the Tran of IT . (Q,s) & the OFun of tfsm . [q,s] = the OFun of IT . [Q,s] )reconsider a19 = 1 as
Integer ;
let Q be
Element of
IT;
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . [q,s] in the Tran of IT . (Q,s) & the OFun of tfsm . [q,s] = the OFun of IT . [Q,s] )let s be
Element of
IAlph;
for q being State of tfsm st q in Q holds
( the Tran of tfsm . [q,s] in the Tran of IT . (Q,s) & the OFun of tfsm . [q,s] = the OFun of IT . [Q,s] )let q be
State of
tfsm;
( q in Q implies ( the Tran of tfsm . [q,s] in the Tran of IT . (Q,s) & the OFun of tfsm . [q,s] = the OFun of IT . [Q,s] ) )assume A4:
q in Q
;
( the Tran of tfsm . [q,s] in the Tran of IT . (Q,s) & the OFun of tfsm . [q,s] = the OFun of IT . [Q,s] )reconsider s9 =
s as
Element of
IAlph ;
reconsider Q9 =
Q as
Element of
final_states_partition tfsm ;
consider Q1 being
Element of
tfsm,
n1 being
Nat such that A5:
Q1 in Q9
and
n1 + 1
= card the
carrier of
tfsm
and A6:
(
s9,
Q9)
-succ_class = Class (
(n1 -eq_states_EqR tfsm),
( the Tran of tfsm . [Q1,s9]))
by Def16;
final_states_partition tfsm is
final
by Def15;
then
q,
Q1 -are_equivalent
by A4, A5;
then A7:
n1 + 1
-equivalent q,
Q1
;
reconsider n19 =
n1 as
Integer ;
( 1
<= n1 + 1 &
(n19 + a19) - a19 = n19 )
by NAT_1:11;
then
n1 -equivalent the
Tran of
tfsm . [q,s9], the
Tran of
tfsm . [Q1,s9]
by A7, Th27;
then A8:
[( the Tran of tfsm . [q,s9]),( the Tran of tfsm . [Q1,s9])] in n1 -eq_states_EqR tfsm
by Def12;
the
Tran of
IT . (
Q9,
s9)
= Class (
(n1 -eq_states_EqR tfsm),
( the Tran of tfsm . (Q1,s9)))
by A2, A6;
hence
the
Tran of
tfsm . [q,s] in the
Tran of
IT . (
Q,
s)
by A8, EQREL_1:19;
the OFun of tfsm . [q,s] = the OFun of IT . [Q,s]A9:
the
OFun of
IT . (
Q9,
s9)
= (
Q9,
s9)
-class_response
by A3;
consider Q1 being
Element of
tfsm such that A10:
Q1 in Q9
and A11:
(
Q9,
s9)
-class_response = the
OFun of
tfsm . [Q1,s9]
by Def17;
final_states_partition tfsm is
final
by Def15;
then
q,
Q1 -are_equivalent
by A4, A10;
hence
the
OFun of
tfsm . [q,s] = the
OFun of
IT . [Q,s]
by A9, A11, Th19;
verum end;
hence
( the carrier of IT = final_states_partition tfsm & ( for Q being State of IT
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of IT . (Q,s) & the OFun of tfsm . (q,s) = the OFun of IT . (Q,s) ) ) & the InitS of tfsm in the InitS of IT )
by EQREL_1:20; verum