:: FSM_1 semantic presentation

theorem Th1: :: FSM_1:1

for m, n being Nat st m < n holds
ex p being Nat st
( n = m + p & 1 <= p )

proof end;

theorem :: FSM_1:2

canceled;

theorem :: FSM_1:3

canceled;

theorem :: FSM_1:4

canceled;

theorem :: FSM_1:5

canceled;

theorem :: FSM_1:6

canceled;

theorem Th7: :: FSM_1:7

for S being set
for D1, D2 being non empty set
for f1 being Function of S,D1
for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds
f2 * f1 is bijective

proof end;

theorem Th8: :: FSM_1:8

for Y being set
for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds
E1 = E2

proof end;

theorem :: FSM_1:9

for W being non empty set
for PW being a_partition of W holds not PW is empty ;

theorem Th10: :: FSM_1:10

for Z being finite set
for PZ being a_partition of Z holds PZ is finite

proof end;

registration

let Z be finite set ;
cluster -> finite a_partition of Z;
coherence by Th10;

end;

registration

let X be non empty finite set ;
cluster non empty finite a_partition of X;
existence

proof end;

end;

theorem Th11: :: FSM_1:11

for X being non empty set
for PX being a_partition of X
for Pi being set st Pi in PX holds
ex x being Element of X st x in Pi

proof end;

theorem Th12: :: FSM_1:12

for X being non empty finite set
for PX being a_partition of X holds card PX <= card X

proof end;

theorem Th13: :: FSM_1:13

for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds
card PA2 <= card PA1

proof end;

theorem Th14: :: FSM_1:14

for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds
for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2

proof end;

theorem Th15: :: FSM_1:15

for A being non empty finite set
for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds
PA1 = PA2

proof end;

definition

