The abstract of the Mizar article:

Minimization of Finite State Machines

by

Miroslava Kaloper, and

Piotr Rudnicki

Received November 18, 1994

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
 (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:17
 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 q_seq be FinSequence of the carrier of fsm;
 pred q_seq is_admissible_for w means
:: 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
<*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:19
   ((q, w)-admissible).(len (q, w)-admissible) = q' iff q, w-leads_to q';

theorem :: FSM_1:20
 for k st 1 <= k & k <= len w1
   holds (q1,w1^w2)-admissible.k = (q1,w1)-admissible.k;

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

theorem :: FSM_1:22
  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:23
 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;

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-leads_to q2t implies
     (q1t,w1^w2)-response = (q1t,w1)-response ^ (q2t,w2)-response;

theorem :: FSM_1:27
   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 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
           (qa, <*s*>^w)-admissible.(i+1) = (qa', w)-admissible.i;

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
               st qai = (qa, w)-admissible.i & qbi = ((qb, w)-admissible.i) &
                  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
   (q,w)-admissible.k in (qr,w)-admissible.k;

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
          holds Tf.((q11,w)-admissible.k) = (Tf.q11,w)-admissible.k;

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
  implies (q11,w)-admissible = (q,w)-admissible;

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
  implies (q21,w)-admissible = (q,w)-admissible;

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;