:: FSM_2 semantic presentation

notation
let c1 be non empty set ;
let c2 be non empty FSM of c1;
let c3 be State of c2;
let c4 be FinSequence of c1;
synonym GEN c4,c3 for c3,c4 -admissible ;
end;

registration
let c1 be non empty set ;
let c2 be non empty FSM of c1;
let c3 be State of c2;
let c4 be FinSequence of c1;
cluster GEN a4,a3 -> non empty ;
coherence
not GEN c4,c3 is empty
proof end;
end;

theorem Th1: :: FSM_2:1
for b1 being non empty set
for b2 being Element of b1
for b3 being non empty FSM of b1
for b4 being State of b3 holds GEN <*b2*>,b4 = <*b4,(the Tran of b3 . [b4,b2])*>
proof end;

theorem Th2: :: FSM_2:2
for b1 being non empty set
for b2, b3 being Element of b1
for b4 being non empty FSM of b1
for b5 being State of b4 holds GEN <*b2,b3*>,b5 = <*b5,(the Tran of b4 . [b5,b2]),(the Tran of b4 . [(the Tran of b4 . [b5,b2]),b3])*>
proof end;

theorem Th3: :: FSM_2:3
for b1 being non empty set
for b2, b3, b4 being Element of b1
for b5 being non empty FSM of b1
for b6 being State of b5 holds GEN <*b2,b3,b4*>,b6 = <*b6,(the Tran of b5 . [b6,b2]),(the Tran of b5 . [(the Tran of b5 . [b6,b2]),b3]),(the Tran of b5 . [(the Tran of b5 . [(the Tran of b5 . [b6,b2]),b3]),b4])*>
proof end;

definition
let c1 be non empty set ;
let c2 be non empty FSM of c1;
attr a2 is calculating_type means :Def1: :: FSM_2:def 1
for b1 being non empty Nat
for b2, b3 being FinSequence of a1 st b2 . 1 = b3 . 1 & b1 <= (len b2) + 1 & b1 <= (len b3) + 1 holds
(GEN b2,the InitS of a2) . b1 = (GEN b3,the InitS of a2) . b1;
end;

:: deftheorem Def1 defines calculating_type FSM_2:def 1 :
for b1 being non empty set
for b2 being non empty FSM of b1 holds
( b2 is calculating_type iff for b3 being non empty Nat
for b4, b5 being FinSequence of b1 st b4 . 1 = b5 . 1 & b3 <= (len b4) + 1 & b3 <= (len b5) + 1 holds
(GEN b4,the InitS of b2) . b3 = (GEN b5,the InitS of b2) . b3 );

theorem Th4: :: FSM_2:4
for b1 being non empty set
for b2 being non empty FSM of b1 st b2 is calculating_type holds
for b3, b4 being FinSequence of b1 st b3 . 1 = b4 . 1 holds
GEN b3,the InitS of b2, GEN b4,the InitS of b2 are_c=-comparable
proof end;

theorem Th5: :: FSM_2:5
for b1 being non empty set
for b2 being non empty FSM of b1 st ( for b3, b4 being FinSequence of b1 st b3 . 1 = b4 . 1 holds
GEN b3,the InitS of b2, GEN b4,the InitS of b2 are_c=-comparable ) holds
b2 is calculating_type
proof end;

theorem Th6: :: FSM_2:6
for b1 being non empty set
for b2 being non empty FSM of b1 st b2 is calculating_type holds
for b3, b4 being FinSequence of b1 st b3 . 1 = b4 . 1 & len b3 = len b4 holds
GEN b3,the InitS of b2 = GEN b4,the InitS of b2
proof end;

