:: by Hisayoshi Kunimune , Grzegorz Bancerek and Yatsuka Nakamura

::

:: Received December 3, 2001

:: Copyright (c) 2001-2016 Association of Mizar Users

notation

let I be non empty set ;

let S be non empty FSM over I;

let q be State of S;

let w be FinSequence of I;

synonym GEN (w,q) for (q,w) -admissible ;

end;
let S be non empty FSM over I;

let q be State of S;

let w be FinSequence of I;

synonym GEN (w,q) for (q,w) -admissible ;

registration

let I be non empty set ;

let S be non empty FSM over I;

let q be State of S;

let w be FinSequence of I;

coherence

not GEN (w,q) is empty

end;
let S be non empty FSM over I;

let q be State of S;

let w be FinSequence of I;

coherence

not GEN (w,q) is empty

proof end;

theorem Th1: :: FSM_2:1

for I being non empty set

for s being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>

for s being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>

proof end;

theorem Th2: :: FSM_2:2

for I being non empty set

for s1, s2 being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

for s1, s2 being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>

proof end;

theorem :: FSM_2:3

for I being non empty set

for s1, s2, s3 being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*>

for s1, s2, s3 being Element of I

for S being non empty FSM over I

for q being State of S holds GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*>

proof end;

:: deftheorem defines calculating_type FSM_2:def 1 :

for I being non empty set

for S being non empty FSM over I holds

( S is calculating_type iff for j being non zero Element of NAT

for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j );

for I being non empty set

for S being non empty FSM over I holds

( S is calculating_type iff for j being non zero Element of NAT

for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j );

theorem Th4: :: FSM_2:4

for I being non empty set

for S being non empty FSM over I st S is calculating_type holds

for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable

for S being non empty FSM over I st S is calculating_type holds

for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable

proof end;

theorem Th5: :: FSM_2:5

for I being non empty set

for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds

S is calculating_type

for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds

S is calculating_type

proof end;

theorem :: FSM_2:6

for I being non empty set

for S being non empty FSM over I st S is calculating_type holds

for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds

GEN (w1, the InitS of S) = GEN (w2, the InitS of S)

for S being non empty FSM over I st S is calculating_type holds

for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds

GEN (w1, the InitS of S) = GEN (w2, the InitS of S)

proof end;

Lm1: now :: thesis: for I being non empty set

for S being non empty FSM over I

for w being FinSequence of I

for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

for S being non empty FSM over I

for w being FinSequence of I

for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let I be non empty set ; :: thesis: for S being non empty FSM over I

for w being FinSequence of I

for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let S be non empty FSM over I; :: thesis: for w being FinSequence of I

for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let w be FinSequence of I; :: thesis: for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let q be State of S; :: thesis: GEN ((<*> I),q), GEN (w,q) are_c=-comparable

A1: dom (GEN (w,q)) = Seg (len (GEN (w,q))) by FINSEQ_1:def 3

.= Seg ((len w) + 1) by FSM_1:def 2 ;

1 <= (len w) + 1 by NAT_1:11;

then A2: 1 in dom (GEN (w,q)) by A1, FINSEQ_1:1;

(GEN (w,q)) . 1 = q by FSM_1:def 2;

then [1,q] in GEN (w,q) by A2, FUNCT_1:def 2;

then {[1,q]} c= GEN (w,q) by ZFMISC_1:31;

then <*q*> c= GEN (w,q) by FINSEQ_1:def 5;

then GEN ((<*> I),q) c= GEN (w,q) by FSM_1:1;

hence GEN ((<*> I),q), GEN (w,q) are_c=-comparable ; :: thesis: verum

end;
for w being FinSequence of I

for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let S be non empty FSM over I; :: thesis: for w being FinSequence of I

for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let w be FinSequence of I; :: thesis: for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable

let q be State of S; :: thesis: GEN ((<*> I),q), GEN (w,q) are_c=-comparable

A1: dom (GEN (w,q)) = Seg (len (GEN (w,q))) by FINSEQ_1:def 3

.= Seg ((len w) + 1) by FSM_1:def 2 ;

1 <= (len w) + 1 by NAT_1:11;

then A2: 1 in dom (GEN (w,q)) by A1, FINSEQ_1:1;

(GEN (w,q)) . 1 = q by FSM_1:def 2;

then [1,q] in GEN (w,q) by A2, FUNCT_1:def 2;

then {[1,q]} c= GEN (w,q) by ZFMISC_1:31;

then <*q*> c= GEN (w,q) by FINSEQ_1:def 5;

then GEN ((<*> I),q) c= GEN (w,q) by FSM_1:1;

