:: Minimization of finite state machines
:: by Miroslava Kaloper and Piotr Rudnicki
::
:: Received November 18, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

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

definition
let IAlph be set ;
let 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;
existence
 ex b1 being FSM over X st
( not b1 is empty & b1 is finite )
proofend;
end;

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

:: deftheorem  defines -succ_of FSM_1:def_1_:_
 for IAlph being non empty set
for fsm being non empty FSM over IAlph
for s being Element of IAlph
for q being State of fsm holds s -succ_of q = the Tran of fsm . [q,s];

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 :Def2: :: FSM_1:def 2
( it . 1 = q &amp; len it = (len w) + 1 &amp; ( for i being Nat st 1 <= i &amp; i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i &amp; qi = it . i &amp; qi1 = it . (i + 1) &amp; wi -succ_of qi = qi1 ) ) );
existence
 ex b1 being FinSequence of the carrier of fsm st
( b1 . 1 = q &amp; len b1 = (len w) + 1 &amp; ( for i being Nat st 1 <= i &amp; i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i &amp; qi = b1 . i &amp; qi1 = b1 . (i + 1) &amp; wi -succ_of qi = qi1 ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of the carrier of fsm st b1 . 1 = q &amp; len b1 = (len w) + 1 &amp; ( for i being Nat st 1 <= i &amp; i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i &amp; qi = b1 . i &amp; qi1 = b1 . (i + 1) &amp; wi -succ_of qi = qi1 ) ) &amp; b2 . 1 = q &amp; len b2 = (len w) + 1 &amp; ( for i being Nat st 1 <= i &amp; i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i &amp; qi = b2 . i &amp; qi1 = b2 . (i + 1) &amp; wi -succ_of qi = qi1 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines -admissible FSM_1:def_2_:_
 for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm
for w being FinSequence of IAlph
for b5 being FinSequence of the carrier of fsm holds
( b5 = (q,w) -admissible iff ( b5 . 1 = q &amp; len b5 = (len w) + 1 &amp; ( for i being Nat st 1 <= i &amp; i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i &amp; qi = b5 . i &amp; qi1 = b5 . (i + 1) &amp; wi -succ_of qi = qi1 ) ) ) );

theorem Th1: :: FSM_1:1
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm holds (q,(<*> IAlph)) -admissible = <*q*>
proofend;

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;
predq1,w -leads_to q2 means :Def3: :: FSM_1:def 3
((q1,w) -admissible) . ((len w) + 1) = q2;
end;

:: deftheorem Def3 defines -leads_to FSM_1:def_3_:_
 for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w being FinSequence of IAlph
for q1, q2 being State of fsm holds
( q1,w -leads_to q2 iff ((q1,w) -admissible) . ((len w) + 1) = q2 );

theorem Th2: :: FSM_1:2
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm holds q, <*> IAlph -leads_to q
proofend;

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;
predqseq is_admissible_for w means :Def4: :: FSM_1:def 4
 ex q1 being State of fsm st
( q1 = qseq . 1 &amp; (q1,w) -admissible = qseq );
end;

:: deftheorem Def4 defines is_admissible_for FSM_1:def_4_:_
 for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w being FinSequence of IAlph
for qseq being FinSequence of the carrier of fsm holds
( qseq is_admissible_for w iff ex q1 being State of fsm st
( q1 = qseq . 1 &amp; (q1,w) -admissible = qseq ) );

theorem :: FSM_1:3
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm holds <*q*> is_admissible_for <*> IAlph
proofend;

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;
funcq leads_to_under w ->  State of fsm means :Def5: :: FSM_1:def 5
q,w -leads_to it;
existence
 ex b1 being State of fsm st q,w -leads_to b1
proofend;
uniqueness
 for b1, b2 being State of fsm st q,w -leads_to b1 &amp; q,w -leads_to b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines leads_to_under FSM_1:def_5_:_
 for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm
for w being FinSequence of IAlph
for b5 being State of fsm holds
( b5 = q leads_to_under w iff q,w -leads_to b5 );

theorem Th4: :: FSM_1:4
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w being FinSequence of IAlph
for q, q9 being State of fsm holds
( ((q,w) -admissible) . (len ((q,w) -admissible)) = q9 iff q,w -leads_to q9 )
proofend;

theorem Th5: :: FSM_1:5
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1 being State of fsm
for k being Element of NAT st 1 <= k &amp; k <= len w1 holds
((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k
proofend;

theorem Th6: :: FSM_1:6
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
proofend;

theorem Th7: :: FSM_1:7
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
for k being Element of NAT st 1 <= k &amp; k <= (len w2) + 1 holds
((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k
proofend;

theorem Th8: :: FSM_1:8
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
(q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)
proofend;

begin

definition
let IAlph be set ;
let OAlph be non empty set ;
attrc3 is strict ;
struct Mealy-FSM over IAlph,OAlph ->  FSM over IAlph;
aggrMealy-FSM(# carrier, Tran, OFun, InitS #) ->  Mealy-FSM over IAlph,OAlph;
sel OFun c3 ->  Function of [: the carrier of c3,IAlph:],OAlph;
attrc3 is strict ;
struct Moore-FSM over IAlph,OAlph ->  FSM over IAlph;
aggrMoore-FSM(# carrier, Tran, OFun, InitS #) ->  Moore-FSM over IAlph,OAlph;
sel OFun c3 ->  Function of the carrier of c3,OAlph;
end;

registration
let IAlph be set ;
let X be non empty finite set ;
let T be Function of [:X,IAlph:],X;
let I be Element of X;
cluster FSM(# X,T,I #) ->  non empty finite ;
coherence
 ( FSM(# X,T,I #) is finite &amp; not FSM(# X,T,I #) is empty ) ;
end;

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

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

registration
let IAlph be set ;
let OAlph be non empty set ;
cluster non empty finite for Mealy-FSM over IAlph,OAlph;
existence
 ex b1 being Mealy-FSM over IAlph,OAlph st
( b1 is finite &amp; not b1 is empty )
proofend;
cluster non empty finite for Moore-FSM over IAlph,OAlph;
existence
 ex b1 being Moore-FSM over IAlph,OAlph st
( b1 is finite &amp; not b1 is empty )
proofend;
end;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let qt be State of tfsm;
let w be FinSequence of IAlph;
func(qt,w) -response  ->  FinSequence of OAlph means :Def6: :: FSM_1:def 6
( len it = len w &amp; ( for i being Element of NAT st i in dom w holds
it . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) );
existence
 ex b1 being FinSequence of OAlph st
( len b1 = len w &amp; ( for i being Element of NAT st i in dom w holds
b1 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of OAlph st len b1 = len w &amp; ( for i being Element of NAT st i in dom w holds
b1 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) &amp; len b2 = len w &amp; ( for i being Element of NAT st i in dom w holds
b2 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines -response FSM_1:def_6_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qt being State of tfsm
for w being FinSequence of IAlph
for b6 being FinSequence of OAlph holds
( b6 = (qt,w) -response iff ( len b6 = len w &amp; ( for i being Element of NAT st i in dom w holds
b6 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) ) );

theorem Th9: :: FSM_1:9
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qt being State of tfsm holds (qt,(<*> IAlph)) -response = <*> OAlph
proofend;

definition
let IAlph, OAlph be non empty set ;
let sfsm be non empty Moore-FSM over IAlph,OAlph;
let qs be State of sfsm;
let w be FinSequence of IAlph;
func(qs,w) -response  ->  FinSequence of OAlph means :Def7: :: FSM_1:def 7
( len it = (len w) + 1 &amp; ( for i being Element of NAT st i in Seg ((len w) + 1) holds
it . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) );
existence
 ex b1 being FinSequence of OAlph st
( len b1 = (len w) + 1 &amp; ( for i being Element of NAT st i in Seg ((len w) + 1) holds
b1 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of OAlph st len b1 = (len w) + 1 &amp; ( for i being Element of NAT st i in Seg ((len w) + 1) holds
b1 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) &amp; len b2 = (len w) + 1 &amp; ( for i being Element of NAT st i in Seg ((len w) + 1) holds
b2 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines -response FSM_1:def_7_:_
 for IAlph, OAlph being non empty set
for sfsm being non empty Moore-FSM over IAlph,OAlph
for qs being State of sfsm
for w being FinSequence of IAlph
for b6 being FinSequence of OAlph holds
( b6 = (qs,w) -response iff ( len b6 = (len w) + 1 &amp; ( for i being Element of NAT st i in Seg ((len w) + 1) holds
b6 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) ) );

theorem Th10: :: FSM_1:10
for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for sfsm being non empty Moore-FSM over IAlph,OAlph
for qs being State of sfsm holds ((qs,w) -response) . 1 = the OFun of sfsm . qs
proofend;

theorem Th11: :: FSM_1:11
for IAlph, OAlph being non empty set
for w1, w2 being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
proofend;

theorem Th12: :: FSM_1:12
for IAlph, OAlph being non empty set
for w1, w2 being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11, q12 being State of tfsm1
for q21, q22 being State of tfsm2 st q11,w1 -leads_to q12 &amp; q21,w1 -leads_to q22 &amp; (q12,w2) -response <> (q22,w2) -response holds
(q11,(w1 ^ w2)) -response <> (q21,(w1 ^ w2)) -response
proofend;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let sfsm be non empty Moore-FSM over IAlph,OAlph;
predtfsm 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;

:: deftheorem  defines is_similar_to FSM_1:def_8_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for sfsm being non empty Moore-FSM over IAlph,OAlph holds
( tfsm is_similar_to sfsm iff 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 );

theorem :: FSM_1:13
for IAlph, OAlph being non empty set
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
proofend;

theorem :: FSM_1:14
for IAlph being non empty set
for OAlphf being non empty finite set
for tfsmf being non empty finite Mealy-FSM over IAlph,OAlphf ex sfsmf being non empty finite Moore-FSM over IAlph,OAlphf st tfsmf is_similar_to sfsmf
proofend;

begin

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

:: deftheorem Def9 defines -are_equivalent FSM_1:def_9_:_
 for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph holds
( tfsm1,tfsm2 -are_equivalent iff for w being FinSequence of IAlph holds ( the InitS of tfsm1,w) -response = ( the InitS of tfsm2,w) -response );

theorem Th15: :: FSM_1:15
for IAlph, OAlph being non empty set
for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM over IAlph,OAlph st tfsm1,tfsm2 -are_equivalent &amp; tfsm2,tfsm3 -are_equivalent holds
tfsm1,tfsm3 -are_equivalent
proofend;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let qa, qb be State of tfsm;
predqa,qb -are_equivalent  means :Def10: :: FSM_1:def 10
 for w being FinSequence of IAlph holds (qa,w) -response = (qb,w) -response ;
reflexivity
 for qa being State of tfsm
for w being FinSequence of IAlph holds (qa,w) -response = (qa,w) -response ;
symmetry
 for qa, qb being State of tfsm st ( for w being FinSequence of IAlph holds (qa,w) -response = (qb,w) -response ) holds
for w being FinSequence of IAlph holds (qb,w) -response = (qa,w) -response ;
end;

:: deftheorem Def10 defines -are_equivalent FSM_1:def_10_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm holds
( qa,qb -are_equivalent iff for w being FinSequence of IAlph holds (qa,w) -response = (qb,w) -response );

theorem :: FSM_1:16
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1, q2, q3 being State of tfsm st q1,q2 -are_equivalent &amp; q2,q3 -are_equivalent holds
q1,q3 -are_equivalent
proofend;

theorem Th17: :: FSM_1:17
for IAlph, OAlph being non empty set
for s being Element of IAlph
for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa9, qa being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
for i being Element of NAT st i in Seg ((len w) + 1) holds
((qa,(<*s*> ^ w)) -admissible) . (i + 1) = ((qa9,w) -admissible) . i
proofend;

theorem Th18: :: FSM_1:18
for IAlph, OAlph being non empty set
for s being Element of IAlph
for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa9, qa being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
proofend;

theorem Th19: :: FSM_1:19
for OAlph, IAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm holds
( qa,qb -are_equivalent iff for s being Element of IAlph holds
( the OFun of tfsm . [qa,s] = the OFun of tfsm . [qb,s] &amp; the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] -are_equivalent ) )
proofend;

theorem :: FSM_1:20
for OAlph, IAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Element of NAT st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i &amp; qbi = ((qb,w) -admissible) . i &amp; qai,qbi -are_equivalent )
proofend;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let qa, qb be State of tfsm;
let k be Nat;
predk -equivalent qa,qb means :Def11: :: FSM_1:def 11
 for w being FinSequence of IAlph st len w <= k holds
(qa,w) -response = (qb,w) -response ;
end;

:: deftheorem Def11 defines -equivalent FSM_1:def_11_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k being Nat holds
( k -equivalent qa,qb iff for w being FinSequence of IAlph st len w <= k holds
(qa,w) -response = (qb,w) -response );

theorem Th21: :: FSM_1:21
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa being State of tfsm
for k being Nat holds k -equivalent qa,qa
proofend;

theorem Th22: :: FSM_1:22
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k being Nat st k -equivalent qa,qb holds
k -equivalent qb,qa
proofend;

theorem Th23: :: FSM_1:23
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb, qc being State of tfsm
for k being Nat st k -equivalent qa,qb &amp; k -equivalent qb,qc holds
k -equivalent qa,qc
proofend;

theorem Th24: :: FSM_1:24
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
k -equivalent qa,qb
proofend;

theorem Th25: :: FSM_1:25
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm holds 0 -equivalent qa,qb
proofend;

theorem Th26: :: FSM_1:26
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k, m being Nat st k + m -equivalent qa,qb holds
k -equivalent qa,qb
proofend;

theorem Th27: :: FSM_1:27
for OAlph, IAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k being Nat st 1 <= k holds
( k -equivalent qa,qb iff ( 1 -equivalent qa,qb &amp; ( for s being Element of IAlph
for k1 being Element of NAT st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) )
proofend;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let i be Nat;
funci -eq_states_EqR tfsm ->  Equivalence_Relation of the carrier of tfsm means :Def12: :: FSM_1:def 12
 for qa, qb being State of tfsm holds
( [qa,qb] in it iff i -equivalent qa,qb );
existence
 ex b1 being Equivalence_Relation of the carrier of tfsm st
for qa, qb being State of tfsm holds
( [qa,qb] in b1 iff i -equivalent qa,qb )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of the carrier of tfsm st ( for qa, qb being State of tfsm holds
( [qa,qb] in b1 iff i -equivalent qa,qb ) ) &amp; ( for qa, qb being State of tfsm holds
( [qa,qb] in b2 iff i -equivalent qa,qb ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines -eq_states_EqR FSM_1:def_12_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for i being Nat
for b5 being Equivalence_Relation of the carrier of tfsm holds
( b5 = i -eq_states_EqR tfsm iff for qa, qb being State of tfsm holds
( [qa,qb] in b5 iff i -equivalent qa,qb ) );

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

:: deftheorem  defines -eq_states_partition FSM_1:def_13_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for i being Nat holds i -eq_states_partition tfsm = Class (i -eq_states_EqR tfsm);

theorem Th28: :: FSM_1:28
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
proofend;

theorem Th29: :: FSM_1:29
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for k being Nat st Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) holds
for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
proofend;

theorem :: FSM_1:30
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
for m being Element of NAT holds (k + m) -eq_states_partition tfsm = k -eq_states_partition tfsm by Th29;

theorem Th31: :: FSM_1:31
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Element of NAT st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm
proofend;

theorem Th32: :: FSM_1:32
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty finite 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) )
proofend;

theorem Th33: :: FSM_1:33
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q being State of tfsm holds Class ((0 -eq_states_EqR tfsm),q) = the carrier of tfsm
proofend;

theorem :: FSM_1:34
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph holds 0 -eq_states_partition tfsm = { the carrier of tfsm}
proofend;

theorem Th35: :: FSM_1:35
for n being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty finite 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
proofend;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let IT be a_partition of the carrier of tfsm;
attrIT is final  means :Def14: :: 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 &amp; qb in X ) );
end;

:: deftheorem Def14 defines final FSM_1:def_14_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for IT being a_partition of the carrier of tfsm holds
( IT is final iff for qa, qb being State of tfsm holds
( qa,qb -are_equivalent iff ex X being Element of IT st
( qa in X &amp; qb in X ) ) );

theorem :: FSM_1:36
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st k -eq_states_partition tfsm is final holds
(k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm
proofend;

theorem Th37: :: FSM_1:37
for k being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
k -eq_states_partition tfsm is final
proofend;

theorem :: FSM_1:38
for n being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph st n + 1 = card the carrier of tfsm holds
ex k being Element of NAT st
( k <= n &amp; k -eq_states_partition tfsm is final )
proofend;

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;
func final_states_partition tfsm ->  a_partition of the carrier of tfsm means :Def15: :: FSM_1:def 15
it is final ;
existence
 ex b1 being a_partition of the carrier of tfsm st b1 is final
proofend;
uniqueness
 for b1, b2 being a_partition of the carrier of tfsm st b1 is final &amp; b2 is final holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines final_states_partition FSM_1:def_15_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for b4 being a_partition of the carrier of tfsm holds
( b4 = final_states_partition tfsm iff b4 is final );

theorem Th39: :: FSM_1:39
for n being Element of NAT
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph st n + 1 = card the carrier of tfsm holds
final_states_partition tfsm = n -eq_states_partition tfsm
proofend;

begin

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite 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 :Def16: :: FSM_1:def 16
 ex q being State of tfsm ex n being Element of NAT st
( q in qf &amp; n + 1 = card the carrier of tfsm &amp; it = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) );
existence
 ex b1 being Element of final_states_partition tfsm ex q being State of tfsm ex n being Element of NAT st
( q in qf &amp; n + 1 = card the carrier of tfsm &amp; b1 = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) )
proofend;
uniqueness
 for b1, b2 being Element of final_states_partition tfsm st ex q being State of tfsm ex n being Element of NAT st
( q in qf &amp; n + 1 = card the carrier of tfsm &amp; b1 = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) ) &amp; ex q being State of tfsm ex n being Element of NAT st
( q in qf &amp; n + 1 = card the carrier of tfsm &amp; b2 = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines -succ_class FSM_1:def_16_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for qf being Element of final_states_partition tfsm
for s being Element of IAlph
for b6 being Element of final_states_partition tfsm holds
( b6 = (s,qf) -succ_class iff ex q being State of tfsm ex n being Element of NAT st
( q in qf &amp; n + 1 = card the carrier of tfsm &amp; b6 = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) ) );

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;
let qf be Element of final_states_partition tfsm;
let s be Element of IAlph;
func(qf,s) -class_response  ->  Element of OAlph means :Def17: :: FSM_1:def 17
 ex q being State of tfsm st
( q in qf &amp; it = the OFun of tfsm . [q,s] );
existence
 ex b1 being Element of OAlph ex q being State of tfsm st
( q in qf &amp; b1 = the OFun of tfsm . [q,s] )
proofend;
uniqueness
 for b1, b2 being Element of OAlph st ex q being State of tfsm st
( q in qf &amp; b1 = the OFun of tfsm . [q,s] ) &amp; ex q being State of tfsm st
( q in qf &amp; b2 = the OFun of tfsm . [q,s] ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines -class_response FSM_1:def_17_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for qf being Element of final_states_partition tfsm
for s being Element of IAlph
for b6 being Element of OAlph holds
( b6 = (qf,s) -class_response iff ex q being State of tfsm st
( q in qf &amp; b6 = the OFun of tfsm . [q,s] ) );

definition
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;
func the_reduction_of tfsm ->  strict Mealy-FSM over IAlph,OAlph means :Def18: :: FSM_1:def 18
( the carrier of it = final_states_partition tfsm &amp; ( 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) &amp; the OFun of tfsm . (q,s) = the OFun of it . (Q,s) ) ) &amp; the InitS of tfsm in the InitS of it );
existence
 ex b1 being strict Mealy-FSM over IAlph,OAlph st
( the carrier of b1 = final_states_partition tfsm &amp; ( for Q being State of b1
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 b1 . (Q,s) &amp; the OFun of tfsm . (q,s) = the OFun of b1 . (Q,s) ) ) &amp; the InitS of tfsm in the InitS of b1 )
proofend;
uniqueness
 for b1, b2 being strict Mealy-FSM over IAlph,OAlph st the carrier of b1 = final_states_partition tfsm &amp; ( for Q being State of b1
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 b1 . (Q,s) &amp; the OFun of tfsm . (q,s) = the OFun of b1 . (Q,s) ) ) &amp; the InitS of tfsm in the InitS of b1 &amp; the carrier of b2 = final_states_partition tfsm &amp; ( for Q being State of b2
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 b2 . (Q,s) &amp; the OFun of tfsm . (q,s) = the OFun of b2 . (Q,s) ) ) &amp; the InitS of tfsm in the InitS of b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines the_reduction_of FSM_1:def_18_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for b4 being strict Mealy-FSM over IAlph,OAlph holds
( b4 = the_reduction_of tfsm iff ( the carrier of b4 = final_states_partition tfsm &amp; ( for Q being State of b4
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 b4 . (Q,s) &amp; the OFun of tfsm . (q,s) = the OFun of b4 . (Q,s) ) ) &amp; the InitS of tfsm in the InitS of b4 ) );

registration
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;
cluster the_reduction_of tfsm ->  non empty finite strict ;
coherence
 ( not the_reduction_of tfsm is empty &amp; the_reduction_of tfsm is finite )
proofend;
end;

theorem Th40: :: FSM_1:40
for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for rtfsm, tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm
for qr being State of rtfsm st rtfsm = the_reduction_of tfsm &amp; q in qr holds
for k being Element of NAT st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
proofend;

theorem Th41: :: FSM_1:41
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds tfsm, the_reduction_of tfsm -are_equivalent
proofend;

begin

definition
let IAlph, OAlph be non empty set ;
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph;
predtfsm1,tfsm2 -are_isomorphic  means :Def19: :: FSM_1:def 19
 ex Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st
( Tf is bijective &amp; Tf . the InitS of tfsm1 = the InitS of tfsm2 &amp; ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm1 . (q11,s)) = the Tran of tfsm2 . ((Tf . q11),s) &amp; the OFun of tfsm1 . (q11,s) = the OFun of tfsm2 . ((Tf . q11),s) ) ) );
reflexivity
 for tfsm1 being non empty Mealy-FSM over IAlph,OAlph ex Tf being Function of the carrier of tfsm1, the carrier of tfsm1 st
( Tf is bijective &amp; Tf . the InitS of tfsm1 = the InitS of tfsm1 &amp; ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm1 . (q11,s)) = the Tran of tfsm1 . ((Tf . q11),s) &amp; the OFun of tfsm1 . (q11,s) = the OFun of tfsm1 . ((Tf . q11),s) ) ) )
proofend;
symmetry
 for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph st ex Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st