E6: now
let c1 be non empty set ;
let c2 be non empty FSM of c1;
let c3 be FinSequence of c1;
let c4 be State of c2;
E7: dom (GEN c3,c4) = Seg (len (GEN c3,c4)) by FINSEQ_1:def 3
.= Seg ((len c3) + 1) by FSM_1:def 2 ;
( 1 <= 1 & 1 <= (len c3) + 1 ) by NAT_1:29;
then ( 1 in dom (GEN c3,c4) & (GEN c3,c4) . 1 = c4 ) by E7, FINSEQ_1:3, FSM_1:def 2;
then [1,c4] in GEN c3,c4 by FUNCT_1:def 4;
then {[1,c4]} c= GEN c3,c4 by ZFMISC_1:37;
then <*c4*> c= GEN c3,c4 by FINSEQ_1:def 5;
then GEN (<*> c1),c4 c= GEN c3,c4 by FSM_1:16;
hence GEN (<*> c1),c4, GEN c3,c4 are_c=-comparable by XBOOLE_0:def 9;
end;

E7: now
let c1, c2 be FinSequence;
assume that
E8: c1 <> {} and
E9: c2 <> {} and
E10: c1 . (len c1) = c2 . 1 ;
consider c3 being FinSequence, c4 being set such that
E11: c1 = c3 ^ <*c4*> by E8, FINSEQ_1:63;
consider c5 being set , c6 being FinSequence such that
E12: ( c2 = <*c5*> ^ c6 & len c2 = (len c6) + 1 ) by E9, REWRITE1:5;
E13: len c1 = (len c3) + (len <*c4*>) by E11, FINSEQ_1:35
.= (len c3) + 1 by FINSEQ_1:56 ;
then E14: ( c1 . (len c1) = c4 & c2 . 1 = c5 ) by E11, E12, FINSEQ_1:58, FINSEQ_1:59;
(Del c1,(len c1)) ^ c2 = c3 ^ (<*c5*> ^ c6) by E11, E12, E13, WSIERP_1:48
.= c1 ^ c6 by E10, E11, E14, FINSEQ_1:45 ;
hence (Del c1,(len c1)) ^ c2 = c1 ^ (Del c2,1) by E12, WSIERP_1:48;
end;

theorem Th7: :: FSM_2:7
for b1 being non empty set
for b2 being non empty FSM of b1 st ( for b3, b4 being FinSequence of b1 st b3 . 1 = b4 . 1 & len b3 = len b4 holds
GEN b3,the InitS of b2 = GEN b4,the InitS of b2 ) holds
b2 is calculating_type
proof end;

definition
let c1 be non empty set ;
let c2 be non empty FSM of c1;
let c3 be State of c2;
let c4 be Element of c1;
pred c3 is_accessible_via c4 means :Def2: :: FSM_2:def 2
ex b1 being FinSequence of a1 st the InitS of a2,<*a4*> ^ b1 -leads_to a3;
end;

:: deftheorem Def2 defines is_accessible_via FSM_2:def 2 :
for b1 being non empty set
for b2 being non empty FSM of b1
for b3 being State of b2
for b4 being Element of b1 holds
( b3 is_accessible_via b4 iff ex b5 being FinSequence of b1 st the InitS of b2,<*b4*> ^ b5 -leads_to b3 );

definition
let c1 be non empty set ;
let c2 be non empty FSM of c1;
let c3 be State of c2;
attr a3 is accessible means :Def3: :: FSM_2:def 3
ex b1 being FinSequence of a1 st the InitS of a2,b1 -leads_to a3;
end;

:: deftheorem Def3 defines accessible FSM_2:def 3 :
for b1 being non empty set
for b2 being non empty FSM of b1
for b3 being State of b2 holds
( b3 is accessible iff ex b4 being FinSequence of b1 st the InitS of b2,b4 -leads_to b3 );

theorem Th8: :: FSM_2:8
for b1 being non empty set
for b2 being Element of b1
for b3 being non empty FSM of b1
for b4 being State of b3 st b4 is_accessible_via b2 holds
b4 is accessible
proof end;

theorem Th9: :: FSM_2:9
for b1 being non empty set
for b2 being non empty FSM of b1
for b3 being State of b2 st b3 is accessible & b3 <> the InitS of b2 holds
ex b4 being Element of b1 st b3 is_accessible_via b4
proof end;

theorem Th10: :: FSM_2:10
for b1 being non empty set
for b2 being non empty FSM of b1 holds the InitS of b2 is accessible
proof end;