hence GEN ((<*> I),q), GEN (w,q) are_c=-comparable ; :: thesis: verum

Lm2: now :: thesis: for p, q being FinSequence st p <> {} & q <> {} & p . (len p) = q . 1 holds

(Del (p,(len p))) ^ q = p ^ (Del (q,1))

(Del (p,(len p))) ^ q = p ^ (Del (q,1))

let p, q be FinSequence; :: thesis: ( p <> {} & q <> {} & p . (len p) = q . 1 implies (Del (p,(len p))) ^ q = p ^ (Del (q,1)) )

assume that

A1: p <> {} and

A2: q <> {} and

A3: p . (len p) = q . 1 ; :: thesis: (Del (p,(len p))) ^ q = p ^ (Del (q,1))

consider p1 being FinSequence, x being object such that

A4: p = p1 ^ <*x*> by A1, FINSEQ_1:46;

consider y being object , q1 being FinSequence such that

A5: q = <*y*> ^ q1 and

len q = (len q1) + 1 by A2, REWRITE1:5;

A6: len p = (len p1) + (len <*x*>) by A4, FINSEQ_1:22

.= (len p1) + 1 by FINSEQ_1:39 ;

then A7: p . (len p) = x by A4, FINSEQ_1:42;

A8: q . 1 = y by A5, FINSEQ_1:41;

(Del (p,(len p))) ^ q = p1 ^ (<*y*> ^ q1) by A4, A5, A6, WSIERP_1:40

.= p ^ q1 by A3, A4, A7, A8, FINSEQ_1:32 ;

hence (Del (p,(len p))) ^ q = p ^ (Del (q,1)) by A5, WSIERP_1:40; :: thesis: verum

end;
assume that

A1: p <> {} and

A2: q <> {} and

A3: p . (len p) = q . 1 ; :: thesis: (Del (p,(len p))) ^ q = p ^ (Del (q,1))

consider p1 being FinSequence, x being object such that

A4: p = p1 ^ <*x*> by A1, FINSEQ_1:46;

consider y being object , q1 being FinSequence such that

A5: q = <*y*> ^ q1 and

len q = (len q1) + 1 by A2, REWRITE1:5;

A6: len p = (len p1) + (len <*x*>) by A4, FINSEQ_1:22

.= (len p1) + 1 by FINSEQ_1:39 ;

then A7: p . (len p) = x by A4, FINSEQ_1:42;

A8: q . 1 = y by A5, FINSEQ_1:41;

(Del (p,(len p))) ^ q = p1 ^ (<*y*> ^ q1) by A4, A5, A6, WSIERP_1:40

.= p ^ q1 by A3, A4, A7, A8, FINSEQ_1:32 ;

hence (Del (p,(len p))) ^ q = p ^ (Del (q,1)) by A5, WSIERP_1:40; :: thesis: verum

theorem Th7: :: FSM_2:7

for I being non empty set

for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds

GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds

S is calculating_type

for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds

GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds

S is calculating_type

proof end;

definition

let I be non empty set ;

let S be non empty FSM over I;

let q be State of S;

let s be Element of I;

end;
let S be non empty FSM over I;

let q be State of S;

let s be Element of I;

pred q is_accessible_via s means :: FSM_2:def 2

ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q;

ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q;

:: deftheorem defines is_accessible_via FSM_2:def 2 :

for I being non empty set

for S being non empty FSM over I

for q being State of S

for s being Element of I holds

( q is_accessible_via s iff ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q );

for I being non empty set

for S being non empty FSM over I

for q being State of S

for s being Element of I holds

( q is_accessible_via s iff ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q );

definition

let I be non empty set ;

let S be non empty FSM over I;

let q be State of S;

end;
let S be non empty FSM over I;

let q be State of S;

attr q is accessible means :: FSM_2:def 3

ex w being FinSequence of I st the InitS of S,w -leads_to q;

ex w being FinSequence of I st the InitS of S,w -leads_to q;

:: deftheorem defines accessible FSM_2:def 3 :

for I being non empty set

for S being non empty FSM over I

for q being State of S holds

( q is accessible iff ex w being FinSequence of I st the InitS of S,w -leads_to q );

for I being non empty set

for S being non empty FSM over I

for q being State of S holds

( q is accessible iff ex w being FinSequence of I st the InitS of S,w -leads_to q );

theorem :: FSM_2:8

for I being non empty set

for s being Element of I

for S being non empty FSM over I

for q being State of S st q is_accessible_via s holds

q is accessible ;

for s being Element of I

for S being non empty FSM over I

