:: Labelled State Transition Systems
:: by Micha{\l} Trybulec
::
:: Received May 5, 2009
:: Copyright (c) 2009-2026 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;
definitions TARSKI, STRUCT_0;
expansions STRUCT_0;
theorems AFINSQ_1, CALCUL_1, FLANG_1, FLANG_2, FUNCT_1, NAT_1, RELAT_1,
RELSET_1, REWRITE1, TARSKI, XREAL_1, XXREAL_0, ZFMISC_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, REWRITE2, XTUPLE_0;
schemes FINSEQ_1, NAT_1, RELSET_1;
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;
::$CT
theorem Th2:
for p being FinSequence holds p <> {} implies
ex q being FinSequence, x st p = q^<*x*> & len p = len q + 1
proof
let p be FinSequence;
assume p <> {};
then consider q being FinSequence, x being object such that
A1: p = q^<*x*> by FINSEQ_1:46;
take q, x;
len p = len q + len <*x*> by A1,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:40;
hence thesis by A1;
end;
theorem Th3:
for p being FinSequence st k in dom p & not k + 1 in dom p holds len p = k
proof
let p be FinSequence such that
A1: k in dom p and
A2: not k + 1 in dom p;
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 thesis by A3,A4,NAT_1:22;
end;
begin :: Preliminaries - RedSequences
theorem Th4:
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
proof
let R be Relation, P be RedSequence of R, q1, q2 be FinSequence such that
A1: P = q1^q2 and
A2: len q1 > 0 and
A3: len q2 > 0;
now
let i be Nat;
assume that
A4: i in dom q1 and
A5: i + 1 in dom q1;
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;
end;
hence q1 is RedSequence of R by A2,REWRITE1:def 2;
now
let i be Nat;
assume that
A14: i in dom q2 and
A15: i + 1 in dom q2;
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;
end;
hence q2 is RedSequence of R by A3,REWRITE1:def 2;
end;
theorem Th5:
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
proof
let R be Relation, P be RedSequence of R such that
A1: len P > 1;
consider x being object, 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 thesis by A2,A3,A4;
end;
theorem
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
proof
let R be Relation, P be RedSequence of R such that
A1: len P > 1;
consider Q being FinSequence, x 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 thesis by A2,A3,A4;
end;
theorem
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)
proof
let R be Relation, P be RedSequence of R;
assume len P > 1;
then consider Q being RedSequence of R such that
A1: P = <*P.1*>^Q & len Q + 1 = len P by Th5;
take Q;
thus thesis by A1,FINSEQ_3:103;
end;
theorem Th8:
for R being Relation holds <*x, y*> is RedSequence of R implies [x, y] in R
proof
let R be Relation;
set P = <*x, y*>;
A1: P.1 = x & P.2 = y;
len P = 2 by FINSEQ_1:44;
then 1 in dom P & 1 + 1 in dom P by FINSEQ_3:25;
hence thesis by A1,REWRITE1:def 2;
end;
begin :: Preliminaries - XFinSequences
theorem Th9:
w = u^v implies len u <= len w & len v <= len w
proof
assume w = u^v;
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 thesis by XREAL_1:6;
end;
theorem Th10:
w = u^v & u <> <%>E & v <> <%>E implies len u < len w & len v < len w
proof
assume that
A1: w = u^v and
A2: u <> <%>E and
A3: v <> <%>E;
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 thesis by A3,A4,XREAL_1:6,8;
end;
theorem
w1^v1 = w2^v2 & ( len w1 = len w2 or len v1 = len v2 ) implies w1 = w2
& v1 = v2
proof
assume that
A1: w1^v1 = w2^v2 and
A2: len w1 = len w2 or len v1 = len v2;
A3: len w1 + len v1 = len (w2^v2) by A1,AFINSQ_1:17
.= len w2 + len v2 by AFINSQ_1:17;
now
let k be Nat;
assume
A4: k in dom w1;
hence w1.k = (w2^v2).k by A1,AFINSQ_1:def 3
.= w2.k by A2,A3,A4,AFINSQ_1:def 3;
end;
hence w1 = w2 by A2,A3,AFINSQ_1:8;
hence thesis by A1,AFINSQ_1:28;
end;
theorem Th12:
w1^v1 = w2^v2 & ( len w1 <= len w2 or len v1 >= len v2 ) implies
ex u st w1^u = w2 & v1 = u^v2
proof
assume that
A1: w1^v1 = w2^v2 and
A2: len w1 <= len w2 or len v1 >= len 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;
thus w1^u = w2 by A3;
w2^v2 = w1^(u^v2) by A3,AFINSQ_1:27;
hence thesis by A1,AFINSQ_1:28;
end;
theorem Th13:
w1^v1 = w2^v2 implies (ex u st w1^u = w2 & v1 = u^v2) or ex u st
w2^u = w1 & v2 = u^v1
proof
A1: len w1 < len w2 or len w1 >= len w2;
assume w1^v1 = w2^v2;
hence thesis by A1,Th12;
end;
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
:Def1:
(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
for TS being transition-system over F holds dom (the Tran of TS)
= {} implies TS is deterministic
proof
let TS be transition-system over F;
assume dom (the Tran of TS) = {};
then
(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;
hence thesis;
end;
registration
let E, F;
cluster strict non empty finite deterministic for transition-system over F;
existence
proof
set X = the non empty finite set;
reconsider T = {} as Relation of [: X, F :], X by RELSET_1:12;
take TS = transition-system (# X, T #);
thus TS is strict;
thus TS is non empty;
thus the carrier of TS is finite;
thus TS is deterministic;
end;
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
[[x, y], z] in the Tran of TS;
end;
theorem Th15:
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)
proof
let TS be transition-system over X;
assume x, y -->. z, TS;
then
A1: [[x, y], z] in the Tran of TS;
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;
[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,def 13;
thus z in rng (the Tran of TS) by A1,XTUPLE_0:def 13;
end;
theorem
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 Th17:
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
by FUNCT_1:def 1;
theorem
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 TS be transition-system over F such that
A1: not <%>E in rng dom (the Tran of TS);
assume x, <%>E -->. y, TS;
then [[x, <%>E], y] in the Tran of TS;
then [x, <%>E] in dom (the Tran of TS) by XTUPLE_0:def 12;
hence contradiction by A1,XTUPLE_0:def 13;
end;
theorem Th19:
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
proof
let TS be deterministic transition-system over F;
assume that
A1: u <> v and
A2: x, u -->. z1, TS and
A3: x, v -->. z2, TS;
x in TS by A2,Th15;
then reconsider x as Element of TS;
[[x, v], z2] in the Tran of TS by A3;
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;
then [x, u] in dom the Tran of TS by XTUPLE_0:def 12;
hence thesis by A1,A4,Def1;
end;
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
ex v, w st v = y2 & x1, w -->. y1, TS & x2 = w^v;
end;
theorem Th20:
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)
by Th15;
theorem Th21:
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
proof
let TS1 be transition-system over F1, TS2 be transition-system over F2 such
that
A1: the Tran of TS1 = the Tran of TS2 and
A2: x1, x2 ==>. y1, y2, TS1;
consider v, w such that
A3: v = y2 & x1, w -->. y1, TS1 & x2 = w^v by A2;
take v, w;
thus thesis by A1,A3;
end;
theorem
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 Th23:
for TS being transition-system over F holds x, y -->. z, TS iff
x, y ==>. z, <%>E, TS
proof
let TS be transition-system over F;
thus x, y -->. z, TS implies x, y ==>. z, <%>E, TS
proof
assume
A1: x, y -->. z, TS;
then y in F by Th15;
then reconsider w = y as Element of E^omega;
w = w^{};
hence thesis by A1;
end;
assume x, y ==>. z, <%>E, TS;
then ex v, w st v = <%>E & x, w -->. z, TS & y = w^v;
hence thesis;
end;
theorem Th24:
for TS being transition-system over F holds x, v -->. y, TS iff
x, v^w ==>. y, w, TS
by AFINSQ_1:28;
theorem Th25:
for TS being transition-system over F holds x, u ==>. y, v, TS
implies x, u^w ==>. y, v^w, TS
proof
let TS be transition-system over F;
assume x, u ==>. y, v, TS;
then consider u1 such that
A1: x, u1 -->. y, TS and
A2: u = u1^v;
u^w = u1^(v^w) by A2,AFINSQ_1:27;
hence thesis by A1;
end;
theorem Th26:
for TS being transition-system over F holds x, u ==>. y, v, TS
implies len u >= len v
by Th9;
theorem Th27:
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
proof
let TS be transition-system over F such that
A1: the Tran of TS is Function;
assume that
A2: x1, x2 ==>. y1, z, TS and
A3: x1, x2 ==>. y2, z, TS;
consider v1, w1 such that
A4: v1 = z and
A5: x1, w1 -->. y1, TS and
A6: x2 = w1^v1 by A2;
consider v2, w2 such that
A7: v2 = z and
A8: x1, w2 -->. y2, TS and
A9: x2 = w2^v2 by A3;
w1 = w2 by A4,A6,A7,A9,AFINSQ_1:28;
hence thesis by A1,A5,A8,Th17;
end;
theorem Th28:
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 TS be transition-system over F such that
A1: not <%>E in rng dom (the Tran of TS);
assume x, z ==>. y, z, TS;
then consider v, w such that
A2: v = z and
A3: x, w -->. y, TS and
A4: z = w^v;
[[x, w], y] in the Tran of TS by A3;
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;
end;
theorem Th29:
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
proof
let TS be transition-system over F such that
A1: not <%>E in rng dom (the Tran of TS);
assume
A2: x, u ==>. y, v, TS;
then consider w such that
A3: x, w -->. y, TS and
A4: u = w^v;
A5: w in rng dom (the Tran of TS) by A3,Th15;
per cases;
suppose
A6: v = <%>E;
then u <> <%>E by A1,A2,Th28;
then len u > 0;
hence thesis by A6;
end;
suppose
v <> <%>E;
hence thesis by A1,A4,A5,Th10;
end;
end;
theorem Th30:
for TS being deterministic transition-system over F holds x1, x2
==>. y1, z1, TS & x1, x2 ==>. y2, z2, TS implies y1 = y2 & z1 = z2
proof
let TS be deterministic transition-system over F;
assume that
A1: x1, x2 ==>. y1, z1, TS and
A2: x1, x2 ==>. y2, z2, TS;
consider v2, w2 such that
A3: v2 = z2 and
A4: x1, w2 -->. y2, TS and
A5: x2 = w2^v2 by A2;
consider v1, w1 such that
A6: v1 = z1 and
A7: x1, w1 -->. y1, TS and
A8: x2 = w1^v1 by A1;
A9: the Tran of TS is Function by Def1;
(ex u9 st w1^u9 = w2 & v1 = u9^v2) or ex u9 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 thesis by A1,A2,A6,A3,A9,Th27;
end;
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
:Def4:
[[x1, x2], [y1, y2]] in it iff x1, x2 ==>. y1, y2, TS;
existence
proof
defpred P[Element of [: the carrier of TS, E^omega :], Element of [: the
carrier of TS, E^omega :]] means ex x1, x2, y1, y2 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 P[s, t] from RELSET_1:sch 2;
take R;
now
let x1, x2, y1, y2;
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,def 19;
thus x1, x2 ==>. y1, y2, TS implies [[x1, x2], [y1, y2]] in R
proof
assume
A3: x1, x2 ==>. y1, y2, TS;
then y1 in TS by Th20;
then
A4: y1 in the carrier of TS;
x1 in TS by A3,Th20;
then
A5: x1 in the carrier of TS;
y2 in E^omega by A3;
then
A6: t in [: the carrier of TS, E^omega :] by A4,ZFMISC_1:def 2;
x2 in E^omega by A3;
then s in [: the carrier of TS, E^omega :] by A5,ZFMISC_1:def 2;
hence thesis by A1,A3,A6;
end;
assume
A7: [[x1, x2], [y1, y2]] in R;
then [x1, x2] in dom R & [y1, y2] in rng R by XTUPLE_0:def 12,def 13;
then consider x19, x29, y19, y29 being object such that
A8: [x19, x29] = s and
A9: [y19, y29] = t 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;
end;
hence thesis;
end;
uniqueness
proof
let R1, R2 be Relation of [: the carrier of TS, E^omega :] such that
A12: [[x1, x2], [y1, y2]] in R1 iff x1, x2 ==>. y1, y2, TS and
A13: [[x1, x2], [y1, y2]] in R2 iff x1, x2 ==>. y1, y2, TS;
now
let s, t be Element of [: the carrier of TS, E^omega :];
consider x, u being object 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 as Element of E^omega by A15;
reconsider x as Element of TS by A14;
consider y, v being object 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 as Element of E^omega by A18;
reconsider 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;
end;
hence thesis by RELSET_1:def 2;
end;
end;
theorem Th31:
[x, y] in ==>.-relation(TS) implies ex s, v, t, w st x = [s, v] & y = [t, w]
proof
assume
A1: [x, y] in ==>.-relation(TS);
then y in [: the carrier of TS, E^omega :] by ZFMISC_1:87;
then
A2: ex y1, y2 being object
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 object
st x1 in the carrier of TS & x2 in E^omega & x = [x1, x2] by
ZFMISC_1:def 2;
hence thesis by A2;
end;
theorem Th32:
[[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)
proof
assume [[x1, x2], [y1, y2]] in ==>.-relation(TS);
then x1, x2 ==>. y1, y2, TS by Def4;
hence thesis by Th20;
end;
theorem Th33:
x in ==>.-relation(TS) implies ex s, t, v, w st x = [[s, v], [t, w]]
proof
assume
A1: x in ==>.-relation(TS);
then consider y, z being object such that
A2: x = [y, z] by RELAT_1:def 1;
ex s, v, t, w st y = [s, v] & z = [t, w] by A1,A2,Th31;
hence thesis by A2;
end;
theorem Th34:
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)
proof
let TS1 be non empty transition-system over F1, TS2 be non empty
transition-system over F2 such that
A1: the Tran of TS1 = the Tran of TS2;
A2: now
let x be object;
assume
A3: x in ==>.-relation(TS1);
then consider s, t being Element of TS1, v, w 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;
end;
now
let x be object;
assume
A5: x in ==>.-relation(TS2);
then consider s, t being Element of TS2, v, w 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;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th35:
[[x1, x2], [y1, y2]] in ==>.-relation(TS) implies ex v, w st v =
y2 & x1, w -->. y1, TS & x2 = w^v
proof
assume [[x1, x2], [y1, y2]] in ==>.-relation(TS);
then x1, x2 ==>. y1, y2, TS by Def4;
hence thesis;
end;
theorem Th36:
[[x, u], [y, v]] in ==>.-relation(TS) implies ex w st x, w -->.
y, TS & u = w^v
proof
assume [[x, u], [y, v]] in ==>.-relation(TS);
then x, u ==>. y, v, TS by Def4;
hence thesis;
end;
theorem Th37:
x, y -->. z, TS iff [[x, y], [z, <%>E]] in ==>.-relation(TS)
proof
thus x, y -->. z, TS implies [[x, y], [z, <%>E]] in ==>.-relation(TS)
proof
assume x, y -->. z, TS;
then x, y ==>. z, <%>E, TS by Th23;
hence thesis by Def4;
end;
assume [[x, y], [z, <%>E]] in ==>.-relation(TS);
then x, y ==>. z, <%>E, TS by Def4;
hence thesis;
end;
theorem Th38:
x, v -->. y, TS iff [[x, v^w], [y, w]] in ==>.-relation(TS)
proof
thus x, v -->. y, TS implies [[x, v^w], [y, w]] in ==>.-relation(TS)
proof
assume x, v -->. y, TS;
then x, v^w ==>. y, w, TS;
hence thesis by Def4;
end;
assume [[x, v^w], [y, w]] in ==>.-relation(TS);
then x, v^w ==>. y, w, TS by Def4;
hence thesis by Th24;
end;
theorem
[[x, u], [y, v]] in ==>.-relation(TS) implies [[x, u^w], [y, v^w]] in
==>.-relation(TS)
proof
assume [[x, u], [y, v]] in ==>.-relation(TS);
then x, u ==>. y, v, TS by Def4;
then x, u^w ==>. y, v^w, TS by Th25;
hence thesis by Def4;
end;
theorem
[[x, u], [y, v]] in ==>.-relation(TS) implies len u >= len v
proof
assume [[x, u], [y, v]] in ==>.-relation(TS);
then x, u ==>. y, v, TS by Def4;
hence thesis by Th26;
end;
theorem
the Tran of TS is Function implies ([x, [y1, z]] in ==>.-relation(TS)
& [x, [y2, z]] in ==>.-relation(TS) implies y1 = y2)
proof
assume
A1: the Tran of TS is Function;
assume that
A2: [x, [y1, z]] in ==>.-relation(TS) and
A3: [x, [y2, z]] in ==>.-relation(TS);
consider s, v, t, w 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 thesis by A1,Th27;
end;
theorem
not <%>E in rng dom (the Tran of TS) implies ([[x, u], [y, v]] in
==>.-relation(TS) implies len u > len v)
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
assume [[x, u], [y, v]] in ==>.-relation(TS);
then x, u ==>. y, v, TS by Def4;
hence thesis by A1,Th29;
end;
theorem Th43:
not <%>E in rng dom (the Tran of TS) implies not [[x, z], [y, z]
] in ==>.-relation(TS)
proof
assume not <%>E in rng dom (the Tran of TS);
then not x, z ==>. y, z, TS by Th28;
hence thesis by Def4;
end;
theorem Th44:
TS is deterministic implies ([x, y1] in ==>.-relation(TS) & [x,
y2] in ==>.-relation(TS) implies y1 = y2)
proof
assume
A1: TS is deterministic;
assume that
A2: [x, y1] in ==>.-relation(TS) and
A3: [x, y2] in ==>.-relation(TS);
consider s2, v2, t2, w2 such that
x = [s2, v2] and
A4: y2 = [t2, w2] by A3,Th31;
consider s1, v1, t1, w1 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 thesis by A1,A6,A4,A7,A8,Th30;
end;
theorem
TS is deterministic implies ([x, [y1, z1]] in ==>.-relation(TS) & [x,
[y2, z2]] in ==>.-relation(TS) implies y1 = y2 & z1 = z2)
proof
assume
A1: TS is deterministic;
assume
[x, [y1, z1]] in ==>.-relation(TS) & [x, [y2, z2]] in ==>.-relation( TS);
then [y1, z1] = [y2, z2] by A1,Th44;
hence thesis by XTUPLE_0:1;
end;
theorem
TS is deterministic implies ==>.-relation(TS) is Function-like
proof
assume TS is deterministic;
then
for x, y, z being object
st [x, y] in ==>.-relation(TS) & [x, z] in ==>.-relation(TS)
holds y = z by Th44;
hence thesis by FUNCT_1:def 1;
end;
begin :: Reduction Sequences of ==>.-relation
definition
let x, E;
func dim2(x, E) -> Element of E^omega equals
:Def5:
x`2 if ex y, u st x = [y
, u] otherwise {};
coherence
proof
thus (ex y, u st x = [y, u]) implies x`2 is Element of E^omega;
{} = <%>E;
hence thesis;
end;
consistency;
end;
theorem Th47:
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]
proof
let P be RedSequence of ==>.-relation(TS), k;
assume k in dom P & k + 1 in dom P;
then [P.k, P.(k + 1)] in ==>.-relation(TS) by REWRITE1:def 2;
hence thesis by Th31;
end;
theorem Th48:
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]
proof
let P be RedSequence of ==>.-relation(TS), k;
assume k in dom P & k + 1 in dom P;
then ex s, v, t, w st P.k = [s, v] & P.(k + 1) = [t, w] by Th47;
hence thesis;
end;
theorem Th49:
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)
proof
let P be RedSequence of ==>.-relation(TS), k;
assume k in dom P & k + 1 in dom P;
then
A1: [P.k, P.(k + 1)] in ==>.-relation(TS) by REWRITE1:def 2;
then consider s, v, t, w 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;
thus thesis by A2,A3;
end;
theorem
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)
proof
let TS1 be non empty transition-system over F1, TS2 be non empty
transition-system over F2 such that
A1: the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran
of TS2;
let P be RedSequence of ==>.-relation(TS1);
A2: now
let i be Nat;
assume i in dom P & i + 1 in dom P;
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;
end;
len P > 0;
hence thesis by A2,REWRITE1:def 2;
end;
theorem Th51:
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
proof
let P be RedSequence of ==>.-relation(TS);
given x, u such that
A1: P.1 = [x, u];
let k such that
A2: k in dom P;
per cases;
suppose
A3: k > 1;
A4: k <= len P by A2,FINSEQ_3:25;
consider l 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 object
st x1 in the carrier of TS & y1 in E^omega & P .k = [x1, y1]
by A7,ZFMISC_1:def 2;
hence thesis by Def5;
end;
suppose
A8: k <= 1;
k >= 1 by A2,FINSEQ_3:25;
then k = 1 by A8,XXREAL_0:1;
hence thesis by A1,Def5;
end;
end;
theorem Th52:
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
proof
let P be RedSequence of ==>.-relation(TS);
assume P.len P = [y, w];
then
A1:(P.len P)`2 = {}^w .= <%>E^w;
defpred P[Nat] means len P - $1 in dom P implies ex u st (P.(len P - $1))`2
= u^w;
A2: now
let k;
assume
A3: P[k];
now
set len2 = len P - k;
set len1 = len P - (k + 1);
A4: len1 + 1 = len2;
assume
A5: len P - (k + 1) in dom P;
thus ex u st (P.(len P - (k + 1)))`2 = u^w
proof
per cases;
suppose
A6: len P - k in dom P;
then consider u1 such that
A7: (P.len2)`2 = u1^w by A3;
A8: [P.len1, P.len2] 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 such that
A9: P.len1 = [x, v1] and
A10: P.len2 = [y, v2] by Th31;
x, v1 ==>. y, v2, TS by A8,A9,A10,Def4;
then consider u2 such that
x, u2 -->. y, TS and
A11: v1 = u2^v2;
take u2^u1;
(P.len1)`2 = u2^v2 by A9,A11
.= u2^(u1^w) by A7,A10
.= u2^u1^w by AFINSQ_1:27;
hence thesis;
end;
suppose
not len P - k in dom P;
then len1 = len P - 0 by A5,A4,Th3;
hence thesis;
end;
end;
end;
hence P[k + 1];
end;
A12: P[0] by A1;
A13: for k holds P[k] from NAT_1:sch 2(A12, A2);
hereby
let k such that
A14: k in dom P;
k <= len P by A14,FINSEQ_3:25;
then consider l such that
A15: k + l = len P by NAT_1:10;
k + l - l = len P - l by A15;
hence ex u st (P.k)`2 = u^w by A13,A14;
end;
end;
theorem Th53:
for P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P
.len P = [y, w] holds ex u st v = u^w
proof
let P be RedSequence of ==>.-relation(TS) such that
A1: P.1 = [x, v] and
A2: P.len P = [y, w];
0 + 1 <= len P by NAT_1:8;
then 1 in dom P by FINSEQ_3:25;
then consider u such that
A3: (P.1)`2 = u^w by A2,Th52;
take u;
thus thesis by A1,A3;
end;
theorem Th54:
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
proof
defpred P[Nat] means for P being RedSequence of ==>.-relation(TS), x, y st P
.1 = [x, u] & P.len P = [y, u] & len P = $1 holds (for k st k in dom P holds (P
.k)`2 = u);
A1: now
let k;
assume
A2: P[k];
now
let P be RedSequence of ==>.-relation(TS), x, y such that
A3: P.1 = [x, u] and
A4: P.len P = [y, u] and
A5: len P = k + 1;
per cases;
suppose
A6: k = 0;
hereby
let l;
assume l in dom P;
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;
end;
end;
suppose
k <> 0;
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 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 such that
A18: u1 = v^u by A16,Th53;
A19: {}^u1 = u1;
u = w^v^u by A18,A11,AFINSQ_1:27;
then w^v = {} by FLANG_2:4;
then
A20: Q.1 = [(P.(1 + 1))`1, u] by A16,A11,A19,AFINSQ_1:30;
hereby
let l;
assume
A21: l in dom P;
then
A22: 1 <= l by FINSEQ_3:25;
then reconsider l9 = l - 1 as Nat by NAT_1:21;
1 + 1 <= l + 1 by A22,XREAL_1:6;
then
A23: 1 + 1 = l + 1 or 1 + 1 <= l by NAT_1:8;
l <= len P by A21,FINSEQ_3:25;
then
1 = l or 1 + 1 - 1 <= l - 1 & l - 1 <= len Q + 1 - 1 by A14,A23,XREAL_1:9;
then
A24: l = 1 or l9 in dom Q by FINSEQ_3:25;
per cases by A24;
suppose
l = 1;
hence (P.l)`2 = u by A3;
end;
suppose
A25: (l - 1) in dom Q;
then l - 1 <= len Q by FINSEQ_3:25;
then
A26: l - 1 + 1 <= len Q + 1 by XREAL_1:6;
1 <= l - 1 by A25,FINSEQ_3:25;
then
A27: 1 + 0 < l - 1 + 1 by XREAL_1:6;
(Q.(l - 1))`2 = u by A2,A5,A14,A17,A20,A25;
hence (P.l)`2 = u by A13,A14,A12,A27,A26,FINSEQ_1:24;
end;
end;
end;
end;
hence P[k + 1];
end;
A28: P[0];
for k holds P[k] from NAT_1:sch 2(A28, A1);
hence thesis;
end;
theorem
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
proof
let P be RedSequence of ==>.-relation(TS), k such that
A1: k in dom P & k + 1 in dom P;
consider s, u, t, v 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 such that
A4: v1 = v and
A5: s, w1 -->. t, TS and
A6: u = w1^v1 by Th35;
take v1, w1;
thus v1 = (P.(k + 1))`2 by A3,A4;
(P.k)`1, w1 -->. t, TS by A2,A5;
hence thesis by A2,A3,A6;
end;
theorem
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
proof
let P be RedSequence of ==>.-relation(TS), k;
assume k in dom P & k + 1 in dom P & P.k = [x, u] & P.(k + 1) = [y, v];
then [[x, u], [y, v]] in ==>.-relation(TS) by REWRITE1:def 2;
hence thesis by Th36;
end;
theorem Th57:
x, y -->. z, TS iff <*[x, y], [z, <%>E]*> is RedSequence of ==>.-relation(TS)
proof
thus x, y -->. z, TS implies <*[x, y], [z, <%>E]*> is RedSequence of
==>.-relation(TS)
proof
assume x, y -->. z, TS;
then [[x, y], [z, <%>E]] in ==>.-relation(TS) by Th37;
hence thesis by REWRITE1:7;
end;
assume <*[x, y], [z, <%>E]*> is RedSequence of ==>.-relation(TS);
then [[x, y], [z, <%>E]] in ==>.-relation(TS) by Th8;
hence thesis by Th37;
end;
theorem Th58:
x, v -->. y, TS iff <*[x, v^w], [y, w]*> is RedSequence of ==>.-relation(TS)
proof
thus x, v -->. y, TS implies <*[x, v^w], [y, w]*> is RedSequence of
==>.-relation(TS)
proof
assume x, v -->. y, TS;
then [[x, v^w], [y, w]] in ==>.-relation(TS) by Th38;
hence thesis by REWRITE1:7;
end;
assume <*[x, v^w], [y, w]*> is RedSequence of ==>.-relation(TS);
then [[x, v^w], [y, w]] in ==>.-relation(TS) by Th8;
hence thesis by Th38;
end;
theorem Th59:
for P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P
.len P = [y, w] holds len v >= len w
proof
let P be RedSequence of ==>.-relation(TS);
assume P.1 = [x, v] & P.len P = [y, w];
then ex u st v = u^w by Th53;
hence thesis by Th9;
end;
theorem Th60:
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
proof
defpred P[Nat] means for P being RedSequence of ==>.-relation(TS), x, y st P
.1 = [x, u] & P.len P = [y, u] & len P = $1 & $1 <> 1 holds contradiction;
assume
A1: not <%>E in rng dom (the Tran of TS);
A2: now
let k;
assume P[k];
now
let P be RedSequence of ==>.-relation(TS), x, y such that
A3: P.1 = [x, u] and
A4: P.len P = [y, u] and
A5: len P = k + 1 & k + 1 <> 1;
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;
end;
hence P[k + 1];
end;
let P be RedSequence of ==>.-relation(TS) such that
A9: P.1 = [x, u] & P.len P = [y, u];
A10: P[0];
for k holds P[k] from NAT_1:sch 2(A10, A2);
hence len P = 1 by A9;
hence thesis by A9,XTUPLE_0:1;
end;
theorem Th61:
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
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
let P be RedSequence of ==>.-relation(TS) such that
A2: (P.1)`2 = (P.len P)`2;
per cases;
suppose
A3: len P <= 1;
len P >= 0 + 1 by NAT_1:13;
hence len P = 1 by A3,XXREAL_0:1;
end;
suppose
A4: 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, v2, t2, w2 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, v1, t1, w1 such that
A10: P.1 = [s1, v1] and
P.(1 + 1) = [t1, w1] by A7,Th47;
(P.len P)`2 = w2 by A9;
then v1 = w2 by A2,A10;
hence len P = 1 by A1,A10,A9,Th60;
end;
end;
theorem Th62:
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
proof
defpred P[Nat] means for P being RedSequence of ==>.-relation(TS), u, x 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);
A2: now
let k;
assume
A3: for n st n < k holds P[n];
now
let P be RedSequence of ==>.-relation(TS), u, x such that
A4: len u = k and
A5: P.1 = [x, u] and
A6: P.len P = [y, <%>E];
per cases;
suppose
len u < 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;
end;
suppose
A7: len u >= 1;
A8: len P <> 1
proof
assume len P = 1;
then u = <%>E by A5,A6,XTUPLE_0:1;
hence contradiction by A7;
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 such that
A18: x, v -->. (P.(1 + 1))`1, TS & u = v^u1;
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;
end;
end;
hence P[k];
end;
for k holds P[k] from NAT_1:sch 4(A2);
hence thesis;
end;
theorem Th63:
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
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
let P be RedSequence of ==>.-relation(TS) such that
A2: P.1 = [x, <%e%>] & P.len P = [y, <%>E];
len P <= len <%e%> + 1 by A1,A2,Th62;
then
len P <= 1 + 1 by AFINSQ_1:34;
then
A3: len P = 0 or ... or len P = 2;
len P <> 1 by A2,XTUPLE_0:1;
hence thesis by A3;
end;
theorem Th64:
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
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
let P be RedSequence of ==>.-relation(TS) such that
A2: P.1 = [x, v] & P.len P = [y, w];
consider u such that
A3: v = u^w by A2,Th53;
A4: len v >= len w by A2,Th59;
per cases;
suppose
len v > len w;
hence thesis;
end;
suppose
A5: len v <= len w;
A6: len v = len u + len w by A3,AFINSQ_1:17;
len v = len w by A4,A5,XXREAL_0:1;
then u = <%>E by A6;
hence thesis by A1,A2,Th60,A3;
end;
end;
theorem
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
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
let P be RedSequence of ==>.-relation(TS), k such that
A2: k in dom P & k + 1 in dom P;
consider s, u, t, v 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;
hence thesis by A4;
end;
theorem Th66:
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
proof
defpred P[Nat] means for P being RedSequence of ==>.-relation(TS), k, l 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);
A2: now
let i;
assume
A3: P[i];
now
let P be RedSequence of ==>.-relation(TS), k, l such that
A4: len P = i + 1 and
A5: k in dom P and
A6: l in dom P and
A7: k < l;
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;
per cases;
suppose
k = 1 & l = len P;
hence (P.k)`2 <> (P.l)`2 by A1,A7,Th61;
end;
suppose
A13: k <> 1 & l = len P;
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;
end;
suppose
A25: l <> len P;
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;
end;
end;
hence P[i + 1];
end;
A32: P[0];
A33: for i holds P[i] from NAT_1:sch 2(A32, A2);
let P be RedSequence of ==>.-relation(TS), k, l such that
A34: k in dom P & l in dom P & k < l;
len P = len P;
hence thesis by A33,A34;
end;
theorem Th67:
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
proof
assume
A1: TS is deterministic;
let P, Q be RedSequence of ==>.-relation(TS) such that
A2: P.1 = Q.1;
defpred P[Nat] means $1 in dom P & $1 in dom Q implies P.$1 = Q.$1;
A3: now
let k;
assume
A4: P[k];
now
assume
A5: k + 1 in dom P & k + 1 in dom Q;
per cases;
suppose
A6: k in dom P & k in dom Q;
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;
end;
suppose
not k in dom P or not k in dom Q;
then k = 0 by A5,REWRITE2:1;
hence P.(k + 1) = Q.(k + 1) by A2;
end;
end;
hence P[k + 1];
end;
A7: P[0] by FINSEQ_3:25;
for k holds P[k] from NAT_1:sch 2(A7, A3);
hence thesis;
end;
theorem Th68:
TS is deterministic implies for P, Q being RedSequence of
==>.-relation(TS) st P.1 = Q.1 & len P = len Q holds P = Q
proof
assume
A1: TS is deterministic;
let P, Q be RedSequence of ==>.-relation(TS) such that
A2: P.1 = Q.1 and
A3: len P = len Q;
now
let k;
assume
A4: k in dom P;
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;
end;
hence thesis by A3,FINSEQ_2:9;
end;
theorem Th69:
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
proof
assume
A1: TS is deterministic;
then
A2: not <%>E in rng dom (the Tran of TS);
let P, Q be RedSequence of ==>.-relation(TS) such that
A3: P.1 = Q.1 and
A4: (P.len P)`2 = (Q.len Q)`2;
per cases by XXREAL_0:1;
suppose
len P = len Q;
hence thesis by A1,A3,Th68;
end;
suppose
A5: len P > len 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: k >= 0 + 1 by NAT_1:13;
then
A8: k in dom P by A5,FINSEQ_3:25;
k in dom Q by A7,FINSEQ_3:25;
then (P.len Q)`2 = (P.len P)`2 by A1,A3,A4,A8,Th67;
hence thesis by A2,A5,A8,A6,Th66;
end;
suppose
A9: len P < len 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: k >= 0 + 1 by NAT_1:13;
then
A12: k in dom Q by A9,FINSEQ_3:25;
k in dom P by A11,FINSEQ_3:25;
then (Q.len P)`2 = (Q.len Q)`2 by A1,A3,A4,A12,Th67;
hence thesis by A2,A9,A12,A10,Th66;
end;
end;
begin :: Reductions
theorem Th70:
==>.-relation(TS) reduces [x, v], [y, w] implies ex u st v = u^w
proof
assume ==>.-relation(TS) reduces [x, v], [y, w];
then
ex P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P.len P = [
y, w] by REWRITE1:def 3;
hence thesis by Th53;
end;
theorem Th71:
==>.-relation(TS) reduces [x, u], [y, v] implies ==>.-relation(
TS) reduces [x, u^w], [y, v^w]
proof
assume ==>.-relation(TS) reduces [x, u], [y, v];
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;
deffunc F(set) = [(P.$1)`1, dim2(P.$1, E)^w];
consider Q being FinSequence such that
A5: len Q = len P and
A6: for k st k in dom Q holds Q.k = F(k) from FINSEQ_1:sch 2;
for k being Nat st k in dom Q & k + 1 in dom Q holds [Q.k, Q.
(k + 1)] in ==>.-relation(TS)
proof
let k be Nat such that
A7: k in dom Q and
A8: k + 1 in dom Q;
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 thesis by A6,A7;
end;
then reconsider 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;
1 in dom P by A3,FINSEQ_3:25;
then
A13: dim2(P.1, E) = (P.1)`2 by A1,Th51
.= u by A1;
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;
hence thesis by A12,REWRITE1:def 3;
end;
theorem Th72:
x, y -->. z, TS implies ==>.-relation(TS) reduces [x, y], [z, <%>E]
proof
assume x, y -->. z, TS;
then <*[x, y], [z, <%>E]*> is RedSequence of ==>.-relation(TS) by Th57;
then [[x, y], [z, <%>E]] in ==>.-relation(TS) by Th8;
hence thesis by REWRITE1:15;
end;
theorem Th73:
x, v -->. y, TS implies ==>.-relation(TS) reduces [x, v^w], [y, w]
proof
assume x, v -->. y, TS;
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 thesis by REWRITE1:15;
end;
theorem Th74:
x1, x2 ==>. y1, y2, TS implies ==>.-relation(TS) reduces [x1, x2 ], [y1, y2]
proof
assume x1, x2 ==>. y1, y2, TS;
then [[x1, x2], [y1, y2]] in ==>.-relation(TS) by Def4;
hence thesis by REWRITE1:15;
end;
theorem Th75:
==>.-relation(TS) reduces [x, v], [y, w] implies len v >= len w
proof
assume ==>.-relation(TS) reduces [x, v], [y, w];
then
ex P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P.len P = [
y, w] by REWRITE1:def 3;
hence thesis by Th59;
end;
theorem
==>.-relation(TS) reduces [x, w], [y, v^w] implies v = <%>E
proof
assume ==>.-relation(TS) reduces [x, w], [y, v^w];
then len w >= len(v^w) by Th75;
then len v + len w <= 0 + len w by AFINSQ_1:17;
hence thesis by XREAL_1:6;
end;
theorem Th77:
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 )
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
assume ==>.-relation(TS) reduces [x, v], [y, w];
then
ex P being RedSequence of ==>.-relation(TS) st P.1 = [x, v] & P.len P = [
y, w] by REWRITE1:def 3;
hence thesis by A1,Th64;
end;
theorem
not <%>E in rng dom (the Tran of TS) implies (==>.-relation(TS)
reduces [x, u], [y, u] implies x = y)
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
assume ==>.-relation(TS) reduces [x, u], [y, u];
then len u > len u or x = y by A1,Th77;
hence thesis;
end;
theorem Th79:
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))
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
assume ==>.-relation(TS) reduces [x, <%e%>], [y, <%>E];
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 thesis by A2,A3,REWRITE1:def 2;
end;
theorem Th80:
TS is deterministic implies (==>.-relation(TS) reduces x, [y1, z
] & ==>.-relation(TS) reduces x, [y2, z] implies y1 = y2)
proof
assume
A1: TS is deterministic;
assume that
A2: ==>.-relation(TS) reduces x, [y1, z] and
A3: ==>.-relation(TS) reduces x, [y2, z];
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;
(P.len P)`2 = z by A5;
then P = Q by A1,A4,A6,A8,Th69;
hence thesis by A5,A7,XTUPLE_0:1;
end;
begin :: Transitions
definition
let E, F, TS; let x1, x2, y1, y2 be object;
pred x1, x2 ==>* y1, y2, TS means
==>.-relation(TS) reduces [x1, x2], [y1, y2];
end;
theorem Th81:
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
by Th34;
theorem Th82:
x, y ==>* x, y, TS
by REWRITE1:12;
theorem Th83:
x1, x2 ==>* y1, y2, TS & y1, y2 ==>* z1, z2, TS implies x1, x2
==>* z1, z2, TS
by REWRITE1:16;
theorem Th84:
x, y -->. z, TS implies x, y ==>* z, <%>E, TS
by Th72;
theorem
x, v -->. y, TS implies x, v^w ==>* y, w, TS
by Th73;
theorem Th86:
x, u ==>* y, v, TS implies x, u^w ==>* y, v^w, TS
by Th71;
theorem Th87:
x1, x2 ==>. y1, y2, TS implies x1, x2 ==>* y1, y2, TS
by Th74;
theorem Th88:
x, v ==>* y, w, TS implies ex u st v = u^w
by Th70;
theorem Th89:
x, v ==>* y, w, TS implies len w <= len v
proof
assume x, v ==>* y, w, TS;
then ex u st v = u^w by Th88;
hence thesis by Th9;
end;
theorem
x, w ==>* y, v^w, TS implies v = <%>E
proof
assume x, w ==>* y, v^w, TS;
then len(v^w) <= len w by Th89;
then len v + len w <= 0 + len w by AFINSQ_1:17;
hence thesis by XREAL_1:6;
end;
theorem Th91:
not <%>E in rng dom (the Tran of TS) implies (x, u ==>* y, u, TS iff x = y)
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
thus x, u ==>* y, u, TS implies x = y
proof
assume x, u ==>* y, u, TS;
then ==>.-relation(TS) reduces [x, u], [y, u];
then
ex p being RedSequence of ==>.-relation(TS) st p.1 = [x, u] & p.len p =
[y, u] by REWRITE1:def 3;
hence thesis by A1,Th60;
end;
assume x = y;
hence thesis by Th82;
end;
theorem Th92:
not <%>E in rng dom (the Tran of TS) implies (x, <%e%> ==>* y,
<%>E, TS implies x, <%e%> ==>. y, <%>E, TS)
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
assume x, <%e%> ==>* y, <%>E, TS;
then ==>.-relation(TS) reduces [x, <%e%>], [y, <%>E];
then [[x, <%e%>], [y, <%>E]] in ==>.-relation(TS) by A1,Th79;
hence thesis by Def4;
end;
theorem Th93:
TS is deterministic implies ( x1, x2 ==>* y1, z, TS & x1, x2
==>* y2, z, TS implies y1 = y2)
by Th80;
begin :: Acceptance of Words
definition
let E, F, TS; let x1, x2, y be object;
pred x1, x2 ==>* y, TS means
x1, x2 ==>* y, <%>E, TS;
end;
theorem Th94:
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
by Th81;
theorem Th95:
x, <%>E ==>* x, TS
by Th82;
theorem Th96:
x, u ==>* y, TS implies x, u^v ==>* y, v, TS
proof
assume x, u ==>* y, TS;
then x, u ==>* y, <%>E, TS;
then x, u^v ==>* y, {}^v, TS by Th86;
hence thesis;
end;
theorem
x, y -->. z, TS implies x, y ==>* z, TS
by Th84;
theorem
x1, x2 ==>. y, <%>E, TS implies x1, x2 ==>* y, TS
by Th87;
theorem
x, u ==>* y, TS & y, v ==>* z, TS implies x, u^v ==>* z, TS
proof
assume that
A1: x, u ==>* y, TS and
A2: y, 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;
then x, u^v^{} ==>* z, <%>E, TS by A3,Th83;
hence thesis;
end;
theorem Th100:
not <%>E in rng dom (the Tran of TS) implies (x, <%>E ==>* y, TS iff x = y)
by Th91;
theorem
not <%>E in rng dom (the Tran of TS) implies (x, <%e%> ==>* y, TS
implies x, <%e%> ==>. y, <%>E, TS)
by Th92;
theorem
TS is deterministic implies ( x1, x2 ==>* y1, TS & x1, x2 ==>* y2, TS
implies y1 = y2)
by Th93;
begin :: Reachable States
definition
let E, F, TS, x, X;
func x-succ_of (X, TS) -> Subset of TS equals
{ s : ex t st t in X & t, x
==>* s, TS };
coherence
proof
set Y = { s : ex t st t in X & t, x ==>* s, TS };
Y c= the carrier of TS
proof
let y be object;
assume y in Y;
then ex s st s = y & ex t st t in X & t, x ==>* s, TS;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th103:
s in x-succ_of (X, TS) iff ex t st t in X & t, x ==>* s, TS
proof
thus s in x-succ_of (X, TS) implies ex t st t in X & t, x ==>* s, TS
proof
assume s in x-succ_of (X, TS);
then ex s9 st s9 = s & ex t st t in X & t, x ==>* s9, TS;
hence thesis;
end;
thus thesis;
end;
theorem
not <%>E in rng dom (the Tran of TS) implies <%>E-succ_of (S, TS) = S
proof
assume
A1: not <%>E in rng dom (the Tran of TS);
A2: now
let x be object;
assume x in <%>E-succ_of (S, TS);
then ex s st s in S & s, <%>E ==>* x, TS by Th103;
hence x in S by A1,Th100;
end;
now
let x be object;
assume
A3: x in S;
x, <%>E ==>* x, TS by Th95;
hence x in <%>E-succ_of (S, TS) by A3;
end;
hence thesis by A2,TARSKI:2;
end;
theorem
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)
proof
let TS1 be non empty transition-system over F1, TS2 be non empty
transition-system over F2 such that
A1: the carrier of TS1 = the carrier of TS2 and
A2: the Tran of TS1 = the Tran of TS2;
A3: now
let y be object;
assume
A4: y in x-succ_of (X, TS2);
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 as Element of TS1 by A1;
reconsider 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;
end;
now
let y be object;
assume
A7: y in x-succ_of (X, TS1);
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 as Element of TS2 by A1;
reconsider 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;
end;
hence thesis by A3,TARSKI:2;
end;