theorem Th11: :: FSM_2:11
for b1 being non empty set
for b2 being Element of b1
for b3 being non empty FSM of b1
for b4 being State of b3 st b3 is calculating_type & b4 is_accessible_via b2 holds
ex b5 being non empty Nat st
for b6 being FinSequence of b1 st (len b6) + 1 >= b5 & b6 . 1 = b2 holds
( b4 = (GEN b6,the InitS of b3) . b5 & ( for b7 being non empty Nat st b7 < b5 holds
(GEN b6,the InitS of b3) . b7 <> b4 ) )
proof end;

definition
let c1 be non empty set ;
let c2 be non empty FSM of c1;
attr a2 is regular means :Def4: :: FSM_2:def 4
for b1 being State of a2 holds b1 is accessible;
end;

:: deftheorem Def4 defines regular FSM_2:def 4 :
for b1 being non empty set
for b2 being non empty FSM of b1 holds
( b2 is regular iff for b3 being State of b2 holds b3 is accessible );

theorem Th12: :: FSM_2:12
for b1 being non empty set
for b2 being non empty FSM of b1 st ( for b3, b4 being Element of b1
for b5 being State of b2 holds the Tran of b2 . [b5,b3] = the Tran of b2 . [b5,b4] ) holds
b2 is calculating_type
proof end;

theorem Th13: :: FSM_2:13
for b1 being non empty set
for b2 being non empty FSM of b1 st ( for b3, b4 being Element of b1
for b5 being State of b2 st b5 <> the InitS of b2 holds
the Tran of b2 . [b5,b3] = the Tran of b2 . [b5,b4] ) & ( for b3 being Element of b1
for b4 being State of b2 holds the Tran of b2 . [b4,b3] <> the InitS of b2 ) holds
b2 is calculating_type
proof end;

theorem Th14: :: FSM_2:14
for b1 being non empty set
for b2 being non empty FSM of b1 st b2 is regular & b2 is calculating_type holds
for b3, b4 being Element of b1
for b5 being State of b2 st b5 <> the InitS of b2 holds
(GEN <*b3*>,b5) . 2 = (GEN <*b4*>,b5) . 2
proof end;

theorem Th15: :: FSM_2:15
for b1 being non empty set
for b2 being non empty FSM of b1 st b2 is regular & b2 is calculating_type holds
for b3, b4 being Element of b1
for b5 being State of b2 st b5 <> the InitS of b2 holds
the Tran of b2 . [b5,b3] = the Tran of b2 . [b5,b4]
proof end;

theorem Th16: :: FSM_2:16
for b1 being non empty set
for b2 being non empty FSM of b1 st b2 is regular & b2 is calculating_type holds
for b3, b4, b5 being Element of b1
for b6 being State of b2 st the Tran of b2 . [the InitS of b2,b4] <> the Tran of b2 . [the InitS of b2,b5] holds
the Tran of b2 . [b6,b3] <> the InitS of b2
proof end;

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

registration
let c1 be set ;
cluster non empty SM_Final of a1;
existence
not for b1 being SM_Final of c1 holds b1 is empty
proof end;
end;

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be non empty SM_Final of c1;
pred c2 leads_to_final_state_of c3 means :Def5: :: FSM_2:def 5
ex b1 being State of a3 st
( b1 is_accessible_via a2 & b1 in the FinalS of a3 );
end;

:: deftheorem Def5 defines leads_to_final_state_of FSM_2:def 5 :
for b1 being non empty set
for b2 being Element of b1
for b3 being non empty SM_Final of b1 holds
( b2 leads_to_final_state_of b3 iff ex b4 being State of b3 st
( b4 is_accessible_via b2 & b4 in the FinalS of b3 ) );

definition
let c1 be non empty set ;
let c2 be non empty SM_Final of c1;
attr a2 is halting means :Def6: :: FSM_2:def 6
for b1 being Element of a1 holds b1 leads_to_final_state_of a2;
end;

