:: by Miroslava Kaloper and Piotr Rudnicki

::

:: Received November 18, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

definition

let IAlph be set ;

attr c_{2} is strict ;

struct FSM over IAlph -> 1-sorted ;

aggr FSM(# carrier, Tran, InitS #) -> FSM over IAlph;

sel Tran c_{2} -> Function of [: the carrier of c_{2},IAlph:], the carrier of c_{2};

sel InitS c_{2} -> Element of the carrier of c_{2};

end;
attr c

struct FSM over IAlph -> 1-sorted ;

aggr FSM(# carrier, Tran, InitS #) -> FSM over IAlph;

sel Tran c

sel InitS c

registration

let X be set ;

existence

ex b_{1} being FSM over X st

( not b_{1} is empty & b_{1} is finite )

end;
existence

ex b

( not b

proof 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;

correctness

coherence

the Tran of fsm . [q,s] is State of fsm;

;

end;
let fsm be non empty FSM over IAlph;

let s be Element of IAlph;

let q be State of fsm;

correctness

coherence

the Tran of fsm . [q,s] is State of fsm;

;

:: 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];

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;

ex b_{1} being FinSequence of the carrier of fsm st

( b_{1} . 1 = q & len b_{1} = (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 = b_{1} . i & qi1 = b_{1} . (i + 1) & wi -succ_of qi = qi1 ) ) )

for b_{1}, b_{2} being FinSequence of the carrier of fsm st b_{1} . 1 = q & len b_{1} = (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 = b_{1} . i & qi1 = b_{1} . (i + 1) & wi -succ_of qi = qi1 ) ) & b_{2} . 1 = q & len b_{2} = (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 = b_{2} . i & qi1 = b_{2} . (i + 1) & wi -succ_of qi = qi1 ) ) holds

b_{1} = b_{2}

end;
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 & 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 ( 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 ) ) );

ex b