let IAlph be set ;
attr c₂ is strict;
struct FSM of IAlph -> 1-sorted ;
aggr FSM(# carrier, Tran, InitS #) -> FSM of IAlph;
sel Tran c₂ -> Function of [:the carrier of c₂,IAlph:],the carrier of c₂;
sel InitS c₂ -> Element of the carrier of c₂;

end;

definition

let IAlph be set ;
let fsm be FSM of IAlph;
mode State of fsm is Element of fsm;

end;

registration

let X be set ;
cluster non empty finite FSM of X;
existence

proof end;

end;

registration

cluster non empty finite 1-sorted ;
existence

proof end;

end;

registration

let S be finite 1-sorted ;
cluster the carrier of S -> finite ;
coherence by GROUP_1:def 14;

end;

definition

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

end;

:: deftheorem defines -succ_of FSM_1:def 1 :

definition

let IAlph be non empty set ;
let fsm be non empty FSM of 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 & len it = (len w) + 1 & ( for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = it . i & qi1 = it . (i + 1) & wi -succ_of qi = qi1 ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines -admissible FSM_1:def 2 :

theorem Th16: :: FSM_1:16

for IAlph being non empty set
for fsm being non empty FSM of IAlph
for q being State of fsm holds q,(<*> IAlph) -admissible = <*q*>

proof end;

definition

let IAlph be non empty set ;
let fsm be non empty FSM of IAlph;
let w be FinSequence of IAlph;
let q1, q2 be State of fsm;
pred q1,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 :

theorem Th17: :: FSM_1:17

for IAlph being non empty set
for fsm being non empty FSM of IAlph
for q being State of fsm holds q, <*> IAlph -leads_to q

proof end;

definition

let IAlph be non empty set ;
let fsm be non empty FSM of IAlph;
let w be FinSequence of IAlph;
let qseq be FinSequence of the carrier of fsm;
pred qseq is_admissible_for w means :Def4: :: FSM_1:def 4
ex q1 being State of fsm st
( q1 = qseq . 1 & q1,w -admissible = qseq );

end;

:: deftheorem Def4 defines is_admissible_for FSM_1:def 4 :

theorem :: FSM_1:18

for IAlph being non empty set
for fsm being non empty FSM of IAlph
for q being State of fsm holds <*q*> is_admissible_for <*> IAlph

proof end;

definition

let IAlph be non empty set ;
let fsm be non empty FSM of IAlph;
let q be State of fsm;
let w be FinSequence of IAlph;
func q leads_to_under w -> State of fsm means :Def5: :: FSM_1:def 5
q,w -leads_to it;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines leads_to_under FSM_1:def 5 :

theorem Th19: :: FSM_1:19

for IAlph being non empty set
for fsm being non empty FSM of IAlph
for w being FinSequence of IAlph
for q, q' being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q' iff q,w -leads_to q' )

proof end;

theorem Th20: :: FSM_1:20

for IAlph being non empty set
for fsm being non empty FSM of IAlph
for w1, w2 being FinSequence of IAlph
for q1 being State of fsm
for k being Nat st 1 <= k & k <= len w1 holds
(q1,(w1 ^ w2) -admissible ) . k = (q1,w1 -admissible ) . k

proof end;

theorem Th21: :: FSM_1:21

for IAlph being non empty set
for fsm being non empty FSM of 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

proof end;

theorem Th22: :: FSM_1:22

for IAlph being non empty set
for fsm being non empty FSM of 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 Nat st 1 <= k & k <= (len w2) + 1 holds
(q1,(w1 ^ w2) -admissible ) . ((len w1) + k) = (q2,w2 -admissible ) . k

proof end;

theorem Th23: :: FSM_1:23

for IAlph being non empty set
for fsm being non empty FSM of 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 )

proof end;

definition

let IAlph be set ;
let OAlph be non empty set ;
attr c₃ is strict;
struct Mealy-FSM of IAlph,OAlph -> FSM of IAlph;
aggr Mealy-FSM(# carrier, Tran, OFun, InitS #) -> Mealy-FSM of IAlph,OAlph;
sel OFun c₃ -> Function of [:the carrier of c₃,IAlph:],OAlph;
attr c₃ is strict;
struct Moore-FSM of IAlph,OAlph -> FSM of IAlph;
aggr Moore-FSM(# carrier, Tran, OFun, InitS #) -> Moore-FSM of IAlph,OAlph;
sel OFun c₃ -> Function of the carrier of c₃,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 by GROUP_1:def 14, STRUCT_0:def 1;

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 by GROUP_1:def 14, STRUCT_0:def 1;

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 by GROUP_1:def 14, STRUCT_0:def 1;

end;

registration

let IAlph be set ;
let OAlph be non empty set ;
cluster non empty finite Mealy-FSM of IAlph,OAlph;
existence

proof end;

cluster non empty finite Moore-FSM of IAlph,OAlph;
existence

proof end;

end;

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM of 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 & ( for i being Nat st i in dom w holds
it . i = the OFun of tfsm . [((qt,w -admissible ) . i),(w . i)] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines -response FSM_1:def 6 :

theorem Th24: :: FSM_1:24

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qt being State of tfsm holds qt,(<*> IAlph) -response = <*> OAlph

proof end;

definition

let IAlph, OAlph be non empty set ;
let sfsm be non empty Moore-FSM of 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 & ( for i being Nat st i in Seg ((len w) + 1) holds
it . i = the OFun of sfsm . ((qs,w -admissible ) . i) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines -response FSM_1:def 7 :

theorem Th25: :: FSM_1:25

for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for sfsm being non empty Moore-FSM of IAlph,OAlph
for qs being State of sfsm holds (qs,w -response ) . 1 = the OFun of sfsm . qs

proof end;

theorem Th26: :: FSM_1:26

for IAlph, OAlph being non empty set
for w1, w2 being FinSequence of IAlph
for tfsm being non empty Mealy-FSM of 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 )

proof end;

theorem Th27: :: FSM_1:27

for IAlph, OAlph being non empty set
for w1, w2 being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11, q12 being State of tfsm1
for q21, q22 being State of tfsm2 st q11,w1 -leads_to q12 & q21,w1 -leads_to q22 & q12,w2 -response <> q22,w2 -response holds
q11,(w1 ^ w2) -response <> q21,(w1 ^ w2) -response

proof end;

definition

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

:: deftheorem defines is_similar_to FSM_1:def 8 :

theorem :: FSM_1:28

for IAlph, OAlph being non empty set
for sfsm being non empty finite Moore-FSM of IAlph,OAlph ex tfsm being non empty finite Mealy-FSM of IAlph,OAlph st tfsm is_similar_to sfsm

proof end;

theorem :: FSM_1:29

for IAlph being non empty set
for OAlphf being non empty finite set
for tfsmf being non empty finite Mealy-FSM of IAlph,OAlphf ex sfsmf being non empty finite Moore-FSM of IAlph,OAlphf st tfsmf is_similar_to sfsmf

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph;
pred tfsm1,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 ;
symmetry ;

end;

:: deftheorem Def9 defines -are_equivalent FSM_1:def 9 :

theorem Th30: :: FSM_1:30

for IAlph, OAlph being non empty set
for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_equivalent & tfsm2,tfsm3 -are_equivalent holds
tfsm1,tfsm3 -are_equivalent

proof end;

definition

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

end;

:: deftheorem Def10 defines -are_equivalent FSM_1:def 10 :

theorem :: FSM_1:31

canceled;

theorem :: FSM_1:32

canceled;

theorem :: FSM_1:33

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for q1, q2, q3 being State of tfsm st q1,q2 -are_equivalent & q2,q3 -are_equivalent holds
q1,q3 -are_equivalent

proof end;

theorem Th34: :: FSM_1:34

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 of IAlph,OAlph
for qa', qa being State of tfsm st qa' = the Tran of tfsm . [qa,s] holds
for i being Nat st i in Seg ((len w) + 1) holds
(qa,(<*s*> ^ w) -admissible ) . (i + 1) = (qa',w -admissible ) . i

proof end;

theorem Th35: :: FSM_1:35

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 of IAlph,OAlph
for qa', qa being State of tfsm st qa' = the Tran of tfsm . [qa,s] holds
qa,(<*s*> ^ w) -response = <*(the OFun of tfsm . [qa,s])*> ^ (qa',w -response )

proof end;

theorem Th36: :: FSM_1:36

for OAlph, IAlph being non empty set
for tfsm being non empty Mealy-FSM of 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] & the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] -are_equivalent ) )

proof end;

theorem :: FSM_1:37

for OAlph, IAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = (qa,w -admissible ) . i & qbi = (qb,w -admissible ) . i & qai,qbi -are_equivalent )

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM of IAlph,OAlph;
let qa, qb be State of tfsm;
let k be Nat;
pred k -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 :

theorem Th38: :: FSM_1:38

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa being State of tfsm holds k -equivalent qa,qa

proof end;

theorem Th39: :: FSM_1:39

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st k -equivalent qa,qb holds
k -equivalent qb,qa

proof end;

theorem Th40: :: FSM_1:40

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb, qc being State of tfsm st k -equivalent qa,qb & k -equivalent qb,qc holds
k -equivalent qa,qc

proof end;

theorem Th41: :: FSM_1:41

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
k -equivalent qa,qb

proof end;

theorem Th42: :: FSM_1:42

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm holds 0 -equivalent qa,qb

proof end;

theorem Th43: :: FSM_1:43

for k, m being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st k + m -equivalent qa,qb holds
k -equivalent qa,qb

proof end;

theorem Th44: :: FSM_1:44

for k being Nat
for OAlph, IAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for qa, qb being State of tfsm st 1 <= k holds
( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] ) ) )

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM of IAlph,OAlph;
let i be Nat;
func i -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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines -eq_states_EqR FSM_1:def 12 :

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM of 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);
coherence ;

