:: Labelled State Transition Systems
:: by Micha{\l} Trybulec
::
:: Received May 5, 2009
:: Copyright (c) 2009-2019 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);