:: REWRITE3 semantic presentation
begin
theorem Th1: :: REWRITE3:1
for x being set
for k being Nat
for p being FinSequence st k in dom p holds
(<*x*> ^ p) . (k + 1) = p . k
proof
let x be set ; ::_thesis: for k being Nat
for p being FinSequence st k in dom p holds
(<*x*> ^ p) . (k + 1) = p . k
let k be Nat; ::_thesis: for p being FinSequence st k in dom p holds
(<*x*> ^ p) . (k + 1) = p . k
let p be FinSequence; ::_thesis: ( k in dom p implies (<*x*> ^ p) . (k + 1) = p . k )
assume A1: k in dom p ; ::_thesis: (<*x*> ^ p) . (k + 1) = p . k
k >= 1 by A1, FINSEQ_3:25;
then k >= len <*x*> by FINSEQ_1:39;
then A2: (len <*x*>) + 0 < k + 1 by XREAL_1:8;
(len <*x*>) + k in dom (<*x*> ^ p) by A1, FINSEQ_1:28;
then k + 1 in dom (<*x*> ^ p) by FINSEQ_1:39;
then k + 1 <= len (<*x*> ^ p) by FINSEQ_3:25;
then (<*x*> ^ p) . (k + 1) = p . ((k + 1) - (len <*x*>)) by A2, FINSEQ_1:24
.= p . ((k + 1) - 1) by FINSEQ_1:39
.= p . (k + (1 - 1)) ;
hence (<*x*> ^ p) . (k + 1) = p . k ; ::_thesis: verum
end;
theorem Th2: :: REWRITE3:2
for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being set st
( p = q ^ <*x*> & len p = (len q) + 1 )
proof
let p be FinSequence; ::_thesis: ( p <> {} implies ex q being FinSequence ex x being set st
( p = q ^ <*x*> & len p = (len q) + 1 ) )
assume p <> {} ; ::_thesis: ex q being FinSequence ex x being set st
( p = q ^ <*x*> & len p = (len q) + 1 )
then consider q being FinSequence, x being set such that
A1: p = q ^ <*x*> by FINSEQ_1:46;
take q ; ::_thesis: ex x being set st
( p = q ^ <*x*> & len p = (len q) + 1 )
take x ; ::_thesis: ( p = q ^ <*x*> & len p = (len q) + 1 )
len p = (len q) + (len <*x*>) by A1, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:40 ;
hence ( p = q ^ <*x*> & len p = (len q) + 1 ) by A1; ::_thesis: verum
end;
theorem Th3: :: REWRITE3:3
for k being Nat
for p being FinSequence st k in dom p & not k + 1 in dom p holds
len p = k
proof
let k be Nat; ::_thesis: for p being FinSequence st k in dom p & not k + 1 in dom p holds
len p = k
let p be FinSequence; ::_thesis: ( k in dom p & not k + 1 in dom p implies len p = k )
assume that
A1: k in dom p and
A2: not k + 1 in dom p ; ::_thesis: len p = k
A3: ( 1 > k + 1 or k + 1 > len p ) by A2, FINSEQ_3:25;
A4: 1 + 0 <= k + 1 by XREAL_1:7;
k <= len p by A1, FINSEQ_3:25;
hence len p = k by A3, A4, NAT_1:22; ::_thesis: verum
end;
begin
theorem Th4: :: REWRITE3:4
for R being Relation
for P being RedSequence of R
for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds
( q1 is RedSequence of R & q2 is RedSequence of R )
proof
let R be Relation; ::_thesis: for P being RedSequence of R
for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds
( q1 is RedSequence of R & q2 is RedSequence of R )
let P be RedSequence of R; ::_thesis: for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds
( q1 is RedSequence of R & q2 is RedSequence of R )
let q1, q2 be FinSequence; ::_thesis: ( P = q1 ^ q2 & len q1 > 0 & len q2 > 0 implies ( q1 is RedSequence of R & q2 is RedSequence of R ) )
assume that
A1: P = q1 ^ q2 and
A2: len q1 > 0 and
A3: len q2 > 0 ; ::_thesis: ( q1 is RedSequence of R & q2 is RedSequence of R )
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_q1_&_i_+_1_in_dom_q1_holds_
[(q1_._i),(q1_._(i_+_1))]_in_R
let i be Element of NAT ; ::_thesis: ( i in dom q1 & i + 1 in dom q1 implies [(q1 . i),(q1 . (i + 1))] in R )
assume that
A4: i in dom q1 and
A5: i + 1 in dom q1 ; ::_thesis: [(q1 . i),(q1 . (i + 1))] in R
A6: i + 1 <= len q1 by A5, FINSEQ_3:25;
A7: 1 <= i + 1 by A5, FINSEQ_3:25;
then A8: q1 . (i + 1) = (q1 ^ q2) . (i + 1) by A6, FINSEQ_1:64;
A9: len q1 <= len P by A1, CALCUL_1:6;
then i + 1 <= len P by A6, XXREAL_0:2;
then A10: i + 1 in dom P by A7, FINSEQ_3:25;
A11: 1 <= i by A4, FINSEQ_3:25;
A12: i <= len q1 by A4, FINSEQ_3:25;
then i <= len P by A9, XXREAL_0:2;
then A13: i in dom P by A11, FINSEQ_3:25;
q1 . i = (q1 ^ q2) . i by A11, A12, FINSEQ_1:64;
hence [(q1 . i),(q1 . (i + 1))] in R by A1, A8, A13, A10, REWRITE1:def_2; ::_thesis: verum
end;
hence q1 is RedSequence of R by A2, REWRITE1:def_2; ::_thesis: q2 is RedSequence of R
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_q2_&_i_+_1_in_dom_q2_holds_
[(q2_._i),(q2_._(i_+_1))]_in_R
let i be Element of NAT ; ::_thesis: ( i in dom q2 & i + 1 in dom q2 implies [(q2 . i),(q2 . (i + 1))] in R )
assume that
A14: i in dom q2 and
A15: i + 1 in dom q2 ; ::_thesis: [(q2 . i),(q2 . (i + 1))] in R
A16: 1 <= i + 1 by A15, FINSEQ_3:25;
then A17: 1 <= (i + 1) + (len q1) by NAT_1:12;
A18: 1 <= i by A14, FINSEQ_3:25;
then A19: 1 <= i + (len q1) by NAT_1:12;
A20: i + 1 <= len q2 by A15, FINSEQ_3:25;
then A21: q2 . (i + 1) = (q1 ^ q2) . ((len q1) + (i + 1)) by A16, FINSEQ_1:65;
A22: (len q1) + (len q2) = len P by A1, FINSEQ_1:22;
then (len q1) + (i + 1) <= ((len P) - (len q2)) + (len q2) by A20, XREAL_1:7;
then A23: ((len q1) + i) + 1 in dom P by A17, FINSEQ_3:25;
A24: i <= len q2 by A14, FINSEQ_3:25;
then (len q1) + i <= ((len P) - (len q2)) + (len q2) by A22, XREAL_1:7;
then A25: (len q1) + i in dom P by A19, FINSEQ_3:25;
q2 . i = (q1 ^ q2) . ((len q1) + i) by A18, A24, FINSEQ_1:65;
hence [(q2 . i),(q2 . (i + 1))] in R by A1, A21, A25, A23, REWRITE1:def_2; ::_thesis: verum
end;
hence q2 is RedSequence of R by A3, REWRITE1:def_2; ::_thesis: verum
end;
theorem Th5: :: REWRITE3:5
for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P )
proof
let R be Relation; ::_thesis: for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P )
let P be RedSequence of R; ::_thesis: ( len P > 1 implies ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) )
assume A1: len P > 1 ; ::_thesis: ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P )
consider x being set , Q being FinSequence such that
A2: P = <*x*> ^ Q and
A3: len P = (len Q) + 1 by REWRITE1:5;
1 + (len Q) > 1 + 0 by A1, A3;
then ( len <*x*> = 1 & len Q > 0 ) by FINSEQ_1:39;
then A4: Q is RedSequence of R by A2, Th4;
P . 1 = x by A2, FINSEQ_1:41;
hence ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) by A2, A3, A4; ::_thesis: verum
end;
theorem :: REWRITE3:6
for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P )
proof
let R be Relation; ::_thesis: for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P )
let P be RedSequence of R; ::_thesis: ( len P > 1 implies ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) )
assume A1: len P > 1 ; ::_thesis: ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P )
consider Q being FinSequence, x being set such that
A2: P = Q ^ <*x*> and
A3: (len Q) + 1 = len P by Th2;
1 + (len Q) > 1 + 0 by A1, A3;
then ( len <*x*> = 1 & len Q > 0 ) by FINSEQ_1:39;
then A4: Q is RedSequence of R by A2, Th4;
P . (len P) = x by A2, A3, FINSEQ_1:42;
hence ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) by A2, A3, A4; ::_thesis: verum
end;
theorem :: REWRITE3:7
for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
proof
let R be Relation; ::_thesis: for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
let P be RedSequence of R; ::_thesis: ( len P > 1 implies ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) ) )
assume len P > 1 ; ::_thesis: ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
then consider Q being RedSequence of R such that
A1: ( P = <*(P . 1)*> ^ Q & (len Q) + 1 = len P ) by Th5;
take Q ; ::_thesis: ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
thus ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) ) by A1, Th1; ::_thesis: verum
end;
theorem Th8: :: REWRITE3:8
for x, y being set
for R being Relation st <*x,y*> is RedSequence of R holds
[x,y] in R
proof
let x, y be set ; ::_thesis: for R being Relation st <*x,y*> is RedSequence of R holds
[x,y] in R
let R be Relation; ::_thesis: ( <*x,y*> is RedSequence of R implies [x,y] in R )
set P = <*x,y*>;
A1: ( <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:44;
len <*x,y*> = 2 by FINSEQ_1:44;
then A2: ( 1 in dom <*x,y*> & 1 + 1 in dom <*x,y*> ) by FINSEQ_3:25;
assume <*x,y*> is RedSequence of R ; ::_thesis: [x,y] in R
hence [x,y] in R by A1, A2, REWRITE1:def_2; ::_thesis: verum
end;
begin
theorem Th9: :: REWRITE3:9
for E being non empty set
for w, u, v being Element of E ^omega st w = u ^ v holds
( len u <= len w & len v <= len w )
proof
let E be non empty set ; ::_thesis: for w, u, v being Element of E ^omega st w = u ^ v holds
( len u <= len w & len v <= len w )
let w, u, v be Element of E ^omega ; ::_thesis: ( w = u ^ v implies ( len u <= len w & len v <= len w ) )
assume w = u ^ v ; ::_thesis: ( len u <= len w & len v <= len w )
then len w = (len u) + (len v) by AFINSQ_1:17;
then ( (len w) + (len u) >= ((len u) + (len v)) + 0 & (len w) + (len v) >= ((len u) + (len v)) + 0 ) by XREAL_1:7;
hence ( len u <= len w & len v <= len w ) by XREAL_1:6; ::_thesis: verum
end;
theorem Th10: :: REWRITE3:10
for E being non empty set
for w, u, v being Element of E ^omega st w = u ^ v & u <> <%> E & v <> <%> E holds
( len u < len w & len v < len w )
proof
let E be non empty set ; ::_thesis: for w, u, v being Element of E ^omega st w = u ^ v & u <> <%> E & v <> <%> E holds
( len u < len w & len v < len w )
let w, u, v be Element of E ^omega ; ::_thesis: ( w = u ^ v & u <> <%> E & v <> <%> E implies ( len u < len w & len v < len w ) )
assume that
A1: w = u ^ v and
A2: u <> <%> E and
A3: v <> <%> E ; ::_thesis: ( len u < len w & len v < len w )
A4: len w = (len u) + (len v) by A1, AFINSQ_1:17;
then (len w) + (len u) > ((len u) + (len v)) + 0 by A2, XREAL_1:8;
hence ( len u < len w & len v < len w ) by A3, A4, XREAL_1:6, XREAL_1:8; ::_thesis: verum
end;
theorem :: REWRITE3:11
for E being non empty set
for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) holds
( w1 = w2 & v1 = v2 )
proof
let E be non empty set ; ::_thesis: for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) holds
( w1 = w2 & v1 = v2 )
let w1, v1, w2, v2 be Element of E ^omega ; ::_thesis: ( w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) implies ( w1 = w2 & v1 = v2 ) )
assume that
A1: w1 ^ v1 = w2 ^ v2 and
A2: ( len w1 = len w2 or len v1 = len v2 ) ; ::_thesis: ( w1 = w2 & v1 = v2 )
A3: (len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:17
.= (len w2) + (len v2) by AFINSQ_1:17 ;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_w1_holds_
w1_._k_=_w2_._k
let k be Nat; ::_thesis: ( k in dom w1 implies w1 . k = w2 . k )
assume A4: k in dom w1 ; ::_thesis: w1 . k = w2 . k
hence w1 . k = (w2 ^ v2) . k by A1, AFINSQ_1:def_3
.= w2 . k by A2, A3, A4, AFINSQ_1:def_3 ;
::_thesis: verum
end;
hence w1 = w2 by A2, A3, AFINSQ_1:8; ::_thesis: v1 = v2
hence v1 = v2 by A1, AFINSQ_1:28; ::_thesis: verum
end;
theorem Th12: :: REWRITE3:12
for E being non empty set
for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) holds
ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 )
proof
let E be non empty set ; ::_thesis: for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) holds
ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 )
let w1, v1, w2, v2 be Element of E ^omega ; ::_thesis: ( w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) implies ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) )
assume that
A1: w1 ^ v1 = w2 ^ v2 and
A2: ( len w1 <= len w2 or len v1 >= len v2 ) ; ::_thesis: ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 )
(len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:17
.= (len w2) + (len v2) by AFINSQ_1:17 ;
then ( len v1 >= len v2 implies ((len w1) + (len v1)) - (len v1) <= ((len w2) + (len v2)) - (len v2) ) by XREAL_1:13;
then consider u9 being XFinSequence such that
A3: w1 ^ u9 = w2 by A1, A2, AFINSQ_1:41;
reconsider u = u9 as Element of E ^omega by A3, FLANG_1:5;
take u ; ::_thesis: ( w1 ^ u = w2 & v1 = u ^ v2 )
thus w1 ^ u = w2 by A3; ::_thesis: v1 = u ^ v2
w2 ^ v2 = w1 ^ (u ^ v2) by A3, AFINSQ_1:27;
hence v1 = u ^ v2 by A1, AFINSQ_1:28; ::_thesis: verum
end;
theorem Th13: :: REWRITE3:13
for E being non empty set
for w1, v1, w2, v2 being Element of E ^omega holds
( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st
( w2 ^ u = w1 & v2 = u ^ v1 ) )
proof
let E be non empty set ; ::_thesis: for w1, v1, w2, v2 being Element of E ^omega holds
( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st
( w2 ^ u = w1 & v2 = u ^ v1 ) )
let w1, v1, w2, v2 be Element of E ^omega ; ::_thesis: ( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st
( w2 ^ u = w1 & v2 = u ^ v1 ) )
A1: ( len w1 < len w2 or len w1 >= len w2 ) ;
assume w1 ^ v1 = w2 ^ v2 ; ::_thesis: ( ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st
( w2 ^ u = w1 & v2 = u ^ v1 ) )
hence ( ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st
( w2 ^ u = w1 & v2 = u ^ v1 ) ) by A1, Th12; ::_thesis: verum
end;
begin
definition
let X be set ;
attrc2 is strict ;
struct transition-system over X -> 1-sorted ;
aggrtransition-system(# carrier, Tran #) -> transition-system over X;
sel Tran c2 -> Relation of [: the carrier of c2,X:], the carrier of c2;
end;
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be transition-system over F;
attrTS is deterministic means :Def1: :: REWRITE3:def 1
( the Tran of TS is Function & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) ) );
end;
:: deftheorem Def1 defines deterministic REWRITE3:def_1_:_
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( TS is deterministic iff ( the Tran of TS is Function & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) ) ) );
theorem Th14: :: REWRITE3:14
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic
let TS be transition-system over F; ::_thesis: ( dom the Tran of TS = {} implies TS is deterministic )
assume dom the Tran of TS = {} ; ::_thesis: TS is deterministic
then ( the Tran of TS = {} & ( for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) ) ) ;
hence TS is deterministic by Def1, RELAT_1:38; ::_thesis: verum
end;
registration
let E be non empty set ;
let F be Subset of (E ^omega);
cluster non empty finite strict deterministic for transition-system over F;
existence
ex b1 being transition-system 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;
take TS = transition-system(# the non empty finite set ,T #); ::_thesis: ( TS is strict & not TS is empty & TS is finite & TS is deterministic )
thus TS is strict ; ::_thesis: ( not TS is empty & TS is finite & TS is deterministic )
thus not TS is empty ; ::_thesis: ( TS is finite & TS is deterministic )
thus the carrier of TS is finite ; :: according to STRUCT_0:def_11 ::_thesis: TS is deterministic
thus TS is deterministic by Th14, RELAT_1:38; ::_thesis: verum
end;
end;
begin
definition
let X be set ;
let TS be transition-system over X;
let x, y, z be set ;
predx,y -->. z,TS means :Def2: :: REWRITE3:def 2
[[x,y],z] in the Tran of TS;
end;
:: deftheorem Def2 defines -->. REWRITE3:def_2_:_
for X being set
for TS being transition-system over X
for x, y, z being set holds
( x,y -->. z,TS iff [[x,y],z] in the Tran of TS );
theorem Th15: :: REWRITE3:15
for X, x, y, z being set
for TS being transition-system over X st x,y -->. z,TS holds
( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
proof
let X, x, y, z be set ; ::_thesis: for TS being transition-system over X st x,y -->. z,TS holds
( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
let TS be transition-system over X; ::_thesis: ( x,y -->. z,TS implies ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) )
assume x,y -->. z,TS ; ::_thesis: ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
then A1: [[x,y],z] in the Tran of TS by Def2;
then [x,y] in [: the carrier of TS,X:] by ZFMISC_1:87;
hence ( x in the carrier of TS & y in X & z in the carrier of TS ) by A1, ZFMISC_1:87; :: according to STRUCT_0:def_5 ::_thesis: ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
[x,y] in dom the Tran of TS by A1, XTUPLE_0:def_12;
hence ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) ) by XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: z in rng the Tran of TS
thus z in rng the Tran of TS by A1, XTUPLE_0:def_13; ::_thesis: verum
end;
theorem Th16: :: REWRITE3:16
for X1, X2, x, y, z being set
for TS1 being transition-system over X1
for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds
x,y -->. z,TS2
proof
let X1, X2, x, y, z be set ; ::_thesis: for TS1 being transition-system over X1
for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds
x,y -->. z,TS2
let TS1 be transition-system over X1; ::_thesis: for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds
x,y -->. z,TS2
let TS2 be transition-system over X2; ::_thesis: ( the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 implies x,y -->. z,TS2 )
assume A1: the Tran of TS1 = the Tran of TS2 ; ::_thesis: ( not x,y -->. z,TS1 or x,y -->. z,TS2 )
assume x,y -->. z,TS1 ; ::_thesis: x,y -->. z,TS2
then [[x,y],z] in the Tran of TS1 by Def2;
hence x,y -->. z,TS2 by A1, Def2; ::_thesis: verum
end;
theorem Th17: :: REWRITE3:17
for x, y, z1, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
proof
let x, y, z1, z2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2
let TS be transition-system over F; ::_thesis: ( the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS implies z1 = z2 )
assume A1: the Tran of TS is Function ; ::_thesis: ( not x,y -->. z1,TS or not x,y -->. z2,TS or z1 = z2 )
assume ( x,y -->. z1,TS & x,y -->. z2,TS ) ; ::_thesis: z1 = z2
then ( [[x,y],z1] in the Tran of TS & [[x,y],z2] in the Tran of TS ) by Def2;
hence z1 = z2 by A1, FUNCT_1:def_1; ::_thesis: verum
end;
theorem :: REWRITE3:18
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x, <%> E -->. y,TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x, <%> E -->. y,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x, <%> E -->. y,TS
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x, <%> E -->. y,TS
let TS be transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies not x, <%> E -->. y,TS )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: not x, <%> E -->. y,TS
assume x, <%> E -->. y,TS ; ::_thesis: contradiction
then [[x,(<%> E)],y] in the Tran of TS by Def2;
then [x,(<%> E)] in dom the Tran of TS by XTUPLE_0:def_12;
hence contradiction by A1, XTUPLE_0:def_13; ::_thesis: verum
end;
theorem Th19: :: REWRITE3:19
for x, z1, z2 being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
proof
let x, z1, z2 be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,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: for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let F be Subset of (E ^omega); ::_thesis: for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let TS be deterministic transition-system over F; ::_thesis: ( u <> v & x,u -->. z1,TS & x,v -->. z2,TS implies for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) )
assume that
A1: u <> v and
A2: x,u -->. z1,TS and
A3: x,v -->. z2,TS ; ::_thesis: for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
x in TS by A2, Th15;
then reconsider x = x as Element of TS by STRUCT_0:def_5;
[[x,v],z2] in the Tran of TS by A3, Def2;
then A4: [x,v] in dom the Tran of TS by XTUPLE_0:def_12;
[[x,u],z1] in the Tran of TS by A2, Def2;
then [x,u] in dom the Tran of TS by XTUPLE_0:def_12;
hence for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) by A1, A4, Def1; ::_thesis: verum
end;
begin
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be transition-system over F;
let x1, x2, y1, y2 be set ;
predx1,x2 ==>. y1,y2,TS means :Def3: :: REWRITE3:def 3
ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v );
end;
:: deftheorem Def3 defines ==>. REWRITE3:def_3_:_
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F
for x1, x2, y1, y2 being set holds
( x1,x2 ==>. y1,y2,TS iff ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) );
theorem Th20: :: REWRITE3:20
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
let TS be transition-system over F; ::_thesis: ( x1,x2 ==>. y1,y2,TS implies ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) )
assume x1,x2 ==>. y1,y2,TS ; ::_thesis: ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
then ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) by Def3;
hence ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) by Th15; ::_thesis: verum
end;
theorem Th21: :: REWRITE3:21
for x1, x2, y1, y2 being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let TS1 be transition-system over F1; ::_thesis: for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let TS2 be transition-system over F2; ::_thesis: ( the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 implies x1,x2 ==>. y1,y2,TS2 )
assume that
A1: the Tran of TS1 = the Tran of TS2 and
A2: x1,x2 ==>. y1,y2,TS1 ; ::_thesis: x1,x2 ==>. y1,y2,TS2
consider v, w being Element of E ^omega such that
A3: ( v = y2 & x1,w -->. y1,TS1 & x2 = w ^ v ) by A2, Def3;
take v ; :: according to REWRITE3:def_3 ::_thesis: ex w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
take w ; ::_thesis: ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
thus ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v ) by A1, A3, Th16; ::_thesis: verum
end;
theorem Th22: :: REWRITE3:22
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x,u ==>. y,v,TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let TS be transition-system over F; ::_thesis: ( x,u ==>. y,v,TS implies ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v ) )
assume x,u ==>. y,v,TS ; ::_thesis: ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
then consider v1, w being Element of E ^omega such that
A1: ( v1 = v & x,w -->. y,TS & u = w ^ v1 ) by Def3;
take w ; ::_thesis: ( x,w -->. y,TS & u = w ^ v )
thus ( x,w -->. y,TS & u = w ^ v ) by A1; ::_thesis: verum
end;
theorem Th23: :: REWRITE3:23
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F holds
( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )
let TS be transition-system over F; ::_thesis: ( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )
thus ( x,y -->. z,TS implies x,y ==>. z, <%> E,TS ) ::_thesis: ( x,y ==>. z, <%> E,TS implies x,y -->. z,TS )
proof
assume A1: x,y -->. z,TS ; ::_thesis: x,y ==>. z, <%> E,TS
then y in F by Th15;
then reconsider w = y as Element of E ^omega ;
w = w ^ {} ;
hence x,y ==>. z, <%> E,TS by A1, Def3; ::_thesis: verum
end;
B: for w being Element of E ^omega holds w ^ {} = w ;
assume x,y ==>. z, <%> E,TS ; ::_thesis: x,y -->. z,TS
then ex v, w being Element of E ^omega st
( v = <%> E & x,w -->. z,TS & y = w ^ v ) by Def3;
hence x,y -->. z,TS by B; ::_thesis: verum
end;
theorem Th24: :: REWRITE3:24
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let TS be transition-system over F; ::_thesis: ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
thus ( x,v -->. y,TS implies x,v ^ w ==>. y,w,TS ) by Def3; ::_thesis: ( x,v ^ w ==>. y,w,TS implies x,v -->. y,TS )
assume x,v ^ w ==>. y,w,TS ; ::_thesis: x,v -->. y,TS
then ex u being Element of E ^omega st
( x,u -->. y,TS & v ^ w = u ^ w ) by Th22;
hence x,v -->. y,TS by AFINSQ_1:28; ::_thesis: verum
end;
theorem Th25: :: REWRITE3:25
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
x,u ^ w ==>. y,v ^ w,TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
x,u ^ w ==>. y,v ^ w,TS
let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
x,u ^ w ==>. y,v ^ w,TS
let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
x,u ^ w ==>. y,v ^ w,TS
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x,u ==>. y,v,TS holds
x,u ^ w ==>. y,v ^ w,TS
let TS be transition-system over F; ::_thesis: ( x,u ==>. y,v,TS implies x,u ^ w ==>. y,v ^ w,TS )
assume x,u ==>. y,v,TS ; ::_thesis: x,u ^ w ==>. y,v ^ w,TS
then consider u1 being Element of E ^omega such that
A1: x,u1 -->. y,TS and
A2: u = u1 ^ v by Th22;
u ^ w = u1 ^ (v ^ w) by A2, AFINSQ_1:27;
hence x,u ^ w ==>. y,v ^ w,TS by A1, Def3; ::_thesis: verum
end;
theorem Th26: :: REWRITE3:26
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
len u >= len v
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
len u >= len v
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
len u >= len v
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
len u >= len v
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x,u ==>. y,v,TS holds
len u >= len v
let TS be transition-system over F; ::_thesis: ( x,u ==>. y,v,TS implies len u >= len v )
assume x,u ==>. y,v,TS ; ::_thesis: len u >= len v
then ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v ) by Th22;
hence len u >= len v by Th9; ::_thesis: verum
end;
theorem Th27: :: REWRITE3:27
for x1, x2, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
proof
let x1, x2, y1, z, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
let TS be transition-system over F; ::_thesis: ( the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS implies y1 = y2 )
assume A1: the Tran of TS is Function ; ::_thesis: ( not x1,x2 ==>. y1,z,TS or not x1,x2 ==>. y2,z,TS or y1 = y2 )
assume that
A2: x1,x2 ==>. y1,z,TS and
A3: x1,x2 ==>. y2,z,TS ; ::_thesis: y1 = y2
consider v1, w1 being Element of E ^omega such that
A4: v1 = z and
A5: x1,w1 -->. y1,TS and
A6: x2 = w1 ^ v1 by A2, Def3;
consider v2, w2 being Element of E ^omega such that
A7: v2 = z and
A8: x1,w2 -->. y2,TS and
A9: x2 = w2 ^ v2 by A3, Def3;
w1 = w2 by A4, A6, A7, A9, AFINSQ_1:28;
hence y1 = y2 by A1, A5, A8, Th17; ::_thesis: verum
end;
theorem Th28: :: REWRITE3:28
for x, z, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
proof
let x, z, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
let TS be transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies not x,z ==>. y,z,TS )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: not x,z ==>. y,z,TS
assume x,z ==>. y,z,TS ; ::_thesis: contradiction
then consider v, w being Element of E ^omega such that
A2: v = z and
A3: x,w -->. y,TS and
A4: z = w ^ v by Def3;
[[x,w],y] in the Tran of TS by A3, Def2;
then A5: [x,w] in dom the Tran of TS by XTUPLE_0:def_12;
w = <%> E by A2, A4, FLANG_2:4;
hence contradiction by A1, A5, XTUPLE_0:def_13; ::_thesis: verum
end;
theorem Th29: :: REWRITE3:29
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds
len u > len v
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds
len u > len v
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds
len u > len v
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds
len u > len v
let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds
len u > len v
let TS be transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS implies len u > len v )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not x,u ==>. y,v,TS or len u > len v )
assume A2: x,u ==>. y,v,TS ; ::_thesis: len u > len v
then consider w being Element of E ^omega such that
A3: x,w -->. y,TS and
A4: u = w ^ v by Th22;
A5: w in rng (dom the Tran of TS) by A3, Th15;
percases ( v = <%> E or v <> <%> E ) ;
supposeA6: v = <%> E ; ::_thesis: len u > len v
then u <> <%> E by A1, A2, Th28;
then len u > 0 ;
hence len u > len v by A6; ::_thesis: verum
end;
suppose v <> <%> E ; ::_thesis: len u > len v
hence len u > len v by A1, A4, A5, Th10; ::_thesis: verum
end;
end;
end;
theorem Th30: :: REWRITE3:30
for x1, x2, y1, z1, y2, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
proof
let x1, x2, y1, z1, y2, z2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
let F be Subset of (E ^omega); ::_thesis: for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
let TS be deterministic transition-system over F; ::_thesis: ( x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS implies ( y1 = y2 & z1 = z2 ) )
assume that
A1: x1,x2 ==>. y1,z1,TS and
A2: x1,x2 ==>. y2,z2,TS ; ::_thesis: ( y1 = y2 & z1 = z2 )
consider v2, w2 being Element of E ^omega such that
A3: v2 = z2 and
A4: x1,w2 -->. y2,TS and
A5: x2 = w2 ^ v2 by A2, Def3;
consider v1, w1 being Element of E ^omega such that
A6: v1 = z1 and
A7: x1,w1 -->. y1,TS and
A8: x2 = w1 ^ v1 by A1, Def3;
A9: the Tran of TS is Function by Def1;
( ex u9 being Element of E ^omega st
( w1 ^ u9 = w2 & v1 = u9 ^ v2 ) or ex u9 being Element of E ^omega st
( w2 ^ u9 = w1 & v2 = u9 ^ v1 ) ) by A8, A5, Th13;
then w1 = w2 by A7, A4, Th19;
then v1 = v2 by A8, A5, AFINSQ_1:28;
hence ( y1 = y2 & z1 = z2 ) by A1, A2, A6, A3, A9, Th27; ::_thesis: verum
end;
begin
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
func ==>.-relation TS -> Relation of [: the carrier of TS,(E ^omega):] means :Def4: :: REWRITE3:def 4
for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in it iff x1,x2 ==>. y1,y2,TS );
existence
ex b1 being Relation of [: the carrier of TS,(E ^omega):] st
for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS )
proof
defpred S1[ Element of [: the carrier of TS,(E ^omega):], Element of [: the carrier of TS,(E ^omega):]] means ex x1, x2, y1, y2 being set st
( [x1,x2] = $1 & [y1,y2] = $2 & x1,x2 ==>. y1,y2,TS );
consider R being Relation of [: the carrier of TS,(E ^omega):] such that
A1: for s, t being Element of [: the carrier of TS,(E ^omega):] holds
( [s,t] in R iff S1[s,t] ) from RELSET_1:sch_2();
take R ; ::_thesis: for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS )
now__::_thesis:_for_x1,_x2,_y1,_y2_being_set_holds_
(_(_x1,x2_==>._y1,y2,TS_implies_[[x1,x2],[y1,y2]]_in_R_)_&_(_[[x1,x2],[y1,y2]]_in_R_implies_x1,x2_==>._y1,y2,TS_)_)
let x1, x2, y1, y2 be set ; ::_thesis: ( ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) & ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS ) )
set s = [x1,x2];
set t = [y1,y2];
A2: ( dom R c= [: the carrier of TS,(E ^omega):] & rng R c= [: the carrier of TS,(E ^omega):] ) by RELAT_1:def_18, RELAT_1:def_19;
thus ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) ::_thesis: ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS )
proof
assume A3: x1,x2 ==>. y1,y2,TS ; ::_thesis: [[x1,x2],[y1,y2]] in R
then y1 in TS by Th20;
then A4: y1 in the carrier of TS by STRUCT_0:def_5;
x1 in TS by A3, Th20;
then A5: x1 in the carrier of TS by STRUCT_0:def_5;
y2 in E ^omega by A3, Th20;
then A6: [y1,y2] in [: the carrier of TS,(E ^omega):] by A4, ZFMISC_1:def_2;
x2 in E ^omega by A3, Th20;
then [x1,x2] in [: the carrier of TS,(E ^omega):] by A5, ZFMISC_1:def_2;
hence [[x1,x2],[y1,y2]] in R by A1, A3, A6; ::_thesis: verum
end;
assume A7: [[x1,x2],[y1,y2]] in R ; ::_thesis: x1,x2 ==>. y1,y2,TS
then ( [x1,x2] in dom R & [y1,y2] in rng R ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
then consider x19, x29, y19, y29 being set such that
A8: [x19,x29] = [x1,x2] and
A9: [y19,y29] = [y1,y2] and
A10: x19,x29 ==>. y19,y29,TS by A1, A7, A2;
A11: y1 = y19 by A9, XTUPLE_0:1;
( x1 = x19 & x2 = x29 ) by A8, XTUPLE_0:1;
hence x1,x2 ==>. y1,y2,TS by A9, A10, A11, XTUPLE_0:1; ::_thesis: verum
end;
hence for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of [: the carrier of TS,(E ^omega):] st ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b2 iff x1,x2 ==>. y1,y2,TS ) ) holds
b1 = b2
proof
let R1, R2 be Relation of [: the carrier of TS,(E ^omega):]; ::_thesis: ( ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS ) ) implies R1 = R2 )
assume that
A12: for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS ) and
A13: for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS ) ; ::_thesis: R1 = R2
now__::_thesis:_for_s,_t_being_Element_of_[:_the_carrier_of_TS,(E_^omega):]_holds_
(_[s,t]_in_R1_iff_[s,t]_in_R2_)
let s, t be Element of [: the carrier of TS,(E ^omega):]; ::_thesis: ( [s,t] in R1 iff [s,t] in R2 )
consider x, u being set such that
A14: x in the carrier of TS and
A15: u in E ^omega and
A16: s = [x,u] by ZFMISC_1:def_2;
reconsider u = u as Element of E ^omega by A15;
reconsider x = x as Element of TS by A14;
consider y, v being set such that
A17: y in the carrier of TS and
A18: v in E ^omega and
A19: t = [y,v] by ZFMISC_1:def_2;
reconsider v = v as Element of E ^omega by A18;
reconsider y = y as Element of TS by A17;
( [s,t] in R1 iff x,u ==>. y,v,TS ) by A12, A16, A19;
hence ( [s,t] in R1 iff [s,t] in R2 ) by A13, A16, A19; ::_thesis: verum
end;
hence R1 = R2 by RELSET_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines ==>.-relation REWRITE3:def_4_:_
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 Relation of [: the carrier of TS,(E ^omega):] holds
( b4 = ==>.-relation TS iff for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b4 iff x1,x2 ==>. y1,y2,TS ) );
theorem Th31: :: REWRITE3:31
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] )
proof
let x, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] )
let TS be non empty transition-system over F; ::_thesis: ( [x,y] in ==>.-relation TS implies ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] ) )
assume A1: [x,y] in ==>.-relation TS ; ::_thesis: ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] )
then y in [: the carrier of TS,(E ^omega):] by ZFMISC_1:87;
then A2: ex y1, y2 being set st
( y1 in the carrier of TS & y2 in E ^omega & y = [y1,y2] ) by ZFMISC_1:def_2;
x in [: the carrier of TS,(E ^omega):] by A1, ZFMISC_1:87;
then ex x1, x2 being set st
( x1 in the carrier of TS & x2 in E ^omega & x = [x1,x2] ) by ZFMISC_1:def_2;
hence ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] & y = [t,w] ) by A2; ::_thesis: verum
end;
theorem Th32: :: REWRITE3:32
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
let TS be non empty transition-system over F; ::_thesis: ( [[x1,x2],[y1,y2]] in ==>.-relation TS implies ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) )
assume [[x1,x2],[y1,y2]] in ==>.-relation TS ; ::_thesis: ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
then x1,x2 ==>. y1,y2,TS by Def4;
hence ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) by Th20; ::_thesis: verum
end;
theorem Th33: :: REWRITE3:33
for x being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
proof
let x be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
let TS be non empty transition-system over F; ::_thesis: ( x in ==>.-relation TS implies ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] )
assume A1: x in ==>.-relation TS ; ::_thesis: ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
then consider y, z being set such that
A2: x = [y,z] by RELAT_1:def_1;
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( y = [s,v] & z = [t,w] ) by A1, A2, Th31;
hence ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] by A2; ::_thesis: verum
end;
theorem Th34: :: REWRITE3:34
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
proof
let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let TS2 be non empty transition-system over F2; ::_thesis: ( the Tran of TS1 = the Tran of TS2 implies ==>.-relation TS1 = ==>.-relation TS2 )
assume A1: the Tran of TS1 = the Tran of TS2 ; ::_thesis: ==>.-relation TS1 = ==>.-relation TS2
A2: now__::_thesis:_for_x_being_set_st_x_in_==>.-relation_TS1_holds_
x_in_==>.-relation_TS2
let x be set ; ::_thesis: ( x in ==>.-relation TS1 implies x in ==>.-relation TS2 )
assume A3: x in ==>.-relation TS1 ; ::_thesis: x in ==>.-relation TS2
then consider s, t being Element of TS1, v, w being Element of E ^omega such that
A4: x = [[s,v],[t,w]] by Th33;
s,v ==>. t,w,TS1 by A3, A4, Def4;
then s,v ==>. t,w,TS2 by A1, Th21;
hence x in ==>.-relation TS2 by A4, Def4; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_==>.-relation_TS2_holds_
x_in_==>.-relation_TS1
let x be set ; ::_thesis: ( x in ==>.-relation TS2 implies x in ==>.-relation TS1 )
assume A5: x in ==>.-relation TS2 ; ::_thesis: x in ==>.-relation TS1
then consider s, t being Element of TS2, v, w being Element of E ^omega such that
A6: x = [[s,v],[t,w]] by Th33;
s,v ==>. t,w,TS2 by A5, A6, Def4;
then s,v ==>. t,w,TS1 by A1, Th21;
hence x in ==>.-relation TS1 by A6, Def4; ::_thesis: verum
end;
hence ==>.-relation TS1 = ==>.-relation TS2 by A2, TARSKI:1; ::_thesis: verum
end;
theorem Th35: :: REWRITE3:35
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v )
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v )
let TS be non empty transition-system over F; ::_thesis: ( [[x1,x2],[y1,y2]] in ==>.-relation TS implies ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) )
assume [[x1,x2],[y1,y2]] in ==>.-relation TS ; ::_thesis: ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v )
then x1,x2 ==>. y1,y2,TS by Def4;
hence ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) by Def3; ::_thesis: verum
end;
theorem Th36: :: REWRITE3:36
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let TS be non empty transition-system over F; ::_thesis: ( [[x,u],[y,v]] in ==>.-relation TS implies ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v ) )
assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
then x,u ==>. y,v,TS by Def4;
hence ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v ) by Th22; ::_thesis: verum
end;
theorem Th37: :: REWRITE3:37
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS )
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds
( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS )
let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS )
thus ( x,y -->. z,TS implies [[x,y],[z,(<%> E)]] in ==>.-relation TS ) ::_thesis: ( [[x,y],[z,(<%> E)]] in ==>.-relation TS implies x,y -->. z,TS )
proof
assume x,y -->. z,TS ; ::_thesis: [[x,y],[z,(<%> E)]] in ==>.-relation TS
then x,y ==>. z, <%> E,TS by Th23;
hence [[x,y],[z,(<%> E)]] in ==>.-relation TS by Def4; ::_thesis: verum
end;
assume [[x,y],[z,(<%> E)]] in ==>.-relation TS ; ::_thesis: x,y -->. z,TS
then x,y ==>. z, <%> E,TS by Def4;
hence x,y -->. z,TS by Th23; ::_thesis: verum
end;
theorem Th38: :: REWRITE3:38
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds
( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
thus ( x,v -->. y,TS implies [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) ::_thesis: ( [[x,(v ^ w)],[y,w]] in ==>.-relation TS implies x,v -->. y,TS )
proof
assume x,v -->. y,TS ; ::_thesis: [[x,(v ^ w)],[y,w]] in ==>.-relation TS
then x,v ^ w ==>. y,w,TS by Th24;
hence [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Def4; ::_thesis: verum
end;
assume [[x,(v ^ w)],[y,w]] in ==>.-relation TS ; ::_thesis: x,v -->. y,TS
then x,v ^ w ==>. y,w,TS by Def4;
hence x,v -->. y,TS by Th24; ::_thesis: verum
end;
theorem :: REWRITE3:39
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
[[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
[[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
[[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
[[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
[[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
let TS be non empty transition-system over F; ::_thesis: ( [[x,u],[y,v]] in ==>.-relation TS implies [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS )
assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
then x,u ==>. y,v,TS by Def4;
then x,u ^ w ==>. y,v ^ w,TS by Th25;
hence [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS by Def4; ::_thesis: verum
end;
theorem :: REWRITE3:40
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
len u >= len v
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
len u >= len v
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
len u >= len v
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
len u >= len v
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
len u >= len v
let TS be non empty transition-system over F; ::_thesis: ( [[x,u],[y,v]] in ==>.-relation TS implies len u >= len v )
assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: len u >= len v
then x,u ==>. y,v,TS by Def4;
hence len u >= len v by Th26; ::_thesis: verum
end;
theorem :: REWRITE3:41
for x, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
proof
let x, y1, z, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
let TS be non empty transition-system over F; ::_thesis: ( the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS implies y1 = y2 )
assume A1: the Tran of TS is Function ; ::_thesis: ( not [x,[y1,z]] in ==>.-relation TS or not [x,[y2,z]] in ==>.-relation TS or y1 = y2 )
assume that
A2: [x,[y1,z]] in ==>.-relation TS and
A3: [x,[y2,z]] in ==>.-relation TS ; ::_thesis: y1 = y2
consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that
A4: x = [s,v] and
[y1,z] = [t,w] by A2, Th31;
( s,v ==>. y1,z,TS & s,v ==>. y2,z,TS ) by A2, A3, A4, Def4;
hence y1 = y2 by A1, Th27; ::_thesis: verum
end;
theorem :: REWRITE3:42
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS implies len u > len v )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not [[x,u],[y,v]] in ==>.-relation TS or len u > len v )
assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: len u > len v
then x,u ==>. y,v,TS by Def4;
hence len u > len v by A1, Th29; ::_thesis: verum
end;
theorem Th43: :: REWRITE3:43
for x, z, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not [[x,z],[y,z]] in ==>.-relation TS
proof
let x, z, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not [[x,z],[y,z]] in ==>.-relation TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not [[x,z],[y,z]] in ==>.-relation TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not [[x,z],[y,z]] in ==>.-relation TS
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies not [[x,z],[y,z]] in ==>.-relation TS )
assume not <%> E in rng (dom the Tran of TS) ; ::_thesis: not [[x,z],[y,z]] in ==>.-relation TS
then not x,z ==>. y,z,TS by Th28;
hence not [[x,z],[y,z]] in ==>.-relation TS by Def4; ::_thesis: verum
end;
theorem Th44: :: REWRITE3:44
for x, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS implies y1 = y2 )
assume A1: TS is deterministic ; ::_thesis: ( not [x,y1] in ==>.-relation TS or not [x,y2] in ==>.-relation TS or y1 = y2 )
assume that
A2: [x,y1] in ==>.-relation TS and
A3: [x,y2] in ==>.-relation TS ; ::_thesis: y1 = y2
consider s2 being Element of TS, v2 being Element of E ^omega , t2 being Element of TS, w2 being Element of E ^omega such that
x = [s2,v2] and
A4: y2 = [t2,w2] by A3, Th31;
consider s1 being Element of TS, v1 being Element of E ^omega , t1 being Element of TS, w1 being Element of E ^omega such that
A5: x = [s1,v1] and
A6: y1 = [t1,w1] by A2, Th31;
A7: s1,v1 ==>. t1,w1,TS by A2, A5, A6, Def4;
A8: s1,v1 ==>. t2,w2,TS by A3, A5, A4, Def4;
then t1 = t2 by A1, A7, Th30;
hence y1 = y2 by A1, A6, A4, A7, A8, Th30; ::_thesis: verum
end;
theorem :: REWRITE3:45
for x, y1, z1, y2, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
proof
let x, y1, z1, y2, z2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS implies ( y1 = y2 & z1 = z2 ) )
assume A1: TS is deterministic ; ::_thesis: ( not [x,[y1,z1]] in ==>.-relation TS or not [x,[y2,z2]] in ==>.-relation TS or ( y1 = y2 & z1 = z2 ) )
assume ( [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS ) ; ::_thesis: ( y1 = y2 & z1 = z2 )
then [y1,z1] = [y2,z2] by A1, Th44;
hence ( y1 = y2 & z1 = z2 ) by XTUPLE_0:1; ::_thesis: verum
end;
theorem :: REWRITE3:46
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
==>.-relation TS is Function-like
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
==>.-relation TS is Function-like
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds
==>.-relation TS is Function-like
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies ==>.-relation TS is Function-like )
assume TS is deterministic ; ::_thesis: ==>.-relation TS is Function-like
then for x, y, z being set st [x,y] in ==>.-relation TS & [x,z] in ==>.-relation TS holds
y = z by Th44;
hence ==>.-relation TS is Function-like by FUNCT_1:def_1; ::_thesis: verum
end;
begin
definition
let x be set ;
let E be non empty set ;
func dim2 (x,E) -> Element of E ^omega equals :Def5: :: REWRITE3:def 5
x `2 if ex y being set ex u being Element of E ^omega st x = [y,u]
otherwise {} ;
coherence
( ( ex y being set ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) & ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) )
proof
thus ( ex y being set ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) by MCART_1:7; ::_thesis: ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega )
{} = <%> E ;
hence ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) ; ::_thesis: verum
end;
consistency
for b1 being Element of E ^omega holds verum ;
end;
:: deftheorem Def5 defines dim2 REWRITE3:def_5_:_
for x being set
for E being non empty set holds
( ( ex y being set ex u being Element of E ^omega st x = [y,u] implies dim2 (x,E) = x `2 ) & ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies dim2 (x,E) = {} ) );
theorem Th47: :: REWRITE3:47
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )
let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )
let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] ) )
assume ( k in dom P & k + 1 in dom P ) ; ::_thesis: ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] )
then [(P . k),(P . (k + 1))] in ==>.-relation TS by REWRITE1:def_2;
hence ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th31; ::_thesis: verum
end;
theorem Th48: :: REWRITE3:48
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) )
assume ( k in dom P & k + 1 in dom P ) ; ::_thesis: ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
then ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th47;
hence ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) by MCART_1:8; ::_thesis: verum
end;
theorem Th49: :: REWRITE3:49
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) )
assume ( k in dom P & k + 1 in dom P ) ; ::_thesis: ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
then A1: [(P . k),(P . (k + 1))] in ==>.-relation TS by REWRITE1:def_2;
then consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that
A2: ( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th31;
A3: ( s in dom (dom the Tran of TS) & t in rng the Tran of TS ) by A1, A2, Th32;
A4: ( v in E ^omega & w in E ^omega ) ;
( s in TS & t in TS ) by A1, A2, Th32;
hence ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) by A2, A4, A3, MCART_1:7; ::_thesis: verum
end;
theorem :: REWRITE3:50
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
proof
let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 implies for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 )
assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; ::_thesis: for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let P be RedSequence of ==>.-relation TS1; ::_thesis: P is RedSequence of ==>.-relation TS2
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_P_&_i_+_1_in_dom_P_holds_
[(P_._i),(P_._(i_+_1))]_in_==>.-relation_TS2
let i be Element of NAT ; ::_thesis: ( i in dom P & i + 1 in dom P implies [(P . i),(P . (i + 1))] in ==>.-relation TS2 )
assume ( i in dom P & i + 1 in dom P ) ; ::_thesis: [(P . i),(P . (i + 1))] in ==>.-relation TS2
then [(P . i),(P . (i + 1))] in ==>.-relation TS1 by REWRITE1:def_2;
hence [(P . i),(P . (i + 1))] in ==>.-relation TS2 by A1, Th34; ::_thesis: verum
end;
len P > 0 ;
hence P is RedSequence of ==>.-relation TS2 by A2, REWRITE1:def_2; ::_thesis: verum
end;
theorem Th51: :: REWRITE3:51
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2
let P be RedSequence of ==>.-relation TS; ::_thesis: ( ex x being set ex u being Element of E ^omega st P . 1 = [x,u] implies for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2 )
given x being set , u being Element of E ^omega such that A1: P . 1 = [x,u] ; ::_thesis: for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2
let k be Nat; ::_thesis: ( k in dom P implies dim2 ((P . k),E) = (P . k) `2 )
assume A2: k in dom P ; ::_thesis: dim2 ((P . k),E) = (P . k) `2
percases ( k > 1 or k <= 1 ) ;
supposeA3: k > 1 ; ::_thesis: dim2 ((P . k),E) = (P . k) `2
A4: k <= len P by A2, FINSEQ_3:25;
consider l being Nat such that
A5: k = l + 1 by A3, NAT_1:6;
l <= k by A5, NAT_1:11;
then A6: l <= len P by A4, XXREAL_0:2;
l >= 1 by A3, A5, NAT_1:19;
then l in dom P by A6, FINSEQ_3:25;
then [(P . l),(P . k)] in ==>.-relation TS by A2, A5, REWRITE1:def_2;
then A7: P . k in rng (==>.-relation TS) by XTUPLE_0:def_13;
rng (==>.-relation TS) c= [: the carrier of TS,(E ^omega):] by RELAT_1:def_19;
then ex x1, y1 being set st
( x1 in the carrier of TS & y1 in E ^omega & P . k = [x1,y1] ) by A7, ZFMISC_1:def_2;
hence dim2 ((P . k),E) = (P . k) `2 by Def5; ::_thesis: verum
end;
supposeA8: k <= 1 ; ::_thesis: dim2 ((P . k),E) = (P . k) `2
k >= 1 by A2, FINSEQ_3:25;
then k = 1 by A8, XXREAL_0:1;
hence dim2 ((P . k),E) = (P . k) `2 by A1, Def5; ::_thesis: verum
end;
end;
end;
theorem Th52: :: REWRITE3:52
for y 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 P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
proof
let y 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 P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
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 P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
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 P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . (len P) = [y,w] implies for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w )
assume P . (len P) = [y,w] ; ::_thesis: for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
then A1: (P . (len P)) `2 = {} ^ w by MCART_1:7
.= (<%> E) ^ w ;
defpred S1[ Nat] means ( (len P) - $1 in dom P implies ex u being Element of E ^omega st (P . ((len P) - $1)) `2 = u ^ w );
A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(len_P)_-_(k_+_1)_in_dom_P_implies_ex_u_being_Element_of_E_^omega_st_(P_._((len_P)_-_(k_+_1)))_`2_=_u_^_w_)
set len2 = (len P) - k;
set len1 = (len P) - (k + 1);
A4: ((len P) - (k + 1)) + 1 = (len P) - k ;
assume A5: (len P) - (k + 1) in dom P ; ::_thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w
thus ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w ::_thesis: verum
proof
percases ( (len P) - k in dom P or not (len P) - k in dom P ) ;
supposeA6: (len P) - k in dom P ; ::_thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w
then consider u1 being Element of E ^omega such that
A7: (P . ((len P) - k)) `2 = u1 ^ w by A3;
A8: [(P . ((len P) - (k + 1))),(P . ((len P) - k))] in ==>.-relation TS by A5, A4, A6, REWRITE1:def_2;
then consider x being Element of TS, v1 being Element of E ^omega , y being Element of TS, v2 being Element of E ^omega such that
A9: P . ((len P) - (k + 1)) = [x,v1] and
A10: P . ((len P) - k) = [y,v2] by Th31;
x,v1 ==>. y,v2,TS by A8, A9, A10, Def4;
then consider u2 being Element of E ^omega such that
x,u2 -->. y,TS and
A11: v1 = u2 ^ v2 by Th22;
take u2 ^ u1 ; ::_thesis: (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w
(P . ((len P) - (k + 1))) `2 = u2 ^ v2 by A9, A11, MCART_1:7
.= u2 ^ (u1 ^ w) by A7, A10, MCART_1:7
.= (u2 ^ u1) ^ w by AFINSQ_1:27 ;
hence (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w ; ::_thesis: verum
end;
suppose not (len P) - k in dom P ; ::_thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w
then (len P) - (k + 1) = (len P) - 0 by A5, A4, Th3;
hence ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w ; ::_thesis: verum
end;
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A12: S1[ 0 ] by A1;
A13: for k being Nat holds S1[k] from NAT_1:sch_2(A12, A2);
hereby ::_thesis: verum
let k be Nat; ::_thesis: ( k in dom P implies ex u being Element of E ^omega st (P . k) `2 = u ^ w )
assume A14: k in dom P ; ::_thesis: ex u being Element of E ^omega st (P . k) `2 = u ^ w
k <= len P by A14, FINSEQ_3:25;
then consider l being Nat such that
A15: k + l = len P by NAT_1:10;
(k + l) - l = (len P) - l by A15;
hence ex u being Element of E ^omega st (P . k) `2 = u ^ w by A13, A14; ::_thesis: verum
end;
end;
theorem Th53: :: REWRITE3:53
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,v] & P . (len P) = [y,w] implies ex u being Element of E ^omega st v = u ^ w )
assume that
A1: P . 1 = [x,v] and
A2: P . (len P) = [y,w] ; ::_thesis: ex u being Element of E ^omega st v = u ^ w
0 + 1 <= len P by NAT_1:8;
then 1 in dom P by FINSEQ_3:25;
then consider u being Element of E ^omega such that
A3: (P . 1) `2 = u ^ w by A2, Th52;
take u ; ::_thesis: v = u ^ w
thus v = u ^ w by A1, A3, MCART_1:7; ::_thesis: verum
end;
theorem Th54: :: REWRITE3:54
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
proof
let x, y be set ; ::_thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let E be non empty set ; ::_thesis: for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS
for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = $1 holds
for k being Nat st k in dom P holds
(P . k) `2 = 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_P_being_RedSequence_of_==>.-relation_TS
for_x,_y_being_set_st_P_._1_=_[x,u]_&_P_._(len_P)_=_[y,u]_&_len_P_=_k_+_1_holds_
for_l_being_Nat_st_l_in_dom_P_holds_
(P_._l)_`2_=_u
let P be RedSequence of ==>.-relation TS; ::_thesis: for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
for l being Nat st b6 in dom l holds
(l . b6) `2 = u
let x, y be set ; ::_thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies for l being Nat st b4 in dom l holds
(l . b4) `2 = u )
assume that
A3: P . 1 = [x,u] and
A4: P . (len P) = [y,u] and
A5: len P = k + 1 ; ::_thesis: for l being Nat st b4 in dom l holds
(l . b4) `2 = u
percases ( k = 0 or k <> 0 ) ;
supposeA6: k = 0 ; ::_thesis: for l being Nat st b4 in dom l holds
(l . b4) `2 = u
hereby ::_thesis: verum
let l be Nat; ::_thesis: ( l in dom P implies (P . l) `2 = u )
assume l in dom P ; ::_thesis: (P . l) `2 = u
then ( l <= 1 & 1 <= l ) by A5, A6, FINSEQ_3:25;
then l = 1 by XXREAL_0:1;
hence (P . l) `2 = u by A3, MCART_1:7; ::_thesis: verum
end;
end;
suppose k <> 0 ; ::_thesis: for l being Nat st b4 in dom l holds
(l . b4) `2 = u
then A7: k + 1 > 0 + 1 by XREAL_1:6;
then A8: 1 in dom P by A5, FINSEQ_3:25;
len P >= 1 + 1 by A5, A7, NAT_1:8;
then A9: 1 + 1 in dom P by FINSEQ_3:25;
then A10: P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A8, Th48;
reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by A8, A9, Th49;
==>.-relation TS reduces P . 1,P . (1 + 1) by A8, A9, REWRITE1:17;
then ex P9 being RedSequence of ==>.-relation TS st
( P9 . 1 = P . 1 & P9 . (len P9) = P . (1 + 1) ) by REWRITE1:def_3;
then consider w being Element of E ^omega such that
A11: u = w ^ u1 by A3, A10, Th53;
A12: len <*(P . 1)*> = 1 by FINSEQ_1:40;
consider Q being RedSequence of ==>.-relation TS such that
A13: <*(P . 1)*> ^ Q = P and
A14: len P = (len Q) + 1 by A5, A7, Th5;
A15: len Q >= 0 + 1 by NAT_1:8;
then A16: Q . 1 = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A13, A12, A10, FINSEQ_1:65;
A17: Q . (len Q) = [y,u] by A4, A13, A14, A12, A15, FINSEQ_1:65;
then consider v being Element of E ^omega such that
A18: u1 = v ^ u by A16, Th53;
B: {} ^ u1 = u1 ;
u = (w ^ v) ^ u by A18, A11, AFINSQ_1:27;
then w ^ v = {} by FLANG_2:4;
then A19: Q . 1 = [((P . (1 + 1)) `1),u] by A16, A11, B, AFINSQ_1:30;
hereby ::_thesis: verum
let l be Nat; ::_thesis: ( l in dom P implies (P . b1) `2 = u )
assume A20: l in dom P ; ::_thesis: (P . b1) `2 = u
then A21: 1 <= l by FINSEQ_3:25;
then reconsider l9 = l - 1 as Element of NAT by NAT_1:21;
1 + 1 <= l + 1 by A21, XREAL_1:6;
then A22: ( 1 + 1 = l + 1 or 1 + 1 <= l ) by NAT_1:8;
l <= len P by A20, FINSEQ_3:25;
then ( 1 = l or ( (1 + 1) - 1 <= l - 1 & l - 1 <= ((len Q) + 1) - 1 ) ) by A14, A22, XREAL_1:9;
then A23: ( l = 1 or l9 in dom Q ) by FINSEQ_3:25;
percases ( l = 1 or l - 1 in dom Q ) by A23;
suppose l = 1 ; ::_thesis: (P . b1) `2 = u
hence (P . l) `2 = u by A3, MCART_1:7; ::_thesis: verum
end;
supposeA24: l - 1 in dom Q ; ::_thesis: (P . b1) `2 = u
then l - 1 <= len Q by FINSEQ_3:25;
then A25: (l - 1) + 1 <= (len Q) + 1 by XREAL_1:6;
1 <= l - 1 by A24, FINSEQ_3:25;
then A26: 1 + 0 < (l - 1) + 1 by XREAL_1:6;
(Q . (l - 1)) `2 = u by A2, A5, A14, A17, A19, A24;
hence (P . l) `2 = u by A13, A14, A12, A26, A25, FINSEQ_1:24; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A27: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A27, A1);
hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u ; ::_thesis: verum
end;
theorem :: REWRITE3:55
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) )
assume A1: ( k in dom P & k + 1 in dom P ) ; ::_thesis: ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
consider s being Element of TS, u being Element of E ^omega , t being Element of TS, v being Element of E ^omega such that
A2: P . k = [s,u] and
A3: P . (k + 1) = [t,v] by A1, Th47;
[[s,u],[t,v]] in ==>.-relation TS by A1, A2, A3, REWRITE1:def_2;
then consider v1, w1 being Element of E ^omega such that
A4: v1 = v and
A5: s,w1 -->. t,TS and
A6: u = w1 ^ v1 by Th35;
take v1 ; ::_thesis: ex w being Element of E ^omega st
( v1 = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v1 )
take w1 ; ::_thesis: ( v1 = (P . (k + 1)) `2 & (P . k) `1 ,w1 -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w1 ^ v1 )
thus v1 = (P . (k + 1)) `2 by A3, A4, MCART_1:7; ::_thesis: ( (P . k) `1 ,w1 -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w1 ^ v1 )
(P . k) `1 ,w1 -->. t,TS by A2, A5, MCART_1:7;
hence ( (P . k) `1 ,w1 -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w1 ^ v1 ) by A2, A3, A6, MCART_1:7; ::_thesis: verum
end;
theorem :: REWRITE3:56
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] implies ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v ) )
assume ( k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] ) ; ::_thesis: ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
then [[x,u],[y,v]] in ==>.-relation TS by REWRITE1:def_2;
hence ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v ) by Th36; ::_thesis: verum
end;
theorem Th57: :: REWRITE3:57
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
thus ( x,y -->. z,TS implies <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) ::_thesis: ( <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS implies x,y -->. z,TS )
proof
assume x,y -->. z,TS ; ::_thesis: <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS
then [[x,y],[z,(<%> E)]] in ==>.-relation TS by Th37;
hence <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS by REWRITE1:7; ::_thesis: verum
end;
assume <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ; ::_thesis: x,y -->. z,TS
then [[x,y],[z,(<%> E)]] in ==>.-relation TS by Th8;
hence x,y -->. z,TS by Th37; ::_thesis: verum
end;
theorem Th58: :: REWRITE3:58
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
thus ( x,v -->. y,TS implies <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) ::_thesis: ( <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS implies x,v -->. y,TS )
proof
assume x,v -->. y,TS ; ::_thesis: <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS
then [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Th38;
hence <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS by REWRITE1:7; ::_thesis: verum
end;
assume <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ; ::_thesis: x,v -->. y,TS
then [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Th8;
hence x,v -->. y,TS by Th38; ::_thesis: verum
end;
theorem Th59: :: REWRITE3:59
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
len v >= len w
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
len v >= len w
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
len v >= len w
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
len v >= len w
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
len v >= len w
let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds
len v >= len w
let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,v] & P . (len P) = [y,w] implies len v >= len w )
assume ( P . 1 = [x,v] & P . (len P) = [y,w] ) ; ::_thesis: len v >= len w
then ex u being Element of E ^omega st v = u ^ w by Th53;
hence len v >= len w by Th9; ::_thesis: verum
end;
theorem Th60: :: REWRITE3:60
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
proof
let x, y be set ; ::_thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let E be non empty set ; ::_thesis: for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y ) )
defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS
for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = $1 holds
not $1 <> 1;
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
A2: 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 S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS
for_x,_y_being_set_st_P_._1_=_[x,u]_&_P_._(len_P)_=_[y,u]_&_len_P_=_k_+_1_holds_
not_k_+_1_<>_1
let P be RedSequence of ==>.-relation TS; ::_thesis: for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
not k + 1 <> 1
let x, y be set ; ::_thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies not k + 1 <> 1 )
assume that
A3: P . 1 = [x,u] and
A4: P . (len P) = [y,u] and
A5: ( len P = k + 1 & k + 1 <> 1 ) ; ::_thesis: contradiction
consider Q being RedSequence of ==>.-relation TS such that
<*(P . 1)*> ^ Q = P and
A6: len P = (len Q) + 1 by A5, Th5, NAT_1:25;
len Q >= 0 + 1 by NAT_1:8;
then (len Q) + 1 >= 1 + 1 by XREAL_1:6;
then A7: 1 + 1 in dom P by A6, FINSEQ_3:25;
len P > 1 by A5, NAT_1:25;
then A8: 1 in dom P by FINSEQ_3:25;
then P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A7, Th48
.= [((P . (1 + 1)) `1),u] by A3, A4, A7, Th54 ;
then [[x,u],[((P . (1 + 1)) `1),u]] in ==>.-relation TS by A3, A8, A7, REWRITE1:def_2;
then x,u ==>. (P . (1 + 1)) `1 ,u,TS by Def4;
hence contradiction by A1, Th28; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] implies ( len P = 1 & x = y ) )
assume A9: ( P . 1 = [x,u] & P . (len P) = [y,u] ) ; ::_thesis: ( len P = 1 & x = y )
A10: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A10, A2);
hence len P = 1 by A9; ::_thesis: x = y
hence x = y by A9, XTUPLE_0:1; ::_thesis: verum
end;
theorem Th61: :: REWRITE3:61
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1 )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
let P be RedSequence of ==>.-relation TS; ::_thesis: ( (P . 1) `2 = (P . (len P)) `2 implies len P = 1 )
assume A2: (P . 1) `2 = (P . (len P)) `2 ; ::_thesis: len P = 1
percases ( len P <= 1 or len P > 1 ) ;
supposeA3: len P <= 1 ; ::_thesis: len P = 1
len P >= 0 + 1 by NAT_1:13;
hence len P = 1 by A3, XXREAL_0:1; ::_thesis: verum
end;
supposeA4: len P > 1 ; ::_thesis: len P = 1
then reconsider p1 = (len P) - 1 as Nat by NAT_1:21;
A5: p1 + 1 = len P ;
then A6: p1 <= len P by NAT_1:13;
1 + 1 <= len P by A4, NAT_1:13;
then A7: 1 + 1 in dom P by FINSEQ_3:25;
0 + 1 <= p1 + 1 by XREAL_1:6;
then A8: p1 + 1 in dom P by FINSEQ_3:25;
1 <= p1 by A4, A5, NAT_1:13;
then p1 in dom P by A6, FINSEQ_3:25;
then consider s2 being Element of TS, v2 being Element of E ^omega , t2 being Element of TS, w2 being Element of E ^omega such that
P . p1 = [s2,v2] and
A9: P . (p1 + 1) = [t2,w2] by A8, Th47;
1 in dom P by A4, FINSEQ_3:25;
then consider s1 being Element of TS, v1 being Element of E ^omega , t1 being Element of TS, w1 being Element of E ^omega such that
A10: P . 1 = [s1,v1] and
P . (1 + 1) = [t1,w1] by A7, Th47;
(P . (len P)) `2 = w2 by A9, MCART_1:7;
then v1 = w2 by A2, A10, MCART_1:7;
hence len P = 1 by A1, A10, A9, Th60; ::_thesis: verum
end;
end;
end;
theorem Th62: :: REWRITE3:62
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
proof
let x, y be set ; ::_thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let E be non empty set ; ::_thesis: for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1 )
defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS
for u being Element of E ^omega
for x being set st len u = $1 & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1;
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
A2: now__::_thesis:_for_k_being_Nat_st_(_for_n_being_Nat_st_n_<_k_holds_
S1[n]_)_holds_
S1[k]
let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A3: for n being Nat st n < k holds
S1[n] ; ::_thesis: S1[k]
now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS
for_u_being_Element_of_E_^omega_
for_x_being_set_st_len_u_=_k_&_P_._1_=_[x,u]_&_P_._(len_P)_=_[y,(<%>_E)]_holds_
len_P_<=_(len_u)_+_1
let P be RedSequence of ==>.-relation TS; ::_thesis: for u being Element of E ^omega
for x being set st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len b3 <= (len b4) + 1
let u be Element of E ^omega ; ::_thesis: for x being set st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len b2 <= (len b3) + 1
let x be set ; ::_thesis: ( len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] implies len b1 <= (len b2) + 1 )
assume that
A4: len u = k and
A5: P . 1 = [x,u] and
A6: P . (len P) = [y,(<%> E)] ; ::_thesis: len b1 <= (len b2) + 1
percases ( len u < 1 or len u >= 1 ) ;
suppose len u < 1 ; ::_thesis: len b1 <= (len b2) + 1
then u = <%> E by NAT_1:25;
then len P = 1 by A1, A5, A6, Th60;
hence len P <= (len u) + 1 by NAT_1:25; ::_thesis: verum
end;
supposeA7: len u >= 1 ; ::_thesis: len b1 <= (len b2) + 1
A8: len P <> 1
proof
assume len P = 1 ; ::_thesis: contradiction
then u = <%> E by A5, A6, XTUPLE_0:1;
hence contradiction by A7; ::_thesis: verum
end;
then consider P9 being RedSequence of ==>.-relation TS such that
A9: <*(P . 1)*> ^ P9 = P and
A10: (len P9) + 1 = len P by Th5, NAT_1:25;
A11: len P > 1 by A8, NAT_1:25;
then len P >= 1 + 1 by NAT_1:13;
then A12: 1 + 1 in dom P by FINSEQ_3:25;
A13: 1 in dom P by A11, FINSEQ_3:25;
then A14: P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A12, Th48;
then A15: [[x,u],[((P . (1 + 1)) `1),((P . (1 + 1)) `2)]] in ==>.-relation TS by A5, A13, A12, REWRITE1:def_2;
then reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by Th32;
A16: ( len <*(P . 1)*> = 1 & len P9 >= 1 ) by FINSEQ_1:39, NAT_1:25;
then A17: P9 . 1 = [((P . (1 + 1)) `1),u1] by A9, A14, FINSEQ_1:65;
x,u ==>. (P . (1 + 1)) `1 ,u1,TS by A15, Def4;
then consider v being Element of E ^omega such that
A18: ( x,v -->. (P . (1 + 1)) `1 ,TS & u = v ^ u1 ) by Th22;
( v <> <%> E & len u = (len u1) + (len v) ) by A1, A18, Th15, AFINSQ_1:17;
then A19: (len u) - 0 > ((len u1) + (len v)) - (len v) by XREAL_1:15;
then A20: (len u1) + 1 <= len u by NAT_1:13;
P9 . (len P9) = [y,(<%> E)] by A6, A9, A10, A16, FINSEQ_1:65;
then len P9 <= (len u1) + 1 by A3, A4, A19, A17;
then len P9 <= len u by A20, XXREAL_0:2;
hence len P <= (len u) + 1 by A10, XREAL_1:6; ::_thesis: verum
end;
end;
end;
hence S1[k] ; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_4(A2);
hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1 ; ::_thesis: verum
end;
theorem Th63: :: REWRITE3:63
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 not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
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 not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
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 not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
let e be Element of E; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2 )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] implies len P = 2 )
assume A2: ( P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] ) ; ::_thesis: len P = 2
len P <= (len <%e%>) + 1 by A1, A2, Th62;
then A3: len P <= 1 + 1 by AFINSQ_1:34;
len P <> 1 by A2, XTUPLE_0:1;
hence len P = 2 by A3, NAT_1:26; ::_thesis: verum
end;
theorem Th64: :: REWRITE3:64
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w ) )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w implies ( len P = 1 & x = y & v = w ) )
assume A2: ( P . 1 = [x,v] & P . (len P) = [y,w] ) ; ::_thesis: ( len v > len w or ( len P = 1 & x = y & v = w ) )
consider u being Element of E ^omega such that
A3: v = u ^ w by A2, Th53;
A4: len v >= len w by A2, Th59;
percases ( len v > len w or len v <= len w ) ;
suppose len v > len w ; ::_thesis: ( len v > len w or ( len P = 1 & x = y & v = w ) )
hence ( len v > len w or ( len P = 1 & x = y & v = w ) ) ; ::_thesis: verum
end;
supposeA5: len v <= len w ; ::_thesis: ( len v > len w or ( len P = 1 & x = y & v = w ) )
A6: len v = (len u) + (len w) by A3, AFINSQ_1:17;
B: {} ^ w = w ;
len v = len w by A4, A5, XXREAL_0:1;
then u = <%> E by A6;
hence ( len v > len w or ( len P = 1 & x = y & v = w ) ) by A1, A2, Th60, A3, B; ::_thesis: verum
end;
end;
end;
theorem :: REWRITE3:65
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2 )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies (P . k) `2 <> (P . (k + 1)) `2 )
assume A2: ( k in dom P & k + 1 in dom P ) ; ::_thesis: (P . k) `2 <> (P . (k + 1)) `2
consider s being Element of TS, u being Element of E ^omega , t being Element of TS, v being Element of E ^omega such that
A3: P . k = [s,u] and
A4: P . (k + 1) = [t,v] by A2, Th47;
[[s,u],[t,v]] in ==>.-relation TS by A2, A3, A4, REWRITE1:def_2;
then u <> v by A1, Th43;
then (P . k) `2 <> v by A3, MCART_1:7;
hence (P . k) `2 <> (P . (k + 1)) `2 by A4, MCART_1:7; ::_thesis: verum
end;
theorem Th66: :: REWRITE3:66
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 )
defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS
for k, l being Nat st len P = $1 & k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2 ;
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
A2: 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 A3: S1[i] ; ::_thesis: S1[i + 1]
now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS
for_k,_l_being_Nat_st_len_P_=_i_+_1_&_k_in_dom_P_&_l_in_dom_P_&_k_<_l_holds_
(P_._k)_`2_<>_(P_._l)_`2
let P be RedSequence of ==>.-relation TS; ::_thesis: for k, l being Nat st len P = i + 1 & k in dom P & l in dom P & k < l holds
(b3 . b4) `2 <> (b3 . b5) `2
let k, l be Nat; ::_thesis: ( len P = i + 1 & k in dom P & l in dom P & k < l implies (b1 . b2) `2 <> (b1 . b3) `2 )
assume that
A4: len P = i + 1 and
A5: k in dom P and
A6: l in dom P and
A7: k < l ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2
A8: i < len P by A4, NAT_1:13;
A9: k <= len P by A5, FINSEQ_3:25;
A10: 1 <= k by A5, FINSEQ_3:25;
A11: 1 <= l by A6, FINSEQ_3:25;
A12: l <= len P by A6, FINSEQ_3:25;
percases ( ( k = 1 & l = len P ) or ( k <> 1 & l = len P ) or l <> len P ) ;
suppose ( k = 1 & l = len P ) ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2
hence (P . k) `2 <> (P . l) `2 by A1, A7, Th61; ::_thesis: verum
end;
supposeA13: ( k <> 1 & l = len P ) ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2
reconsider k1 = k - 1 as Nat by A10, NAT_1:21;
A14: k > 1 by A10, A13, XXREAL_0:1;
then k1 > 1 - 1 by XREAL_1:9;
then A15: k1 >= 0 + 1 by NAT_1:13;
reconsider l1 = l - 1 as Nat by A11, NAT_1:21;
A16: k1 < l1 by A7, XREAL_1:9;
A17: l > 1 by A7, A10, A11, XXREAL_0:1;
then consider Q being RedSequence of ==>.-relation TS such that
A18: <*(P . 1)*> ^ Q = P and
A19: (len Q) + 1 = len P by A13, Th5;
l1 > 1 - 1 by A17, XREAL_1:9;
then A20: l1 >= 0 + 1 by NAT_1:13;
k1 <= ((len Q) + 1) - 1 by A9, A19, XREAL_1:9;
then A21: k1 in dom Q by A15, FINSEQ_3:25;
A22: len <*(P . 1)*> = 1 by FINSEQ_1:40;
then A23: P . l = Q . l1 by A12, A17, A18, FINSEQ_1:24;
l1 <= ((len Q) + 1) - 1 by A12, A19, XREAL_1:9;
then A24: l1 in dom Q by A20, FINSEQ_3:25;
P . k = Q . k1 by A9, A14, A18, A22, FINSEQ_1:24;
hence (P . k) `2 <> (P . l) `2 by A3, A4, A19, A21, A24, A16, A23; ::_thesis: verum
end;
supposeA25: l <> len P ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2
k < i + 1 by A4, A7, A12, XXREAL_0:2;
then A26: k <= i by NAT_1:13;
then reconsider Q = P | i as RedSequence of ==>.-relation TS by A10, REWRITE2:3, XXREAL_0:2;
A27: P . k = Q . k by A26, FINSEQ_3:112;
l < i + 1 by A4, A12, A25, XXREAL_0:1;
then A28: l <= i by NAT_1:13;
then A29: P . l = Q . l by FINSEQ_3:112;
k <= len Q by A8, A26, FINSEQ_1:59;
then A30: k in dom Q by A10, FINSEQ_3:25;
l <= len Q by A8, A28, FINSEQ_1:59;
then A31: l in dom Q by A11, FINSEQ_3:25;
len Q = i by A8, FINSEQ_1:59;
hence (P . k) `2 <> (P . l) `2 by A3, A7, A30, A31, A27, A29; ::_thesis: verum
end;
end;
end;
hence S1[i + 1] ; ::_thesis: verum
end;
A32: S1[ 0 ] ;
A33: for i being Nat holds S1[i] from NAT_1:sch_2(A32, A2);
let P be RedSequence of ==>.-relation TS; ::_thesis: for k, l being Nat st k in dom P & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
let k, l be Nat; ::_thesis: ( k in dom P & l in dom P & k < l implies (P . k) `2 <> (P . l) `2 )
assume A34: ( k in dom P & l in dom P & k < l ) ; ::_thesis: (P . k) `2 <> (P . l) `2
len P = len P ;
hence (P . k) `2 <> (P . l) `2 by A33, A34; ::_thesis: verum
end;
theorem Th67: :: REWRITE3:67
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k )
assume A1: TS is deterministic ; ::_thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
let P, Q be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = Q . 1 implies for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k )
assume A2: P . 1 = Q . 1 ; ::_thesis: for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k
defpred S1[ Nat] means ( $1 in dom P & $1 in dom Q implies P . $1 = Q . $1 );
A3: 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 A4: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_k_+_1_in_dom_P_&_k_+_1_in_dom_Q_implies_P_._(k_+_1)_=_Q_._(k_+_1)_)
assume A5: ( k + 1 in dom P & k + 1 in dom Q ) ; ::_thesis: P . (k + 1) = Q . (k + 1)
percases ( ( k in dom P & k in dom Q ) or not k in dom P or not k in dom Q ) ;
supposeA6: ( k in dom P & k in dom Q ) ; ::_thesis: P . (k + 1) = Q . (k + 1)
then ( [(P . k),(P . (k + 1))] in ==>.-relation TS & [(Q . k),(Q . (k + 1))] in ==>.-relation TS ) by A5, REWRITE1:def_2;
hence P . (k + 1) = Q . (k + 1) by A1, A4, A6, Th44; ::_thesis: verum
end;
suppose ( not k in dom P or not k in dom Q ) ; ::_thesis: P . (k + 1) = Q . (k + 1)
then k = 0 by A5, REWRITE2:1;
hence P . (k + 1) = Q . (k + 1) by A2; ::_thesis: verum
end;
end;
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A7: S1[ 0 ] by FINSEQ_3:25;
for k being Nat holds S1[k] from NAT_1:sch_2(A7, A3);
hence for k being Nat st k in dom P & k in dom Q holds
P . k = Q . k ; ::_thesis: verum
end;
theorem Th68: :: REWRITE3:68
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q )
assume A1: TS is deterministic ; ::_thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds
P = Q
let P, Q be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = Q . 1 & len P = len Q implies P = Q )
assume that
A2: P . 1 = Q . 1 and
A3: len P = len Q ; ::_thesis: P = Q
now__::_thesis:_for_k_being_Nat_st_k_in_dom_P_holds_
P_._k_=_Q_._k
let k be Nat; ::_thesis: ( k in dom P implies P . k = Q . k )
assume A4: k in dom P ; ::_thesis: P . k = Q . k
then ( 1 <= k & k <= len P ) by FINSEQ_3:25;
then k in dom Q by A3, FINSEQ_3:25;
hence P . k = Q . k by A1, A2, A4, Th67; ::_thesis: verum
end;
hence P = Q by A3, FINSEQ_2:9; ::_thesis: verum
end;
theorem Th69: :: REWRITE3:69
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q )
assume A1: TS is deterministic ; ::_thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
then A2: not <%> E in rng (dom the Tran of TS) by Def1;
let P, Q be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 implies P = Q )
assume that
A3: P . 1 = Q . 1 and
A4: (P . (len P)) `2 = (Q . (len Q)) `2 ; ::_thesis: P = Q
percases ( len P = len Q or len P > len Q or len P < len Q ) by XXREAL_0:1;
suppose len P = len Q ; ::_thesis: P = Q
hence P = Q by A1, A3, Th68; ::_thesis: verum
end;
supposeA5: len P > len Q ; ::_thesis: P = Q
len P >= 0 + 1 by NAT_1:13;
then A6: len P in dom P by FINSEQ_3:25;
set k = len Q;
A7: len Q >= 0 + 1 by NAT_1:13;
then A8: len Q in dom P by A5, FINSEQ_3:25;
len Q in dom Q by A7, FINSEQ_3:25;
then (P . (len Q)) `2 = (P . (len P)) `2 by A1, A3, A4, A8, Th67;
hence P = Q by A2, A5, A8, A6, Th66; ::_thesis: verum
end;
supposeA9: len P < len Q ; ::_thesis: P = Q
len Q >= 0 + 1 by NAT_1:13;
then A10: len Q in dom Q by FINSEQ_3:25;
set k = len P;
A11: len P >= 0 + 1 by NAT_1:13;
then A12: len P in dom Q by A9, FINSEQ_3:25;
len P in dom P by A11, FINSEQ_3:25;
then (Q . (len P)) `2 = (Q . (len Q)) `2 by A1, A3, A4, A12, Th67;
hence P = Q by A2, A9, A12, A10, Th66; ::_thesis: verum
end;
end;
end;
begin
theorem Th70: :: REWRITE3:70
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
ex u being Element of E ^omega st v = u ^ w
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
ex u being Element of E ^omega st v = u ^ w
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
ex u being Element of E ^omega st v = u ^ w
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
ex u being Element of E ^omega st v = u ^ w
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
ex u being Element of E ^omega st v = u ^ w
let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,v],[y,w] implies ex u being Element of E ^omega st v = u ^ w )
assume ==>.-relation TS reduces [x,v],[y,w] ; ::_thesis: ex u being Element of E ^omega st v = u ^ w
then ex P being RedSequence of ==>.-relation TS st
( P . 1 = [x,v] & P . (len P) = [y,w] ) by REWRITE1:def_3;
hence ex u being Element of E ^omega st v = u ^ w by Th53; ::_thesis: verum
end;
theorem Th71: :: REWRITE3:71
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,u],[y,v] implies ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] )
assume ==>.-relation TS reduces [x,u],[y,v] ; ::_thesis: ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
then consider P being RedSequence of ==>.-relation TS such that
A1: P . 1 = [x,u] and
A2: P . (len P) = [y,v] by REWRITE1:def_3;
A3: len P >= 0 + 1 by NAT_1:13;
then len P in dom P by FINSEQ_3:25;
then A4: dim2 ((P . (len P)),E) = (P . (len P)) `2 by A1, Th51
.= v by A2, MCART_1:7 ;
deffunc H1( set ) -> set = [((P . $1) `1),((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();
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
A7: k in dom Q and
A8: k + 1 in dom Q ; ::_thesis: [(Q . k),(Q . (k + 1))] in ==>.-relation TS
( 1 <= k + 1 & k + 1 <= len Q ) by A8, FINSEQ_3:25;
then A9: k + 1 in dom P by A5, FINSEQ_3:25;
( 1 <= k & k <= len Q ) by A7, FINSEQ_3:25;
then A10: k in dom P by A5, FINSEQ_3:25;
then [(P . k),(P . (k + 1))] in ==>.-relation TS by A9, REWRITE1:def_2;
then [[((P . k) `1),((P . k) `2)],(P . (k + 1))] in ==>.-relation TS by A10, A9, Th48;
then [[((P . k) `1),((P . k) `2)],[((P . (k + 1)) `1),((P . (k + 1)) `2)]] in ==>.-relation TS by A10, A9, Th48;
then [[((P . k) `1),(dim2 ((P . k),E))],[((P . (k + 1)) `1),((P . (k + 1)) `2)]] in ==>.-relation TS by A1, A10, Th51;
then [[((P . k) `1),(dim2 ((P . k),E))],[((P . (k + 1)) `1),(dim2 ((P . (k + 1)),E))]] in ==>.-relation TS by A1, A9, Th51;
then (P . k) `1 , dim2 ((P . k),E) ==>. (P . (k + 1)) `1 , dim2 ((P . (k + 1)),E),TS by Def4;
then (P . k) `1 ,(dim2 ((P . k),E)) ^ w ==>. (P . (k + 1)) `1 ,(dim2 ((P . (k + 1)),E)) ^ w,TS by Th25;
then [[((P . k) `1),((dim2 ((P . k),E)) ^ w)],[((P . (k + 1)) `1),((dim2 ((P . (k + 1)),E)) ^ w)]] in ==>.-relation TS by Def4;
then [[((P . k) `1),((dim2 ((P . k),E)) ^ w)],(Q . (k + 1))] in ==>.-relation TS by A6, A8;
hence [(Q . k),(Q . (k + 1))] in ==>.-relation TS by A6, A7; ::_thesis: verum
end;
then reconsider Q = Q as RedSequence of ==>.-relation TS by A5, REWRITE1:def_2;
A11: len Q >= 0 + 1 by NAT_1:13;
then len Q in dom Q by FINSEQ_3:25;
then Q . (len Q) = [((P . (len Q)) `1),((dim2 ((P . (len Q)),E)) ^ w)] by A6;
then A12: Q . (len Q) = [y,(v ^ w)] by A2, A5, A4, MCART_1:7;
1 in dom P by A3, FINSEQ_3:25;
then A13: dim2 ((P . 1),E) = (P . 1) `2 by A1, Th51
.= u by A1, MCART_1:7 ;
1 in dom Q by A11, FINSEQ_3:25;
then Q . 1 = [((P . 1) `1),((dim2 ((P . 1),E)) ^ w)] by A6
.= [x,(u ^ w)] by A1, A13, MCART_1:7 ;
hence ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by A12, REWRITE1:def_3; ::_thesis: verum
end;
theorem Th72: :: REWRITE3:72
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
==>.-relation TS reduces [x,y],[z,(<%> E)]
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
==>.-relation TS reduces [x,y],[z,(<%> E)]
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
==>.-relation TS reduces [x,y],[z,(<%> E)]
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,y -->. z,TS holds
==>.-relation TS reduces [x,y],[z,(<%> E)]
let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS implies ==>.-relation TS reduces [x,y],[z,(<%> E)] )
assume x,y -->. z,TS ; ::_thesis: ==>.-relation TS reduces [x,y],[z,(<%> E)]
then <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS by Th57;
then [[x,y],[z,(<%> E)]] in ==>.-relation TS by Th8;
hence ==>.-relation TS reduces [x,y],[z,(<%> E)] by REWRITE1:15; ::_thesis: verum
end;
theorem Th73: :: REWRITE3:73
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
==>.-relation TS reduces [x,(v ^ w)],[y,w]
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
==>.-relation TS reduces [x,(v ^ w)],[y,w]
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
==>.-relation TS reduces [x,(v ^ w)],[y,w]
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
==>.-relation TS reduces [x,(v ^ w)],[y,w]
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v -->. y,TS holds
==>.-relation TS reduces [x,(v ^ w)],[y,w]
let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS implies ==>.-relation TS reduces [x,(v ^ w)],[y,w] )
assume x,v -->. y,TS ; ::_thesis: ==>.-relation TS reduces [x,(v ^ w)],[y,w]
then <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS by Th58;
then [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Th8;
hence ==>.-relation TS reduces [x,(v ^ w)],[y,w] by REWRITE1:15; ::_thesis: verum
end;
theorem Th74: :: REWRITE3:74
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>. y1,y2,TS implies ==>.-relation TS reduces [x1,x2],[y1,y2] )
assume x1,x2 ==>. y1,y2,TS ; ::_thesis: ==>.-relation TS reduces [x1,x2],[y1,y2]
then [[x1,x2],[y1,y2]] in ==>.-relation TS by Def4;
hence ==>.-relation TS reduces [x1,x2],[y1,y2] by REWRITE1:15; ::_thesis: verum
end;
theorem Th75: :: REWRITE3:75
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
len v >= len w
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
len v >= len w
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
len v >= len w
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
len v >= len w
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
len v >= len w
let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,v],[y,w] implies len v >= len w )
assume ==>.-relation TS reduces [x,v],[y,w] ; ::_thesis: len v >= len w
then ex P being RedSequence of ==>.-relation TS st
( P . 1 = [x,v] & P . (len P) = [y,w] ) by REWRITE1:def_3;
hence len v >= len w by Th59; ::_thesis: verum
end;
theorem :: REWRITE3:76
for x, y being set
for E being non empty set
for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
proof
let x, y be set ; ::_thesis: for E being non empty set
for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
let E be non empty set ; ::_thesis: for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
let w, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,w],[y,(v ^ w)] implies v = <%> E )
assume ==>.-relation TS reduces [x,w],[y,(v ^ w)] ; ::_thesis: v = <%> E
then len w >= len (v ^ w) by Th75;
then (len v) + (len w) <= 0 + (len w) by AFINSQ_1:17;
hence v = <%> E by XREAL_1:6; ::_thesis: verum
end;
theorem Th77: :: REWRITE3:77
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds
( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
let TS be non empty transition-system over F; ::_thesis: ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) )
assume ==>.-relation TS reduces [x,v],[y,w] ; ::_thesis: ( len v > len w or ( x = y & v = w ) )
then ex P being RedSequence of ==>.-relation TS st
( P . 1 = [x,v] & P . (len P) = [y,w] ) by REWRITE1:def_3;
hence ( len v > len w or ( x = y & v = w ) ) by A1, Th64; ::_thesis: verum
end;
theorem :: REWRITE3:78
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds
x = y
proof
let x, y be set ; ::_thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds
x = y
let E be non empty set ; ::_thesis: for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds
x = y
let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds
x = y
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds
x = y
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] implies x = y )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not ==>.-relation TS reduces [x,u],[y,u] or x = y )
assume ==>.-relation TS reduces [x,u],[y,u] ; ::_thesis: x = y
then ( len u > len u or x = y ) by A1, Th77;
hence x = y ; ::_thesis: verum
end;
theorem Th79: :: REWRITE3:79
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 not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation 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 not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation 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 not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation 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 not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] implies [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] or [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS )
assume ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] ; ::_thesis: [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS
then consider P being RedSequence of ==>.-relation TS such that
A2: ( P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] ) by REWRITE1:def_3;
A3: len P = 1 + 1 by A1, A2, Th63;
then ( 1 in dom P & 1 + 1 in dom P ) by FINSEQ_3:25;
hence [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS by A2, A3, REWRITE1:def_2; ::_thesis: verum
end;
theorem Th80: :: REWRITE3:80
for x, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
proof
let x, y1, z, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] implies y1 = y2 )
assume A1: TS is deterministic ; ::_thesis: ( not ==>.-relation TS reduces x,[y1,z] or not ==>.-relation TS reduces x,[y2,z] or y1 = y2 )
assume that
A2: ==>.-relation TS reduces x,[y1,z] and
A3: ==>.-relation TS reduces x,[y2,z] ; ::_thesis: y1 = y2
consider P being RedSequence of ==>.-relation TS such that
A4: P . 1 = x and
A5: P . (len P) = [y1,z] by A2, REWRITE1:def_3;
consider Q being RedSequence of ==>.-relation TS such that
A6: Q . 1 = x and
A7: Q . (len Q) = [y2,z] by A3, REWRITE1:def_3;
A8: (Q . (len Q)) `2 = z by A7, MCART_1:7;
(P . (len P)) `2 = z by A5, MCART_1:7;
then P = Q by A1, A4, A6, A8, Th69;
hence y1 = y2 by A5, A7, XTUPLE_0:1; ::_thesis: verum
end;
begin
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
let x1, x2, y1, y2 be set ;
predx1,x2 ==>* y1,y2,TS means :Def6: :: REWRITE3:def 6
==>.-relation TS reduces [x1,x2],[y1,y2];
end;
:: deftheorem Def6 defines ==>* REWRITE3:def_6_:_
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for x1, x2, y1, y2 being set holds
( x1,x2 ==>* y1,y2,TS iff ==>.-relation TS reduces [x1,x2],[y1,y2] );
theorem Th81: :: REWRITE3:81
for x1, x2, y1, y2 being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 implies x1,x2 ==>* y1,y2,TS2 )
assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; ::_thesis: ( not x1,x2 ==>* y1,y2,TS1 or x1,x2 ==>* y1,y2,TS2 )
assume x1,x2 ==>* y1,y2,TS1 ; ::_thesis: x1,x2 ==>* y1,y2,TS2
then ==>.-relation TS1 reduces [x1,x2],[y1,y2] by Def6;
then ==>.-relation TS2 reduces [x1,x2],[y1,y2] by A1, Th34;
hence x1,x2 ==>* y1,y2,TS2 by Def6; ::_thesis: verum
end;
theorem Th82: :: REWRITE3:82
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x,y ==>* x,y,TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x,y ==>* x,y,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x,y ==>* x,y,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds x,y ==>* x,y,TS
let TS be non empty transition-system over F; ::_thesis: x,y ==>* x,y,TS
==>.-relation TS reduces [x,y],[x,y] by REWRITE1:12;
hence x,y ==>* x,y,TS by Def6; ::_thesis: verum
end;
theorem Th83: :: REWRITE3:83
for x1, x2, y1, y2, z1, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
proof
let x1, x2, y1, y2, z1, z2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS implies x1,x2 ==>* z1,z2,TS )
assume ( x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS ) ; ::_thesis: x1,x2 ==>* z1,z2,TS
then ( ==>.-relation TS reduces [x1,x2],[y1,y2] & ==>.-relation TS reduces [y1,y2],[z1,z2] ) by Def6;
then ==>.-relation TS reduces [x1,x2],[z1,z2] by REWRITE1:16;
hence x1,x2 ==>* z1,z2,TS by Def6; ::_thesis: verum
end;
theorem Th84: :: REWRITE3:84
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS implies x,y ==>* z, <%> E,TS )
assume x,y -->. z,TS ; ::_thesis: x,y ==>* z, <%> E,TS
then ==>.-relation TS reduces [x,y],[z,(<%> E)] by Th72;
hence x,y ==>* z, <%> E,TS by Def6; ::_thesis: verum
end;
theorem :: REWRITE3:85
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
x,v ^ w ==>* y,w,TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
x,v ^ w ==>* y,w,TS
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
x,v ^ w ==>* y,w,TS
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
x,v ^ w ==>* y,w,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v -->. y,TS holds
x,v ^ w ==>* y,w,TS
let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS implies x,v ^ w ==>* y,w,TS )
assume x,v -->. y,TS ; ::_thesis: x,v ^ w ==>* y,w,TS
then ==>.-relation TS reduces [x,(v ^ w)],[y,w] by Th73;
hence x,v ^ w ==>* y,w,TS by Def6; ::_thesis: verum
end;
theorem Th86: :: REWRITE3:86
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,v,TS holds
x,u ^ w ==>* y,v ^ w,TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,v,TS holds
x,u ^ w ==>* y,v ^ w,TS
let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,v,TS holds
x,u ^ w ==>* y,v ^ w,TS
let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,v,TS holds
x,u ^ w ==>* y,v ^ w,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,u ==>* y,v,TS holds
x,u ^ w ==>* y,v ^ w,TS
let TS be non empty transition-system over F; ::_thesis: ( x,u ==>* y,v,TS implies x,u ^ w ==>* y,v ^ w,TS )
assume x,u ==>* y,v,TS ; ::_thesis: x,u ^ w ==>* y,v ^ w,TS
then ==>.-relation TS reduces [x,u],[y,v] by Def6;
then ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by Th71;
hence x,u ^ w ==>* y,v ^ w,TS by Def6; ::_thesis: verum
end;
theorem Th87: :: REWRITE3:87
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
x1,x2 ==>* y1,y2,TS
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
x1,x2 ==>* y1,y2,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
x1,x2 ==>* y1,y2,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
x1,x2 ==>* y1,y2,TS
let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>. y1,y2,TS implies x1,x2 ==>* y1,y2,TS )
assume x1,x2 ==>. y1,y2,TS ; ::_thesis: x1,x2 ==>* y1,y2,TS
then ==>.-relation TS reduces [x1,x2],[y1,y2] by Th74;
hence x1,x2 ==>* y1,y2,TS by Def6; ::_thesis: verum
end;
theorem Th88: :: REWRITE3:88
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
ex u being Element of E ^omega st v = u ^ w
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
ex u being Element of E ^omega st v = u ^ w
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
ex u being Element of E ^omega st v = u ^ w
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
ex u being Element of E ^omega st v = u ^ w
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
ex u being Element of E ^omega st v = u ^ w
let TS be non empty transition-system over F; ::_thesis: ( x,v ==>* y,w,TS implies ex u being Element of E ^omega st v = u ^ w )
assume x,v ==>* y,w,TS ; ::_thesis: ex u being Element of E ^omega st v = u ^ w
then ==>.-relation TS reduces [x,v],[y,w] by Def6;
hence ex u being Element of E ^omega st v = u ^ w by Th70; ::_thesis: verum
end;
theorem Th89: :: REWRITE3:89
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
len w <= len v
proof
let x, y be set ; ::_thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
len w <= len v
let E be non empty set ; ::_thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
len w <= len v
let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
len w <= len v
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
len w <= len v
let TS be non empty transition-system over F; ::_thesis: ( x,v ==>* y,w,TS implies len w <= len v )
assume x,v ==>* y,w,TS ; ::_thesis: len w <= len v
then ex u being Element of E ^omega st v = u ^ w by Th88;
hence len w <= len v by Th9; ::_thesis: verum
end;
theorem :: REWRITE3:90
for x, y being set
for E being non empty set
for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
proof
let x, y be set ; ::_thesis: for E being non empty set
for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let E be non empty set ; ::_thesis: for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let w, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let TS be non empty transition-system over F; ::_thesis: ( x,w ==>* y,v ^ w,TS implies v = <%> E )
assume x,w ==>* y,v ^ w,TS ; ::_thesis: v = <%> E
then len (v ^ w) <= len w by Th89;
then (len v) + (len w) <= 0 + (len w) by AFINSQ_1:17;
hence v = <%> E by XREAL_1:6; ::_thesis: verum
end;
theorem Th91: :: REWRITE3:91
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x,u ==>* y,u,TS iff x = y )
proof
let x, y be set ; ::_thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x,u ==>* y,u,TS iff x = y )
let E be non empty set ; ::_thesis: for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x,u ==>* y,u,TS iff x = y )
let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x,u ==>* y,u,TS iff x = y )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x,u ==>* y,u,TS iff x = y )
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies ( x,u ==>* y,u,TS iff x = y ) )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( x,u ==>* y,u,TS iff x = y )
thus ( x,u ==>* y,u,TS implies x = y ) ::_thesis: ( x = y implies x,u ==>* y,u,TS )
proof
assume x,u ==>* y,u,TS ; ::_thesis: x = y
then ==>.-relation TS reduces [x,u],[y,u] by Def6;
then ex p being RedSequence of ==>.-relation TS st
( p . 1 = [x,u] & p . (len p) = [y,u] ) by REWRITE1:def_3;
hence x = y by A1, Th60; ::_thesis: verum
end;
assume x = y ; ::_thesis: x,u ==>* y,u,TS
hence x,u ==>* y,u,TS by Th82; ::_thesis: verum
end;
theorem Th92: :: REWRITE3:92
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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,TS
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS implies x,<%e%> ==>. y, <%> E,TS )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not x,<%e%> ==>* y, <%> E,TS or x,<%e%> ==>. y, <%> E,TS )
assume x,<%e%> ==>* y, <%> E,TS ; ::_thesis: x,<%e%> ==>. y, <%> E,TS
then ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] by Def6;
then [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS by A1, Th79;
hence x,<%e%> ==>. y, <%> E,TS by Def4; ::_thesis: verum
end;
theorem Th93: :: REWRITE3:93
for x1, x2, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
proof
let x1, x2, y1, z, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS implies y1 = y2 )
assume A1: TS is deterministic ; ::_thesis: ( not x1,x2 ==>* y1,z,TS or not x1,x2 ==>* y2,z,TS or y1 = y2 )
assume ( x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS ) ; ::_thesis: y1 = y2
then ( ==>.-relation TS reduces [x1,x2],[y1,z] & ==>.-relation TS reduces [x1,x2],[y2,z] ) by Def6;
hence y1 = y2 by A1, Th80; ::_thesis: verum
end;
begin
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
let x1, x2, y be set ;
predx1,x2 ==>* y,TS means :Def7: :: REWRITE3:def 7
x1,x2 ==>* y, <%> E,TS;
end;
:: deftheorem Def7 defines ==>* REWRITE3:def_7_:_
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for x1, x2, y being set holds
( x1,x2 ==>* y,TS iff x1,x2 ==>* y, <%> E,TS );
theorem Th94: :: REWRITE3:94
for x, y, z being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2
let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 implies x,y ==>* z,TS2 )
assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; ::_thesis: ( not x,y ==>* z,TS1 or x,y ==>* z,TS2 )
assume x,y ==>* z,TS1 ; ::_thesis: x,y ==>* z,TS2
then x,y ==>* z, <%> E,TS1 by Def7;
then x,y ==>* z, <%> E,TS2 by A1, Th81;
hence x,y ==>* z,TS2 by Def7; ::_thesis: verum
end;
theorem Th95: :: REWRITE3:95
for x being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x, <%> E ==>* x,TS
proof
let x be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x, <%> E ==>* x,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x, <%> E ==>* x,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds x, <%> E ==>* x,TS
let TS be non empty transition-system over F; ::_thesis: x, <%> E ==>* x,TS
x, <%> E ==>* x, <%> E,TS by Th82;
hence x, <%> E ==>* x,TS by Def7; ::_thesis: verum
end;
theorem Th96: :: REWRITE3:96
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS holds
x,u ^ v ==>* y,v,TS
proof
let x, y be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS holds
x,u ^ v ==>* y,v,TS
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS holds
x,u ^ v ==>* y,v,TS
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS holds
x,u ^ v ==>* y,v,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,u ==>* y,TS holds
x,u ^ v ==>* y,v,TS
let TS be non empty transition-system over F; ::_thesis: ( x,u ==>* y,TS implies x,u ^ v ==>* y,v,TS )
assume x,u ==>* y,TS ; ::_thesis: x,u ^ v ==>* y,v,TS
then x,u ==>* y, <%> E,TS by Def7;
then x,u ^ v ==>* y,{} ^ v,TS by Th86;
hence x,u ^ v ==>* y,v,TS ; ::_thesis: verum
end;
theorem :: REWRITE3:97
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z,TS
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z,TS
let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS implies x,y ==>* z,TS )
assume x,y -->. z,TS ; ::_thesis: x,y ==>* z,TS
then x,y ==>* z, <%> E,TS by Th84;
hence x,y ==>* z,TS by Def7; ::_thesis: verum
end;
theorem :: REWRITE3:98
for x1, x2, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
proof
let x1, x2, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>. y, <%> E,TS implies x1,x2 ==>* y,TS )
assume x1,x2 ==>. y, <%> E,TS ; ::_thesis: x1,x2 ==>* y,TS
then x1,x2 ==>* y, <%> E,TS by Th87;
hence x1,x2 ==>* y,TS by Def7; ::_thesis: verum
end;
theorem :: REWRITE3:99
for x, y, z being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
proof
let x, y, z be set ; ::_thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
let E be non empty set ; ::_thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
let TS be non empty transition-system over F; ::_thesis: ( x,u ==>* y,TS & y,v ==>* z,TS implies x,u ^ v ==>* z,TS )
assume that
A1: x,u ==>* y,TS and
A2: y,v ==>* z,TS ; ::_thesis: x,u ^ v ==>* z,TS
x,(u ^ v) ^ {} ==>* y,v,TS by A1, Th96;
then A3: x,(u ^ v) ^ (<%> E) ==>* y,v ^ {},TS ;
y,v ==>* z, <%> E,TS by A2, Def7;
then x,(u ^ v) ^ {} ==>* z, <%> E,TS by A3, Th83;
hence x,u ^ v ==>* z,TS by Def7; ::_thesis: verum
end;
theorem Th100: :: REWRITE3:100
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x, <%> E ==>* y,TS iff x = y )
proof
let x, y be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x, <%> E ==>* y,TS iff x = y )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x, <%> E ==>* y,TS iff x = y )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x, <%> E ==>* y,TS iff x = y )
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies ( x, <%> E ==>* y,TS iff x = y ) )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( x, <%> E ==>* y,TS iff x = y )
thus ( x, <%> E ==>* y,TS implies x = y ) ::_thesis: ( x = y implies x, <%> E ==>* y,TS )
proof
assume x, <%> E ==>* y,TS ; ::_thesis: x = y
then x, <%> E ==>* y, <%> E,TS by Def7;
hence x = y by A1, Th91; ::_thesis: verum
end;
assume x = y ; ::_thesis: x, <%> E ==>* y,TS
hence x, <%> E ==>* y,TS by Th95; ::_thesis: verum
end;
theorem :: REWRITE3:101
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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,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 not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,TS
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,TS
let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS implies x,<%e%> ==>. y, <%> E,TS )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not x,<%e%> ==>* y,TS or x,<%e%> ==>. y, <%> E,TS )
assume x,<%e%> ==>* y,TS ; ::_thesis: x,<%e%> ==>. y, <%> E,TS
then x,<%e%> ==>* y, <%> E,TS by Def7;
hence x,<%e%> ==>. y, <%> E,TS by A1, Th92; ::_thesis: verum
end;
theorem :: REWRITE3:102
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds
y1 = y2
proof
let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds
y1 = y2
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds
y1 = y2
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds
y1 = y2
let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS implies y1 = y2 )
assume A1: TS is deterministic ; ::_thesis: ( not x1,x2 ==>* y1,TS or not x1,x2 ==>* y2,TS or y1 = y2 )
assume ( x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS ) ; ::_thesis: y1 = y2
then ( x1,x2 ==>* y1, <%> E,TS & x1,x2 ==>* y2, <%> E,TS ) by Def7;
hence y1 = y2 by A1, Th93; ::_thesis: verum
end;
begin
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
let x, X be set ;
funcx -succ_of (X,TS) -> Subset of TS equals :: REWRITE3:def 8
{ s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } ;
coherence
{ s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } is Subset of TS
proof
set Y = { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } ;
{ s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } c= the carrier of TS
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } or y in the carrier of TS )
assume y in { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } ; ::_thesis: y in the carrier of TS
then ex s being Element of TS st
( s = y & ex t being Element of TS st
( t in X & t,x ==>* s,TS ) ) ;
hence y in the carrier of TS ; ::_thesis: verum
end;
hence { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } is Subset of TS ; ::_thesis: verum
end;
end;
:: deftheorem defines -succ_of REWRITE3:def_8_:_
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for x, X being set holds x -succ_of (X,TS) = { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } ;
theorem Th103: :: REWRITE3:103
for x, X being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for s being Element of TS holds
( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
proof
let x, X be set ; ::_thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for s being Element of TS holds
( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for s being Element of TS holds
( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for s being Element of TS holds
( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let TS be non empty transition-system over F; ::_thesis: for s being Element of TS holds
( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
let s be Element of TS; ::_thesis: ( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X & t,x ==>* s,TS ) )
thus ( s in x -succ_of (X,TS) implies ex t being Element of TS st
( t in X & t,x ==>* s,TS ) ) ::_thesis: ( ex t being Element of TS st
( t in X & t,x ==>* s,TS ) implies s in x -succ_of (X,TS) )
proof
assume s in x -succ_of (X,TS) ; ::_thesis: ex t being Element of TS st
( t in X & t,x ==>* s,TS )
then ex s9 being Element of TS st
( s9 = s & ex t being Element of TS st
( t in X & t,x ==>* s9,TS ) ) ;
hence ex t being Element of TS st
( t in X & t,x ==>* s,TS ) ; ::_thesis: verum
end;
thus ( ex t being Element of TS st
( t in X & t,x ==>* s,TS ) implies s in x -succ_of (X,TS) ) ; ::_thesis: verum
end;
theorem :: REWRITE3:104
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of (S,TS) = S
proof
let E be non empty set ; ::_thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of (S,TS) = S
let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F
for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of (S,TS) = S
let TS be non empty transition-system over F; ::_thesis: for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of (S,TS) = S
let S be Subset of TS; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies (<%> E) -succ_of (S,TS) = S )
assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: (<%> E) -succ_of (S,TS) = S
A2: now__::_thesis:_for_x_being_set_st_x_in_(<%>_E)_-succ_of_(S,TS)_holds_
x_in_S
let x be set ; ::_thesis: ( x in (<%> E) -succ_of (S,TS) implies x in S )
assume x in (<%> E) -succ_of (S,TS) ; ::_thesis: x in S
then ex s being Element of TS st
( s in S & s, <%> E ==>* x,TS ) by Th103;
hence x in S by A1, Th100; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_S_holds_
x_in_(<%>_E)_-succ_of_(S,TS)
let x be set ; ::_thesis: ( x in S implies x in (<%> E) -succ_of (S,TS) )
assume A3: x in S ; ::_thesis: x in (<%> E) -succ_of (S,TS)
x, <%> E ==>* x,TS by Th95;
hence x in (<%> E) -succ_of (S,TS) by A3; ::_thesis: verum
end;
hence (<%> E) -succ_of (S,TS) = S by A2, TARSKI:1; ::_thesis: verum
end;
theorem :: REWRITE3:105
for x, X being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
proof
let x, X be set ; ::_thesis: for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 implies x -succ_of (X,TS1) = x -succ_of (X,TS2) )
assume that
A1: the carrier of TS1 = the carrier of TS2 and
A2: the Tran of TS1 = the Tran of TS2 ; ::_thesis: x -succ_of (X,TS1) = x -succ_of (X,TS2)
A3: now__::_thesis:_for_y_being_set_st_y_in_x_-succ_of_(X,TS2)_holds_
y_in_x_-succ_of_(X,TS1)
let y be set ; ::_thesis: ( y in x -succ_of (X,TS2) implies y in x -succ_of (X,TS1) )
assume A4: y in x -succ_of (X,TS2) ; ::_thesis: y in x -succ_of (X,TS1)
then reconsider q = y as Element of TS2 ;
consider p being Element of TS2 such that
A5: p in X and
A6: p,x ==>* q,TS2 by A4, Th103;
reconsider q = q as Element of TS1 by A1;
reconsider p = p as Element of TS1 by A1;
p,x ==>* q,TS1 by A1, A2, A6, Th94;
hence y in x -succ_of (X,TS1) by A5; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_x_-succ_of_(X,TS1)_holds_
y_in_x_-succ_of_(X,TS2)
let y be set ; ::_thesis: ( y in x -succ_of (X,TS1) implies y in x -succ_of (X,TS2) )
assume A7: y in x -succ_of (X,TS1) ; ::_thesis: y in x -succ_of (X,TS2)
then reconsider q = y as Element of TS1 ;
consider p being Element of TS1 such that
A8: p in X and
A9: p,x ==>* q,TS1 by A7, Th103;
reconsider q = q as Element of TS2 by A1;
reconsider p = p as Element of TS2 by A1;
p,x ==>* q,TS2 by A1, A2, A9, Th94;
hence y in x -succ_of (X,TS2) by A8; ::_thesis: verum
end;
hence x -succ_of (X,TS1) = x -succ_of (X,TS2) by A3, TARSKI:1; ::_thesis: verum
end;