end;

:: deftheorem defines -eq_states_partition FSM_1:def 13 :

theorem Th45: :: FSM_1:45

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm

proof end;

theorem Th46: :: FSM_1:46

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph 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)

proof end;

theorem Th47: :: FSM_1:47

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
for m being Nat holds (k + m) -eq_states_partition tfsm = k -eq_states_partition tfsm by Th46;

theorem Th48: :: FSM_1:48

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph st (k + 1) -eq_states_partition tfsm <> k -eq_states_partition tfsm holds
for i being Nat st i <= k holds
(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm

proof end;

theorem Th49: :: FSM_1:49

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of 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) )

proof end;

theorem Th50: :: FSM_1:50

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph
for q being State of tfsm holds Class (0 -eq_states_EqR tfsm),q = the carrier of tfsm

proof end;

theorem Th51: :: FSM_1:51

for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph holds 0 -eq_states_partition tfsm = {the carrier of tfsm}

proof end;

theorem Th52: :: FSM_1:52

for n being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph st n + 1 = card the carrier of tfsm holds
(n + 1) -eq_states_partition tfsm = n -eq_states_partition tfsm

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM of IAlph,OAlph;
let IT be a_partition of the carrier of tfsm;
attr IT 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 & qb in X ) );

end;

:: deftheorem Def14 defines final FSM_1:def 14 :

