let X be non empty set ; for f being BinOp of X
for M being non empty Moore-SM_Final over [: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; for M being non empty Moore-SM_Final over [: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 over [:X,X:], succ X; ( 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 that
A1:
M is calculating_type
and
A2:
the carrier of M = succ X
and
A3:
the FinalS of M = X
and
A4:
the InitS of M = X
and
A5:
the OFun of M = id the carrier of M
and
A6:
for x, y being Element of X holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
; ( M is halting & ( for x, y being Element of X holds f . (x,y) is_result_of [x,y],M ) )
A7:
not the InitS of M in the FinalS of M
by A3, A4;
hereby FSM_2:def 6 for x, y being Element of X holds f . (x,y) is_result_of [x,y],M
let s be
Element of
[:X,X:];
s leads_to_final_state_of Mconsider x,
y being
object such that A9:
x in X
and A10:
y in X
and A11:
s = [x,y]
by ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Element of
X by A9, A10;
thus
s leads_to_final_state_of M
verumproof
reconsider q =
f . (
x,
y) as
State of
M by A2, XBOOLE_0:def 3;
take
q
;
FSM_2:def 5 ( q is_accessible_via s & q in the FinalS of M )
thus
q is_accessible_via s
q in the FinalS of Mproof
take w =
<*> [:X,X:];
FSM_2:def 2 the InitS of M,<*s*> ^ w -leads_to q
reconsider W =
<*s*> ^ w as
FinSequence of
[:X,X:] ;
A12:
W = <*[x,y]*>
by A11, FINSEQ_1:34;
then
len W = 1
by FINSEQ_1:39;
then A13:
ex
WI being
Element of
[:X,X:] ex
QI,
QI1 being
State of
M st
(
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 A12, FINSEQ_1:39
.=
the
Tran of
M . [ the InitS of M,(W . 1)]
by A13, FSM_1:def 2
.=
the
Tran of
M . [ the InitS of M,[x,y]]
by A11, FINSEQ_1:41
.=
f . (
x,
y)
by A6
;
hence
the
InitS of
M,
<*s*> ^ w -leads_to q
;
verum
end;
thus
q in the
FinalS of
M
by A3;
verum
end;
end;
let x, y be Element of X; f . (x,y) is_result_of [x,y],M
consider m being non zero Element of NAT such that
A14:
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
A15:
for w being FinSequence of [:X,X:]
for i being non zero 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, A8, Th18;
take
m
; FSM_2:def 8 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 zero 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:]; ( 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 zero 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 A16:
w . 1 = [x,y]
; ( ( 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 zero 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 for n being non zero 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 A17:
m <= (len w) + 1
;
( 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 A4, FSM_1:def 2;
then A18:
m <> 1
by A4, A7, A14, A16, A17;
m >= 1
by NAT_1:14;
then
m > 1
by A18, XXREAL_0:1;
then A19:
m >= 1
+ 1
by NAT_1:13;
then A20:
1
+ 1
<= (len w) + 1
by A17, XXREAL_0:2;
then
1
<= len w
by XREAL_1:6;
then
ex
WI being
Element of
[:X,X:] ex
QI,
QI1 being
State of
M st
(
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;
then A21:
(GEN (w, the InitS of M)) . 2 =
the
Tran of
M . [ the InitS of M,(w . 1)]
by FSM_1:def 2
.=
f . (
x,
y)
by A6, A16
;
A22:
(
m = 2 or
m > 2 )
by A19, 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 A2, A3, A5, A15, A16, A20, A21, A22, FUNCT_1:18;
(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 A14, A16, A17;
verum
end;
thus
for n being non zero 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 A15, A16; verum