let X be non empty set ; :: thesis: 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; :: thesis: 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; :: 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 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) ; :: thesis: ( 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 :: 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 M
consider 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 :: thesis: verum

proof

reconsider q = f . (x,y) as State of M by A2, 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 M

proof

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:] ;
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 ; :: thesis: verum

end;

thus q in the FinalS of M by A3; :: thesis: verum

end;

end;

let x, y be Element of X; :: thesis: 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 ; :: 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 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:]; :: 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 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] ; :: 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 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 :: thesis: 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 ; :: 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 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; :: thesis: (GEN (w, the InitS of M)) . m in the FinalS of M
thus (GEN (w, the InitS of M)) . m in the FinalS of M by A14, A16, A17; :: thesis: 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; :: thesis: verum