:: FSM_2 semantic presentation begin notation let I be non empty set ; let S be non empty FSM over I; let q be State of S; let w be FinSequence of I; synonym GEN (w,q) for (q,w) -admissible ; end; registration let I be non empty set ; let S be non empty FSM over I; let q be State of S; let w be FinSequence of I; cluster GEN (w,q) -> non empty ; coherence not GEN (w,q) is empty proof len (GEN (w,q)) = (len w) + 1 by FSM_1:def_2; hence not GEN (w,q) is empty ; ::_thesis: verum end; end; theorem Th1: :: FSM_2:1 for I being non empty set for s being Element of I for S being non empty FSM over I for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> proof let I be non empty set ; ::_thesis: for s being Element of I for S being non empty FSM over I for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> let s be Element of I; ::_thesis: for S being non empty FSM over I for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> let S be non empty FSM over I; ::_thesis: for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> let q be State of S; ::_thesis: GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> A1: len <*s*> = 1 by FINSEQ_1:39; A2: len (GEN (<*s*>,q)) = (len <*s*>) + 1 by FSM_1:def_2 .= 2 by A1 ; A3: (GEN (<*s*>,q)) . 1 = q by FSM_1:def_2; 1 <= len <*s*> by FINSEQ_1:39; then consider WI being Element of I, QI, QI1 being State of S such that A4: WI = <*s*> . 1 and A5: QI = (GEN (<*s*>,q)) . 1 and A6: QI1 = (GEN (<*s*>,q)) . (1 + 1) and A7: WI -succ_of QI = QI1 by FSM_1:def_2; WI = s by A4, FINSEQ_1:40; hence GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*> by A2, A3, A5, A6, A7, FINSEQ_1:44; ::_thesis: verum end; theorem Th2: :: FSM_2:2 for I being non empty set for s1, s2 being Element of I for S being non empty FSM over I for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> proof let I be non empty set ; ::_thesis: for s1, s2 being Element of I for S being non empty FSM over I for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> let s1, s2 be Element of I; ::_thesis: for S being non empty FSM over I for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> let S be non empty FSM over I; ::_thesis: for q being State of S holds GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> let q be State of S; ::_thesis: GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> set w = <*s1,s2*>; A1: (GEN (<*s1,s2*>,q)) . 1 = q by FSM_1:def_2; A2: <*s1,s2*> = <*s1*> ^ <*s2*> by FINSEQ_1:def_9; A3: len <*s1*> = 1 by FINSEQ_1:39; GEN (<*s1*>,q) = <*q,( the Tran of S . [q,s1])*> by Th1; then (GEN (<*s1*>,q)) . (1 + 1) = the Tran of S . [q,s1] by FINSEQ_1:44; then q,<*s1*> -leads_to the Tran of S . [q,s1] by A3, FSM_1:def_3; then A4: (GEN (<*s1,s2*>,q)) . (1 + 1) = the Tran of S . [q,s1] by A2, A3, FSM_1:6; A5: len <*s1,s2*> = 2 by FINSEQ_1:44; 2 <= len <*s1,s2*> by FINSEQ_1:44; then consider WI being Element of I, QI, QI1 being State of S such that A6: WI = <*s1,s2*> . 2 and A7: QI = (GEN (<*s1,s2*>,q)) . 2 and A8: QI1 = (GEN (<*s1,s2*>,q)) . (2 + 1) and A9: WI -succ_of QI = QI1 by FSM_1:def_2; A10: WI = s2 by A6, FINSEQ_1:44; len (GEN (<*s1,s2*>,q)) = (len <*s1,s2*>) + 1 by FSM_1:def_2 .= 3 by A5 ; hence GEN (<*s1,s2*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> by A1, A4, A7, A8, A9, A10, FINSEQ_1:45; ::_thesis: verum end; theorem :: FSM_2:3 for I being non empty set for s1, s2, s3 being Element of I for S being non empty FSM over I for q being State of S holds GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> proof let I be non empty set ; ::_thesis: for s1, s2, s3 being Element of I for S being non empty FSM over I for q being State of S holds GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> let s1, s2, s3 be Element of I; ::_thesis: for S being non empty FSM over I for q being State of S holds GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> let S be non empty FSM over I; ::_thesis: for q being State of S holds GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> let q be State of S; ::_thesis: GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> set w = <*s1,s2,s3*>; reconsider w1 = <*s1,s2*>, w2 = <*s3*> as FinSequence of I ; set Q = the Tran of S . [( the Tran of S . [q,s1]),s2]; A1: <*s1,s2,s3*> = w1 ^ w2 by FINSEQ_1:43; A2: len w1 = 2 by FINSEQ_1:44; GEN (w1,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*> by Th2; then (GEN (w1,q)) . ((len w1) + 1) = the Tran of S . [( the Tran of S . [q,s1]),s2] by A2, FINSEQ_1:45; then q,w1 -leads_to the Tran of S . [( the Tran of S . [q,s1]),s2] by FSM_1:def_3; then A3: GEN (<*s1,s2,s3*>,q) = (Del ((GEN (w1,q)),((len w1) + 1))) ^ (GEN (w2,( the Tran of S . [( the Tran of S . [q,s1]),s2]))) by A1, FSM_1:8; Del ((GEN (w1,q)),((len w1) + 1)) = Del (<*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2])*>,3) by A2, Th2 .= <*q,( the Tran of S . [q,s1])*> by WSIERP_1:19 ; then GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1])*> ^ <*( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> by A3, Th1; hence GEN (<*s1,s2,s3*>,q) = <*q,( the Tran of S . [q,s1]),( the Tran of S . [( the Tran of S . [q,s1]),s2]),( the Tran of S . [( the Tran of S . [( the Tran of S . [q,s1]),s2]),s3])*> by FINSEQ_4:74; ::_thesis: verum end; definition let I be non empty set ; let S be non empty FSM over I; attrS is calculating_type means :Def1: :: FSM_2:def 1 for j being non empty Element of NAT for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j; end; :: deftheorem Def1 defines calculating_type FSM_2:def_1_:_ for I being non empty set for S being non empty FSM over I holds ( S is calculating_type iff for j being non empty Element of NAT for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j ); theorem Th4: :: FSM_2:4 for I being non empty set for S being non empty FSM over I st S is calculating_type holds for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is calculating_type holds for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable let S be non empty FSM over I; ::_thesis: ( S is calculating_type implies for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) assume A1: S is calculating_type ; ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) assume A2: w1 . 1 = w2 . 1 ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable set A = (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))); ( 1 + (len w1) <= 1 + (len w2) or 1 + (len w2) <= 1 + (len w1) ) ; then A3: ( ( Seg (1 + (len w1)) c= Seg (1 + (len w2)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w1)) ) or ( Seg (1 + (len w2)) c= Seg (1 + (len w1)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w2)) ) ) by FINSEQ_1:5, FINSEQ_1:7; A4: len (GEN (w1, the InitS of S)) = 1 + (len w1) by FSM_1:def_2; A5: len (GEN (w2, the InitS of S)) = 1 + (len w2) by FSM_1:def_2; A6: dom (GEN (w1, the InitS of S)) = Seg (1 + (len w1)) by A4, FINSEQ_1:def_3; A7: dom (GEN (w2, the InitS of S)) = Seg (1 + (len w2)) by A5, FINSEQ_1:def_3; now__::_thesis:_for_x_being_set_st_x_in_(Seg_(1_+_(len_w1)))_/\_(Seg_(1_+_(len_w2)))_holds_ (GEN_(w1,_the_InitS_of_S))_._x_=_(GEN_(w2,_the_InitS_of_S))_._x let x be set ; ::_thesis: ( x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) implies (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x ) assume A8: x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) ; ::_thesis: (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x then reconsider i = x as Element of NAT ; A9: i >= 1 by A3, A8, FINSEQ_1:1; A10: i <= 1 + (len w1) by A3, A8, FINSEQ_1:1; i <= 1 + (len w2) by A3, A8, FINSEQ_1:1; hence (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x by A1, A2, A9, A10, Def1; ::_thesis: verum end; hence ( GEN (w1, the InitS of S) c= GEN (w2, the InitS of S) or GEN (w2, the InitS of S) c= GEN (w1, the InitS of S) ) by A3, A6, A7, GRFUNC_1:2; :: according to XBOOLE_0:def_9 ::_thesis: verum end; theorem Th5: :: FSM_2:5 for I being non empty set for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds S is calculating_type proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds S is calculating_type let S be non empty FSM over I; ::_thesis: ( ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) implies S is calculating_type ) assume A1: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ; ::_thesis: S is calculating_type let j be non empty Element of NAT ; :: according to FSM_2:def_1 ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j ) assume that A2: w1 . 1 = w2 . 1 and A3: j <= (len w1) + 1 and A4: j <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j A5: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def_3 .= Seg ((len w1) + 1) by FSM_1:def_2 ; A6: dom (GEN (w2, the InitS of S)) = Seg (len (GEN (w2, the InitS of S))) by FINSEQ_1:def_3 .= Seg ((len w2) + 1) by FSM_1:def_2 ; A7: 1 <= j by NAT_1:14; then A8: j in dom (GEN (w1, the InitS of S)) by A3, A5, FINSEQ_1:1; j in dom (GEN (w2, the InitS of S)) by A4, A6, A7, FINSEQ_1:1; then A9: j in (dom (GEN (w1, the InitS of S))) /\ (dom (GEN (w2, the InitS of S))) by A8, XBOOLE_0:def_4; GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by A1, A2; then ( GEN (w1, the InitS of S) c= GEN (w2, the InitS of S) or GEN (w2, the InitS of S) c= GEN (w1, the InitS of S) ) by XBOOLE_0:def_9; then GEN (w1, the InitS of S) tolerates GEN (w2, the InitS of S) by PARTFUN1:54; hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A9, PARTFUN1:def_4; ::_thesis: verum end; theorem :: FSM_2:6 for I being non empty set for S being non empty FSM over I st S is calculating_type holds for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is calculating_type holds for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) let S be non empty FSM over I; ::_thesis: ( S is calculating_type implies for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) assume A1: S is calculating_type ; ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) assume that A2: w1 . 1 = w2 . 1 and A3: len w1 = len w2 ; ::_thesis: GEN (w1, the InitS of S) = GEN (w2, the InitS of S) A4: len (GEN (w1, the InitS of S)) = 1 + (len w1) by FSM_1:def_2; len (GEN (w2, the InitS of S)) = 1 + (len w2) by FSM_1:def_2; hence GEN (w1, the InitS of S) = GEN (w2, the InitS of S) by A1, A2, A3, A4, Th4, TREES_1:4; ::_thesis: verum end; Lm1: now__::_thesis:_for_I_being_non_empty_set_ for_S_being_non_empty_FSM_over_I for_w_being_FinSequence_of_I for_q_being_State_of_S_holds_GEN_((<*>_I),q),_GEN_(w,q)_are_c=-comparable let I be non empty set ; ::_thesis: for S being non empty FSM over I for w being FinSequence of I for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable let S be non empty FSM over I; ::_thesis: for w being FinSequence of I for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable let w be FinSequence of I; ::_thesis: for q being State of S holds GEN ((<*> I),q), GEN (w,q) are_c=-comparable let q be State of S; ::_thesis: GEN ((<*> I),q), GEN (w,q) are_c=-comparable A1: dom (GEN (w,q)) = Seg (len (GEN (w,q))) by FINSEQ_1:def_3 .= Seg ((len w) + 1) by FSM_1:def_2 ; 1 <= (len w) + 1 by NAT_1:11; then A2: 1 in dom (GEN (w,q)) by A1, FINSEQ_1:1; (GEN (w,q)) . 1 = q by FSM_1:def_2; then [1,q] in GEN (w,q) by A2, FUNCT_1:def_2; then {[1,q]} c= GEN (w,q) by ZFMISC_1:31; then <*q*> c= GEN (w,q) by FINSEQ_1:def_5; then GEN ((<*> I),q) c= GEN (w,q) by FSM_1:1; hence GEN ((<*> I),q), GEN (w,q) are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum end; Lm2: now__::_thesis:_for_p,_q_being_FinSequence_st_p_<>_{}_&_q_<>_{}_&_p_._(len_p)_=_q_._1_holds_ (Del_(p,(len_p)))_^_q_=_p_^_(Del_(q,1)) let p, q be FinSequence; ::_thesis: ( p <> {} & q <> {} & p . (len p) = q . 1 implies (Del (p,(len p))) ^ q = p ^ (Del (q,1)) ) assume that A1: p <> {} and A2: q <> {} and A3: p . (len p) = q . 1 ; ::_thesis: (Del (p,(len p))) ^ q = p ^ (Del (q,1)) consider p1 being FinSequence, x being set such that A4: p = p1 ^ <*x*> by A1, FINSEQ_1:46; consider y being set , q1 being FinSequence such that A5: q = <*y*> ^ q1 and len q = (len q1) + 1 by A2, REWRITE1:5; A6: len p = (len p1) + (len <*x*>) by A4, FINSEQ_1:22 .= (len p1) + 1 by FINSEQ_1:39 ; then A7: p . (len p) = x by A4, FINSEQ_1:42; A8: q . 1 = y by A5, FINSEQ_1:41; (Del (p,(len p))) ^ q = p1 ^ (<*y*> ^ q1) by A4, A5, A6, WSIERP_1:40 .= p ^ q1 by A3, A4, A7, A8, FINSEQ_1:32 ; hence (Del (p,(len p))) ^ q = p ^ (Del (q,1)) by A5, WSIERP_1:40; ::_thesis: verum end; theorem Th7: :: FSM_2:7 for I being non empty set for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds S is calculating_type proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds S is calculating_type let S be non empty FSM over I; ::_thesis: ( ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) implies S is calculating_type ) assume A1: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ; ::_thesis: S is calculating_type now__::_thesis:_for_w1,_w2_being_FinSequence_of_I_st_w1_._1_=_w2_._1_holds_ GEN_(w1,_the_InitS_of_S),_GEN_(w2,_the_InitS_of_S)_are_c=-comparable let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) assume A2: w1 . 1 = w2 . 1 ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable thus GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ::_thesis: verum proof percases ( w1 = <*> I or w2 = <*> I or ( w1 <> {} & w2 <> {} ) ) ; suppose ( w1 = <*> I or w2 = <*> I ) ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable hence GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by Lm1; ::_thesis: verum end; supposeA3: ( w1 <> {} & w2 <> {} ) ; ::_thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable reconsider v1 = w2 | (Seg (len w1)), v2 = w1 | (Seg (len w2)) as FinSequence of I by FINSEQ_1:18; ( len w1 <= len w2 or len w2 <= len w1 ) ; then A4: ( ( v1 = w2 & len v2 = len w2 & len w1 >= len w2 ) or ( len v1 = len w1 & v2 = w1 & len w1 <= len w2 ) ) by FINSEQ_1:17, FINSEQ_2:20; A5: len w1 >= 0 + 1 by A3, NAT_1:13; A6: len w2 >= 0 + 1 by A3, NAT_1:13; A7: v1 . 1 = w2 . 1 by A4, A5, GRAPH_2:2; v2 . 1 = w1 . 1 by A4, A6, GRAPH_2:2; then A8: ( GEN (v1, the InitS of S) = GEN (w1, the InitS of S) or GEN (v2, the InitS of S) = GEN (w2, the InitS of S) ) by A1, A2, A4, A7; consider s1 being FinSequence such that A9: w2 = v1 ^ s1 by FINSEQ_1:80; consider s2 being FinSequence such that A10: w1 = v2 ^ s2 by FINSEQ_1:80; reconsider s1 = s1, s2 = s2 as FinSequence of I by A9, A10, FINSEQ_1:36; v1 <> {} proof assume A11: v1 = {} ; ::_thesis: contradiction A12: dom v1 = (dom w2) /\ (Seg (len w1)) by RELAT_1:61 .= (Seg (len w2)) /\ (Seg (len w1)) by FINSEQ_1:def_3 ; ( len w2 <= len w1 or len w1 <= len w2 ) ; then ( dom v1 = Seg (len w2) or dom v1 = Seg (len w1) ) by A12, FINSEQ_1:7; then ( len v1 = len w2 or len v1 = len w1 ) by FINSEQ_1:def_3; hence contradiction by A3, A11; ::_thesis: verum end; then 1 <= len v1 by NAT_1:14; then A13: ex WI being Element of I ex QI, QI1 being State of S st ( WI = v1 . (len v1) & QI = (GEN (v1, the InitS of S)) . (len v1) & QI1 = (GEN (v1, the InitS of S)) . ((len v1) + 1) & WI -succ_of QI = QI1 ) by FSM_1:def_2; v2 <> {} proof assume v2 = {} ; ::_thesis: contradiction then A14: len v2 = 0 ; A15: dom v2 = (dom w1) /\ (Seg (len w2)) by RELAT_1:61 .= (Seg (len w1)) /\ (Seg (len w2)) by FINSEQ_1:def_3 ; ( len w2 <= len w1 or len w1 <= len w2 ) ; then ( dom v2 = Seg (len w2) or dom v2 = Seg (len w1) ) by A15, FINSEQ_1:7; hence contradiction by A3, A14, FINSEQ_1:def_3; ::_thesis: verum end; then 1 <= len v2 by NAT_1:14; then ex WI2 being Element of I ex QI2, QI12 being State of S st ( WI2 = v2 . (len v2) & QI2 = (GEN (v2, the InitS of S)) . (len v2) & QI12 = (GEN (v2, the InitS of S)) . ((len v2) + 1) & WI2 -succ_of QI2 = QI12 ) by FSM_1:def_2; then reconsider q1 = (GEN (v1, the InitS of S)) . ((len v1) + 1), q2 = (GEN (v2, the InitS of S)) . ((len v2) + 1) as State of S by A13; A16: (GEN (s1,q1)) . 1 = q1 by FSM_1:def_2; A17: (GEN (s2,q2)) . 1 = q2 by FSM_1:def_2; A18: len (GEN (v1, the InitS of S)) = (len v1) + 1 by FSM_1:def_2; A19: len (GEN (v2, the InitS of S)) = (len v2) + 1 by FSM_1:def_2; the InitS of S,v1 -leads_to q1 by FSM_1:def_3; then A20: GEN (w2, the InitS of S) = (Del ((GEN (v1, the InitS of S)),((len v1) + 1))) ^ (GEN (s1,q1)) by A9, FSM_1:8 .= (GEN (v1, the InitS of S)) ^ (Del ((GEN (s1,q1)),1)) by A16, A18, Lm2 ; the InitS of S,v2 -leads_to q2 by FSM_1:def_3; then GEN (w1, the InitS of S) = (Del ((GEN (v2, the InitS of S)),((len v2) + 1))) ^ (GEN (s2,q2)) by A10, FSM_1:8 .= (GEN (v2, the InitS of S)) ^ (Del ((GEN (s2,q2)),1)) by A17, A19, Lm2 ; then ( GEN (w1, the InitS of S) c= GEN (w2, the InitS of S) or GEN (w2, the InitS of S) c= GEN (w1, the InitS of S) ) by A8, A20, TREES_1:1; hence GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum end; end; end; end; hence S is calculating_type by Th5; ::_thesis: verum end; definition let I be non empty set ; let S be non empty FSM over I; let q be State of S; let s be Element of I; predq is_accessible_via s means :Def2: :: FSM_2:def 2 ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q; end; :: deftheorem Def2 defines is_accessible_via FSM_2:def_2_:_ for I being non empty set for S being non empty FSM over I for q being State of S for s being Element of I holds ( q is_accessible_via s iff ex w being FinSequence of I st the InitS of S,<*s*> ^ w -leads_to q ); definition let I be non empty set ; let S be non empty FSM over I; let q be State of S; attrq is accessible means :Def3: :: FSM_2:def 3 ex w being FinSequence of I st the InitS of S,w -leads_to q; end; :: deftheorem Def3 defines accessible FSM_2:def_3_:_ for I being non empty set for S being non empty FSM over I for q being State of S holds ( q is accessible iff ex w being FinSequence of I st the InitS of S,w -leads_to q ); theorem :: FSM_2:8 for I being non empty set for s being Element of I for S being non empty FSM over I for q being State of S st q is_accessible_via s holds q is accessible proof let I be non empty set ; ::_thesis: for s being Element of I for S being non empty FSM over I for q being State of S st q is_accessible_via s holds q is accessible let s be Element of I; ::_thesis: for S being non empty FSM over I for q being State of S st q is_accessible_via s holds q is accessible let S be non empty FSM over I; ::_thesis: for q being State of S st q is_accessible_via s holds q is accessible let q be State of S; ::_thesis: ( q is_accessible_via s implies q is accessible ) assume q is_accessible_via s ; ::_thesis: q is accessible then consider W being FinSequence of I such that A1: the InitS of S,<*s*> ^ W -leads_to q by Def2; take <*s*> ^ W ; :: according to FSM_2:def_3 ::_thesis: the InitS of S,<*s*> ^ W -leads_to q thus the InitS of S,<*s*> ^ W -leads_to q by A1; ::_thesis: verum end; theorem :: FSM_2:9 for I being non empty set for S being non empty FSM over I for q being State of S st q is accessible & q <> the InitS of S holds ex s being Element of I st q is_accessible_via s proof let I be non empty set ; ::_thesis: for S being non empty FSM over I for q being State of S st q is accessible & q <> the InitS of S holds ex s being Element of I st q is_accessible_via s let S be non empty FSM over I; ::_thesis: for q being State of S st q is accessible & q <> the InitS of S holds ex s being Element of I st q is_accessible_via s let q be State of S; ::_thesis: ( q is accessible & q <> the InitS of S implies ex s being Element of I st q is_accessible_via s ) assume that A1: q is accessible and A2: q <> the InitS of S ; ::_thesis: ex s being Element of I st q is_accessible_via s consider W being FinSequence of I such that A3: the InitS of S,W -leads_to q by A1, Def3; W <> {} proof assume W = {} ; ::_thesis: contradiction then len W = 0 ; then (GEN (W, the InitS of S)) . ((len W) + 1) = the InitS of S by FSM_1:def_2; hence contradiction by A2, A3, FSM_1:def_3; ::_thesis: verum end; then consider S being Element of I, w9 being FinSequence of I such that W . 1 = S and A4: W = <*S*> ^ w9 by FINSEQ_3:102; take S ; ::_thesis: q is_accessible_via S thus q is_accessible_via S by A3, A4, Def2; ::_thesis: verum end; theorem :: FSM_2:10 for I being non empty set for S being non empty FSM over I holds the InitS of S is accessible proof let I be non empty set ; ::_thesis: for S being non empty FSM over I holds the InitS of S is accessible let S be non empty FSM over I; ::_thesis: the InitS of S is accessible set w = <*> I; (GEN ((<*> I), the InitS of S)) . ((len (<*> I)) + 1) = the InitS of S by FSM_1:def_2; then the InitS of S, <*> I -leads_to the InitS of S by FSM_1:def_3; hence the InitS of S is accessible by Def3; ::_thesis: verum end; theorem :: FSM_2:11 for I being non empty set for s being Element of I for S being non empty FSM over I for q being State of S st S is calculating_type & q is_accessible_via s holds ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) proof let I be non empty set ; ::_thesis: for s being Element of I for S being non empty FSM over I for q being State of S st S is calculating_type & q is_accessible_via s holds ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) let s be Element of I; ::_thesis: for S being non empty FSM over I for q being State of S st S is calculating_type & q is_accessible_via s holds ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) let S be non empty FSM over I; ::_thesis: for q being State of S st S is calculating_type & q is_accessible_via s holds ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) let q be State of S; ::_thesis: ( S is calculating_type & q is_accessible_via s implies ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) ) assume A1: S is calculating_type ; ::_thesis: ( not q is_accessible_via s or ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) ) given w being FinSequence of I such that A2: the InitS of S,<*s*> ^ w -leads_to q ; :: according to FSM_2:def_2 ::_thesis: ex m being non empty Element of NAT st for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) defpred S1[ Nat] means ( q = (GEN ((<*s*> ^ w), the InitS of S)) . $1 & $1 >= 1 & $1 <= (len (<*s*> ^ w)) + 1 ); A3: (len (<*s*> ^ w)) + 1 >= 1 by NAT_1:11; q = (GEN ((<*s*> ^ w), the InitS of S)) . ((len (<*s*> ^ w)) + 1) by A2, FSM_1:def_3; then A4: ex m being Nat st S1[m] by A3; consider m being Nat such that A5: S1[m] and A6: for k being Nat st S1[k] holds m <= k from NAT_1:sch_5(A4); reconsider m = m as non empty Element of NAT by A5, ORDINAL1:def_12; take m ; ::_thesis: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds ( q = (GEN (w, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w, the InitS of S)) . i <> q ) ) let w1 be FinSequence of I; ::_thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies ( q = (GEN (w1, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w1, the InitS of S)) . i <> q ) ) ) assume that A7: (len w1) + 1 >= m and A8: w1 . 1 = s ; ::_thesis: ( q = (GEN (w1, the InitS of S)) . m & ( for i being non empty Element of NAT st i < m holds (GEN (w1, the InitS of S)) . i <> q ) ) (<*s*> ^ w) . 1 = s by FINSEQ_1:41; then GEN (w1, the InitS of S), GEN ((<*s*> ^ w), the InitS of S) are_c=-comparable by A1, A8, Th4; then A9: ( GEN (w1, the InitS of S) c= GEN ((<*s*> ^ w), the InitS of S) or GEN ((<*s*> ^ w), the InitS of S) c= GEN (w1, the InitS of S) ) by XBOOLE_0:def_9; A10: dom (GEN ((<*s*> ^ w), the InitS of S)) = Seg (len (GEN ((<*s*> ^ w), the InitS of S))) by FINSEQ_1:def_3 .= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def_2 ; A11: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def_3 .= Seg ((len w1) + 1) by FSM_1:def_2 ; A12: m in dom (GEN ((<*s*> ^ w), the InitS of S)) by A5, A10, FINSEQ_1:1; m in dom (GEN (w1, the InitS of S)) by A5, A7, A11, FINSEQ_1:1; hence q = (GEN (w1, the InitS of S)) . m by A5, A9, A12, GRFUNC_1:2; ::_thesis: for i being non empty Element of NAT st i < m holds (GEN (w1, the InitS of S)) . i <> q let i be non empty Element of NAT ; ::_thesis: ( i < m implies (GEN (w1, the InitS of S)) . i <> q ) assume A13: i < m ; ::_thesis: (GEN (w1, the InitS of S)) . i <> q A14: 1 <= i by NAT_1:14; A15: i <= (len (<*s*> ^ w)) + 1 by A5, A13, XXREAL_0:2; A16: i <= (len w1) + 1 by A7, A13, XXREAL_0:2; A17: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def_3 .= Seg ((len w1) + 1) by FSM_1:def_2 ; dom (GEN ((<*s*> ^ w), the InitS of S)) = Seg (len (GEN ((<*s*> ^ w), the InitS of S))) by FINSEQ_1:def_3 .= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def_2 ; then A18: i in dom (GEN ((<*s*> ^ w), the InitS of S)) by A14, A15, FINSEQ_1:1; A19: i in dom (GEN (w1, the InitS of S)) by A14, A16, A17, FINSEQ_1:1; assume (GEN (w1, the InitS of S)) . i = q ; ::_thesis: contradiction then q = (GEN ((<*s*> ^ w), the InitS of S)) . i by A9, A18, A19, GRFUNC_1:2; hence contradiction by A6, A13, A14, A15; ::_thesis: verum end; definition let I be non empty set ; let S be non empty FSM over I; attrS is regular means :Def4: :: FSM_2:def 4 for q being State of S holds q is accessible ; end; :: deftheorem Def4 defines regular FSM_2:def_4_:_ for I being non empty set for S being non empty FSM over I holds ( S is regular iff for q being State of S holds q is accessible ); theorem :: FSM_2:12 for I being non empty set for S being non empty FSM over I st ( for s1, s2 being Element of I for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds S is calculating_type proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for s1, s2 being Element of I for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds S is calculating_type let S be non empty FSM over I; ::_thesis: ( ( for s1, s2 being Element of I for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) implies S is calculating_type ) assume A1: for s1, s2 being Element of I for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ; ::_thesis: S is calculating_type for j being non empty Element of NAT for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j proof let j be non empty Element of NAT ; ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j ) assume that A2: w1 . 1 = w2 . 1 and A3: j <= (len w1) + 1 and A4: j <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j defpred S1[ Nat] means for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & $1 <= (len w1) + 1 & $1 <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . $1 = (GEN (w2, the InitS of S)) . $1; A5: S1[1] proof let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) (GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def_2; hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def_2; ::_thesis: verum end; A6: for h being non empty Nat st S1[h] holds S1[h + 1] proof let h be non empty Nat; ::_thesis: ( S1[h] implies S1[h + 1] ) assume A7: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & h <= (len w1) + 1 & h <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . h = (GEN (w2, the InitS of S)) . h ; ::_thesis: S1[h + 1] let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & h + 1 <= (len w1) + 1 & h + 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) ) assume that A8: w1 . 1 = w2 . 1 and A9: h + 1 <= (len w1) + 1 and A10: h + 1 <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) A11: h <= len w1 by A9, XREAL_1:6; A12: h <= (len w1) + 1 by A9, NAT_1:13; 1 <= h by NAT_1:14; then consider WI being Element of I, QI, QI1 being State of S such that WI = w1 . h and A13: QI = (GEN (w1, the InitS of S)) . h and A14: QI1 = (GEN (w1, the InitS of S)) . (h + 1) and A15: WI -succ_of QI = QI1 by A11, FSM_1:def_2; A16: h <= len w2 by A10, XREAL_1:6; A17: h <= (len w2) + 1 by A10, NAT_1:13; 1 <= h by NAT_1:14; then consider WI2 being Element of I, QI2, QI12 being State of S such that WI2 = w2 . h and A18: QI2 = (GEN (w2, the InitS of S)) . h and A19: QI12 = (GEN (w2, the InitS of S)) . (h + 1) and A20: WI2 -succ_of QI2 = QI12 by A16, FSM_1:def_2; QI = QI2 by A7, A8, A12, A13, A17, A18; hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A14, A15, A19, A20; ::_thesis: verum end; for j being non empty Nat holds S1[j] from NAT_1:sch_10(A5, A6); hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A2, A3, A4; ::_thesis: verum end; hence S is calculating_type by Def1; ::_thesis: verum end; theorem :: FSM_2:13 for I being non empty set for S being non empty FSM over I st ( for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds S is calculating_type proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st ( for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds S is calculating_type let S be non empty FSM over I; ::_thesis: ( ( for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) implies S is calculating_type ) assume that A1: for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] and A2: for s being Element of I for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ; ::_thesis: S is calculating_type A3: for j being non empty Element of NAT st j >= 2 holds for w1 being FinSequence of I st j <= (len w1) + 1 holds (GEN (w1, the InitS of S)) . j <> the InitS of S proof let j be non empty Element of NAT ; ::_thesis: ( j >= 2 implies for w1 being FinSequence of I st j <= (len w1) + 1 holds (GEN (w1, the InitS of S)) . j <> the InitS of S ) assume j >= 2 ; ::_thesis: for w1 being FinSequence of I st j <= (len w1) + 1 holds (GEN (w1, the InitS of S)) . j <> the InitS of S then j <> 1 ; then A4: not j is trivial by NAT_2:def_1; defpred S1[ Nat] means for w1 being FinSequence of I st $1 <= (len w1) + 1 holds (GEN (w1, the InitS of S)) . $1 <> the InitS of S; A5: S1[2] proof let w1 be FinSequence of I; ::_thesis: ( 2 <= (len w1) + 1 implies (GEN (w1, the InitS of S)) . 2 <> the InitS of S ) assume 2 <= (len w1) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . 2 <> the InitS of S then 1 + 1 <= (len w1) + 1 ; then 1 <= len w1 by XREAL_1:6; then ex WI being Element of I ex QI, QI1 being State of S st ( WI = w1 . 1 & QI = (GEN (w1, the InitS of S)) . 1 & QI1 = (GEN (w1, the InitS of S)) . (1 + 1) & WI -succ_of QI = QI1 ) by FSM_1:def_2; hence (GEN (w1, the InitS of S)) . 2 <> the InitS of S by A2; ::_thesis: verum end; A6: for h being non trivial Nat st S1[h] holds S1[h + 1] proof let h be non trivial Nat; ::_thesis: ( S1[h] implies S1[h + 1] ) assume for w1 being FinSequence of I st h <= (len w1) + 1 holds (GEN (w1, the InitS of S)) . h <> the InitS of S ; ::_thesis: S1[h + 1] let w1 be FinSequence of I; ::_thesis: ( h + 1 <= (len w1) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S ) assume A7: h + 1 <= (len w1) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S A8: 1 <= h by NAT_1:14; h <= len w1 by A7, XREAL_1:6; then ex WI being Element of I ex QI, QI1 being State of S st ( WI = w1 . h & QI = (GEN (w1, the InitS of S)) . h & QI1 = (GEN (w1, the InitS of S)) . (h + 1) & WI -succ_of QI = QI1 ) by A8, FSM_1:def_2; hence (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S by A2; ::_thesis: verum end; for h being non trivial Nat holds S1[h] from NAT_2:sch_2(A5, A6); hence for w1 being FinSequence of I st j <= (len w1) + 1 holds (GEN (w1, the InitS of S)) . j <> the InitS of S by A4; ::_thesis: verum end; for j being non empty Element of NAT for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j proof let j be non empty Element of NAT ; ::_thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j ) assume that A9: w1 . 1 = w2 . 1 and A10: j <= (len w1) + 1 and A11: j <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j defpred S1[ Nat] means for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & $1 <= (len w1) + 1 & $1 <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . $1 = (GEN (w2, the InitS of S)) . $1; A12: S1[1] proof let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) (GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def_2; hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def_2; ::_thesis: verum end; A13: for h being non empty Nat st S1[h] holds S1[h + 1] proof let h be non empty Nat; ::_thesis: ( S1[h] implies S1[h + 1] ) assume A14: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & h <= (len w1) + 1 & h <= (len w2) + 1 holds (GEN (w1, the InitS of S)) . h = (GEN (w2, the InitS of S)) . h ; ::_thesis: S1[h + 1] let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & h + 1 <= (len w1) + 1 & h + 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) ) assume that A15: w1 . 1 = w2 . 1 and A16: h + 1 <= (len w1) + 1 and A17: h + 1 <= (len w2) + 1 ; ::_thesis: (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) A18: h <= len w1 by A16, XREAL_1:6; A19: h <= (len w1) + 1 by A16, NAT_1:13; A20: 1 <= h by NAT_1:14; then consider WI being Element of I, QI, QI1 being State of S such that A21: WI = w1 . h and A22: QI = (GEN (w1, the InitS of S)) . h and A23: QI1 = (GEN (w1, the InitS of S)) . (h + 1) and A24: WI -succ_of QI = QI1 by A18, FSM_1:def_2; A25: h <= len w2 by A17, XREAL_1:6; A26: h <= (len w2) + 1 by A17, NAT_1:13; 1 <= h by NAT_1:14; then consider WI2 being Element of I, QI2, QI12 being State of S such that A27: WI2 = w2 . h and A28: QI2 = (GEN (w2, the InitS of S)) . h and A29: QI12 = (GEN (w2, the InitS of S)) . (h + 1) and A30: WI2 -succ_of QI2 = QI12 by A25, FSM_1:def_2; A31: QI = QI2 by A14, A15, A19, A22, A26, A28; A32: h in NAT by ORDINAL1:def_12; ( h = 1 or h > 1 ) by A20, XXREAL_0:1; then ( h = 1 or h >= 1 + 1 ) by NAT_1:13; hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A3, A15, A19, A21, A22, A23, A24, A27, A29, A30, A31, A32; ::_thesis: verum end; for j being non empty Nat holds S1[j] from NAT_1:sch_10(A12, A13); hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A9, A10, A11; ::_thesis: verum end; hence S is calculating_type by Def1; ::_thesis: verum end; theorem Th14: :: FSM_2:14 for I being non empty set for S being non empty FSM over I st S is regular & S is calculating_type holds for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 let S be non empty FSM over I; ::_thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 ) assume that A1: S is regular and A2: S is calculating_type ; ::_thesis: for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 let s1, s2 be Element of I; ::_thesis: for q being State of S st q <> the InitS of S holds (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 let q be State of S; ::_thesis: ( q <> the InitS of S implies (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 ) assume A3: q <> the InitS of S ; ::_thesis: (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 q is accessible by A1, Def4; then consider w being FinSequence of I such that A4: the InitS of S,w -leads_to q by Def3; w <> {} proof assume w = {} ; ::_thesis: contradiction then len w = 0 ; then (GEN (w, the InitS of S)) . ((len w) + 1) = the InitS of S by FSM_1:def_2; hence contradiction by A3, A4, FSM_1:def_3; ::_thesis: verum end; then consider x being Element of I, w9 being FinSequence of I such that w . 1 = x and A5: w = <*x*> ^ w9 by FINSEQ_3:102; set w1 = w ^ <*s1*>; set w2 = w ^ <*s2*>; len <*x*> = 1 by FINSEQ_1:39; then (len <*x*>) + (len w9) >= 1 by NAT_1:11; then len w >= 1 by A5, FINSEQ_1:22; then A6: 1 in dom w by FINSEQ_3:25; then w . 1 = (w ^ <*s1*>) . 1 by FINSEQ_1:def_7; then A7: (w ^ <*s1*>) . 1 = (w ^ <*s2*>) . 1 by A6, FINSEQ_1:def_7; A8: len <*s1*> = 1 by FINSEQ_1:39; then A9: len (w ^ <*s1*>) = (len w) + 1 by FINSEQ_1:22; A10: len <*s2*> = 1 by FINSEQ_1:39; then A11: len (w ^ <*s2*>) = (len w) + 1 by FINSEQ_1:22; A12: len (w ^ <*s1*>) = len (w ^ <*s2*>) by A9, A10, FINSEQ_1:22; set p = Del ((GEN (w, the InitS of S)),((len w) + 1)); set p1 = GEN (<*s1*>,q); A13: GEN ((w ^ <*s1*>), the InitS of S) = (Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q)) by A4, FSM_1:8; A14: len (GEN (w, the InitS of S)) = (len w) + 1 by FSM_1:def_2; then A15: len (Del ((GEN (w, the InitS of S)),((len w) + 1))) = len w by PRE_POLY:12; A16: len (GEN (<*s1*>,q)) = (len <*s1*>) + 1 by FSM_1:def_2 .= 1 + 1 by FINSEQ_1:39 ; A17: len (GEN ((w ^ <*s1*>), the InitS of S)) = len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q))) by A4, FSM_1:8 .= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s1*>,q))) by FINSEQ_1:22 .= (len w) + (1 + 1) by A14, A16, PRE_POLY:12 .= ((len w) + 1) + 1 .= (len (w ^ <*s1*>)) + 1 by A8, FINSEQ_1:22 ; A18: (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + 1 <= (len (w ^ <*s1*>)) + 1 by A9, A15, NAT_1:11; len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q))) = (len (w ^ <*s1*>)) + 1 by A4, A17, FSM_1:8; then (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s1*>,q))) = (len (w ^ <*s1*>)) + 1 by FINSEQ_1:22; then A19: (GEN ((w ^ <*s1*>), the InitS of S)) . ((len (w ^ <*s1*>)) + 1) = (GEN (<*s1*>,q)) . (((len (w ^ <*s1*>)) + 1) - (len (Del ((GEN (w, the InitS of S)),((len w) + 1))))) by A13, A18, FINSEQ_1:23 .= (GEN (<*s1*>,q)) . (((len (w ^ <*s1*>)) + 1) - (len w)) by A14, PRE_POLY:12 .= (GEN (<*s1*>,q)) . ((((len w) + 1) + 1) - (len w)) by A8, FINSEQ_1:22 .= (GEN (<*s1*>,q)) . 2 ; set p2 = GEN (<*s2*>,q); A20: GEN ((w ^ <*s2*>), the InitS of S) = (Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q)) by A4, FSM_1:8; A21: len (GEN (<*s2*>,q)) = (len <*s2*>) + 1 by FSM_1:def_2 .= 1 + 1 by FINSEQ_1:39 ; A22: len (GEN ((w ^ <*s2*>), the InitS of S)) = len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q))) by A4, FSM_1:8 .= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s2*>,q))) by FINSEQ_1:22 .= (len w) + (1 + 1) by A14, A21, PRE_POLY:12 .= ((len w) + 1) + 1 .= (len (w ^ <*s2*>)) + 1 by A10, FINSEQ_1:22 ; (len w) + 1 <= (len (w ^ <*s2*>)) + 1 by A11, NAT_1:11; then A23: (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + 1 <= (len (w ^ <*s2*>)) + 1 by A14, PRE_POLY:12; len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q))) = (len (w ^ <*s2*>)) + 1 by A4, A22, FSM_1:8; then (len (w ^ <*s2*>)) + 1 <= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s2*>,q))) by FINSEQ_1:22; then (GEN ((w ^ <*s2*>), the InitS of S)) . ((len (w ^ <*s2*>)) + 1) = (GEN (<*s2*>,q)) . (((len (w ^ <*s2*>)) + 1) - (len (Del ((GEN (w, the InitS of S)),((len w) + 1))))) by A20, A23, FINSEQ_1:23 .= (GEN (<*s2*>,q)) . (((len (w ^ <*s2*>)) + 1) - (len w)) by A14, PRE_POLY:12 .= (GEN (<*s2*>,q)) . ((((len w) + 1) + 1) - (len w)) by A10, FINSEQ_1:22 .= (GEN (<*s2*>,q)) . 2 ; hence (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 by A2, A7, A12, A19, Def1; ::_thesis: verum end; theorem :: FSM_2:15 for I being non empty set for S being non empty FSM over I st S is regular & S is calculating_type holds for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] let S be non empty FSM over I; ::_thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) assume that A1: S is regular and A2: S is calculating_type ; ::_thesis: for s1, s2 being Element of I for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] let s1, s2 be Element of I; ::_thesis: for q being State of S st q <> the InitS of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] let q be State of S; ::_thesis: ( q <> the InitS of S implies the Tran of S . [q,s1] = the Tran of S . [q,s2] ) assume A3: q <> the InitS of S ; ::_thesis: the Tran of S . [q,s1] = the Tran of S . [q,s2] set w1 = <*s1*>; set w2 = <*s2*>; A4: len <*s1*> = 0 + 1 by FINSEQ_1:39; reconsider j = len <*s1*> as non empty Element of NAT ; consider WI being Element of I, QI, QI1 being State of S such that A5: WI = <*s1*> . j and A6: QI = (GEN (<*s1*>,q)) . j and A7: QI1 = (GEN (<*s1*>,q)) . (j + 1) and A8: WI -succ_of QI = QI1 by A4, FSM_1:def_2; WI = s1 by A4, A5, FINSEQ_1:def_8; then A9: QI1 = s1 -succ_of q by A4, A6, A8, FSM_1:def_2; A10: len <*s2*> = 0 + 1 by FINSEQ_1:39; reconsider h = len <*s2*> as non empty Element of NAT ; consider WI2 being Element of I, QI2, QI12 being State of S such that A11: WI2 = <*s2*> . h and A12: QI2 = (GEN (<*s2*>,q)) . h and A13: QI12 = (GEN (<*s2*>,q)) . (h + 1) and A14: WI2 -succ_of QI2 = QI12 by A10, FSM_1:def_2; A15: QI2 = q by A10, A12, FSM_1:def_2; WI2 = s2 by A10, A11, FINSEQ_1:def_8; hence the Tran of S . [q,s1] = the Tran of S . [q,s2] by A1, A2, A3, A4, A7, A9, A10, A13, A14, A15, Th14; ::_thesis: verum end; theorem :: FSM_2:16 for I being non empty set for S being non empty FSM over I st S is regular & S is calculating_type holds for s, s1, s2 being Element of I for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds the Tran of S . [q,s] <> the InitS of S proof let I be non empty set ; ::_thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds for s, s1, s2 being Element of I for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds the Tran of S . [q,s] <> the InitS of S let S be non empty FSM over I; ::_thesis: ( S is regular & S is calculating_type implies for s, s1, s2 being Element of I for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds the Tran of S . [q,s] <> the InitS of S ) assume that A1: S is regular and A2: S is calculating_type ; ::_thesis: for s, s1, s2 being Element of I for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds the Tran of S . [q,s] <> the InitS of S let s, s1, s2 be Element of I; ::_thesis: for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds the Tran of S . [q,s] <> the InitS of S let q be State of S; ::_thesis: ( the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] implies the Tran of S . [q,s] <> the InitS of S ) assume A3: the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] ; ::_thesis: the Tran of S . [q,s] <> the InitS of S q is accessible by A1, Def4; then consider w being FinSequence of I such that A4: the InitS of S,w -leads_to q by Def3; A5: (GEN (w, the InitS of S)) . ((len w) + 1) = q by A4, FSM_1:def_3; assume A6: the Tran of S . [q,s] = the InitS of S ; ::_thesis: contradiction reconsider w1 = <*s,s1*>, w2 = <*s,s2*> as FinSequence of I ; A7: GEN (w1,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s1])*> by A6, Th2; A8: GEN (w2,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s2])*> by A6, Th2; A9: (GEN (w1,q)) . 3 = the Tran of S . [ the InitS of S,s1] by A7, FINSEQ_1:45; A10: (GEN (w2,q)) . 3 = the Tran of S . [ the InitS of S,s2] by A8, FINSEQ_1:45; A11: len w1 = 2 by FINSEQ_1:44; A12: len w2 = 2 by FINSEQ_1:44; A13: 3 <= (len w1) + 1 by A11; A14: 3 <= (len w2) + 1 by A12; A15: (GEN ((w ^ w1), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s1] by A4, A9, A13, FSM_1:7; A16: (GEN ((w ^ w2), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s2] by A4, A10, A14, FSM_1:7; percases ( w = {} or w <> {} ) ; suppose w = {} ; ::_thesis: contradiction then A17: len w = 0 ; A18: GEN (w1, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1])*> by Th2; A19: GEN (w2, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2])*> by Th2; A20: w1 . 1 = s by FINSEQ_1:44; A21: w2 . 1 = s by FINSEQ_1:44; A22: 3 <= (len w1) + 1 by A11; A23: 3 <= (len w2) + 1 by A12; A24: (GEN (w1, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1] by A18, FINSEQ_1:45 .= the Tran of S . [ the InitS of S,s1] by A5, A6, A17, FSM_1:def_2 ; (GEN (w2, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2] by A19, FINSEQ_1:45 .= the Tran of S . [ the InitS of S,s2] by A5, A6, A17, FSM_1:def_2 ; hence contradiction by A2, A3, A20, A21, A22, A23, A24, Def1; ::_thesis: verum end; suppose w <> {} ; ::_thesis: contradiction then consider s9 being set , w9 being FinSequence such that A25: w = <*s9*> ^ w9 and len w = (len w9) + 1 by REWRITE1:5; dom <*s9*> = Seg 1 by FINSEQ_1:def_8; then A26: 1 in dom <*s9*> by FINSEQ_1:1; then A27: w . 1 = <*s9*> . 1 by A25, FINSEQ_1:def_7 .= s9 by FINSEQ_1:def_8 ; A28: dom <*s9*> c= dom w by A25, FINSEQ_1:26; then A29: (w ^ w1) . 1 = s9 by A26, A27, FINSEQ_1:def_7; A30: (w ^ w2) . 1 = s9 by A26, A27, A28, FINSEQ_1:def_7; A31: (len (w ^ w1)) + 1 = ((len w) + 2) + 1 by A11, FINSEQ_1:22; (len (w ^ w2)) + 1 = ((len w) + 2) + 1 by A12, FINSEQ_1:22; hence contradiction by A2, A3, A15, A16, A29, A30, A31, Def1; ::_thesis: verum end; end; end; begin definition let I be set ; attrc2 is strict ; struct SM_Final over I -> FSM over I; aggrSM_Final(# carrier, Tran, InitS, FinalS #) -> SM_Final over I; sel FinalS c2 -> Subset of the carrier of c2; end; registration let I be set ; cluster non empty for SM_Final over I; existence not for b1 being SM_Final over I holds b1 is empty proof set A = the non empty set ; set T = the Function of [: the non empty set ,I:], the non empty set ; set I = the Element of the non empty set ; set F = the Subset of the non empty set ; take S = SM_Final(# the non empty set , the Function of [: the non empty set ,I:], the non empty set , the Element of the non empty set , the Subset of the non empty set #); ::_thesis: not S is empty thus not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; definition let I be non empty set ; let s be Element of I; let S be non empty SM_Final over I; preds leads_to_final_state_of S means :Def5: :: FSM_2:def 5 ex q being State of S st ( q is_accessible_via s & q in the FinalS of S ); end; :: deftheorem Def5 defines leads_to_final_state_of FSM_2:def_5_:_ for I being non empty set for s being Element of I for S being non empty SM_Final over I holds ( s leads_to_final_state_of S iff ex q being State of S st ( q is_accessible_via s & q in the FinalS of S ) ); definition let I be non empty set ; let S be non empty SM_Final over I; attrS is halting means :Def6: :: FSM_2:def 6 for s being Element of I holds s leads_to_final_state_of S; end; :: deftheorem Def6 defines halting FSM_2:def_6_:_ for I being non empty set for S being non empty SM_Final over I holds ( S is halting iff for s being Element of I holds s leads_to_final_state_of S ); definition let I be set ; let O be non empty set ; attrc3 is strict ; struct Moore-SM_Final over I,O -> SM_Final over I, Moore-FSM over I,O; aggrMoore-SM_Final(# carrier, Tran, OFun, InitS, FinalS #) -> Moore-SM_Final over I,O; end; registration let I be set ; let O be non empty set ; cluster non empty strict for Moore-SM_Final over I,O; existence ex b1 being Moore-SM_Final over I,O st ( not b1 is empty & b1 is strict ) proof set A = the non empty set ; set T = the Function of [: the non empty set ,I:], the non empty set ; set o = the Function of the non empty set ,O; set I = the Element of the non empty set ; set F = the Subset of the non empty set ; take S = Moore-SM_Final(# the non empty set , the Function of [: the non empty set ,I:], the non empty set , the Function of the non empty set ,O, the Element of the non empty set , the Subset of the non empty set #); ::_thesis: ( not S is empty & S is strict ) thus not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is strict thus S is strict ; ::_thesis: verum end; end; definition let I, O be non empty set ; let i, f be set ; let o be Function of {i,f},O; funcI -TwoStatesMooreSM (i,f,o) -> non empty strict Moore-SM_Final over I,O means :Def7: :: FSM_2:def 7 ( the carrier of it = {i,f} & the Tran of it = [:{i,f},I:] --> f & the OFun of it = o & the InitS of it = i & the FinalS of it = {f} ); uniqueness for b1, b2 being non empty strict Moore-SM_Final over I,O st the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} & the carrier of b2 = {i,f} & the Tran of b2 = [:{i,f},I:] --> f & the OFun of b2 = o & the InitS of b2 = i & the FinalS of b2 = {f} holds b1 = b2 ; existence ex b1 being non empty strict Moore-SM_Final over I,O st ( the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} ) proof set X = {i,f}; reconsider ii = i, ff = f as Element of {i,f} by TARSKI:def_2; reconsider oo = o as Function of {i,f},O ; not Moore-SM_Final(# {i,f},([:{i,f},I:] --> ff),oo,ii,{ff} #) is empty ; hence ex b1 being non empty strict Moore-SM_Final over I,O st ( the carrier of b1 = {i,f} & the Tran of b1 = [:{i,f},I:] --> f & the OFun of b1 = o & the InitS of b1 = i & the FinalS of b1 = {f} ) ; ::_thesis: verum end; end; :: deftheorem Def7 defines -TwoStatesMooreSM FSM_2:def_7_:_ for I, O being non empty set for i, f being set for o being Function of {i,f},O for b6 being non empty strict Moore-SM_Final over I,O holds ( b6 = I -TwoStatesMooreSM (i,f,o) iff ( the carrier of b6 = {i,f} & the Tran of b6 = [:{i,f},I:] --> f & the OFun of b6 = o & the InitS of b6 = i & the FinalS of b6 = {f} ) ); theorem Th17: :: FSM_2:17 for O, I being non empty set for w being FinSequence of I for i, f being set for o being Function of {i,f},O for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f proof let O, I be non empty set ; ::_thesis: for w being FinSequence of I for i, f being set for o being Function of {i,f},O for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f let w be FinSequence of I; ::_thesis: for i, f being set for o being Function of {i,f},O for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f let i, f be set ; ::_thesis: for o being Function of {i,f},O for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f let o be Function of {i,f},O; ::_thesis: for j being non empty Element of NAT st 1 < j & j <= (len w) + 1 holds (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f let j be non empty Element of NAT ; ::_thesis: ( 1 < j & j <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f ) assume A1: 1 < j ; ::_thesis: ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f ) set M = I -TwoStatesMooreSM (i,f,o); A2: the carrier of (I -TwoStatesMooreSM (i,f,o)) = {i,f} by Def7; A3: the Tran of (I -TwoStatesMooreSM (i,f,o)) = [:{i,f},I:] --> f by Def7; defpred S1[ Nat] means ( $1 <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . $1 = f ); A4: S1[2] proof assume 2 <= (len w) + 1 ; ::_thesis: (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 2 = f then 1 + 1 <= (len w) + 1 ; then 1 < (len w) + 1 by NAT_1:13; then 1 <= len w by NAT_1:13; then ex WI being Element of I ex QI, QI1 being State of (I -TwoStatesMooreSM (i,f,o)) st ( WI = w . 1 & QI = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 1 & QI1 = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (1 + 1) & WI -succ_of QI = QI1 ) by FSM_1:def_2; hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . 2 = f by A2, A3, FUNCOP_1:7; ::_thesis: verum end; A5: for k being non trivial Nat st S1[k] holds S1[k + 1] proof let k be non trivial Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that ( k <= (len w) + 1 implies (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . k = f ) and A6: k + 1 <= (len w) + 1 ; ::_thesis: (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f A7: 1 <= k by NAT_2:19; k <= len w by A6, XREAL_1:6; then ex WI being Element of I ex QI, QI1 being State of (I -TwoStatesMooreSM (i,f,o)) st ( WI = w . k & QI = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . k & QI1 = (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) & WI -succ_of QI = QI1 ) by A7, FSM_1:def_2; hence (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . (k + 1) = f by A2, A3, FUNCOP_1:7; ::_thesis: verum end; A8: j is non trivial Nat by A1, NAT_2:def_1; for k being non trivial Nat holds S1[k] from NAT_2:sch_2(A4, A5); hence ( not j <= (len w) + 1 or (GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f ) by A8; ::_thesis: verum end; registration let I, O be non empty set ; let i, f be set ; let o be Function of {i,f},O; clusterI -TwoStatesMooreSM (i,f,o) -> non empty calculating_type strict ; coherence I -TwoStatesMooreSM (i,f,o) is calculating_type proof set M = I -TwoStatesMooreSM (i,f,o); for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) proof let w1, w2 be FinSequence of I; ::_thesis: ( w1 . 1 = w2 . 1 & len w1 = len w2 implies GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) ) assume that w1 . 1 = w2 . 1 and A1: len w1 = len w2 ; ::_thesis: GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) reconsider p = GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))), q = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) as FinSequence ; A2: p . 1 = the InitS of (I -TwoStatesMooreSM (i,f,o)) by FSM_1:def_2 .= q . 1 by FSM_1:def_2 ; A3: len p = (len w1) + 1 by FSM_1:def_2; A4: len q = (len w1) + 1 by A1, FSM_1:def_2; now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_p_holds_ p_._j_=_q_._j let j be Nat; ::_thesis: ( 1 <= j & j <= len p implies p . j = q . j ) assume A5: 1 <= j ; ::_thesis: ( j <= len p implies p . j = q . j ) A6: j in NAT by ORDINAL1:def_12; ( j = 1 or j > 1 ) by A5, XXREAL_0:1; then not ( not p . j = q . j & j <= len p & not ( p . j = f & q . j = f ) ) by A1, A2, A3, A6, Th17; hence ( j <= len p implies p . j = q . j ) ; ::_thesis: verum end; hence GEN (w1, the InitS of (I -TwoStatesMooreSM (i,f,o))) = GEN (w2, the InitS of (I -TwoStatesMooreSM (i,f,o))) by A3, A4, FINSEQ_1:14; ::_thesis: verum end; hence I -TwoStatesMooreSM (i,f,o) is calculating_type by Th7; ::_thesis: verum end; end; registration let I, O be non empty set ; let i, f be set ; let o be Function of {i,f},O; clusterI -TwoStatesMooreSM (i,f,o) -> non empty halting strict ; coherence I -TwoStatesMooreSM (i,f,o) is halting proof let s be Element of I; :: according to FSM_2:def_6 ::_thesis: s leads_to_final_state_of I -TwoStatesMooreSM (i,f,o) {i,f} = the carrier of (I -TwoStatesMooreSM (i,f,o)) by Def7; then reconsider q = f as State of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def_2; take q ; :: according to FSM_2:def_5 ::_thesis: ( q is_accessible_via s & q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) ) thus q is_accessible_via s ::_thesis: q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) proof take w = <*> I; :: according to FSM_2:def_2 ::_thesis: the InitS of (I -TwoStatesMooreSM (i,f,o)),<*s*> ^ w -leads_to q <*s*> ^ w = <*s*> by FINSEQ_1:34; then len (<*s*> ^ w) = 1 by FINSEQ_1:39; hence (GEN ((<*s*> ^ w), the InitS of (I -TwoStatesMooreSM (i,f,o)))) . ((len (<*s*> ^ w)) + 1) = q by Th17; :: according to FSM_1:def_3 ::_thesis: verum end; the FinalS of (I -TwoStatesMooreSM (i,f,o)) = {f} by Def7; hence q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def_1; ::_thesis: verum end; end; theorem Th18: :: FSM_2:18 for O, I being non empty set for s being Element of I for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds ex m being non empty Element of NAT st ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) proof let O, I be non empty set ; ::_thesis: for s being Element of I for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds ex m being non empty Element of NAT st ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds ex m being non empty Element of NAT st ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) let M be non empty Moore-SM_Final over I,O; ::_thesis: ( M is calculating_type & s leads_to_final_state_of M implies ex m being non empty Element of NAT st ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) ) assume A1: M is calculating_type ; ::_thesis: ( not s leads_to_final_state_of M or ex m being non empty Element of NAT st ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) ) given q being State of M such that A2: q is_accessible_via s and A3: q in the FinalS of M ; :: according to FSM_2:def_5 ::_thesis: ex m being non empty Element of NAT st ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) consider w being FinSequence of I such that A4: the InitS of M,<*s*> ^ w -leads_to q by A2, Def2; defpred S1[ Nat] means ( (GEN ((<*s*> ^ w), the InitS of M)) . $1 in the FinalS of M & $1 >= 1 & $1 <= (len (<*s*> ^ w)) + 1 ); A5: (len (<*s*> ^ w)) + 1 >= 1 by NAT_1:11; q = (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) by A4, FSM_1:def_3; then A6: ex m being Nat st S1[m] by A3, A5; consider m being Nat such that A7: S1[m] and A8: for k being Nat st S1[k] holds m <= k from NAT_1:sch_5(A6); reconsider m = m as non empty Element of NAT by A7, ORDINAL1:def_12; take m ; ::_thesis: ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) hereby ::_thesis: for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M let w1 be FinSequence of I; ::_thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies (GEN (w1, the InitS of M)) . m in the FinalS of M ) assume that A9: (len w1) + 1 >= m and A10: w1 . 1 = s ; ::_thesis: (GEN (w1, the InitS of M)) . m in the FinalS of M (<*s*> ^ w) . 1 = s by FINSEQ_1:41; then GEN (w1, the InitS of M), GEN ((<*s*> ^ w), the InitS of M) are_c=-comparable by A1, A10, Th4; then A11: ( GEN (w1, the InitS of M) c= GEN ((<*s*> ^ w), the InitS of M) or GEN ((<*s*> ^ w), the InitS of M) c= GEN (w1, the InitS of M) ) by XBOOLE_0:def_9; A12: dom (GEN ((<*s*> ^ w), the InitS of M)) = Seg (len (GEN ((<*s*> ^ w), the InitS of M))) by FINSEQ_1:def_3 .= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def_2 ; A13: dom (GEN (w1, the InitS of M)) = Seg (len (GEN (w1, the InitS of M))) by FINSEQ_1:def_3 .= Seg ((len w1) + 1) by FSM_1:def_2 ; A14: m in dom (GEN ((<*s*> ^ w), the InitS of M)) by A7, A12, FINSEQ_1:1; m in dom (GEN (w1, the InitS of M)) by A7, A9, A13, FINSEQ_1:1; hence (GEN (w1, the InitS of M)) . m in the FinalS of M by A7, A11, A14, GRFUNC_1:2; ::_thesis: verum end; let w1 be FinSequence of I; ::_thesis: for j being non empty Element of NAT st j <= (len w1) + 1 & w1 . 1 = s & j < m holds not (GEN (w1, the InitS of M)) . j in the FinalS of M let i be non empty Element of NAT ; ::_thesis: ( i <= (len w1) + 1 & w1 . 1 = s & i < m implies not (GEN (w1, the InitS of M)) . i in the FinalS of M ) assume that A15: i <= (len w1) + 1 and A16: w1 . 1 = s and A17: i < m ; ::_thesis: not (GEN (w1, the InitS of M)) . i in the FinalS of M (<*s*> ^ w) . 1 = s by FINSEQ_1:41; then GEN (w1, the InitS of M), GEN ((<*s*> ^ w), the InitS of M) are_c=-comparable by A1, A16, Th4; then A18: ( GEN (w1, the InitS of M) c= GEN ((<*s*> ^ w), the InitS of M) or GEN ((<*s*> ^ w), the InitS of M) c= GEN (w1, the InitS of M) ) by XBOOLE_0:def_9; A19: 1 <= i by NAT_1:14; A20: i <= (len (<*s*> ^ w)) + 1 by A7, A17, XXREAL_0:2; A21: dom (GEN (w1, the InitS of M)) = Seg (len (GEN (w1, the InitS of M))) by FINSEQ_1:def_3 .= Seg ((len w1) + 1) by FSM_1:def_2 ; dom (GEN ((<*s*> ^ w), the InitS of M)) = Seg (len (GEN ((<*s*> ^ w), the InitS of M))) by FINSEQ_1:def_3 .= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def_2 ; then A22: i in dom (GEN ((<*s*> ^ w), the InitS of M)) by A19, A20, FINSEQ_1:1; A23: i in dom (GEN (w1, the InitS of M)) by A15, A19, A21, FINSEQ_1:1; assume (GEN (w1, the InitS of M)) . i in the FinalS of M ; ::_thesis: contradiction then (GEN ((<*s*> ^ w), the InitS of M)) . i in the FinalS of M by A18, A22, A23, GRFUNC_1:2; hence contradiction by A8, A17, A19, A20; ::_thesis: verum end; begin definition let I, O be non empty set ; let M be non empty Moore-SM_Final over I,O; let s be Element of I; let t be set ; predt is_result_of s,M means :Def8: :: FSM_2:def 8 ex m being non empty Element of NAT st for w being FinSequence of I st w . 1 = s holds ( ( m <= (len w) + 1 implies ( t = 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 ) ); end; :: deftheorem Def8 defines is_result_of FSM_2:def_8_:_ for I, O being non empty set for M being non empty Moore-SM_Final over I,O for s being Element of I for t being set holds ( t is_result_of s,M iff ex m being non empty Element of NAT st for w being FinSequence of I st w . 1 = s holds ( ( m <= (len w) + 1 implies ( t = 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 ) ) ); theorem :: FSM_2:19 for I, O being non empty set for s being Element of I for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds the OFun of M . the InitS of M is_result_of s,M proof let I, O be non empty set ; ::_thesis: for s being Element of I for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds the OFun of M . the InitS of M is_result_of s,M let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st the InitS of M in the FinalS of M holds the OFun of M . the InitS of M is_result_of s,M let M be non empty Moore-SM_Final over I,O; ::_thesis: ( the InitS of M in the FinalS of M implies the OFun of M . the InitS of M is_result_of s,M ) assume A1: the InitS of M in the FinalS of M ; ::_thesis: the OFun of M . the InitS of M is_result_of s,M take 1 ; :: according to FSM_2:def_8 ::_thesis: for w being FinSequence of I st w . 1 = s holds ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) let w be FinSequence of I; ::_thesis: ( w . 1 = s implies ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) ) assume w . 1 = s ; ::_thesis: ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) thus ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN (w, the InitS of M)) . 1) & (GEN (w, the InitS of M)) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) by A1, FSM_1:def_2, NAT_1:14; ::_thesis: verum end; theorem Th20: :: FSM_2:20 for I, O being non empty set for s being Element of I for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds ex t being Element of O st t is_result_of s,M proof let I, O be non empty set ; ::_thesis: for s being Element of I for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds ex t being Element of O st t is_result_of s,M let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds ex t being Element of O st t is_result_of s,M let M be non empty Moore-SM_Final over I,O; ::_thesis: ( M is calculating_type & s leads_to_final_state_of M implies ex t being Element of O st t is_result_of s,M ) assume that A1: M is calculating_type and A2: s leads_to_final_state_of M ; ::_thesis: ex t being Element of O st t is_result_of s,M consider q being State of M such that A3: q is_accessible_via s and A4: q in the FinalS of M by A2, Def5; consider w being FinSequence of I such that A5: the InitS of M,<*s*> ^ w -leads_to q by A3, Def2; A6: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A5, FSM_1:def_3; consider m being non empty Element of NAT such that A7: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of M)) . m in the FinalS of M and A8: for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of M)) . j in the FinalS of M by A1, A2, Th18; A9: (<*s*> ^ w) . 1 = s by FINSEQ_1:41; then A10: (len (<*s*> ^ w)) + 1 >= m by A4, A6, A8; then (GEN ((<*s*> ^ w), the InitS of M)) . m in the FinalS of M by A7, A9; then reconsider t = the OFun of M . ((GEN ((<*s*> ^ w), the InitS of M)) . m) as Element of O by FUNCT_2:5; take t ; ::_thesis: t is_result_of s,M take m ; :: according to FSM_2:def_8 ::_thesis: for w being FinSequence of I st w . 1 = s holds ( ( m <= (len w) + 1 implies ( t = 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 ) ) let w1 be FinSequence of I; ::_thesis: ( w1 . 1 = s implies ( ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) ) assume A11: w1 . 1 = s ; ::_thesis: ( ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) (<*s*> ^ w) . 1 = s by FINSEQ_1:41; hence ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) by A1, A7, A10, A11, Def1; ::_thesis: for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds not (GEN (w1, the InitS of M)) . n in the FinalS of M thus for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds not (GEN (w1, the InitS of M)) . n in the FinalS of M by A8, A11; ::_thesis: verum end; theorem Th21: :: FSM_2:21 for I, O being non empty set for s being Element of I for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds t1 = t2 proof let I, O be non empty set ; ::_thesis: for s being Element of I for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds t1 = t2 let s be Element of I; ::_thesis: for M being non empty Moore-SM_Final over I,O st s leads_to_final_state_of M holds for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds t1 = t2 let M be non empty Moore-SM_Final over I,O; ::_thesis: ( s leads_to_final_state_of M implies for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds t1 = t2 ) assume A1: s leads_to_final_state_of M ; ::_thesis: for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds t1 = t2 let t1, t2 be Element of O; ::_thesis: ( t1 is_result_of s,M & t2 is_result_of s,M implies t1 = t2 ) given m being non empty Element of NAT such that A2: for w1 being FinSequence of I st w1 . 1 = s holds ( ( m <= (len w1) + 1 implies ( t1 = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w1) + 1 holds not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) ; :: according to FSM_2:def_8 ::_thesis: ( not t2 is_result_of s,M or t1 = t2 ) given o being non empty Element of NAT such that A3: for w2 being FinSequence of I st w2 . 1 = s holds ( ( o <= (len w2) + 1 implies ( t2 = the OFun of M . ((GEN (w2, the InitS of M)) . o) & (GEN (w2, the InitS of M)) . o in the FinalS of M ) ) & ( for p being non empty Element of NAT st p < o & p <= (len w2) + 1 holds not (GEN (w2, the InitS of M)) . p in the FinalS of M ) ) ; :: according to FSM_2:def_8 ::_thesis: t1 = t2 consider q being State of M such that A4: q is_accessible_via s and A5: q in the FinalS of M by A1, Def5; consider w being FinSequence of I such that A6: the InitS of M,<*s*> ^ w -leads_to q by A4, Def2; set w1 = <*s*> ^ w; A7: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A6, FSM_1:def_3; A8: (<*s*> ^ w) . 1 = s by FINSEQ_1:41; then A9: (len (<*s*> ^ w)) + 1 >= m by A2, A5, A7; A10: o <= (len (<*s*> ^ w)) + 1 by A3, A5, A7, A8; A11: ( o < m or o = m or o > m ) by XXREAL_0:1; A12: (<*s*> ^ w) . 1 = s by FINSEQ_1:41; then A13: t1 = the OFun of M . ((GEN ((<*s*> ^ w), the InitS of M)) . m) by A2, A9; A14: (GEN ((<*s*> ^ w), the InitS of M)) . m in the FinalS of M by A2, A9, A12; (GEN ((<*s*> ^ w), the InitS of M)) . o in the FinalS of M by A3, A10, A12; hence t1 = t2 by A2, A3, A9, A10, A11, A12, A13, A14; ::_thesis: verum end; theorem Th22: :: FSM_2:22 for X being 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 ) ) proof 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 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: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 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: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 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 end; theorem Th23: :: FSM_2:23 for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = y ) holds for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M proof consider f being BinOp of REAL such that A1: for x, y being Real holds f . (x,y) = max (x,y) from BINOP_1:sch_4(); let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M ) assume that A2: M is calculating_type and A3: the carrier of M = succ REAL and A4: the FinalS of M = REAL and A5: the InitS of M = REAL and A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st ( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st ( x < y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M ) assume that A7: for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = x and A8: for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M let x, y be Real; ::_thesis: max (x,y) is_result_of [x,y],M now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y) let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) A9: ( x >= y implies the Tran of M . [ the InitS of M,[x,y]] = x ) by A7; ( x < y implies the Tran of M . [ the InitS of M,[x,y]] = y ) by A8; then the Tran of M . [ the InitS of M,[x,y]] = max (x,y) by A9, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum end; then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22; hence max (x,y) is_result_of [x,y],M by A1; ::_thesis: verum end; theorem Th24: :: FSM_2:24 for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = y ) holds for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M proof consider f being BinOp of REAL such that A1: for x, y being Real holds f . (x,y) = min (x,y) from BINOP_1:sch_4(); let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M ) assume that A2: M is calculating_type and A3: the carrier of M = succ REAL and A4: the FinalS of M = REAL and A5: the InitS of M = REAL and A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st ( x < y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st ( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M ) assume that A7: for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = x and A8: for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds min (x,y) is_result_of [x,y],M let x, y be Real; ::_thesis: min (x,y) is_result_of [x,y],M now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y) let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) A9: ( x < y implies the Tran of M . [ the InitS of M,[x,y]] = x ) by A7; ( x >= y implies the Tran of M . [ the InitS of M,[x,y]] = y ) by A8; then the Tran of M . [ the InitS of M,[x,y]] = min (x,y) by A9, XXREAL_0:def_9; hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum end; then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22; hence min (x,y) is_result_of [x,y],M by A1; ::_thesis: verum end; theorem Th25: :: FSM_2:25 for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) holds for x, y being Element of REAL holds x + y is_result_of [x,y],M proof deffunc H1( Real, Real) -> Element of REAL = $1 + $2; consider f being BinOp of REAL such that A1: for x, y being Real holds f . (x,y) = H1(x,y) from BINOP_1:sch_4(); let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) implies for x, y being Element of REAL holds x + y is_result_of [x,y],M ) assume that A2: M is calculating_type and A3: the carrier of M = succ REAL and A4: the FinalS of M = REAL and A5: the InitS of M = REAL and A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st not the Tran of M . [ the InitS of M,[x,y]] = x + y or for x, y being Element of REAL holds x + y is_result_of [x,y],M ) assume A7: for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ; ::_thesis: for x, y being Element of REAL holds x + y is_result_of [x,y],M let x, y be Real; ::_thesis: x + y is_result_of [x,y],M now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y) let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) the Tran of M . [ the InitS of M,[x,y]] = x + y by A7; hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum end; then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22; hence x + y is_result_of [x,y],M by A1; ::_thesis: verum end; theorem Th26: :: FSM_2:26 for M being non empty Moore-SM_Final over [:REAL,REAL:], succ REAL st M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M proof deffunc H1( Real, Real) -> Element of REAL = max ((sgn $1),(sgn $2)); consider f being BinOp of REAL such that A1: for x, y being Real holds f . (x,y) = H1(x,y) from BINOP_1:sch_4(); let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M ) assume that A2: M is calculating_type and A3: the carrier of M = succ REAL and A4: the FinalS of M = REAL and A5: the InitS of M = REAL and A6: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st ( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st ( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st ( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M ) assume that A7: for x, y being Real st ( x > 0 or y > 0 ) holds the Tran of M . [ the InitS of M,[x,y]] = 1 and A8: for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds the Tran of M . [ the InitS of M,[x,y]] = 0 and A9: for x, y being Real st x < 0 & y < 0 holds the Tran of M . [ the InitS of M,[x,y]] = - 1 ; ::_thesis: for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M let x, y be Real; ::_thesis: max ((sgn x),(sgn y)) is_result_of [x,y],M now__::_thesis:_for_x,_y_being_Real_holds_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_f_._(x,y) let x, y be Real; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) proof now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y)) percases ( x > 0 or x = 0 or x < 0 ) ; supposeA10: x > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then A11: sgn x = 1 by ABSVALUE:def_2; now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y)) percases ( y > 0 or y = 0 or y < 0 ) ; suppose y > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = 1 by ABSVALUE:def_2; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10, A11; ::_thesis: verum end; suppose y = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = 0 by ABSVALUE:def_2; then max ((sgn x),(sgn y)) = 1 by A11, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10; ::_thesis: verum end; suppose y < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = - 1 by ABSVALUE:def_2; then max ((sgn x),(sgn y)) = 1 by A11, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A10; ::_thesis: verum end; end; end; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum end; supposeA12: x = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then A13: sgn x = 0 by ABSVALUE:def_2; now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y)) percases ( y > 0 or y = 0 or y < 0 ) ; supposeA14: y > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = 1 by ABSVALUE:def_2; then max ((sgn x),(sgn y)) = 1 by A13, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A14; ::_thesis: verum end; supposeA15: y = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = 0 by ABSVALUE:def_2; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A12, A15; ::_thesis: verum end; supposeA16: y < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = - 1 by ABSVALUE:def_2; then max ((sgn x),(sgn y)) = 0 by A13, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A12, A16; ::_thesis: verum end; end; end; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum end; supposeA17: x < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then A18: sgn x = - 1 by ABSVALUE:def_2; now__::_thesis:_the_Tran_of_M_._[_the_InitS_of_M,[x,y]]_=_max_((sgn_x),(sgn_y)) percases ( y > 0 or y = 0 or y < 0 ) ; supposeA19: y > 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = 1 by ABSVALUE:def_2; then max ((sgn x),(sgn y)) = 1 by A18, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A7, A19; ::_thesis: verum end; supposeA20: y = 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = 0 by ABSVALUE:def_2; then max ((sgn x),(sgn y)) = 0 by A18, XXREAL_0:def_10; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A8, A17, A20; ::_thesis: verum end; supposeA21: y < 0 ; ::_thesis: the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) then sgn y = - 1 by ABSVALUE:def_2; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) by A9, A17, A18, A21; ::_thesis: verum end; end; end; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum end; end; end; hence the Tran of M . [ the InitS of M,[x,y]] = max ((sgn x),(sgn y)) ; ::_thesis: verum end; hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; ::_thesis: verum end; then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22; hence max ((sgn x),(sgn y)) is_result_of [x,y],M by A1; ::_thesis: verum end; registration let I, O be non empty set ; cluster non empty calculating_type halting for Moore-SM_Final over I,O; existence ex b1 being non empty Moore-SM_Final over I,O st ( b1 is calculating_type & b1 is halting ) proof set f = the Function of {0,1},O; take I -TwoStatesMooreSM (0,1, the Function of {0,1},O) ; ::_thesis: ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting ) thus ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting ) ; ::_thesis: verum end; end; registration let I be non empty set ; cluster non empty calculating_type halting for SM_Final over I; existence ex b1 being non empty SM_Final over I st ( b1 is calculating_type & b1 is halting ) proof set O = the non empty set ; set M = the non empty calculating_type halting Moore-SM_Final over I, the non empty set ; take the non empty calculating_type halting Moore-SM_Final over I, the non empty set ; ::_thesis: ( the non empty calculating_type halting Moore-SM_Final over I, the non empty set is calculating_type & the non empty calculating_type halting Moore-SM_Final over I, the non empty set is halting ) thus ( the non empty calculating_type halting Moore-SM_Final over I, the non empty set is calculating_type & the non empty calculating_type halting Moore-SM_Final over I, the non empty set is halting ) ; ::_thesis: verum end; end; definition let I, O be non empty set ; let M be non empty calculating_type halting Moore-SM_Final over I,O; let s be Element of I; A1: s leads_to_final_state_of M by Def6; func Result (s,M) -> Element of O means :Def9: :: FSM_2:def 9 it is_result_of s,M; uniqueness for b1, b2 being Element of O st b1 is_result_of s,M & b2 is_result_of s,M holds b1 = b2 by A1, Th21; existence ex b1 being Element of O st b1 is_result_of s,M by A1, Th20; end; :: deftheorem Def9 defines Result FSM_2:def_9_:_ for I, O being non empty set for M being non empty calculating_type halting Moore-SM_Final over I,O for s being Element of I for b5 being Element of O holds ( b5 = Result (s,M) iff b5 is_result_of s,M ); theorem :: FSM_2:27 for O, I being non empty set for s being Element of I for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 proof let O, I be non empty set ; ::_thesis: for s being Element of I for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 let s be Element of I; ::_thesis: for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 let f be Function of {0,1},O; ::_thesis: Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 set M = I -TwoStatesMooreSM (0,1,f); reconsider 01 = 1 as Element of {0,1} by TARSKI:def_2; A1: s leads_to_final_state_of I -TwoStatesMooreSM (0,1,f) by Def6; A2: the FinalS of (I -TwoStatesMooreSM (0,1,f)) = {1} by Def7; A3: the OFun of (I -TwoStatesMooreSM (0,1,f)) = f by Def7; consider m being non empty Element of NAT such that A4: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) and A5: for w being FinSequence of I for j being non empty Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . j in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A1, Th18; now__::_thesis:_ex_m_being_non_empty_Element_of_NAT_st_ for_w_being_FinSequence_of_I_st_w_._1_=_s_holds_ (_(_m_<=_(len_w)_+_1_implies_(_f_._1_=_the_OFun_of_(I_-TwoStatesMooreSM_(0,1,f))_._((GEN_(w,_the_InitS_of_(I_-TwoStatesMooreSM_(0,1,f))))_._m)_&_(GEN_(w,_the_InitS_of_(I_-TwoStatesMooreSM_(0,1,f))))_._m_in_the_FinalS_of_(I_-TwoStatesMooreSM_(0,1,f))_)_)_&_(_for_n_being_non_empty_Element_of_NAT_st_n_<_m_&_n_<=_(len_w)_+_1_holds_ not_(GEN_(w,_the_InitS_of_(I_-TwoStatesMooreSM_(0,1,f))))_._n_in_the_FinalS_of_(I_-TwoStatesMooreSM_(0,1,f))_)_) take m = m; ::_thesis: for w being FinSequence of I st w . 1 = s holds ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) let w be FinSequence of I; ::_thesis: ( w . 1 = s implies ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) ) assume A6: w . 1 = s ; ::_thesis: ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) hereby ::_thesis: for n being non empty Element of NAT st n < m & n <= (len w) + 1 holds not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) assume m <= (len w) + 1 ; ::_thesis: ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) then (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A4, A6; hence ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) by A2, A3, TARSKI:def_1; ::_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 (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A5, A6; ::_thesis: verum end; then f . 01 is_result_of s,I -TwoStatesMooreSM (0,1,f) by Def8; hence Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 by Def9; ::_thesis: verum end; theorem :: FSM_2:28 for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = y ) holds for x, y being Element of REAL holds Result ([x,y],M) = max (x,y) proof let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds Result ([x,y],M) = max (x,y) ) assume that A1: the carrier of M = succ REAL and A2: the FinalS of M = REAL and A3: the InitS of M = REAL and A4: the OFun of M = id the carrier of M and A5: for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = x and A6: for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = max (x,y) let x, y be Real; ::_thesis: Result ([x,y],M) = max (x,y) A7: max (x,y) in succ REAL by XBOOLE_0:def_3; max (x,y) is_result_of [x,y],M by A1, A2, A3, A4, A5, A6, Th23; hence Result ([x,y],M) = max (x,y) by A7, Def9; ::_thesis: verum end; theorem :: FSM_2:29 for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = y ) holds for x, y being Element of REAL holds Result ([x,y],M) = min (x,y) proof let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds Result ([x,y],M) = min (x,y) ) assume that A1: the carrier of M = succ REAL and A2: the FinalS of M = REAL and A3: the InitS of M = REAL and A4: the OFun of M = id the carrier of M and A5: for x, y being Real st x < y holds the Tran of M . [ the InitS of M,[x,y]] = x and A6: for x, y being Real st x >= y holds the Tran of M . [ the InitS of M,[x,y]] = y ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = min (x,y) let x, y be Real; ::_thesis: Result ([x,y],M) = min (x,y) A7: min (x,y) in succ REAL by XBOOLE_0:def_3; min (x,y) is_result_of [x,y],M by A1, A2, A3, A4, A5, A6, Th24; hence Result ([x,y],M) = min (x,y) by A7, Def9; ::_thesis: verum end; theorem :: FSM_2:30 for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) holds for x, y being Element of REAL holds Result ([x,y],M) = x + y proof let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) implies for x, y being Element of REAL holds Result ([x,y],M) = x + y ) assume that A1: the carrier of M = succ REAL and A2: the FinalS of M = REAL and A3: the InitS of M = REAL and A4: the OFun of M = id the carrier of M and A5: for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = x + y let x, y be Real; ::_thesis: Result ([x,y],M) = x + y A6: x + y in succ REAL by XBOOLE_0:def_3; x + y is_result_of [x,y],M by A1, A2, A3, A4, A5, Th25; hence Result ([x,y],M) = x + y by A6, Def9; ::_thesis: verum end; theorem :: FSM_2:31 for M being non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL st the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds the Tran of M . [ the InitS of M,[x,y]] = - 1 ) holds for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y)) proof let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; ::_thesis: ( the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y)) ) assume that A1: the carrier of M = succ REAL and A2: the FinalS of M = REAL and A3: the InitS of M = REAL and A4: the OFun of M = id the carrier of M ; ::_thesis: ( ex x, y being Real st ( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st ( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st ( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y)) ) assume that A5: for x, y being Real st ( x > 0 or y > 0 ) holds the Tran of M . [ the InitS of M,[x,y]] = 1 and A6: for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds the Tran of M . [ the InitS of M,[x,y]] = 0 and A7: for x, y being Real st x < 0 & y < 0 holds the Tran of M . [ the InitS of M,[x,y]] = - 1 ; ::_thesis: for x, y being Element of REAL holds Result ([x,y],M) = max ((sgn x),(sgn y)) let x, y be Real; ::_thesis: Result ([x,y],M) = max ((sgn x),(sgn y)) A8: max ((sgn x),(sgn y)) in succ REAL by XBOOLE_0:def_3; max ((sgn x),(sgn y)) is_result_of [x,y],M by A1, A2, A3, A4, A5, A6, A7, Th26; hence Result ([x,y],M) = max ((sgn x),(sgn y)) by A8, Def9; ::_thesis: verum end;