:: FSM_3 semantic presentation begin theorem Th1: :: FSM_3:1 for i, k, l being Nat st i >= k + l holds i >= k proof let i, k, l be Nat; ::_thesis: ( i >= k + l implies i >= k ) assume i >= k + l ; ::_thesis: i >= k then i + l >= (k + l) + 0 by XREAL_1:7; hence i >= k by XREAL_1:6; ::_thesis: verum end; theorem :: FSM_3:2 for a, b being FinSequence st ( a ^ b = a or b ^ a = a ) holds b = {} proof let a, b be FinSequence; ::_thesis: ( ( a ^ b = a or b ^ a = a ) implies b = {} ) assume A1: ( a ^ b = a or b ^ a = a ) ; ::_thesis: b = {} percases ( a ^ b = a or b ^ a = a ) by A1; supposeA2: a ^ b = a ; ::_thesis: b = {} len (a ^ b) = (len a) + (len b) by FINSEQ_1:22; hence b = {} by A2; ::_thesis: verum end; supposeA3: b ^ a = a ; ::_thesis: b = {} len (b ^ a) = (len b) + (len a) by FINSEQ_1:22; hence b = {} by A3; ::_thesis: verum end; end; end; theorem Th3: :: FSM_3:3 for k being Nat for p, q being FinSequence st k in dom p & (len p) + 1 = len q holds k + 1 in dom q proof let k be Nat; ::_thesis: for p, q being FinSequence st k in dom p & (len p) + 1 = len q holds k + 1 in dom q let p, q be FinSequence; ::_thesis: ( k in dom p & (len p) + 1 = len q implies k + 1 in dom q ) assume that A1: k in dom p and A2: (len p) + 1 = len q ; ::_thesis: k + 1 in dom q k <= len p by A1, FINSEQ_3:25; then ( 1 + 0 <= k + 1 & k + 1 <= (len p) + 1 ) by XREAL_1:7; hence k + 1 in dom q by A2, FINSEQ_3:25; ::_thesis: verum end; theorem Th4: :: FSM_3:4 for E being non empty set for u being Element of E ^omega st len u = 1 holds ex e being Element of E st ( <%e%> = u & e = u . 0 ) proof let E be non empty set ; ::_thesis: for u being Element of E ^omega st len u = 1 holds ex e being Element of E st ( <%e%> = u & e = u . 0 ) let u be Element of E ^omega ; ::_thesis: ( len u = 1 implies ex e being Element of E st ( <%e%> = u & e = u . 0 ) ) assume len u = 1 ; ::_thesis: ex e being Element of E st ( <%e%> = u & e = u . 0 ) then len u = 0 + 1 ; then consider v being Element of E ^omega , e being Element of E such that A1: len v = 0 and A2: u = v ^ <%e%> by FLANG_1:7; take e ; ::_thesis: ( <%e%> = u & e = u . 0 ) v = <%> E by A1; then u = {} ^ <%e%> by A2; then u = <%e%> ; hence ( <%e%> = u & e = u . 0 ) by AFINSQ_1:34; ::_thesis: verum end; theorem Th5: :: FSM_3:5 for E being non empty set for u being Element of E ^omega for k being Nat st k <> 0 & len u <= k + 1 holds ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) proof let E be non empty set ; ::_thesis: for u being Element of E ^omega for k being Nat st k <> 0 & len u <= k + 1 holds ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) let u be Element of E ^omega ; ::_thesis: for k being Nat st k <> 0 & len u <= k + 1 holds ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) let k be Nat; ::_thesis: ( k <> 0 & len u <= k + 1 implies ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) ) assume that A1: k <> 0 and A2: len u <= k + 1 ; ::_thesis: ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) percases ( len u = k + 1 or len u <> k + 1 ) ; suppose len u = k + 1 ; ::_thesis: ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) then consider v1 being Element of E ^omega , e being Element of E such that A3: len v1 = k and A4: u = v1 ^ <%e%> by FLANG_1:7; reconsider v2 = <%e%> as Element of E ^omega ; take v1 ; ::_thesis: ex v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) take v2 ; ::_thesis: ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) thus len v1 <= k by A3; ::_thesis: ( len v2 <= k & u = v1 ^ v2 ) 0 + 1 <= k by A1, NAT_1:13; hence len v2 <= k by AFINSQ_1:34; ::_thesis: u = v1 ^ v2 thus u = v1 ^ v2 by A4; ::_thesis: verum end; supposeA5: len u <> k + 1 ; ::_thesis: ex v1, v2 being Element of E ^omega st ( len v1 <= k & len v2 <= k & u = v1 ^ v2 ) reconsider v2 = <%> E as Element of E ^omega ; take u ; ::_thesis: ex v2 being Element of E ^omega st ( len u <= k & len v2 <= k & u = u ^ v2 ) take v2 ; ::_thesis: ( len u <= k & len v2 <= k & u = u ^ v2 ) thus len u <= k by A2, A5, NAT_1:8; ::_thesis: ( len v2 <= k & u = u ^ v2 ) thus len v2 <= k ; ::_thesis: u = u ^ v2 thus u = u ^ {} .= u ^ v2 ; ::_thesis: verum end; end; end; theorem Th6: :: FSM_3:6 for x, y being set for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds ( x = y & p = q ) proof let x, y be set ; ::_thesis: for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds ( x = y & p = q ) let p, q be XFinSequence; ::_thesis: ( <%x%> ^ p = <%y%> ^ q implies ( x = y & p = q ) ) assume A1: <%x%> ^ p = <%y%> ^ q ; ::_thesis: ( x = y & p = q ) (<%x%> ^ p) . 0 = x by AFINSQ_1:35; then x = y by A1, AFINSQ_1:35; hence ( x = y & p = q ) by A1, AFINSQ_1:28; ::_thesis: verum end; theorem Th7: :: FSM_3:7 for E being non empty set for u being Element of E ^omega st len u > 0 holds ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 proof let E be non empty set ; ::_thesis: for u being Element of E ^omega st len u > 0 holds ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 let u be Element of E ^omega ; ::_thesis: ( len u > 0 implies ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 ) assume len u > 0 ; ::_thesis: ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 then consider k being Nat such that A1: len u = k + 1 by NAT_1:6; ex u1 being Element of E ^omega ex e being Element of E st ( len u1 = k & u = <%e%> ^ u1 ) by A1, FLANG_1:9; hence ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 ; ::_thesis: verum end; registration let E be non empty set ; cluster Lex E -> non empty ; coherence not Lex E is empty proof for e being Element of E holds <%e%> in Lex E by FLANG_1:def_4; hence not Lex E is empty ; ::_thesis: verum end; end; theorem Th8: :: FSM_3:8 for E being non empty set holds not <%> E in Lex E proof let E be non empty set ; ::_thesis: not <%> E in Lex E assume <%> E in Lex E ; ::_thesis: contradiction then ex e being Element of E st ( e in E & <%> E = <%e%> ) by FLANG_1:def_4; hence contradiction ; ::_thesis: verum end; theorem Th9: :: FSM_3:9 for E being non empty set for u being Element of E ^omega holds ( u in Lex E iff len u = 1 ) proof let E be non empty set ; ::_thesis: for u being Element of E ^omega holds ( u in Lex E iff len u = 1 ) let u be Element of E ^omega ; ::_thesis: ( u in Lex E iff len u = 1 ) thus ( u in Lex E implies len u = 1 ) ::_thesis: ( len u = 1 implies u in Lex E ) proof assume u in Lex E ; ::_thesis: len u = 1 then ex e being Element of E st ( e in E & u = <%e%> ) by FLANG_1:def_4; hence len u = 1 by AFINSQ_1:def_4; ::_thesis: verum end; assume len u = 1 ; ::_thesis: u in Lex E then ex e being Element of E st ( <%e%> = u & e = u . 0 ) by Th4; hence u in Lex E by FLANG_1:def_4; ::_thesis: verum end; theorem Th10: :: FSM_3:10 for E being non empty set for u, v being Element of E ^omega st u <> v & u in Lex E & v in Lex E holds for w being Element of E ^omega holds ( not u ^ w = v & not w ^ u = v ) proof let E be non empty set ; ::_thesis: for u, v being Element of E ^omega st u <> v & u in Lex E & v in Lex E holds for w being Element of E ^omega holds ( not u ^ w = v & not w ^ u = v ) let u, v be Element of E ^omega ; ::_thesis: ( u <> v & u in Lex E & v in Lex E implies for w being Element of E ^omega holds ( not u ^ w = v & not w ^ u = v ) ) assume that A1: u <> v and A2: u in Lex E and A3: v in Lex E ; ::_thesis: for w being Element of E ^omega holds ( not u ^ w = v & not w ^ u = v ) A4: len u = 1 by A2, Th9; given w being Element of E ^omega such that A5: ( u ^ w = v or w ^ u = v ) ; ::_thesis: contradiction A6: len v = 1 by A3, Th9; F: ( u ^ {} = u & {} ^ u = u ) ; percases ( u ^ w = v or w ^ u = v ) by A5; supposeA7: u ^ w = v ; ::_thesis: contradiction len (u ^ w) = 1 + (len w) by A4, AFINSQ_1:17; then w = <%> E by A6, A7; hence contradiction by A1, A7, F; ::_thesis: verum end; supposeA8: w ^ u = v ; ::_thesis: contradiction len (w ^ u) = 1 + (len w) by A4, AFINSQ_1:17; then w = <%> E by A6, A8; hence contradiction by A1, A8, F; ::_thesis: verum end; end; end; theorem Th11: :: FSM_3:11 for E being non empty set for TS being transition-system over Lex E st the Tran of TS is Function holds TS is deterministic proof let E be non empty set ; ::_thesis: for TS being transition-system over Lex E st the Tran of TS is Function holds TS is deterministic let TS be transition-system over Lex E; ::_thesis: ( the Tran of TS is Function implies TS is deterministic ) assume A1: the Tran of TS is Function ; ::_thesis: TS is deterministic A2: now__::_thesis:_for_p_being_Element_of_TS for_u,_v_being_Element_of_E_^omega_st_u_<>_v_&_[p,u]_in_dom_the_Tran_of_TS_&_[p,v]_in_dom_the_Tran_of_TS_holds_ for_w_being_Element_of_E_^omega_holds_ (_not_u_^_w_=_v_&_not_v_^_w_=_u_) let p be Element of TS; ::_thesis: for u, v being Element of E ^omega st u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) let u, v be Element of E ^omega ; ::_thesis: ( u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS implies for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) ) assume that A3: u <> v and A4: ( [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS ) ; ::_thesis: for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) ( u in Lex E & v in Lex E ) by A4, ZFMISC_1:87; hence for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) by A3, Th10; ::_thesis: verum end; not <%> E in rng (dom the Tran of TS) by Th8; hence TS is deterministic by A1, A2, REWRITE3:def_1; ::_thesis: verum end; definition let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty transition-system over F; func _bool TS -> strict transition-system over Lex E means :Def1: :: FSM_3:def 1 ( the carrier of it = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of it iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ); existence ex b1 being strict transition-system over Lex E st ( the carrier of b1 = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of b1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ) proof set cTS = bool the carrier of TS; defpred S1[ set , set ] means for c being Element of bool the carrier of TS for i being Element of E ^omega st $1 = [c,i] holds ( len i = 1 & $2 = i -succ_of (c,TS) ); consider tTS being Relation of [:(bool the carrier of TS),(Lex E):],(bool the carrier of TS) such that A1: for x being Element of [:(bool the carrier of TS),(Lex E):] for y being Element of bool the carrier of TS holds ( [x,y] in tTS iff S1[x,y] ) from RELSET_1:sch_2(); set bTS = transition-system(# (bool the carrier of TS),tTS #); reconsider bTS = transition-system(# (bool the carrier of TS),tTS #) as strict transition-system over Lex E ; take bTS ; ::_thesis: ( the carrier of bTS = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ) thus the carrier of bTS = bool the carrier of TS ; ::_thesis: for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) let S be Subset of TS; ::_thesis: for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) let w be Element of E ^omega ; ::_thesis: for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) let T be Subset of TS; ::_thesis: ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) thus ( [[S,w],T] in the Tran of bTS implies ( len w = 1 & T = w -succ_of (S,TS) ) ) ::_thesis: ( len w = 1 & T = w -succ_of (S,TS) implies [[S,w],T] in the Tran of bTS ) proof assume A2: [[S,w],T] in the Tran of bTS ; ::_thesis: ( len w = 1 & T = w -succ_of (S,TS) ) then reconsider xc = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87; [xc,T] in tTS by A2; hence ( len w = 1 & T = w -succ_of (S,TS) ) by A1; ::_thesis: verum end; set x = [S,w]; assume that A3: len w = 1 and A4: T = w -succ_of (S,TS) ; ::_thesis: [[S,w],T] in the Tran of bTS A5: now__::_thesis:_for_xc_being_Element_of_bool_the_carrier_of_TS for_xi_being_Element_of_E_^omega_st_[S,w]_=_[xc,xi]_holds_ (_len_xi_=_1_&_T_=_xi_-succ_of_(xc,TS)_) let xc be Element of bool the carrier of TS; ::_thesis: for xi being Element of E ^omega st [S,w] = [xc,xi] holds ( len xi = 1 & T = xi -succ_of (xc,TS) ) let xi be Element of E ^omega ; ::_thesis: ( [S,w] = [xc,xi] implies ( len xi = 1 & T = xi -succ_of (xc,TS) ) ) assume A6: [S,w] = [xc,xi] ; ::_thesis: ( len xi = 1 & T = xi -succ_of (xc,TS) ) xc = S by A6, XTUPLE_0:1; hence ( len xi = 1 & T = xi -succ_of (xc,TS) ) by A3, A4, A6, XTUPLE_0:1; ::_thesis: verum end; w in Lex E by A3, Th9; then reconsider x = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87; [x,T] in tTS by A1, A5; hence [[S,w],T] in the Tran of bTS ; ::_thesis: verum end; uniqueness for b1, b2 being strict transition-system over Lex E st the carrier of b1 = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of b1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) & the carrier of b2 = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of b2 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) holds b1 = b2 proof set cTS = bool the carrier of TS; let bTS1, bTS2 be strict transition-system over Lex E; ::_thesis: ( the carrier of bTS1 = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) & the carrier of bTS2 = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS2 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) implies bTS1 = bTS2 ) assume that A7: the carrier of bTS1 = bool the carrier of TS and A8: for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) and A9: the carrier of bTS2 = bool the carrier of TS and A10: for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of bTS2 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ; ::_thesis: bTS1 = bTS2 A11: for x being set st x in the Tran of bTS2 holds x in the Tran of bTS1 proof let x be set ; ::_thesis: ( x in the Tran of bTS2 implies x in the Tran of bTS1 ) assume A12: x in the Tran of bTS2 ; ::_thesis: x in the Tran of bTS1 then consider xbi, xc being set such that A13: x = [xbi,xc] and A14: xbi in [:(bool the carrier of TS),(Lex E):] and A15: xc in bool the carrier of TS by A9, RELSET_1:2; reconsider xc = xc as Element of bool the carrier of TS by A15; [:(bool the carrier of TS),(Lex E):] c= [:(bool the carrier of TS),(Lex E):] ; then consider xb, xi being set such that A16: xbi = [xb,xi] and A17: xb in bool the carrier of TS and A18: xi in Lex E by A14, RELSET_1:2; reconsider xb = xb as Element of bool the carrier of TS by A17; reconsider xi = xi as Element of Lex E by A18; reconsider xe = xi as Element of E ^omega ; A19: len xe = 1 by Th9; xc = xi -succ_of (xb,TS) by A10, A12, A13, A16; hence x in the Tran of bTS1 by A8, A13, A16, A19; ::_thesis: verum end; for x being set st x in the Tran of bTS1 holds x in the Tran of bTS2 proof let x be set ; ::_thesis: ( x in the Tran of bTS1 implies x in the Tran of bTS2 ) assume A20: x in the Tran of bTS1 ; ::_thesis: x in the Tran of bTS2 then consider xbi, xc being set such that A21: x = [xbi,xc] and A22: xbi in [:(bool the carrier of TS),(Lex E):] and A23: xc in bool the carrier of TS by A7, RELSET_1:2; reconsider xc = xc as Element of bool the carrier of TS by A23; [:(bool the carrier of TS),(Lex E):] c= [:(bool the carrier of TS),(Lex E):] ; then consider xb, xi being set such that A24: xbi = [xb,xi] and A25: xb in bool the carrier of TS and A26: xi in Lex E by A22, RELSET_1:2; reconsider xb = xb as Element of bool the carrier of TS by A25; reconsider xi = xi as Element of Lex E by A26; reconsider xe = xi as Element of E ^omega ; A27: len xe = 1 by Th9; xc = xi -succ_of (xb,TS) by A8, A20, A21, A24; hence x in the Tran of bTS2 by A10, A21, A24, A27; ::_thesis: verum end; hence bTS1 = bTS2 by A7, A9, A11, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines _bool FSM_3:def_1_:_ for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for b4 being strict transition-system over Lex E holds ( b4 = _bool TS iff ( the carrier of b4 = bool the carrier of TS & ( for S being Subset of TS for w being Element of E ^omega for T being Subset of TS holds ( [[S,w],T] in the Tran of b4 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ) ); registration let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty transition-system over F; cluster _bool TS -> non empty strict deterministic ; coherence ( not _bool TS is empty & _bool TS is deterministic ) proof set bTS = _bool TS; set wTS = the carrier of (_bool TS); set tTS = the Tran of (_bool TS); for x, y1, y2 being set st [x,y1] in the Tran of (_bool TS) & [x,y2] in the Tran of (_bool TS) holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( [x,y1] in the Tran of (_bool TS) & [x,y2] in the Tran of (_bool TS) implies y1 = y2 ) assume that A1: [x,y1] in the Tran of (_bool TS) and A2: [x,y2] in the Tran of (_bool TS) ; ::_thesis: y1 = y2 reconsider x = x as Element of [: the carrier of (_bool TS),(Lex E):] by A1, ZFMISC_1:87; reconsider y1 = y1, y2 = y2 as Element of the carrier of (_bool TS) by A1, A2, ZFMISC_1:87; the carrier of (_bool TS) = bool the carrier of TS by Def1; then consider xc, xi being set such that A3: xc in the carrier of (_bool TS) and A4: xi in Lex E and A5: x = [xc,xi] by ZFMISC_1:def_2; reconsider xc = xc as Element of the carrier of (_bool TS) by A3; reconsider xi = xi as Element of Lex E by A4; reconsider xi = xi as Element of E ^omega ; reconsider xc = xc, y1 = y1, y2 = y2 as Subset of TS by Def1; ( y1 = xi -succ_of (xc,TS) & y2 = xi -succ_of (xc,TS) ) by A1, A2, A5, Def1; hence y1 = y2 ; ::_thesis: verum end; then A6: the Tran of (_bool TS) is Function by FUNCT_1:def_1; the carrier of (_bool TS) = bool the carrier of TS by Def1; hence ( not _bool TS is empty & _bool TS is deterministic ) by A6, Th11; ::_thesis: verum end; end; registration let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty finite transition-system over F; cluster _bool TS -> finite strict ; coherence _bool TS is finite proof bool the carrier of TS is finite ; hence _bool TS is finite by Def1; ::_thesis: verum end; end; theorem Th12: :: FSM_3:12 for x, y being set for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds x,<%e%> ==>. y, <%> E, _bool TS proof let x, y be set ; ::_thesis: for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds x,<%e%> ==>. y, <%> E, _bool TS let E be non empty set ; ::_thesis: for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds x,<%e%> ==>. y, <%> E, _bool TS let e be Element of E; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds x,<%e%> ==>. y, <%> E, _bool TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,<%e%> ==>* y, <%> E, _bool TS holds x,<%e%> ==>. y, <%> E, _bool TS let TS be non empty transition-system over F; ::_thesis: ( x,<%e%> ==>* y, <%> E, _bool TS implies x,<%e%> ==>. y, <%> E, _bool TS ) not <%> E in rng (dom the Tran of (_bool TS)) by REWRITE3:def_1; hence ( x,<%e%> ==>* y, <%> E, _bool TS implies x,<%e%> ==>. y, <%> E, _bool TS ) by REWRITE3:92; ::_thesis: verum end; theorem Th13: :: FSM_3:13 for X being set for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for S being Subset of TS st len w = 1 holds ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) proof let X be set ; ::_thesis: for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for S being Subset of TS st len w = 1 holds ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) let E be non empty set ; ::_thesis: for w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for S being Subset of TS st len w = 1 holds ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) let w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for S being Subset of TS st len w = 1 holds ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for S being Subset of TS st len w = 1 holds ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) let TS be non empty transition-system over F; ::_thesis: for S being Subset of TS st len w = 1 holds ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) let S be Subset of TS; ::_thesis: ( len w = 1 implies ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) ) assume A1: len w = 1 ; ::_thesis: ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) thus ( X = w -succ_of (S,TS) implies S,w ==>* X, _bool TS ) ::_thesis: ( S,w ==>* X, _bool TS implies X = w -succ_of (S,TS) ) proof assume X = w -succ_of (S,TS) ; ::_thesis: S,w ==>* X, _bool TS then [[S,w],X] in the Tran of (_bool TS) by A1, Def1; then S,w -->. X, _bool TS by REWRITE3:def_2; then S,w ==>. X, <%> E, _bool TS by REWRITE3:23; then S,w ==>* X, <%> E, _bool TS by REWRITE3:87; hence S,w ==>* X, _bool TS by REWRITE3:def_7; ::_thesis: verum end; assume S,w ==>* X, _bool TS ; ::_thesis: X = w -succ_of (S,TS) then A2: S,w ==>* X, <%> E, _bool TS by REWRITE3:def_7; ex e being Element of E st ( w = <%e%> & w . 0 = e ) by A1, Th4; then S,w ^ {} ==>. X, <%> E, _bool TS by A2, Th12; then A3: S,w -->. X, _bool TS by REWRITE3:24; then X in _bool TS by REWRITE3:15; then X in the carrier of (_bool TS) by STRUCT_0:def_5; then reconsider X9 = X as Subset of TS by Def1; [[S,w],X9] in the Tran of (_bool TS) by A3, REWRITE3:def_2; hence X = w -succ_of (S,TS) by Def1; ::_thesis: verum end; definition let E be non empty set ; let F be Subset of (E ^omega); attrc3 is strict ; struct semiautomaton over F -> transition-system over F; aggrsemiautomaton(# carrier, Tran, InitS #) -> semiautomaton over F; sel InitS c3 -> Subset of the carrier of c3; end; definition let E be non empty set ; let F be Subset of (E ^omega); let SA be semiautomaton over F; attrSA is deterministic means :Def2: :: FSM_3:def 2 ( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 ); end; :: deftheorem Def2 defines deterministic FSM_3:def_2_:_ for E being non empty set for F being Subset of (E ^omega) for SA being semiautomaton over F holds ( SA is deterministic iff ( transition-system(# the carrier of SA, the Tran of SA #) is deterministic & card the InitS of SA = 1 ) ); registration let E be non empty set ; let F be Subset of (E ^omega); cluster non empty finite strict deterministic for semiautomaton over F; existence ex b1 being semiautomaton over F st ( b1 is strict & not b1 is empty & b1 is finite & b1 is deterministic ) proof set X = the non empty finite set ; reconsider T = {} as Relation of [: the non empty finite set ,F:], the non empty finite set by RELSET_1:12; set x = the Element of the non empty finite set ; reconsider I = { the Element of the non empty finite set } as Subset of the non empty finite set ; take SA = semiautomaton(# the non empty finite set ,T,I #); ::_thesis: ( SA is strict & not SA is empty & SA is finite & SA is deterministic ) thus SA is strict ; ::_thesis: ( not SA is empty & SA is finite & SA is deterministic ) thus not SA is empty ; ::_thesis: ( SA is finite & SA is deterministic ) thus the carrier of SA is finite ; :: according to STRUCT_0:def_11 ::_thesis: SA is deterministic thus transition-system(# the carrier of SA, the Tran of SA #) is deterministic by RELAT_1:38, REWRITE3:14; :: according to FSM_3:def_2 ::_thesis: card the InitS of SA = 1 thus card the InitS of SA = 1 by CARD_1:30; ::_thesis: verum end; end; registration let E be non empty set ; let F be Subset of (E ^omega); let SA be non empty semiautomaton over F; cluster transition-system(# the carrier of SA, the Tran of SA #) -> non empty ; coherence not transition-system(# the carrier of SA, the Tran of SA #) is empty ; end; definition let E be non empty set ; let F be Subset of (E ^omega); let SA be non empty semiautomaton over F; func _bool SA -> strict semiautomaton over Lex E means :Def3: :: FSM_3:def 3 ( transition-system(# the carrier of it, the Tran of it #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of it = {((<%> E) -succ_of ( the InitS of SA,SA))} ); existence ex b1 being strict semiautomaton over Lex E st ( transition-system(# the carrier of b1, the Tran of b1 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b1 = {((<%> E) -succ_of ( the InitS of SA,SA))} ) proof reconsider TS = transition-system(# the carrier of SA, the Tran of SA #) as non empty transition-system over F ; set cSA = the carrier of (_bool TS); reconsider iSA = {((<%> E) -succ_of ( the InitS of SA,SA))} as Subset of the carrier of (_bool TS) by Def1; reconsider tSA = the Tran of (_bool TS) as Relation of [: the carrier of (_bool TS),(Lex E):], the carrier of (_bool TS) ; set bSA = semiautomaton(# the carrier of (_bool TS),tSA,iSA #); card iSA = 1 by CARD_1:30; then reconsider bSA = semiautomaton(# the carrier of (_bool TS),tSA,iSA #) as non empty strict deterministic semiautomaton over Lex E by Def2; take bSA ; ::_thesis: ( transition-system(# the carrier of bSA, the Tran of bSA #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of bSA = {((<%> E) -succ_of ( the InitS of SA,SA))} ) thus ( transition-system(# the carrier of bSA, the Tran of bSA #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of bSA = {((<%> E) -succ_of ( the InitS of SA,SA))} ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict semiautomaton over Lex E st transition-system(# the carrier of b1, the Tran of b1 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b1 = {((<%> E) -succ_of ( the InitS of SA,SA))} & transition-system(# the carrier of b2, the Tran of b2 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b2 = {((<%> E) -succ_of ( the InitS of SA,SA))} holds b1 = b2 ; end; :: deftheorem Def3 defines _bool FSM_3:def_3_:_ for E being non empty set for F being Subset of (E ^omega) for SA being non empty semiautomaton over F for b4 being strict semiautomaton over Lex E holds ( b4 = _bool SA iff ( transition-system(# the carrier of b4, the Tran of b4 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b4 = {((<%> E) -succ_of ( the InitS of SA,SA))} ) ); registration let E be non empty set ; let F be Subset of (E ^omega); let SA be non empty semiautomaton over F; cluster _bool SA -> non empty strict deterministic ; coherence ( not _bool SA is empty & _bool SA is deterministic ) proof set TS = _bool SA; the InitS of (_bool SA) = {((<%> E) -succ_of ( the InitS of SA,SA))} by Def3; then A1: card the InitS of (_bool SA) = 1 by CARD_1:30; transition-system(# the carrier of (_bool SA), the Tran of (_bool SA) #) = _bool transition-system(# the carrier of SA, the Tran of SA #) by Def3; hence ( not _bool SA is empty & _bool SA is deterministic ) by A1, Def2; ::_thesis: verum end; end; theorem Th14: :: FSM_3:14 for E being non empty set for F being Subset of (E ^omega) for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA let F be Subset of (E ^omega); ::_thesis: for SA being non empty semiautomaton over F holds the carrier of (_bool SA) = bool the carrier of SA let SA be non empty semiautomaton over F; ::_thesis: the carrier of (_bool SA) = bool the carrier of SA transition-system(# the carrier of (_bool SA), the Tran of (_bool SA) #) = _bool transition-system(# the carrier of SA, the Tran of SA #) by Def3; hence the carrier of (_bool SA) = bool the carrier of SA by Def1; ::_thesis: verum end; registration let E be non empty set ; let F be Subset of (E ^omega); let SA be non empty finite semiautomaton over F; cluster _bool SA -> finite strict ; coherence _bool SA is finite proof bool the carrier of SA is finite ; hence _bool SA is finite by Th14; ::_thesis: verum end; end; definition let E be non empty set ; let F be Subset of (E ^omega); let SA be non empty semiautomaton over F; let Q be Subset of SA; func left-Lang Q -> Subset of (E ^omega) equals :: FSM_3:def 4 { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ; coherence { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } is Subset of (E ^omega) proof defpred S1[ Element of E ^omega ] means Q meets $1 -succ_of ( the InitS of SA,SA); { w where w is Element of E ^omega : S1[w] } c= E ^omega from FRAENKEL:sch_10(); hence { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } is Subset of (E ^omega) ; ::_thesis: verum end; end; :: deftheorem defines left-Lang FSM_3:def_4_:_ for E being non empty set for F being Subset of (E ^omega) for SA being non empty semiautomaton over F for Q being Subset of SA holds left-Lang Q = { w where w is Element of E ^omega : Q meets w -succ_of ( the InitS of SA,SA) } ; theorem Th15: :: FSM_3:15 for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for SA being non empty semiautomaton over F for Q being Subset of SA holds ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) ) proof let E be non empty set ; ::_thesis: for w being Element of E ^omega for F being Subset of (E ^omega) for SA being non empty semiautomaton over F for Q being Subset of SA holds ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) ) let w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for SA being non empty semiautomaton over F for Q being Subset of SA holds ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) ) let F be Subset of (E ^omega); ::_thesis: for SA being non empty semiautomaton over F for Q being Subset of SA holds ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) ) let SA be non empty semiautomaton over F; ::_thesis: for Q being Subset of SA holds ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) ) let Q be Subset of SA; ::_thesis: ( w in left-Lang Q iff Q meets w -succ_of ( the InitS of SA,SA) ) thus ( w in left-Lang Q implies Q meets w -succ_of ( the InitS of SA,SA) ) ::_thesis: ( Q meets w -succ_of ( the InitS of SA,SA) implies w in left-Lang Q ) proof assume w in left-Lang Q ; ::_thesis: Q meets w -succ_of ( the InitS of SA,SA) then ex w9 being Element of E ^omega st ( w9 = w & Q meets w9 -succ_of ( the InitS of SA,SA) ) ; hence Q meets w -succ_of ( the InitS of SA,SA) ; ::_thesis: verum end; thus ( Q meets w -succ_of ( the InitS of SA,SA) implies w in left-Lang Q ) ; ::_thesis: verum end; definition let E be non empty set ; let F be Subset of (E ^omega); attrc3 is strict ; struct automaton over F -> semiautomaton over F; aggrautomaton(# carrier, Tran, InitS, FinalS #) -> automaton over F; sel FinalS c3 -> Subset of the carrier of c3; end; definition let E be non empty set ; let F be Subset of (E ^omega); let A be automaton over F; attrA is deterministic means :Def5: :: FSM_3:def 5 semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic ; end; :: deftheorem Def5 defines deterministic FSM_3:def_5_:_ for E being non empty set for F being Subset of (E ^omega) for A being automaton over F holds ( A is deterministic iff semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic ); registration let E be non empty set ; let F be Subset of (E ^omega); cluster non empty finite strict deterministic for automaton over F; existence ex b1 being automaton over F st ( b1 is strict & not b1 is empty & b1 is finite & b1 is deterministic ) proof set X = the non empty finite set ; reconsider T = {} as Relation of [: the non empty finite set ,F:], the non empty finite set by RELSET_1:12; set x = the Element of the non empty finite set ; reconsider I = { the Element of the non empty finite set } as Subset of the non empty finite set ; take A = automaton(# the non empty finite set ,T,I,I #); ::_thesis: ( A is strict & not A is empty & A is finite & A is deterministic ) thus A is strict ; ::_thesis: ( not A is empty & A is finite & A is deterministic ) thus not A is empty ; ::_thesis: ( A is finite & A is deterministic ) thus the carrier of A is finite ; :: according to STRUCT_0:def_11 ::_thesis: A is deterministic ( transition-system(# the carrier of A, the Tran of A #) is deterministic & card the InitS of A = 1 ) by CARD_1:30, RELAT_1:38, REWRITE3:14; then semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is deterministic by Def2; hence A is deterministic by Def5; ::_thesis: verum end; end; registration let E be non empty set ; let F be Subset of (E ^omega); let A be non empty automaton over F; cluster transition-system(# the carrier of A, the Tran of A #) -> non empty ; coherence not transition-system(# the carrier of A, the Tran of A #) is empty ; cluster semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) -> non empty ; coherence not semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) is empty ; end; definition let E be non empty set ; let F be Subset of (E ^omega); let A be non empty automaton over F; func _bool A -> strict automaton over Lex E means :Def6: :: FSM_3:def 6 ( semiautomaton(# the carrier of it, the Tran of it, the InitS of it #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of it = { Q where Q is Element of it : Q meets the FinalS of A } ); existence ex b1 being strict automaton over Lex E st ( semiautomaton(# the carrier of b1, the Tran of b1, the InitS of b1 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b1 = { Q where Q is Element of b1 : Q meets the FinalS of A } ) proof reconsider SA = semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) as non empty semiautomaton over F ; set cA = the carrier of (_bool SA); reconsider tA = the Tran of (_bool SA) as Relation of [: the carrier of (_bool SA),(Lex E):], the carrier of (_bool SA) ; set iA = the InitS of (_bool SA); { Q where Q is Element of (_bool SA) : Q meets the FinalS of A } is Subset of the carrier of (_bool SA) proof defpred S1[ set ] means $1 meets the FinalS of A; { Q where Q is Element of (_bool SA) : S1[Q] } c= the carrier of (_bool SA) from FRAENKEL:sch_10(); hence { Q where Q is Element of (_bool SA) : Q meets the FinalS of A } is Subset of the carrier of (_bool SA) ; ::_thesis: verum end; then reconsider fA = { Q where Q is Element of (_bool SA) : Q meets the FinalS of A } as Subset of the carrier of (_bool SA) ; set bA = automaton(# the carrier of (_bool SA),tA, the InitS of (_bool SA),fA #); reconsider bA = automaton(# the carrier of (_bool SA),tA, the InitS of (_bool SA),fA #) as non empty strict deterministic automaton over Lex E by Def5; take bA ; ::_thesis: ( semiautomaton(# the carrier of bA, the Tran of bA, the InitS of bA #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of bA = { Q where Q is Element of bA : Q meets the FinalS of A } ) thus ( semiautomaton(# the carrier of bA, the Tran of bA, the InitS of bA #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of bA = { Q where Q is Element of bA : Q meets the FinalS of A } ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict automaton over Lex E st semiautomaton(# the carrier of b1, the Tran of b1, the InitS of b1 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b1 = { Q where Q is Element of b1 : Q meets the FinalS of A } & semiautomaton(# the carrier of b2, the Tran of b2, the InitS of b2 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b2 = { Q where Q is Element of b2 : Q meets the FinalS of A } holds b1 = b2 ; end; :: deftheorem Def6 defines _bool FSM_3:def_6_:_ for E being non empty set for F being Subset of (E ^omega) for A being non empty automaton over F for b4 being strict automaton over Lex E holds ( b4 = _bool A iff ( semiautomaton(# the carrier of b4, the Tran of b4, the InitS of b4 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b4 = { Q where Q is Element of b4 : Q meets the FinalS of A } ) ); registration let E be non empty set ; let F be Subset of (E ^omega); let A be non empty automaton over F; cluster _bool A -> non empty strict deterministic ; coherence ( not _bool A is empty & _bool A is deterministic ) proof set XX = _bool A; semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) by Def6; hence ( not _bool A is empty & _bool A is deterministic ) by Def5; ::_thesis: verum end; end; theorem Th16: :: FSM_3:16 for E being non empty set for F being Subset of (E ^omega) for A being non empty automaton over F holds the carrier of (_bool A) = bool the carrier of A proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for A being non empty automaton over F holds the carrier of (_bool A) = bool the carrier of A let F be Subset of (E ^omega); ::_thesis: for A being non empty automaton over F holds the carrier of (_bool A) = bool the carrier of A let A be non empty automaton over F; ::_thesis: the carrier of (_bool A) = bool the carrier of A semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) by Def6; hence the carrier of (_bool A) = bool the carrier of A by Th14; ::_thesis: verum end; registration let E be non empty set ; let F be Subset of (E ^omega); let A be non empty finite automaton over F; cluster _bool A -> finite strict ; coherence _bool A is finite proof bool the carrier of A is finite ; hence _bool A is finite by Th16; ::_thesis: verum end; end; definition let E be non empty set ; let F be Subset of (E ^omega); let A be non empty automaton over F; let Q be Subset of A; func right-Lang Q -> Subset of (E ^omega) equals :: FSM_3:def 7 { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ; coherence { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } is Subset of (E ^omega) proof defpred S1[ Element of E ^omega ] means $1 -succ_of (Q,A) meets the FinalS of A; { w where w is Element of E ^omega : S1[w] } c= E ^omega from FRAENKEL:sch_10(); hence { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } is Subset of (E ^omega) ; ::_thesis: verum end; end; :: deftheorem defines right-Lang FSM_3:def_7_:_ for E being non empty set for F being Subset of (E ^omega) for A being non empty automaton over F for Q being Subset of A holds right-Lang Q = { w where w is Element of E ^omega : w -succ_of (Q,A) meets the FinalS of A } ; theorem Th17: :: FSM_3:17 for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for A being non empty automaton over F for Q being Subset of A holds ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A ) proof let E be non empty set ; ::_thesis: for w being Element of E ^omega for F being Subset of (E ^omega) for A being non empty automaton over F for Q being Subset of A holds ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A ) let w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for A being non empty automaton over F for Q being Subset of A holds ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A ) let F be Subset of (E ^omega); ::_thesis: for A being non empty automaton over F for Q being Subset of A holds ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A ) let A be non empty automaton over F; ::_thesis: for Q being Subset of A holds ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A ) let Q be Subset of A; ::_thesis: ( w in right-Lang Q iff w -succ_of (Q,A) meets the FinalS of A ) thus ( w in right-Lang Q implies w -succ_of (Q,A) meets the FinalS of A ) ::_thesis: ( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q ) proof assume w in right-Lang Q ; ::_thesis: w -succ_of (Q,A) meets the FinalS of A then ex w9 being Element of E ^omega st ( w = w9 & w9 -succ_of (Q,A) meets the FinalS of A ) ; hence w -succ_of (Q,A) meets the FinalS of A ; ::_thesis: verum end; thus ( w -succ_of (Q,A) meets the FinalS of A implies w in right-Lang Q ) ; ::_thesis: verum end; definition let E be non empty set ; let F be Subset of (E ^omega); let A be non empty automaton over F; func Lang A -> Subset of (E ^omega) equals :: FSM_3:def 8 { u where u is Element of E ^omega : ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ; coherence { u where u is Element of E ^omega : ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } is Subset of (E ^omega) proof defpred S1[ Element of E ^omega ] means ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,$1 ==>* q,A ); { w where w is Element of E ^omega : S1[w] } c= E ^omega from FRAENKEL:sch_10(); hence { u where u is Element of E ^omega : ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } is Subset of (E ^omega) ; ::_thesis: verum end; end; :: deftheorem defines Lang FSM_3:def_8_:_ for E being non empty set for F being Subset of (E ^omega) for A being non empty automaton over F holds Lang A = { u where u is Element of E ^omega : ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } ; theorem Th18: :: FSM_3:18 for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for A being non empty automaton over F holds ( w in Lang A iff ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) proof let E be non empty set ; ::_thesis: for w being Element of E ^omega for F being Subset of (E ^omega) for A being non empty automaton over F holds ( w in Lang A iff ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) let w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for A being non empty automaton over F holds ( w in Lang A iff ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) let F be Subset of (E ^omega); ::_thesis: for A being non empty automaton over F holds ( w in Lang A iff ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) let A be non empty automaton over F; ::_thesis: ( w in Lang A iff ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) thus ( w in Lang A implies ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ) ::_thesis: ( ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) implies w in Lang A ) proof assume w in Lang A ; ::_thesis: ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) then ex u being Element of E ^omega st ( w = u & ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) ) ; hence ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) ; ::_thesis: verum end; thus ( ex p, q being Element of A st ( p in the InitS of A & q in the FinalS of A & p,w ==>* q,A ) implies w in Lang A ) ; ::_thesis: verum end; theorem Th19: :: FSM_3:19 for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for A being non empty automaton over F holds ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A ) proof let E be non empty set ; ::_thesis: for w being Element of E ^omega for F being Subset of (E ^omega) for A being non empty automaton over F holds ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A ) let w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for A being non empty automaton over F holds ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A ) let F be Subset of (E ^omega); ::_thesis: for A being non empty automaton over F holds ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A ) let A be non empty automaton over F; ::_thesis: ( w in Lang A iff w -succ_of ( the InitS of A,A) meets the FinalS of A ) thus ( w in Lang A implies w -succ_of ( the InitS of A,A) meets the FinalS of A ) ::_thesis: ( w -succ_of ( the InitS of A,A) meets the FinalS of A implies w in Lang A ) proof assume w in Lang A ; ::_thesis: w -succ_of ( the InitS of A,A) meets the FinalS of A then consider p, q being Element of A such that A1: p in the InitS of A and A2: q in the FinalS of A and A3: p,w ==>* q,A by Th18; q in w -succ_of ( the InitS of A,A) by A1, A3, REWRITE3:103; hence w -succ_of ( the InitS of A,A) meets the FinalS of A by A2, XBOOLE_0:3; ::_thesis: verum end; assume w -succ_of ( the InitS of A,A) meets the FinalS of A ; ::_thesis: w in Lang A then consider x being set such that A4: x in w -succ_of ( the InitS of A,A) and A5: x in the FinalS of A by XBOOLE_0:3; reconsider x = x as Element of A by A4; ex p being Element of A st ( p in the InitS of A & p,w ==>* x,A ) by A4, REWRITE3:103; hence w in Lang A by A5; ::_thesis: verum end; theorem :: FSM_3:20 for E being non empty set for F being Subset of (E ^omega) for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A let F be Subset of (E ^omega); ::_thesis: for A being non empty automaton over F holds Lang A = left-Lang the FinalS of A let A be non empty automaton over F; ::_thesis: Lang A = left-Lang the FinalS of A A1: for w being Element of E ^omega st w in Lang A holds w in left-Lang the FinalS of A proof let w be Element of E ^omega ; ::_thesis: ( w in Lang A implies w in left-Lang the FinalS of A ) assume w in Lang A ; ::_thesis: w in left-Lang the FinalS of A then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th19; hence w in left-Lang the FinalS of A ; ::_thesis: verum end; for w being Element of E ^omega st w in left-Lang the FinalS of A holds w in Lang A proof let w be Element of E ^omega ; ::_thesis: ( w in left-Lang the FinalS of A implies w in Lang A ) assume w in left-Lang the FinalS of A ; ::_thesis: w in Lang A then the FinalS of A meets w -succ_of ( the InitS of A,A) by Th15; hence w in Lang A by Th19; ::_thesis: verum end; hence Lang A = left-Lang the FinalS of A by A1, SUBSET_1:3; ::_thesis: verum end; theorem :: FSM_3:21 for E being non empty set for F being Subset of (E ^omega) for A being non empty automaton over F holds Lang A = right-Lang the InitS of A proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for A being non empty automaton over F holds Lang A = right-Lang the InitS of A let F be Subset of (E ^omega); ::_thesis: for A being non empty automaton over F holds Lang A = right-Lang the InitS of A let A be non empty automaton over F; ::_thesis: Lang A = right-Lang the InitS of A A1: for w being Element of E ^omega st w in Lang A holds w in right-Lang the InitS of A proof let w be Element of E ^omega ; ::_thesis: ( w in Lang A implies w in right-Lang the InitS of A ) assume w in Lang A ; ::_thesis: w in right-Lang the InitS of A then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th19; hence w in right-Lang the InitS of A ; ::_thesis: verum end; for w being Element of E ^omega st w in right-Lang the InitS of A holds w in Lang A proof let w be Element of E ^omega ; ::_thesis: ( w in right-Lang the InitS of A implies w in Lang A ) assume w in right-Lang the InitS of A ; ::_thesis: w in Lang A then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th17; hence w in Lang A by Th19; ::_thesis: verum end; hence Lang A = right-Lang the InitS of A by A1, SUBSET_1:3; ::_thesis: verum end; theorem Th22: :: FSM_3:22 for E being non empty set for e being Element of E for u being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds (R . 2) `2 = u proof let E be non empty set ; ::_thesis: for e being Element of E for u being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds (R . 2) `2 = u let e be Element of E; ::_thesis: for u being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds (R . 2) `2 = u let u be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds (R . 2) `2 = u let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds (R . 2) `2 = u let R be RedSequence of ==>.-relation TS; ::_thesis: ( (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u implies (R . 2) `2 = u ) assume that A1: (R . 1) `2 = <%e%> ^ u and A2: (R . (len R)) `2 = <%> E ; ::_thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) (R . 1) `2 <> (R . (len R)) `2 by A1, A2, AFINSQ_1:30; then len R >= 1 + 1 by NAT_1:8, NAT_1:25; then ( rng R <> {} & 1 + 1 in dom R ) by FINSEQ_3:25; then A3: [(R . 1),(R . 2)] in ==>.-relation TS by FINSEQ_3:32, REWRITE1:def_2; then consider p being Element of TS, v being Element of E ^omega , q being Element of TS, w being Element of E ^omega such that A4: R . 1 = [p,v] and A5: R . 2 = [q,w] by REWRITE3:31; p,v ==>. q,w,TS by A3, A4, A5, REWRITE3:def_4; then consider u1 being Element of E ^omega such that A6: p,u1 -->. q,TS and A7: v = u1 ^ w by REWRITE3:22; A8: u1 in (Lex E) \/ {(<%> E)} by A6, REWRITE3:15; percases ( u1 in Lex E or u1 in {(<%> E)} ) by A8, XBOOLE_0:def_3; suppose u1 in Lex E ; ::_thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) then len u1 = 1 by Th9; then consider f being Element of E such that A9: u1 = <%f%> and u1 . 0 = f by Th4; (R . 1) `2 = <%f%> ^ w by A4, A7, A9, MCART_1:7; then u = w by A1, Th6; hence ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) by A5, MCART_1:7; ::_thesis: verum end; suppose u1 in {(<%> E)} ; ::_thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) then A10: u1 = <%> E by TARSKI:def_1; B10: {} ^ w = w ; ( v = (R . 1) `2 & w = (R . 2) `2 ) by A4, A5, MCART_1:7; hence ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) by A1, A7, A10, B10; ::_thesis: verum end; end; end; theorem Th23: :: FSM_3:23 for E being non empty set for u being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len R > len u proof let E be non empty set ; ::_thesis: for u being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len R > len u let u be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len R > len u let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len R > len u defpred S1[ Nat] means for R being RedSequence of ==>.-relation TS for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len R > len u; A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_R_being_RedSequence_of_==>.-relation_TS for_u_being_Element_of_E_^omega_st_len_R_=_k_+_1_&_(R_._1)_`2_=_u_&_(R_._(len_R))_`2_=_<%>_E_holds_ len_R_>_len_u let R be RedSequence of ==>.-relation TS; ::_thesis: for u being Element of E ^omega st len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len b2 > len b3 let u be Element of E ^omega ; ::_thesis: ( len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E implies len b1 > len b2 ) assume that A3: len R = k + 1 and A4: (R . 1) `2 = u and A5: (R . (len R)) `2 = <%> E ; ::_thesis: len b1 > len b2 percases ( len u = 0 or len u > 0 ) ; suppose len u = 0 ; ::_thesis: len b1 > len b2 hence len R > len u ; ::_thesis: verum end; supposeA6: len u > 0 ; ::_thesis: len b1 > len b2 then consider e being Element of E, u1 being Element of E ^omega such that A7: u = <%e%> ^ u1 by Th7; len R <> 1 by A4, A5, A6; then consider R9 being RedSequence of ==>.-relation TS such that A8: <*(R . 1)*> ^ R9 = R and A9: (len R9) + 1 = len R by NAT_1:25, REWRITE3:5; A10: (len R9) + 0 < k + 1 by A3, A9, XREAL_1:6; A11: len R9 >= 0 + 1 by NAT_1:8; then len R9 in dom R9 by FINSEQ_3:25; then A12: (R9 . (len R9)) `2 = <%> E by A5, A8, A9, REWRITE3:1; 1 in dom R9 by A11, FINSEQ_3:25; then A13: (<*(R . 1)*> ^ R9) . (1 + 1) = R9 . 1 by REWRITE3:1; percases ( (R . 2) `2 = <%e%> ^ u1 or (R . 2) `2 = u1 ) by A4, A5, A7, Th22; suppose (R . 2) `2 = <%e%> ^ u1 ; ::_thesis: len b1 > len b2 hence len R > len u by A2, A3, A7, A8, A9, A10, A13, A12, XXREAL_0:2; ::_thesis: verum end; suppose (R . 2) `2 = u1 ; ::_thesis: len b1 > len b2 then len R9 > len u1 by A2, A3, A8, A9, A13, A12; then len R > 1 + (len u1) by A9, XREAL_1:6; then len R > (len <%e%>) + (len u1) by AFINSQ_1:def_4; hence len R > len u by A7, AFINSQ_1:17; ::_thesis: verum end; end; end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A14: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A14, A1); hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds len R > len u ; ::_thesis: verum end; theorem Th24: :: FSM_3:24 for E being non empty set for u, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ) proof let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ) let u, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ) let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ) defpred S1[ Nat] means for R being RedSequence of ==>.-relation TS for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ); A1: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_ S1[i_+_1] let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A2: S1[i] ; ::_thesis: S1[i + 1] thus S1[i + 1] ::_thesis: verum proof let R be RedSequence of ==>.-relation TS; ::_thesis: for u being Element of E ^omega st len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ) let u be Element of E ^omega ; ::_thesis: ( len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E implies ex l being Nat st ( l in dom R & (R . l) `2 = v ) ) assume that A3: len R = i + 1 and A4: (R . 1) `2 = u ^ v and A5: (R . (len R)) `2 = <%> E ; ::_thesis: ex l being Nat st ( l in dom R & (R . l) `2 = v ) percases ( len u = 0 or len u > 0 ) ; supposeA6: len u = 0 ; ::_thesis: ex l being Nat st ( l in dom R & (R . l) `2 = v ) set j = 1; take 1 ; ::_thesis: ( 1 in dom R & (R . 1) `2 = v ) rng R <> {} ; hence 1 in dom R by FINSEQ_3:32; ::_thesis: (R . 1) `2 = v B: {} ^ v = v ; u = {} by A6; hence (R . 1) `2 = v by A4, B; ::_thesis: verum end; supposeA7: len u > 0 ; ::_thesis: ex l being Nat st ( l in dom R & (R . l) `2 = v ) then consider e being Element of E, u1 being Element of E ^omega such that A8: u = <%e%> ^ u1 by Th7; len u >= 0 + 1 by A7, NAT_1:13; then (len u) + (len v) >= 1 + (len v) by XREAL_1:6; then len (u ^ v) >= 1 + (len v) by AFINSQ_1:17; then len (u ^ v) >= 1 by Th1; then (len R) + (len (u ^ v)) > (len (u ^ v)) + 1 by A4, A5, Th23, XREAL_1:8; then len R > 1 by XREAL_1:6; then consider R9 being RedSequence of ==>.-relation TS such that A9: (len R9) + 1 = len R and A10: for k being Nat st k in dom R9 holds R9 . k = R . (k + 1) by REWRITE3:7; A11: rng R9 <> {} ; then A12: (R9 . 1) `2 = (R . (1 + 1)) `2 by A10, FINSEQ_3:32; 1 in dom R9 by A11, FINSEQ_3:32; then 1 <= len R9 by FINSEQ_3:25; then len R9 in dom R9 by FINSEQ_3:25; then A13: (R9 . (len R9)) `2 = <%> E by A5, A9, A10; A14: (R . 1) `2 = <%e%> ^ (u1 ^ v) by A4, A8, AFINSQ_1:27; thus ex k being Nat st ( k in dom R & (R . k) `2 = v ) ::_thesis: verum proof percases ( (R . 2) `2 = u ^ v or (R . 2) `2 = u1 ^ v ) by A4, A5, A14, Th22; suppose (R . 2) `2 = u ^ v ; ::_thesis: ex k being Nat st ( k in dom R & (R . k) `2 = v ) then consider l being Nat such that A15: l in dom R9 and A16: (R9 . l) `2 = v by A2, A3, A9, A12, A13; set k = l + 1; take l + 1 ; ::_thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v ) thus l + 1 in dom R by A9, A15, Th3; ::_thesis: (R . (l + 1)) `2 = v thus (R . (l + 1)) `2 = v by A10, A15, A16; ::_thesis: verum end; suppose (R . 2) `2 = u1 ^ v ; ::_thesis: ex k being Nat st ( k in dom R & (R . k) `2 = v ) then consider l being Nat such that A17: l in dom R9 and A18: (R9 . l) `2 = v by A2, A3, A9, A12, A13; set k = l + 1; take l + 1 ; ::_thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v ) thus l + 1 in dom R by A9, A17, Th3; ::_thesis: (R . (l + 1)) `2 = v thus (R . (l + 1)) `2 = v by A10, A17, A18; ::_thesis: verum end; end; end; end; end; end; end; A19: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A19, A1); hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds ex l being Nat st ( l in dom R & (R . l) `2 = v ) ; ::_thesis: verum end; definition let E be non empty set ; let u, v be Element of E ^omega ; func chop (u,v) -> Element of E ^omega means :Def9: :: FSM_3:def 9 for w being Element of E ^omega st w ^ v = u holds it = w if ex w being Element of E ^omega st w ^ v = u otherwise it = u; existence ( ( ex w being Element of E ^omega st w ^ v = u implies ex b1 being Element of E ^omega st for w being Element of E ^omega st w ^ v = u holds b1 = w ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b1 being Element of E ^omega st b1 = u ) ) proof thus ( ex w being Element of E ^omega st w ^ v = u implies ex w1 being Element of E ^omega st for w being Element of E ^omega st w ^ v = u holds w1 = w ) ::_thesis: ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b1 being Element of E ^omega st b1 = u ) proof given w1 being Element of E ^omega such that A1: w1 ^ v = u ; ::_thesis: ex w1 being Element of E ^omega st for w being Element of E ^omega st w ^ v = u holds w1 = w take w1 ; ::_thesis: for w being Element of E ^omega st w ^ v = u holds w1 = w let w be Element of E ^omega ; ::_thesis: ( w ^ v = u implies w1 = w ) assume w ^ v = u ; ::_thesis: w1 = w hence w1 = w by A1, AFINSQ_1:28; ::_thesis: verum end; thus ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ex b1 being Element of E ^omega st b1 = u ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of E ^omega holds ( ( ex w being Element of E ^omega st w ^ v = u & ( for w being Element of E ^omega st w ^ v = u holds b1 = w ) & ( for w being Element of E ^omega st w ^ v = u holds b2 = w ) implies b1 = b2 ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) & b1 = u & b2 = u implies b1 = b2 ) ) proof let w1, w2 be Element of E ^omega ; ::_thesis: ( ( ex w being Element of E ^omega st w ^ v = u & ( for w being Element of E ^omega st w ^ v = u holds w1 = w ) & ( for w being Element of E ^omega st w ^ v = u holds w2 = w ) implies w1 = w2 ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) & w1 = u & w2 = u implies w1 = w2 ) ) hereby ::_thesis: ( ( for w being Element of E ^omega holds not w ^ v = u ) & w1 = u & w2 = u implies w1 = w2 ) given w being Element of E ^omega such that A2: w ^ v = u ; ::_thesis: ( ( for w being Element of E ^omega st w ^ v = u holds w1 = w ) & ( for w being Element of E ^omega st w ^ v = u holds w2 = w ) implies w1 = w2 ) assume that A3: for w being Element of E ^omega st w ^ v = u holds w1 = w and A4: for w being Element of E ^omega st w ^ v = u holds w2 = w ; ::_thesis: w1 = w2 w1 = w by A2, A3; hence w1 = w2 by A2, A4; ::_thesis: verum end; thus ( ( for w being Element of E ^omega holds not w ^ v = u ) & w1 = u & w2 = u implies w1 = w2 ) ; ::_thesis: verum end; consistency for b1 being Element of E ^omega holds verum ; end; :: deftheorem Def9 defines chop FSM_3:def_9_:_ for E being non empty set for u, v, b4 being Element of E ^omega holds ( ( ex w being Element of E ^omega st w ^ v = u implies ( b4 = chop (u,v) iff for w being Element of E ^omega st w ^ v = u holds b4 = w ) ) & ( ( for w being Element of E ^omega holds not w ^ v = u ) implies ( b4 = chop (u,v) iff b4 = u ) ) ); theorem Th25: :: FSM_3:25 for x, y being set for E being non empty set for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) proof let x, y be set ; ::_thesis: for E being non empty set for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) let E be non empty set ; ::_thesis: for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) let u, w, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) let p be RedSequence of ==>.-relation TS; ::_thesis: ( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] implies ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) ) assume that A1: p . 1 = [x,(u ^ w)] and A2: p . (len p) = [y,(v ^ w)] ; ::_thesis: ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) A3: len p >= 0 + 1 by NAT_1:13; then 1 in dom p by FINSEQ_3:25; then A4: dim2 ((p . 1),E) = (p . 1) `2 by A1, REWRITE3:51 .= u ^ w by A1, MCART_1:7 ; deffunc H1( set ) -> set = [((p . $1) `1),(chop ((dim2 ((p . $1),E)),w))]; consider q being FinSequence such that A5: len q = len p and A6: for k being Nat st k in dom q holds q . k = H1(k) from FINSEQ_1:sch_2(); A7: for k being Element of NAT st k in dom q & k + 1 in dom q holds [(q . k),(q . (k + 1))] in ==>.-relation TS proof let k be Element of NAT ; ::_thesis: ( k in dom q & k + 1 in dom q implies [(q . k),(q . (k + 1))] in ==>.-relation TS ) assume that A8: k in dom q and A9: k + 1 in dom q ; ::_thesis: [(q . k),(q . (k + 1))] in ==>.-relation TS ( 1 <= k & k <= len q ) by A8, FINSEQ_3:25; then A10: k in dom p by A5, FINSEQ_3:25; then consider v1 being Element of E ^omega such that A11: (p . k) `2 = v1 ^ (v ^ w) by A2, REWRITE3:52; ( 1 <= k + 1 & k + 1 <= len q ) by A9, FINSEQ_3:25; then A12: k + 1 in dom p by A5, FINSEQ_3:25; then consider v2 being Element of E ^omega such that A13: (p . (k + 1)) `2 = v2 ^ (v ^ w) by A2, REWRITE3:52; A14: [(p . k),(p . (k + 1))] in ==>.-relation TS by A10, A12, REWRITE1:def_2; then [(p . k),[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A13, REWRITE3:48; then [[((p . k) `1),(v1 ^ (v ^ w))],[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A11, REWRITE3:48; then (p . k) `1 ,v1 ^ (v ^ w) ==>. (p . (k + 1)) `1 ,v2 ^ (v ^ w),TS by REWRITE3:def_4; then consider u1 being Element of E ^omega such that A15: (p . k) `1 ,u1 -->. (p . (k + 1)) `1 ,TS and A16: v1 ^ (v ^ w) = u1 ^ (v2 ^ (v ^ w)) by REWRITE3:22; A17: ex r1 being Element of TS ex w1 being Element of E ^omega ex r2 being Element of TS ex w2 being Element of E ^omega st ( p . k = [r1,w1] & p . (k + 1) = [r2,w2] ) by A14, REWRITE3:31; then dim2 ((p . (k + 1)),E) = v2 ^ (v ^ w) by A13, REWRITE3:def_5; then A18: q . (k + 1) = [((p . (k + 1)) `1),(chop ((v2 ^ (v ^ w)),w))] by A6, A9 .= [((p . (k + 1)) `1),(chop (((v2 ^ v) ^ w),w))] by AFINSQ_1:27 .= [((p . (k + 1)) `1),(v2 ^ v)] by Def9 ; (v1 ^ v) ^ w = u1 ^ (v2 ^ (v ^ w)) by A16, AFINSQ_1:27 .= (u1 ^ v2) ^ (v ^ w) by AFINSQ_1:27 .= ((u1 ^ v2) ^ v) ^ w by AFINSQ_1:27 ; then v1 ^ v = (u1 ^ v2) ^ v by AFINSQ_1:28 .= u1 ^ (v2 ^ v) by AFINSQ_1:27 ; then A19: (p . k) `1 ,v1 ^ v ==>. (p . (k + 1)) `1 ,v2 ^ v,TS by A15, REWRITE3:def_3; dim2 ((p . k),E) = v1 ^ (v ^ w) by A11, A17, REWRITE3:def_5; then q . k = [((p . k) `1),(chop ((v1 ^ (v ^ w)),w))] by A6, A8 .= [((p . k) `1),(chop (((v1 ^ v) ^ w),w))] by AFINSQ_1:27 .= [((p . k) `1),(v1 ^ v)] by Def9 ; hence [(q . k),(q . (k + 1))] in ==>.-relation TS by A19, A18, REWRITE3:def_4; ::_thesis: verum end; len p in dom p by A3, FINSEQ_3:25; then A20: dim2 ((p . (len p)),E) = (p . (len p)) `2 by A1, REWRITE3:51 .= v ^ w by A2, MCART_1:7 ; reconsider q = q as RedSequence of ==>.-relation TS by A5, A7, REWRITE1:def_2; 1 in dom q by A5, A3, FINSEQ_3:25; then A21: q . 1 = [((p . 1) `1),(chop ((dim2 ((p . 1),E)),w))] by A6 .= [x,(chop ((u ^ w),w))] by A1, A4, MCART_1:7 .= [x,u] by Def9 ; len p in dom q by A5, A3, FINSEQ_3:25; then q . (len q) = [((p . (len p)) `1),(chop ((dim2 ((p . (len p)),E)),w))] by A5, A6 .= [y,(chop ((v ^ w),w))] by A2, A20, MCART_1:7 .= [y,v] by Def9 ; hence ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) by A21; ::_thesis: verum end; theorem Th26: :: FSM_3:26 for x, y being set for E being non empty set for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds ==>.-relation TS reduces [x,u],[y,v] proof let x, y be set ; ::_thesis: for E being non empty set for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds ==>.-relation TS reduces [x,u],[y,v] let E be non empty set ; ::_thesis: for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds ==>.-relation TS reduces [x,u],[y,v] let u, w, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds ==>.-relation TS reduces [x,u],[y,v] let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: ( ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] implies ==>.-relation TS reduces [x,u],[y,v] ) assume ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] ; ::_thesis: ==>.-relation TS reduces [x,u],[y,v] then ex p being RedSequence of ==>.-relation TS st ( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] ) by REWRITE1:def_3; then ex q being RedSequence of ==>.-relation TS st ( q . 1 = [x,u] & q . (len q) = [y,v] ) by Th25; hence ==>.-relation TS reduces [x,u],[y,v] by REWRITE1:def_3; ::_thesis: verum end; theorem Th27: :: FSM_3:27 for x, y being set for E being non empty set for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds x,u ==>* y,v,TS proof let x, y be set ; ::_thesis: for E being non empty set for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds x,u ==>* y,v,TS let E be non empty set ; ::_thesis: for u, w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds x,u ==>* y,v,TS let u, w, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st x,u ^ w ==>* y,v ^ w,TS holds x,u ==>* y,v,TS let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: ( x,u ^ w ==>* y,v ^ w,TS implies x,u ==>* y,v,TS ) assume x,u ^ w ==>* y,v ^ w,TS ; ::_thesis: x,u ==>* y,v,TS then ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by REWRITE3:def_6; then ==>.-relation TS reduces [x,u],[y,v] by Th26; hence x,u ==>* y,v,TS by REWRITE3:def_6; ::_thesis: verum end; theorem Th28: :: FSM_3:28 for E being non empty set for u, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p, q being Element of TS st p,u ^ v ==>* q,TS holds ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) proof let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p, q being Element of TS st p,u ^ v ==>* q,TS holds ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) let u, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} for p, q being Element of TS st p,u ^ v ==>* q,TS holds ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: for p, q being Element of TS st p,u ^ v ==>* q,TS holds ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) let p, q be Element of TS; ::_thesis: ( p,u ^ v ==>* q,TS implies ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) ) assume A1: p,u ^ v ==>* q,TS ; ::_thesis: ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) then p,u ^ v ==>* q, <%> E,TS by REWRITE3:def_7; then ==>.-relation TS reduces [p,(u ^ v)],[q,(<%> E)] by REWRITE3:def_6; then consider R being RedSequence of ==>.-relation TS such that A2: R . 1 = [p,(u ^ v)] and A3: R . (len R) = [q,(<%> E)] by REWRITE1:def_3; A4: (R . (len R)) `2 = <%> E by A3, MCART_1:7; (R . 1) `2 = u ^ v by A2, MCART_1:7; then consider l being Nat such that A5: l in dom R and A6: (R . l) `2 = v by A4, Th24; percases ( l + 1 in dom R or not l + 1 in dom R ) ; supposeA7: l + 1 in dom R ; ::_thesis: ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) then (R . l) `1 in TS by A5, REWRITE3:49; then reconsider r = (R . l) `1 as Element of TS by STRUCT_0:def_5; A8: R . l = [r,v] by A5, A6, A7, REWRITE3:48; A9: l <= len R by A5, FINSEQ_3:25; take r ; ::_thesis: ( p,u ==>* r,TS & r,v ==>* q,TS ) A10: ( 1 in dom R & 1 <= l ) by A5, FINSEQ_3:25, FINSEQ_5:6; reconsider l = l as Element of NAT by ORDINAL1:def_12; ==>.-relation TS reduces R . 1,R . l by A5, A10, REWRITE1:17; then p,u ^ v ==>* r,{} ^ v,TS by A2, A8, REWRITE3:def_6; then p,u ==>* r, <%> E,TS by Th27; hence p,u ==>* r,TS by REWRITE3:def_7; ::_thesis: r,v ==>* q,TS 0 + 1 <= len R by NAT_1:13; then len R in dom R by FINSEQ_3:25; then ==>.-relation TS reduces R . l,R . (len R) by A5, A9, REWRITE1:17; then r,v ==>* q, <%> E,TS by A3, A8, REWRITE3:def_6; hence r,v ==>* q,TS by REWRITE3:def_7; ::_thesis: verum end; suppose not l + 1 in dom R ; ::_thesis: ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) then A11: v = <%> E by A4, A5, A6, REWRITE3:3; u ^ {} = u ; hence ex r being Element of TS st ( p,u ==>* r,TS & r,v ==>* q,TS ) by A1, A11, REWRITE3:95; ::_thesis: verum end; end; end; theorem Th29: :: FSM_3:29 for X being set for E being non empty set for w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) proof let X be set ; ::_thesis: for E being non empty set for w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) let E be non empty set ; ::_thesis: for w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) let w, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) A1: now__::_thesis:_for_x_being_set_st_x_in_v_-succ_of_((w_-succ_of_(X,TS)),TS)_holds_ x_in_(w_^_v)_-succ_of_(X,TS) let x be set ; ::_thesis: ( x in v -succ_of ((w -succ_of (X,TS)),TS) implies x in (w ^ v) -succ_of (X,TS) ) assume A2: x in v -succ_of ((w -succ_of (X,TS)),TS) ; ::_thesis: x in (w ^ v) -succ_of (X,TS) then reconsider r = x as Element of TS ; consider p being Element of TS such that A3: p in w -succ_of (X,TS) and A4: p,v ==>* r,TS by A2, REWRITE3:103; consider q being Element of TS such that A5: q in X and A6: q,w ==>* p,TS by A3, REWRITE3:103; q,w ^ v ==>* r,TS by A4, A6, REWRITE3:99; hence x in (w ^ v) -succ_of (X,TS) by A5, REWRITE3:103; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_(w_^_v)_-succ_of_(X,TS)_holds_ x_in_v_-succ_of_((w_-succ_of_(X,TS)),TS) let x be set ; ::_thesis: ( x in (w ^ v) -succ_of (X,TS) implies x in v -succ_of ((w -succ_of (X,TS)),TS) ) assume A7: x in (w ^ v) -succ_of (X,TS) ; ::_thesis: x in v -succ_of ((w -succ_of (X,TS)),TS) then reconsider r = x as Element of TS ; consider q being Element of TS such that A8: q in X and A9: q,w ^ v ==>* r,TS by A7, REWRITE3:103; consider p being Element of TS such that A10: q,w ==>* p,TS and A11: p,v ==>* r,TS by A9, Th28; p in w -succ_of (X,TS) by A8, A10, REWRITE3:103; hence x in v -succ_of ((w -succ_of (X,TS)),TS) by A11, REWRITE3:103; ::_thesis: verum end; hence (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) by A1, TARSKI:1; ::_thesis: verum end; theorem Th30: :: FSM_3:30 for E being non empty set for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)} proof let E be non empty set ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)} let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)} Lex E c= (Lex E) \/ {(<%> E)} by XBOOLE_1:7; then ( dom the Tran of (_bool TS) c= [: the carrier of (_bool TS),(Lex E):] & [: the carrier of (_bool TS),(Lex E):] c= [: the carrier of (_bool TS),((Lex E) \/ {(<%> E)}):] ) by ZFMISC_1:95; hence _bool TS is non empty transition-system over (Lex E) \/ {(<%> E)} by RELSET_1:5, XBOOLE_1:1; ::_thesis: verum end; theorem Th31: :: FSM_3:31 for X being set for E being non empty set for w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} proof let X be set ; ::_thesis: for E being non empty set for w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} let E be non empty set ; ::_thesis: for w, v being Element of E ^omega for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} let w, v be Element of E ^omega ; ::_thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; ::_thesis: w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} defpred S1[ Nat] means for u being Element of E ^omega st len u <= $1 holds for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))}; A1: not <%> E in rng (dom the Tran of (_bool TS)) by Th8; A2: S1[ 0 ] proof let u be Element of E ^omega ; ::_thesis: ( len u <= 0 implies for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} ) assume len u <= 0 ; ::_thesis: for v being Element of E ^omega holds u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} then A3: u = <%> E ; let v be Element of E ^omega ; ::_thesis: u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} reconsider vso = {(v -succ_of (X,TS))} as Subset of (_bool TS) by Def1; u -succ_of (vso,(_bool TS)) = vso by A1, A3, REWRITE3:104; hence u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ {}) -succ_of (X,TS))} .= {((v ^ {}) -succ_of (X,TS))} .= {((v ^ u) -succ_of (X,TS))} by A3 ; ::_thesis: verum end; A4: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_u_being_Element_of_E_^omega_st_len_u_<=_k_+_1_holds_ for_v_being_Element_of_E_^omega_holds_u_-succ_of_({(v_-succ_of_(X,TS))},(_bool_TS))_=_{((v_^_u)_-succ_of_(X,TS))} let u be Element of E ^omega ; ::_thesis: ( len u <= k + 1 implies for v being Element of E ^omega holds b2 -succ_of ({(b3 -succ_of (X,TS))},(_bool TS)) = {((b3 ^ b2) -succ_of (X,TS))} ) assume A6: len u <= k + 1 ; ::_thesis: for v being Element of E ^omega holds b2 -succ_of ({(b3 -succ_of (X,TS))},(_bool TS)) = {((b3 ^ b2) -succ_of (X,TS))} let v be Element of E ^omega ; ::_thesis: b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))} percases ( k = 0 or k <> 0 ) ; supposeA7: k = 0 ; ::_thesis: b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))} percases ( len u = 0 or len u = 1 ) by A6, A7, NAT_1:25; suppose len u = 0 ; ::_thesis: b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))} hence u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} by A2; ::_thesis: verum end; supposeA8: len u = 1 ; ::_thesis: b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))} A9: now__::_thesis:_for_x_being_set_st_x_in_{((v_^_u)_-succ_of_(X,TS))}_holds_ x_in_u_-succ_of_({(v_-succ_of_(X,TS))},(_bool_TS)) let x be set ; ::_thesis: ( x in {((v ^ u) -succ_of (X,TS))} implies x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) ) assume A10: x in {((v ^ u) -succ_of (X,TS))} ; ::_thesis: x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) then reconsider P = x as Element of (_bool TS) by Def1; x = (v ^ u) -succ_of (X,TS) by A10, TARSKI:def_1; then x = u -succ_of ((v -succ_of (X,TS)),TS) by Th29; then A11: v -succ_of (X,TS),u ==>* x, _bool TS by A8, Th13; ( v -succ_of (X,TS) is Element of (_bool TS) & v -succ_of (X,TS) in {(v -succ_of (X,TS))} ) by Def1, TARSKI:def_1; then P in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) by A11, REWRITE3:103; hence x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_u_-succ_of_({(v_-succ_of_(X,TS))},(_bool_TS))_holds_ x_in_{((v_^_u)_-succ_of_(X,TS))} let x be set ; ::_thesis: ( x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) implies x in {((v ^ u) -succ_of (X,TS))} ) assume A12: x in u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) ; ::_thesis: x in {((v ^ u) -succ_of (X,TS))} then reconsider P = x as Element of (_bool TS) ; consider Q being Element of (_bool TS) such that A13: ( Q in {(v -succ_of (X,TS))} & Q,u ==>* P, _bool TS ) by A12, REWRITE3:103; ( Q = v -succ_of (X,TS) & P = u -succ_of (Q,TS) ) by A8, A13, Th13, TARSKI:def_1; then P = (v ^ u) -succ_of (X,TS) by Th29; hence x in {((v ^ u) -succ_of (X,TS))} by TARSKI:def_1; ::_thesis: verum end; hence u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} by A9, TARSKI:1; ::_thesis: verum end; end; end; supposeA14: k <> 0 ; ::_thesis: b1 -succ_of ({(b2 -succ_of (X,TS))},(_bool TS)) = {((b2 ^ b1) -succ_of (X,TS))} reconsider bTS = _bool TS as non empty transition-system over (Lex E) \/ {(<%> E)} by Th30; consider v1, v2 being Element of E ^omega such that A15: len v1 <= k and A16: len v2 <= k and A17: u = v1 ^ v2 by A6, A14, Th5; A18: v1 -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ v1) -succ_of (X,TS))} by A5, A15; A19: the Tran of bTS = the Tran of (_bool TS) ; then (v1 ^ v2) -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = (v1 ^ v2) -succ_of ({(v -succ_of (X,TS))},bTS) by REWRITE3:105 .= v2 -succ_of ((v1 -succ_of ({(v -succ_of (X,TS))},bTS)),bTS) by Th29 .= v2 -succ_of ((v1 -succ_of ({(v -succ_of (X,TS))},(_bool TS))),bTS) by A19, REWRITE3:105 .= v2 -succ_of ((v1 -succ_of ({(v -succ_of (X,TS))},(_bool TS))),(_bool TS)) by A19, REWRITE3:105 .= {(((v ^ v1) ^ v2) -succ_of (X,TS))} by A5, A16, A18 .= {((v ^ (v1 ^ v2)) -succ_of (X,TS))} by AFINSQ_1:27 ; hence u -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ u) -succ_of (X,TS))} by A17; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A2, A4); then ( len w <= len w implies w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} ) ; hence w -succ_of ({(v -succ_of (X,TS))},(_bool TS)) = {((v ^ w) -succ_of (X,TS))} ; ::_thesis: verum end; theorem Th32: :: FSM_3:32 for X being set for E being non empty set for w being Element of E ^omega for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))} proof let X be set ; ::_thesis: for E being non empty set for w being Element of E ^omega for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))} let E be non empty set ; ::_thesis: for w being Element of E ^omega for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))} let w be Element of E ^omega ; ::_thesis: for SA being non empty semiautomaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))} let SA be non empty semiautomaton over (Lex E) \/ {(<%> E)}; ::_thesis: w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = {(w -succ_of (X,SA))} set TS = transition-system(# the carrier of SA, the Tran of SA #); set Es = (<%> E) -succ_of (X,SA); transition-system(# the carrier of (_bool SA), the Tran of (_bool SA) #) = _bool transition-system(# the carrier of SA, the Tran of SA #) by Def3; hence w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool SA)) = w -succ_of ({((<%> E) -succ_of (X,SA))},(_bool transition-system(# the carrier of SA, the Tran of SA #))) by REWRITE3:105 .= w -succ_of ({((<%> E) -succ_of (X,transition-system(# the carrier of SA, the Tran of SA #)))},(_bool transition-system(# the carrier of SA, the Tran of SA #))) by REWRITE3:105 .= {(({} ^ w) -succ_of (X,transition-system(# the carrier of SA, the Tran of SA #)))} by Th31 .= {(w -succ_of (X,transition-system(# the carrier of SA, the Tran of SA #)))} .= {(w -succ_of (X,SA))} by REWRITE3:105 ; ::_thesis: verum end; theorem Th33: :: FSM_3:33 for x being set for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} for P being Subset of A st x in the FinalS of A & x in P holds P in the FinalS of (_bool A) proof let x be set ; ::_thesis: for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} for P being Subset of A st x in the FinalS of A & x in P holds P in the FinalS of (_bool A) let E be non empty set ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} for P being Subset of A st x in the FinalS of A & x in P holds P in the FinalS of (_bool A) let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: for P being Subset of A st x in the FinalS of A & x in P holds P in the FinalS of (_bool A) let P be Subset of A; ::_thesis: ( x in the FinalS of A & x in P implies P in the FinalS of (_bool A) ) assume ( x in the FinalS of A & x in P ) ; ::_thesis: P in the FinalS of (_bool A) then A1: P meets the FinalS of A by XBOOLE_0:3; P is Element of (_bool A) by Th16; then P in { Q where Q is Element of (_bool A) : Q meets the FinalS of A } by A1; hence P in the FinalS of (_bool A) by Def6; ::_thesis: verum end; theorem Th34: :: FSM_3:34 for X being set for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds X meets the FinalS of A proof let X be set ; ::_thesis: for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds X meets the FinalS of A let E be non empty set ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} st X in the FinalS of (_bool A) holds X meets the FinalS of A let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: ( X in the FinalS of (_bool A) implies X meets the FinalS of A ) assume A1: X in the FinalS of (_bool A) ; ::_thesis: X meets the FinalS of A the FinalS of (_bool A) = { Q where Q is Element of (_bool A) : Q meets the FinalS of A } by Def6; then ex Q being Element of (_bool A) st ( X = Q & Q meets the FinalS of A ) by A1; hence X meets the FinalS of A ; ::_thesis: verum end; theorem Th35: :: FSM_3:35 for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} holds the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} proof let E be non empty set ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} the InitS of (_bool A) = the InitS of semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #) .= the InitS of (_bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)) by Def6 .= {((<%> E) -succ_of ( the InitS of semiautomaton(# the carrier of A, the Tran of A, the InitS of A #),semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)))} by Def3 ; hence the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} by REWRITE3:105; ::_thesis: verum end; theorem Th36: :: FSM_3:36 for X being set for E being non empty set for w being Element of E ^omega for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))} proof let X be set ; ::_thesis: for E being non empty set for w being Element of E ^omega for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))} let E be non empty set ; ::_thesis: for w being Element of E ^omega for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))} let w be Element of E ^omega ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))} let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = {(w -succ_of (X,A))} set SA = semiautomaton(# the carrier of A, the Tran of A, the InitS of A #); set Es = (<%> E) -succ_of (X,A); semiautomaton(# the carrier of (_bool A), the Tran of (_bool A), the InitS of (_bool A) #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) by Def6; hence w -succ_of ({((<%> E) -succ_of (X,A))},(_bool A)) = w -succ_of ({((<%> E) -succ_of (X,A))},(_bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #))) by REWRITE3:105 .= w -succ_of ({((<%> E) -succ_of (X,semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)))},(_bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #))) by REWRITE3:105 .= {(w -succ_of (X,semiautomaton(# the carrier of A, the Tran of A, the InitS of A #)))} by Th32 .= {(w -succ_of (X,A))} by REWRITE3:105 ; ::_thesis: verum end; theorem Th37: :: FSM_3:37 for E being non empty set for w being Element of E ^omega for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} proof let E be non empty set ; ::_thesis: for w being Element of E ^omega for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} let w be Element of E ^omega ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} set Es = (<%> E) -succ_of ( the InitS of A,A); the InitS of (_bool A) = {((<%> E) -succ_of ( the InitS of A,A))} by Th35; hence w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} by Th36; ::_thesis: verum end; theorem Th38: :: FSM_3:38 for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang (_bool A) proof let E be non empty set ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} holds Lang A = Lang (_bool A) let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: Lang A = Lang (_bool A) set DA = _bool A; A1: for w being Element of E ^omega st w in Lang A holds w in Lang (_bool A) proof let w be Element of E ^omega ; ::_thesis: ( w in Lang A implies w in Lang (_bool A) ) assume w in Lang A ; ::_thesis: w in Lang (_bool A) then w -succ_of ( the InitS of A,A) meets the FinalS of A by Th19; then ex x being set st ( x in w -succ_of ( the InitS of A,A) & x in the FinalS of A ) by XBOOLE_0:3; then A2: w -succ_of ( the InitS of A,A) in the FinalS of (_bool A) by Th33; w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} by Th37; then w -succ_of ( the InitS of A,A) in w -succ_of ( the InitS of (_bool A),(_bool A)) by TARSKI:def_1; then w -succ_of ( the InitS of (_bool A),(_bool A)) meets the FinalS of (_bool A) by A2, XBOOLE_0:3; hence w in Lang (_bool A) by Th19; ::_thesis: verum end; for w being Element of E ^omega st w in Lang (_bool A) holds w in Lang A proof let w be Element of E ^omega ; ::_thesis: ( w in Lang (_bool A) implies w in Lang A ) assume w in Lang (_bool A) ; ::_thesis: w in Lang A then w -succ_of ( the InitS of (_bool A),(_bool A)) meets the FinalS of (_bool A) by Th19; then consider x being set such that A3: x in w -succ_of ( the InitS of (_bool A),(_bool A)) and A4: x in the FinalS of (_bool A) by XBOOLE_0:3; w -succ_of ( the InitS of (_bool A),(_bool A)) = {(w -succ_of ( the InitS of A,A))} by Th37; then x = w -succ_of ( the InitS of A,A) by A3, TARSKI:def_1; then w -succ_of ( the InitS of A,A) meets the FinalS of A by A4, Th34; hence w in Lang A by Th19; ::_thesis: verum end; hence Lang A = Lang (_bool A) by A1, SUBSET_1:3; ::_thesis: verum end; theorem :: FSM_3:39 for E being non empty set for A being non empty automaton over (Lex E) \/ {(<%> E)} ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA proof let E be non empty set ; ::_thesis: for A being non empty automaton over (Lex E) \/ {(<%> E)} ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA let A be non empty automaton over (Lex E) \/ {(<%> E)}; ::_thesis: ex DA being non empty deterministic automaton over Lex E st Lang A = Lang DA set DA = _bool A; take _bool A ; ::_thesis: Lang A = Lang (_bool A) thus Lang A = Lang (_bool A) by Th38; ::_thesis: verum end; theorem :: FSM_3:40 for E being non empty set for FA being non empty finite automaton over (Lex E) \/ {(<%> E)} ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA proof let E be non empty set ; ::_thesis: for FA being non empty finite automaton over (Lex E) \/ {(<%> E)} ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA let FA be non empty finite automaton over (Lex E) \/ {(<%> E)}; ::_thesis: ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA set bNFA = _bool FA; Lang FA = Lang (_bool FA) by Th38; hence ex DFA being non empty finite deterministic automaton over Lex E st Lang FA = Lang DFA ; ::_thesis: verum end;