:: FSM_1 semantic presentation

theorem Th1: :: FSM_1:1

for b₁, b₂ being Nat st b₁ < b₂ holds
ex b₃ being Nat st
( b₂ = b₁ + b₃ & 1 <= b₃ )

proof end;

theorem Th2: :: FSM_1:2

canceled;

theorem Th3: :: FSM_1:3

canceled;

theorem Th4: :: FSM_1:4

canceled;

theorem Th5: :: FSM_1:5

canceled;

theorem Th6: :: FSM_1:6

canceled;

theorem Th7: :: FSM_1:7

for b₁ being set
for b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is bijective & b₅ is bijective holds
b₅ * b₄ is bijective

proof end;

theorem Th8: :: FSM_1:8

for b₁ being set
for b₂, b₃ being Equivalence_Relation of b₁ st Class b₂ = Class b₃ holds
b₂ = b₃

proof end;

theorem Th9: :: FSM_1:9

for b₁ being non empty set
for b₂ being a_partition of b₁ holds not b₂ is empty ;

theorem Th10: :: FSM_1:10

for b₁ being finite set
for b₂ being a_partition of b₁ holds b₂ is finite

proof end;

registration

let c₁ be finite set ;
cluster -> finite a_partition of a₁;
coherence by Th10;

end;

registration

let c₁ be non empty finite set ;
cluster non empty finite a_partition of a₁;
existence

proof end;

end;

theorem Th11: :: FSM_1:11

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being set st b₃ in b₂ holds
ex b₄ being Element of b₁ st b₄ in b₃

proof end;

theorem Th12: :: FSM_1:12

for b₁ being non empty finite set
for b₂ being a_partition of b₁ holds card b₂ <= card b₁

proof end;

theorem Th13: :: FSM_1:13

for b₁ being non empty finite set
for b₂, b₃ being a_partition of b₁ st b₂ is_finer_than b₃ holds
card b₃ <= card b₂

proof end;

theorem Th14: :: FSM_1:14

for b₁ being non empty finite set
for b₂, b₃ being a_partition of b₁ st b₂ is_finer_than b₃ holds
for b₄ being Element of b₃ ex b₅ being Element of b₂ st b₅ c= b₄

proof end;

theorem Th15: :: FSM_1:15

for b₁ being non empty finite set
for b₂, b₃ being a_partition of b₁ st b₂ is_finer_than b₃ & card b₂ = card b₃ holds
b₂ = b₃

proof end;

definition

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

end;

definition

let c₁ be set ;
let c₂ be FSM of c₁;
mode State of a₂ is Element of a₂;

end;

registration

let c₁ be set ;
cluster non empty finite FSM of a₁;
existence

proof end;

end;

registration

cluster non empty finite 1-sorted ;
existence

proof end;

end;

registration

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

end;

definition

let c₁ be non empty set ;
let c₂ be non empty FSM of c₁;
let c₃ be Element of c₁;
let c₄ be State of c₂;
func c₃ -succ_of c₄ -> State of a₂ equals :: FSM_1:def 1
the Tran of a₂ . [a₄,a₃];
correctness ;

end;

:: deftheorem Def1 defines -succ_of FSM_1:def 1 :

definition