( b

ex wi being Element of IAlph ex qi, qi1 being State of fsm st

( wi = w . i & qi = b

proof end;

uniqueness for b

ex wi being Element of IAlph ex qi, qi1 being State of fsm st

( wi = w . i & qi = b

ex wi being Element of IAlph ex qi, qi1 being State of fsm st

( wi = w . i & qi = b

b

proof 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 b_{5} being FinSequence of the carrier of fsm holds

( b_{5} = (q,w) -admissible iff ( b_{5} . 1 = q & len b_{5} = (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 = b_{5} . i & qi1 = b_{5} . (i + 1) & wi -succ_of qi = qi1 ) ) ) );

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 b

( b

ex wi being Element of IAlph ex qi, qi1 being State of fsm st

( wi = w . i & qi = b

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*>

for fsm being non empty FSM over 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 over IAlph;

let w be FinSequence of IAlph;

let q1, q2 be State of fsm;

end;
let fsm be non empty FSM over IAlph;

let w be FinSequence of IAlph;

let q1, q2 be State of fsm;

:: deftheorem 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 );

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

for fsm being non empty FSM over 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 over IAlph;

let w be FinSequence of IAlph;

let qseq be FinSequence of the carrier of fsm;

end;
let fsm be non empty FSM over IAlph;

let w be FinSequence of IAlph;

let qseq be FinSequence of the carrier of fsm;

pred qseq is_admissible_for w means :: FSM_1:def 4

ex q1 being State of fsm st

( q1 = qseq . 1 & (q1,w) -admissible = qseq );

ex q1 being State of fsm st

( q1 = qseq . 1 & (q1,w) -admissible = qseq );

:: deftheorem 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 & (q1,w) -admissible = qseq ) );

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 & (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

for fsm being non empty FSM over 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 over IAlph;

let q be State of fsm;

let w be FinSequence of IAlph;

existence

ex b_{1} being State of fsm st q,w -leads_to b_{1}

for b_{1}, b_{2} being State of fsm st q,w -leads_to b_{1} & q,w -leads_to b_{2} holds

b_{1} = b_{2}
;

end;
let fsm be non empty FSM over IAlph;

let q be State of fsm;

let w be FinSequence of IAlph;

existence

ex b

proof end;

uniqueness for b

b

:: 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 b_{5} being State of fsm holds

( b_{5} = q leads_to_under w iff q,w -leads_to b_{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 b

( b

theorem :: 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 ) by Def2;

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 ) by Def2;

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 Nat st 1 <= k & k <= len w1 holds

((q1,(w1 ^ w2)) -admissible) . k = ((q1,w1) -admissible) . k

for fsm being non empty FSM over 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 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

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

proof end;

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 Nat st 1 <= k & k <= (len w2) + 1 holds

((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k

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 Nat st 1 <= k & k <= (len w2) + 1 holds

((q1,(w1 ^ w2)) -admissible) . ((len w1) + k) = ((q2,w2) -admissible) . k

proof end;

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)

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)

proof end;

definition

let IAlph be set ;

let OAlph be non empty set ;

attr c_{3} is strict ;

struct Mealy-FSM over IAlph,OAlph -> FSM over IAlph;

aggr Mealy-FSM(# carrier, Tran, OFun, InitS #) -> Mealy-FSM over IAlph,OAlph;

sel OFun c_{3} -> Function of [: the carrier of c_{3},IAlph:],OAlph;

attr c_{3} is strict ;

struct Moore-FSM over IAlph,OAlph -> FSM over IAlph;

aggr Moore-FSM(# carrier, Tran, OFun, InitS #) -> Moore-FSM over IAlph,OAlph;

sel OFun c_{3} -> Function of the carrier of c_{3},OAlph;

end;
let OAlph be non empty set ;

attr c

struct Mealy-FSM over IAlph,OAlph -> FSM over IAlph;

aggr Mealy-FSM(# carrier, Tran, OFun, InitS #) -> Mealy-FSM over IAlph,OAlph;

sel OFun c

attr c

struct Moore-FSM over IAlph,OAlph -> FSM over IAlph;

aggr Moore-FSM(# carrier, Tran, OFun, InitS #) -> Moore-FSM over IAlph,OAlph;

sel OFun c

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;

coherence

( FSM(# X,T,I #) is finite & not FSM(# X,T,I #) is empty ) ;

end;
let X be non empty finite set ;

let T be Function of [:X,IAlph:],X;

let I be Element of X;

coherence

( FSM(# X,T,I #) is finite & not FSM(# X,T,I #) is empty ) ;

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;

coherence

( Mealy-FSM(# X,T,O,I #) is finite & not Mealy-FSM(# X,T,O,I #) is empty ) ;

end;
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;

coherence

( Mealy-FSM(# X,T,O,I #) is finite & not Mealy-FSM(# X,T,O,I #) is empty ) ;

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;

coherence

( Moore-FSM(# X,T,O,I #) is finite & not Moore-FSM(# X,T,O,I #) is empty ) ;

end;
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;

coherence

( Moore-FSM(# X,T,O,I #) is finite & not Moore-FSM(# X,T,O,I #) is empty ) ;

registration

let IAlph be set ;

let OAlph be non empty set ;

existence

ex b_{1} being Mealy-FSM over IAlph,OAlph st

( b_{1} is finite & not b_{1} is empty )

ex b_{1} being Moore-FSM over IAlph,OAlph st

( b_{1} is finite & not b_{1} is empty )

end;
let OAlph be non empty set ;

existence

ex b

( b

proof end;

existence ex b

( b

proof 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;

ex b_{1} being FinSequence of OAlph st

( len b_{1} = len w & ( for i being Nat st i in dom w holds

b_{1} . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) )

for b_{1}, b_{2} being FinSequence of OAlph st len b_{1} = len w & ( for i being Nat st i in dom w holds

b_{1} . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) & len b_{2} = len w & ( for i being Nat st i in dom w holds

b_{2} . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) holds

b_{1} = b_{2}

end;
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 & ( for i being Nat st i in dom w holds

it . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) );

existence ( 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)] ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{6} being FinSequence of OAlph holds

( b_{6} = (qt,w) -response iff ( len b_{6} = len w & ( for i being Nat st i in dom w holds

b_{6} . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) ) );

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 b

( b

b

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

for tfsm being non empty Mealy-FSM over 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 over IAlph,OAlph;

let qs be State of sfsm;

let w be FinSequence of IAlph;

ex b_{1} being FinSequence of OAlph st

( len b_{1} = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds

b_{1} . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) )

for b_{1}, b_{2} being FinSequence of OAlph st len b_{1} = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds

b_{1} . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) & len b_{2} = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds

b_{2} . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) holds

b_{1} = b_{2}

end;
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 & ( for i being Nat st i in Seg ((len w) + 1) holds

it . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) );

existence ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{6} being FinSequence of OAlph holds

( b_{6} = (qs,w) -response iff ( len b_{6} = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds

b_{6} . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) ) );

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 b

( b

b

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

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

proof end;

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)

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)

proof end;

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 & q21,w1 -leads_to q22 & (q12,w2) -response <> (q22,w2) -response holds

(q11,(w1 ^ w2)) -response <> (q21,(w1 ^ w2)) -response

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 & 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 over IAlph,OAlph;

let sfsm be non empty Moore-FSM over IAlph,OAlph;

end;
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 ;

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 ;

:: 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 );

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

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

proof end;

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

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

proof end;

definition

let IAlph, OAlph be non empty set ;

let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph;

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;
let 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 for w being FinSequence of IAlph holds ( the InitS of tfsm1,w) -response = ( the InitS of tfsm2,w) -response ;

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 ;

:: deftheorem 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 );

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 & tfsm2,tfsm3 -are_equivalent holds

tfsm1,tfsm3 -are_equivalent

for tfsm1, tfsm2, tfsm3 being non empty Mealy-FSM over 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 over IAlph,OAlph;

let qa, qb be State of tfsm;

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

let qa, qb be State of tfsm;

pred qa,qb -are_equivalent means :: FSM_1:def 10

for w being FinSequence of IAlph holds (qa,w) -response = (qb,w) -response ;

reflexivity for w being FinSequence of IAlph holds (qa,w) -response = (qb,w) -response ;

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 ;

:: deftheorem 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 );

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 & q2,q3 -are_equivalent holds

q1,q3 -are_equivalent

for tfsm being non empty Mealy-FSM over 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 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 qa, qa9 being State of tfsm st qa9 = 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) = ((qa9,w) -admissible) . i

for s being Element of IAlph

for w being FinSequence of IAlph

for tfsm being non empty Mealy-FSM over IAlph,OAlph

for qa, qa9 being State of tfsm st qa9 = 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) = ((qa9,w) -admissible) . i

proof end;

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 qa, qa9 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)

for s being Element of IAlph

for w being FinSequence of IAlph

for tfsm being non empty Mealy-FSM over IAlph,OAlph

for qa, qa9 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)

proof end;

theorem Th19: :: FSM_1:19

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 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 ) )

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] & the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] -are_equivalent ) )

proof end;

theorem :: FSM_1:20

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

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 )

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 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 over IAlph,OAlph;

let qa, qb be State of tfsm;

let k be Nat;

end;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;

let qa, qb be State of tfsm;

let k be Nat;

pred k -equivalent qa,qb means :: FSM_1:def 11

for w being FinSequence of IAlph st len w <= k holds

(qa,w) -response = (qb,w) -response ;

for w being FinSequence of IAlph st len w <= k holds

(qa,w) -response = (qb,w) -response ;

:: deftheorem 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 );

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 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 ;

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 ;

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 & k -equivalent qb,qc holds