:: deftheorem Def6 defines halting FSM_2:def 6 :
for b1 being non empty set
for b2 being non empty SM_Final of b1 holds
( b2 is halting iff for b3 being Element of b1 holds b3 leads_to_final_state_of b2 );

definition
let c1 be set ;
let c2 be non empty set ;
attr a3 is strict;
struct Moore-SM_Final of c1,c2 -> SM_Final of a1, Moore-FSM of a1,a2;
aggr Moore-SM_Final(# carrier, Tran, OFun, InitS, FinalS #) -> Moore-SM_Final of a1,a2;
end;

registration
let c1 be set ;
let c2 be non empty set ;
cluster non empty strict Moore-SM_Final of a1,a2;
existence
ex b1 being Moore-SM_Final of c1,c2 st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let c1, c2 be non empty set ;
let c3, c4 be set ;
let c5 be Function of {c3,c4},c2;
func c1 -TwoStatesMooreSM c3,c4,c5 -> non empty strict Moore-SM_Final of a1,a2 means :Def7: :: FSM_2:def 7
( the carrier of a6 = {a3,a4} & the Tran of a6 = [:{a3,a4},a1:] --> a4 & the OFun of a6 = a5 & the InitS of a6 = a3 & the FinalS of a6 = {a4} );
uniqueness
for b1, b2 being non empty strict Moore-SM_Final of c1,c2 st the carrier of b1 = {c3,c4} & the Tran of b1 = [:{c3,c4},c1:] --> c4 & the OFun of b1 = c5 & the InitS of b1 = c3 & the FinalS of b1 = {c4} & the carrier of b2 = {c3,c4} & the Tran of b2 = [:{c3,c4},c1:] --> c4 & the OFun of b2 = c5 & the InitS of b2 = c3 & the FinalS of b2 = {c4} holds
b1 = b2 ;
existence
ex b1 being non empty strict Moore-SM_Final of c1,c2 st
( the carrier of b1 = {c3,c4} & the Tran of b1 = [:{c3,c4},c1:] --> c4 & the OFun of b1 = c5 & the InitS of b1 = c3 & the FinalS of b1 = {c4} )
proof end;
end;

:: deftheorem Def7 defines -TwoStatesMooreSM FSM_2:def 7 :
for b1, b2 being non empty set
for b3, b4 being set
for b5 being Function of {b3,b4},b2
for b6 being non empty strict Moore-SM_Final of b1,b2 holds
( b6 = b1 -TwoStatesMooreSM b3,b4,b5 iff ( the carrier of b6 = {b3,b4} & the Tran of b6 = [:{b3,b4},b1:] --> b4 & the OFun of b6 = b5 & the InitS of b6 = b3 & the FinalS of b6 = {b4} ) );

theorem Th17: :: FSM_2:17
for b1, b2 being non empty set
for b3 being FinSequence of b2
for b4, b5 being set
for b6 being Function of {b4,b5},b1
for b7 being non empty Nat st 1 < b7 & b7 <= (len b3) + 1 holds
(GEN b3,the InitS of (b2 -TwoStatesMooreSM b4,b5,b6)) . b7 = b5
proof end;

registration
let c1, c2 be non empty set ;
let c3, c4 be set ;
let c5 be Function of {c3,c4},c2;
cluster a1 -TwoStatesMooreSM a3,a4,a5 -> non empty calculating_type strict ;
coherence
c1 -TwoStatesMooreSM c3,c4,c5 is calculating_type
proof end;
end;

registration
let c1, c2 be non empty set ;
let c3, c4 be set ;
let c5 be Function of {c3,c4},c2;
cluster a1 -TwoStatesMooreSM a3,a4,a5 -> non empty calculating_type halting strict ;
coherence
c1 -TwoStatesMooreSM c3,c4,c5 is halting
proof end;
end;

theorem Th18: :: FSM_2:18
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being non empty Moore-SM_Final of b2,b1 st b4 is calculating_type & b3 leads_to_final_state_of b4 & not the InitS of b4 in the FinalS of b4 holds
ex b5 being non empty Nat st
( ( for b6 being FinSequence of b2 st (len b6) + 1 >= b5 & b6 . 1 = b3 holds
(GEN b6,the InitS of b4) . b5 in the FinalS of b4 ) & ( for b6 being FinSequence of b2
for b7 being non empty Nat st b7 <= (len b6) + 1 & b6 . 1 = b3 & b7 < b5 holds
not (GEN b6,the InitS of b4) . b7 in the FinalS of b4 ) )
proof end;

definition
let c1, c2 be non empty set ;
let c3 be non empty Moore-SM_Final of c1,c2;
let c4 be Element of c1;
let c5 be set ;
pred c5 is_result_of c4,c3 means :Def8: :: FSM_2:def 8
ex b1 being non empty Nat st
for b2 being FinSequence of a1 st b2 . 1 = a4 holds
( ( b1 <= (len b2) + 1 implies ( a5 = the OFun of a3 . ((GEN b2,the InitS of a3) . b1) & (GEN b2,the InitS of a3) . b1 in the FinalS of a3 ) ) & ( for b3 being non empty Nat st b3 < b1 & b3 <= (len b2) + 1 holds
not (GEN b2,the InitS of a3) . b3 in the FinalS of a3 ) );
end;

:: deftheorem Def8 defines is_result_of FSM_2:def 8 :
for b1, b2 being non empty set
for b3 being non empty Moore-SM_Final of b1,b2
for b4 being Element of b1
for b5 being set holds
( b5 is_result_of b4,b3 iff ex b6 being non empty Nat st
for b7 being FinSequence of b1 st b7 . 1 = b4 holds
( ( b6 <= (len b7) + 1 implies ( b5 = the OFun of b3 . ((GEN b7,the InitS of b3) . b6) & (GEN b7,the InitS of b3) . b6 in the FinalS of b3 ) ) & ( for b8 being non empty Nat st b8 < b6 & b8 <= (len b7) + 1 holds
not (GEN b7,the InitS of b3) . b8 in the FinalS of b3 ) ) );

theorem Th19: :: FSM_2:19
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being non empty Moore-SM_Final of b1,b2 st the InitS of b4 in the FinalS of b4 holds
the OFun of b4 . the InitS of b4 is_result_of b3,b4
proof end;

theorem Th20: :: FSM_2:20
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being non empty Moore-SM_Final of b1,b2 st b4 is calculating_type & b3 leads_to_final_state_of b4 & not the InitS of b4 in the FinalS of b4 holds
ex b5 being Element of b2 st b5 is_result_of b3,b4
proof end;

theorem Th21: :: FSM_2:21
for b1, b2 being non empty set
for b3 being Element of b1
for b4 being non empty Moore-SM_Final of b1,b2 st b4 is calculating_type & b3 leads_to_final_state_of b4 holds
for b5, b6 being Element of b2 st b5 is_result_of b3,b4 & b6 is_result_of b3,b4 holds
b5 = b6
proof end;

theorem Th22: :: FSM_2:22
for b1 being non empty set
for b2 being BinOp of b1
for b3 being non empty Moore-SM_Final of [:b1,b1:],b1 \/ {b1} st b3 is calculating_type & the carrier of b3 = b1 \/ {b1} & the FinalS of b3 = b1 & the InitS of b3 = b1 & the OFun of b3 = id the carrier of b3 & ( for b4, b5 being Element of b1 holds the Tran of b3 . [the InitS of b3,[b4,b5]] = b2 . b4,b5 ) holds
( b3 is halting & ( for b4, b5 being Element of b1 holds b2 . b4,b5 is_result_of [b4,b5],b3 ) )
proof end;

theorem Th23: :: FSM_2:23
for b1 being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st b1 is calculating_type & the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real st b2 >= b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b2 ) & ( for b2, b3 being Real st b2 < b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b3 ) holds
for b2, b3 being Element of REAL holds max b2,b3 is_result_of [b2,b3],b1
proof end;

