:: On state machines of calculating type
:: by Hisayoshi Kunimune , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received December 3, 2001
:: Copyright (c) 2001-2021 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;

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;

cluster GEN (w,q) -> non empty ;

coherence
not GEN (w,q) is empty

proof end;

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

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

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

proof end;

definition

let I be non empty set ;
let S be non empty FSM over I;

attr S is calculating_type means :: FSM_2:def 1
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;

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

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

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

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)

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

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;

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

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;

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

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;

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;

end;

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

definition

let I be non empty set ;
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;

end;

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

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 ;

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

proof end;

theorem :: FSM_2:10

for I being non empty set
for S being non empty FSM over I holds the InitS of S is accessible

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

proof end;

definition

let I be non empty set ;
let S be non empty FSM over I;

attr S is regular means :: FSM_2:def 4
for q being State of S holds q is accessible ;

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

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

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

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

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]

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

proof end;

definition

let I be set ;
attr c₂ is strict ;
struct SM_Final over I -> FSM over I;
aggr SM_Final(# carrier, Tran, InitS, FinalS #) -> SM_Final over I;
sel FinalS c₂ -> Subset of the carrier of c₂;

end;

registration

let I be set ;

cluster non empty for SM_Final over I;

existence
not for b₁ being SM_Final over I holds b₁ is empty

proof end;

end;

definition

let I be non empty set ;
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 );

end;

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

definition

let I be non empty set ;
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;

end;

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

definition

let I be set ;
let O be non empty set ;
attr c₃ 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;

registration

let I be set ;
let O be non empty set ;

cluster non empty strict for Moore-SM_Final over I,O;

existence
ex b₁ being Moore-SM_Final over I,O st
( not b₁ is empty & b₁ is strict )

proof end;

end;

definition

let I, O be non empty set ;
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
for b₁, b₂ being non empty strict Moore-SM_Final over I,O st the carrier of b₁ = {i,f} & the Tran of b₁ = [:{i,f},I:] --> f & the OFun of b₁ = o & the InitS of b₁ = i & the FinalS of b₁ = {f} & the carrier of b₂ = {i,f} & the Tran of b₂ = [:{i,f},I:] --> f & the OFun of b₂ = o & the InitS of b₂ = i & the FinalS of b₂ = {f} holds
b₁ = b₂ ;
existence
ex b₁ being non empty strict Moore-SM_Final over I,O st
( the carrier of b₁ = {i,f} & the Tran of b₁ = [:{i,f},I:] --> f & the OFun of b₁ = o & the InitS of b₁ = i & the FinalS of b₁ = {f} )

proof end;

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₆ being non empty strict Moore-SM_Final over I,O holds
( b₆ = I -TwoStatesMooreSM (i,f,o) iff ( the carrier of b₆ = {i,f} & the Tran of b₆ = [:{i,f},I:] --> f & the OFun of b₆ = o & the InitS of b₆ = i & the FinalS of b₆ = {f} ) );

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

proof end;

registration

let I, O be non empty set ;
let i, f be set ;
let o be Function of {i,f},O;

cluster I -TwoStatesMooreSM (i,f,o) -> non empty calculating_type strict ;

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

proof end;

end;

registration

let I, O be non empty set ;
let i, f be set ;
let o be Function of {i,f},O;

cluster I -TwoStatesMooreSM (i,f,o) -> non empty halting strict ;

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

proof end;

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

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 ;

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

end;

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

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

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

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

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

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

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

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

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

proof end;

registration

let I, O be non empty set ;

cluster non empty calculating_type halting for Moore-SM_Final over I,O;

existence
ex b₁ being non empty Moore-SM_Final over I,O st
( b₁ is calculating_type & b₁ is halting )

proof end;

end;

registration

let I be non empty set ;

cluster non empty calculating_type halting for SM_Final over I;

existence
ex b₁ being non empty SM_Final over I st
( b₁ is calculating_type & b₁ is halting )

proof end;

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;

func Result (s,M) -> Element of O means :Def9: :: FSM_2:def 9
it is_result_of s,M;

uniqueness
for b₁, b₂ being Element of O st b₁ is_result_of s,M & b₂ is_result_of s,M holds
b₁ = b₂ by A1, Th21;
existence
ex b₁ being Element of O st b₁ is_result_of s,M by A1, Th20;

end;

:: 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₅ being Element of O holds
( b₅ = Result (s,M) iff b₅ is_result_of s,M );

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

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)

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)

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

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

proof end;