k -equivalent qa,qc

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 & k -equivalent qb,qc holds

k -equivalent qa,qc

proof end;

theorem :: FSM_1:24

for k being 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 ;

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 ;

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

for tfsm being non empty Mealy-FSM over IAlph,OAlph

for qa, qb being State of tfsm holds 0 -equivalent qa,qb

proof end;

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

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

proof end;

theorem Th27: :: FSM_1:27

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 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] ) ) )

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 & ( 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 over IAlph,OAlph;

let i be Nat;

ex b_{1} being Equivalence_Relation of the carrier of tfsm st

for qa, qb being State of tfsm holds

( [qa,qb] in b_{1} iff i -equivalent qa,qb )

for b_{1}, b_{2} being Equivalence_Relation of the carrier of tfsm st ( for qa, qb being State of tfsm holds

( [qa,qb] in b_{1} iff i -equivalent qa,qb ) ) & ( for qa, qb being State of tfsm holds

( [qa,qb] in b_{2} iff i -equivalent qa,qb ) ) holds

b_{1} = b_{2}

end;
let tfsm be non empty Mealy-FSM over 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 for qa, qb being State of tfsm holds

( [qa,qb] in it iff i -equivalent qa,qb );

ex b

for qa, qb being State of tfsm holds

( [qa,qb] in b

proof end;

uniqueness for b

( [qa,qb] in b

( [qa,qb] in b

b

proof 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 b_{5} being Equivalence_Relation of the carrier of tfsm holds

( b_{5} = i -eq_states_EqR tfsm iff for qa, qb being State of tfsm holds

( [qa,qb] in b_{5} iff i -equivalent qa,qb ) );

for IAlph, OAlph being non empty set

for tfsm being non empty Mealy-FSM over IAlph,OAlph

for i being Nat

for b

( b

( [qa,qb] in b

definition

let IAlph, OAlph be non empty set ;

let tfsm be non empty Mealy-FSM over IAlph,OAlph;

let i be Nat;

Class (i -eq_states_EqR tfsm) is non empty a_partition of the carrier of tfsm ;

end;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;

let i be Nat;

func i -eq_states_partition tfsm -> non empty a_partition of the carrier of tfsm equals :: FSM_1:def 13

Class (i -eq_states_EqR tfsm);

coherence Class (i -eq_states_EqR tfsm);

Class (i -eq_states_EqR tfsm) is non empty a_partition of the carrier of tfsm ;

:: 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);

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 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

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

proof end;

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)

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)

proof end;

theorem :: FSM_1:30

for k being 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 Nat holds (k + m) -eq_states_partition tfsm = k -eq_states_partition tfsm by Th29;

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 Nat holds (k + m) -eq_states_partition tfsm = k -eq_states_partition tfsm by Th29;

theorem Th31: :: FSM_1:31

for k being 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 Nat st i <= k holds

(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm

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 Nat st i <= k holds

(i + 1) -eq_states_partition tfsm <> i -eq_states_partition tfsm

proof end;

theorem Th32: :: FSM_1:32

for k being 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) )

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) )

