:: Minimization of finite state machines
:: by Miroslava Kaloper and Piotr Rudnicki
::
:: Received November 18, 1994
:: Copyright (c) 1994-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0, CARD_1, XBOOLE_0,
FUNCT_1, FUNCT_2, RELAT_1, EQREL_1, FINSET_1, CARD_3, SETFAM_1, TARSKI,
STRUCT_0, ZFMISC_1, FINSEQ_1, ORDINAL4, FINSEQ_3, ARYTM_1, MCART_1,
LATTICES, INT_1, RELAT_2, FUNCOP_1, FUNCT_4, FSM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, INT_1, SETFAM_1, FINSET_1, STRUCT_0, XTUPLE_0, MCART_1,
DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1,
XXREAL_0, FUNCT_4, FINSEQ_1, FINSEQ_3, EQREL_1;
constructors FUNCT_4, REAL_1, NAT_1, NAT_D, MEMBERED, FUNCOP_1, FINSEQ_3,
BORSUK_1, BINOP_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, INT_1, EQREL_1, STRUCT_0, FINSEQ_1, CARD_1,
RELSET_1, RELAT_1, XTUPLE_0, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Definitions and terminology for FSM
reserve m, n, i, k for Nat;
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;
registration
let X be set;
cluster non empty finite for FSM over X;
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, q9, 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 being Nat 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:1
(q, <*>IAlph)-admissible = <*q*>;
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;
pred q1, w-leads_to q2 means
:: FSM_1:def 3
(q1, w)-admissible.(len w + 1) = q2;
end;
theorem :: FSM_1:2
q, <*>IAlph-leads_to q;
definition
let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let w be FinSequence of IAlph;
let qseq be FinSequence of the carrier of fsm;
pred qseq is_admissible_for w means
:: FSM_1:def 4
ex q1 being State of fsm st q1 = qseq.1 & (q1, w)-admissible = qseq;
end;
theorem :: FSM_1:3
<*q*> is_admissible_for <*>IAlph;
definition
let IAlph, fsm, q, w;
func q leads_to_under w -> State of fsm means
:: FSM_1:def 5
q, w-leads_to it;
end;
theorem :: FSM_1:4
((q, w)-admissible).(len (q, w)-admissible) = q9 iff q, w -leads_to q9;
theorem :: FSM_1:5
for k st 1 <= k & k <= len w1 holds
(q1,w1^w2)-admissible.k = (q1,w1)-admissible.k;
theorem :: FSM_1:6
q1,w1-leads_to q2 implies (q1,w1^w2)-admissible.(len w1 + 1) = q2;
theorem :: FSM_1:7
q1,w1-leads_to q2 implies for k st 1 <= k & k <= len w2 + 1
holds (q1,w1^w2)-admissible.(len w1 + k) = (q2,w2)-admissible.k;
theorem :: FSM_1:8
q1,w1-leads_to q2 implies (q1,w1^w2)-admissible = Del((q1,w1)
-admissible,(len w1 + 1))^(q2,w2)-admissible;
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;
registration
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;
registration
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;
registration
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;
registration
let IAlph be set, OAlph be non empty set;
cluster finite non empty for Mealy-FSM over IAlph, OAlph;
cluster finite non empty for 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, qa9, 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:9
(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:10
((qs, w)-response).1 = (the OFun of sfsm).qs;
theorem :: FSM_1:11
q1t,w1-leads_to q2t implies (q1t,w1^w2)-response = (q1t,w1)
-response ^ (q2t,w2)-response;
theorem :: FSM_1:12
q11, w1 -leads_to q12 & q21, w1 -leads_to q22 & (q12,w2)
-response <> (q22,w2)-response implies (q11,w1^w2)-response <> (q21,w1^w2)
-response;
reserve OAlphf for finite non empty set,
tfsmf for finite non empty Mealy-FSM over IAlph, OAlphf,
sfsmf for finite non empty Moore-FSM over IAlph, OAlphf;
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:13
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:14
ex sfsmf st tfsmf is_similar_to sfsmf;
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:15
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;
theorem :: FSM_1:16
q1, q2-are_equivalent & q2, q3-are_equivalent implies q1, q3 -are_equivalent;
theorem :: FSM_1:17
qa9 = (the Tran of tfsm).[qa, s] implies for i st i in Seg (len
w + 1) holds (qa, <*s*>^w)-admissible.(i+1) = (qa9, w)-admissible.i;
theorem :: FSM_1:18
qa9 = (the Tran of tfsm).[qa, s] implies (qa, <*s*>^w)-response
= <*(the OFun of tfsm).[qa, s]*>^(qa9, w)-response;
theorem :: FSM_1:19
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:20
qa, qb-are_equivalent implies for w, i st i in dom w ex qai, qbi being
State of tfsm st qai = (qa, w)-admissible.i & qbi = ((qb, w)-admissible.i) &
qai, qbi-are_equivalent;
definition
let IAlph, OAlph,tfsm, qa, qb;
let k be Nat;
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:21
for k be Nat holds k-equivalent qa, qa;
theorem :: FSM_1:22
for k be Nat st k-equivalent qa, qb holds k-equivalent qb, qa;
theorem :: FSM_1:23
for k be Nat st k-equivalent qa, qb & k-equivalent qb, qc holds
k-equivalent qa, qc;
theorem :: FSM_1:24
qa,qb-are_equivalent implies k-equivalent qa,qb;
theorem :: FSM_1:25
0-equivalent qa, qb;
theorem :: FSM_1:26
for k, m be Nat st (k+m)-equivalent qa, qb holds k-equivalent qa , qb;
theorem :: FSM_1:27
for k be Nat st 1 <= k holds (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;
let i be Nat;
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 be Nat;
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:28
(k+1)-eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm;
theorem :: FSM_1:29
for k be Nat holds Class (k-eq_states_EqR tfsm) = Class ((k+1)
-eq_states_EqR tfsm)implies for m be Nat holds Class ((k+m)-eq_states_EqR tfsm)
= Class (k-eq_states_EqR tfsm);
theorem :: FSM_1:30
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:31
(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:32
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:33
Class (0-eq_states_EqR tfsm, q) = the carrier of tfsm;
theorem :: FSM_1:34
0-eq_states_partition tfsm = { the carrier of tfsm };
theorem :: FSM_1:35
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:36
k-eq_states_partition tfsm is final implies (k+1)-eq_states_EqR tfsm =
k-eq_states_EqR tfsm;
theorem :: FSM_1:37
k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm
implies k-eq_states_partition tfsm is final;
theorem :: FSM_1:38
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:39
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;
registration
let IAlph, OAlph, tfsm;
cluster the_reduction_of tfsm -> non empty finite;
end;
theorem :: FSM_1:40
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 (q,w)
-admissible.k in (qr,w)-admissible.k;
theorem :: FSM_1:41
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:42
tfsm1,tfsm2-are_isomorphic & tfsm2,tfsm3-are_isomorphic implies
tfsm1,tfsm3-are_isomorphic;
theorem :: FSM_1:43
(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
holds Tf.((q11,w)-admissible.k) = (Tf.q11,w)-admissible.k;
theorem :: FSM_1:44
( 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:45
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;
registration
let IAlph,OAlph,tfsm;
cluster the_reduction_of tfsm -> reduced;
end;
registration
let IAlph, OAlph;
cluster reduced finite for non empty Mealy-FSM over IAlph,OAlph;
end;
reserve Rtfsm for reduced finite non empty Mealy-FSM over IAlph, OAlph;
theorem :: FSM_1:46
Rtfsm, the_reduction_of Rtfsm-are_isomorphic;
theorem :: FSM_1:47
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;
registration
let IAlph, OAlph;
cluster connected for finite non empty Mealy-FSM over IAlph,OAlph;
end;
reserve Ctfsm, Ctfsm1, Ctfsm2 for connected finite non empty Mealy-FSM over
IAlph, OAlph;
registration
let IAlph,OAlph,Ctfsm;
cluster the_reduction_of Ctfsm -> connected;
end;
registration
let IAlph, OAlph;
cluster connected reduced finite for 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 -> set equals
:: FSM_1:def 23
{ q where q is State of tfsm : q is
accessible };
end;
registration
let IAlph, OAlph, tfsm;
cluster accessibleStates tfsm -> finite non empty;
end;
theorem :: FSM_1:48
accessibleStates tfsm c= the carrier of tfsm & for q holds q in
accessibleStates tfsm iff q is accessible;
theorem :: FSM_1:49
(the Tran of tfsm)|[:accessibleStates tfsm, IAlph:] is Function
of [:accessibleStates tfsm, IAlph:], accessibleStates tfsm;
theorem :: FSM_1:50
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:51
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;
registration
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:52
tfsm = tfsm1-Mealy_union tfsm2 & the carrier of tfsm1 misses the
carrier of tfsm2 & q11 = q implies (q11,w)-admissible = (q,w)-admissible;
theorem :: FSM_1:53
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:54
tfsm = tfsm1-Mealy_union tfsm2 & q21 = q implies (q21,w)
-admissible = (q,w)-admissible;
theorem :: FSM_1:55
tfsm = tfsm1-Mealy_union 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:56
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:57
for crq11, crq12 being State of CRtfsm1 holds crq11 = q1u &
crq12 = q2u & the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm =
CRtfsm1-Mealy_union CRtfsm2 & not crq11, crq12-are_equivalent implies not q1u,
q2u-are_equivalent;
theorem :: FSM_1:58
for crq21, crq22 being State of CRtfsm2 holds crq21 = q1u &
crq22 = q2u & 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:59
the carrier of CRtfsm1 misses the carrier of CRtfsm2 & 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:60
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:61
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:62
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:63
tfsm1, tfsm2-are_isomorphic implies tfsm1, tfsm2-are_equivalent;
theorem :: FSM_1:64
the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,
CRtfsm2-are_equivalent implies CRtfsm1, CRtfsm2-are_isomorphic;
theorem :: FSM_1:65
Ctfsm1, Ctfsm2-are_equivalent implies the_reduction_of Ctfsm1,
the_reduction_of Ctfsm2-are_isomorphic;
::$N Myhill-Nerode theorem
theorem :: FSM_1:66
for M1, M2 being connected reduced finite non empty Mealy-FSM over
IAlph, OAlph holds M1, M2-are_isomorphic iff M1, M2-are_equivalent;