:: by Micha{\l} Trybulec

::

:: Received May 25, 2009

:: Copyright (c) 2009-2018 Association of Mizar Users

:: Preliminaries - Natural Numbers

:: Preliminaries - Sequences

:: Preliminaries - XFinSequences and Words in E^omega

theorem Th4: :: FSM_3:4

for E being non empty set

for u being Element of E ^omega st len u = 1 holds

ex e being Element of E st

( <%e%> = u & e = u . 0 )

for u being Element of E ^omega st len u = 1 holds

ex e being Element of E st

( <%e%> = u & e = u . 0 )

proof end;

theorem Th5: :: FSM_3:5

for E being non empty set

for u being Element of E ^omega

for k being Nat st k <> 0 & len u <= k + 1 holds

ex v1, v2 being Element of E ^omega st

( len v1 <= k & len v2 <= k & u = v1 ^ v2 )

for u being Element of E ^omega

for k being Nat st k <> 0 & len u <= k + 1 holds

ex v1, v2 being Element of E ^omega st

( len v1 <= k & len v2 <= k & u = v1 ^ v2 )

proof end;

theorem Th7: :: FSM_3:7

for E being non empty set

for u being Element of E ^omega st len u > 0 holds

ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1

for u being Element of E ^omega st len u > 0 holds

ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1

proof end;

:: Preliminaries - Lex

registration
end;

theorem Th10: :: FSM_3:10

for E being non empty set

for u, v being Element of E ^omega st u <> v & u in Lex E & v in Lex E holds

for w being Element of E ^omega holds

( not u ^ w = v & not w ^ u = v )

for u, v being Element of E ^omega st u <> v & u in Lex E & v in Lex E holds

for w being Element of E ^omega holds

( not u ^ w = v & not w ^ u = v )

proof end;

:: Transition Systems over Lex(E)

theorem Th11: :: FSM_3:11

for E being non empty set

for TS being transition-system over Lex E st the Tran of TS is Function holds

TS is deterministic

for TS being transition-system over Lex E st the Tran of TS is Function holds

TS is deterministic

proof end;

:: Powerset Construction for Transition Systems

:: This is a construction that limits new transitions to single character ones.

:: This is a construction that limits new transitions to single character ones.

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let TS be non empty transition-system over F;

ex b_{1} being strict transition-system over Lex E st

( the carrier of b_{1} = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b_{1} iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) )

for b_{1}, b_{2} being strict transition-system over Lex E st the carrier of b_{1} = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b_{1} iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) & the carrier of b_{2} = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b_{2} iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) holds

b_{1} = b_{2}

end;
let F be Subset of (E ^omega);

let TS be non empty transition-system over F;

func _bool TS -> strict transition-system over Lex E means :Def1: :: FSM_3:def 1

( the carrier of it = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of it iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) );

existence ( the carrier of it = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of it iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) );

ex b

