Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Minimization of Finite State Machines

by
Miroslava Kaloper, and
Piotr Rudnicki

MML identifier: FSM_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, ARYTM_1, INT_1, FUNCT_1, RELAT_1, SGRAPH1, EQREL_1,
TARSKI, FINSET_1, BOOLE, CARD_1, BORSUK_1, SETFAM_1, AMI_1, MATRIX_2,
MCART_1, RELAT_2, FUNCOP_1, FUNCT_4, FSM_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1,
INT_1, SETFAM_1, STRUCT_0, FINSET_1, GROUP_1, MCART_1, DOMAIN_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FINSEQ_1, CARD_1, EQREL_1, BORSUK_1,
MATRIX_2;
constructors NAT_1, DOMAIN_1, FUNCT_4, BORSUK_1, MATRIX_2, PARTFUN1, GROUP_1,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, INT_1, FINSET_1, CARD_1, XBOOLE_0, RELSET_1,
FINSEQ_1, STRUCT_0, BORSUK_1, NAT_1, XREAL_0, MEMBERED, ZFMISC_1,
FUNCT_2, PARTFUN1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;

begin :: Preliminaries

reserve m, n, i, k for Nat;

theorem :: FSM_1:1
for m, n being Nat holds
m < n implies ex p being Nat st n = m+p & 1 <= p;

theorem :: FSM_1:2
i in Seg n implies i+m in Seg (n+m);

theorem :: FSM_1:3
i>0 & i+m in Seg (n+m) implies i in Seg n & i in Seg (n+m);

theorem :: FSM_1:4
k < i implies ex j being Nat st j = i-k & 1 <= j;

theorem :: FSM_1:5
for D being non empty set, df being FinSequence of D holds
df is non empty implies ex d being Element of D, df1 being FinSequence of D
st d = df.1 & df = <*d*>^df1;

theorem :: FSM_1:6
for df being FinSequence, d being set holds
i in dom df implies (<*d*>^df).(i+1) = df.i;

theorem :: FSM_1:7
for S being set, D1, D2 being non empty set,
f1 being Function of S, D1, f2 being Function of D1, D2 holds
f1 is bijective & f2 is bijective implies f2*f1 is bijective;

:: Partitions & Equivalence Relations

theorem :: FSM_1:8
for Y being set, E1, E2 being Equivalence_Relation of Y
holds Class E1 = Class E2 implies E1 = E2;

theorem :: FSM_1:9
for W being non empty set, PW being a_partition of W
holds PW is non empty;

theorem :: FSM_1:10
for Z being finite set, PZ being a_partition of Z
holds PZ is finite;

definition let W be non empty set;
cluster -> non empty a_partition of W;
end;

definition let Z be finite set;
cluster -> finite a_partition of Z;
end;

definition let X be non empty finite set;
cluster non empty finite a_partition of X;
end;

reserve X, A for non empty finite set,
PX for a_partition of X,
PA1, PA2 for a_partition of A;

theorem :: FSM_1:11
for X being non empty set, PX being a_partition of X
for Pi being set st Pi in PX ex x being Element of X st x in Pi;

theorem :: FSM_1:12
card PX <= card X;

theorem :: FSM_1:13
PA1 is_finer_than PA2 implies card PA2 <= card PA1;

theorem :: FSM_1:14
PA1 is_finer_than PA2 implies
for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c=p2;

theorem :: FSM_1:15
PA1 is_finer_than PA2 & card PA1 = card PA2 implies PA1 = PA2;

begin :: Definitions and terminology for FSM

