:: Labelled State Transition Systems
::  by Micha{\l} Trybulec
::
:: Received May 5, 2009
:: Copyright (c) 2009-2012 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, MEMBERED, XXREAL_0,
      STRUCT_0, SUBSET_1, REWRITE1, AFINSQ_1, RELAT_1, FUNCT_1, FINSEQ_1,
      XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, STRUCT_0, XTUPLE_0;
 theorems AFINSQ_1, CALCUL_1, FLANG_1, FLANG_2, FUNCT_1, NAT_1, RELAT_1,
      RELSET_1, REWRITE1, STRUCT_0, TARSKI, XREAL_1, XXREAL_0, ZFMISC_1,
      FINSEQ_1, FINSEQ_2, FINSEQ_3, MCART_1, REWRITE2, XTUPLE_0;
 schemes FINSEQ_1, NAT_1, RELSET_1;

begin :: Preliminaries - FinSequences

reserve x, x1, x2, y, y1, y2, z, z1, z2, 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 Th1:
  for p being FinSequence st k in dom p holds (<*x*>^p).(k + 1) = p.k
proof
  let p be FinSequence such that
A1: k in dom p;
  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 thesis;
end;

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 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 Element of 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 Element of 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 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 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,Th1;
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 by FINSEQ_1:44;
  len P = 2 by FINSEQ_1:44;
  then
A2: 1 in dom P & 1 + 1 in dom P by FINSEQ_3:25;
  assume <*x, y*> is RedSequence of R;
  hence thesis by A1,A2,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 Th14:
  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 by Def1,RELAT_1:38;
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 by Th14,RELAT_1:38;
  end;
end;

begin :: Productions