let c₁ be non empty set ;
let c₂ be non empty FSM of c₁;
let c₃ be State of c₂;
let c₄ be FinSequence of c₁;
func c₃,c₄ -admissible -> FinSequence of the carrier of a₂ means :Def2: :: FSM_1:def 2
( a₅ . 1 = a₃ & len a₅ = (len a₄) + 1 & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₄ holds
ex b₂ being Element of a₁ex b₃, b₄ being State of a₂ st
( b₂ = a₄ . b₁ & b₃ = a₅ . b₁ & b₄ = a₅ . (b₁ + 1) & b₂ -succ_of b₃ = b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th16: :: FSM_1:16

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃ being State of b₂ holds b₃,(<*> b₁) -admissible = <*b₃*>

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty FSM of c₁;
let c₃ be FinSequence of c₁;
let c₄, c₅ be State of c₂;
pred c₄,c₃ -leads_to c₅ means :Def3: :: FSM_1:def 3
(a₄,a₃ -admissible ) . ((len a₃) + 1) = a₅;

end;

:: deftheorem Def3 defines -leads_to FSM_1:def 3 :

theorem Th17: :: FSM_1:17

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃ being State of b₂ holds b₃, <*> b₁ -leads_to b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty FSM of c₁;
let c₃ be FinSequence of c₁;
let c₄ be FinSequence of the carrier of c₂;
pred c₄ is_admissible_for c₃ means :Def4: :: FSM_1:def 4
ex b₁ being State of a₂ st
( b₁ = a₄ . 1 & b₁,a₃ -admissible = a₄ );

end;

:: deftheorem Def4 defines is_admissible_for FSM_1:def 4 :

theorem Th18: :: FSM_1:18

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃ being State of b₂ holds <*b₃*> is_admissible_for <*> b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty FSM of c₁;
let c₃ be State of c₂;
let c₄ be FinSequence of c₁;
func c₃ leads_to_under c₄ -> State of a₂ means :Def5: :: FSM_1:def 5
a₃,a₄ -leads_to a₅;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines leads_to_under FSM_1:def 5 :

theorem Th19: :: FSM_1:19

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃ being FinSequence of b₁
for b₄, b₅ being State of b₂ holds
( (b₄,b₃ -admissible ) . (len (b₄,b₃ -admissible )) = b₅ iff b₄,b₃ -leads_to b₅ )

proof end;

theorem Th20: :: FSM_1:20

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃, b₄ being FinSequence of b₁
for b₅ being State of b₂
for b₆ being Nat st 1 <= b₆ & b₆ <= len b₃ holds
(b₅,(b₃ ^ b₄) -admissible ) . b₆ = (b₅,b₃ -admissible ) . b₆

proof end;

theorem Th21: :: FSM_1:21

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃, b₄ being FinSequence of b₁
for b₅, b₆ being State of b₂ st b₅,b₃ -leads_to b₆ holds
(b₅,(b₃ ^ b₄) -admissible ) . ((len b₃) + 1) = b₆

proof end;

theorem Th22: :: FSM_1:22

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃, b₄ being FinSequence of b₁
for b₅, b₆ being State of b₂ st b₅,b₃ -leads_to b₆ holds
for b₇ being Nat st 1 <= b₇ & b₇ <= (len b₄) + 1 holds
(b₅,(b₃ ^ b₄) -admissible ) . ((len b₃) + b₇) = (b₆,b₄ -admissible ) . b₇

proof end;

theorem Th23: :: FSM_1:23

for b₁ being non empty set
for b₂ being non empty FSM of b₁
for b₃, b₄ being FinSequence of b₁
for b₅, b₆ being State of b₂ st b₅,b₃ -leads_to b₆ holds
b₅,(b₃ ^ b₄) -admissible = (Del (b₅,b₃ -admissible ),((len b₃) + 1)) ^ (b₆,b₄ -admissible )

proof end;

definition

let c₁ be set ;
let c₂ be non empty set ;
attr a₃ is strict;
struct Mealy-FSM of c₁,c₂ -> FSM of a₁;
aggr Mealy-FSM(# carrier, Tran, OFun, InitS #) -> Mealy-FSM of a₁,a₂;
sel OFun c₃ -> Function of [:the carrier of a₃,a₁:],a₂;
attr a₃ is strict;
struct Moore-FSM of c₁,c₂ -> FSM of a₁;
aggr Moore-FSM(# carrier, Tran, OFun, InitS #) -> Moore-FSM of a₁,a₂;
sel OFun c₃ -> Function of the carrier of a₃,a₂;

end;

registration

let c₁ be set ;
let c₂ be non empty finite set ;
let c₃ be Function of [:c₂,c₁:],c₂;
let c₄ be Element of c₂;
cluster FSM(# a₂,a₃,a₄ #) -> non empty finite ;
coherence by GROUP_1:def 14, STRUCT_0:def 1;

end;

registration

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be non empty finite set ;
let c₄ be Function of [:c₃,c₁:],c₃;
let c₅ be Function of [:c₃,c₁:],c₂;
let c₆ be Element of c₃;
cluster Mealy-FSM(# a₃,a₄,a₅,a₆ #) -> non empty finite ;
coherence by GROUP_1:def 14, STRUCT_0:def 1;

end;

registration

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be non empty finite set ;
let c₄ be Function of [:c₃,c₁:],c₃;
let c₅ be Function of c₃,c₂;
let c₆ be Element of c₃;
cluster Moore-FSM(# a₃,a₄,a₅,a₆ #) -> non empty finite ;
coherence by GROUP_1:def 14, STRUCT_0:def 1;

end;

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster non empty finite Mealy-FSM of a₁,a₂;
existence

proof end;

cluster non empty finite Moore-FSM of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄ be State of c₃;
let c₅ be FinSequence of c₁;
func c₄,c₅ -response -> FinSequence of a₂ means :Def6: :: FSM_1:def 6
( len a₆ = len a₅ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₆ . b₁ = the OFun of a₃ . [((a₄,a₅ -admissible ) . b₁),(a₅ . b₁)] ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th24: :: FSM_1:24

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₁,b₂
for b₄ being State of b₃ holds b₄,(<*> b₁) -response = <*> b₂

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Moore-FSM of c₁,c₂;
let c₄ be State of c₃;
let c₅ be FinSequence of c₁;
func c₄,c₅ -response -> FinSequence of a₂ means :Def7: :: FSM_1:def 7
( len a₆ = (len a₅) + 1 & ( for b₁ being Nat st b₁ in Seg ((len a₅) + 1) holds
a₆ . b₁ = the OFun of a₃ . ((a₄,a₅ -admissible ) . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th25: :: FSM_1:25

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁
for b₄ being non empty Moore-FSM of b₁,b₂
for b₅ being State of b₄ holds (b₅,b₃ -response ) . 1 = the OFun of b₄ . b₅

proof end;

theorem Th26: :: FSM_1:26

for b₁, b₂ being non empty set
for b₃, b₄ being FinSequence of b₁
for b₅ being non empty Mealy-FSM of b₁,b₂
for b₆, b₇ being State of b₅ st b₆,b₃ -leads_to b₇ holds
b₆,(b₃ ^ b₄) -response = (b₆,b₃ -response ) ^ (b₇,b₄ -response )

proof end;

theorem Th27: :: FSM_1:27

for b₁, b₂ being non empty set
for b₃, b₄ being FinSequence of b₁
for b₅, b₆ being non empty Mealy-FSM of b₁,b₂
for b₇, b₈ being State of b₅
for b₉, b₁₀ being State of b₆ st b₇,b₃ -leads_to b₈ & b₉,b₃ -leads_to b₁₀ & b₈,b₄ -response <> b₁₀,b₄ -response holds
b₇,(b₃ ^ b₄) -response <> b₉,(b₃ ^ b₄) -response

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄ be non empty Moore-FSM of c₁,c₂;
pred c₃ is_similar_to c₄ means :: FSM_1:def 8
for b₁ being FinSequence of a₁ holds <*(the OFun of a₄ . the InitS of a₄)*> ^ (the InitS of a₃,b₁ -response ) = the InitS of a₄,b₁ -response ;

end;

:: deftheorem Def8 defines is_similar_to FSM_1:def 8 :

theorem Th28: :: FSM_1:28

for b₁, b₂ being non empty set
for b₃ being non empty finite Moore-FSM of b₁,b₂ ex b₄ being non empty finite Mealy-FSM of b₁,b₂ st b₄ is_similar_to b₃

proof end;

theorem Th29: :: FSM_1:29

for b₁ being non empty set
for b₂ being non empty finite set
for b₃ being non empty finite Mealy-FSM of b₁,b₂ ex b₄ being non empty finite Moore-FSM of b₁,b₂ st b₃ is_similar_to b₄

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be non empty Mealy-FSM of c₁,c₂;
pred c₃,c₄ -are_equivalent means :Def9: :: FSM_1:def 9
for b₁ being FinSequence of a₁ holds the InitS of a₃,b₁ -response = the InitS of a₄,b₁ -response ;
reflexivity ;
symmetry ;

end;

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

theorem Th30: :: FSM_1:30

for b₁, b₂ being non empty set
for b₃, b₄, b₅ being non empty Mealy-FSM of b₁,b₂ st b₃,b₄ -are_equivalent & b₄,b₅ -are_equivalent holds
b₃,b₅ -are_equivalent

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄, c₅ be State of c₃;
pred c₄,c₅ -are_equivalent means :Def10: :: FSM_1:def 10
for b₁ being FinSequence of a₁ holds a₄,b₁ -response = a₅,b₁ -response ;
reflexivity ;
symmetry ;

end;

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

theorem Th31: :: FSM_1:31

canceled;

theorem Th32: :: FSM_1:32

canceled;

theorem Th33: :: FSM_1:33

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₁,b₂
for b₄, b₅, b₆ being State of b₃ st b₄,b₅ -are_equivalent & b₅,b₆ -are_equivalent holds
b₄,b₆ -are_equivalent

proof end;

theorem Th34: :: FSM_1:34

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being FinSequence of b₁
for b₅ being non empty Mealy-FSM of b₁,b₂
for b₆, b₇ being State of b₅ st b₆ = the Tran of b₅ . [b₇,b₃] holds
for b₈ being Nat st b₈ in Seg ((len b₄) + 1) holds
(b₇,(<*b₃*> ^ b₄) -admissible ) . (b₈ + 1) = (b₆,b₄ -admissible ) . b₈

proof end;

theorem Th35: :: FSM_1:35

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being FinSequence of b₁
for b₅ being non empty Mealy-FSM of b₁,b₂
for b₆, b₇ being State of b₅ st b₆ = the Tran of b₅ . [b₇,b₃] holds
b₇,(<*b₃*> ^ b₄) -response = <*(the OFun of b₅ . [b₇,b₃])*> ^ (b₆,b₄ -response )

proof end;

theorem Th36: :: FSM_1:36

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₂,b₁
for b₄, b₅ being State of b₃ holds
( b₄,b₅ -are_equivalent iff for b₆ being Element of b₂ holds
( the OFun of b₃ . [b₄,b₆] = the OFun of b₃ . [b₅,b₆] & the Tran of b₃ . [b₄,b₆],the Tran of b₃ . [b₅,b₆] -are_equivalent ) )

proof end;

theorem Th37: :: FSM_1:37

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₂,b₁
for b₄, b₅ being State of b₃ st b₄,b₅ -are_equivalent holds
for b₆ being FinSequence of b₂
for b₇ being Nat st b₇ in dom b₆ holds
ex b₈, b₉ being State of b₃ st
( b₈ = (b₄,b₆ -admissible ) . b₇ & b₉ = (b₅,b₆ -admissible ) . b₇ & b₈,b₉ -are_equivalent )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄, c₅ be State of c₃;
let c₆ be Nat;
pred c₆ -equivalent c₄,c₅ means :Def11: :: FSM_1:def 11
for b₁ being FinSequence of a₁ st len b₁ <= a₆ holds
a₄,b₁ -response = a₅,b₁ -response ;

end;

:: deftheorem Def11 defines -equivalent FSM_1:def 11 :

theorem Th38: :: FSM_1:38

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃
for b₅ being State of b₄ holds b₁ -equivalent b₅,b₅

proof end;

theorem Th39: :: FSM_1:39

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃
for b₅, b₆ being State of b₄ st b₁ -equivalent b₅,b₆ holds
b₁ -equivalent b₆,b₅

proof end;

theorem Th40: :: FSM_1:40

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃
for b₅, b₆, b₇ being State of b₄ st b₁ -equivalent b₅,b₆ & b₁ -equivalent b₆,b₇ holds
b₁ -equivalent b₅,b₇

proof end;

theorem Th41: :: FSM_1:41

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃
for b₅, b₆ being State of b₄ st b₅,b₆ -are_equivalent holds
b₁ -equivalent b₅,b₆

proof end;

theorem Th42: :: FSM_1:42

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₁,b₂
for b₄, b₅ being State of b₃ holds 0 -equivalent b₄,b₅

proof end;

theorem Th43: :: FSM_1:43

for b₁, b₂ being Nat
for b₃, b₄ being non empty set
for b₅ being non empty Mealy-FSM of b₃,b₄
for b₆, b₇ being State of b₅ st b₁ + b₂ -equivalent b₆,b₇ holds
b₁ -equivalent b₆,b₇

proof end;

theorem Th44: :: FSM_1:44

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₃,b₂
for b₅, b₆ being State of b₄ st 1 <= b₁ holds
( b₁ -equivalent b₅,b₆ iff ( 1 -equivalent b₅,b₆ & ( for b₇ being Element of b₃
for b₈ being Nat st b₈ = b₁ - 1 holds
b₈ -equivalent the Tran of b₄ . [b₅,b₇],the Tran of b₄ . [b₆,b₇] ) ) )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄ be Nat;
func c₄ -eq_states_EqR c₃ -> Equivalence_Relation of the carrier of a₃ means :Def12: :: FSM_1:def 12
for b₁, b₂ being State of a₃ holds
( [b₁,b₂] in a₅ iff a₄ -equivalent b₁,b₂ );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄ be Nat;
func c₄ -eq_states_partition c₃ -> non empty a_partition of the carrier of a₃ equals :: FSM_1:def 13
Class (a₄ -eq_states_EqR a₃);
coherence ;

end;

:: deftheorem Def13 defines -eq_states_partition FSM_1:def 13 :

theorem Th45: :: FSM_1:45

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃ holds (b₁ + 1) -eq_states_partition b₄ is_finer_than b₁ -eq_states_partition b₄

proof end;

theorem Th46: :: FSM_1:46

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃ st Class (b₁ -eq_states_EqR b₄) = Class ((b₁ + 1) -eq_states_EqR b₄) holds
for b₅ being Nat holds Class ((b₁ + b₅) -eq_states_EqR b₄) = Class (b₁ -eq_states_EqR b₄)

proof end;

theorem Th47: :: FSM_1:47

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃ st b₁ -eq_states_partition b₄ = (b₁ + 1) -eq_states_partition b₄ holds
for b₅ being Nat holds (b₁ + b₅) -eq_states_partition b₄ = b₁ -eq_states_partition b₄ by Th46;

theorem Th48: :: FSM_1:48

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃ st (b₁ + 1) -eq_states_partition b₄ <> b₁ -eq_states_partition b₄ holds
for b₅ being Nat st b₅ <= b₁ holds
(b₅ + 1) -eq_states_partition b₄ <> b₅ -eq_states_partition b₄

proof end;

theorem Th49: :: FSM_1:49

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty finite Mealy-FSM of b₂,b₃ holds
( b₁ -eq_states_partition b₄ = (b₁ + 1) -eq_states_partition b₄ or card (b₁ -eq_states_partition b₄) < card ((b₁ + 1) -eq_states_partition b₄) )

proof end;

theorem Th50: :: FSM_1:50

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₁,b₂
for b₄ being State of b₃ holds Class (0 -eq_states_EqR b₃),b₄ = the carrier of b₃

proof end;

theorem Th51: :: FSM_1:51

for b₁, b₂ being non empty set
for b₃ being non empty Mealy-FSM of b₁,b₂ holds 0 -eq_states_partition b₃ = {the carrier of b₃}

proof end;

theorem Th52: :: FSM_1:52

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty finite Mealy-FSM of b₂,b₃ st b₁ + 1 = card the carrier of b₄ holds
(b₁ + 1) -eq_states_partition b₄ = b₁ -eq_states_partition b₄

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄ be a_partition of the carrier of c₃;
attr a₄ is final means :Def14: :: FSM_1:def 14
for b₁, b₂ being State of a₃ holds
( b₁,b₂ -are_equivalent iff ex b₃ being Element of a₄ st
( b₁ in b₃ & b₂ in b₃ ) );

end;

:: deftheorem Def14 defines final FSM_1:def 14 :

theorem Th53: :: FSM_1:53

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃ st b₁ -eq_states_partition b₄ is final holds
(b₁ + 1) -eq_states_EqR b₄ = b₁ -eq_states_EqR b₄

proof end;

theorem Th54: :: FSM_1:54

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty Mealy-FSM of b₂,b₃ holds
( b₁ -eq_states_partition b₄ = (b₁ + 1) -eq_states_partition b₄ iff b₁ -eq_states_partition b₄ is final )

proof end;

theorem Th55: :: FSM_1:55

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty finite Mealy-FSM of b₂,b₃ st b₁ + 1 = card the carrier of b₄ holds
ex b₅ being Nat st
( b₅ <= b₁ & b₅ -eq_states_partition b₄ is final )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty finite Mealy-FSM of c₁,c₂;
func final_states_partition c₃ -> a_partition of the carrier of a₃ means :Def15: :: FSM_1:def 15
a₄ 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 b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being non empty finite Mealy-FSM of b₂,b₃ st b₁ + 1 = card the carrier of b₄ holds
final_states_partition b₄ = b₁ -eq_states_partition b₄

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty finite Mealy-FSM of c₁,c₂;
let c₄ be Element of final_states_partition c₃;
let c₅ be Element of c₁;
func c₅,c₄ -succ_class -> Element of final_states_partition a₃ means :Def16: :: FSM_1:def 16
ex b₁ being State of a₃ex b₂ being Nat st
( b₁ in a₄ & b₂ + 1 = card the carrier of a₃ & a₆ = Class (b₂ -eq_states_EqR a₃),(the Tran of a₃ . [b₁,a₅]) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty finite Mealy-FSM of c₁,c₂;
let c₄ be Element of final_states_partition c₃;
let c₅ be Element of c₁;
func c₄,c₅ -class_response -> Element of a₂ means :Def17: :: FSM_1:def 17
ex b₁ being State of a₃ st
( b₁ in a₄ & a₆ = the OFun of a₃ . [b₁,a₅] );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty finite Mealy-FSM of c₁,c₂;
func the_reduction_of c₃ -> strict Mealy-FSM of a₁,a₂ means :Def18: :: FSM_1:def 18
( the carrier of a₄ = final_states_partition a₃ & ( for b₁ being State of a₄
for b₂ being Element of a₁
for b₃ being State of a₃ st b₃ in b₁ holds
( the Tran of a₃ . [b₃,b₂] in the Tran of a₄ . [b₁,b₂] & the OFun of a₃ . [b₃,b₂] = the OFun of a₄ . [b₁,b₂] ) ) & the InitS of a₃ in the InitS of a₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines the_reduction_of FSM_1:def 18 :

registration

let c₁, c₂ be non empty set ;
let c₃ be non empty finite Mealy-FSM of c₁,c₂;
cluster the_reduction_of a₃ -> non empty finite strict ;
coherence

proof end;

end;

theorem Th57: :: FSM_1:57

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁
for b₄, b₅ being non empty finite Mealy-FSM of b₁,b₂
for b₆ being State of b₅
for b₇ being State of b₄ st b₄ = the_reduction_of b₅ & b₆ in b₇ holds
for b₈ being Nat st b₈ in Seg ((len b₃) + 1) holds
(b₆,b₃ -admissible ) . b₈ in (b₇,b₃ -admissible ) . b₈

proof end;

theorem Th58: :: FSM_1:58

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂ holds b₃, the_reduction_of b₃ -are_equivalent

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be non empty Mealy-FSM of c₁,c₂;
pred c₃,c₄ -are_isomorphic means :Def19: :: FSM_1:def 19
ex b₁ being Function of the carrier of a₃,the carrier of a₄ st
( b₁ is bijective & b₁ . the InitS of a₃ = the InitS of a₄ & ( for b₂ being State of a₃
for b₃ being Element of a₁ holds
( b₁ . (the Tran of a₃ . [b₂,b₃]) = the Tran of a₄ . [(b₁ . b₂),b₃] & the OFun of a₃ . [b₂,b₃] = the OFun of a₄ . [(b₁ . b₂),b₃] ) ) );
reflexivity

proof end;

symmetry

proof end;

end;

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

theorem Th59: :: FSM_1:59

for b₁, b₂ being non empty set
for b₃, b₄, b₅ being non empty Mealy-FSM of b₁,b₂ st b₃,b₄ -are_isomorphic & b₄,b₅ -are_isomorphic holds
b₃,b₅ -are_isomorphic

proof end;

theorem Th60: :: FSM_1:60

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₂
for b₄, b₅ being non empty Mealy-FSM of b₂,b₁
for b₆ being State of b₄
for b₇ being Function of the carrier of b₄,the carrier of b₅ st ( for b₈ being State of b₄
for b₉ being Element of b₂ holds b₇ . (the Tran of b₄ . [b₈,b₉]) = the Tran of b₅ . [(b₇ . b₈),b₉] ) holds
for b₈ being Nat st 1 <= b₈ & b₈ <= (len b₃) + 1 holds
b₇ . ((b₆,b₃ -admissible ) . b₈) = ((b₇ . b₆),b₃ -admissible ) . b₈

proof end;

theorem Th61: :: FSM_1:61

for b₁, b₂ being non empty set
for b₃, b₄ being non empty Mealy-FSM of b₂,b₁
for b₅, b₆ being State of b₃
for b₇ being Function of the carrier of b₃,the carrier of b₄ st b₇ . the InitS of b₃ = the InitS of b₄ & ( for b₈ being State of b₃
for b₉ being Element of b₂ holds
( b₇ . (the Tran of b₃ . [b₈,b₉]) = the Tran of b₄ . [(b₇ . b₈),b₉] & the OFun of b₃ . [b₈,b₉] = the OFun of b₄ . [(b₇ . b₈),b₉] ) ) holds
( b₅,b₆ -are_equivalent iff b₇ . b₅,b₇ . b₆ -are_equivalent )

proof end;

theorem Th62: :: FSM_1:62

for b₁, b₂ being non empty set
for b₃, b₄ being non empty finite Mealy-FSM of b₁,b₂
for b₅, b₆ being State of b₃ st b₃ = the_reduction_of b₄ & b₅ <> b₆ holds
not b₅,b₆ -are_equivalent

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
attr a₃ is reduced means :Def20: :: FSM_1:def 20
for b₁, b₂ being State of a₃ st b₁ <> b₂ holds
not b₁,b₂ -are_equivalent ;

end;

:: deftheorem Def20 defines reduced FSM_1:def 20 :

theorem Th63: :: FSM_1:63

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂ holds the_reduction_of b₃ is reduced

proof end;

registration

let c₁, c₂ be non empty set ;
cluster non empty finite reduced Mealy-FSM of a₁,a₂;
existence

proof end;

end;

theorem Th64: :: FSM_1:64

for b₁, b₂ being non empty set
for b₃ being non empty finite reduced Mealy-FSM of b₁,b₂ holds b₃, the_reduction_of b₃ -are_isomorphic

proof end;

theorem Th65: :: FSM_1:65

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂ holds
( b₃ is reduced iff ex b₄ being non empty finite Mealy-FSM of b₁,b₂ st b₃, the_reduction_of b₄ -are_isomorphic )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
let c₄ be State of c₃;
attr a₄ is accessible means :Def21: :: FSM_1:def 21
ex b₁ being FinSequence of a₁ st the InitS of a₃,b₁ -leads_to a₄;

end;

:: deftheorem Def21 defines accessible FSM_1:def 21 :

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
attr a₃ is connected means :Def22: :: FSM_1:def 22
for b₁ being State of a₃ holds b₁ is accessible;

end;

:: deftheorem Def22 defines connected FSM_1:def 22 :

registration

let c₁, c₂ be non empty set ;
cluster non empty finite connected Mealy-FSM of a₁,a₂;
existence

proof end;

end;

theorem Th66: :: FSM_1:66

for b₁, b₂ being non empty set
for b₃ being non empty finite connected Mealy-FSM of b₁,b₂ holds the_reduction_of b₃ is connected

proof end;

registration

let c₁, c₂ be non empty set ;
cluster non empty finite reduced connected Mealy-FSM of a₁,a₂;
existence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Mealy-FSM of c₁,c₂;
func accessibleStates c₃ -> set equals :: FSM_1:def 23
{ b₁ where B is State of a₃ : b₁ is accessible } ;
coherence ;

end;

:: deftheorem Def23 defines accessibleStates FSM_1:def 23 :

registration

let c₁, c₂ be non empty set ;
let c₃ be non empty finite Mealy-FSM of c₁,c₂;
cluster accessibleStates a₃ -> non empty finite ;
coherence

proof end;

end;

theorem Th67: :: FSM_1:67

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₂,b₁ holds
( accessibleStates b₃ c= the carrier of b₃ & ( for b₄ being State of b₃ holds
( b₄ in accessibleStates b₃ iff b₄ is accessible ) ) )

proof end;

theorem Th68: :: FSM_1:68

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₂,b₁ holds the Tran of b₃ | [:(accessibleStates b₃),b₂:] is Function of [:(accessibleStates b₃),b₂:], accessibleStates b₃

proof end;

theorem Th69: :: FSM_1:69

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄ being Function of [:(accessibleStates b₃),b₁:], accessibleStates b₃
for b₅ being Function of [:(accessibleStates b₃),b₁:],b₂
for b₆ being Element of accessibleStates b₃ st b₄ = the Tran of b₃ | [:(accessibleStates b₃),b₁:] & b₅ = the OFun of b₃ | [:(accessibleStates b₃),b₁:] & b₆ = the InitS of b₃ holds
b₃, Mealy-FSM(# (accessibleStates b₃),b₄,b₅,b₆ #) -are_equivalent

proof end;

theorem Th70: :: FSM_1:70

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₂,b₁ ex b₄ being non empty finite connected Mealy-FSM of b₂,b₁ st
( the Tran of b₄ = the Tran of b₃ | [:(accessibleStates b₃),b₂:] & the OFun of b₄ = the OFun of b₃ | [:(accessibleStates b₃),b₂:] & the InitS of b₄ = the InitS of b₃ & b₃,b₄ -are_equivalent )

proof end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃, c₄ be non empty Mealy-FSM of c₁,c₂;
func c₃ -Mealy_union c₄ -> strict Mealy-FSM of a₁,a₂ means :Def24: :: FSM_1:def 24
( the carrier of a₅ = the carrier of a₃ \/ the carrier of a₄ & the Tran of a₅ = the Tran of a₃ +* the Tran of a₄ & the OFun of a₅ = the OFun of a₃ +* the OFun of a₄ & the InitS of a₅ = the InitS of a₃ );
existence

proof end;

uniqueness ;

end;

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

registration

let c₁ be set ;
let c₂ be non empty set ;
let c₃, c₄ be non empty finite Mealy-FSM of c₁,c₂;
cluster a₃ -Mealy_union a₄ -> non empty finite strict ;
coherence

proof end;

end;

theorem Th71: :: FSM_1:71

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁
for b₄, b₅ being non empty Mealy-FSM of b₁,b₂
for b₆ being State of b₄
for b₇ being non empty finite Mealy-FSM of b₁,b₂
for b₈ being State of b₇ st b₇ = b₄ -Mealy_union b₅ & the carrier of b₄ misses the carrier of b₅ & b₆ = b₈ holds
b₆,b₃ -admissible = b₈,b₃ -admissible

proof end;

theorem Th72: :: FSM_1:72

proof end;

theorem Th73: :: FSM_1:73

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁
for b₄, b₅ being non empty Mealy-FSM of b₁,b₂
for b₆ being State of b₅
for b₇ being non empty finite Mealy-FSM of b₁,b₂
for b₈ being State of b₇ st b₇ = b₄ -Mealy_union b₅ & the carrier of b₄ misses the carrier of b₅ & b₆ = b₈ holds
b₆,b₃ -admissible = b₈,b₃ -admissible

proof end;

theorem Th74: :: FSM_1:74

proof end;

theorem Th75: :: FSM_1:75

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄, b₅ being non empty reduced Mealy-FSM of b₁,b₂ st b₃ = b₄ -Mealy_union b₅ & the carrier of b₄ misses the carrier of b₅ & b₄,b₅ -are_equivalent holds
ex b₆ being State of (the_reduction_of b₃) st
( the InitS of b₄ in b₆ & the InitS of b₅ in b₆ & b₆ = the InitS of (the_reduction_of b₃) )

proof end;

theorem Th76: :: FSM_1:76

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄, b₅ being non empty reduced connected Mealy-FSM of b₁,b₂
for b₆, b₇ being State of b₃
for b₈, b₉ being State of b₄ st b₈ = b₆ & b₉ = b₇ & the carrier of b₄ misses the carrier of b₅ & b₄,b₅ -are_equivalent & b₃ = b₄ -Mealy_union b₅ & not b₈,b₉ -are_equivalent holds
not b₆,b₇ -are_equivalent

proof end;

theorem Th77: :: FSM_1:77

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄, b₅ being non empty reduced connected Mealy-FSM of b₁,b₂
for b₆, b₇ being State of b₃
for b₈, b₉ being State of b₄ st b₈ = b₆ & b₉ = b₇ & the carrier of b₅ misses the carrier of b₄ & b₅,b₄ -are_equivalent & b₃ = b₅ -Mealy_union b₄ & not b₈,b₉ -are_equivalent holds
not b₆,b₇ -are_equivalent

proof end;

theorem Th78: :: FSM_1:78

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄, b₅ being non empty finite reduced connected Mealy-FSM of b₁,b₂ st the carrier of b₄ misses the carrier of b₅ & b₄,b₅ -are_equivalent & b₃ = b₄ -Mealy_union b₅ holds
for b₆ being State of (the_reduction_of b₃)
for b₇, b₈ being Element of b₆ holds
( not b₇ in the carrier of b₄ or not b₈ in the carrier of b₄ or not b₇ <> b₈ )

proof end;

theorem Th79: :: FSM_1:79

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄, b₅ being non empty finite reduced connected Mealy-FSM of b₁,b₂ st the carrier of b₄ misses the carrier of b₅ & b₄,b₅ -are_equivalent & b₃ = b₄ -Mealy_union b₅ holds
for b₆ being State of (the_reduction_of b₃)
for b₇, b₈ being Element of b₆ holds
( not b₇ in the carrier of b₅ or not b₈ in the carrier of b₅ or not b₇ <> b₈ )

proof end;

theorem Th80: :: FSM_1:80

for b₁, b₂ being non empty set
for b₃ being non empty finite Mealy-FSM of b₁,b₂
for b₄, b₅ being non empty finite reduced connected Mealy-FSM of b₁,b₂ st the carrier of b₄ misses the carrier of b₅ & b₄,b₅ -are_equivalent & b₃ = b₄ -Mealy_union b₅ holds
for b₆ being State of (the_reduction_of b₃) ex b₇, b₈ being Element of b₆ st
( b₇ in the carrier of b₄ & b₈ in the carrier of b₅ & ( for b₉ being Element of b₆ holds
( b₉ = b₇ or b₉ = b₈ ) ) )

proof end;

theorem Th81: :: FSM_1:81

for b₁, b₂ being non empty set
for b₃, b₄ being non empty finite Mealy-FSM of b₁,b₂ ex b₅, b₆ being non empty finite Mealy-FSM of b₁,b₂ st
( the carrier of b₅ misses the carrier of b₆ & b₅,b₃ -are_isomorphic & b₆,b₄ -are_isomorphic )

proof end;

theorem Th82: :: FSM_1:82

for b₁, b₂ being non empty set
for b₃, b₄ being non empty Mealy-FSM of b₁,b₂ st b₃,b₄ -are_isomorphic holds
b₃,b₄ -are_equivalent

proof end;

theorem Th83: :: FSM_1:83

for b₁, b₂ being non empty set
for b₃, b₄ being non empty finite reduced connected Mealy-FSM of b₁,b₂ st the carrier of b₃ misses the carrier of b₄ & b₃,b₄ -are_equivalent holds
b₃,b₄ -are_isomorphic

proof end;

theorem Th84: :: FSM_1:84

for b₁, b₂ being non empty set
for b₃, b₄ being non empty finite connected Mealy-FSM of b₁,b₂ st b₃,b₄ -are_equivalent holds
the_reduction_of b₃, the_reduction_of b₄ -are_isomorphic

proof end;

theorem Th85: :: FSM_1:85

for b₁, b₂ being non empty set
for b₃, b₄ being non empty finite reduced connected Mealy-FSM of b₁,b₂ holds
( b₃,b₄ -are_isomorphic iff b₃,b₄ -are_equivalent )

proof end;