for q being State of S st q is_accessible_via s holds

q is accessible ;

theorem :: FSM_2:9

for I being non empty set

for S being non empty FSM over I

for q being State of S st q is accessible & q <> the InitS of S holds

ex s being Element of I st q is_accessible_via s

for S being non empty FSM over I

for q being State of S st q is accessible & q <> the InitS of S holds

ex s being Element of I st q is_accessible_via s

proof end;

theorem :: FSM_2:11

for I being non empty set

for s being Element of I

for S being non empty FSM over I

for q being State of S st S is calculating_type & q is_accessible_via s holds

ex m being non zero Element of NAT st

for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds

( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds

(GEN (w, the InitS of S)) . i <> q ) )

for s being Element of I

for S being non empty FSM over I

for q being State of S st S is calculating_type & q is_accessible_via s holds

ex m being non zero Element of NAT st

for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds

( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds

(GEN (w, the InitS of S)) . i <> q ) )

proof end;

:: deftheorem defines regular FSM_2:def 4 :

for I being non empty set

for S being non empty FSM over I holds

( S is regular iff for q being State of S holds q is accessible );

for I being non empty set

for S being non empty FSM over I holds

( S is regular iff for q being State of S holds q is accessible );

theorem :: FSM_2:12

for I being non empty set