definition
  let X;
  let TS be transition-system over X;
  let x, y, z;
  pred x, y -->. z, TS means
  :Def2:
  [[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 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;
  [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 Th16:
  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
proof
  let TS1 be transition-system over X1, TS2 be transition-system over X2 such
  that
A1: the Tran of TS1 = the Tran of TS2;
  assume x, y -->. z, TS1;
  then [[x, y], z] in the Tran of TS1 by Def2;
  hence thesis by A1,Def2;
end;

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
proof
  let TS be transition-system over F such that
A1: the Tran of TS is Function;
  assume x, y -->. z1, TS & x, y -->. z2, TS;
  then [[x, y], z1] in the Tran of TS & [[x, y], z2] in the Tran of TS by Def2;
  hence thesis by A1,FUNCT_1:def 1;
end;

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 by Def2;
  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 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 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;
  pred x1, x2 ==>. y1, y2, TS means
  :Def3:
  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)
proof
  let TS be transition-system over F;
  assume x1, x2 ==>. y1, y2, TS;
  then ex v, w st v = y2 & x1, w -->. y1, TS & x2 = w^v by Def3;
  hence thesis by Th15;
end;

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,Def3;
  take v, w;
  thus thesis by A1,A3,Th16;
end;

theorem Th22:
  for TS being transition-system over F holds x, u ==>. y, v, TS
  implies ex w st x, w -->. y, TS & u = w^v
proof
  let TS be transition-system over F;
  assume x, u ==>. y, v, TS;
  then consider v1, w such that
A1: v1 = v & x, w -->. y, TS & u = w^v1 by Def3;
  take w;
  thus thesis by A1;
end;

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,Def3;
  end;
B: w^{} = w;
  assume x, y ==>. z, <%>E, TS;
  then ex v, w st v = <%>E & x, w -->. z, TS & y = w^v by Def3;
  hence thesis by B;
end;

theorem Th24:
  for TS being transition-system over F holds x, v -->. y, TS iff
  x, v^w ==>. y, w, TS
proof
  let TS be transition-system over F;
  thus x, v -->. y, TS implies x, v^w ==>. y, w, TS by Def3;
  assume x, v^w ==>. y, w, TS;
  then ex u st x, u -->. y, TS & v^w = u^w by Th22;
  hence thesis by AFINSQ_1:28;
end;

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 by Th22;
  u^w = u1^(v^w) by A2,AFINSQ_1:27;
  hence thesis by A1,Def3;
end;

theorem Th26:
  for TS being transition-system over F holds x, u ==>. y, v, TS
  implies len u >= len v
proof
  let TS be transition-system over F;
  assume x, u ==>. y, v, TS;
  then ex w st x, w -->. y, TS & u = w^v by Th22;
  hence thesis by Th9;
end;

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,Def3;
  consider v2, w2 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 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 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;
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 by Th22;
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,Def3;
  consider v1, w1 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 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 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:     t in [: the carrier of TS, E^omega :] by A4,ZFMISC_1:def 2;
        x2 in E^omega by A3,Th20;
        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 set 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 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 as Element of E^omega by A15;
      reconsider 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 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 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 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 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;
    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;
    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:1;
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 by Def3;
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 by Th22;
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 by Th23;
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 by Th24;
    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 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 by MCART_1:7
;
    {} = <%>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 by MCART_1:8;
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;
A4: v in E^omega & w in E^omega;
  s in TS & t in TS by A1,A2,Th32;
  hence thesis by A2,A4,A3,MCART_1:7;
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 Element of 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 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 by MCART_1:7 .= <%>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 by Th22;
          take u2^u1;
          (P.len1)`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 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,MCART_1:7;
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,MCART_1:7;
        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;
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
          let l;
          assume
A20:      l in dom P;
          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;
          per cases by A23;
          suppose
            l = 1;
            hence (P.l)`2 = u by A3,MCART_1:7;
          end;
          suppose
A24:        (l - 1) in dom Q;
            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;
          end;
        end;
      end;
    end;
    hence P[k + 1];
  end;
A27: P[0];
  for k holds P[k] from NAT_1:sch 2(A27, 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,MCART_1:7;
  (P.k)`1, w1 -->. t, TS by A2,A5,MCART_1:7;
  hence thesis by A2,A3,A6,MCART_1:7;
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,MCART_1:7;
    then v1 = w2 by A2,A10,MCART_1:7;
    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 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;
      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
A3: len P <= 1 + 1 by AFINSQ_1:34;
  len P <> 1 by A2,XTUPLE_0:1;
  hence thesis by A3,NAT_1:26;
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;
B:  {}^w = w;
    len v = len w by A4,A5,XXREAL_0:1;
    then u = <%>E by A6;
    hence thesis by A1,A2,Th60,A3,B;
  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,MCART_1:7;
  hence thesis by A4,MCART_1:7;
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) by Def1;
  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,MCART_1:7;
  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 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 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,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 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,MCART_1:7;
  (P.len P)`2 = z by A5,MCART_1:7;
  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, x1, x2, y1, y2;
  pred x1, x2 ==>* y1, y2, TS means
  :Def6:
  ==>.-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
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;
  assume x1, x2 ==>* y1, y2, TS1;
  then ==>.-relation(TS1) reduces [x1, x2], [y1, y2] by Def6;
  then ==>.-relation(TS2) reduces [x1, x2], [y1, y2] by A1,Th34;
  hence thesis by Def6;
end;

theorem Th82:
  x, y ==>* x, y, TS
proof
  ==>.-relation(TS) reduces [x, y], [x, y] by REWRITE1:12;
  hence thesis by Def6;
end;

theorem Th83:
  x1, x2 ==>* y1, y2, TS & y1, y2 ==>* z1, z2, TS implies x1, x2
  ==>* z1, z2, TS
proof
  assume x1, x2 ==>* y1, y2, TS & y1, y2 ==>* 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 thesis by Def6;
end;

theorem Th84:
  x, y -->. z, TS implies x, y ==>* z, <%>E, TS
proof
  assume x, y -->. z, TS;
  then ==>.-relation(TS) reduces [x, y], [z, <%>E] by Th72;
  hence thesis by Def6;
end;

theorem
  x, v -->. y, TS implies x, v^w ==>* y, w, TS
proof
  assume x, v -->. y, TS;
  then ==>.-relation(TS) reduces [x, v^w], [y, w] by Th73;
  hence thesis by Def6;
end;

theorem Th86:
  x, u ==>* y, v, TS implies x, u^w ==>* y, v^w, TS
proof
  assume x, u ==>* y, v, TS;
  then ==>.-relation(TS) reduces [x, u], [y, v] by Def6;
  then ==>.-relation(TS) reduces [x, u^w], [y, v^w] by Th71;
  hence thesis by Def6;
end;

theorem Th87:
  x1, x2 ==>. y1, y2, TS implies x1, x2 ==>* y1, y2, TS
proof
  assume x1, x2 ==>. y1, y2, TS;
  then ==>.-relation(TS) reduces [x1, x2], [y1, y2] by Th74;
  hence thesis by Def6;
end;

theorem Th88:
  x, v ==>* y, w, TS implies ex u st v = u^w
proof
  assume x, v ==>* y, w, TS;
  then ==>.-relation(TS) reduces [x, v], [y, w] by Def6;
  hence thesis by Th70;
end;

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] 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 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] by Def6;
  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)