theorem Th24: :: FSM_2:24
for b1 being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st b1 is calculating_type & the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real st b2 < b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b2 ) & ( for b2, b3 being Real st b2 >= b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b3 ) holds
for b2, b3 being Element of REAL holds min b2,b3 is_result_of [b2,b3],b1
proof end;

theorem Th25: :: FSM_2:25
for b1 being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st b1 is calculating_type & the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real holds the Tran of b1 . [the InitS of b1,[b2,b3]] = b2 + b3 ) holds
for b2, b3 being Element of REAL holds b2 + b3 is_result_of [b2,b3],b1
proof end;

theorem Th26: :: FSM_2:26
for b1 being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st b1 is calculating_type & the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real st ( b2 > 0 or b3 > 0 ) holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = 1 ) & ( for b2, b3 being Real st ( b2 = 0 or b3 = 0 ) & b2 <= 0 & b3 <= 0 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = 0 ) & ( for b2, b3 being Real st b2 < 0 & b3 < 0 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = - 1 ) holds
for b2, b3 being Element of REAL holds max (sgn b2),(sgn b3) is_result_of [b2,b3],b1
proof end;

registration
let c1, c2 be non empty set ;
cluster non empty calculating_type halting Moore-SM_Final of a1,a2;
existence
ex b1 being non empty Moore-SM_Final of c1,c2 st
( b1 is calculating_type & b1 is halting )
proof end;
end;

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

