:: Labelled State Transition Systems :: by Micha{\l} Trybulec :: :: Received May 5, 2009 :: Copyright (c) 2009-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, AFINSQ_1, NAT_1, FINSEQ_1, RELAT_1, ORDINAL4, FUNCT_1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, REWRITE1, STRUCT_0, FSM_1, ZFMISC_1, FINSET_1, REWRITE2, PRELAMB, TARSKI, MCART_1, REWRITE3; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XCMPLX_0, ORDINAL1, FUNCT_1, RELSET_1, XXREAL_0, FINSET_1, RELAT_1, AFINSQ_1, SUBSET_1, REWRITE1, FLANG_1, STRUCT_0, NUMBERS, MCART_1, FINSEQ_1; constructors NAT_1, FSM_1, MEMBERED, REWRITE1, FLANG_1, XREAL_0, RELSET_1, XTUPLE_0; registrations CARD_1, RELSET_1, NAT_1, XREAL_0, XBOOLE_0, XXREAL_0, STRUCT_0, SUBSET_1, REWRITE1, AFINSQ_1, RELAT_1, FUNCT_1, FINSEQ_1, XTUPLE_0, ORDINAL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries - FinSequences reserve x, x1, x2, y, y1, y2, z, z1, z2 for object, X, X1, X2 for set; reserve E for non empty set; reserve e for Element of E; reserve u, u9, u1, u2, v, v1, v2, w, w1, w2 for Element of E^omega; reserve F, F1, F2 for Subset of E^omega; reserve i, k, l, n for Nat; theorem :: REWRITE3:1 for p being FinSequence st k in dom p holds (<*x*>^p).(k + 1) = p.k; theorem :: REWRITE3:2 for p being FinSequence holds p <> {} implies ex q being FinSequence, x st p = q^<*x*> & len p = len q + 1; theorem :: REWRITE3:3 for p being FinSequence st k in dom p & not k + 1 in dom p holds len p = k; begin :: Preliminaries - RedSequences theorem :: REWRITE3:4 for R being Relation, P being RedSequence of R, 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; theorem :: REWRITE3:5 for R being Relation, 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; theorem :: REWRITE3:6 for R being Relation, 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; theorem :: REWRITE3:7 for R being Relation, P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st len Q + 1 = len P & for k st k in dom Q holds Q.k = P .(k + 1); theorem :: REWRITE3:8 for R being Relation holds <*x, y*> is RedSequence of R implies [ x, y] in R; begin :: Preliminaries - XFinSequences theorem :: REWRITE3:9 w = u^v implies len u <= len w & len v <= len w; theorem :: REWRITE3:10 w = u^v & u <> <%>E & v <> <%>E implies len u < len w & len v < len w; theorem :: REWRITE3:11 w1^v1 = w2^v2 & ( len w1 = len w2 or len v1 = len v2 ) implies w1 = w2 & v1 = v2; theorem :: REWRITE3:12 w1^v1 = w2^v2 & ( len w1 <= len w2 or len v1 >= len v2 ) implies ex u st w1^u = w2 & v1 = u^v2; theorem :: REWRITE3:13 w1^v1 = w2^v2 implies (ex u st w1^u = w2 & v1 = u^v2) or ex u st w2^u = w1 & v2 = u^v1; begin :: Labelled State Transition Systems definition let X; struct (1-sorted) transition-system over X (# carrier -> set, Tran -> Relation of [: the carrier, X :], the carrier #); end; :: Transition Systems over Subsets of E^omega :: Deterministic Transition Systems definition let E, F; let TS be transition-system over F; attr TS is deterministic means :: REWRITE3:def 1 (the Tran of TS) is Function & not <%> E in rng dom (the Tran of TS) & for s being Element of TS, u, v st u <> v & [s, u] in dom (the Tran of TS) & [s, v] in dom (the Tran of TS) holds not ex w st u ^w = v or v^w = u; end; theorem :: REWRITE3:14 for TS being transition-system over F holds dom (the Tran of TS) = {} implies TS is deterministic; registration let E, F; cluster strict non empty finite deterministic for transition-system over F; end; begin :: Productions definition let X; let TS be transition-system over X; let x, y, z be object; pred x, y -->. z, TS means :: REWRITE3:def 2 [[x, y], z] in the Tran of TS; end; theorem :: REWRITE3:15 for TS being transition-system over X holds 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); theorem :: REWRITE3:16 for TS1 being transition-system over X1, TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 holds x, y -->. z, TS1 implies x, y -->. z, TS2; theorem :: REWRITE3:17 for TS being transition-system over F st the Tran of TS is Function holds x, y -->. z1, TS & x, y -->. z2, TS implies z1 = z2; theorem :: REWRITE3:18 for TS being transition-system over F st not <%>E in rng dom (the Tran of TS) holds not x, <%>E -->. y, TS; theorem :: REWRITE3:19 for TS being deterministic transition-system over F holds u <> v & x, u -->. z1, TS & x, v -->. z2, TS implies not ex w st u^w = v or v^w = u; begin :: Direct Transitions definition let E, F; let TS be transition-system over F; let x1, x2, y1, y2 be object; pred x1, x2 ==>. y1, y2, TS means :: REWRITE3:def 3 ex v, w st v = y2 & x1, w -->. y1, TS & x2 = w^v; end; theorem :: REWRITE3:20 for TS being transition-system over F holds 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); theorem :: REWRITE3:21 for TS1 being transition-system over F1, 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; theorem :: REWRITE3:22 for TS being transition-system over F holds x, u ==>. y, v, TS implies ex w st x, w -->. y, TS & u = w^v; theorem :: REWRITE3:23 for TS being transition-system over F holds x, y -->. z, TS iff x, y ==>. z, <%>E, TS; theorem :: REWRITE3:24 for TS being transition-system over F holds x, v -->. y, TS iff x, v^w ==>. y, w, TS; theorem :: REWRITE3:25 for TS being transition-system over F holds x, u ==>. y, v, TS implies x, u^w ==>. y, v^w, TS; theorem :: REWRITE3:26 for TS being transition-system over F holds x, u ==>. y, v, TS implies len u >= len v; theorem :: REWRITE3:27 for TS being transition-system over F st the Tran of TS is Function holds x1, x2 ==>. y1, z, TS & x1, x2 ==>. y2, z, TS implies y1 = y2; theorem :: REWRITE3:28 for TS being transition-system over F st not <%>E in rng dom ( the Tran of TS) holds not x, z ==>. y, z, TS; theorem :: REWRITE3:29 for TS being transition-system over F st not <%>E in rng dom ( the Tran of TS) holds x, u ==>. y, v, TS implies len u > len v; theorem :: REWRITE3:30 for TS being deterministic transition-system over F holds x1, x2 ==>. y1, z1, TS & x1, x2 ==>. y2, z2, TS implies y1 = y2 & z1 = z2; begin :: ==>.-relation is introduced to define transitions :: using reduction relations from REWRITE1 reserve TS for non empty transition-system over F; reserve s, s9, s1, s2, t, t1, t2 for Element of TS; reserve S for Subset of TS; definition let E, F, TS; func ==>.-relation(TS) -> Relation of [: the carrier of TS, E^omega :] means :: REWRITE3:def 4 [[x1, x2], [y1, y2]] in it iff x1, x2 ==>. y1, y2, TS; end; theorem :: REWRITE3:31 [x, y] in ==>.-relation(TS) implies ex s, v, t, w st x = [s, v] & y = [t, w]; theorem :: REWRITE3:32 [[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); theorem :: REWRITE3:33 x in ==>.-relation(TS) implies ex s, t, v, w st x = [[s, v], [t, w]]; theorem :: REWRITE3:34 for TS1 being non empty transition-system over F1, TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds ==>.-relation(TS1) = ==>.-relation(TS2) ; theorem :: REWRITE3:35 [[x1, x2], [y1, y2]] in ==>.-relation(TS) implies ex v, w st v = y2 & x1, w -->. y1, TS & x2 = w^v; theorem :: REWRITE3:36 [[x, u], [y, v]] in ==>.-relation(TS) implies ex w st x, w -->. y, TS & u = w^v; theorem :: REWRITE3:37 x, y -->. z, TS iff [[x, y], [z, <%>E]] in ==>.-relation(TS); theorem :: REWRITE3:38 x, v -->. y, TS iff [[x, v^w], [y, w]] in ==>.-relation(TS); theorem :: REWRITE3:39 [[x, u], [y, v]] in ==>.-relation(TS) implies [[x, u^w], [y, v^w]] in ==>.-relation(TS); theorem :: REWRITE3:40 [[x, u], [y, v]] in ==>.-relation(TS) implies len u >= len v; theorem :: REWRITE3:41 the Tran of TS is Function implies ([x, [y1, z]] in ==>.-relation(TS) & [x, [y2, z]] in ==>.-relation(TS) implies y1 = y2); theorem :: REWRITE3:42 not <%>E in rng dom (the Tran of TS) implies ([[x, u], [y, v]] in ==>.-relation(TS) implies len u > len v); theorem :: REWRITE3:43 not <%>E in rng dom (the Tran of TS) implies not [[x, z], [y, z] ] in ==>.-relation(TS); theorem :: REWRITE3:44 TS is deterministic implies ([x, y1] in ==>.-relation(TS) & [x, y2] in ==>.-relation(TS) implies y1 = y2); theorem :: REWRITE3:45 TS is deterministic implies ([x, [y1, z1]] in ==>.-relation(TS) & [x, [y2, z2]] in ==>.-relation(TS) implies y1 = y2 & z1 = z2); theorem :: REWRITE3:46 TS is deterministic implies ==>.-relation(TS) is Function-like; begin :: Reduction Sequences of ==>.-relation definition let x, E; func dim2(x, E) -> Element of E^omega equals :: REWRITE3:def 5 x`2 if ex y, u st x = [y , u] otherwise {}; end; theorem :: REWRITE3:47 for P being RedSequence of ==>.-relation(TS), k st k in dom P & k + 1 in dom P holds ex s, v, t, w st P.k = [s, v] & P.(k + 1) = [t, w]; theorem :: REWRITE3:48 for P being RedSequence of ==>.-relation(TS), k 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]; theorem :: REWRITE3:49 for P being RedSequence of ==>.-relation(TS), k 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); theorem :: REWRITE3:50 for TS1 being non empty transition-system over F1, 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); theorem :: REWRITE3:51 for P being RedSequence of ==>.-relation(TS) st ex x, u st P.1 = [x, u] holds for k st k in dom P holds dim2(P.k, E) = (P.k)`2; theorem :: REWRITE3:52 for P being RedSequence of ==>.-relation(TS) st P.len P = [y, w] holds for k st k in dom P ex u st (P.k)`2 = u^w; theorem :: REWRITE3:53 for P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P .len P = [y, w] holds ex u st v = u^w; theorem :: REWRITE3:54 for P being RedSequence of ==>.-relation(TS) st P.1 = [x, u] & P .len P = [y, u] holds for k st k in dom P holds (P.k)`2 = u; theorem :: REWRITE3:55 for P being RedSequence of ==>.-relation(TS), k st k in dom P & k + 1 in dom P holds ex v, w st v = (P.(k + 1))`2 & (P.k)`1, w -->. (P.(k + 1))`1, TS & (P.k)`2 = w^v; theorem :: REWRITE3:56 for P being RedSequence of ==>.-relation(TS), k st k in dom P & k + 1 in dom P & P.k = [x, u] & P.(k + 1) = [y, v] holds ex w st x, w -->. y, TS & u = w^v; theorem :: REWRITE3:57 x, y -->. z, TS iff <*[x, y], [z, <%>E]*> is RedSequence of ==>.-relation(TS) ; theorem :: REWRITE3:58 x, v -->. y, TS iff <*[x, v^w], [y, w]*> is RedSequence of ==>.-relation(TS); theorem :: REWRITE3:59 for P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P .len P = [y, w] holds len v >= len w; theorem :: REWRITE3:60 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; theorem :: REWRITE3:61 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; theorem :: REWRITE3:62 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; theorem :: REWRITE3:63 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; theorem :: REWRITE3:64 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] holds len v > len w or len P = 1 & x = y & v = w; theorem :: REWRITE3:65 not <%>E in rng dom (the Tran of TS) implies for P being RedSequence of ==>.-relation(TS), k st k in dom P & k + 1 in dom P holds (P.k)`2 <> (P.(k + 1))`2; theorem :: REWRITE3:66 not <%>E in rng dom (the Tran of TS) implies for P being RedSequence of ==>.-relation(TS), k, l st k in dom P & l in dom P & k < l holds (P.k)`2 <> (P.l)`2; theorem :: REWRITE3:67 TS is deterministic implies for P, Q being RedSequence of ==>.-relation(TS) st P.1 = Q.1 holds for k st k in dom P & k in dom Q holds P.k = Q.k; theorem :: REWRITE3:68 TS is deterministic implies for P, Q being RedSequence of ==>.-relation(TS) st P.1 = Q.1 & len P = len Q holds P = Q; theorem :: REWRITE3:69 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; begin :: Reductions theorem :: REWRITE3:70 ==>.-relation(TS) reduces [x, v], [y, w] implies ex u st v = u^w; theorem :: REWRITE3:71 ==>.-relation(TS) reduces [x, u], [y, v] implies ==>.-relation( TS) reduces [x, u^w], [y, v^w]; theorem :: REWRITE3:72 x, y -->. z, TS implies ==>.-relation(TS) reduces [x, y], [z, <%>E]; theorem :: REWRITE3:73 x, v -->. y, TS implies ==>.-relation(TS) reduces [x, v^w], [y, w]; theorem :: REWRITE3:74 x1, x2 ==>. y1, y2, TS implies ==>.-relation(TS) reduces [x1, x2 ], [y1, y2]; theorem :: REWRITE3:75 ==>.-relation(TS) reduces [x, v], [y, w] implies len v >= len w; theorem :: REWRITE3:76 ==>.-relation(TS) reduces [x, w], [y, v^w] implies v = <%>E; theorem :: REWRITE3:77 not <%>E in rng dom (the Tran of TS) implies (==>.-relation(TS) reduces [x, v], [y, w] implies len v > len w or x = y & v = w ); theorem :: REWRITE3:78 not <%>E in rng dom (the Tran of TS) implies (==>.-relation(TS) reduces [x, u], [y, u] implies x = y); theorem :: REWRITE3:79 not <%>E in rng dom (the Tran of TS) implies (==>.-relation(TS) reduces [x, <%e%>], [y, <%>E] implies [[x, <%e%>], [y, <%>E]] in ==>.-relation( TS)); theorem :: REWRITE3:80 TS is deterministic implies (==>.-relation(TS) reduces x, [y1, z ] & ==>.-relation(TS) reduces x, [y2, z] implies y1 = y2); begin :: Transitions definition let E, F, TS; let x1, x2, y1, y2 be object; pred x1, x2 ==>* y1, y2, TS means :: REWRITE3:def 6 ==>.-relation(TS) reduces [x1, x2], [y1, y2]; end; theorem :: REWRITE3:81 for TS1 being non empty transition-system over F1, 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 x1, x2 ==>* y1, y2, TS1 implies x1, x2 ==>* y1, y2, TS2; theorem :: REWRITE3:82 x, y ==>* x, y, TS; theorem :: REWRITE3:83 x1, x2 ==>* y1, y2, TS & y1, y2 ==>* z1, z2, TS implies x1, x2 ==>* z1, z2, TS; theorem :: REWRITE3:84 x, y -->. z, TS implies x, y ==>* z, <%>E, TS; theorem :: REWRITE3:85 x, v -->. y, TS implies x, v^w ==>* y, w, TS; theorem :: REWRITE3:86 x, u ==>* y, v, TS implies x, u^w ==>* y, v^w, TS; theorem :: REWRITE3:87 x1, x2 ==>. y1, y2, TS implies x1, x2 ==>* y1, y2, TS; theorem :: REWRITE3:88 x, v ==>* y, w, TS implies ex u st v = u^w; theorem :: REWRITE3:89 x, v ==>* y, w, TS implies len w <= len v; theorem :: REWRITE3:90 x, w ==>* y, v^w, TS implies v = <%>E; theorem :: REWRITE3:91 not <%>E in rng dom (the Tran of TS) implies (x, u ==>* y, u, TS iff x = y); theorem :: REWRITE3:92 not <%>E in rng dom (the Tran of TS) implies (x, <%e%> ==>* y, <%>E, TS implies x, <%e%> ==>. y, <%>E, TS); theorem :: REWRITE3:93 TS is deterministic implies ( x1, x2 ==>* y1, z, TS & x1, x2 ==>* y2, z, TS implies y1 = y2); begin :: Acceptance of Words definition let E, F, TS; let x1, x2, y be object; pred x1, x2 ==>* y, TS means :: REWRITE3:def 7 x1, x2 ==>* y, <%>E, TS; end; theorem :: REWRITE3:94 for TS1 being non empty transition-system over F1, 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, y ==>* z, TS1 implies x, y ==>* z, TS2; theorem :: REWRITE3:95 x, <%>E ==>* x, TS; theorem :: REWRITE3:96 x, u ==>* y, TS implies x, u^v ==>* y, v, TS; theorem :: REWRITE3:97 x, y -->. z, TS implies x, y ==>* z, TS; theorem :: REWRITE3:98 x1, x2 ==>. y, <%>E, TS implies x1, x2 ==>* y, TS; theorem :: REWRITE3:99 x, u ==>* y, TS & y, v ==>* z, TS implies x, u^v ==>* z, TS; theorem :: REWRITE3:100 not <%>E in rng dom (the Tran of TS) implies (x, <%>E ==>* y, TS iff x = y); theorem :: REWRITE3:101 not <%>E in rng dom (the Tran of TS) implies (x, <%e%> ==>* y, TS implies x, <%e%> ==>. y, <%>E, TS); theorem :: REWRITE3:102 TS is deterministic implies ( x1, x2 ==>* y1, TS & x1, x2 ==>* y2, TS implies y1 = y2); begin :: Reachable States definition let E, F, TS, x, X; func x-succ_of (X, TS) -> Subset of TS equals :: REWRITE3:def 8 { s : ex t st t in X & t, x ==>* s, TS }; end; theorem :: REWRITE3:103 s in x-succ_of (X, TS) iff ex t st t in X & t, x ==>* s, TS; theorem :: REWRITE3:104 not <%>E in rng dom (the Tran of TS) implies <%>E-succ_of (S, TS) = S; theorem :: REWRITE3:105 for TS1 being non empty transition-system over F1, 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);