( Tf is bijective &amp; Tf . the InitS of tfsm1 = the InitS of tfsm2 &amp; ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm1 . (q11,s)) = the Tran of tfsm2 . ((Tf . q11),s) &amp; the OFun of tfsm1 . (q11,s) = the OFun of tfsm2 . ((Tf . q11),s) ) ) ) holds
ex Tf being Function of the carrier of tfsm2, the carrier of tfsm1 st
( Tf is bijective &amp; Tf . the InitS of tfsm2 = the InitS of tfsm1 &amp; ( for q11 being State of tfsm2
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm2 . (q11,s)) = the Tran of tfsm1 . ((Tf . q11),s) &amp; the OFun of tfsm2 . (q11,s) = the OFun of tfsm1 . ((Tf . q11),s) ) ) )
proofend;
end;

:: deftheorem Def19 defines -are_isomorphic FSM_1:def_19_:_
 for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph holds
( tfsm1,tfsm2 -are_isomorphic iff ex Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st
( Tf is bijective &amp; Tf . the InitS of tfsm1 = the InitS of tfsm2 &amp; ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm1 . (q11,s)) = the Tran of tfsm2 . ((Tf . q11),s) &amp; the OFun of tfsm1 . (q11,s) = the OFun of tfsm2 . ((Tf . q11),s) ) ) ) );