definition
let c1, c2 be non empty set ;
let c3 be non empty calculating_type halting Moore-SM_Final of c1,c2;
let c4 be Element of c1;
E27: c4 leads_to_final_state_of c3 by Def6;
func Result c4,c3 -> Element of a2 means :Def9: :: FSM_2:def 9
a5 is_result_of a4,a3;
uniqueness
for b1, b2 being Element of c2 st b1 is_result_of c4,c3 & b2 is_result_of c4,c3 holds
b1 = b2 by E27, Th21;
existence
ex b1 being Element of c2 st b1 is_result_of c4,c3
proof end;
end;

:: deftheorem Def9 defines Result FSM_2:def 9 :
for b1, b2 being non empty set
for b3 being non empty calculating_type halting Moore-SM_Final of b1,b2
for b4 being Element of b1
for b5 being Element of b2 holds
( b5 = Result b4,b3 iff b5 is_result_of b4,b3 );

theorem Th27: :: FSM_2:27
for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Function of {0,1},b1 holds Result b3,(b2 -TwoStatesMooreSM 0,1,b4) = b4 . 1
proof end;

theorem Th28: :: FSM_2:28
for b1 being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real st b2 >= b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b2 ) & ( for b2, b3 being Real st b2 < b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b3 ) holds
for b2, b3 being Element of REAL holds Result [b2,b3],b1 = max b2,b3
proof end;

theorem Th29: :: FSM_2:29
for b1 being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real st b2 < b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b2 ) & ( for b2, b3 being Real st b2 >= b3 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = b3 ) holds
for b2, b3 being Element of REAL holds Result [b2,b3],b1 = min b2,b3
proof end;

theorem Th30: :: FSM_2:30
for b1 being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real holds the Tran of b1 . [the InitS of b1,[b2,b3]] = b2 + b3 ) holds
for b2, b3 being Element of REAL holds Result [b2,b3],b1 = b2 + b3
proof end;

theorem Th31: :: FSM_2:31
for b1 being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of b1 = REAL \/ {REAL } & the FinalS of b1 = REAL & the InitS of b1 = REAL & the OFun of b1 = id the carrier of b1 & ( for b2, b3 being Real st ( b2 > 0 or b3 > 0 ) holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = 1 ) & ( for b2, b3 being Real st ( b2 = 0 or b3 = 0 ) & b2 <= 0 & b3 <= 0 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = 0 ) & ( for b2, b3 being Real st b2 < 0 & b3 < 0 holds
the Tran of b1 . [the InitS of b1,[b2,b3]] = - 1 ) holds
for b2, b3 being Element of REAL holds Result [b2,b3],b1 = max (sgn b2),(sgn b3)
proof end;