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;

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 ) )

not (GEN (w, the InitS of M)) . n in the FinalS of M by A15, A16; :: thesis: verum

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 x, y be Element of X; :: thesis: f . (x,y) is_result_of [x,y],Mlet 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

end;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

end;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

thus
q in the FinalS of M
by A3; :: thesis: verum
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;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

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

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

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;(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

not (GEN (w, the InitS of M)) . n in the FinalS of M by A15, A16; :: thesis: verum