definition let IAlph be set;
struct (1-sorted) FSM over IAlph (#
carrier -> set,
Tran -> Function of [: the carrier, IAlph :], the carrier,
InitS -> Element of the carrier #);
end;

definition let IAlph be set, fsm be FSM over IAlph;
mode State of fsm is Element of fsm;
end;

definition let X be set;
cluster non empty finite FSM over X;
end;

definition :: WAYBEL11
cluster finite non empty 1-sorted;
end;

definition let S be finite 1-sorted; :: YELLOW13
cluster the carrier of S -> finite;
end;

reserve IAlph, OAlph for non empty set,
fsm for non empty FSM over IAlph,
s for Element of IAlph,
w, w1, w2 for FinSequence of IAlph,
q, q', q1, q2 for State of fsm;

definition let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let s be Element of IAlph, q be State of fsm;
func s -succ_of q -> State of fsm equals
:: FSM_1:def 1
(the Tran of fsm).[q, s];
end;

definition let IAlph be non empty set; let fsm be non empty FSM over IAlph;
let q be State of fsm; let w be FinSequence of IAlph;
func (q, w)-admissible -> FinSequence of the carrier of fsm means
:: FSM_1:def 2

it.1 = q & len it = len w + 1 &
for i st 1 <= i & i <= len w
ex wi being Element of IAlph, qi, qi1 being State of fsm st
wi = w.i & qi = it.i & qi1 = it.(i+1) & wi-succ_of qi = qi1;
end;

theorem :: FSM_1:16

definition let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let w be FinSequence of IAlph;
let q1, q2 be State of fsm;
:: FSM_1:def 3
(q1, w)-admissible.(len w + 1) = q2;
end;

theorem :: FSM_1:17

definition let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let w be FinSequence of IAlph;
let q_seq be FinSequence of the carrier of fsm;
:: FSM_1:def 4
ex q1 being State of fsm st q1 = q_seq.1 & (q1, w)-admissible = q_seq;
end;

theorem :: FSM_1:18

definition let IAlph, fsm, q, w;
func q leads_to_under w -> State of fsm means
:: FSM_1:def 5
end;

theorem :: FSM_1:19

theorem :: FSM_1:20
for k st 1 <= k & k <= len w1

theorem :: FSM_1:21
(q1,w1^w2)-admissible.(len w1 + 1) = q2;

theorem :: FSM_1:22
for k st 1 <= k & k <= len w2 + 1

theorem :: FSM_1:23

begin :: Mealy and Moore machines and their responses

definition let IAlph be set, OAlph be non empty set;
struct (FSM over IAlph) Mealy-FSM over IAlph, OAlph (#
carrier -> set,
Tran -> Function of [: the carrier, IAlph :], the carrier,
OFun -> Function of [: the carrier, IAlph :], OAlph,
InitS -> Element of the carrier #);

struct (FSM over IAlph) Moore-FSM over IAlph, OAlph (#
carrier -> set,
Tran -> Function of [: the carrier, IAlph :], the carrier,
OFun -> Function of the carrier, OAlph,
InitS -> Element of the carrier #);
end;

definition let IAlph be set,
X be finite non empty set,
T be Function of [: X, IAlph :], X,
I be Element of X;
cluster FSM (# X, T, I #) -> finite non empty;
end;

definition let IAlph be set, OAlph be non empty set,
X be finite non empty set,
T be Function of [: X, IAlph :], X,
O be Function of [: X, IAlph :], OAlph,
I be Element of X;
cluster Mealy-FSM (# X, T, O, I #) -> finite non empty;
end;

definition let IAlph be set, OAlph be non empty set,
X be finite non empty set,
T be Function of [: X, IAlph :], X,
O be Function of X, OAlph,
I be Element of X;
cluster Moore-FSM (# X, T, O, I #) -> finite non empty;
end;

definition let IAlph be set, OAlph be non empty set;
cluster finite non empty Mealy-FSM over IAlph, OAlph;

cluster finite non empty Moore-FSM over IAlph, OAlph;
end;

reserve tfsm, tfsm1, tfsm2, tfsm3 for non empty Mealy-FSM over IAlph, OAlph,
sfsm for non empty Moore-FSM over IAlph, OAlph,
qs for State of sfsm,
q, q1, q2, q3, qa, qb, qc, qa', qt, q1t, q2t for State of tfsm,
q11, q12 for State of tfsm1,
q21, q22 for State of tfsm2;

definition let IAlph, OAlph, tfsm, qt, w;
func (qt, w)-response -> FinSequence of OAlph means
:: FSM_1:def 6

len it = len w &
for i st i in dom w holds
it.i = (the OFun of tfsm).[(qt, w)-admissible.i, w.i];
end;

theorem :: FSM_1:24
(qt, <*>IAlph)-response = <*>OAlph;

definition let IAlph, OAlph, sfsm, qs, w;
func (qs, w)-response -> FinSequence of OAlph means
:: FSM_1:def 7
len it = len w + 1 &
for i st i in Seg (len w + 1) holds
it.i = (the OFun of sfsm).((qs, w)-admissible.i);
end;

theorem :: FSM_1:25
((qs, w)-response).1 = (the OFun of sfsm).qs;

theorem :: FSM_1:26
(q1t,w1^w2)-response = (q1t,w1)-response ^ (q2t,w2)-response;

theorem :: FSM_1:27
(q12,w2)-response <> (q22,w2)-response
implies (q11,w1^w2)-response <> (q21,w1^w2)-response;

reserve OAlph_f for finite non empty set,
tfsm_f for finite non empty Mealy-FSM over IAlph, OAlph_f,
sfsm_f for finite non empty Moore-FSM over IAlph, OAlph_f;

definition let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph, OAlph;
let sfsm be non empty Moore-FSM over IAlph, OAlph;
pred tfsm is_similar_to sfsm means
:: FSM_1:def 8
for tw being FinSequence of IAlph holds
<*(the OFun of sfsm).(the InitS of sfsm)*>^((the InitS of tfsm, tw)-response)
= (the InitS of sfsm, tw)-response;
end;

theorem :: FSM_1:28
for sfsm being non empty finite Moore-FSM over IAlph, OAlph
ex tfsm being non empty finite Mealy-FSM over IAlph, OAlph
st tfsm is_similar_to sfsm;

theorem :: FSM_1:29
ex sfsm_f st tfsm_f is_similar_to sfsm_f;

begin :: Equivalence of states and machines (for Mealy machines)

definition let IAlph, OAlph be non empty set,
tfsm1, tfsm2 be non empty Mealy-FSM over IAlph, OAlph;
pred tfsm1, tfsm2-are_equivalent means
:: FSM_1:def 9
for w being FinSequence of IAlph holds
(the InitS of tfsm1,w)-response = (the InitS of tfsm2,w)-response;
reflexivity;
symmetry;
end;

theorem :: FSM_1:30
tfsm1, tfsm2-are_equivalent & tfsm2, tfsm3-are_equivalent
implies tfsm1, tfsm3-are_equivalent;

definition let IAlph, OAlph, tfsm, qa, qb;
pred qa, qb-are_equivalent means
:: FSM_1:def 10
for w holds (qa, w)-response = (qb, w)-response;
reflexivity;
symmetry;
end;

canceled 2;

theorem :: FSM_1:33
q1, q2-are_equivalent & q2, q3-are_equivalent implies q1, q3-are_equivalent
;

theorem :: FSM_1:34
qa' = (the Tran of tfsm).[qa, s]
implies for i st i in Seg (len w + 1) holds

theorem :: FSM_1:35
qa' = (the Tran of tfsm).[qa, s] implies
(qa, <*s*>^w)-response = <*(the OFun of tfsm).[qa, s]*>^(qa', w)-response;

theorem :: FSM_1:36
qa, qb-are_equivalent iff
for s holds (the OFun of tfsm).[qa, s] = (the OFun of tfsm).[qb, s] &
(the Tran of tfsm).[qa, s], (the Tran of tfsm).[qb, s]-are_equivalent;

theorem :: FSM_1:37
qa, qb-are_equivalent implies
for w, i st i in dom w ex qai, qbi being State of tfsm
qai, qbi-are_equivalent;

definition let IAlph, OAlph,tfsm, qa, qb, k;
pred k-equivalent qa, qb means
:: FSM_1:def 11
for w st len w<=k holds (qa,w)-response = (qb,w)-response;
end;

theorem :: FSM_1:38
k-equivalent qa, qa;

theorem :: FSM_1:39
k-equivalent qa, qb implies k-equivalent qb, qa;

theorem :: FSM_1:40
k-equivalent qa, qb & k-equivalent qb, qc implies k-equivalent qa, qc;

theorem :: FSM_1:41
qa,qb-are_equivalent implies k-equivalent qa,qb;

theorem :: FSM_1:42
0-equivalent qa, qb;

theorem :: FSM_1:43
(k+m)-equivalent qa, qb implies k-equivalent qa, qb;

theorem :: FSM_1:44
1 <= k implies
(k-equivalent qa, qb iff
1-equivalent qa, qb &
for s being Element of IAlph, k1 being Nat st k1 = k - 1
holds k1-equivalent (the Tran of tfsm).[qa, s], (the Tran of tfsm).[qb, s])
;

definition let IAlph, OAlph, tfsm, i;
func i-eq_states_EqR tfsm -> Equivalence_Relation of the carrier of tfsm
means
:: FSM_1:def 12
for qa, qb holds [qa, qb] in it iff i-equivalent qa, qb;
end;

definition let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph, OAlph;
let i;
func i-eq_states_partition tfsm ->
non empty a_partition of the carrier of tfsm equals
:: FSM_1:def 13
Class (i-eq_states_EqR tfsm);
end;

theorem :: FSM_1:45
(k+1)-eq_states_partition tfsm is_finer_than k-eq_states_partition tfsm;

theorem :: FSM_1:46
Class (k-eq_states_EqR tfsm) = Class ((k+1)-eq_states_EqR tfsm)implies
for m holds Class ((k+m)-eq_states_EqR tfsm) = Class (k-eq_states_EqR tfsm);

theorem :: FSM_1:47
k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm implies
for m holds (k+m)-eq_states_partition tfsm = k-eq_states_partition tfsm;

theorem :: FSM_1:48
(k+1)-eq_states_partition tfsm <> k-eq_states_partition tfsm implies
for i st i <= k holds
(i+1)-eq_states_partition tfsm <> i-eq_states_partition tfsm;

theorem :: FSM_1:49
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph holds
k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm or
card (k-eq_states_partition tfsm) < card ((k+1)-eq_states_partition tfsm);

theorem :: FSM_1:50
Class (0-eq_states_EqR tfsm, q) = the carrier of tfsm;

theorem :: FSM_1:51
0-eq_states_partition tfsm = { the carrier of tfsm };

theorem :: FSM_1:52
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph st
n+1 = card the carrier of tfsm holds
(n+1)-eq_states_partition tfsm = n-eq_states_partition tfsm;

definition let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph, OAlph;
let IT be a_partition of the carrier of tfsm;
attr IT is final means
:: FSM_1:def 14
for qa, qb being State of tfsm holds qa, qb-are_equivalent iff
ex X being Element of IT st qa in X & qb in X;
end;

theorem :: FSM_1:53
k-eq_states_partition tfsm is final implies
(k+1)-eq_states_EqR tfsm = k-eq_states_EqR tfsm;

theorem :: FSM_1:54
k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm
iff k-eq_states_partition tfsm is final;

theorem :: FSM_1:55
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph st
n+1 = card the carrier of tfsm holds
ex k being Nat st k <= n & k-eq_states_partition tfsm is final;

definition let IAlph, OAlph;
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
func final_states_partition tfsm -> a_partition of the carrier of tfsm
means
:: FSM_1:def 15
it is final;
end;

theorem :: FSM_1:56
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph holds
n+1 = card the carrier of tfsm implies
final_states_partition tfsm = n-eq_states_partition tfsm;

begin :: The reduction of a Mealy machine

reserve tfsm, rtfsm for finite non empty Mealy-FSM over IAlph, OAlph,
q for State of tfsm;

definition let IAlph, OAlph be non empty set;
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
let qf be Element of final_states_partition tfsm;
let s be Element of IAlph;
func (s,qf)-succ_class -> Element of final_states_partition tfsm means
:: FSM_1:def 16

ex q being State of tfsm, n being Nat st
q in qf & (n+1) = card the carrier of tfsm &
it = Class(n-eq_states_EqR tfsm, (the Tran of tfsm).[q,s]);
end;

definition let IAlph, OAlph, tfsm;
let qf be Element of final_states_partition tfsm, s;
func (qf,s)-class_response -> Element of OAlph means
:: FSM_1:def 17
ex q st q in qf & it = (the OFun of tfsm).[q,s];
end;

definition let IAlph, OAlph, tfsm;
func the_reduction_of tfsm -> strict Mealy-FSM over IAlph, OAlph means
:: FSM_1:def 18

the carrier of it = final_states_partition tfsm &
(for Q being State of it, s 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;
end;

definition let IAlph, OAlph, tfsm;
cluster the_reduction_of tfsm -> non empty finite;
end;

theorem :: FSM_1:57
for qr being State of rtfsm st
rtfsm = the_reduction_of tfsm & q in qr holds
for k being Nat st k in Seg (len w +1) holds

theorem :: FSM_1:58
tfsm, the_reduction_of tfsm-are_equivalent;

begin :: Machine Isomorphism

reserve qr1, qr2 for State of rtfsm,
Tf for Function of the carrier of tfsm1, the carrier of tfsm2;

definition let IAlph, OAlph, tfsm1, tfsm2;
pred tfsm1, tfsm2-are_isomorphic means
:: FSM_1:def 19

ex Tf st Tf is bijective & Tf.the InitS of tfsm1 = the InitS of tfsm2 &
for q11, s holds
Tf.((the Tran of tfsm1).[q11,s])=(the Tran of tfsm2).[Tf.q11, s] &
(the OFun of tfsm1).[q11,s] = (the OFun of tfsm2).[Tf.q11, s];
reflexivity;
symmetry;
end;

theorem :: FSM_1:59
tfsm1,tfsm2-are_isomorphic & tfsm2,tfsm3-are_isomorphic
implies tfsm1,tfsm3-are_isomorphic;

theorem :: FSM_1:60
(for q being State of tfsm1, s
holds Tf.((the Tran of tfsm1).[q,s]) = (the Tran of tfsm2).[Tf.q,s])
implies for k st 1 <= k & k <= len w + 1

theorem :: FSM_1:61
(Tf.the InitS of tfsm1 = the InitS of tfsm2 &
for q being State of tfsm1, s holds
Tf.((the Tran of tfsm1).[q, s]) = (the Tran of tfsm2).[Tf.q, s] &
(the OFun of tfsm1).[q,s] = (the OFun of tfsm2).[Tf.q, s])
implies (q11,q12-are_equivalent iff Tf.q11, Tf.q12 -are_equivalent);

theorem :: FSM_1:62
rtfsm = the_reduction_of tfsm & qr1<>qr2 implies
not qr1,qr2 -are_equivalent;

begin :: Reduced and Connected Machines

definition let IAlph, OAlph be non empty set;
let IT be non empty Mealy-FSM over IAlph,OAlph;
attr IT is reduced means
:: FSM_1:def 20
for qa, qb being State of IT
st qa <> qb holds not qa, qb-are_equivalent;
end;

theorem :: FSM_1:63
the_reduction_of tfsm is reduced;

definition let IAlph, OAlph;
cluster reduced finite (non empty Mealy-FSM over IAlph,OAlph);
end;

reserve Rtfsm for reduced (finite non empty Mealy-FSM over IAlph, OAlph);

theorem :: FSM_1:64
Rtfsm, the_reduction_of Rtfsm-are_isomorphic;

theorem :: FSM_1:65
tfsm is reduced iff
ex M being finite non empty Mealy-FSM over IAlph,OAlph
st tfsm, the_reduction_of M-are_isomorphic;

definition let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let IT be State of tfsm;
attr IT is accessible means
:: FSM_1:def 21
ex w st the InitS of tfsm, w-leads_to IT;
end;

definition let IAlph, OAlph;
let IT be non empty Mealy-FSM over IAlph, OAlph;
attr IT is connected means
:: FSM_1:def 22
for q being State of IT holds q is accessible;
end;

definition let IAlph, OAlph;
cluster connected (finite non empty Mealy-FSM over IAlph,OAlph);
end;

reserve Ctfsm, Ctfsm1, Ctfsm2 for connected (finite
non empty Mealy-FSM over IAlph, OAlph);

theorem :: FSM_1:66
the_reduction_of Ctfsm is connected;

definition let IAlph, OAlph;
cluster connected reduced finite (non empty Mealy-FSM over IAlph,OAlph);
end;

definition let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
func accessibleStates tfsm equals
:: FSM_1:def 23
{ q where q is State of tfsm : q is accessible };
end;

definition let IAlph, OAlph, tfsm;
cluster accessibleStates tfsm -> finite non empty;
end;

theorem :: FSM_1:67
accessibleStates tfsm c= the carrier of tfsm &
for q holds q in accessibleStates tfsm iff q is accessible;

theorem :: FSM_1:68
(the Tran of tfsm)|[:accessibleStates tfsm, IAlph:] is
Function of [:accessibleStates tfsm, IAlph:], accessibleStates tfsm;

theorem :: FSM_1:69
for cTran being Function of [:accessibleStates tfsm, IAlph:],
accessibleStates tfsm,
cOFun being Function of [:accessibleStates tfsm, IAlph:], OAlph,
cInitS being Element of accessibleStates tfsm
st cTran = (the Tran of tfsm) | [:accessibleStates tfsm, IAlph:] &
cOFun = (the OFun of tfsm) | [:accessibleStates tfsm, IAlph:] &
cInitS = the InitS of tfsm
holds tfsm, Mealy-FSM(#accessibleStates tfsm, cTran, cOFun, cInitS#)
-are_equivalent;

theorem :: FSM_1:70
ex Ctfsm st
the Tran of Ctfsm = (the Tran of tfsm)|[:accessibleStates tfsm, IAlph:] &
the OFun of Ctfsm = (the OFun of tfsm)|[:accessibleStates tfsm, IAlph:] &
the InitS of Ctfsm = the InitS of tfsm & tfsm, Ctfsm-are_equivalent;

begin :: Machine union

definition let IAlph be set, OAlph be non empty set;
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph, OAlph;
func tfsm1-Mealy_union tfsm2 -> strict Mealy-FSM over IAlph, OAlph means
:: FSM_1:def 24

the carrier of it = (the carrier of tfsm1) \/ (the carrier of tfsm2) &
the Tran of it = (the Tran of tfsm1) +* (the Tran of tfsm2) &
the OFun of it = (the OFun of tfsm1) +* (the OFun of tfsm2) &
the InitS of it = the InitS of tfsm1;
end;

definition let IAlph be set, OAlph be non empty set;
let tfsm1, tfsm2 be non empty finite Mealy-FSM over IAlph, OAlph;
cluster tfsm1-Mealy_union tfsm2 -> non empty finite;
end;

theorem :: FSM_1:71
tfsm = tfsm1-Mealy_union tfsm2 &
the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q

theorem :: FSM_1:72
tfsm = tfsm1-Mealy_union tfsm2 &
the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q
implies (q11,w)-response = (q,w)-response;

theorem :: FSM_1:73
tfsm = tfsm1-Mealy_union tfsm2 &
the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q

theorem :: FSM_1:74
tfsm = tfsm1-Mealy_union tfsm2 &
the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q
implies (q21,w)-response = (q,w)-response;

reserve Rtfsm1, Rtfsm2 for reduced (non empty Mealy-FSM over IAlph, OAlph);

theorem :: FSM_1:75
tfsm = Rtfsm1-Mealy_union Rtfsm2 &
the carrier of Rtfsm1 misses the carrier of Rtfsm2 &
Rtfsm1, Rtfsm2-are_equivalent
implies ex Q being State of the_reduction_of tfsm
st the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q &
Q = the InitS of the_reduction_of tfsm;

reserve CRtfsm1, CRtfsm2 for connected reduced
(non empty Mealy-FSM over IAlph, OAlph),
q1u, q2u for State of tfsm;

theorem :: FSM_1:76
for crq11, crq12 being State of CRtfsm1 holds
crq11 = q1u & crq12 = q2u &
the carrier of CRtfsm1 misses the carrier of CRtfsm2 &
CRtfsm1, CRtfsm2-are_equivalent & tfsm = CRtfsm1-Mealy_union CRtfsm2 &
not crq11, crq12-are_equivalent
implies not q1u,q2u-are_equivalent;

theorem :: FSM_1:77
for crq21, crq22 being State of CRtfsm2 holds
crq21 = q1u & crq22 = q2u &
the carrier of CRtfsm1 misses the carrier of CRtfsm2 &
CRtfsm1, CRtfsm2-are_equivalent & tfsm = CRtfsm1-Mealy_union CRtfsm2 &
not crq21, crq22-are_equivalent
implies not q1u, q2u-are_equivalent;

reserve CRtfsm1, CRtfsm2 for connected reduced (finite non empty
Mealy-FSM over IAlph, OAlph);

theorem :: FSM_1:78
the carrier of CRtfsm1 misses the carrier of CRtfsm2 &
CRtfsm1, CRtfsm2-are_equivalent &
tfsm = CRtfsm1-Mealy_union CRtfsm2
implies for Q being State of the_reduction_of tfsm holds
not ex q1, q2 being Element of Q st
q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm1 & q1 <> q2;

theorem :: FSM_1:79
the carrier of CRtfsm1 misses the carrier of CRtfsm2 &
CRtfsm1, CRtfsm2-are_equivalent & tfsm = CRtfsm1-Mealy_union CRtfsm2
implies for Q being State of the_reduction_of tfsm holds
not ex q1, q2 being Element of Q st
q1 in the carrier of CRtfsm2 & q2 in the carrier of CRtfsm2 & q1 <> q2;

theorem :: FSM_1:80
the carrier of CRtfsm1 misses the carrier of CRtfsm2 &
CRtfsm1, CRtfsm2-are_equivalent &
tfsm = CRtfsm1-Mealy_union CRtfsm2
implies for Q being State of the_reduction_of tfsm
ex q1, q2 being Element of Q st
q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm2 &
for q being Element of Q holds q = q1 or q = q2;

begin :: The minimization theorem

theorem :: FSM_1:81
for tfsm1, tfsm2 being finite non empty Mealy-FSM over IAlph, OAlph
ex fsm1, fsm2 being finite non empty Mealy-FSM over IAlph, OAlph st
the carrier of fsm1 misses the carrier of fsm2 &
fsm1, tfsm1-are_isomorphic & fsm2,tfsm2-are_isomorphic;

theorem :: FSM_1:82
tfsm1, tfsm2-are_isomorphic implies tfsm1, tfsm2-are_equivalent;

theorem :: FSM_1:83
the carrier of CRtfsm1 misses the carrier of CRtfsm2 &
CRtfsm1, CRtfsm2-are_equivalent
implies CRtfsm1, CRtfsm2-are_isomorphic;

theorem :: FSM_1:84
Ctfsm1, Ctfsm2-are_equivalent implies
the_reduction_of Ctfsm1, the_reduction_of Ctfsm2-are_isomorphic;

theorem :: FSM_1:85
for M1, M2 being connected reduced
(finite non empty Mealy-FSM over IAlph, OAlph)
holds M1, M2-are_isomorphic iff M1, M2-are_equivalent;

```