for S being non empty FSM over I st ( for s1, s2 being Element of I

for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds

S is calculating_type

for S being non empty FSM over I st ( for s1, s2 being Element of I

for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds

S is calculating_type

proof end;

theorem :: FSM_2:13

for I being non empty set

for S being non empty FSM over I st ( for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds

S is calculating_type

for S being non empty FSM over I st ( for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds

S is calculating_type

proof end;

theorem Th14: :: FSM_2:14

for I being non empty set

for S being non empty FSM over I st S is regular & S is calculating_type holds

for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2

for S being non empty FSM over I st S is regular & S is calculating_type holds

for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2

proof end;

theorem :: FSM_2:15

for I being non empty set

for S being non empty FSM over I st S is regular & S is calculating_type holds

for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

for S being non empty FSM over I st S is regular & S is calculating_type holds

for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

proof end;

theorem :: FSM_2:16

for I being non empty set

for S being non empty FSM over I st S is regular & S is calculating_type holds

for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

for S being non empty FSM over I st S is regular & S is calculating_type holds

for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

proof end;

definition

let I be set ;

attr c_{2} is strict ;

struct SM_Final over I -> FSM over I;

aggr SM_Final(# carrier, Tran, InitS, FinalS #) -> SM_Final over I;

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

end;
attr c

struct SM_Final over I -> FSM over I;

aggr SM_Final(# carrier, Tran, InitS, FinalS #) -> SM_Final over I;

sel FinalS c

registration
end;

definition

let I be non empty set ;

let s be Element of I;

let S be non empty SM_Final over I;

end;
let s be Element of I;

let S be non empty SM_Final over I;

pred s leads_to_final_state_of S means :: FSM_2:def 5

ex q being State of S st

( q is_accessible_via s & q in the FinalS of S );

ex q being State of S st

( q is_accessible_via s & q in the FinalS of S );

:: deftheorem defines leads_to_final_state_of FSM_2:def 5 :

for I being non empty set

for s being Element of I

for S being non empty SM_Final over I holds

( s leads_to_final_state_of S iff ex q being State of S st

( q is_accessible_via s & q in the FinalS of S ) );

for I being non empty set

for s being Element of I

for S being non empty SM_Final over I holds

( s leads_to_final_state_of S iff ex q being State of S st

( q is_accessible_via s & q in the FinalS of S ) );

definition

let I be non empty set ;

let S be non empty SM_Final over I;

end;
let S be non empty SM_Final over I;

attr S is halting means :Def6: :: FSM_2:def 6

for s being Element of I holds s leads_to_final_state_of S;

for s being Element of I holds s leads_to_final_state_of S;

:: deftheorem Def6 defines halting FSM_2:def 6 :

for I being non empty set

for S being non empty SM_Final over I holds

( S is halting iff for s being Element of I holds s leads_to_final_state_of S );

for I being non empty set

for S being non empty SM_Final over I holds

( S is halting iff for s being Element of I holds s leads_to_final_state_of S );

definition

let I be set ;

let O be non empty set ;

attr c_{3} is strict ;

struct Moore-SM_Final over I,O -> SM_Final over I, Moore-FSM over I,O;

aggr Moore-SM_Final(# carrier, Tran, OFun, InitS, FinalS #) -> Moore-SM_Final over I,O;

end;
let O be non empty set ;

attr c

struct Moore-SM_Final over I,O -> SM_Final over I, Moore-FSM over I,O;

aggr Moore-SM_Final(# carrier, Tran, OFun, InitS, FinalS #) -> Moore-SM_Final over I,O;

registration

let I be set ;

let O be non empty set ;

existence

ex b_{1} being Moore-SM_Final over I,O st

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

end;
let O be non empty set ;

existence

ex b

( not b

proof end;

definition

let I, O be non empty set ;

let i, f be set ;

let o be Function of {i,f},O;

for b_{1}, b_{2} being non empty strict Moore-SM_Final over I,O st the carrier of b_{1} = {i,f} & the Tran of b_{1} = [:{i,f},I:] --> f & the OFun of b_{1} = o & the InitS of b_{1} = i & the FinalS of b_{1} = {f} & the carrier of b_{2} = {i,f} & the Tran of b_{2} = [:{i,f},I:] --> f & the OFun of b_{2} = o & the InitS of b_{2} = i & the FinalS of b_{2} = {f} holds

b_{1} = b_{2}
;

existence

ex b_{1} being non empty strict Moore-SM_Final over I,O st

( the carrier of b_{1} = {i,f} & the Tran of b_{1} = [:{i,f},I:] --> f & the OFun of b_{1} = o & the InitS of b_{1} = i & the FinalS of b_{1} = {f} )

end;
let i, f be set ;

let o be Function of {i,f},O;

func I -TwoStatesMooreSM (i,f,o) -> non empty strict Moore-SM_Final over I,O means :Def7: :: FSM_2:def 7

( the carrier of it = {i,f} & the Tran of it = [:{i,f},I:] --> f & the OFun of it = o & the InitS of it = i & the FinalS of it = {f} );

uniqueness ( the carrier of it = {i,f} & the Tran of it = [:{i,f},I:] --> f & the OFun of it = o & the InitS of it = i & the FinalS of it = {f} );

for b

b

existence

ex b

( the carrier of b

proof end;

:: deftheorem Def7 defines -TwoStatesMooreSM FSM_2:def 7 :

for I, O being non empty set

for i, f being set

for o being Function of {i,f},O

for b_{6} being non empty strict Moore-SM_Final over I,O holds

( b_{6} = I -TwoStatesMooreSM (i,f,o) iff ( the carrier of b_{6} = {i,f} & the Tran of b_{6} = [:{i,f},I:] --> f & the OFun of b_{6} = o & the InitS of b_{6} = i & the FinalS of b_{6} = {f} ) );

for I, O being non empty set

for i, f being set

for o being Function of {i,f},O

for b

( b

theorem Th17: :: FSM_2:17

for I, O being non empty set

for w being FinSequence of I

for i, f being set

for o being Function of {i,f},O

for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds

(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f

for w being FinSequence of I

for i, f being set

for o being Function of {i,f},O

for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds

(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f

proof end;

registration

let I, O be non empty set ;

let i, f be set ;

let o be Function of {i,f},O;

coherence

I -TwoStatesMooreSM (i,f,o) is calculating_type

end;
let i, f be set ;

let o be Function of {i,f},O;

coherence

I -TwoStatesMooreSM (i,f,o) is calculating_type

proof end;

registration

let I, O be non empty set ;

let i, f be set ;

let o be Function of {i,f},O;

coherence

I -TwoStatesMooreSM (i,f,o) is halting

end;
let i, f be set ;

let o be Function of {i,f},O;

coherence

I -TwoStatesMooreSM (i,f,o) is halting

proof end;

theorem Th18: :: FSM_2:18

for I, O being non empty set

for s being Element of I

for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds

ex m being non zero Element of NAT st

( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds

(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I

for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds

not (GEN (w, the InitS of M)) . j in the FinalS of M ) )

for s being Element of I

for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds

ex m being non zero Element of NAT st

( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds

(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I

for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds

not (GEN (w, the InitS of M)) . j in the FinalS of M ) )

proof end;

definition

let I, O be non empty set ;

let M be non empty Moore-SM_Final over I,O;

let s be Element of I;

let t be object ;

end;
let M be non empty Moore-SM_Final over I,O;

let s be Element of I;

let t be object ;

pred t is_result_of s,M means :: FSM_2:def 8

ex m being non zero Element of NAT st

for w being FinSequence of I st w . 1 = s holds

( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds

not (GEN (w, the InitS of M)) . n in the FinalS of M ) );

ex m being non zero Element of NAT st

for w being FinSequence of I st w . 1 = s holds

( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds

not (GEN (w, the InitS of M)) . n in the FinalS of M ) );

:: deftheorem defines is_result_of FSM_2:def 8 :

for I, O being non empty set

for M being non empty Moore-SM_Final over I,O

for s being Element of I

for t being object holds

( t is_result_of s,M iff ex m being non zero Element of NAT st

for w being FinSequence of I st w . 1 = s holds

( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds

not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) );

for I, O being non empty set

for M being non empty Moore-SM_Final over I,O

for s being Element of I

for t being object holds

( t is_result_of s,M iff ex m being non zero Element of NAT st

for w being FinSequence of I st w . 1 = s holds

( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds

not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) );

theorem :: FSM_2:19

for I, O being non empty set

for s being Element of I

for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds

the OFun of M . the InitS of M is_result_of s,M

for s being Element of I

for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds

the OFun of M . the InitS of M is_result_of s,M

proof end;

theorem Th20: :: FSM_2:20

for I, O being non empty set

for s being Element of I

for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds

ex t being Element of O st t is_result_of s,M

for s being Element of I

for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds

ex t being Element of O st t is_result_of s,M

proof end;

theorem Th21: :: FSM_2:21

for I, O being non empty set

for s being Element of I

for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds

for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds

t1 = t2

for s being Element of I

for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds

for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds

t1 = t2

proof end;

theorem Th22: :: FSM_2:22

for X being non empty set

for f being BinOp of X

for M being non empty Moore-SM_Final over [:X,X:], succ X st M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & ( for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ) holds

( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )

for f being BinOp of X

for M being non empty Moore-SM_Final over [:X,X:], succ X st M is calculating_type & the carrier of M = succ X & the FinalS of M = X & the InitS of M = X & the OFun of M = id the carrier of M & ( for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) ) holds

( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )

proof end;

theorem Th23: :: FSM_2:23

for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M

proof end;

theorem Th24: :: FSM_2:24

for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M

proof end;

theorem Th25: :: FSM_2:25

for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) holds

for x, y being Element of REAL holds x + y is_result_of [x,y],M

for x, y being Element of REAL holds x + y is_result_of [x,y],M

proof end;

theorem Th26: :: FSM_2:26

for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds

the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds

for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M

the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds

for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M

proof end;

registration

let I, O be non empty set ;

existence

ex b_{1} being non empty Moore-SM_Final over I,O st

( b_{1} is calculating_type & b_{1} is halting )

end;
existence

ex b

( b

proof end;

registration

let I be non empty set ;

existence

ex b_{1} being non empty SM_Final over I st

( b_{1} is calculating_type & b_{1} is halting )

end;
existence

ex b

( b

proof end;

definition

let I, O be non empty set ;

let M be non empty calculating_type halting Moore-SM_Final over I,O;

let s be Element of I;

A1: s leads_to_final_state_of M by Def6;

uniqueness

for b_{1}, b_{2} being Element of O st b_{1} is_result_of s,M & b_{2} is_result_of s,M holds

b_{1} = b_{2}
by A1, Th21;

existence

ex b_{1} being Element of O st b_{1} is_result_of s,M
by A1, Th20;

end;
let M be non empty calculating_type halting Moore-SM_Final over I,O;

let s be Element of I;

A1: s leads_to_final_state_of M by Def6;

uniqueness

for b

b

existence

ex b

:: deftheorem Def9 defines Result FSM_2:def 9 :

for I, O being non empty set

for M being non empty calculating_type halting Moore-SM_Final over I,O

for s being Element of I

for b_{5} being Element of O holds

( b_{5} = Result (s,M) iff b_{5} is_result_of s,M );

for I, O being non empty set

for M being non empty calculating_type halting Moore-SM_Final over I,O

for s being Element of I

for b

( b

theorem :: FSM_2:27

for I, O being non empty set

for s being Element of I

for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1

for s being Element of I

for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1

proof end;

theorem :: FSM_2:28

for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds Result ([x,y],M) = max (x,y)

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds Result ([x,y],M) = max (x,y)

proof end;

theorem :: FSM_2:29

for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds Result ([x,y],M) = min (x,y)

the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds

the Tran of M . [ the InitS of M,[x,y]] = y ) holds

for x, y being Element of REAL holds Result ([x,y],M) = min (x,y)

proof end;

theorem :: FSM_2:30

for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) holds

for x, y being Element of REAL holds Result ([x,y],M) = x + y

for x, y being Element of REAL holds Result ([x,y],M) = x + y

proof end;

theorem :: FSM_2:31

for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds

the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds

for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y))

the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds

for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y))

proof end;