theorem Th42: :: FSM_1:42
for IAlph, OAlph being non empty set
for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM over IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic &amp; tfsm2,tfsm3 -are_isomorphic holds
tfsm1,tfsm3 -are_isomorphic
proofend;

theorem Th43: :: FSM_1:43
for OAlph, IAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Element of NAT st 1 <= k &amp; k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
proofend;

theorem Th44: :: FSM_1:44
for OAlph, IAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11, q12 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds
( Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) &amp; the OFun of tfsm1 . (q,s) = the OFun of tfsm2 . ((Tf . q),s) ) ) holds
( q11,q12 -are_equivalent iff Tf . q11,Tf . q12 -are_equivalent )
proofend;

theorem Th45: :: FSM_1:45
for IAlph, OAlph being non empty set
for rtfsm, tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for qr1, qr2 being State of rtfsm st rtfsm = the_reduction_of tfsm &amp; qr1 <> qr2 holds
not qr1,qr2 -are_equivalent
proofend;

begin

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

:: deftheorem Def20 defines reduced FSM_1:def_20_:_
 for IAlph, OAlph being non empty set
for IT being non empty Mealy-FSM over IAlph,OAlph holds
( IT is reduced iff for qa, qb being State of IT st qa <> qb holds
not qa,qb -are_equivalent );

