let X be non empty set ; :: thesis: 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 ) )
let f be BinOp of X; :: thesis: 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 ) )
let M be non empty Moore-SM_Final of [:X,X:], succ X; :: thesis: ( 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 ) implies ( M is halting & ( for x, y being Element of X holds f . x,y is_result_of [x,y],M ) ) )
assume A1:
( 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 ) )
; :: thesis: ( M is halting & ( for x, y being Element of X holds f . x,y is_result_of [x,y],M ) )
then A2:
not the InitS of M in the FinalS of M
;
hereby :: according to FSM_2:def 6 :: thesis: for x, y being Element of X holds f . x,y is_result_of [x,y],M
let s be
Element of
[:X,X:];
:: thesis: s leads_to_final_state_of Mconsider x,
y being
set such that A4:
(
x in X &
y in X &
s = [x,y] )
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
X by A4;
thus
s leads_to_final_state_of M
:: thesis: verumproof
reconsider q =
f . x,
y as
State of
M by A1, XBOOLE_0:def 3;
take
q
;
:: according to FSM_2:def 5 :: thesis: ( q is_accessible_via s & q in the FinalS of M )
thus
q is_accessible_via s
:: thesis: q in the FinalS of Mproof
take w =
<*> [:X,X:];
:: according to FSM_2:def 2 :: thesis: the InitS of M,<*s*> ^ w -leads_to q
reconsider W =
<*s*> ^ w as
FinSequence of
[:X,X:] ;
A5:
W = <*[x,y]*>
by A4, FINSEQ_1:47;
then
len W = 1
by FINSEQ_1:56;
then consider WI being
Element of
[:X,X:],
QI,
QI1 being
State of
M such that A6:
(
WI = W . 1 &
QI = (GEN W,the InitS of M) . 1 &
QI1 = (GEN W,the InitS of M) . (1 + 1) &
WI -succ_of QI = QI1 )
by FSM_1:def 2;
(GEN W,the InitS of M) . ((len W) + 1) =
(GEN W,the InitS of M) . (1 + 1)
by A5, FINSEQ_1:56
.=
the
Tran of
M . [the InitS of M,(W . 1)]
by A6, FSM_1:def 2
.=
the
Tran of
M . [the InitS of M,[x,y]]
by A4, FINSEQ_1:58
.=
f . x,
y
by A1
;
hence
the
InitS of
M,
<*s*> ^ w -leads_to q
by FSM_1:def 3;
:: thesis: verum
end;
thus
q in the
FinalS of
M
by A1;
:: thesis: verum
end;
end;
let x, y be Element of X; :: thesis: f . x,y is_result_of [x,y],M
[x,y] leads_to_final_state_of M
by A3;
then consider m being non empty Element of NAT such that
A7:
for w being FinSequence of [:X,X:] st (len w) + 1 >= m & w . 1 = [x,y] holds
(GEN w,the InitS of M) . m in the FinalS of M
and
A8:
for w being FinSequence of [:X,X:]
for i being non empty Element of NAT st i <= (len w) + 1 & w . 1 = [x,y] & i < m holds
not (GEN w,the InitS of M) . i in the FinalS of M
by A1, A2, Th18;
take
m
; :: according to FSM_2:def 8 :: thesis: for w being FinSequence of [:X,X:] st w . 1 = [x,y] holds
( ( m <= (len w) + 1 implies ( f . x,y = 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 ) )
set s = [x,y];
set t = f . x,y;
let w be FinSequence of [:X,X:]; :: thesis: ( w . 1 = [x,y] implies ( ( m <= (len w) + 1 implies ( f . x,y = 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 ) ) )
assume A9:
w . 1 = [x,y]
; :: thesis: ( ( m <= (len w) + 1 implies ( f . x,y = 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 ) )
hereby :: thesis: 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
assume A10:
m <= (len w) + 1
;
:: thesis: ( f . x,y = the OFun of M . ((GEN w,the InitS of M) . m) & (GEN w,the InitS of M) . m in the FinalS of M )
(GEN w,the InitS of M) . 1
= X
by A1, FSM_1:def 2;
then
(
m <> 1 &
m >= 1 )
by A1, A2, A7, A9, A10, NAT_1:14;
then
m > 1
by XXREAL_0:1;
then A11:
m >= 1
+ 1
by NAT_1:13;
then A12:
1
+ 1
<= (len w) + 1
by A10, XXREAL_0:2;
then
( 1
<= 1 & 1
<= len w )
by XREAL_1:8;
then consider WI being
Element of
[:X,X:],
QI,
QI1 being
State of
M such that A13:
(
WI = w . 1 &
QI = (GEN w,the InitS of M) . 1 &
QI1 = (GEN w,the InitS of M) . (1 + 1) &
WI -succ_of QI = QI1 )
by FSM_1:def 2;
A14:
(GEN w,the InitS of M) . 2 =
the
Tran of
M . [the InitS of M,(w . 1)]
by A13, FSM_1:def 2
.=
f . x,
y
by A1, A9
;
A15:
(
m = 2 or
m > 2 )
by A11, XXREAL_0:1;
f . x,
y in succ X
by XBOOLE_0:def 3;
hence
f . x,
y = the
OFun of
M . ((GEN w,the InitS of M) . m)
by A1, A8, A9, A12, A14, A15, FUNCT_1:35;
:: thesis: (GEN w,the InitS of M) . m in the FinalS of Mthus
(GEN w,the InitS of M) . m in the
FinalS of
M
by A7, A9, A10;
:: thesis: verum
end;
thus
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
by A8, A9; :: thesis: verum