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 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 set 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:47;
then len W = 1 by FINSEQ_1:56;
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:56
.= 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:58
.= f . x,y by A6 ;
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 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 empty 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 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, 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 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 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 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 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:8;
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:35; :: 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 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 A15, A16; :: thesis: verum