:: FSM_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 <= 1 & 1 <= (len w) + 1 ) by NAT_1:29;
then ( 1 in dom (GEN w,q) & (GEN w,q) . 1 = q ) by A1, FINSEQ_1:3, FSM_1:def 2;
then [1,q] in GEN w,q by 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 & 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 & q . 1 = y ) by A4, A5, FINSEQ_1:58, FINSEQ_1:59;
(Del p,(len p)) ^ q = p1 ^ (<*y*> ^ q1) by A4, A5, A6, WSIERP_1:48
.= p ^ q1 by A3, A4, A7, 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 calculating_type halting strict ;
coherence
I -TwoStatesMooreSM i,f,o is halting
proof end;
end;

theorem Th18: :: FSM_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & not the InitS of M in the FinalS of M holds
ex m being non empty 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 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 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 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 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 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 Nat st n < m & n <= (len w) + 1 holds
not (GEN w,the InitS of M) . n in the FinalS of M ) ) );

theorem Th19: :: FSM_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & not the InitS of M in the FinalS of M holds
ex t being Element of O st t is_result_of s,M
proof end;

theorem Th21: :: FSM_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for f being BinOp of X
for M being non empty Moore-SM_Final of [:X,X:],X \/ {X} st M is calculating_type & the carrier of M = X \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st M is calculating_type & the carrier of M = REAL \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st M is calculating_type & the carrier of M = REAL \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st M is calculating_type & the carrier of M = REAL \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st M is calculating_type & the carrier of M = REAL \/ {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
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of M = REAL \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of M = REAL \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of M = REAL \/ {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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty calculating_type halting Moore-SM_Final of [:REAL ,REAL :],REAL \/ {REAL } st the carrier of M = REAL \/ {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;