theorem Th53: :: FSM_1:53

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph st k -eq_states_partition tfsm is final holds
(k + 1) -eq_states_EqR tfsm = k -eq_states_EqR tfsm

proof end;

theorem Th54: :: FSM_1:54

for k being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM of IAlph,OAlph holds
( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm iff k -eq_states_partition tfsm is final )

proof end;

theorem :: FSM_1:55

for n being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of 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 )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines final_states_partition FSM_1:def 15 :

theorem Th56: :: FSM_1:56

for n being Nat
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph st n + 1 = card the carrier of tfsm holds
final_states_partition tfsm = n -eq_states_partition tfsm

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM of 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 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]) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines -succ_class FSM_1:def 16 :

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM of 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 & it = the OFun of tfsm . [q,s] );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines -class_response FSM_1:def 17 :

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph;
func the_reduction_of tfsm -> strict Mealy-FSM of IAlph,OAlph means :Def18: :: FSM_1:def 18
( the carrier of it = final_states_partition tfsm & ( for Q being State of it
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . [q,s] in the Tran of it . [Q,s] & the OFun of tfsm . [q,s] = the OFun of it . [Q,s] ) ) & the InitS of tfsm in the InitS of it );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines the_reduction_of FSM_1:def 18 :

registration

let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph;
cluster the_reduction_of tfsm -> non empty finite strict ;
coherence

proof end;

end;

theorem Th57: :: FSM_1:57

for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for rtfsm, tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm
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

proof end;

theorem Th58: :: FSM_1:58

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds tfsm, the_reduction_of tfsm -are_equivalent

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph;
pred tfsm1,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 & Tf . the InitS of tfsm1 = the InitS of tfsm2 & ( 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] & the OFun of tfsm1 . [q11,s] = the OFun of tfsm2 . [(Tf . q11),s] ) ) );
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def19 defines -are_isomorphic FSM_1:def 19 :

theorem Th59: :: FSM_1:59

for IAlph, OAlph being non empty set
for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic & tfsm2,tfsm3 -are_isomorphic holds
tfsm1,tfsm3 -are_isomorphic

proof end;

theorem Th60: :: FSM_1:60

for OAlph, IAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of 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 Nat st 1 <= k & k <= (len w) + 1 holds
Tf . ((q11,w -admissible ) . k) = ((Tf . q11),w -admissible ) . k

proof end;

theorem Th61: :: FSM_1:61

for OAlph, IAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11, q12 being State of tfsm1
for Tf being Function of the carrier of tfsm1,the carrier of tfsm2 st Tf . the InitS of tfsm1 = the InitS of tfsm2 & ( 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] & 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 )

proof end;

theorem Th62: :: FSM_1:62

for IAlph, OAlph being non empty set
for rtfsm, tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for qr1, qr2 being State of rtfsm st rtfsm = the_reduction_of tfsm & qr1 <> qr2 holds
not qr1,qr2 -are_equivalent

proof end;

definition

let IAlph, OAlph be non empty set ;
let IT be non empty Mealy-FSM of IAlph,OAlph;
attr IT 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 :

theorem Th63: :: FSM_1:63

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds the_reduction_of tfsm is reduced

proof end;

registration

let IAlph, OAlph be non empty set ;
cluster non empty finite reduced Mealy-FSM of IAlph,OAlph;
existence

proof end;

end;

theorem Th64: :: FSM_1:64

for IAlph, OAlph being non empty set
for Rtfsm being non empty finite reduced Mealy-FSM of IAlph,OAlph holds Rtfsm, the_reduction_of Rtfsm -are_isomorphic

proof end;

theorem Th65: :: FSM_1:65

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds
( tfsm is reduced iff ex M being non empty finite Mealy-FSM of IAlph,OAlph st tfsm, the_reduction_of M -are_isomorphic )

proof end;

definition

let IAlph, OAlph be non empty set ;
let tfsm be non empty Mealy-FSM of IAlph,OAlph;
let IT be State of tfsm;
attr IT 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 :

definition

let IAlph, OAlph be non empty set ;
let IT be non empty Mealy-FSM of IAlph,OAlph;
attr IT 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 :

registration

let IAlph, OAlph be non empty set ;
cluster non empty finite connected Mealy-FSM of IAlph,OAlph;
existence

proof end;

end;

theorem Th66: :: FSM_1:66

for IAlph, OAlph being non empty set
for Ctfsm being non empty finite connected Mealy-FSM of IAlph,OAlph holds the_reduction_of Ctfsm is connected