registration
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;
cluster the_reduction_of tfsm ->  strict reduced ;
coherence
 the_reduction_of tfsm is reduced
proofend;
end;

registration
let IAlph, OAlph be non empty set ;
cluster non empty finite reduced for Mealy-FSM over IAlph,OAlph;
existence
 ex b1 being non empty Mealy-FSM over IAlph,OAlph st
( b1 is reduced &amp; b1 is finite )
proofend;
end;

theorem Th46: :: FSM_1:46
for IAlph, OAlph being non empty set
for Rtfsm being non empty finite reduced Mealy-FSM over IAlph,OAlph holds Rtfsm, the_reduction_of Rtfsm -are_isomorphic
proofend;

theorem Th47: :: FSM_1:47
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( tfsm is reduced iff ex M being non empty finite Mealy-FSM over IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic )
proofend;

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

:: deftheorem Def21 defines accessible FSM_1:def_21_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for IT being State of tfsm holds
( IT is accessible iff ex w being FinSequence of IAlph st the InitS of tfsm,w -leads_to IT );

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

:: deftheorem Def22 defines connected FSM_1:def_22_:_
 for IAlph, OAlph being non empty set
for IT being non empty Mealy-FSM over IAlph,OAlph holds
( IT is connected iff for q being State of IT holds q is accessible );

