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