proof end;

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

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

proof end;

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}

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

proof end;

theorem Th35: :: FSM_1:35

for n being 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

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

proof end;

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;

end;
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 ) );

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 ) );

:: deftheorem 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 & qb in X ) ) );

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 & qb in X ) ) );

theorem :: FSM_1:36

for k being 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

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

proof end;

theorem Th37: :: FSM_1:37

for k being 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

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

proof end;

theorem :: FSM_1:38

for n being 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 Nat st

( k <= n & k -eq_states_partition tfsm is final )

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 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 over IAlph,OAlph;

ex b_{1} being a_partition of the carrier of tfsm st b_{1} is final

for b_{1}, b_{2} being a_partition of the carrier of tfsm st b_{1} is final & b_{2} is final holds

b_{1} = b_{2}

end;
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 it is final ;

ex b

proof end;

uniqueness for b

b

proof 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 b_{4} being a_partition of the carrier of tfsm holds

( b_{4} = final_states_partition tfsm iff b_{4} is final );

for IAlph, OAlph being non empty set

for tfsm being non empty finite Mealy-FSM over IAlph,OAlph

for b

( b

theorem Th39: :: FSM_1:39

for n being 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

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

proof end;

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;

ex b_{1} being Element of final_states_partition tfsm ex q being State of tfsm ex n being Nat st

( q in qf & n + 1 = card the carrier of tfsm & b_{1} = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) )

for b_{1}, b_{2} being Element of final_states_partition tfsm st ex q being State of tfsm ex n being Nat st

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

( q in qf & n + 1 = card the carrier of tfsm & b_{2} = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) ) holds

b_{1} = b_{2}

end;
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 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 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])) );

ex b