registration
let IAlph, OAlph be non empty set ;
cluster non empty finite connected for Mealy-FSM over IAlph,OAlph;
existence
 ex b1 being non empty finite Mealy-FSM over IAlph,OAlph st b1 is connected
proofend;
end;

registration
let IAlph, OAlph be non empty set ;
let Ctfsm be non empty finite connected Mealy-FSM over IAlph,OAlph;
cluster the_reduction_of Ctfsm ->  strict connected ;
coherence
 the_reduction_of Ctfsm is connected
proofend;
end;

registration
let IAlph, OAlph be non empty set ;
cluster non empty finite reduced connected for Mealy-FSM over IAlph,OAlph;
existence
 ex b1 being non empty Mealy-FSM over IAlph,OAlph st
( b1 is connected &amp; b1 is reduced &amp; b1 is finite )
proofend;
end;

definition
let IAlph, OAlph be non empty set ;
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  }  ;
coherence
  {  q where q is State of tfsm : q is accessible  }  is set ;
end;

:: deftheorem  defines accessibleStates FSM_1:def_23_:_
 for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph holds accessibleStates tfsm =  {  q where q is State of tfsm : q is accessible  }  ;

registration
let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;
cluster accessibleStates tfsm ->  non empty finite ;
coherence
 ( accessibleStates tfsm is finite &amp; not accessibleStates tfsm is empty )