( the carrier of b

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b

proof end;

uniqueness for b

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b

b

proof end;

:: deftheorem Def1 defines _bool FSM_3:def 1 :

for E being non empty set

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for b_{4} being strict transition-system over Lex E holds

( b_{4} = _bool TS iff ( the carrier of b_{4} = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b_{4} iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ) );

for E being non empty set

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for b

( b

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of b

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let TS be non empty transition-system over F;

coherence

( not _bool TS is empty & _bool TS is deterministic )

end;
let F be Subset of (E ^omega);

let TS be non empty transition-system over F;

coherence

( not _bool TS is empty & _bool TS is deterministic )

proof end;

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let TS be non empty finite transition-system over F;

coherence

_bool TS is finite

end;
let F be Subset of (E ^omega);

let TS be non empty finite transition-system over F;

coherence

_bool TS is finite

proof end;

theorem Th12: :: FSM_3:12

for x, y being set

for E being non empty set

for e being Element of E

for F being Subset of (E ^omega)

for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds

x,<%e%> ==>. y, <%> E, _bool TS

for E being non empty set

for e being Element of E

for F being Subset of (E ^omega)

for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds

x,<%e%> ==>. y, <%> E, _bool TS

proof end;

theorem Th13: :: FSM_3:13

for X being set

for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

proof end;

:: Semiautomata

definition

let E be non empty set ;

let F be Subset of (E ^omega);

attr c_{3} is strict ;

struct semiautomaton over F -> transition-system over F;

aggr semiautomaton(# carrier, Tran, InitS #) -> semiautomaton over F;

sel InitS c_{3} -> Subset of the carrier of c_{3};

end;
let F be Subset of (E ^omega);

attr c

struct semiautomaton over F -> transition-system over F;

aggr semiautomaton(# carrier, Tran, InitS #) -> semiautomaton over F;

sel InitS c

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let SA be semiautomaton over F;

end;
let F be Subset of (E ^omega);

let SA be semiautomaton over F;

attr SA is deterministic means :Def2: :: FSM_3:def 2

( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 );

( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 );

:: deftheorem Def2 defines deterministic FSM_3:def 2 :

for E being non empty set

for F being Subset of (E ^omega)

for SA being semiautomaton over F holds

( SA is deterministic iff ( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 ) );

for E being non empty set

for F being Subset of (E ^omega)

for SA being semiautomaton over F holds

( SA is deterministic iff ( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 ) );

registration

let E be non empty set ;

let F be Subset of (E ^omega);

existence

ex b_{1} being semiautomaton over F st

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

end;
let F be Subset of (E ^omega);

existence

ex b

( b

proof end;

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

coherence

not transition-system(# the carrier of SA, the Tran of SA #) is empty ;

end;
let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

coherence

not transition-system(# the carrier of SA, the Tran of SA #) is empty ;

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

ex b_{1} being strict semiautomaton over Lex E st

( transition-system(# the carrier of b_{1}, the Tran of b_{1} #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b_{1} = {((<%> E) -succ_of ( the InitS of SA,SA))} )

for b_{1}, b_{2} being strict semiautomaton over Lex E st transition-system(# the carrier of b_{1}, the Tran of b_{1} #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b_{1} = {((<%> E) -succ_of ( the InitS of SA,SA))} & transition-system(# the carrier of b_{2}, the Tran of b_{2} #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b_{2} = {((<%> E) -succ_of ( the InitS of SA,SA))} holds

b_{1} = b_{2}
;

end;
let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

func _bool SA -> strict semiautomaton over Lex E means :Def3: :: FSM_3:def 3

( transition-system(# the carrier of it, the Tran of it #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of it = {((<%> E) -succ_of ( the InitS of SA,SA))} );

existence ( transition-system(# the carrier of it, the Tran of it #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of it = {((<%> E) -succ_of ( the InitS of SA,SA))} );

ex b

( transition-system(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines _bool FSM_3:def 3 :

for E being non empty set

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F

for b_{4} being strict semiautomaton over Lex E holds

( b_{4} = _bool SA iff ( transition-system(# the carrier of b_{4}, the Tran of b_{4} #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b_{4} = {((<%> E) -succ_of ( the InitS of SA,SA))} ) );

for E being non empty set

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F

for b

( b

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

coherence

( not _bool SA is empty & _bool SA is deterministic )

end;
let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

coherence

( not _bool SA is empty & _bool SA is deterministic )

proof end;

theorem Th14: :: FSM_3:14

for E being non empty set

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA

proof end;

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let SA be non empty finite semiautomaton over F;

coherence

_bool SA is finite

end;
let F be Subset of (E ^omega);

let SA be non empty finite semiautomaton over F;

coherence

_bool SA is finite

proof end;

:: Left-languages

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

let Q be Subset of SA;

{ w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } is Subset of (E ^omega)

end;
let F be Subset of (E ^omega);

let SA be non empty semiautomaton over F;

let Q be Subset of SA;

func left-Lang Q -> Subset of (E ^omega) equals :: FSM_3:def 4

{ w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;

coherence { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;

{ w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } is Subset of (E ^omega)

proof end;

:: deftheorem defines left-Lang FSM_3:def 4 :

for E being non empty set

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F

for Q being Subset of SA holds left-Lang Q = { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;

for E being non empty set

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F

for Q being Subset of SA holds left-Lang Q = { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ;

theorem Th15: :: FSM_3:15

for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F

for Q being Subset of SA holds

( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )

for w being Element of E ^omega

for F being Subset of (E ^omega)

for SA being non empty semiautomaton over F

for Q being Subset of SA holds

( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) )

proof end;

:: Automata

definition

let E be non empty set ;

let F be Subset of (E ^omega);

attr c_{3} is strict ;

struct automaton over F -> semiautomaton over F;

aggr automaton(# carrier, Tran, InitS, FinalS #) -> automaton over F;

sel FinalS c_{3} -> Subset of the carrier of c_{3};

end;
let F be Subset of (E ^omega);

attr c

struct automaton over F -> semiautomaton over F;

aggr automaton(# carrier, Tran, InitS, FinalS #) -> automaton over F;

sel FinalS c

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let A be automaton over F;

end;
let F be Subset of (E ^omega);

let A be automaton over F;

attr A is deterministic means :Def5: :: FSM_3:def 5

semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic ;

semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic ;

:: deftheorem Def5 defines deterministic FSM_3:def 5 :

for E being non empty set

for F being Subset of (E ^omega)

for A being automaton over F holds

( A is deterministic iff semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic );

for E being non empty set

for F being Subset of (E ^omega)

for A being automaton over F holds

( A is deterministic iff semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic );

registration

let E be non empty set ;

let F be Subset of (E ^omega);

existence

ex b_{1} being automaton over F st

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

end;
let F be Subset of (E ^omega);

existence

ex b

( b

proof end;

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let A be non empty automaton over F;

coherence

not transition-system(# the carrier of A, the Tran of A #) is empty ;

coherence

not semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is empty ;

end;
let F be Subset of (E ^omega);

let A be non empty automaton over F;

coherence

not transition-system(# the carrier of A, the Tran of A #) is empty ;

coherence

not semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is empty ;

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let A be non empty automaton over F;

ex b_{1} being strict automaton over Lex E st

( semiautomaton(# the carrier of b_{1}, the Tran of b_{1}, the InitS of b_{1} #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b_{1} = { Q where Q is Element of b_{1} : Q meets the FinalS of A } )

for b_{1}, b_{2} being strict automaton over Lex E st semiautomaton(# the carrier of b_{1}, the Tran of b_{1}, the InitS of b_{1} #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b_{1} = { Q where Q is Element of b_{1} : Q meets the FinalS of A } & semiautomaton(# the carrier of b_{2}, the Tran of b_{2}, the InitS of b_{2} #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b_{2} = { Q where Q is Element of b_{2} : Q meets the FinalS of A } holds

b_{1} = b_{2}
;

end;
let F be Subset of (E ^omega);

let A be non empty automaton over F;

func _bool A -> strict automaton over Lex E means :Def6: :: FSM_3:def 6

( semiautomaton(# the carrier of it, the Tran of it, the InitS of it #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of it = { Q where Q is Element of it : Q meets the FinalS of A } );

existence ( semiautomaton(# the carrier of it, the Tran of it, the InitS of it #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of it = { Q where Q is Element of it : Q meets the FinalS of A } );

ex b

( semiautomaton(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines _bool FSM_3:def 6 :

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F

for b_{4} being strict automaton over Lex E holds

( b_{4} = _bool A iff ( semiautomaton(# the carrier of b_{4}, the Tran of b_{4}, the InitS of b_{4} #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b_{4} = { Q where Q is Element of b_{4} : Q meets the FinalS of A } ) );

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F

for b

( b

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let A be non empty automaton over F;

coherence

( not _bool A is empty & _bool A is deterministic )

end;
let F be Subset of (E ^omega);

let A be non empty automaton over F;

coherence

( not _bool A is empty & _bool A is deterministic )

proof end;

theorem Th16: :: FSM_3:16

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F holds the carrier of (_bool A) = bool the carrier of A

for F being Subset of (E ^omega)

for A being non empty automaton over F holds the carrier of (_bool A) = bool the carrier of A

proof end;

registration

let E be non empty set ;

let F be Subset of (E ^omega);

let A be non empty finite automaton over F;

coherence

_bool A is finite

end;
let F be Subset of (E ^omega);

let A be non empty finite automaton over F;

coherence

_bool A is finite

proof end;

:: Languages Accepted by Automata

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let A be non empty automaton over F;

let Q be Subset of A;

{ w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } is Subset of (E ^omega)

end;
let F be Subset of (E ^omega);

let A be non empty automaton over F;

let Q be Subset of A;

func right-Lang Q -> Subset of (E ^omega) equals :: FSM_3:def 7

{ w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ;

coherence { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ;

{ w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } is Subset of (E ^omega)

proof end;

:: deftheorem defines right-Lang FSM_3:def 7 :

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F

for Q being Subset of A holds right-Lang Q = { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ;

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F

for Q being Subset of A holds right-Lang Q = { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ;

theorem Th17: :: FSM_3:17

for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for A being non empty automaton over F

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

for w being Element of E ^omega

for F being Subset of (E ^omega)

for A being non empty automaton over F

for Q being Subset of A holds

( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A )

proof end;

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let A be non empty automaton over F;

{ u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } is Subset of (E ^omega)

end;
let F be Subset of (E ^omega);

let A be non empty automaton over F;

func Lang A -> Subset of (E ^omega) equals :: FSM_3:def 8

{ u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ;

coherence { u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ;

{ u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } is Subset of (E ^omega)

proof end;

:: deftheorem defines Lang FSM_3:def 8 :

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = { u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ;

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = { u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ;

theorem Th18: :: FSM_3:18

for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for A being non empty automaton over F holds

( w in Lang A iff ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )

for w being Element of E ^omega

for F being Subset of (E ^omega)

for A being non empty automaton over F holds

( w in Lang A iff ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) )

proof end;

theorem Th19: :: FSM_3:19

for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for A being non empty automaton over F holds

( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )

for w being Element of E ^omega

for F being Subset of (E ^omega)

for A being non empty automaton over F holds

( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A )

proof end;

theorem :: FSM_3:20

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A

for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A

proof end;

theorem :: FSM_3:21

for E being non empty set

for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = right-Lang the InitS of A

for F being Subset of (E ^omega)

for A being non empty automaton over F holds Lang A = right-Lang the InitS of A

proof end;

theorem Th22: :: FSM_3:22

for E being non empty set

for e being Element of E

for u being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds

(R . 2) `2 = u

for e being Element of E

for u being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds

(R . 2) `2 = u

proof end;

theorem Th23: :: FSM_3:23

for E being non empty set

for u being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

for u being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds

len R > len u

proof end;

theorem Th24: :: FSM_3:24

for E being non empty set

for u, v being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

for u, v being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds

ex l being Nat st

( l in dom R & (R . l) `2 = v )

proof end;

definition

let E be non empty set ;

let u, v be Element of E ^omega ;

( ( ex w being Element of E ^omega st w ^ v = u implies ex b_{1} being Element of E ^omega st

for w being Element of E ^omega st w ^ v = u holds

b_{1} = w ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b_{1} being Element of E ^omega st b_{1} = u ) )

for b_{1}, b_{2} being Element of E ^omega holds

( ( ex w being Element of E ^omega st w ^ v = u & ( for w being Element of E ^omega st w ^ v = u holds

b_{1} = w ) & ( for w being Element of E ^omega st w ^ v = u holds

b_{2} = w ) implies b_{1} = b_{2} ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) & b_{1} = u & b_{2} = u implies b_{1} = b_{2} ) )

for b_{1} being Element of E ^omega holds verum
;

end;
let u, v be Element of E ^omega ;

func chop (u,v) -> Element of E ^omega means :Def9: :: FSM_3:def 9

for w being Element of E ^omega st w ^ v = u holds

it = w if ex w being Element of E ^omega st w ^ v = u

otherwise it = u;

existence for w being Element of E ^omega st w ^ v = u holds

it = w if ex w being Element of E ^omega st w ^ v = u

otherwise it = u;

( ( ex w being Element of E ^omega st w ^ v = u implies ex b

for w being Element of E ^omega st w ^ v = u holds

b

proof end;

uniqueness for b

( ( ex w being Element of E ^omega st w ^ v = u & ( for w being Element of E ^omega st w ^ v = u holds

b

b

proof end;

consistency for b

:: deftheorem Def9 defines chop FSM_3:def 9 :

for E being non empty set

for u, v, b_{4} being Element of E ^omega holds

( ( ex w being Element of E ^omega st w ^ v = u implies ( b_{4} = chop (u,v) iff for w being Element of E ^omega st w ^ v = u holds

b_{4} = w ) ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ( b_{4} = chop (u,v) iff b_{4} = u ) ) );

for E being non empty set

for u, v, b

( ( ex w being Element of E ^omega st w ^ v = u implies ( b

b

theorem Th25: :: FSM_3:25

for x, y being set

for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds

ex q being RedSequence of ==>.-relation TS st

( q . 1 = [x,u] & q . (len q) = [y,v] )

for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds

ex q being RedSequence of ==>.-relation TS st

( q . 1 = [x,u] & q . (len q) = [y,v] )

proof end;

theorem Th26: :: FSM_3:26

for x, y being set

for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds

==>.-relation TS reduces [x,u],[y,v]

for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds

==>.-relation TS reduces [x,u],[y,v]

proof end;

theorem Th27: :: FSM_3:27

for x, y being set

for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds

x,u ==>* y,v,TS

for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds

x,u ==>* y,v,TS

proof end;

theorem Th28: :: FSM_3:28

for E being non empty set

for u, v being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for p, q being Element of TS st p,u ^ v ==>* q,TS holds

ex r being Element of TS st

( p,u ==>* r,TS & r,v ==>* q,TS )

for u, v being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)}

for p, q being Element of TS st p,u ^ v ==>* q,TS holds

ex r being Element of TS st

( p,u ==>* r,TS & r,v ==>* q,TS )

proof end;

theorem Th29: :: FSM_3:29

for X being set

for E being non empty set

for v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)

for E being non empty set

for v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)

proof end;

theorem Th30: :: FSM_3:30

for E being non empty set

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)}

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)}

proof end;

theorem Th31: :: FSM_3:31

for X being set

for E being non empty set

for v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}

for E being non empty set

for v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))}

proof end;

theorem Th32: :: FSM_3:32

for X being set

for E being non empty set

for w being Element of E ^omega

for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))}

for E being non empty set

for w being Element of E ^omega

for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))}

proof end;

theorem Th33: :: FSM_3:33

for x being set

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)}

for P being Subset of A st x in the FinalS of A & x in P holds

P in the FinalS of (_bool A)

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)}

for P being Subset of A st x in the FinalS of A & x in P holds

P in the FinalS of (_bool A)

proof end;

theorem Th34: :: FSM_3:34

for X being set

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds

X meets the FinalS of A

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds

X meets the FinalS of A

proof end;

theorem Th35: :: FSM_3:35

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))}

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))}

proof end;

theorem Th36: :: FSM_3:36

for X being set

for E being non empty set

for w being Element of E ^omega

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))}

for E being non empty set

for w being Element of E ^omega

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))}

proof end;

theorem Th37: :: FSM_3:37

for E being non empty set

for w being Element of E ^omega

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))}

for w being Element of E ^omega

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))}

proof end;

theorem Th38: :: FSM_3:38

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang (_bool A)

for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang (_bool A)

proof end;

theorem :: FSM_3:39

for E being non empty set

for A being non empty automaton over (Lex E) \/ {(<%> E)} ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA

for A being non empty automaton over (Lex E) \/ {(<%> E)} ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA

proof end;

theorem :: FSM_3:40

for E being non empty set

for FA being non empty finite automaton over (Lex E) \/ {(<%> E)} ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA

for FA being non empty finite automaton over (Lex E) \/ {(<%> E)} ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA

proof end;