( q in qf & n + 1 = card the carrier of tfsm & b

proof end;

uniqueness for b

( q in qf & n + 1 = card the carrier of tfsm & b

( q in qf & n + 1 = card the carrier of tfsm & b

b

proof 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 b_{6} being Element of final_states_partition tfsm holds

( b_{6} = (s,qf) -succ_class iff ex q being State of tfsm ex n being Nat st

( q in qf & n + 1 = card the carrier of tfsm & b_{6} = Class ((n -eq_states_EqR tfsm),( the Tran of tfsm . [q,s])) ) );

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 b

( b

( q in qf & n + 1 = card the carrier of tfsm & b

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;

ex b_{1} being Element of OAlph ex q being State of tfsm st

( q in qf & b_{1} = the OFun of tfsm . [q,s] )

for b_{1}, b_{2} being Element of OAlph st ex q being State of tfsm st

( q in qf & b_{1} = the OFun of tfsm . [q,s] ) & ex q being State of tfsm st

( q in qf & b_{2} = the OFun of tfsm . [q,s] ) holds

b_{1} = b_{2}

end;
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 & it = the OFun of tfsm . [q,s] );

existence ex q being State of tfsm st

( q in qf & it = the OFun of tfsm . [q,s] );

ex b

( q in qf & b

proof end;

uniqueness for b

( q in qf & b

( q in qf & b

b

proof 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 b_{6} being Element of OAlph holds

( b_{6} = (qf,s) -class_response iff ex q being State of tfsm st

( q in qf & b_{6} = the OFun of tfsm . [q,s] ) );

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 b

( b

( q in qf & b

definition

let IAlph, OAlph be non empty set ;

let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;

ex b_{1} being strict Mealy-FSM over IAlph,OAlph st

( the carrier of b_{1} = final_states_partition tfsm & ( for Q being State of b_{1}

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 b_{1} . (Q,s) & the OFun of tfsm . (q,s) = the OFun of b_{1} . (Q,s) ) ) & the InitS of tfsm in the InitS of b_{1} )

for b_{1}, b_{2} being strict Mealy-FSM over IAlph,OAlph st the carrier of b_{1} = final_states_partition tfsm & ( for Q being State of b_{1}

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 b_{1} . (Q,s) & the OFun of tfsm . (q,s) = the OFun of b_{1} . (Q,s) ) ) & the InitS of tfsm in the InitS of b_{1} & the carrier of b_{2} = final_states_partition tfsm & ( for Q being State of b_{2}

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 b_{2} . (Q,s) & the OFun of tfsm . (q,s) = the OFun of b_{2} . (Q,s) ) ) & the InitS of tfsm in the InitS of b_{2} holds

b_{1} = b_{2}

end;
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 & ( 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 ( 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 );

ex b

( the carrier of b

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 b

proof end;

uniqueness for b

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 b

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 b

b

proof 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 b_{4} being strict Mealy-FSM over IAlph,OAlph holds

( b_{4} = the_reduction_of tfsm iff ( the carrier of b_{4} = final_states_partition tfsm & ( for Q being State of b_{4}

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 b_{4} . (Q,s) & the OFun of tfsm . (q,s) = the OFun of b_{4} . (Q,s) ) ) & the InitS of tfsm in the InitS of b_{4} ) );

for IAlph, OAlph being non empty set

for tfsm being non empty finite Mealy-FSM over IAlph,OAlph

for b

( b

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 b

registration

let IAlph, OAlph be non empty set ;

let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;

coherence

( not the_reduction_of tfsm is empty & the_reduction_of tfsm is finite )

end;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;

coherence

( not the_reduction_of tfsm is empty & the_reduction_of tfsm is finite )

proof end;

theorem Th40: :: FSM_1:40

for IAlph, OAlph being non empty set

for w being FinSequence of IAlph

for tfsm, rtfsm 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 & 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

for w being FinSequence of IAlph

for tfsm, rtfsm 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 & 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 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

for tfsm being non empty finite Mealy-FSM over 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 over IAlph,OAlph;

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 & Tf . the InitS of tfsm1 = the InitS of tfsm1 & ( 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) & the OFun of tfsm1 . (q11,s) = the OFun of tfsm1 . ((Tf . q11),s) ) ) )

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 & 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) ) ) ) holds

ex Tf being Function of the carrier of tfsm2, the carrier of tfsm1 st

( Tf is bijective & Tf . the InitS of tfsm2 = the InitS of tfsm1 & ( 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) & the OFun of tfsm2 . (q11,s) = the OFun of tfsm1 . ((Tf . q11),s) ) ) )