proofend;
end;

theorem Th48: :: FSM_1:48
for OAlph, IAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds
( accessibleStates tfsm c= the carrier of tfsm &amp; ( for q being State of tfsm holds
( q in accessibleStates tfsm iff q is accessible ) ) )
proofend;

theorem Th49: :: FSM_1:49
for OAlph, IAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
proofend;

theorem :: FSM_1:50
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for cTran being Function of [:(accessibleStates tfsm),IAlph:],(accessibleStates tfsm)
for cOFun being Function of [:(accessibleStates tfsm),IAlph:],OAlph
for cInitS being Element of accessibleStates tfsm st cTran = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] &amp; cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] &amp; cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent
proofend;

theorem :: FSM_1:51
for OAlph, IAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph ex Ctfsm being non empty finite connected Mealy-FSM over IAlph,OAlph st
( the Tran of Ctfsm = the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] &amp; the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] &amp; the InitS of Ctfsm = the InitS of tfsm &amp; tfsm,Ctfsm -are_equivalent )
proofend;

begin

definition
let IAlph be set ;
let OAlph be non empty set ;
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph;
functfsm1 -Mealy_union tfsm2 ->  strict Mealy-FSM over IAlph,OAlph means :Def24: :: FSM_1:def 24
( the carrier of it = the carrier of tfsm1 \/ the carrier of tfsm2 &amp; the Tran of it = the Tran of tfsm1 +* the Tran of tfsm2 &amp; the OFun of it = the OFun of tfsm1 +* the OFun of tfsm2 &amp; the InitS of it = the InitS of tfsm1 );
existence
 ex b1 being strict Mealy-FSM over IAlph,OAlph st
