:: On state machines of calculating type
:: by Hisayoshi Kunimune , Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received December 3, 2001
:: Copyright (c) 2001-2011 Association of Mizar Users


begin

notation
let I be non empty set ;
let S be non empty FSM of 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 of 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 of 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 of 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 of 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 of I;
attr S is calculating_type means :Def1: :: FSM_2:def 1
 for j being non empty 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 Def1 defines calculating_type FSM_2:def 1 :
for I being non empty set
for S being non empty FSM of I holds
( S is calculating_type iff for j being non empty 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 of 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 of 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 of 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
let I be non empty set ; :: thesis: for S being non empty FSM of 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 of 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:3;
(GEN (w,q)) . 1 = q by FSM_1:def 2;
then [1,q] in GEN (w,q) by A2, FUNCT_1:def 4;
then {[1,q]} c= GEN (w,q) by ZFMISC_1:37;
then <*q*> c= GEN (w,q) by FINSEQ_1:def 5;
then GEN ((<*> I),q) c= GEN (w,q) by FSM_1:16;
hence GEN ((<*> I),q), GEN (w,q) are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum
end;

Lm2: now
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 set such that
A4: p = p1 ^ <*x*> by A1, FINSEQ_1:63;
consider y being set , 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:35
.= (len p1) + 1 by FINSEQ_1:56 ;
then A7: p . (len p) = x by A4, FINSEQ_1:59;
A8: q . 1 = y by A5, FINSEQ_1:58;
(Del (p,(len p))) ^ q = p1 ^ (<*y*> ^ q1) by A4, A5, A6, WSIERP_1:48
.= p ^ q1 by A3, A4, A7, A8, FINSEQ_1:45 ;
hence (Del (p,(len p))) ^ q = p ^ (Del (q,1)) by A5, WSIERP_1:48; :: thesis: verum
end;

theorem Th7: :: FSM_2:7
for I being non empty set
for S being non empty FSM of 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 of I;
let q be State of S;
let s be Element of I;
pred q is_accessible_via s means :Def2: :: FSM_2:def 2
 ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q;
end;

:: deftheorem Def2 defines is_accessible_via FSM_2:def 2 :
for I being non empty set
for S being non empty FSM of 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 of I;
let q be State of S;
attr q is accessible means :Def3: :: FSM_2:def 3
 ex w being FinSequence of I st the InitS of S,w -leads_to q;
end;

:: deftheorem Def3 defines accessible FSM_2:def 3 :
for I being non empty set
for S being non empty FSM of 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 of I
for q being State of S st q is_accessible_via s holds
q is accessible
proof end;

theorem :: FSM_2:9
for I being non empty set
for S being non empty FSM of 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 of 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 of I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty 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 empty 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 of I;
attr S is regular means :Def4: :: FSM_2:def 4
 for q being State of S holds q is accessible ;
end;

:: deftheorem Def4 defines regular FSM_2:def 4 :
for I being non empty set
for S being non empty FSM of 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 of 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 of 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 of 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 of 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 of 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;

begin

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

registration
let I be set ;
cluster non empty SM_Final of I;
existence
not for b1 being SM_Final of I holds b1 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 of I;
pred s leads_to_final_state_of S means :Def5: :: FSM_2:def 5
 ex q being State of S st
( q is_accessible_via s & q in the FinalS of S );
end;

:: deftheorem Def5 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 of 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 of 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 of 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 c3 is strict ;
struct Moore-SM_Final of I,O -> SM_Final of I, Moore-FSM of I,O;
aggr Moore-SM_Final(# carrier, Tran, OFun, InitS, FinalS #) -> Moore-SM_Final of I,O;
end;

registration
let I be set ;
let O be non empty set ;
cluster non empty strict Moore-SM_Final of I,O;
existence
ex b1 being Moore-SM_Final of I,O st
( not b1 is empty & b1 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 of 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 b1, b2 being non empty strict Moore-SM_Final of I,O st the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} & the carrier of b2 = {i,f} & the Tran of b2 = [:{i,f},I:] --> f & the OFun of b2 = o & the InitS of b2 = i & the FinalS of b2 = {f} holds
b1 = b2 ;
existence
ex b1 being non empty strict Moore-SM_Final of I,O st
( the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {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 b6 being non empty strict Moore-SM_Final of I,O holds
( b6 = I -TwoStatesMooreSM (i,f,o) iff ( the carrier of b6 = {i,f} & the Tran of b6 = [:{i,f},I:] --> f & the OFun of b6 = o & the InitS of b6 = i & the FinalS of b6 = {f} ) );

theorem Th17: :: FSM_2:17
for O, I 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 empty 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 O, I being non empty set
for s being Element of I
for M being non empty Moore-SM_Final of I,O st M is calculating_type & s leads_to_final_state_of M holds
ex m being non empty 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 empty 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;

begin

definition
let I, O be non empty set ;
let M be non empty Moore-SM_Final of I,O;
let s be Element of I;
let t be set ;
pred t is_result_of s,M means :Def8: :: FSM_2:def 8
 ex m being non empty 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 empty 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 Def8 defines is_result_of FSM_2:def 8 :
for I, O being non empty set
for M being non empty Moore-SM_Final of I,O
for s being Element of I
for t being set holds
( t is_result_of s,M iff ex m being non empty 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 empty 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 of 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 of 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 of 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 of [: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 of [: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 of [: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 of [: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 of [: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 Moore-SM_Final of I,O;
existence
ex b1 being non empty Moore-SM_Final of I,O st
( b1 is calculating_type & b1 is halting )
proof end;
end;

registration
let I be non empty set ;
cluster non empty calculating_type halting SM_Final of I;
existence
ex b1 being non empty SM_Final of I st
( b1 is calculating_type & b1 is halting )
proof end;
end;

definition
let I, O be non empty set ;
let M be non empty calculating_type halting Moore-SM_Final of 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 b1, b2 being Element of O st b1 is_result_of s,M & b2 is_result_of s,M holds
b1 = b2 by A1, Th21;
existence
ex b1 being Element of O st b1 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 of I,O
for s being Element of I
for b5 being Element of O holds
( b5 = Result (s,M) iff b5 is_result_of s,M );

theorem :: FSM_2:27
for O, I 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 of [: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 of [: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 of [: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 of [: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;