end;
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph;

pred tfsm1,tfsm2 -are_isomorphic means :: 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 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) ) ) );

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 & Tf . the InitS of tfsm1 = the InitS of tfsm1 & ( 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) & the OFun of tfsm1 . (q11,s) = the OFun of tfsm1 . ((Tf . q11),s) ) ) )

proof end;

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 & 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) ) ) ) holds

ex Tf being Function of the carrier of tfsm2, the carrier of tfsm1 st

( Tf is bijective & Tf . the InitS of tfsm2 = the InitS of tfsm1 & ( 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) & the OFun of tfsm2 . (q11,s) = the OFun of tfsm1 . ((Tf . q11),s) ) ) )

proof end;

:: deftheorem 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 & 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) ) ) ) );

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 & 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) ) ) ) );

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 & tfsm2,tfsm3 -are_isomorphic holds

tfsm1,tfsm3 -are_isomorphic

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

tfsm1,tfsm3 -are_isomorphic

proof end;

theorem Th43: :: FSM_1:43

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 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

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 Nat st 1 <= k & k <= (len w) + 1 holds

Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k

proof end;

theorem Th44: :: FSM_1:44

for IAlph, OAlph 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) & 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 )

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) & 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 Th45: :: FSM_1:45

for IAlph, OAlph being non empty set

for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph

for qr1, qr2 being State of rtfsm st rtfsm = the_reduction_of tfsm & qr1 <> qr2 holds

not qr1,qr2 -are_equivalent

for tfsm, rtfsm being non empty finite Mealy-FSM over 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 over IAlph,OAlph;

end;
let IT be non empty Mealy-FSM over 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 ;

for qa, qb being State of IT st qa <> qb holds

not qa,qb -are_equivalent ;

:: 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 );

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;

coherence

the_reduction_of tfsm is reduced by Th45;

end;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;

coherence

the_reduction_of tfsm is reduced by Th45;

registration

let IAlph, OAlph be non empty set ;

existence

ex b_{1} being non empty Mealy-FSM over IAlph,OAlph st

( b_{1} is reduced & b_{1} is finite )

end;
existence

ex b

( b

proof 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

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

proof end;

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 )

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 )

proof end;

definition

let IAlph, OAlph be non empty set ;

let tfsm be non empty Mealy-FSM over IAlph,OAlph;

let IT be State of tfsm;

end;
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 being FinSequence of IAlph st the InitS of tfsm,w -leads_to IT;

ex w being FinSequence of IAlph st the InitS of tfsm,w -leads_to IT;

:: deftheorem 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 );

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 );

:: 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 );

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 ;

existence

ex b_{1} being non empty finite Mealy-FSM over IAlph,OAlph st b_{1} is connected

end;
existence

ex b

proof end;

registration

let IAlph, OAlph be non empty set ;

let Ctfsm be non empty finite connected Mealy-FSM over IAlph,OAlph;

coherence

the_reduction_of Ctfsm is connected

end;
let Ctfsm be non empty finite connected Mealy-FSM over IAlph,OAlph;

coherence

the_reduction_of Ctfsm is connected

proof end;

registration

let IAlph, OAlph be non empty set ;

existence

ex b_{1} being non empty Mealy-FSM over IAlph,OAlph st

( b_{1} is connected & b_{1} is reduced & b_{1} is finite )

end;
existence

ex b

( b

proof end;

definition

let IAlph, OAlph be non empty set ;

let tfsm be non empty Mealy-FSM over IAlph,OAlph;

{ q where q is State of tfsm : q is accessible } is set ;

end;
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 } ;

{ q where q is State of tfsm : q is accessible } is set ;

:: 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 } ;

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;

coherence

( accessibleStates tfsm is finite & not accessibleStates tfsm is empty )

end;
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph;

coherence

( accessibleStates tfsm is finite & not accessibleStates tfsm is empty )

proof end;

theorem Th48: :: FSM_1:48