( the carrier of b1 = the carrier of tfsm1 \/ the carrier of tfsm2 &amp; the Tran of b1 = the Tran of tfsm1 +* the Tran of tfsm2 &amp; the OFun of b1 = the OFun of tfsm1 +* the OFun of tfsm2 &amp; the InitS of b1 = the InitS of tfsm1 )
proofend;
uniqueness
 for b1, b2 being strict Mealy-FSM over IAlph,OAlph st the carrier of b1 = the carrier of tfsm1 \/ the carrier of tfsm2 &amp; the Tran of b1 = the Tran of tfsm1 +* the Tran of tfsm2 &amp; the OFun of b1 = the OFun of tfsm1 +* the OFun of tfsm2 &amp; the InitS of b1 = the InitS of tfsm1 &amp; the carrier of b2 = the carrier of tfsm1 \/ the carrier of tfsm2 &amp; the Tran of b2 = the Tran of tfsm1 +* the Tran of tfsm2 &amp; the OFun of b2 = the OFun of tfsm1 +* the OFun of tfsm2 &amp; the InitS of b2 = the InitS of tfsm1 holds
b1 = b2 ;
end;

:: deftheorem Def24 defines -Mealy_union FSM_1:def_24_:_
 for IAlph being set
for OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for b5 being strict Mealy-FSM over IAlph,OAlph holds
( b5 = tfsm1 -Mealy_union tfsm2 iff ( the carrier of b5 = the carrier of tfsm1 \/ the carrier of tfsm2 &amp; the Tran of b5 = the Tran of tfsm1 +* the Tran of tfsm2 &amp; the OFun of b5 = the OFun of tfsm1 +* the OFun of tfsm2 &amp; the InitS of b5 = the InitS of tfsm1 ) );

