begin
theorem Th1:
theorem Th2:
theorem
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])*>
:: deftheorem Def1 defines calculating_type FSM_2:def 1 :
theorem Th4:
theorem Th5:
theorem
Lm1:
now
let I be non
empty set ;
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;
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;
for q being State of S holds GEN (<*> I),q, GEN w,q are_c=-comparable let q be
State of
S;
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;
verum
end;
Lm2:
now
let p,
q be
FinSequence;
( 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
;
(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;
verum
end;
theorem Th7:
:: deftheorem Def2 defines is_accessible_via FSM_2:def 2 :
:: deftheorem Def3 defines accessible FSM_2:def 3 :
theorem
theorem
theorem
theorem
:: deftheorem Def4 defines regular FSM_2:def 4 :
theorem
theorem
theorem Th14:
theorem
theorem
begin
:: deftheorem Def5 defines leads_to_final_state_of FSM_2:def 5 :
:: deftheorem Def6 defines halting FSM_2:def 6 :
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:
( 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} )
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:
theorem Th18:
begin
:: deftheorem Def8 defines is_result_of FSM_2:def 8 :
theorem
theorem Th20:
theorem Th21:
theorem Th22:
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 ) )
theorem Th23:
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
theorem Th24:
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
theorem Th25:
theorem Th26:
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
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:
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 :
theorem
theorem
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
theorem
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
theorem
theorem
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)