for IAlph, OAlph being non empty set

for tfsm being non empty finite Mealy-FSM over 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 ) ) )

for tfsm being non empty finite Mealy-FSM over 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 Th49: :: FSM_1:49

for IAlph, OAlph 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)

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)

proof end;

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:] & cOFun = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & cInitS = the InitS of tfsm holds

tfsm, Mealy-FSM(# (accessibleStates tfsm),cTran,cOFun,cInitS #) -are_equivalent

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:] & 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:51

for IAlph, OAlph 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:] & the OFun of Ctfsm = the OFun of tfsm | [:(accessibleStates tfsm),IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm,Ctfsm -are_equivalent )

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:] & 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 over IAlph,OAlph;

ex b_{1} being strict Mealy-FSM over IAlph,OAlph st

( the carrier of b_{1} = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of b_{1} = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of b_{1} = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of b_{1} = the InitS of tfsm1 )

for b_{1}, b_{2} being strict Mealy-FSM over IAlph,OAlph st the carrier of b_{1} = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of b_{1} = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of b_{1} = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of b_{1} = the InitS of tfsm1 & the carrier of b_{2} = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of b_{2} = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of b_{2} = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of b_{2} = the InitS of tfsm1 holds

b_{1} = b_{2}
;

end;
let 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 :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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: 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 b_{5} being strict Mealy-FSM over IAlph,OAlph holds

( b_{5} = tfsm1 -Mealy_union tfsm2 iff ( the carrier of b_{5} = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of b_{5} = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of b_{5} = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of b_{5} = the InitS of tfsm1 ) );

for IAlph being set

for OAlph being non empty set

for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph

for b

( b

registration

let IAlph be set ;

let OAlph be non empty set ;

let tfsm1, tfsm2 be non empty finite Mealy-FSM over IAlph,OAlph;

coherence

( not tfsm1 -Mealy_union tfsm2 is empty & tfsm1 -Mealy_union tfsm2 is finite )

end;
let OAlph be non empty set ;

let tfsm1, tfsm2 be non empty finite Mealy-FSM over IAlph,OAlph;

coherence

( not tfsm1 -Mealy_union tfsm2 is empty & tfsm1 -Mealy_union tfsm2 is finite )

proof 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 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds

(q11,w) -admissible = (q,w) -admissible

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 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds

(q11,w) -admissible = (q,w) -admissible

proof end;

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 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds

(q11,w) -response = (q,w) -response

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 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds

(q11,w) -response = (q,w) -response

proof end;

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 & q21 = q holds

(q21,w) -admissible = (q,w) -admissible

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 & q21 = q holds

(q21,w) -admissible = (q,w) -admissible

proof end;

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 & q21 = q holds

(q21,w) -response = (q,w) -response

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 & q21 = q holds

(q21,w) -response = (q,w) -response

proof end;

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 & 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) )

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 & 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 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 & crq12 = q2u & the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq11,crq12 -are_equivalent holds

not q1u,q2u -are_equivalent

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 & crq12 = q2u & the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq11,crq12 -are_equivalent holds

not q1u,q2u -are_equivalent

proof end;

theorem Th58: :: FSM_1:58

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 crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds

not q1u,q2u -are_equivalent

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 crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds

not q1u,q2u -are_equivalent

proof end;

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 & 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 )

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 & 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 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 )

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 )

proof end;

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 & 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 ) ) )

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 & 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 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 & fsm1,tfsm1 -are_isomorphic & fsm2,tfsm2 -are_isomorphic )

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 & fsm1,tfsm1 -are_isomorphic & fsm2,tfsm2 -are_isomorphic )

proof end;

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

for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph st tfsm1,tfsm2 -are_isomorphic holds

tfsm1,tfsm2 -are_equivalent

proof end;

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 & CRtfsm1,CRtfsm2 -are_equivalent holds

CRtfsm1,CRtfsm2 -are_isomorphic

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

CRtfsm1,CRtfsm2 -are_isomorphic

proof end;

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

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

proof end;

:: 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 )

for M1, M2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph holds

( M1,M2 -are_isomorphic iff M1,M2 -are_equivalent )

proof end;