registration
let IAlph be set ;
let OAlph be non empty set ;
let tfsm1, tfsm2 be non empty finite Mealy-FSM over IAlph,OAlph;
clustertfsm1 -Mealy_union tfsm2 ->  non empty finite strict ;
coherence
 ( not tfsm1 -Mealy_union tfsm2 is empty &amp; tfsm1 -Mealy_union tfsm2 is finite )
proofend;
end;

theorem Th52: :: FSM_1:52
for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 &amp; the carrier of tfsm1 misses the carrier of tfsm2 &amp; q11 = q holds
(q11,w) -admissible = (q,w) -admissible
proofend;

theorem Th53: :: FSM_1:53
for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 &amp; the carrier of tfsm1 misses the carrier of tfsm2 &amp; q11 = q holds
(q11,w) -response = (q,w) -response
proofend;

theorem Th54: :: FSM_1:54
for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 &amp; q21 = q holds
(q21,w) -admissible = (q,w) -admissible
proofend;

theorem Th55: :: FSM_1:55
for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 &amp; q21 = q holds
(q21,w) -response = (q,w) -response
proofend;

theorem Th56: :: FSM_1:56
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for Rtfsm1, Rtfsm2 being non empty reduced Mealy-FSM over IAlph,OAlph st tfsm = Rtfsm1 -Mealy_union Rtfsm2 &amp; the carrier of Rtfsm1 misses the carrier of Rtfsm2 &amp; Rtfsm1,Rtfsm2 -are_equivalent holds
ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q &amp; the InitS of Rtfsm2 in Q &amp; Q = the InitS of (the_reduction_of tfsm) )
proofend;

theorem Th57: :: FSM_1:57
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty reduced connected Mealy-FSM over IAlph,OAlph
for q1u, q2u being State of tfsm
for crq11, crq12 being State of CRtfsm1 st crq11 = q1u &amp; crq12 = q2u &amp; the carrier of CRtfsm1 misses the carrier of CRtfsm2 &amp; tfsm = CRtfsm1 -Mealy_union CRtfsm2 &amp; not crq11,crq12 -are_equivalent holds
not q1u,q2u -are_equivalent
proofend;

theorem Th58: :: FSM_1:58
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm2, CRtfsm1 being non empty reduced connected Mealy-FSM over IAlph,OAlph
for q1u, q2u being State of tfsm
for crq21, crq22 being State of CRtfsm2 st crq21 = q1u &amp; crq22 = q2u &amp; tfsm = CRtfsm1 -Mealy_union CRtfsm2 &amp; not crq21,crq22 -are_equivalent holds
not q1u,q2u -are_equivalent
proofend;

theorem Th59: :: FSM_1:59
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 &amp; tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 )
proofend;

theorem Th60: :: FSM_1:60
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm2 or not q2 in the carrier of CRtfsm2 or not q1 <> q2 )
proofend;

theorem Th61: :: FSM_1:61
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 &amp; CRtfsm1,CRtfsm2 -are_equivalent &amp; tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm) ex q1, q2 being Element of Q st
( q1 in the carrier of CRtfsm1 &amp; q2 in the carrier of CRtfsm2 &amp; ( for q being Element of Q holds
( q = q1 or q = q2 ) ) )
proofend;

begin

theorem Th62: :: FSM_1:62
for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty finite Mealy-FSM over IAlph,OAlph ex fsm1, fsm2 being non empty finite Mealy-FSM over IAlph,OAlph st
( the carrier of fsm1 misses the carrier of fsm2 &amp; fsm1,tfsm1 -are_isomorphic &amp; fsm2,tfsm2 -are_isomorphic )
proofend;

theorem Th63: :: FSM_1:63
for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic holds
tfsm1,tfsm2 -are_equivalent
proofend;

theorem Th64: :: FSM_1:64
for IAlph, OAlph being non empty set
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 &amp; CRtfsm1,CRtfsm2 -are_equivalent holds
CRtfsm1,CRtfsm2 -are_isomorphic
proofend;

theorem Th65: :: FSM_1:65
for IAlph, OAlph being non empty set
for Ctfsm1, Ctfsm2 being non empty finite connected Mealy-FSM over IAlph,OAlph st Ctfsm1,Ctfsm2 -are_equivalent holds
the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic
proofend;

:: [WP: ] Myhill-Nerode_theorem
theorem :: FSM_1:66
for IAlph, OAlph being non empty set
for M1, M2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph holds
( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )
proofend;