proof
  assume
A1: TS is deterministic;
  assume x1, x2 ==>* y1, z, TS & x1, x2 ==>* y2, z, TS;
  then
  ==>.-relation(TS) reduces [x1, x2], [y1, z] & ==>.-relation(TS) reduces
  [x1, x2], [y2, z] by Def6;
  hence thesis by A1,Th80;
end;

begin :: Acceptance of Words

definition
  let E, F, TS, x1, x2, y;
  pred x1, x2 ==>* y, TS means
  :Def7:
  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
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;
  assume x, y ==>* z, TS1;
  then x, y ==>* z, <%>E, TS1 by Def7;
  then x, y ==>* z, <%>E, TS2 by A1,Th81;
  hence thesis by Def7;
end;

theorem Th95:
  x, <%>E ==>* x, TS
proof
  x, <%>E ==>* x, <%>E, TS by Th82;
  hence thesis by Def7;
end;

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 by Def7;
  then x, u^v ==>* y, {}^v, TS by Th86;
  hence thesis;
end;

theorem
  x, y -->. z, TS implies x, y ==>* z, TS
proof
  assume x, y -->. z, TS;
  then x, y ==>* z, <%>E, TS by Th84;
  hence thesis by Def7;
end;

theorem
  x1, x2 ==>. y, <%>E, TS implies x1, x2 ==>* y, TS
proof
  assume x1, x2 ==>. y, <%>E, TS;
  then x1, x2 ==>* y, <%>E, TS by Th87;
  hence thesis by Def7;
end;

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,Def7;
  then x, u^v^{} ==>* z, <%>E, TS by A3,Th83;
  hence thesis by Def7;
end;

theorem Th100:
  not <%>E in rng dom (the Tran of TS) implies (x, <%>E ==>* y, TS iff x = y)
proof
  assume
A1: not <%>E in rng dom (the Tran of TS);
  thus x, <%>E ==>* y, TS implies x = y
  proof
    assume x, <%>E ==>* y, TS;
    then x, <%>E ==>* y, <%>E, TS by Def7;
    hence thesis by A1,Th91;
  end;
  assume x = y;
  hence thesis by Th95;
end;

theorem
  not <%>E in rng dom (the Tran of TS) implies (x, <%e%> ==>* y, TS
  implies x, <%e%> ==>. y, <%>E, TS)
proof
  assume
A1: not <%>E in rng dom (the Tran of TS);
  assume x, <%e%> ==>* y, TS;
  then x, <%e%> ==>* y, <%>E, TS by Def7;
  hence thesis by A1,Th92;
end;

theorem
  TS is deterministic implies ( x1, x2 ==>* y1, TS & x1, x2 ==>* y2, TS
  implies y1 = y2)
proof
  assume
A1: TS is deterministic;
  assume x1, x2 ==>* y1, TS & x1, x2 ==>* y2, TS;
  then x1, x2 ==>* y1, <%>E, TS & x1, x2 ==>* y2, <%>E, TS by Def7;
  hence thesis by A1,Th93;
end;

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