proof end;

registration

let IAlph, OAlph be non empty set ;
cluster non empty finite reduced connected Mealy-FSM of IAlph,OAlph;
existence

proof end;

end;

definition

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

end;

:: deftheorem defines accessibleStates FSM_1:def 23 :

registration

let IAlph, OAlph be non empty set ;
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph;
cluster accessibleStates tfsm -> non empty finite ;
coherence

proof end;

end;

theorem Th67: :: FSM_1:67

for OAlph, IAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds
( accessibleStates tfsm c= the carrier of tfsm & ( for q being State of tfsm holds
( q in accessibleStates tfsm iff q is accessible ) ) )

proof end;

theorem Th68: :: FSM_1:68

for OAlph, IAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds the Tran of tfsm | [:(accessibleStates tfsm),IAlph:] is Function of [:(accessibleStates tfsm),IAlph:], accessibleStates tfsm

proof end;

theorem :: FSM_1:69

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of 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:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds
tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent

proof end;

theorem :: FSM_1:70

for OAlph, IAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph ex Ctfsm being non empty finite connected Mealy-FSM of IAlph,OAlph 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 )

proof end;

definition

let IAlph be set ;
let OAlph be non empty set ;
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph;
func tfsm1 -Mealy_union tfsm2 -> strict Mealy-FSM of IAlph,OAlph means :Def24: :: 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 );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def24 defines -Mealy_union FSM_1:def 24 :

registration

let IAlph be set ;
let OAlph be non empty set ;
let tfsm1, tfsm2 be non empty finite Mealy-FSM of IAlph,OAlph;
cluster tfsm1 -Mealy_union tfsm2 -> non empty finite strict ;
coherence

proof end;

end;

theorem Th71: :: FSM_1:71

for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
q11,w -admissible = q,w -admissible

proof end;

theorem Th72: :: FSM_1:72

proof end;

theorem Th73: :: FSM_1:73

for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q holds
q21,w -admissible = q,w -admissible

proof end;

theorem Th74: :: FSM_1:74

proof end;

theorem Th75: :: FSM_1:75

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for Rtfsm1, Rtfsm2 being non empty reduced Mealy-FSM of IAlph,OAlph st tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent holds
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) )

proof end;

theorem Th76: :: FSM_1:76

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty reduced connected Mealy-FSM of IAlph,OAlph
for q1u, q2u being State of tfsm
for crq11, crq12 being State of CRtfsm1 st 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 holds
not q1u,q2u -are_equivalent

proof end;

theorem Th77: :: FSM_1:77

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for CRtfsm2, CRtfsm1 being non empty reduced connected Mealy-FSM of IAlph,OAlph
for q1u, q2u being State of tfsm
for crq21, crq22 being State of CRtfsm2 st 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 holds
not q1u,q2u -are_equivalent

proof end;

theorem Th78: :: FSM_1:78

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent & 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 )

proof end;

theorem Th79: :: FSM_1:79

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent & 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 )

proof end;

theorem Th80: :: FSM_1:80

for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent & 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 & q2 in the carrier of CRtfsm2 & ( for q being Element of Q holds
( q = q1 or q = q2 ) ) )

proof end;

theorem Th81: :: FSM_1:81

for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty finite Mealy-FSM of IAlph,OAlph ex fsm1, fsm2 being non empty finite Mealy-FSM of IAlph,OAlph st
( the carrier of fsm1 misses the carrier of fsm2 & fsm1,tfsm1 -are_isomorphic & fsm2,tfsm2 -are_isomorphic )

proof end;

theorem Th82: :: FSM_1:82

for IAlph, OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic holds
tfsm1,tfsm2 -are_equivalent

proof end;

theorem Th83: :: FSM_1:83

for IAlph, OAlph being non empty set
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent holds
CRtfsm1,CRtfsm2 -are_isomorphic

proof end;

theorem Th84: :: FSM_1:84

for IAlph, OAlph being non empty set
for Ctfsm1, Ctfsm2 being non empty finite connected Mealy-FSM of IAlph,OAlph st Ctfsm1,Ctfsm2 -are_equivalent holds
the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic

proof end;

theorem :: FSM_1:85

for IAlph, OAlph being non empty set
for M1, M2 being non empty finite reduced connected Mealy-FSM of IAlph,OAlph holds
( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )

proof end;