The Mizar article:

Processes in Petri nets

by
Grzegorz Bancerek,
Mitsuru Aoki,
Akio Matsumoto, and
Yasunari Shidama

Received December 20, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: PNPROC_1
[ MML identifier index ]


environ

 vocabulary PNPROC_1, TARSKI, RELAT_1, FUNCT_1, BOOLE, MCART_1, ARYTM_1, NET_1,
      FINSEQ_1, FUNCT_2, FUNCT_7, FUNCOP_1, PRALG_1, FINSEQ_4, CARD_1,
      FINSET_1, PETRI, RELOC, INT_1;
 notation TARSKI, XBOOLE_0, DOMAIN_1, RELAT_1, FUNCT_1, SUBSET_1, FINSET_1,
      CARD_1, FINSEQ_1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
      BINARITH, MCART_1, FINSEQ_2, FINSEQ_4, LANG1, PRALG_1, FUNCT_7, INT_1,
      GRAPH_2;
 constructors WELLORD2, DOMAIN_1, INT_1, FINSEQ_4, FUNCT_7, BINARITH, GRAPH_2,
      MEMBERED;
 clusters RELAT_1, RELSET_1, FUNCT_1, FUNCT_7, FUNCOP_1, SUBSET_1, FINSEQ_1,
      HEYTING2, PRELAMB, INT_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0, PRALG_1, RELAT_1;
 theorems TARSKI, AXIOMS, NAT_1, FUNCT_1, FUNCT_2, REAL_1, REAL_2, RELSET_1,
      FUNCOP_1, XBOOLE_1, CARD_1, RELAT_1, SCMFSA_7, MCART_1, INT_1, FINSEQ_1,
      FUNCT_7, XBOOLE_0, FINSEQ_4, TREES_2, FINSEQ_3, ENUMSET1, ZFMISC_1,
      GRFUNC_1, PRE_CIRC, CARD_2, BAGORDER, FINSET_1, AMI_1, GRAPH_2, WELLORD2,
      FINSEQ_6, XCMPLX_1;
 schemes NAT_1, FUNCT_1, FINSEQ_1;

begin :: Preliminaries

reserve i,j,k,l for Nat,
        x,x1,x2,y1,y2 for set;

theorem Th1:
  i > 0 implies {[i,x]} is FinSubsequence
    proof
      assume A1: i > 0;
        {[i,x]} is FinSubsequence-like
        proof
A2:       dom {[i,x]} = {i} by RELAT_1:23;
            {i} c= Seg i
           proof
             let x;
             assume x in {i};
then x = i by TARSKI:def 1;
             hence x in Seg i by A1,FINSEQ_1:5;
           end;
          hence thesis by A2,FINSEQ_1:def 12;
        end;
      hence {[i,x]} is FinSubsequence-like Function;
    end;

Lm1:
  for p being FinSubsequence st Seq p = {} holds p = {}
   proof
     let p be FinSubsequence such that
A1:  Seq p = {};
       Seq p = p * Sgm(dom p) & rng Sgm dom p = dom p
       by FINSEQ_1:71,def 14;
     then dom {} = dom Sgm dom p by A1,RELAT_1:46;
     then Sgm dom p = {} by RELAT_1:64;
     then dom p = rng {} by FINSEQ_1:71;
    hence thesis by RELAT_1:64;
   end;

theorem Th2:
  for q being FinSubsequence holds q = {} iff Seq q = {}
   proof let q be FinSubsequence;
     consider k be Nat such that
A1:  dom q c= Seg k by FINSEQ_1:def 12;
     thus q = {} implies Seq q = {}
      proof assume
A2:     q = {};
A3:     Seq q = q*Sgm dom q by FINSEQ_1:def 14;
          dom q = {} by A2,FINSEQ_1:26;
        hence Seq q = q*{} by A1,A3,FINSEQ_1:72
                   .= {};
      end;
     thus thesis by Lm1;
   end;

theorem Th3:
  for q being FinSubsequence st q = {[i,x]} holds Seq q = <*x*>
    proof
      let q be FinSubsequence; assume
A1:   q = {[i,x]};
      then [i,x] in q by TARSKI:def 1;
then A2:   i in dom q by RELAT_1:20;
      consider k be Nat such that
A3:    dom q c= Seg k by FINSEQ_1:def 12;
        i >= 0+1 by A2,A3,FINSEQ_1:3;
then A4:   i > 0 by NAT_1:38;
      then reconsider p = {[i,x]} as FinSubsequence by Th1;
      A5: Seq q = q* Sgm(dom q) by FINSEQ_1:def 14;
        dom p = {i} by RELAT_1:23;
      then Seq p = {[i,x]}*<*i*> by A1,A4,A5,FINSEQ_3:50
           .= <*{[i,x]}.i*> by A1,A2,BAGORDER:3
           .= <*x*> by GRFUNC_1:16;
           hence thesis by A1;
    end;

definition
  cluster -> finite FinSubsequence;
  coherence
   proof let q be FinSubsequence;
     consider n being Nat such that
A1:  dom q c= Seg n by FINSEQ_1:def 12;
       dom q is finite by A1,FINSET_1:13;
     hence thesis by AMI_1:21;
   end;
end;

theorem Th4:
  for q being FinSubsequence st Seq q = <*x*>
   ex i st q = {[i,x]}
    proof
      let q be FinSubsequence; assume
        Seq q = <*x*>;
then A1:   Seq q = {[1,x]} by FINSEQ_1:def 5;
then A2:   dom Seq q = {1} by RELAT_1:23;
A3:   rng Seq q = {x} by A1,RELAT_1:23;
A4:   Seq q = q* Sgm(dom q) by FINSEQ_1:def 14;
        rng Sgm(dom q) = dom q by FINSEQ_1:71;
then A5:   {1} = dom Sgm(dom q) &
      rng Seq q = rng q by A2,A4,RELAT_1:46,47;
      consider n being Nat such that
A6:   dom q c= Seg n by FINSEQ_1:def 12;
        Seg Card dom q = {1} by A5,A6,FINSEQ_3:45;
      then Card dom q = Card {1} by FINSEQ_1:78;
      then consider y be set such that
A7:   dom q = {y} by CARD_1:49;
        y in dom q by A7,TARSKI:def 1;
      then y in Seg n by A6;
      then reconsider y as Nat;
        q = {[y,x]} by A3,A5,A7,PRE_CIRC:2;
      hence thesis;
    end;

theorem Th5:
  {[x1,y1], [x2,y2]} is FinSequence implies
    x1 = 1 & x2 = 1 & y1 = y2 or
    x1 = 1 & x2 = 2 or
    x1 = 2 & x2 = 1
     proof
          assume
            {[x1,y1], [x2,y2]} is FinSequence;
          then reconsider p = {[x1,y1], [x2,y2]} as FinSequence;
            dom p = {x1,x2} by RELAT_1:24;
then A1:       x1 in dom p & x2 in dom p by TARSKI:def 2;
            [x1,y1] in p & [x2,y2] in p by TARSKI:def 2;
then A2:       p.x1 = y1 & p.x2 = y2 by FUNCT_1:8;
A3:       dom p = Seg len p by FINSEQ_1:def 3;
A4:       len p <= 1+1 by CARD_2:69;
            len p <> 0 by CARD_2:59;
          then len p > 0 by NAT_1:19;
          then A5: len p >= 0+1 by NAT_1:38;
A6:    now assume len p = 1;
         hence x1 = 1 & x2 = 1 by A1,A3,FINSEQ_1:4,TARSKI:def 1;
         hence y1 = y2 by A2;
       end;
         now assume
A7:         len p = 2;
       A8: x1 = x2 implies p = {[x1,y1]} by A2,ENUMSET1:69;
            x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1 or
          x1 = 1 & x2 = 1 or x1 = 2 & x2 = 2
            by A1,A3,A7,FINSEQ_1:4,TARSKI:def 2;
         hence x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1 by A7,A8,CARD_1:79;
       end;
       hence thesis by A4,A5,A6,NAT_1:27;
     end;

theorem Th6:
  <*x1,x2*> = {[1,x1], [2,x2]}
   proof
     reconsider f={[1,x1], [2,x2]} as Function by GRFUNC_1:19;
A1:  dom f = {1,2} by RELAT_1:24;
then A2:  dom <*x1,x2*> = dom f by FINSEQ_1:4,FINSEQ_3:29;
       now let x; assume
A3:    x in {1,2};
       per cases by A3,TARSKI:def 2;
         suppose A4: x = 1;
then A5:      <*x1,x2*>.x = x1 by FINSEQ_1:61;
           [x,x1] in f by A4,TARSKI:def 2;
         hence f.x = <*x1,x2*>.x by A5,FUNCT_1:8;
         suppose A6: x = 2;
then A7:      <*x1,x2*>.x = x2 by FINSEQ_1:61;
           [x,x2] in f by A6,TARSKI:def 2;
         hence f.x = <*x1,x2*>.x by A7,FUNCT_1:8;
     end;
     hence <*x1,x2*> = {[1,x1], [2,x2]} by A1,A2,FUNCT_1:9;
   end;

Lm2: for j,k,l st
    1 <= j & j <= l or l+1 <= j & j <= l+k holds 1 <= j & j <= l+k
  proof
    let j,k,l; assume
A1: 1 <= j & j <= l or l+1 <= j & j <= l+k;
    per cases by A1;
    suppose A2: 1 <= j & j <= l;
       0 <= k by NAT_1:18;
     then l+0 <= l+k by REAL_1:55;
     hence thesis by A2,AXIOMS:22;
    suppose A3: l+1 <= j & j <= l+k;
       0 <= l by NAT_1:18;
     then 0+1 <= l+1 by REAL_1:55;
     hence thesis by A3,AXIOMS:22;
  end;

theorem Th7:
 for p being FinSubsequence holds Card p = len Seq p
  proof let p be FinSubsequence;
    consider k being Nat such that
A1: dom p c= Seg k by FINSEQ_1:def 12;
A2: Seq p = p*(Sgm dom p) by FINSEQ_1:def 14;
A3: rng Sgm dom p = dom p by FINSEQ_1:71;
    then A4: dom Seq p = dom Sgm dom p by A2,RELAT_1:46;
      Sgm dom p is one-to-one by A1,FINSEQ_3:99;
    then rng Sgm dom p, dom Sgm dom p are_equipotent by WELLORD2:def 4;
    then Card dom p = Card dom Sgm dom p & Card dom p = Card p
     by A3,CARD_1:21,PRE_CIRC:21;
   hence thesis by A4,PRE_CIRC:21;
  end;

Lm3:
  for X, Y being set holds
  (for x st x in X holds not x in Y) iff X misses Y
   proof
     let X, Y be set;
     thus (for x st x in X holds not x in Y) implies X misses Y
      proof assume
A1:     for x st x in X holds not x in Y;
          now given x1 such that
A2:       x1 in X /\ Y;
            x1 in X & x1 in Y by A2,XBOOLE_0:def 3;
          hence contradiction by A1;
        end;
        then X /\ Y = {} by XBOOLE_0:def 1;
        hence X misses Y by XBOOLE_0:def 7;
      end; assume A3: X misses Y;
       now let x; assume
A4:    x in X;
         now assume x in Y;
         then x in X /\ Y by A4,XBOOLE_0:def 3;
         hence contradiction by A3,XBOOLE_0:def 7;
       end;
       hence not x in Y;
     end;
     hence for x st x in X holds not x in Y;
   end;

theorem Th8:
  for P,R being Relation st dom P misses dom R holds P misses R
   proof let P,R be Relation; assume A1: dom P misses dom R;
       now given x such that
A2:    x in dom (P /\ R);
         dom (P /\ R) c= dom P /\ dom R by RELAT_1:14;
       hence contradiction by A1,A2,XBOOLE_0:def 7;
     end;
     then dom (P /\ R) = {} by XBOOLE_0:def 1;
     hence P /\ R = {} by RELAT_1:64;
   end;

theorem Th9:
  for X,Y being set, P,R being Relation st X misses Y holds P|X misses R|Y
   proof let X,Y be set, P,R be Relation; assume X misses Y;
then A1:  X /\ Y = {} by XBOOLE_0:def 7;
       dom (P|X) = dom P /\ X & dom (R|Y) = dom R /\ Y by RELAT_1:90;
     then dom (P|X) /\ dom (R|Y) = dom P /\ (X /\ (dom R /\ Y)) by XBOOLE_1:16
                           .= dom P /\ (X /\ Y /\ dom R) by XBOOLE_1:16
                           .= {} by A1;
     then dom (P|X) misses dom (R|Y) by XBOOLE_0:def 7;
     hence thesis by Th8;
   end;

Lm4:
 for q being FinSubsequence holds dom Seq q = dom Sgm dom q
  proof let q be FinSubsequence;
A1: Seq q = q* Sgm dom q by FINSEQ_1:def 14;
      rng Sgm dom q = dom q by FINSEQ_1:71;
    hence thesis by A1,RELAT_1:46;
  end;

Lm5:
  for q being FinSubsequence holds rng q = rng Seq q
   proof let q be FinSubsequence;
A1:  rng Seq q = rng (q*Sgm dom q) by FINSEQ_1:def 14;
       dom q = rng Sgm dom q by FINSEQ_1:71;
     hence thesis by A1,RELAT_1:47;
   end;

theorem Th10:
 for f,g,h being Function st
    f c= h & g c= h & f misses g holds dom f misses dom g
  proof let f,g,h be Function such that
A1: f c= h and
A2: g c= h and
A3: f misses g;
      for x st x in dom f holds not x in dom g
     proof let x; assume x in dom f;
then A4:    [x,f.x] in f by FUNCT_1:def 4;
         now assume x in dom g;
then A5:      [x,g.x] in g by FUNCT_1:def 4;
         then f.x = g.x by A1,A2,A4,FUNCT_1:def 1;
         hence contradiction by A3,A4,A5,Lm3;
       end;
       hence thesis;
     end;
    hence thesis by Lm3;
  end;

theorem
    for Y being set, R being Relation holds Y|R c= R|(R"Y)
   proof let Y be set, R be Relation;
     let a,b be set; assume [a,b] in Y|R;
then A1:  b in Y & [a,b] in R by RELAT_1:def 12;
     then a in R"Y by RELAT_1:def 14;
     hence thesis by A1,RELAT_1:def 11;
   end;

theorem Th12:
  for Y being set, f being Function holds Y|f = f|(f"Y)
   proof let Y be set, f be Function;
     let x,y be set;
     thus [x,y] in Y|f implies [x,y] in f|(f"Y)
      proof assume [x,y] in Y|f;
then A1:     y in Y & [x,y] in f by RELAT_1:def 12;
        then x in dom f & f.x in Y by FUNCT_1:8;
        then x in f"Y by FUNCT_1:def 13;
        hence thesis by A1,RELAT_1:def 11;
      end; assume [x,y] in f|(f"Y);
then A2:  x in f"Y & [x,y] in f by RELAT_1:def 11;
     then f.x in Y by FUNCT_1:def 13;
     then y in Y by A2,FUNCT_1:8;
     hence thesis by A2,RELAT_1:def 12;
   end;

begin :: Markings on Petri nets

definition let P be set;
 mode marking of P -> Function means :Def1:
  dom it = P & rng it c= NAT;
 existence
  proof consider f being Function of P, NAT;
   take f;
   thus thesis by FUNCT_2:def 1,RELSET_1:12;
 end;
end;

reserve P,p,x,y,x1,x2,y1,y2 for set,
        m1,m2,m3,m4,m for marking of P,
        i,j,j1,j2,k,k1,k2,l,l1,l2 for Nat;

definition
 let P be set;
 let m be marking of P;
 let p be set;
 redefine func m.p -> Nat;
 coherence
  proof
A1:   rng m c= NAT by Def1;
       p in dom m or not p in dom m;
     then m.p in rng m or m.p = {} by FUNCT_1:12,def 4;
    hence m.p is Element of NAT by A1,CARD_1:51;
  end;
 synonym m multitude_of p;
end;

scheme MarkingLambda { P() -> set, F(set) -> Nat }:
 ex m being marking of P() st
  for p st p in P() holds m multitude_of p = F(p)
  proof
   deffunc F1(set) = F($1);
   consider m being Function such that
A1: dom m = P() and
A2: for p st p in P() holds m.p = F1(p) from Lambda;
      m is marking of P()
     proof
      thus dom m = P() by A1;
      thus rng m c= NAT
       proof
        let y; assume y in rng m;
        then consider x such that
A3:      x in dom m & y = m.x by FUNCT_1:def 5;
           y = F(x) by A1,A2,A3;
        hence y in NAT;
       end;
     end;
   hence thesis by A2;
  end;

definition let P,m1,m2;
  redefine pred m1 = m2 means
   for p st p in P holds m1 multitude_of p = m2 multitude_of p;
 compatibility
  proof
   thus m1 = m2 implies
     for p st p in P holds m1 multitude_of p = m2 multitude_of p;
    dom m1 = P & dom m2 = P by Def1;
   hence (for p st p in P holds m1 multitude_of p = m2 multitude_of p)
     implies m1 = m2 by FUNCT_1:9;
 end;
end;

definition let P;
 func {$} P -> marking of P equals :Def3:
   P --> 0;
 coherence
  proof
   thus dom (P --> 0) = P by FUNCOP_1:19;
  rng (P --> 0) c= {0} by FUNCOP_1:19;
   hence rng (P --> 0) c= NAT by XBOOLE_1:1;
  end;
end;

definition
 let P be set;
 let m1, m2 be marking of P;
 pred m1 c= m2 means :Def4:
  for p being set st p in P holds
    m1 multitude_of p <= m2 multitude_of p;
 reflexivity;
end;

Lm6:
  p in P implies {$}P multitude_of p = 0
   proof assume
A1:  p in P;
     then reconsider P as non empty set;
       p in dom {$}P by A1,Def1;
     then ({$}P).p in rng {$}P by FUNCT_1:def 5;
     then ({$}P).p in rng (P --> 0) by Def3;
     then ({$}P).p in {0} by FUNCOP_1:14;
     hence thesis by TARSKI:def 1;
   end;

theorem Th13:
  {$}P c= m
   proof let p; assume p in P;
     then ({$}P).p = 0 by Lm6;
     hence thesis by NAT_1:18;
   end;

theorem Th14:
  m1 c= m2 & m2 c= m3 implies m1 c= m3
proof
 assume A1: m1 c= m2 & m2 c= m3;
 let p;
 assume p in P;
 then m1.p <= m2.p & m2.p <= m3.p by A1,Def4;
 hence
   m1.p <= m3.p by AXIOMS:22;
end;

definition
 let P be set;
 let m1, m2 be marking of P;
 func m1 + m2 -> marking of P means :Def5:
  for p being set st p in P holds
    it multitude_of p = (m1 multitude_of p)+(m2 multitude_of p);
 existence
 proof
  deffunc F(set) = (m1 multitude_of $1)+(m2 multitude_of $1);
  thus ex m be marking of P st for p being set st p in P holds
   m multitude_of p = F(p) from MarkingLambda;
 end;
 uniqueness
  proof
   let M1, M2 being marking of P such that
A1: for p being set st p in P holds
     M1 multitude_of p = (m1 multitude_of p)+(m2 multitude_of p) and
A2: for p being set st p in P holds
     M2 multitude_of p = (m1 multitude_of p)+(m2 multitude_of p);
   let p; assume
A3: p in P;
   hence M1 multitude_of p = (m1 multitude_of p)+(m2 multitude_of p) by A1
     .= M2 multitude_of p by A2,A3;
  end;
 commutativity;
end;

theorem
    m + {$}P = m
   proof
       now let p; assume
         p in P;
       then ({$}P).p = 0 by Lm6;
       hence m.p = m.p + ({$}P).p;
     end;
     hence thesis by Def5;
   end;

definition
 let P be set;
 let m1, m2 be marking of P such that
A1:  m2 c= m1;
 func m1 - m2 -> marking of P means :Def6:
  for p being set st p in P holds
    it multitude_of p = (m1 multitude_of p)-(m2 multitude_of p);
 existence
  proof
   deffunc F(set) = (m1 multitude_of $1)-'(m2 multitude_of $1);
   consider m being marking of P such that
A2: for p st p in P holds m multitude_of p = F(p) from MarkingLambda;
   take m;
   let p;
   assume
A3: p in P;
then A4: (m1 multitude_of p) >= (m2 multitude_of p) by A1,Def4;
   thus m multitude_of p = (m1 multitude_of p)-'(m2 multitude_of p) by A2,A3
     .= (m1 multitude_of p)-(m2 multitude_of p) by A4,SCMFSA_7:3;
  end;
 uniqueness
  proof
   let M1, M2 be marking of P such that
A5: for p being set st p in P holds
     M1 multitude_of p = (m1 multitude_of p) - (m2 multitude_of p) and
A6: for p st p in P holds
     M2 multitude_of p = (m1 multitude_of p) - (m2 multitude_of p);
   let p; assume
A7: p in P;
   hence M1 multitude_of p
              = (m1 multitude_of p) - (m2 multitude_of p) by A5
             .= M2 multitude_of p by A6,A7;
    end;
end;

theorem Th16:
  m1 c= m1 + m2
proof
 let p;
 assume p in P;
then (m1 + m2) multitude_of p = (m1 multitude_of p)+(m2 multitude_of p)
 by Def5;
  hence thesis by NAT_1:29;
end;

theorem
    m - {$}P = m
   proof
A1:  now let p; assume p in P;
       then ({$}P).p = 0 by Lm6;
       hence m.p = m.p - ({$}P).p;
     end;
      {$}P c= m by Th13;
     hence thesis by A1,Def6;
   end;

theorem
    m1 c= m2 & m2 c= m3 implies m3 - m2 c= m3 - m1
proof
 assume A1: m1 c= m2 & m2 c= m3;
 then A2: m1 c= m3 by Th14;
 let p;
 assume A3: p in P;
 then A4: m1.p <= m2.p by A1,Def4;
 A5: (m3-m1).p = m3.p - m1.p by A2,A3,Def6;
        (m3-m2).p = m3.p - m2.p by A1,A3,Def6;
 hence
   (m3-m2).p <= (m3-m1).p by A4,A5,REAL_2:106;
end;

theorem Th19:
  (m1 + m2) - m2 = m1
proof
 let p;
 assume A1: p in P;
    m2 c= (m1 + m2) by Th16;
 hence
  ((m1 + m2) - m2).p = (m1 + m2) .p - m2.p by A1,Def6
                           .= m1.p + m2.p - m2.p by A1,Def5
                           .= m1.p by XCMPLX_1:26;
end;

theorem Th20:
  m c= m1 & m1 c= m2 implies m1 - m c= m2 - m
 proof
  assume A1: m c= m1;
  assume A2: m1 c= m2;
  let p;
  assume A3: p in P;
  A4: m c= m2 by A1,A2,Th14;
    m1.p <= m2.p by A2,A3,Def4;
  then (m1.p - m.p) <= (m2.p - m.p) by REAL_1:49;
  then (m1 - m).p <= m2.p - m.p by A1,A3,Def6;
  hence thesis by A3,A4,Def6;
 end;

theorem Th21:
m1 c= m2 implies m2 + m3 -m1 = m2 - m1 + m3
 proof
  assume A1: m1 c= m2;
  let p;
  assume A2: p in P;
    m2 c= m2 + m3 by Th16;
  then A3: m1 c= m2 + m3 by A1,Th14;
    (m2 - m1 + m3).p = (m2 - m1).p + m3.p by A2,Def5
                          .= m3.p + (m2.p - m1.p) by A1,A2,Def6
                          .= m3.p + m2.p - m1.p by XCMPLX_1:29
                          .= (m3 + m2).p - m1.p by A2,Def5
                          .= (m2 + m3 - m1).p by A2,A3,Def6;
  hence thesis;
 end;

theorem
  m1 c= m2 & m2 c= m1 implies m1 = m2
 proof assume
A1:  m1 c= m2; assume
A2:  m2 c= m1;
  let p; assume
A3:  p in P;
then A4:  m1.p <= m2.p by A1,Def4;
    m2.p <= m1.p by A2,A3,Def4;
  hence m1.p = m2.p by A4,AXIOMS:21;
 end;

theorem Th23:
(m1 + m2) + m3 = m1 + (m2 + m3)
 proof
  let p;
  assume
  A1: p in P;
  then A2: ((m1 + m2) + m3).p = (m1 + m2).p + m3.p by Def5
                        .= m1.p + m2.p + m3.p by A1,Def5;
    (m1 + (m2 + m3)).p = m1.p + (m2 + m3).p by A1,Def5
                        .= m1.p + (m2.p + m3.p) by A1,Def5
                        .= m1.p + m2.p + m3.p by XCMPLX_1:1;
  hence
    ((m1 + m2) + m3).p = (m1 + (m2 + m3)).p by A2;
 end;

theorem
  m1 c= m2 & m3 c= m4 implies m1 + m3 c= m2 + m4
 proof assume
A1:  m1 c= m2; assume
A2:  m3 c= m4;
  let p; assume
A3:  p in P;
then A4:  m1.p <= m2.p by A1,Def4;
       m3.p <= m4.p by A2,A3,Def4;
then A5:  m1.p + m3.p <= m2.p + m4.p by A4,REAL_1:55;
       (m1 + m3).p = m1.p + m3.p by A3,Def5;
  hence (m1 + m3).p <= (m2 + m4).p by A3,A5,Def5;
 end;

theorem
  m1 c= m2 implies m2 - m1 c= m2
 proof
  assume A1: m1 c= m2;
  let p;
  assume p in P;
  then A2: (m2 - m1).p = m2.p - m1.p by A1,Def6;
  A3: m1 multitude_of p >= 0 by NAT_1:18;
        m2.p - 0 = m2.p;
  hence thesis by A2,A3,REAL_1:92;
 end;

theorem Th26:
m1 c= m2 & m3 c= m4 & m4 c= m1 implies m1 - m4 c= m2 - m3
 proof assume
A1:  m1 c= m2; assume
A2:  m3 c= m4; assume
A3:  m4 c= m1;
    then m4 c= m2 by A1,Th14;
then A4:  m3 c= m2 by A2,Th14;
  let p; assume
A5:  p in P;
then A6:  m1.p <= m2.p by A1,Def4;
A7:  m3.p <= m4.p by A2,A5,Def4;
A8:  (m2 - m3).p = m2.p - m3.p by A4,A5,Def6;
       (m1 - m4).p = m1.p - m4.p by A3,A5,Def6;
  hence (m1 - m4).p <= (m2 - m3).p by A6,A7,A8,REAL_1:92;
 end;



::  a1 c= a2 & a2 c= a3 implies a3 - a2 c= a3 - a1 by T6';
::  a c= a1 & a1 c= a2 implies a1 - a c= a2 -a by T6';

theorem Th27:
m1 c= m2 implies m2 = (m2 - m1) + m1
 proof assume
A1:  m1 c= m2;
  let p; assume
A2:  p in P;
  then ((m2 - m1) + m1).p = (m2 - m1).p + m1.p by Def5
                                    .= m2.p - m1.p + m1.p by A1,A2,Def6
                                    .= m2.p + m1.p - m1.p by XCMPLX_1:29
                                    .= m2.p by XCMPLX_1:26;
  hence m2.p = ((m2 - m1) + m1).p;
 end;

theorem Th28:
  (m1 + m2) - m1 = m2
 proof
A1:  m1 c= m1 + m2 by Th16;
  let p; assume
A2:  p in P;
  then ((m1 + m2) - m1).p = (m1 + m2).p - m1.p by A1,Def6
                                    .= m1.p + m2.p - m1.p by A2,Def5
                                    .= m2.p by XCMPLX_1:26;
  hence ((m1 + m2) - m1).p = m2.p;
 end;

theorem Th29:
  m2 + m3 c= m1 implies (m1 - m2) - m3 = m1 - (m2 + m3)
 proof assume
       m2 + m3 c= m1;
  then (m1 - m2) - m3 = ((m1 - (m2 + m3)) + (m2 + m3)) - m2 - m3 by Th27
                        .= (((m1 - (m2 + m3) + m3) + m2) - m2) - m3 by Th23
                        .= ((m1 - (m2 + m3)) + m3) - m3 by Th28
                        .= m1 - (m2 + m3) by Th28;
  hence thesis;
 end;

theorem
    m3 c= m2 & m2 c= m1 implies m1 - (m2 - m3) = (m1 - m2) + m3
 proof assume
A1:  m3 c= m2; assume
A2:  m2 c= m1;
A3:  m2 - m3 c= m3 + (m2 - m3) by Th16;
A4:  m2 = m3 + (m2 - m3) by A1,Th27;
then (m3 + (m2 - m3)) - (m2 - m3) c= m1 - (m2 - m3) by A2,A3,Th26;
then A5:  m3 c= m1 - (m2 - m3) by Th28;
thus (m1 - m2) + m3 = ((m1 - (m2 - m3)) - m3) + m3 by A2,A4,Th29
                                .= m1 - (m2 - m3) by A5,Th27;
 end;

theorem Th31:
  m in Funcs(P, NAT)
   proof
A1:  dom m = P by Def1;
      rng m c= NAT by Def1;
    hence m in Funcs(P, NAT) by A1,FUNCT_2:def 2;
   end;

theorem Th32:
  x in Funcs(P, NAT) implies x is marking of P
   proof
    assume x in Funcs(P, NAT);
    then ex f being Function st x = f &
             dom f = P & rng f c= NAT by FUNCT_2:def 2;
    hence x is marking of P by Def1;
   end;

begin :: Transitions and firing

definition let P;
 mode transition of P means :Def7:
   ex m1,m2 st it=[m1,m2];
 existence
  proof
   consider m1,m2;
   take t = [m1, m2];
   thus ex m1,m2 st t = [m1, m2];
  end;
end;

reserve t,t1,t2 for transition of P;

definition
  let P,t;
  redefine func t`1 -> marking of P;
      coherence
       proof
           ex m1,m2 st t = [m1,m2] by Def7;
        hence t`1 is marking of P by MCART_1:7;
       end;
      synonym Pre t;
  func t`2 -> marking of P;
      coherence
       proof
           ex m1, m2 st t = [m1, m2] by Def7;
        hence t`2 is marking of P by MCART_1:7;
       end;
      synonym Post t;
end;

definition
  let P, m, t;
  func fire(t,m) -> marking of P equals :Def8:
     (m - Pre t) + Post t if Pre t c= m
     otherwise m;
  coherence;
  consistency;
end;

theorem
    (Pre t1) + (Pre t2) c= m implies
    fire(t2, fire(t1,m)) = (m - (Pre t1) - Pre t2) + (Post t1) + (Post t2)
  proof
   assume A1: (Pre t1) + (Pre t2) c= m;
   A2: (Pre t1) c= (Pre t1) + (Pre t2) by Th16;
   then A3: (Pre t1) c= m by A1,Th14;
   then A4: fire(t1, m) = m - (Pre t1) + (Post t1) by Def8;
   A5: Pre t2 = (Pre t2) + (Pre t1) - (Pre t1) by Th19;
   A6: (Pre t1) + (Pre t2) - (Pre t1) c= m - (Pre t1) by A1,A2,Th20;
         m - (Pre t1) c= m - (Pre t1) + (Post t1) by Th16;
       then (Pre t2) c= fire(t1, m) by A4,A5,A6,Th14;
   hence
         fire(t2, fire(t1, m)) = fire(t1, m)- (Pre t2) + (Post t2) by Def8
            .= (m - (Pre t1) + (Post t1)) - (Pre t2) + (Post t2) by A3,Def8
            .= (m - (Pre t1) - (Pre t2)) + (Post t1) + (Post t2) by A5,A6,Th21;
  end;

definition
  let P, t;
  func fire t -> Function means: Def9:
    dom it = Funcs(P, NAT) &
    for m being marking of P holds it.m = fire(t,m);
  existence
   proof
     defpred P[set,set] means
     ex m st m = $1 & $2 = fire(t, m);
A1:  for x,y1,y2 st x in Funcs(P, NAT) & P[x,y1] & P[x,y2] holds y1 = y2;
A2:  for x st x in Funcs(P, NAT) ex y st P[x,y]
      proof let x; assume x in Funcs(P, NAT);
        then reconsider m = x as marking of P by Th32;
        take fire(t, m); thus thesis;
      end;
     consider f being Function such that
A3:  dom f = Funcs(P, NAT) and
A4:  for x st x in Funcs(P, NAT) holds P[x,f.x] from FuncEx(A1,A2);
     take f; thus dom f = Funcs(P, NAT) by A3;
     let m; m in Funcs(P, NAT) by Th31;
     then P[m,f.m] by A4;
     hence f.m = fire(t,m);
   end;
  uniqueness
   proof
     let f1,f2 be Function such that
A5:  dom f1 = Funcs(P, NAT) and
A6:  for m being marking of P holds f1.m = fire(t,m) and
A7:  dom f2 = Funcs(P, NAT) and
A8:  for m being marking of P holds f2.m = fire(t,m);
       now let x be set; assume x in dom f1;
       then reconsider m = x as marking of P by A5,Th32;
       thus f1.x = fire(t,m) by A6 .= f2.x by A8;
     end;
     hence f1 = f2 by A5,A7,FUNCT_1:9;
   end;
end;

theorem Th34:
  rng fire t c= Funcs(P, NAT)
   proof
     let y;
     assume y in rng fire t;
     then consider x such that
A1:  x in dom fire t and
A2:  y = (fire t).x by FUNCT_1:def 5;
       dom fire t = Funcs(P, NAT) by Def9;
     then reconsider m=x as marking of P by A1,Th32;
       y = fire(t,m) by A2,Def9;
     hence y in Funcs(P, NAT) by Th31;
   end;

theorem
    fire(t2, fire(t1,m)) = ((fire t2)*(fire t1)).m
   proof
A1:  dom fire t1 = Funcs(P, NAT) by Def9;
A2:  m in Funcs(P, NAT) by Th31;
    thus
       fire(t2, fire(t1,m)) = (fire t2).fire(t1,m) by Def9
                .= (fire t2).((fire t1).m) by Def9
                .= ((fire t2)*(fire t1)).m by A1,A2,FUNCT_1:23;
   end;

definition
  let P;
  mode Petri_net of P -> non empty set means :Def10:
   for x being set st x in it holds x is transition of P;
  existence
   proof
     consider t;
     take N = {t};
     thus for x being set st x in N holds x is transition of P by TARSKI:def 1
;
   end;
end;

reserve N for Petri_net of P;

definition let P, N;
  redefine mode Element of N -> transition of P;
  coherence by Def10;
end;

reserve e, e1,e2 for Element of N;

begin :: Firing sequences of transitions

definition let P, N;
  mode firing-sequence of N is Element of N*;
end;

reserve C,C1,C2,C3,fs,fs1,fs2 for firing-sequence of N;

definition
  let P, N, C;
  func fire C -> Function means :Def11:
  ex F being Function-yielding FinSequence st
     it = compose(F, Funcs(P, NAT)) &
     len F = len C &
     for i being Nat st i in dom C holds F.i = fire (C /. i qua Element of N);
  existence
   proof
     deffunc G(set) = fire (C/.$1 qua Element of N);
     consider F being FinSequence such that
A1:  len F = len C and
A2:  for k being Nat st k in Seg len C holds F.k = G(k) from SeqLambda;
A3:  dom F = Seg len F & dom C = Seg len C by FINSEQ_1:def 3;
       F is Function-yielding
      proof
        let x be set; assume
A4:     x in dom F;
        then reconsider i = x as Nat;
          F.x = fire (C/.i qua Element of N) by A1,A2,A3,A4;
        hence thesis;
      end;
     then reconsider F as Function-yielding FinSequence;
     take f = compose(F, Funcs(P, NAT)), F;
     thus f = compose(F, Funcs(P, NAT));
     thus len F = len C &
     for i being Nat st i in dom C holds F.i = fire (C /. i qua Element of N)
        by A1,A2,A3;
   end;
  uniqueness
   proof
     let f1,f2 be Function;
     given F1 being Function-yielding FinSequence such that
A5:  f1 = compose(F1, Funcs(P, NAT)) and
A6:  len F1 = len C and
A7:  for i being Nat st i in dom C holds F1.i = fire (C/.i qua Element of N);
     given F2 being Function-yielding FinSequence such that
A8:  f2 = compose(F2, Funcs(P, NAT)) and
A9:  len F2 = len C and
A10:  for i being Nat st i in dom C holds F2.i = fire (C/.i qua Element of N);
A11:  dom F1 = Seg len F1 & dom F2 = Seg len F2 & dom C = Seg len C
      by FINSEQ_1:def 3;
       now
       let i be Nat; assume
A12:    i in dom C;
       then F1.i = fire (C/.i qua Element of N) by A7;
       hence F1.i = F2.i by A10,A12;
     end;
     hence thesis by A5,A6,A8,A9,A11,FINSEQ_1:17;
   end;
end;

:: Firing of empty firing-sequence <*>N
theorem
    fire(<*>N) = id Funcs(P, NAT)
   proof
     consider F being Function-yielding FinSequence such that
A1:  fire(<*>N) = compose(F, Funcs(P, NAT)) and
A2:  len F = len <*>N and
       for i being Nat st i in dom <*>N holds
         F.i = fire ((<*>N)/.i qua Element of N) by Def11;
       len F = 0 by A2,FINSEQ_1:32;
     then F = {} by FINSEQ_1:25;
     hence thesis by A1,FUNCT_7:41;
   end;

:: Firing of firing-sequence with one translation <*e*>
theorem Th37:
  fire <*e*> = fire e
   proof
     consider F being Function-yielding FinSequence such that
A1:  fire <*e*> = compose(F, Funcs(P, NAT)) and
A2:  len F = len <*e*> and
A3:  for i being Nat st i in dom <*e*> holds
         F.i = fire (<*e*>/.i qua Element of N) by Def11;
A4:  len <*e*> = 1 & <*e*>.1 = e by FINSEQ_1:57;
       dom <*e*> = {1} by FINSEQ_1:4,def 8;
then A5:  1 in dom <*e*> by TARSKI:def 1;
then A6:  <*e*>/.1 = <*e*>.1 by FINSEQ_4:def 4;
       F.1 = fire (<*e*>/.1 qua Element of N) by A3,A5;
then A7:  F = <*fire e*> by A2,A4,A6,FINSEQ_1:57;
       dom fire e c= Funcs(P,NAT) by Def9;
     hence thesis by A1,A7,FUNCT_7:48;
   end;

theorem Th38:
  (fire e)*id Funcs(P, NAT) = fire e
   proof
A1:  compose(<*fire e*>, Funcs(P, NAT)) = (fire e)*id Funcs(P, NAT)
        by FUNCT_7:47;
       dom fire e c= Funcs(P, NAT) by Def9;
     hence thesis by A1,FUNCT_7:48;
   end;

:: Firing of firing-sequence with two translations <*e1,e2*>
theorem
    fire <*e1,e2*> = (fire e2)*(fire e1)
   proof
     consider F being Function-yielding FinSequence such that
A1:  fire <*e1,e2*> = compose(F, Funcs(P, NAT)) and
A2:  len F = len <*e1,e2*> and
A3:  for i being Nat st i in dom <*e1,e2*> holds
         F.i = fire (<*e1,e2*>/.i qua Element of N) by Def11;
A4:  len <*e1,e2*> = 2 & <*e1,e2*>.1 = e1 & <*e1,e2*>.2 = e2 by FINSEQ_1:61;
then A5:  dom <*e1,e2*> = {1,2} by FINSEQ_1:4,def 3;
     A6: 1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
then A7:  <*e1,e2*>/.1 = <*e1,e2*>.1 & <*e1,e2*>/.2 = <*e1,e2*>.2 by A5,
FINSEQ_4:def 4;
then A8:  F.1 = fire e1 by A3,A4,A5,A6;
       F.2 = fire e2 by A3,A4,A5,A6,A7;
     then A9: F = <*fire e1,fire e2*> by A2,A4,A8,FINSEQ_1:61;
    (fire e1)*id Funcs(P, NAT) = fire e1 by Th38;
     then (fire e2)*(fire e1)*id Funcs(P, NAT) = (fire e2)*(fire e1)
        by RELAT_1:55;
     hence fire <*e1,e2*> = (fire e2)*(fire e1) by A1,A9,FUNCT_7:53;
   end;

theorem Th40:
  dom fire C = Funcs(P, NAT) & rng fire C c= Funcs(P, NAT)
   proof
     defpred P[Nat] means
        for F being Function-yielding FinSequence st
          len F = $1 &
          for i st i in dom F ex t st F.i = fire t
        holds dom compose(F, Funcs(P, NAT)) = Funcs(P, NAT) &
              rng compose(F, Funcs(P, NAT)) c= Funcs(P, NAT);
A1:  P[0]
       proof let F be Function-yielding FinSequence;
         assume len F = 0;
         then F = {} by FINSEQ_1:25;
         then compose(F, Funcs(P, NAT)) = id Funcs(P, NAT) by FUNCT_7:41;
         hence thesis by RELAT_1:71;
       end;
A2:  for k st P[k] holds P[k + 1]
       proof let k such that
A3:      for G being Function-yielding FinSequence st
           len G = k &
           for i st i in dom G ex t st G.i = fire t
         holds dom compose(G, Funcs(P, NAT)) = Funcs(P, NAT) &
               rng compose(G, Funcs(P, NAT)) c= Funcs(P, NAT);
         let F be Function-yielding FinSequence such that
A4:      len F = k+1 and
A5:      for i st i in dom F ex t st F.i = fire t;
         consider G being FinSequence, x being set such that
A6:      F = G^<*x*> & len G = k by A4,TREES_2:4;
         reconsider G as Function-yielding FinSequence by A6,FUNCT_7:25;
           k+1 in dom F
          proof
              0 <= k by NAT_1:18;
            then 0+1 <= k+1 by REAL_1:55;
            hence thesis by A4,FINSEQ_3:27;
          end;
         then consider t such that
A7:      F.(k+1) = fire t by A5;
           x = F.(k+1) by A6,FINSEQ_1:59;
then A8:      compose(F, Funcs(P, NAT)) = (fire t)*compose(G, Funcs(P, NAT))
           by A6,A7,FUNCT_7:43;
A9:      dom fire t = Funcs(P, NAT) & rng fire t c= Funcs(P, NAT)
           by Def9,Th34;
           for i st i in dom G ex t st G.i = fire t
          proof
            let i;
A10:         dom G c= dom F by A6,FINSEQ_1:39; assume
A11:         i in dom G;
            then consider t such that
A12:         F.i = fire t by A5,A10;
              G.i = F.i by A6,A11,FINSEQ_1:def 7;
            hence thesis by A12;
          end;
         then dom compose(G, Funcs(P, NAT)) = Funcs(P, NAT) &
         rng compose(G, Funcs(P, NAT)) c= Funcs(P, NAT) by A3,A6;
         then dom compose(F, Funcs(P, NAT)) = Funcs(P, NAT) &
         rng compose(F, Funcs(P, NAT)) c= rng fire t
               by A8,A9,RELAT_1:45,46;
        hence thesis by A9,XBOOLE_1:1;
     end;
A13:  P[k] from Ind(A1,A2);
     consider F being Function-yielding FinSequence such that
A14:  fire C = compose(F, Funcs(P, NAT)) and
A15:  len F = len C and
A16:  for i being Nat st i in dom C holds
         F.i = fire (C/.i qua Element of N) by Def11;
       for i st i in dom F ex t st F.i = fire t
      proof
        let i; assume
A17:     i in dom F;
        A18: dom F = Seg len F & dom C = Seg len C by FINSEQ_1:def 3;
        reconsider t = C/.i as Element of N;
        take t;
        thus thesis by A15,A16,A17,A18;
      end;
     hence thesis by A13,A14,A15;
   end;

:: Firing of compound firing-sequence
theorem Th41:
  fire (C1^C2) = (fire C2)*(fire C1)
   proof
     consider F being Function-yielding FinSequence such that
A1:  fire (C1^C2) = compose(F, Funcs(P, NAT)) and
A2:  len F = len (C1^C2) and
A3:  for i being Nat st i in dom (C1^C2) holds
         F.i = fire ((C1^C2)/.i qua Element of N) by Def11;
     consider F1 being Function-yielding FinSequence such that
A4:  fire C1 = compose(F1, Funcs(P, NAT)) and
A5:  len F1 = len C1 and
A6:  for i being Nat st i in dom C1 holds
         F1.i = fire (C1/.i qua Element of N) by Def11;
     consider F2 being Function-yielding FinSequence such that
A7:  fire C2 = compose(F2, Funcs(P, NAT)) and
A8:  len F2 = len C2 and
A9:  for i being Nat st i in dom C2 holds
         F2.i = fire (C2/.i qua Element of N) by Def11;
A10:  rng fire C1 c= Funcs(P, NAT) by Th40;
       len F = len C1 + len C2 by A2,FINSEQ_1:35;
then A11:  dom F = Seg (len F1 + len F2) by A5,A8,FINSEQ_1:def 3;
A12:  for k st k in dom F1 holds F.k = F1.k
      proof
        let k; assume
A13:     k in dom F1;
        A14: dom F1 = Seg len F1 by FINSEQ_1:def 3;
        A15: dom F1 = Seg len C1 by A5,FINSEQ_1:def 3;
        A16: dom F1 = dom C1 by A5,A14,FINSEQ_1:def 3;
A17:     k in dom C1 by A13,A15,FINSEQ_1:def 3;
        A18: dom C1 c= dom (C1^C2) by FINSEQ_1:39;
then A19:     F.k = fire ((C1^C2)/.k qua Element of N) by A3,A17;
A20:     (C1^C2)/.k = (C1^C2).k by A17,A18,FINSEQ_4:def 4;
A21:     (C1^C2).k = C1.k by A13,A16,FINSEQ_1:def 7;
          C1.k = C1/.k by A13,A16,FINSEQ_4:def 4;
        hence thesis by A6,A13,A16,A19,A20,A21;
      end;
       for k st k in dom F2 holds F.(len F1 + k) = F2.k
      proof
        let k; assume
A22:     k in dom F2;
          dom F2 = Seg len F2 by FINSEQ_1:def 3;
        then A23: dom F2 = dom C2 by A8,FINSEQ_1:def 3;
then A24:     len F1 + k in dom (C1^C2) by A5,A22,FINSEQ_1:41;
then A25:     F.(len F1 + k) = fire ((C1^C2)/.(len F1 + k) qua Element of N)
by A3;
A26:     (C1^C2)/.(len F1 + k) = (C1^C2).(len F1 +k) by A24,FINSEQ_4:def 4;
A27:     (C1^C2).(len F1 + k) = C2.k by A5,A22,A23,FINSEQ_1:def 7;
          C2.k = C2/.k by A22,A23,FINSEQ_4:def 4;
        hence thesis by A9,A22,A23,A25,A26,A27;
      end;
     then F = F1^F2 by A11,A12,FINSEQ_1:def 7;
     hence thesis by A1,A4,A7,A10,FUNCT_7:50;
   end;

theorem
    fire (C^<*e*>) = (fire e)*(fire C)
   proof
       fire (C^<*e*>) = (fire <*e*>)*(fire C) by Th41;
     hence thesis by Th37;
   end;

definition
  let P, N, C, m;
  func fire(C, m) -> marking of P equals
     (fire C).m;
  coherence
   proof
A1:  dom fire C = Funcs(P, NAT) & rng fire C c= Funcs(P, NAT) by Th40;
     then m in dom fire C by Th31;
     then [m,(fire C).m] in fire C by FUNCT_1:def 4;
     then (fire C).m in rng fire C by RELAT_1:def 5;
     hence (fire C).m is marking of P by A1,Th32;
    end;
end;

begin :: Sequential composition

definition let P, N;
 mode process of N is Subset of N*;
end;

reserve R, R1, R2, R3, P1, P2 for process of N;

definition
  cluster FinSequence-like -> FinSubsequence-like Function;
  coherence by FINSEQ_1:68;
end;

definition
  let P, N, R1, R2;
  func R1 before R2 -> process of N equals :Def13:
   {C1^C2: C1 in R1 & C2 in R2};
  coherence
   proof
     set X = {C1^C2: C1 in R1 & C2 in R2};
       X c= N*
       proof
         let x; assume x in X;
         then ex C1,C2 st x = C1^C2 & C1 in R1 & C2 in R2;
         hence x in N*;
       end;
     hence thesis;
   end;
end;

definition
 let P, N;
 let R1, R2 be non empty process of N;
 cluster R1 before R2 -> non empty;
 coherence
   proof
A1:  R1 before R2 = {C1^C2: C1 in R1 & C2 in R2} by Def13;
     consider fs1 being set such that
A2:  fs1 in R1 by XBOOLE_0:def 1;
     consider fs2 being set such that
A3:  fs2 in R2 by XBOOLE_0:def 1;
     reconsider fs1,fs2 as firing-sequence of N by A2,A3;
       fs1^fs2 in R1 before R2 by A1,A2,A3;
     hence thesis;
   end;
end;

theorem Th43:
 (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
  proof
   thus (R1 \/ R2) before R c= (R1 before R) \/ (R2 before R)
     proof
      let x; assume x in (R1 \/ R2) before R;
       then x in {fs1^fs: fs1 in R1 \/ R2 & fs in R} by Def13;
       then consider fs1, fs such that
A1:    x = fs1^fs & fs1 in R1 \/ R2 & fs in R;
         fs1 in R1 or fs1 in R2 by A1,XBOOLE_0:def 2;
       then x in {a1^a where a1,a is firing-sequence of N: a1 in R1 & a in R}
or
       x in {b2^b where b2,b is firing-sequence of N: b2 in R2 & b in R}
          by A1;
       then x in R1 before R or x in R2 before R by Def13;
      hence thesis by XBOOLE_0:def 2;
     end;
   let x be set; assume
A2: x in (R1 before R) \/ (R2 before R);
   per cases by A2,XBOOLE_0:def 2;
   suppose x in R1 before R;
    then x in {fs1^fs: fs1 in R1 & fs in R} by Def13;
    then consider fs1, fs such that
A3: x = fs1^fs & fs1 in R1 & fs in R;
      fs1 in R1 \/ R2 by A3,XBOOLE_0:def 2;
    then x in {a1^a where a1,a is firing-sequence of N: a1 in R1 \/ R2 & a in
R}
       by A3;
    hence thesis by Def13;
   suppose x in R2 before R;
    then x in {fs2^fs: fs2 in R2 & fs in R} by Def13;
    then consider fs2, fs such that
A4: x = fs2^fs & fs2 in R2 & fs in R;
      fs2 in R1 \/ R2 by A4,XBOOLE_0:def 2;
    then x in {a2^a where a2,a is firing-sequence of N: a2 in R1 \/ R2 & a in
R}
       by A4;
    hence thesis by Def13;
  end;

theorem Th44:
 R before (R1 \/ R2) = (R before R1) \/ (R before R2)
  proof
   thus R before (R1 \/ R2) c= (R before R1) \/ (R before R2)
     proof
      let x; assume x in R before (R1 \/ R2);
       then x in {fs^fs1: fs in R & fs1 in R1 \/ R2} by Def13;
       then consider fs, fs1 such that
A1:    x = fs^fs1 & fs in R & fs1 in R1 \/ R2;
         fs1 in R1 or fs1 in R2 by A1,XBOOLE_0:def 2;
       then x in {a^a1 where a,a1 is firing-sequence of N: a in R & a1 in R1}
or
       x in {b^b2 where b,b2 is firing-sequence of N: b in R & b2 in R2}
          by A1;
       then x in R before R1 or x in R before R2 by Def13;
      hence thesis by XBOOLE_0:def 2;
     end;
   let x be set; assume
A2: x in (R before R1) \/ (R before R2);
   per cases by A2,XBOOLE_0:def 2;
   suppose x in R before R1;
    then x in {fs^fs1: fs in R & fs1 in R1} by Def13;
    then consider fs, fs1 such that
A3: x = fs^fs1 & fs in R & fs1 in R1;
      fs1 in R1 \/ R2 by A3,XBOOLE_0:def 2;
    then x in {a^a1 where a,a1 is firing-sequence of N: a in R & a1 in R1 \/
R2}
       by A3;
    hence thesis by Def13;
   suppose x in R before R2;
    then x in {fs^fs2: fs in R & fs2 in R2} by Def13;
    then consider fs, fs2 such that
A4: x = fs^fs2 & fs in R & fs2 in R2;
      fs2 in R1 \/ R2 by A4,XBOOLE_0:def 2;
    then x in {a^a2 where a,a2 is firing-sequence of N: a in R & a2 in R1 \/
R2}
       by A4;
    hence thesis by Def13;
  end;

theorem Th45:
 {C1} before {C2} = {C1^C2}
   proof
     set X = {fs1^fs2: fs1 in {C1} & fs2 in {C2}};
A1:  {C1} before {C2} = X by Def13;
     thus {C1} before {C2} c= {C1^C2}
       proof
         let x; assume x in {C1} before {C2};
         then consider fs1, fs2 such that
A2:      x = fs1^fs2 & fs1 in {C1} & fs2 in {C2} by A1;
       fs1 = C1 & fs2 = C2 by A2,TARSKI:def 1;
         hence x in {C1^C2} by A2,TARSKI:def 1;
       end;
     let x;
     assume x in {C1^C2};
     then x = C1^C2 & C1 in {C1} & C2 in {C2} by TARSKI:def 1;
     hence x in {C1} before {C2} by A1;
   end;

theorem
   {C1,C2} before {C} = {C1^C, C2^C}
   proof
    thus
       {C1,C2} before {C} = ({C1} \/ {C2}) before {C} by ENUMSET1:41
                       .= ({C1} before {C}) \/ ({C2} before {C}) by Th43
                       .= {C1^C} \/ ({C2} before {C}) by Th45
                       .= {C1^C} \/ {C2^C} by Th45
                       .= {C1^C, C2^C} by ENUMSET1:41;
   end;

theorem
   {C} before {C1,C2} = {C^C1, C^C2}
   proof
    thus
       {C} before {C1,C2} = {C} before ({C1} \/ {C2}) by ENUMSET1:41
                       .= ({C} before {C1}) \/ ({C} before {C2}) by Th44
                       .= {C^C1} \/ ({C} before {C2}) by Th45
                       .= {C^C1} \/ {C^C2} by Th45
                       .= {C^C1, C^C2} by ENUMSET1:41;
   end;

begin :: Concurrent composition

definition
  let P, N, R1, R2;
  func R1 concur R2 -> process of N equals :Def14:
   {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
       Seq q1 in R1 & Seq q2 in R2};
  coherence
    proof
      set X = {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 &
                  q1 misses q2 & Seq q1 in R1 & Seq q2 in R2};
        X c= N*
       proof
         let x; assume x in X;
         then ex C st x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 &
         q1 misses q2 & Seq q1 in R1 & Seq q2 in R2;
         hence thesis;
       end;
       hence thesis;
    end;
  commutativity
   proof
    let R,R1,R2;
    assume
A1:  R = {C1: ex q1,q2 being FinSubsequence st C1 = q1 \/ q2 &
          q1 misses q2 & Seq q1 in R1 & Seq q2 in R2};
    thus R c= {C2: ex q1,q2 being FinSubsequence st C2 = q1 \/ q2 &
               q1 misses q2 & Seq q1 in R2 & Seq q2 in R1}
      proof let x; assume x in R;
        then consider C1 such that
A2:     x = C1 & ex q1,q2 being FinSubsequence st C1 = q1 \/ q2 &
        q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 by A1;
        set X = {C2: ex q1,q2 being FinSubsequence st C2 = q1 \/ q2 &
                   q1 misses q2 & Seq q1 in R2 & Seq q2 in R1};
        thus x in X by A2;
      end;
    let x; assume x in {C2: ex q1,q2 being FinSubsequence st C2 = q1 \/ q2 &
                    q1 misses q2 & Seq q1 in R2 & Seq q2 in R1};
    then consider C2 such that
A3: x = C2 & ex q1,q2 being FinSubsequence st C2 = q1 \/ q2 &
    q1 misses q2 & Seq q1 in R2 & Seq q2 in R1;
    thus x in R by A1,A3;
   end;
end;

theorem Th48:
 (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
  proof
   thus (R1 \/ R2) concur R c= (R1 concur R) \/ (R2 concur R)
     proof
      let x; assume x in (R1 \/ R2) concur R;
       then x in {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses
q2 &
             Seq q1 in R1 \/ R2 & Seq q2 in R} by Def14;
       then consider C such that
A1:    x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
       Seq q1 in R1 \/ R2 & Seq q2 in R;
       consider q1,q2 being FinSubsequence such that
A2:    C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 \/ R2 & Seq q2 in R by A1;
         Seq q1 in R1 or Seq q1 in R2 by A2,XBOOLE_0:def 2;
       then x in {C1: ex q1,q2 being FinSubsequence st C1 = q1 \/ q2 & q1
misses q2
             & Seq q1 in R1 & Seq q2 in R} or
       x in {C2: ex q1,q2 being FinSubsequence st C2 = q1 \/ q2 & q1 misses q2
             & Seq q1 in R2 & Seq q2 in R} by A1,A2;
       then x in R1 concur R or x in R2 concur R by Def14;
      hence thesis by XBOOLE_0:def 2;
     end;
   let x be set; assume
A3: x in (R1 concur R) \/ (R2 concur R);
   per cases by A3,XBOOLE_0:def 2;
   suppose x in R1 concur R;
    then x in {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2
&
          Seq q1 in R1 & Seq q2 in R} by Def14;
    then consider C such that
A4: x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
    Seq q1 in R1 & Seq q2 in R;
    consider q1,q2 being FinSubsequence such that
A5: C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R by A4;
      Seq q1 in R1 \/ R2 by A5,XBOOLE_0:def 2;
    then x in {C1: ex q1,q2 being FinSubsequence st C1 = q1 \/ q2 & q1 misses
q2 &
          Seq q1 in R1 \/ R2 & Seq q2 in R} by A4,A5;
    hence thesis by Def14;
   suppose x in R2 concur R;
    then x in {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2
&
          Seq q1 in R2 & Seq q2 in R} by Def14;
    then consider C such that
A6: x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
    Seq q1 in R2 & Seq q2 in R;
    consider q1,q2 being FinSubsequence such that
A7: C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R by A6;
      Seq q1 in R1 \/ R2 by A7,XBOOLE_0:def 2;
    then x in {C2: ex q1,q2 being FinSubsequence st C2 = q1 \/ q2 & q1 misses
q2 &
          Seq q1 in R1 \/ R2 & Seq q2 in R} by A6,A7;
    hence thesis by Def14;
  end;

theorem Th49:
 {<*e1*>} concur {<*e2*>} = {<*e1,e2*>, <*e2,e1*>}
   proof
     set C1 = <*e1*>, C2 = <*e2*>;
     set R1 = {C1}, R2 = {C2};
     set X = {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
       Seq q1 in R1 & Seq q2 in R2};
A1:  {C1} concur {C2} = X by Def14;
     thus {C1} concur {C2} c= {<*e1,e2*>, <*e2,e1*>}
       proof
         let x; assume x in {C1} concur {C2};
         then consider C such that
A2:      x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
         Seq q1 in R1 & Seq q2 in R2 by A1;
         consider q1,q2 being FinSubsequence such that
A3:      C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 by A2;
A4:      Seq q1 = C1 & Seq q2 = C2 by A3,TARSKI:def 1;
         then consider i such that
A5:      q1 = {[i,e1]} by Th4;
         consider j such that
A6:      q2 = {[j,e2]} by A4,Th4;
         A7: [i,e1] in q1 & [j,e2] in q2 by A5,A6,TARSKI:def 1;
A8:      C = {[i,e1], [j,e2]} by A3,A5,A6,ENUMSET1:41;
         then i = 1 & j = 1 & e1 = e2 or
         i = 1 & j = 2 or
         i = 2 & j = 1 by Th5;
         then C = <*e1,e2*> or C = <*e2,e1*> by A3,A7,A8,Th6,XBOOLE_0:3;
         hence thesis by A2,TARSKI:def 2;
       end;
     let x;
     assume
A9:  x in {<*e1,e2*>, <*e2,e1*>};
     per cases by A9,TARSKI:def 2;
       suppose
A10:    x = <*e1,e2*>;
then A11:    x = {[1,e1], [2,e2]} by Th6
        .= {[1,e1]} \/ {[2,e2]} by ENUMSET1:41;
       reconsider q1 = {[1,e1]}, q2 = {[2,e2]} as FinSubsequence by Th1;
         [1,e1] <> [2,e2] by ZFMISC_1:33;
       then not [1,e1] in q2 by TARSKI:def 1;
then A12:    q1 misses q2 by ZFMISC_1:56;
A13:    Seq q1 = <*e1*> & Seq q2 = <*e2*> by Th3;
         <*e1*> in R1 & <*e2*> in R2 by TARSKI:def 1;
       hence thesis by A1,A10,A11,A12,A13;
       suppose
A14:    x = <*e2,e1*>;
then A15:    x = {[1,e2], [2,e1]} by Th6
        .= {[1,e2]} \/ {[2,e1]} by ENUMSET1:41;
       reconsider q1 = {[2,e1]}, q2 = {[1,e2]} as FinSubsequence by Th1;
         [1,e2] <> [2,e1] by ZFMISC_1:33;
       then not [2,e1] in q2 by TARSKI:def 1;
then A16:    q1 misses q2 by ZFMISC_1:56;
A17:    Seq q1 = <*e1*> & Seq q2 = <*e2*> by Th3;
         <*e1*> in R1 & <*e2*> in R2 by TARSKI:def 1;
       hence thesis by A1,A14,A15,A16,A17;
   end;

theorem
   {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>, <*e2,e*>, <*e,e1*>, <*e,e2*>}
  proof
      {<*e1*>,<*e2*>} = {<*e1*>} \/ {<*e2*>} by ENUMSET1:41;
then A1:  {<*e1*>,<*e2*>} concur {<*e*>}
                = {<*e1*>} concur {<*e*>} \/ {<*e2*>} concur {<*e*>} by Th48;
A2: {<*e1*>} concur {<*e*>} = {<*e1,e*>,<*e,e1*>} by Th49;
      {<*e2*>} concur {<*e*>} = {<*e2,e*>,<*e,e2*>} by Th49;
   hence
      {<*e1*>,<*e2*>} concur {<*e*>}
                = {<*e1,e*>, <*e,e1*>, <*e2,e*>, <*e,e2*>} by A1,A2,ENUMSET1:45
               .= {<*e1,e*>, <*e2,e*>, <*e,e1*>, <*e,e2*>} by ENUMSET1:104;
  end;

theorem
    (R1 before R2) before R3 = R1 before (R2 before R3)
   proof
A1:  (R1 before R2) before R3
         = {C1^C2: C1 in (R1 before R2) & C2 in R3} by Def13;
     thus (R1 before R2) before R3 c= R1 before (R2 before R3)
      proof
        let x;
        assume x in (R1 before R2) before R3;
        then consider C1,C2 such that
A2:     x = C1^C2 & C1 in (R1 before R2) & C2 in R3 by A1;
          R1 before R2 = {fs1^fs2: fs1 in R1 & fs2 in R2} by Def13;
        then consider fs1,fs2 such that
A3:     C1 = fs1^fs2 & fs1 in R1 & fs2 in R2 by A2;
A4:     x = fs1^(fs2^C2) by A2,A3,FINSEQ_1:45;
        consider C3 such that
A5:     C3 = fs2^C2 & fs2 in R2 & C2 in R3 by A2,A3;
          C3 in {a2^a3 where a2,a3 is firing-sequence of N: a2 in R2 & a3 in R3
}
           by A5;
then C3 in R2 before R3 by Def13;
        then x in {a^a1 where a,a1 is firing-sequence of N:
                 a in R1 & a1 in (R2 before R3)} by A3,A4,A5;
        hence x in R1 before (R2 before R3) by Def13;
      end;
A6:   R1 before (R2 before R3)
         = {C1^C2: C1 in R1 & C2 in R2 before R3} by Def13;
      let x;
      assume x in R1 before (R2 before R3);
      then consider C1,C2 such that
A7:   x = C1^C2 & C1 in R1 & C2 in R2 before R3 by A6;
        R2 before R3 = {fs1^fs2: fs1 in R2 & fs2 in R3} by Def13;
      then consider fs1,fs2 such that
A8:   C2 = fs1^fs2 & fs1 in R2 & fs2 in R3 by A7;
A9:   x = (C1^fs1)^fs2 by A7,A8,FINSEQ_1:45;
      consider C such that
A10:  C = C1^fs1 & C1 in R1 & fs1 in R2 by A7,A8;
        C in {a1^b1 where a1,b1 is firing-sequence of N: a1 in R1 & b1 in R2}
         by A10;
      then C in R1 before R2 by Def13;
      then x in {a^b where a,b is firing-sequence of N:
              a in R1 before R2 & b in R3} by A8,A9,A10;
      hence x in (R1 before R2) before R3 by Def13;
   end;

definition
  let p be FinSubsequence;
  let i be Nat;
     set X = {i+k where k is Nat: k in dom p};
  func i Shift p -> FinSubsequence means
:Def15:
   dom it = {i+k where k is Nat: k in dom p} &
   for j being Nat st j in dom p holds it.(i+j) = p.j;
   existence
   proof
     consider K being Nat such that
A1:  dom p c= Seg K by FINSEQ_1:def 12;
     defpred P[set,set] means ex k st $1 = i+k & $2 = p.k;
A2:  for x,y1,y2 st x in X & P[x,y1] & P[x,y2] holds y1 = y2
      by XCMPLX_1:2;
A3:  for x st x in X ex y st P[x,y]
      proof
        let x; assume x in X;
        then consider k such that
A4:     x = i+k & k in dom p;
          [k,p.k] in p by A4,FUNCT_1:def 4;
        hence thesis by A4;
      end;
     consider f being Function such that
A5:  dom f = X and
A6:  for x st x in X holds P[x,f.x] from FuncEx(A2,A3);
       X c= Seg (i+K)
      proof
        let x; assume x in X;
        then consider k such that
A7:     x = i+k & k in dom p;
          i+k >= k & k >= 1 & k <= K by A1,A7,FINSEQ_1:3,NAT_1:29;
        then i+k >= 1 & i+k <= i+K by AXIOMS:22,24;
        hence x in Seg (i+K) by A7,FINSEQ_1:3;
      end;
     then reconsider f as FinSubsequence by A5,FINSEQ_1:def 12;
     take f; thus dom f = X by A5;
     let j; assume j in dom p;
     then i+j in X;
     then ex k st i+j = i+k & f.(i+j) = p.k by A6;
     hence thesis by XCMPLX_1:2;
   end;
  uniqueness
   proof
     let f1,f2 be FinSubsequence such that
A8:  dom f1 = X and
A9:  for j being Nat st j in dom p holds f1.(i+j) = p.j and
A10:  dom f2 = X and
A11:  for j being Nat st j in dom p holds f2.(i+j) = p.j;
       now let x be set; assume x in X;
       then consider k such that
A12:    x = i+k & k in dom p;
       thus f1.x = p.k by A9,A12 .= f2.x by A11,A12;
     end;
     hence thesis by A8,A10,FUNCT_1:9;
   end;
end;

reserve q,q1,q2,q3,q4 for FinSubsequence;

theorem Th52:
  0 Shift q = q
   proof
     set X = {0+k where k is Nat: k in dom q};
A1:  dom (0 Shift q) = X by Def15;
A2:  X = dom q
      proof
        thus X c= dom q
         proof
           let x;
           assume x in X;
           then consider k such that
A3:        x = 0+k & k in dom q;
           thus x in dom q by A3;
         end;
        let x; assume
A4:     x in dom q;
        consider l being Nat such that
A5:     dom q c= Seg l by FINSEQ_1:def 12;
          x in Seg l by A4,A5;
        then reconsider k = x as Nat;
      x = 0+k;
        hence x in X by A4;
      end;
       now
       let x; assume x in X;
       then consider k such that
A6:    x = 0+k & k in dom q;
       thus (0 Shift q).x = q.x by A6,Def15;
     end;
     hence thesis by A1,A2,FUNCT_1:9;
   end;

theorem
    (i+j) Shift q = i Shift (j Shift q)
   proof
     set Sj = j Shift q;
     set Sij = (i+j) Shift q;
     set Si = i Shift Sj;
     set Xj = {j+k where k is Nat: k in dom q};
     set Xi = {i+k where k is Nat: k in dom Sj};
     set Xij = {(i+j)+k where k is Nat: k in dom q};
A1:  dom Sj = Xj & dom Si = Xi & dom Sij = Xij by Def15;
A2:  Xi = Xij
      proof
        thus Xi c= Xij
         proof
           let x; assume x in Xi;
           then consider k such that
A3:        x = i+k & k in dom Sj;
             dom (j Shift q) = {j+K where K is Nat: K in dom q} by Def15;
           then consider K being Nat such that
A4:        k = j+K & K in dom q by A3;
             x = i+j+K & K in dom q by A3,A4,XCMPLX_1:1;
           hence x in Xij;
         end;
        let x; assume x in Xij;
        then consider k such that
A5:     x = (i+j)+k & k in dom q;
        reconsider K = j+k as Nat;
      dom Sj = {j+l where l is Nat: l in dom q} by Def15;
        then x = i+K & K in dom Sj by A5,XCMPLX_1:1;
        hence x in Xi;
      end;
       now
       let x; assume x in Xij;
       then consider k such that
A6:    x = (i+j)+k & k in dom q;
A7:    x = i+(j+k) & j+k in dom Sj by A1,A6,XCMPLX_1:1;
       thus Sij.x = q.k by A6,Def15 .= Sj.(j+k) by A6,Def15 .= Si.x
          by A7,Def15;
     end;
     hence thesis by A1,A2,FUNCT_1:9;
   end;

theorem Th54:
 for p being FinSequence st p <> {} holds
    dom (i Shift p) = {j1: i+1 <= j1 & j1 <= i+(len p)}
  proof
    let p be FinSequence; assume
      p <> {};
A1:  dom p = Seg len p by FINSEQ_1:def 3
         .= {k: 1 <= k & k <= len p} by FINSEQ_1:def 1;
    set X = {j1: i+1 <= j1 & j1 <= i+(len p)};
A2: dom (i Shift p) = {i+k1: k1 in dom p} by Def15;
    thus dom (i Shift p) c= X
     proof
       let x;
       assume x in dom (i Shift p);
       then consider k1 such that
A3:    x = i+k1 & k1 in dom p by A2;
       consider k such that
A4:    k1 = k & 1 <= k & k <= len p by A1,A3;
         i+1 <= i+k & i+k <= i+(len p) by A4,REAL_1:55;
       hence thesis by A3,A4;
     end;
    let x; assume
  x in X;
     then consider j1 such that
A5:  x = j1 & i+1 <= j1 & j1 <= i+(len p);
       i+0 <= i+1 by REAL_1:55;
     then i <= j1 by A5,AXIOMS:22;
     then consider k2 such that
A6: j1 = i+k2 by NAT_1:28;
       1 <= k2 & k2 <= len p by A5,A6,REAL_1:53;
     then k2 in dom p by A1;
     hence x in dom (i Shift p) by A2,A5,A6;
  end;

theorem Th55:
  for q being FinSubsequence holds q = {} iff i Shift q = {}
   proof let q be FinSubsequence;
A1:  dom (i Shift q) = {i+k: k in dom q} by Def15;
     thus q = {} implies (i Shift q) = {}
      proof assume
        A2: q = {};
        A3: now given x1 such that
A4:       x1 in dom q;
            [x1,q.x1] in q by A4,FUNCT_1:def 4;
          hence contradiction by A2;
        end;
          now let x,y;
            now assume
              x in dom (i Shift q);
            then consider k such that
A5:         x = i+k & k in dom q by A1;
            thus contradiction by A3,A5;
          end;
          hence not [x,y] in (i Shift q) by FUNCT_1:8;
        end;
        hence thesis by RELAT_1:56;
      end; assume
A6:   (i Shift q) = {};
       now assume q <> {};
       then dom q <> {} by RELAT_1:64;
       then consider x such that
A7:    x in dom q by XBOOLE_0:def 1;
A8:    x in rng Sgm dom q by A7,FINSEQ_1:71;
         rng Sgm dom q c= NAT by FINSEQ_1:def 4;
       then reconsider x as Nat by A8;
       consider k such that
A9:    k = i+x & x in dom q by A7;
         k in dom (i Shift q) by A1,A9;
       hence contradiction by A6,RELAT_1:60;
     end;
     hence thesis;
   end;

theorem Th56:
  for q being FinSubsequence ex ss being FinSubsequence st
     dom ss = dom q & rng ss = dom (i Shift q) &
        (for k st k in dom q holds ss.k = i+k) & ss is one-to-one
   proof let q be FinSubsequence;
     consider n being Nat such that
A1:  dom q c= Seg n by FINSEQ_1:def 12;
A2:  Seg n = {k: 1 <= k & k <= n} by FINSEQ_1:def 1;
     defpred P[set,set] means ex k st k = $1 & $2 = i+k;
A3:  for x,y1,y2 st x in dom q & P[x,y1] & P[x,y2] holds y1 = y2;
A4:  for x st x in dom q ex y st P[x,y]
      proof let x; assume x in dom q;
        then x in Seg n by A1;
        then consider k1 such that
A5:     x = k1 & 1 <= k1 & k1 <= n by A2;
        reconsider x as Nat by A5;
        take i+x;
        thus thesis;
      end;
     consider f being Function such that
A6:  dom f = dom q and
A7:  for x st x in dom q holds P[x, f.x] from FuncEx(A3,A4);
     reconsider ss = f as FinSubsequence by A1,A6,FINSEQ_1:def 12;
A8:  dom (i Shift q) = {i+k: k in dom q} by Def15;
A9:  rng ss = dom (i Shift q)
      proof
        thus rng ss c= dom (i Shift q)
         proof let y; assume y in rng ss;
           then consider x such that
A10:        x in dom ss & y = ss.x by FUNCT_1:def 5;
           consider k1 such that
A11:        k1 = x & ss.x = i+k1 by A6,A7,A10;
           thus thesis by A6,A8,A10,A11;
         end; let y; assume y in dom (i Shift q);
        then consider k2 such that
A12:     y = i+k2 & k2 in dom q by A8;
        consider k3 being Nat such that
A13:     k3 = k2 & ss.k2 = i+k3 by A7,A12;
        thus thesis by A6,A12,A13,FUNCT_1:def 5;
      end;
A14:  for k st k in dom q holds ss.k = i+k
      proof let k; assume k in dom q;
        then consider k1 such that
A15:     k1 = k & ss.k = i+k1 by A7;
        thus thesis by A15;
      end;
       ss is one-to-one
      proof
          for x1,x2 st x1 in dom ss & x2 in dom ss & ss.x1 = ss.x2 holds x1 =
x2
         proof let x1,x2; assume
A16:        x1 in dom ss & x2 in dom ss & ss.x1 = ss.x2;
           then consider k1 such that
A17:        k1 = x1 & ss.x1 = i+k1 by A6,A7;
           consider k2 such that
A18:        k2 = x2 & ss.x2 = i+k2 by A6,A7,A16;
           thus thesis by A16,A17,A18,XCMPLX_1:2;
         end;
        hence thesis by FUNCT_1:def 8;
      end;
     hence thesis by A6,A9,A14;
   end;

Lm7:
  for p being FinSequence holds ex fs being FinSequence st
     dom fs = dom p & rng fs = dom (i Shift p) &
        (for k st k in dom p holds fs.k = i+k) & fs is one-to-one
   proof let p be FinSequence;
     consider ss being FinSubsequence such that
A1:  dom ss = dom p & rng ss = dom (i Shift p) &
        (for k st k in dom p holds ss.k = i+k) & ss is one-to-one by Th56;
       dom ss = Seg len p by A1,FINSEQ_1:def 3;
     then reconsider fs = ss as FinSequence by FINSEQ_1:def 2;
       dom fs = dom p & rng fs = dom (i Shift p) &
        (for k st k in dom p holds fs.k = i+k) & fs is one-to-one by A1;
     hence thesis;
   end;

theorem Th57:
  for q being FinSubsequence holds Card q = Card (i Shift q)
   proof let q be FinSubsequence;
     consider ss being FinSubsequence such that
A1:  dom ss = dom q & rng ss = dom (i Shift q) &
     (for k st k in dom q holds ss.k = i+k) & ss is one-to-one by Th56;
     A2: dom q, dom (i Shift q) are_equipotent by A1,WELLORD2:def 4;
       Card dom q = Card q & Card dom (i Shift q) = Card (i Shift q)
        by PRE_CIRC:21;
     hence thesis by A2,CARD_1:21;
   end;

theorem Th58:
  for p being FinSequence holds dom p = dom Seq (i Shift p)
   proof let p be FinSequence;
A1:  rng Sgm dom (i Shift p) = dom (i Shift p) by FINSEQ_1:71;
     A2: Seq (i Shift p) = (i Shift p)*(Sgm dom (i Shift p))
        by FINSEQ_1:def 14;
A3:  dom p = Seg len p &
       dom Sgm dom (i Shift p) = Seg len Sgm dom (i Shift p) by FINSEQ_1:def 3;
     consider k such that
A4:  dom (i Shift p) c= Seg k by FINSEQ_1:def 12;
A5:  len Sgm dom (i Shift p) = Card dom (i Shift p) by A4,FINSEQ_3:44;
       Card dom (i Shift p) = Card (i Shift p) by PRE_CIRC:21;
     then Card dom (i Shift p) = len p by Th57;
     hence dom p = dom Seq (i Shift p) by A1,A2,A3,A5,RELAT_1:46;
   end;

theorem Th59:
  for p being FinSequence st k in dom p holds (Sgm dom (i Shift p)).k = i + k
   proof let p be FinSequence; assume
A1:  k in dom p;
     consider fs being FinSequence such that
A2:  dom fs = dom p & rng fs = dom (i Shift p) &
        (for j st j in dom p holds fs.j = i+j) & fs is one-to-one by Lm7;
     consider l such that
A3:  dom (i Shift p) c= Seg l by FINSEQ_1:def 12;
A4:  rng fs = rng Sgm dom (i Shift p) by A2,FINSEQ_1:71;
       rng Sgm dom (i Shift p) c= NAT by FINSEQ_1:def 4;
     then reconsider fs as FinSequence of NAT by A4,FINSEQ_1:def 4;
       for n,m,k1,k2 being Nat st (1 <= n & n < m & m <= len fs &
        k1 = fs.n & k2 = fs.m) holds k1 < k2
      proof let n,m,k1,k2 be Nat; assume
A5:     1 <= n & n < m & m <= len fs & k1 = fs.n & k2 = fs.m;
A6:     dom fs = Seg len fs by FINSEQ_1:def 3
              .= {n1 where n1 is Nat: 1 <= n1 & n1 <= len fs}
                    by FINSEQ_1:def 1;
          n+1 <= m by A5,INT_1:20;
        then n+1 <= len fs by A5,AXIOMS:22;
then A7:     n <= (len fs) - 1 by REAL_1:84;
          (len fs) + 0 <= (len fs) + 1 & n+0 <= n+1 by REAL_1:55;
        then (len fs) - 1 <= len fs by REAL_1:86;
        then n <= len fs by A7,AXIOMS:22;
then A8:     n in dom p by A2,A5,A6;
          1 <= m by A5,AXIOMS:22;
then m in dom p by A2,A5,A6;
then k1 = i+n & k2 = i+m by A2,A5,A8;
        hence thesis by A5,REAL_1:67;
      end;
     then fs = Sgm dom (i Shift p) by A2,A3,FINSEQ_1:def 13;
     hence thesis by A1,A2;
   end;

theorem Th60:
 for p being FinSequence st k in dom p holds (Seq (i Shift p)).k = p.k
  proof
    let p be FinSequence; assume
A1: k in dom p;
then A2: k in dom Seq (i Shift p) by Th58;
A3: Seq (i Shift p) = (i Shift p)*(Sgm dom (i Shift p))
       by FINSEQ_1:def 14;
A4: (Seq (i Shift p)).k = ((i Shift p)*(Sgm dom (i Shift p))).k by FINSEQ_1:def
14;
      ((i Shift p)*(Sgm dom (i Shift p))).k
                = (i Shift p).((Sgm dom (i Shift p)).k) by A2,A3,FUNCT_1:22
               .= (i Shift p).(i+k) by A1,Th59;
    hence thesis by A1,A4,Def15;
  end;

theorem Th61:
  for p being FinSequence holds Seq (i Shift p) = p
   proof let p be FinSequence;
A1:  dom Seq (i Shift p) = dom p by Th58;
       x in dom p implies (Seq (i Shift p)).x = p.x by Th60;
     hence thesis by A1,FUNCT_1:9;
   end;

reserve p1,p2 for FinSequence;

theorem Th62:
 dom (p1 \/ ((len p1) Shift p2)) = Seg (len p1 + len p2)
  proof
    per cases;
    suppose A1: p1 = {} & p2 = {};
then A2:  dom (p1 \/ ((len p1) Shift p2)) = dom p1 by Th55;
       len p2 = 0 by A1,FINSEQ_1:25;
     hence thesis by A2,FINSEQ_1:def 3;

    suppose A3: p1 <> {} & p2 = {};
     then A4: (len p1) Shift p2 = {} by Th55;
       len p2 = 0 by A3,FINSEQ_1:25;
     hence thesis by A4,FINSEQ_1:def 3;

    suppose A5: p1 = {} & p2 <> {};
     then dom (p1 \/ ((len p1) Shift p2)) = dom (0 Shift p2) by FINSEQ_1:25
                                    .= dom p2 by Th52
                                    .= Seg (0+len p2) by FINSEQ_1:def 3
                                    .= Seg (len p1 + len p2) by A5,FINSEQ_1:25;
     hence thesis;
    suppose A6: p1 <> {} & p2 <> {};
A7:    Seg (len p1 + len p2) = {j: 1 <= j & j <= len p1 + len p2}
         by FINSEQ_1:def 1;
A8:   dom (p1 \/ ((len p1) Shift p2)) = dom p1 \/ dom ((len p1) Shift p2)
         by RELAT_1:13;
A9:   dom p1 = Seg len p1 by FINSEQ_1:def 3
            .= {k: 1 <= k & k <= len p1} by FINSEQ_1:def 1;
A10:   dom ((len p1) Shift p2) = {k1: len p1 + 1 <= k1 & k1 <= len p1 + len p2}
         by A6,Th54;
      thus dom (p1 \/ ((len p1) Shift p2)) c= Seg (len p1 + len p2)
       proof let x; assume x in dom (p1 \/ ((len p1) Shift p2));
         then x in dom p1 or x in dom ((len p1) Shift p2) by A8,XBOOLE_0:def 2
;
         then consider k3 being Nat such that
A11:      x = k3 & 1 <= k3 & k3 <= len p1 or
         x = k3 & len p1 + 1 <= k3 & k3 <= len p1 + len p2 by A9,A10;
         reconsider x as Nat by A11;
           1 <= x & x <= len p1 + len p2 by A11,Lm2;
         hence thesis by A7;
       end; let x; assume
        x in Seg (len p1 + len p2);
      then consider j such that
A12:   x = j & 1 <= j & j <= len p1 + len p2 by A7;
      reconsider i0 = len p1 as Integer;
        1 <= j & j <= i0 or i0 + 1 <= j & j <= i0 + len p2
         by A12,INT_1:20;
      then x in dom p1 or x in dom ((len p1) Shift p2) by A9,A10,A12;
      hence thesis by A8,XBOOLE_0:def 2;
  end;

theorem Th63:
 for p1 being FinSequence, p2 being FinSubsequence st len p1 <= i holds
    dom p1 misses dom (i Shift p2)
  proof let p1 be FinSequence, p2 be FinSubsequence; assume
A1:  len p1 <= i;
A2:  dom p1 = Seg len p1 by FINSEQ_1:def 3
           .= {k: 1 <= k & k <= len p1} by FINSEQ_1:def 1;
A3:  dom (i Shift p2) = {i+k: k in dom p2} by Def15;
       not ex x st x in dom p1 /\ dom (i Shift p2)
      proof given x such that
A4:     x in dom p1 /\ dom (i Shift p2);
A5:     x in dom p1 & x in dom (i Shift p2) by A4,XBOOLE_0:def 3;
        then consider k1 such that
A6:     x = k1 & 1 <= k1 & k1 <= len p1 by A2;
        consider k2 such that
A7:     x = i+k2 & k2 in dom p2 by A3,A5;
        consider n being Nat such that
A8:     dom p2 c= Seg n by FINSEQ_1:def 12;
A9:     k2 in Seg n by A7,A8;
          Seg n = {m where m is Nat: 1 <= m & m <= n} by FINSEQ_1:def 1;
        then consider m being Nat such that
A10:     k2 = m & 1 <= m & m <= n by A9;
        A11: 1-1 < k2-0 by A10,REAL_1:92;
        reconsider x as Nat by A6;
          len p1 + k2 <= i+k2 by A1,REAL_1:55;
        then (len p1 + k2) - k2 < x - 0 by A7,A11,REAL_1:92;
        hence contradiction by A6,XCMPLX_1:26;
      end;
     hence dom p1 /\ dom (i Shift p2) = {} by XBOOLE_0:def 1;
  end;

theorem Th64:
  for p1,p2 being FinSequence holds p1^p2 = p1 \/ ((len p1) Shift p2)
   proof let p1,p2;
       p1 \/ ((len p1) Shift p2) is FinSequence
      proof
A1:     dom (p1 \/ ((len p1) Shift p2)) = Seg (len p1 + len p2) by Th62;
          dom p1 misses dom ((len p1) Shift p2) by Th63;
        hence thesis by A1,FINSEQ_1:def 2,GRFUNC_1:31;
      end;
     then reconsider p = p1 \/ ((len p1) Shift p2) as FinSequence;
A2:  dom p = Seg (len p1 + len p2) by Th62;
A3:  for k st k in dom p1 holds p.k = p1.k
      proof let k; assume k in dom p1;
        then [k,p1.k] in p1 by FUNCT_1:def 4;
        then [k,p1.k] in p by XBOOLE_0:def 2;
        hence p1.k = p.k by FUNCT_1:8;
      end;
       for k st k in dom p2 holds p.(len p1 + k) = p2.k
      proof let k; assume
A4:      k in dom p2;
A5:     dom ((len p1) Shift p2) = {len p1 + j: j in dom p2} by Def15;
      p.(len p1 + k) = ((len p1) Shift p2).(len p1 + k)
         proof
             len p1 + k in dom ((len p1) Shift p2) by A4,A5;
           then [len p1 + k, ((len p1) Shift p2).(len p1 + k)] in
              ((len p1) Shift p2) by FUNCT_1:def 4;
           then [len p1 + k, ((len p1) Shift p2).(len p1 + k)] in p
              by XBOOLE_0:def 2;
           hence thesis by FUNCT_1:8;
         end;
        hence thesis by A4,Def15;
      end;
     hence thesis by A2,A3,FINSEQ_1:def 7;
   end;

theorem Th65:
  for p1 being FinSequence, p2 being FinSubsequence st i >= len p1
   holds p1 misses i Shift p2
   proof
     let p1 be FinSequence, p2 be FinSubsequence;
     assume i >= len p1;
     then dom p1 misses dom (i Shift p2) by Th63;
     hence thesis by Th8;
   end;

theorem
    (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
   proof
A1:  (R1 concur R2) concur R3
        = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
              Seq q1 in R1 concur R2 & Seq q2 in R3} by Def14;
A2:  R1 concur (R2 concur R3)
        = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
              Seq q1 in R1 & Seq q2 in R2 concur R3} by Def14;
A3:  R1 concur R2 = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
                        Seq q1 in R1 & Seq q2 in R2} by Def14;
A4:  R2 concur R3 = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
                        Seq q1 in R2 & Seq q2 in R3} by Def14;
     thus (R1 concur R2) concur R3 c= R1 concur (R2 concur R3)
      proof
        let x; assume x in (R1 concur R2) concur R3;
        then consider C1 such that
A5:     x = C1 & ex q1,q2 st C1 = q1 \/ q2 & q1 misses q2 &
                 Seq q1 in R1 concur R2 & Seq q2 in R3 by A1;
        consider q1,q2 such that
A6:     C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 concur R2 &
        Seq q2 in R3 by A5;
        consider C2 such that
A7:     Seq q1 = C2 & ex q3,q4 st C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R1 &
                      Seq q4 in R2 by A3,A6;
        consider q3,q4 such that
A8:     C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R1 & Seq q4 in R2 by A7;
        consider n1 being Nat such that
A9:     dom q1 c= Seg n1 by FINSEQ_1:def 12;
A10:    q3 c= Seq q1 & q4 c= Seq q1 by A7,A8,XBOOLE_1:7;
then A11:     dom q3 misses dom q4 by A8,Th10;
          Sgm dom q1 is one-to-one by A9,FINSEQ_3:99;
then A12:     (Sgm dom q1).:dom q3 misses (Sgm dom q1).:dom q4 by A11,FUNCT_1:
125;
A13:     rng ((Sgm dom q1)|dom q3) = (Sgm dom q1).:dom q3 &
           rng ((Sgm dom q1)|dom q4) = (Sgm dom q1).:dom q4
              by RELAT_1:148;
then A14:     q1|rng((Sgm dom q1)|dom q3) misses q1|rng((Sgm dom q1)|dom q4)
           by A12,Th9;
A15:     dom Sgm dom q1 = dom (q3 \/ q4) by A7,A8,Lm4
                      .= dom q3 \/ dom q4 by RELAT_1:13;
A16:     q1|rng((Sgm dom q1)|dom q3) \/ q1|rng((Sgm dom q1)|dom q4)
           = q1|(rng((Sgm dom q1)|dom q3) \/ rng((Sgm dom q1)|dom q4))
                by RELAT_1:107
          .= q1|((Sgm dom q1).:(dom q3 \/ dom q4)) by A13,RELAT_1:153
          .= q1|rng((Sgm dom q1)|(dom Sgm dom q1)) by A15,RELAT_1:148
          .= q1|rng Sgm dom q1 by RELAT_1:98
          .= q1|dom q1 by FINSEQ_1:71
          .= q1 by RELAT_1:98;
A17:     dom (q1|rng((Sgm dom q1)|dom q3)) c= rng((Sgm dom q1)|dom q3) &
           dom (q1|rng((Sgm dom q1)|dom q4)) c= rng((Sgm dom q1)|dom q4)
              by RELAT_1:87;
          rng((Sgm dom q1)|dom q3) c= rng Sgm dom q1 &
           rng((Sgm dom q1)|dom q4) c= rng Sgm dom q1 by RELAT_1:99;
        then rng((Sgm dom q1)|dom q3) c= dom q1 & rng((Sgm dom q1)|dom q4) c=
dom q1
           by FINSEQ_1:71;
        then dom (q1|rng((Sgm dom q1)|dom q3)) c= dom q1 &
           dom (q1|rng((Sgm dom q1)|dom q4)) c= dom q1 by A17,XBOOLE_1:1;
then A18:     dom (q1|rng((Sgm dom q1)|dom q3)) c= Seg n1 &
           dom (q1|rng((Sgm dom q1)|dom q4)) c= Seg n1 by A9,XBOOLE_1:1;
A19:     q1 c= C1 by A6,XBOOLE_1:7;
          q1|rng((Sgm dom q1)|dom q3) c= q1 by A16,XBOOLE_1:7;
then A20:     q1|rng((Sgm dom q1)|dom q3) c= C1 by A19,XBOOLE_1:1;
          q1|rng((Sgm dom q1)|dom q4) c= q1 by A16,XBOOLE_1:7;
then A21:     q1|rng((Sgm dom q1)|dom q4) c= C1 by A19,XBOOLE_1:1;
          rng C1 = rng q1 \/ rng q2 by A6,RELAT_1:26;
then A22:     rng q1 c= rng C1 by XBOOLE_1:7;
        A23: rng q1 = rng Seq q1 by Lm5;
A24:     rng Seq q1 c= rng C1 by A22,Lm5;
A25:     rng Seq q1 = rng q3 \/ rng q4 by A7,A8,RELAT_1:26;
then A26:     rng q3 c= rng Seq q1 by XBOOLE_1:7;
          rng q3 = rng Seq q3 by Lm5;
then A27:     rng Seq q3 c= rng C1 by A24,A26,XBOOLE_1:1;
A28:     rng q4 c= rng Seq q1 by A25,XBOOLE_1:7;
          rng q4 = rng Seq q4 by Lm5;
then A29:     rng Seq q4 c= rng C1 by A24,A28,XBOOLE_1:1;
        reconsider q5 = q1|rng((Sgm dom q1)|dom q3),
         q6 = q1|rng((Sgm dom q1)|dom q4) as FinSubsequence
            by A18,FINSEQ_1:def 12;
        reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def 4;
        reconsider fs1 = Seq q1 as FinSequence of rng C1 by A22,A23,FINSEQ_1:
def 4;
        reconsider fs2 = Seq q3 as FinSequence of rng C1 by A27,FINSEQ_1:def 4;
        reconsider fs3 = Seq q4 as FinSequence of rng C1 by A29,FINSEQ_1:def 4;
        reconsider fss = q1, fss1 = q5, fss2 = q6 as FinSubsequence of fs
           by A19,A20,A21,GRAPH_2:def 5;
        reconsider fss3 = q3, fss4 = q4 as FinSubsequence of fs1
           by A10,GRAPH_2:def 5;
          Seq fss = fs1 & Seq fss3 = fs2 &
           fss1 = fss|rng((Sgm dom fss)|dom fss3);
then A30:     Seq q3 = Seq q5 by GRAPH_2:30;
          Seq fss = fs1 & Seq fss4 = fs3 &
           fss2 = fss|rng((Sgm dom fss)|dom fss4);
then A31:     Seq q4 = Seq q6 by GRAPH_2:30;
          q1 /\ q2 = {} by A6,XBOOLE_0:def 7;
        then q5 /\ q2 \/ q6 /\ q2 = {} by A16,XBOOLE_1:23;
then A32:     q5 /\ q2 = {} & q6 /\ q2 = {} by XBOOLE_1:15;
then A33:     q6 misses q2 by XBOOLE_0:def 7;
A34:     q1 c= C1 & q2 c= C1 by A6,XBOOLE_1:7;
          q6 c= q1 by A16,XBOOLE_1:7;
        then q6 c= C1 by A34,XBOOLE_1:1;
then A35:    dom q6 misses dom q2 by A33,A34,Th10;
        then reconsider q7 = q6 \/ q2 as Function by GRFUNC_1:31;
          dom C1 = dom q1 \/ dom q2 by A6,RELAT_1:13
              .= (dom q5 \/ dom q6) \/ dom q2 by A16,RELAT_1:13
              .= dom q5 \/ (dom q6 \/ dom q2) by XBOOLE_1:4
              .= dom q5 \/ dom q7 by RELAT_1:13;
then A36:     dom q7 c= dom C1 by XBOOLE_1:7;
        A37: dom C1 = Seg len C1 by FINSEQ_1:def 3;
        then reconsider q7 as FinSubsequence by A36,FINSEQ_1:def 12;
A38:     C1 = q5 \/ q7 by A6,A16,XBOOLE_1:4;
A39:     q5 /\ q7 = q5 /\ q6 \/ q5 /\ q2 by XBOOLE_1:23;
          q5 /\ q6 = {} by A14,XBOOLE_0:def 7;
then A40:     q5 misses q7 by A32,A39,XBOOLE_0:def 7;
A41:     rng Seq q7 = rng q7 by Lm5;
          rng C1 = rng q7 \/ rng q5 by A38,RELAT_1:26;
then A42:     rng Seq q7 c= rng C1 by A41,XBOOLE_1:7;
          rng C1 c= N by FINSEQ_1:def 4;
        then rng Seq q7 c= N by A42,XBOOLE_1:1;
        then Seq q7 is FinSequence of N by FINSEQ_1:def 4;
        then reconsider C3 = Seq q7 as firing-sequence of N by FINSEQ_1:def 11;
A43:     dom Seq q7 = Seg len Seq q7 by FINSEQ_1:def 3;
          dom (q6*Sgm dom q7) c= dom Sgm dom q7 &
           dom (q2*Sgm dom q7) c= dom Sgm dom q7 by RELAT_1:44;
        then dom (q6*Sgm dom q7) c= dom Seq q7 & dom (q2*Sgm dom q7) c= dom
Seq q7
           by Lm4;
        then reconsider q8 = q6*Sgm dom q7, q9 = q2*Sgm dom q7 as
FinSubsequence
           by A43,FINSEQ_1:def 12;
          ex ss1,ss2 being FinSubsequence st C3 = ss1 \/ ss2 & ss1 misses ss2 &
           Seq ss1 in R2 & Seq ss2 in R3
         proof
A44:        C3 = q7*Sgm dom q7 by FINSEQ_1:def 14
             .= q8 \/ q9 by RELAT_1:51;
A45:        dom q8 = (Sgm dom q7)"dom q6 by RELAT_1:182;
A46:        dom q9 = (Sgm dom q7)"dom q2 by RELAT_1:182;
             dom q2 /\ dom q6 = {} by A35,XBOOLE_0:def 7;
           then (Sgm dom q7)"(dom q6 /\ dom q2) = {} by RELAT_1:171;
           then (Sgm dom q7)"dom q6 /\ (Sgm dom q7)"dom q2 = {} by FUNCT_1:137
;
           then (Sgm dom q7)"dom q6 misses (Sgm dom q7)"dom q2
              by XBOOLE_0:def 7;
then A47:        q8 misses q9 by A45,A46,Th8;
             dom q6 c= dom q6 \/ dom q2 & dom q2 c= dom q6 \/ dom q2
              by XBOOLE_1:7;
           then dom q6 c= dom q7 & dom q2 c= dom q7 by RELAT_1:13;
then A48:        dom q6 c= rng Sgm dom q7 & dom q2 c= rng Sgm dom q7 by
FINSEQ_1:71;
A49:        dom q8 = (Sgm dom q7)"dom q6 &
              dom q9 = (Sgm dom q7)"dom q2 by RELAT_1:182;
then A50:        rng ((Sgm dom q7)|dom q8) = rng ((dom q6)|(Sgm dom q7)) by
Th12
                                    .= dom q6 by A48,RELAT_1:120;
A51:        dom q8 c= dom Sgm dom q7 & dom q9 c= dom Sgm dom q7
              by RELAT_1:44;
then A52:        (Sgm dom q7)*(Sgm dom q8) = Sgm rng ((Sgm dom q7)|dom q8)
                                          by A36,A37,GRAPH_2:3;
           A53: Seq q8 = (q6*Sgm dom q7)*(Sgm dom q8) by FINSEQ_1:def 14
                 .= q6*((Sgm dom q7)*(Sgm dom q8)) by RELAT_1:55
                 .= Seq q6 by A50,A52,FINSEQ_1:def 14;
A54:        rng ((Sgm dom q7)|dom q9) = rng ((dom q2)|(Sgm dom q7)) by A49,Th12
                                    .= dom q2 by A48,RELAT_1:120;
A55:        (Sgm dom q7)*(Sgm dom q9) = Sgm rng ((Sgm dom q7)|dom q9)
                                          by A36,A37,A51,GRAPH_2:3;
             Seq q9 = (q2*Sgm dom q7)*(Sgm dom q9) by FINSEQ_1:def 14
                 .= q2*((Sgm dom q7)*(Sgm dom q9)) by RELAT_1:55
                 .= Seq q2 by A54,A55,FINSEQ_1:def 14;
           hence thesis by A6,A8,A31,A44,A47,A53;
         end;
then Seq q7 in R2 concur R3 by A4;
        hence thesis by A2,A5,A8,A30,A38,A40;
      end;
     let x; assume x in R1 concur (R2 concur R3);
     then consider C1 such that
A56:  x = C1 & ex q1,q2 st C1 = q1 \/ q2 & q1 misses q2 &
              Seq q1 in R1 & Seq q2 in R2 concur R3 by A2;
     consider q1,q2 such that
A57:  C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 &
     Seq q2 in R2 concur R3 by A56;
     consider C2 such that
A58:  Seq q2 = C2 & ex q3,q4 st C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 &
                   Seq q4 in R3 by A4,A57;
     consider q3,q4 such that
A59:  C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 by A58;
     consider n1 being Nat such that
A60:  dom q2 c= Seg n1 by FINSEQ_1:def 12;
A61: q3 c= Seq q2 & q4 c= Seq q2 by A58,A59,XBOOLE_1:7;
then A62:  dom q3 misses dom q4 by A59,Th10;
       Sgm dom q2 is one-to-one by A60,FINSEQ_3:99;
then A63:  (Sgm dom q2).:dom q3 misses (Sgm dom q2).:dom q4 by A62,FUNCT_1:125;
A64:  rng ((Sgm dom q2)|dom q3) = (Sgm dom q2).:dom q3 &
        rng ((Sgm dom q2)|dom q4) = (Sgm dom q2).:dom q4 by RELAT_1:148;
then A65:  q2|rng((Sgm dom q2)|dom q3) misses q2|rng((Sgm dom q2)|dom q4)
        by A63,Th9;
A66:  dom Sgm dom q2 = dom Seq q2 by Lm4
                   .= dom q3 \/ dom q4 by A58,A59,RELAT_1:13;
A67:  q2|rng((Sgm dom q2)|dom q3) \/ q2|rng((Sgm dom q2)|dom q4)
        = q2|(rng((Sgm dom q2)|dom q3) \/ rng ((Sgm dom q2)|dom q4))
             by RELAT_1:107
       .= q2|((Sgm dom q2).:(dom q3 \/ dom q4)) by A64,RELAT_1:153
       .= q2|rng((Sgm dom q2)|(dom Sgm dom q2)) by A66,RELAT_1:148
       .= q2|rng Sgm dom q2 by RELAT_1:98
       .= q2|dom q2 by FINSEQ_1:71
       .= q2 by RELAT_1:98;
A68:  dom (q2|rng((Sgm dom q2)|dom q3)) c= rng((Sgm dom q2)|dom q3) &
        dom (q2|rng((Sgm dom q2)|dom q4)) c= rng ((Sgm dom q2)|dom q4)
           by RELAT_1:87;
       rng((Sgm dom q2)|dom q3) c= rng Sgm dom q2 &
        rng((Sgm dom q2)|dom q4) c= rng Sgm dom q2 by RELAT_1:99;
     then rng((Sgm dom q2)|dom q3) c= dom q2 & rng((Sgm dom q2)|dom q4) c= dom
q2
        by FINSEQ_1:71;
     then dom (q2|rng((Sgm dom q2)|dom q3)) c= dom q2 &
        dom (q2|rng((Sgm dom q2)|dom q4)) c= dom q2 by A68,XBOOLE_1:1;
then A69:  dom (q2|rng((Sgm dom q2)|dom q3)) c= Seg n1 &
        dom (q2|rng((Sgm dom q2)|dom q4)) c= Seg n1 by A60,XBOOLE_1:1;
A70:  q2 c= C1 by A57,XBOOLE_1:7;
       q2|rng((Sgm dom q2)|dom q3) c= q2 by A67,XBOOLE_1:7;
then A71:  q2|rng((Sgm dom q2)|dom q3) c= C1 by A70,XBOOLE_1:1;
       q2|rng((Sgm dom q2)|dom q4) c= q2 by A67,XBOOLE_1:7;
then A72:  q2|rng((Sgm dom q2)|dom q4) c= C1 by A70,XBOOLE_1:1;
       rng C1 = rng q1 \/ rng q2 by A57,RELAT_1:26;
then A73:  rng q2 c= rng C1 by XBOOLE_1:7;
     A74: rng q2 = rng Seq q2 by Lm5;
A75:  rng Seq q2 c= rng C1 by A73,Lm5;
A76:  rng Seq q2 = rng q3 \/ rng q4 by A58,A59,RELAT_1:26;
then A77:  rng q3 c= rng Seq q2 by XBOOLE_1:7;
       rng q3 = rng Seq q3 by Lm5;
then A78:  rng Seq q3 c= rng C1 by A75,A77,XBOOLE_1:1;
A79:  rng q4 c= rng Seq q2 by A76,XBOOLE_1:7;
       rng q4 = rng Seq q4 by Lm5;
then A80:  rng Seq q4 c= rng C1 by A75,A79,XBOOLE_1:1;
     reconsider q5 = q2|rng((Sgm dom q2)|dom q3),
      q6 = q2|rng((Sgm dom q2)|dom q4) as FinSubsequence by A69,FINSEQ_1:def 12
;
     reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def 4;
     reconsider fs1 = Seq q2 as FinSequence of rng C1 by A73,A74,FINSEQ_1:def 4
;
     reconsider fs2 = Seq q3 as FinSequence of rng C1 by A78,FINSEQ_1:def 4;
     reconsider fs3 = Seq q4 as FinSequence of rng C1 by A80,FINSEQ_1:def 4;
     reconsider fss = q2, fss1 = q5, fss2 = q6 as FinSubsequence of fs
        by A70,A71,A72,GRAPH_2:def 5;
     reconsider fss3 = q3, fss4 = q4 as FinSubsequence of fs1
        by A61,GRAPH_2:def 5;
       Seq fss = fs1 & Seq fss3 = fs2 & fss1 = fss|rng((Sgm dom fss)|dom fss3);
then A81:  Seq q5 in R2 by A59,GRAPH_2:30;
       Seq fss = fs1 & Seq fss4 = fs3 & fss2 = fss|rng((Sgm dom fss)|dom fss4);
then A82:  Seq q4 = Seq q6 by GRAPH_2:30;
       q1 /\ q2 = {} by A57,XBOOLE_0:def 7;
     then q1 /\ q5 \/ q1 /\ q6 = {} by A67,XBOOLE_1:23;
then A83:  q1 /\ q5 = {} & q1 /\ q6 = {} by XBOOLE_1:15;
then A84:  q1 misses q5 by XBOOLE_0:def 7;
A85:  q1 c= C1 & q2 c= C1 by A57,XBOOLE_1:7;
       q5 c= q2 by A67,XBOOLE_1:7;
     then q5 c= C1 by A85,XBOOLE_1:1;
then A86: dom q1 misses dom q5 by A84,A85,Th10;
     then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:31;
       dom C1 = dom q1 \/ dom q2 by A57,RELAT_1:13
           .= dom q1 \/ (dom q5 \/ dom q6) by A67,RELAT_1:13
           .= (dom q1 \/ dom q5) \/ dom q6 by XBOOLE_1:4
           .= dom q7 \/ dom q6 by RELAT_1:13;
then A87:  dom q7 c= dom C1 by XBOOLE_1:7;
     A88: dom C1 = Seg len C1 by FINSEQ_1:def 3;
     then reconsider q7 as FinSubsequence by A87,FINSEQ_1:def 12;
A89:  C1 = q7 \/ q6 by A57,A67,XBOOLE_1:4;
A90:  q7 /\ q6 = q1 /\ q6 \/ q5 /\ q6 by XBOOLE_1:23;
       q5 /\ q6 = {} by A65,XBOOLE_0:def 7;
then A91:  q7 misses q6 by A83,A90,XBOOLE_0:def 7;
A92:  rng Seq q7 = rng q7 by Lm5;
       rng C1 = rng q7 \/ rng q6 by A89,RELAT_1:26;
then A93:  rng Seq q7 c= rng C1 by A92,XBOOLE_1:7;
       rng C1 c= N by FINSEQ_1:def 4;
     then rng Seq q7 c= N by A93,XBOOLE_1:1;
     then Seq q7 is FinSequence of N by FINSEQ_1:def 4;
     then reconsider C3 = Seq q7 as firing-sequence of N by FINSEQ_1:def 11;
A94:  dom Seq q7 = Seg len Seq q7 by FINSEQ_1:def 3;
       dom (q1*Sgm dom q7) c= dom Sgm dom q7 &
        dom (q5*Sgm dom q7) c= dom Sgm dom q7 by RELAT_1:44;
     then dom (q1*Sgm dom q7) c= dom Seq q7 & dom (q5*Sgm dom q7) c= dom Seq
q7
        by Lm4;
        then reconsider q8 = q1*Sgm dom q7, q9 = q5*Sgm dom q7 as
FinSubsequence
           by A94,FINSEQ_1:def 12;
       ex ss1,ss2 being FinSubsequence st C3 = ss1 \/ ss2 & ss1 misses ss2 &
        Seq ss1 in R1 & Seq ss2 in R2
      proof
A95:     C3 = q7*Sgm dom q7 by FINSEQ_1:def 14
          .= q8 \/ q9 by RELAT_1:51;
A96:     dom q8 = (Sgm dom q7)"dom q1 by RELAT_1:182;
A97:     dom q9 = (Sgm dom q7)"dom q5 by RELAT_1:182;
          dom q1 /\ dom q5 = {} by A86,XBOOLE_0:def 7;
        then (Sgm dom q7)"(dom q1 /\ dom q5) = {} by RELAT_1:171;
        then (Sgm dom q7)"dom q1 /\ (Sgm dom q7)"dom q5 = {} by FUNCT_1:137;
        then (Sgm dom q7)"dom q1 misses (Sgm dom q7)"dom q5 by XBOOLE_0:def 7;
then A98:     q8 misses q9 by A96,A97,Th8;
          dom q1 c= dom q1 \/ dom q5 & dom q5 c= dom q1 \/ dom q5 by XBOOLE_1:7
;
        then dom q1 c= dom q7 & dom q5 c= dom q7 by RELAT_1:13;
then A99:     dom q1 c= rng Sgm dom q7 & dom q5 c= rng Sgm dom q7 by FINSEQ_1:
71;
A100:     dom q8 = (Sgm dom q7)"dom q1 & dom q9 = (Sgm dom q7)"dom q5
           by RELAT_1:182;
then A101:     rng ((Sgm dom q7)|dom q8) = rng ((dom q1)|(Sgm dom q7)) by Th12
                                 .= dom q1 by A99,RELAT_1:120;
A102:     dom q8 c= dom Sgm dom q7 & dom q9 c= dom Sgm dom q7 by RELAT_1:44;
then A103:     (Sgm dom q7)*(Sgm dom q8) = Sgm rng ((Sgm dom q7)|dom q8)
                                       by A87,A88,GRAPH_2:3;
        A104: Seq q8 = (q1*Sgm dom q7)*(Sgm dom q8) by FINSEQ_1:def 14
              .= q1*((Sgm dom q7)*(Sgm dom q8)) by RELAT_1:55
              .= Seq q1 by A101,A103,FINSEQ_1:def 14;
A105:     rng ((Sgm dom q7)|dom q9) = rng ((dom q5)|(Sgm dom q7)) by A100,Th12
                                 .= dom q5 by A99,RELAT_1:120;
A106:     (Sgm dom q7)*(Sgm dom q9) = Sgm rng ((Sgm dom q7)|dom q9)
                                       by A87,A88,A102,GRAPH_2:3;
          Seq q9 = (q5*Sgm dom q7)*(Sgm dom q9) by FINSEQ_1:def 14
              .= q5*((Sgm dom q7)*(Sgm dom q9)) by RELAT_1:55
              .= Seq q5 by A105,A106,FINSEQ_1:def 14;
        hence thesis by A57,A81,A95,A98,A104;
      end;
then Seq q7 in R1 concur R2 by A3;
     hence thesis by A1,A56,A59,A82,A89,A91;
   end;

theorem
    R1 before R2 c= R1 concur R2
   proof
A1:  R1 before R2 = {C1^C2: C1 in R1 & C2 in R2} by Def13;
     let x; assume
A2:  x in R1 before R2;
     then reconsider C = x as firing-sequence of N;
     consider C1,C2 such that
A3:  x = C1^C2 & C1 in R1 & C2 in R2 by A1,A2;
     set q1 = C1, q2 = (len C1) Shift C2;
     reconsider q1 as FinSequence;
       Seq q1 = q1 & Seq q2 = C2 by Th61,GRAPH_2:24;
     then C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2
        by A3,Th64,Th65;
     then x in {a where a is firing-sequence of N: ex q1,q2 being
FinSubsequence
           st a = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2};
     hence x in R1 concur R2 by Def14;
   end;

theorem
    R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2
   proof assume
A1:  R1 c= P1 & R2 c= P2;
A2:  R1 before R2 = {C1^C2: C1 in R1 & C2 in R2} by Def13;
A3:  P1 before P2 = {fs1^fs2: fs1 in P1 & fs2 in P2} by Def13;
     let x;
     assume x in R1 before R2;
     then consider C1,C2 such that
A4:  x = C1^C2 & C1 in R1 & C2 in R2 by A2;
     thus x in P1 before P2 by A1,A3,A4;
   end;

theorem
    R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2
   proof assume
A1:  R1 c= P1 & R2 c= P2;
A2:  R1 concur R2 = {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 &
                        q1 misses q2 & Seq q1 in R1 & Seq q2 in R2} by Def14;
A3:  P1 concur P2 = {fs: ex q3,q4 being FinSubsequence st fs = q3 \/ q4 &
                         q3 misses q4 & Seq q3 in P1 & Seq q4 in P2} by Def14;
     let x;
     assume x in R1 concur R2;
     then ex C st
      x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
     Seq q1 in R1 & Seq q2 in R2 by A2;
     hence x in P1 concur P2 by A1,A3;
   end;

Lm8:
  for p1,p2 being FinSequence, q1,q2 being FinSubsequence st
     q1 c= p1 & q2 c= p2 holds
        dom (q1 \/ len p1 Shift q2) c= dom (p1^p2)
   proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume
       q1 c= p1 & q2 c= p2;
then A1:  dom q1 c= dom p1 & dom q2 c= dom p2 by GRFUNC_1:8;
     let x; assume x in dom (q1 \/ len p1 Shift q2);
     then A2: x in (dom q1 \/ dom (len p1 Shift q2)) by RELAT_1:13;
A3:  dom (p1^p2) = Seg (len p1 + len p2) by FINSEQ_1:def 7;
A4:  now assume
A5:    x in dom q1;
A6:    dom p1 = Seg len p1 by FINSEQ_1:def 3;
         len p1 <= len p1 + len p2 by INT_1:19;
       then Seg len p1 c= Seg (len p1 + len p2) by FINSEQ_1:7;
       hence x in dom (p1^p2) by A1,A3,A5,A6,TARSKI:def 3;
     end;
       now assume
A7:    x in dom (len p1 Shift q2);
A8:    dom (len p1 Shift q2) c= dom (len p1 Shift p2)
        proof let x; assume
A9:       x in dom (len p1 Shift q2);
A10:       dom (len p1 Shift p2) = {len p1 + k: k in dom p2} by Def15;
            dom (len p1 Shift q2) = {len p1 + k: k in dom q2} by Def15;
          then consider k such that
A11:       x = len p1 + k & k in dom q2 by A9;
          thus thesis by A1,A10,A11;
        end;
         dom (p1^p2) = dom (p1 \/ len p1 Shift p2) by Th64
                  .= dom p1 \/ dom (len p1 Shift p2) by RELAT_1:13;
       then dom (len p1 Shift p2) c= dom (p1^p2) by XBOOLE_1:7;
       then dom (len p1 Shift q2) c= dom (p1^p2) by A8,XBOOLE_1:1;
       hence x in dom (p1^p2) by A7;
     end;
     hence thesis by A2,A4,XBOOLE_0:def 2;
   end;

Lm9:
  for p1 being FinSequence, q1,q2 being FinSubsequence st
     q1 c= p1 holds q1 misses ((len p1) Shift q2)
   proof let p1 be FinSequence, q1,q2 be FinSubsequence; assume
A1:  q1 c= p1;
       p1 misses ((len p1) Shift q2) by Th65;
     hence thesis by A1,XBOOLE_1:63;
   end;

Lm10:
  for p,q being FinSubsequence st q c= p holds
     dom (i Shift q) c= dom (i Shift p)
   proof let p,q be FinSubsequence; assume
A1:  q c= p;
A2:  dom (i Shift q) = {i+k: k in dom q} by Def15;
A3:  dom (i Shift p) = {i+k: k in dom p} by Def15;
A4:  dom q c= dom p by A1,GRFUNC_1:8;
     let x; assume x in dom (i Shift q);
     then consider k1 such that
A5:  x = i+k1 & k1 in dom q by A2;
     thus thesis by A3,A4,A5;
   end;

theorem Th70:
  for p,q being FinSubsequence st q c= p holds
     i Shift q c= i Shift p
   proof let p,q be FinSubsequence; assume
A1:  q c= p;
A2:  dom (i Shift q) = {i+k: k in dom q} by Def15;
A3:  dom (i Shift p) = {i+k: k in dom p} by Def15;
     let x,y; assume [x,y] in i Shift q;
then A4:  x in dom (i Shift q) & y = (i Shift q).x by FUNCT_1:8;
     then consider k such that
A5:  x = i+k & k in dom q by A2;
     A6: dom q c= dom p by A1,GRFUNC_1:8;
then A7:  x in dom (i Shift p) by A3,A5;
       y = q.k by A4,A5,Def15
      .= p.k by A1,A5,GRFUNC_1:8
      .= (i Shift p).x by A5,A6,Def15;
     hence [x,y] in i Shift p by A7,FUNCT_1:8;
   end;

theorem Th71:
  for p1,p2 being FinSequence holds len p1 Shift p2 c= p1^p2
   proof let p1,p2 be FinSequence;
     per cases;
    suppose p2 = {};
     then len p1 Shift p2 = {} by Th55;
     hence thesis by XBOOLE_1:2;
    suppose A1: p2 <> {};
A2:   dom (len p1 Shift p2) = {len p1 + k: k in dom p2} by Def15;
A3:  dom (len p1 Shift p2) = {k: len p1 + 1 <= k & k <= len p1 + len p2}
        by A1,Th54;
A4:  dom (p1^p2) = Seg (len p1 + len p2) by FINSEQ_1:def 7
                .= {k: 1 <= k & k <= len p1 + len p2} by FINSEQ_1:def 1;
     let x,y; assume [x,y] in len p1 Shift p2;
then A5:  x in dom (len p1 Shift p2) & y = (len p1 Shift p2).x by FUNCT_1:8;
     then consider k such that
A6:  x = k & len p1 + 1 <= k & k <= len p1 + len p2 by A3;
       1 <= len p1 + 1 by INT_1:19;
     then 1 <= k by A6,AXIOMS:22;
then A7:  x in dom (p1^p2) by A4,A6;
     consider j such that
A8:  x = len p1 + j & j in dom p2 by A2,A5;
       y = p2.j by A5,A8,Def15
      .= (p1^p2).x by A8,FINSEQ_1:def 7;
     hence [x,y] in p1^p2 by A7,FUNCT_1:8;
   end;

theorem Th72:
  dom q1 misses dom q2 implies dom (i Shift q1) misses dom (i Shift q2)
   proof assume A1: dom q1 misses dom q2;
A2:  dom (i Shift q1) = {i+k: k in dom q1} by Def15;
A3:  dom (i Shift q2) = {i+k: k in dom q2} by Def15;
       now given x such that
A4:    x in dom (i Shift q1) /\ dom (i Shift q2);
A5:    x in dom (i Shift q1) & x in dom (i Shift q2) by A4,XBOOLE_0:def 3;
       then consider k1 such that
A6:    x = i+k1 & k1 in dom q1 by A2;
       consider k2 such that
A7:    x = i+k2 & k2 in dom q2 by A3,A5;
         k1 = k2 by A6,A7,XCMPLX_1:2;
       then k2 in dom q1 /\ dom q2 by A6,A7,XBOOLE_0:def 3;
       hence contradiction by A1,XBOOLE_0:def 7;
     end;
     hence dom (i Shift q1) /\ dom (i Shift q2) = {} by XBOOLE_0:def 1;
   end;

theorem Th73:
  for q,q1,q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
     (i Shift q1) \/ (i Shift q2) = i Shift q
   proof let q,q1,q2 be FinSubsequence such that
A1:  q = q1 \/ q2 and
A2:  q1 misses q2;
A3:  dom (i Shift q) = {i+k: k in dom q} by Def15;
A4:  dom (i Shift q1) = {i+k: k in dom q1} by Def15;
A5:  dom (i Shift q2) = {i+k: k in dom q2} by Def15;
A6:  q1 c= q & q2 c= q by A1,XBOOLE_1:7;
then A7:  (i Shift q1) c= (i Shift q) & (i Shift q2) c= (i Shift q) by Th70;
       dom q1 misses dom q2 by A2,A6,Th10;
     then dom (i Shift q1) misses dom (i Shift q2) by Th72;
     then reconsider q3 = (i Shift q1) \/ (i Shift q2) as Function by GRFUNC_1:
31;
     let x,y;
     thus [x,y] in (i Shift q1) \/ (i Shift q2) implies [x,y] in i Shift q
      proof assume
A8:      [x,y] in (i Shift q1) \/ (i Shift q2);
        then x in dom q3 & y = q3.x by FUNCT_1:8;
        then A9: x in dom (i Shift q1) \/ dom (i Shift q2) by RELAT_1:13;
A10:     now assume
A11:       x in dom (i Shift q1);
then A12:       dom (i Shift q1) c= dom (i Shift q) & (i Shift q1).x = (i Shift
q).x
             by A7,GRFUNC_1:8;
          then [x,(i Shift q).x] in (i Shift q1) by A11,FUNCT_1:def 4;
          then [x,(i Shift q).x] in q3 by XBOOLE_0:def 2;
          hence x in dom (i Shift q) & y = (i Shift q).x by A8,A11,A12,FUNCT_1:
def 1;
        end;
          now assume
A13:       x in dom (i Shift q2);
then A14:       dom (i Shift q2) c= dom (i Shift q) & (i Shift q2).x = (i Shift
q).x
             by A7,GRFUNC_1:8;
          then [x,(i Shift q).x] in (i Shift q2) by A13,FUNCT_1:def 4;
          then [x,(i Shift q).x] in q3 by XBOOLE_0:def 2;
          hence x in dom (i Shift q) & y = (i Shift q).x by A8,A13,A14,FUNCT_1:
def 1;
        end;
        hence thesis by A9,A10,FUNCT_1:8,XBOOLE_0:def 2;
      end; assume [x,y] in (i Shift q);
then A15:  x in dom (i Shift q) & y = (i Shift q).x by FUNCT_1:8;
     then consider k such that
A16:  x = i+k & k in dom q by A3;
       dom q = dom q1 \/ dom q2 by A1,RELAT_1:13;
     then A17: k in dom q1 or k in dom q2 by A16,XBOOLE_0:def 2;
     then x in dom (i Shift q1) or x in dom (i Shift q2) by A4,A5,A16;
     then x in dom (i Shift q1) \/ dom (i Shift q2) by XBOOLE_0:def 2;
then A18:  x in dom q3 by RELAT_1:13;
A19:  now assume
A20:    x in dom (i Shift q1);
       then consider k1 such that
A21:    x = i+k1 & k1 in dom q1 by A4;
       A22: k = k1 by A16,A21,XCMPLX_1:2;
       thus y = q.k by A15,A16,Def15
             .= q1.k by A1,A21,A22,GRFUNC_1:34
             .= (i Shift q1).x by A21,A22,Def15
             .= q3.x by A20,GRFUNC_1:34;
     end;
       now assume
A23:    x in dom (i Shift q2);
       then consider k2 such that
A24:    x = i+k2 & k2 in dom q2 by A5;
       A25: k = k2 by A16,A24,XCMPLX_1:2;
       thus y = q.k by A15,A16,Def15
             .= q2.k by A1,A24,A25,GRFUNC_1:34
             .= (i Shift q2).x by A24,A25,Def15
             .= q3.x by A23,GRFUNC_1:34;
     end;
     hence thesis by A4,A5,A16,A17,A18,A19,FUNCT_1:8;
   end;

theorem Th74:
  for q being FinSubsequence holds dom Seq q = dom Seq (i Shift q)
   proof let q be FinSubsequence;
A1:  Card q = Card (i Shift q) by Th57;
     A2: len Seq q = Card q & len Seq (i Shift q) = Card (i Shift q)
        by Th7;
     thus dom Seq q = Seg len Seq q by FINSEQ_1:def 3
                   .= dom Seq (i Shift q) by A1,A2,FINSEQ_1:def 3;
   end;

theorem Th75:
  for q being FinSubsequence st k in dom Seq q
     ex j st j = (Sgm dom q).k & (Sgm dom (i Shift q)).k = i + j
   proof let q be FinSubsequence such that
A1:  k in dom Seq q;
     consider ss being FinSubsequence such that
A2:  dom ss = dom q & rng ss = dom (i Shift q) &
        (for l st l in dom q holds ss.l = i+l) & ss is one-to-one by Th56;
A3:  rng Seq ss = dom (i Shift q) by A2,Lm5;
A4:  rng Sgm dom q = dom q by FINSEQ_1:71;
A5: dom Seq q = dom (q*Sgm dom q) by FINSEQ_1:def 14
              .= dom Sgm dom q by A4,RELAT_1:46;
A6:  for l1 st l1 in dom Seq q
        ex j1 st j1 = (Sgm dom q).l1 & (Seq ss).l1 = i+j1
      proof let l1 such that
A7:     l1 in dom Seq q;
A8:     (Sgm dom q).l1 in rng Sgm dom q by A5,A7,FUNCT_1:def 5;
then A9:     (Sgm dom q).l1 in dom q by FINSEQ_1:71;
          rng Sgm dom q c= NAT by FINSEQ_1:def 4;
        then reconsider j1 = (Sgm dom q).l1 as Nat by A8;
          (Seq ss).l1 = (ss*Sgm dom ss).l1 by FINSEQ_1:def 14
                   .= ss.j1 by A2,A5,A7,FUNCT_1:23
                   .= i+j1 by A2,A9;
        hence thesis;
      end;
A10:  rng ss = rng Sgm dom (i Shift q) by A2,FINSEQ_1:71;
       rng Sgm dom (i Shift q) c= NAT by FINSEQ_1:def 4;
     then rng Seq ss c= NAT by A10,Lm5;
     then reconsider fs = Seq ss as FinSequence of NAT by FINSEQ_1:def 4;
     consider l2 such that
A11:  dom (i Shift q) c= Seg l2 by FINSEQ_1:def 12;
A12: dom Seq ss = dom (ss*Sgm dom ss) by FINSEQ_1:def 14
               .= dom Sgm dom q by A2,A4,RELAT_1:46;
       for n,m,k1,k2 being Nat st (1 <= n & n < m & m <= len fs &
        k1 = fs.n & k2 = fs.m) holds k1 < k2
      proof let n,m,k1,k2 be Nat; assume
A13:     1 <= n & n < m & m <= len fs & k1 = fs.n & k2 = fs.m;
A14:     dom fs = Seg len fs by FINSEQ_1:def 3
                  .= {l3 where l3 is Nat: 1 <= l3 & l3 <= len fs}
                        by FINSEQ_1:def 1;
          n+1 <= m by A13,INT_1:20;
        then n+1 <= len fs by A13,AXIOMS:22;
then A15:     n <= (len fs) - 1 by REAL_1:84;
          (len fs) + 0 <= (len fs) + 1 & n+0 <= n+1 by REAL_1:55;
        then (len fs) - 1 <= len fs by REAL_1:86;
        then n <= len fs by A15,AXIOMS:22;
then A16:     n in dom Seq q by A5,A12,A13,A14;
          1 <= m by A13,AXIOMS:22;
then A17:     m in dom Seq q by A5,A12,A13,A14;
        consider j2 being Nat such that
A18:     j2 = (Sgm dom q).n & fs.n = i+j2 by A6,A16;
        consider j3 being Nat such that
A19:     j3 = (Sgm dom q).m & fs.m = i+j3 by A6,A17;
        consider l3 being Nat such that
A20:     dom q c= Seg l3 by FINSEQ_1:def 12;
          dom Seq ss = Seg len fs & dom Sgm dom q = Seg len Sgm dom q
           by FINSEQ_1:def 3;
        then len fs = len Sgm dom q by A12,FINSEQ_1:8;
        then j2 < j3 by A13,A18,A19,A20,FINSEQ_1:def 13;
        hence k1 < k2 by A13,A18,A19,REAL_1:67;
      end;
     then fs = Sgm dom (i Shift q) by A3,A11,FINSEQ_1:def 13;
     hence thesis by A1,A6;
   end;

theorem Th76:
  for q being FinSubsequence st
     k in dom Seq q holds (Seq (i Shift q)).k = (Seq q).k
   proof let q be FinSubsequence; assume
A1:  k in dom Seq q;
     then consider j such that
A2:  j = (Sgm dom q).k & (Sgm dom (i Shift q)).k = i+j by Th75;
A3:  rng Sgm dom q = dom q & rng Sgm dom (i Shift q) = dom (i Shift q)
        by FINSEQ_1:71;
     A4: dom Seq q = dom Seq (i Shift q) by Th74
              .= dom ((i Shift q)*(Sgm dom (i Shift q)))
                    by FINSEQ_1:def 14;
     A5: dom Seq q = dom (q*Sgm dom q) by FINSEQ_1:def 14
              .= dom Sgm dom q by A3,RELAT_1:46;
     then j in rng Sgm dom q by A1,A2,FUNCT_1:def 5;
then A6:  j in dom q by FINSEQ_1:71;
       (Seq (i Shift q)).k = ((i Shift q)*(Sgm dom (i Shift q))).k
                              by FINSEQ_1:def 14
                        .= (i Shift q).((Sgm dom (i Shift q)).k)
                              by A1,A4,FUNCT_1:22
                        .= q.j by A2,A6,Def15
                        .= (q*Sgm dom q).k by A1,A2,A5,FUNCT_1:23
                        .= (Seq q).k by FINSEQ_1:def 14;
     hence thesis;
   end;

theorem Th77:
  for q being FinSubsequence holds Seq q = Seq (i Shift q)
   proof let q be FinSubsequence;
A1:  dom Seq q = dom Seq (i Shift q) by Th74;
       x in dom Seq q implies (Seq (i Shift q)).x = (Seq q).x by Th76;
     hence thesis by A1,FUNCT_1:9;
   end;

theorem Th78:
  for q being FinSubsequence st
     dom q c= Seg k holds dom (i Shift q) c= Seg (i+k)
   proof let q be FinSubsequence; assume
A1:  dom q c= Seg k;
A2:  dom (i Shift q) = {i+j: j in dom q} by Def15;
A3:  Seg k = {j: 1 <= j & j <= k} by FINSEQ_1:def 1;
A4:  Seg (i+k) = {j: 1 <= j & j <= i+k} by FINSEQ_1:def 1;
     let x; assume x in dom (i Shift q);
     then consider j1 such that
A5:  x = i+j1 & j1 in dom q by A2;
       j1 in Seg k by A1,A5;
     then consider j2 such that
A6:  j1 = j2 & 1 <= j2 & j2 <= k by A3;
       0 <= i by NAT_1:18;
     then A7: 0+1 <= i+j1 by A6,REAL_1:55;
       i+j1 <= i+k by A6,REAL_1:55;
     hence x in Seg (i+k) by A4,A5,A7;
   end;

theorem Th79:
  for p being FinSequence, q1,q2 being FinSubsequence st q1 c= p
     ex ss being FinSubsequence st ss = q1 \/ (len p Shift q2)
   proof let p be FinSequence, q1,q2 be FinSubsequence; assume
       q1 c= p;
then A1:  dom q1 c= dom p by GRFUNC_1:8;
       dom p misses dom (len p Shift q2) by Th63;
     then dom q1 misses dom (len p Shift q2) by A1,XBOOLE_1:63;
     then reconsider ss = q1 \/ (len p Shift q2) as Function by GRFUNC_1:31;
     A2: dom p = Seg len p by FINSEQ_1:def 3;
     consider k such that
A3:  dom q2 c= Seg k by FINSEQ_1:def 12;
A4:  dom (len p Shift q2) c= Seg (len p + k) by A3,Th78;
       0 <= k by NAT_1:18;
     then len p + 0 <= len p + k by REAL_1:55;
     then Seg len p c= Seg (len p + k) by FINSEQ_1:7;
     then dom q1 c= Seg (len p + k) by A1,A2,XBOOLE_1:1;
     then dom q1 \/ dom (len p Shift q2) c= Seg (len p + k) by A4,XBOOLE_1:8;
     then dom (q1 \/ (len p Shift q2)) c= Seg (len p + k) by RELAT_1:13;
     then reconsider ss as FinSubsequence by FINSEQ_1:def 12;
     take ss;
     thus thesis;
   end;

Lm11:
  for p1,p2 being FinSequence, q1,q2 being FinSubsequence st
     q2 <> {} & q1 c= p1 & q2 c= p2 holds
        Sgm (dom q1 \/ dom (len p1 Shift q2))
           = (Sgm dom q1)^(Sgm dom (len p1 Shift q2))
   proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume
A1:  q2 <> {} & q1 c= p1 & q2 c= p2;
     consider k1 such that
A2:  dom q1 c= Seg k1 by FINSEQ_1:def 12;
     consider k2 such that
A3:  dom (len p1 Shift q2) c= Seg k2 by FINSEQ_1:def 12;
       for m,n being Nat st m in dom q1 & n in dom (len p1 Shift q2) holds m <
n
       proof let m,n be Nat such that
A4:     m in dom q1 and
A5:     n in dom (len p1 Shift q2);
A6:     dom p1 = Seg len p1 by FINSEQ_1:def 3
             .= {k: 1 <= k & k <= len p1} by FINSEQ_1:def 1;
        consider x such that
A7:     x in q2 by A1,XBOOLE_0:def 1;
A8:     dom (len p1 Shift p2) = {k: len p1 + 1 <= k & k <= len p1 + len p2}
           by A1,A7,Th54;
A9:     dom q1 c= dom p1 by A1,GRFUNC_1:8;
A10:     dom (len p1 Shift q2) c= dom (len p1 Shift p2) by A1,Lm10;
A11:     m in dom p1 by A4,A9;
A12:     n in dom (len p1 Shift p2) by A5,A10;
        consider k3 being Nat such that
A13:     k3 = m & 1 <= k3 & k3 <= len p1 by A6,A11;
        consider k4 being Nat such that
A14:     k4 = n & len p1 + 1 <= k4 & k4 <= len p1 + len p2 by A8,A12;
          len p1 < len p1 + 1 by REAL_1:69;
        then k3 <= len p1 + 1 by A13,AXIOMS:22;
then A15:     k3 <= k4 by A14,AXIOMS:22;
          dom p1 misses dom (len p1 Shift p2) by Th63;
        then k3 <> k4 by A4,A5,A9,A10,A13,A14,Lm3;
        hence m < n by A13,A14,A15,REAL_1:def 5;
      end;
      hence thesis by A2,A3,FINSEQ_3:48;
    end;

theorem Th80:
 for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
     ex ss being FinSubsequence st ss = q1 \/ (len p1 Shift q2) &
        dom Seq ss = Seg (len Seq q1 + len Seq q2)
   proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume
A1:  q1 c= p1 & q2 c= p2;
     per cases;
    suppose A2: q2 = {};
     consider ss being FinSubsequence such that
A3:  ss = q1 \/ (len p1 Shift q2) by A1,Th79;
       (len p1 Shift q2) = {} by A2,Th55;
then A4:  dom Seq ss = Seg len Seq q1 by A3,FINSEQ_1:def 3;
       Seq q2 = {} by A2,Th2;
     then len Seq q2 = 0 by FINSEQ_1:25;
     hence thesis by A3,A4;
    suppose A5: q2 <> {};
     consider ss being FinSubsequence such that
A6:  ss = q1 \/ (len p1 Shift q2) by A1,Th79;
     consider k1 such that
A7:  dom q1 c= Seg k1 by FINSEQ_1:def 12;
     consider k2 such that
A8:  dom (len p1 Shift q2) c= Seg k2 by FINSEQ_1:def 12;
A9:  rng Sgm dom ss = dom ss by FINSEQ_1:71;
       dom Seq ss = dom (ss*Sgm dom ss) by FINSEQ_1:def 14;
then A10:  dom Seq ss = dom Sgm dom ss by A9,RELAT_1:46
               .= dom Sgm (dom q1 \/ dom (len p1 Shift q2)) by A6,RELAT_1:13
               .= dom ((Sgm dom q1)^(Sgm dom (len p1 Shift q2)))
                     by A1,A5,Lm11
               .= Seg (len Sgm dom q1 + len Sgm dom (len p1 Shift q2))
                     by FINSEQ_1:def 7;
   len Sgm dom (len p1 Shift q2) = Card dom (len p1 Shift q2) &
        len Sgm dom q1 = Card dom q1 by A7,A8,FINSEQ_3:44;
then len Sgm dom (len p1 Shift q2) = Card (len p1 Shift q2) &
        len Sgm dom q1 = Card q1 by PRE_CIRC:21;
then len Sgm dom (len p1 Shift q2) = Card q2 & len Sgm dom q1 = Card q1 by Th57
;
     then len Sgm dom (len p1 Shift q2) = len Seq q2 & len Sgm dom q1 = len
Seq q1
        by Th7;
     hence thesis by A6,A10;
   end;

theorem Th81:
 for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
     ex ss being FinSubsequence st ss = q1 \/ (len p1 Shift q2) &
        dom Seq ss = Seg (len Seq q1 + len Seq q2) &
           Seq ss = Seq q1 \/ (len Seq q1 Shift Seq q2)
   proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume
A1:  q1 c= p1 & q2 c= p2;
     then consider ss being FinSubsequence such that
A2:  ss = q1 \/ (len p1 Shift q2) and
A3:  dom Seq ss = Seg (len Seq q1 + len Seq q2) by Th80;
     per cases;
    suppose A4: q1 = {} & q2 = {};
     then (len p1 Shift q2) = {} by Th55;
then A5:  Seq ss = {} & Seq q1 = {} & Seq q2 = {} by A2,A4,Th2;
     then Seq q1 \/ (len Seq q1 Shift Seq q2) = {} by Th55;
     hence thesis by A2,A3,A5;
    suppose A6: q1 = {} & q2 <> {};
then A7:  Seq ss = Seq q2 by A2,Th77;
A8:  Seq q1 = {} by A6,Th2;
     then len Seq q1 = 0 by FINSEQ_1:25;
     then Seq q1 \/ (len Seq q1 Shift Seq q2) = Seq q2 by A8,Th52;
     hence thesis by A2,A3,A7;
    suppose A9: q1 <> {} & q2 = {};
     then A10: (len p1 Shift q2) = {} by Th55;
       Seq q2 = {} by A9,Th2;
     then (len Seq q1 Shift Seq q2) = {} by Th55;
     hence thesis by A2,A3,A10;
    suppose A11: q1 <> {} & q2 <> {};
A12:  Seg (len Seq q1 + len Seq q2)
        = {k: 1 <= k & k <= len Seq q1 + len Seq q2} by FINSEQ_1:def 1;
A13:  dom Seq q1 = Seg len Seq q1 by FINSEQ_1:def 3
               .= {k: 1 <= k & k <= len Seq q1} by FINSEQ_1:def 1;
       Seq q2 <> {} by A11,Th2;
then A14:  dom (len Seq q1 Shift Seq q2)
        = {k: len Seq q1 + 1 <= k & k <= len Seq q1 + len Seq q2} by Th54;
A15:  Seg (len Seq q1 + len Seq q2)
        = dom Seq q1 \/ dom (len Seq q1 Shift Seq q2)
      proof
        thus Seg (len Seq q1 + len Seq q2)
                c= dom Seq q1 \/ dom (len Seq q1 Shift Seq q2)
         proof let x; assume x in Seg (len Seq q1 + len Seq q2);
           then consider k1 such that
A16:        x = k1 & 1 <= k1 & k1 <= len Seq q1 + len Seq q2 by A12;
A17:        1 <= k1 & k1 <= len Seq q1 implies k1 in dom Seq q1 by A13;
             len Seq q1 + 1 <= k1 & k1 <= len Seq q1 + len Seq q2 implies
            k1 in dom (len Seq q1 Shift Seq q2) by A14;
           hence thesis by A16,A17,INT_1:20,XBOOLE_0:def 2;
         end; let x; assume
        A18: x in dom Seq q1 \/ dom (len Seq q1 Shift Seq q2);
A19:     0 <= len Seq q1 & 0 <= len Seq q2 by NAT_1:18;
A20:     now assume x in dom Seq q1;
          then consider k1 such that
A21:       x = k1 & 1 <= k1 & k1 <= len Seq q1 by A13;
            len Seq q1 + 0 <= len Seq q1 + len Seq q2 by A19,REAL_1:55;
          then k1 <= len Seq q1 + len Seq q2 by A21,AXIOMS:22;
          hence x in Seg (len Seq q1 + len Seq q2) by A12,A21;
        end;
          now assume x in dom (len Seq q1 Shift Seq q2);
          then consider k2 such that
A22:       x = k2 & len Seq q1 + 1 <= k2 & k2 <= len Seq q1 + len Seq q2 by A14
;
            0+1 <= len Seq q1 + 1 by A19,REAL_1:55;
          then 1 <= k2 by A22,AXIOMS:22;
          hence x in Seg (len Seq q1 + len Seq q2) by A12,A22;
        end;
        hence thesis by A18,A20,XBOOLE_0:def 2;
      end;
     A23: dom Seq q1 \/ dom (len Seq q1 Shift Seq q2)
        = dom (Seq q1 \/ (len Seq q1 Shift Seq q2)) by RELAT_1:13;
       dom Seq q1 misses dom (len Seq q1 Shift Seq q2) by Th63;
     then reconsider ss1 = Seq q1 \/ (len Seq q1 Shift Seq q2) as Function
        by GRFUNC_1:31;
       for x st x in dom Seq ss holds (Seq ss).x = ss1.x
      proof let x; assume
A24:     x in dom Seq ss;
then A25:     x in dom (ss*Sgm dom ss) by FINSEQ_1:def 14;
A26:     (Seq ss).x = (ss*Sgm dom ss).x by FINSEQ_1:def 14
                  .= ss.((Sgm dom ss).x) by A25,FUNCT_1:22
                  .= ss.((Sgm (dom q1 \/ dom (len p1 Shift q2))).x)
                        by A2,RELAT_1:13
                  .= ss.(((Sgm dom q1)^(Sgm dom (len p1 Shift q2))).x)
                        by A1,A11,Lm11;
A27:     now assume
A28:       x in dom Seq q1;
then A29:       x in dom Sgm dom q1 by Lm4;
          then (Sgm dom q1).x in rng Sgm dom q1 by FUNCT_1:def 5;
then A30:       (Sgm dom q1).x in dom q1 by FINSEQ_1:71;
            (Seq ss).x = ss.((Sgm dom q1).x) by A26,A29,FINSEQ_1:def 7
                    .= q1.((Sgm dom q1).x) by A2,A30,GRFUNC_1:34
                    .= (q1*Sgm dom q1).x by A29,FUNCT_1:23
                    .= (Seq q1).x by FINSEQ_1:def 14;
          hence ss1.x = (Seq ss).x by A28,GRFUNC_1:34;
        end;
          now assume
A31:       x in dom (len Seq q1 Shift Seq q2);
            dom (len Seq q1 Shift Seq q2) = {len Seq q1 + j: j in dom Seq q2}
             by Def15;
          then consider j such that
A32:       x = len Seq q1 + j & j in dom Seq q2 by A31;
A33:       ss1.x = (len Seq q1 Shift Seq q2).x by A31,GRFUNC_1:34
               .= (Seq q2).j by A32,Def15;
          consider l1 such that
A34:       dom q1 c= Seg l1 by FINSEQ_1:def 12;
          consider l2 such that
A35:       dom (len p1 Shift q2) c= Seg l2 by FINSEQ_1:def 12;
        Card dom q1 = len Sgm dom q1 by A34,FINSEQ_3:44;
then A36:       Card q1 = len Sgm dom q1 by PRE_CIRC:21;
          A37: len Seq q1 = Card q1 by Th7;
A38:       dom Seq q2 = Seg len Seq q2 by FINSEQ_1:def 3;
        Card q2 = len Seq q2 by Th7;
then Card (len p1 Shift q2) = len Seq q2 by Th57;
then A39:       Card dom (len p1 Shift q2) = len Seq q2 by PRE_CIRC:21;
          A40: Card dom (len p1 Shift q2) = len Sgm dom (len p1 Shift q2)
             by A35,FINSEQ_3:44;
          A41: len Sgm dom (len p1 Shift q2) = len Seq q2 by A35,A39,FINSEQ_3:
44;
          A42: dom Seq q2 = dom Sgm dom (len p1 Shift q2) by A38,A39,A40,
FINSEQ_1:def 3;
A43:       j in dom Sgm dom (len p1 Shift q2) by A32,A38,A41,FINSEQ_1:def 3;
            (Sgm dom (len p1 Shift q2)).j in rng Sgm dom (len p1 Shift q2)
             by A32,A42,FUNCT_1:def 5;
then A44:       (Sgm dom (len p1 Shift q2)).j in dom (len p1 Shift q2)
             by FINSEQ_1:71;
         (Seq ss).x
           = ss.((Sgm dom (len p1 Shift q2)).j) by A26,A32,A36,A37,A43,FINSEQ_1
:def 7
          .= (len p1 Shift q2).((Sgm dom (len p1 Shift q2)).j)
                by A2,A44,GRFUNC_1:34
          .= ((len p1 Shift q2)*(Sgm dom (len p1 Shift q2))).j
                by A32,A42,FUNCT_1:23
          .= (Seq (len p1 Shift q2)).j by FINSEQ_1:def 14
          .= (Seq q2).j by A32,Th76;
          hence ss1.x = (Seq ss).x by A33;
        end;
        hence ss1.x = (Seq ss).x by A3,A15,A24,A27,XBOOLE_0:def 2;
      end;
     then Seq ss = ss1 by A3,A15,A23,FUNCT_1:9;
     hence thesis by A2,A3;
   end;

theorem Th82:
 for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
     ex ss being FinSubsequence st
        ss = q1 \/ (len p1 Shift q2) & (Seq q1)^(Seq q2) = Seq ss
   proof let p1,p2 be FinSequence, q1,q2 be FinSubsequence; assume
       q1 c= p1 & q2 c= p2;
     then consider ss being FinSubsequence such that
A1:  ss = q1 \/ (len p1 Shift q2) and
A2:  dom Seq ss = Seg (len Seq q1 + len Seq q2) and
A3:  Seq ss = Seq q1 \/ (len Seq q1 Shift Seq q2) by Th81;
A4:  for j1 st j1 in dom Seq q1 holds (Seq ss).j1 = (Seq q1).j1
      by A3,GRFUNC_1:34;
   for j2 st j2 in dom Seq q2 holds (Seq ss).(len Seq q1 + j2) = (Seq q2).j2
      proof let j2; assume
A5:     j2 in dom Seq q2;
          dom (len Seq q1 Shift Seq q2) = {len Seq q1 + k: k in dom Seq q2}
           by Def15;
        then len Seq q1 + j2 in dom (len Seq q1 Shift Seq q2) by A5;
        hence (Seq ss).(len Seq q1 + j2)
                 = (len Seq q1 Shift Seq q2).(len Seq q1 + j2)
                      by A3,GRFUNC_1:34
                .= (Seq q2).j2 by A5,Def15;
      end;
     then Seq ss = (Seq q1)^(Seq q2) by A2,A4,FINSEQ_1:def 7;
     hence thesis by A1;
   end;

theorem
    (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2
)
   proof
A1:  (R1 concur R2) before (P1 concur P2)
        = {C1^C2: C1 in R1 concur R2 & C2 in P1 concur P2} by Def13;
A2:  (R1 before P1) concur (R2 before P2)
        = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
              Seq q1 in R1 before P1 & Seq q2 in R2 before P2} by Def14;
A3:  R1 concur R2 = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
                        Seq q1 in R1 & Seq q2 in R2} by Def14;
A4:  P1 concur P2 = {C: ex q1,q2 st C = q1 \/ q2 & q1 misses q2 &
                        Seq q1 in P1 & Seq q2 in P2} by Def14;
A5:  R1 before P1 = {C1^C2: C1 in R1 & C2 in P1} by Def13;
A6:  R2 before P2 = {C1^C2: C1 in R2 & C2 in P2} by Def13;
     let x; assume x in (R1 concur R2) before (P1 concur P2);
     then consider C1,C2 such that
A7:  x = C1^C2 & C1 in R1 concur R2 & C2 in P1 concur P2 by A1;
     consider C3 such that
A8:  C1 = C3 & ex q1,q2 st C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 &
                Seq q2 in R2 by A3,A7;
     consider q1,q2 such that
A9:  C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 by A8;
     consider C4 being firing-sequence of N such that
A10:  C2 = C4 & ex q3,q4 st C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 &
                Seq q4 in P2 by A4,A7;
     consider q3,q4 such that
A11:  C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 by A10;
     reconsider C = C1^C2 as firing-sequence of N;
     reconsider q5 = len C1 Shift q3, q6 = len C1 Shift q4
        as FinSubsequence;
A12:  q1 c= C1 & q2 c= C1 & q3 c= C2 & q4 c= C2 by A8,A9,A10,A11,XBOOLE_1:7;
then A13:  q1 misses q5 & q2 misses q6 by Lm9;
       C1 c= C1^C2 by FINSEQ_6:12;
then A14:  q1 c= C1^C2 & q2 c= C1^C2 by A12,XBOOLE_1:1;
     reconsider ss = C2 as FinSubsequence by FINSEQ_1:68;
A15:  q5 c= len C1 Shift ss & q6 c= len C1 Shift ss by A12,Th70;
       len C1 Shift C2 c= C1^C2 by Th71;
     then q5 c= C1^C2 & q6 c= C1^C2 by A15,XBOOLE_1:1;
     then dom q1 misses dom q5 & dom q2 misses dom q6 by A13,A14,Th10;
     then reconsider ss1 = q1 \/ q5, ss2 = q2 \/ q6 as Function by GRFUNC_1:31;
A16:  dom C = Seg len C by FINSEQ_1:def 3;
       dom ss1 c= dom C & dom ss2 c= dom C by A12,Lm8;
     then reconsider ss1, ss2 as FinSubsequence by A16,FINSEQ_1:def 12;
A17:  ss1 \/ ss2 = q1 \/ (len C1 Shift q3) \/ q2 \/ (len C1 Shift q4)
                     by XBOOLE_1:4
               .= (q1 \/ q2) \/ (len C1 Shift q3) \/ (len C1 Shift q4)
                     by XBOOLE_1:4
               .= C1 \/ ((len C1 Shift q3) \/ (len C1 Shift q4))
                     by A8,A9,XBOOLE_1:4
               .= C1 \/ (len C1 Shift C2) by A10,A11,Th73
               .= C by Th64;
A18:  ss1 misses ss2
      proof
          ss1 /\ q2 = q1 /\ q2 \/ (len C1 Shift q3) /\ q2 &
          ss1 /\ (len C1 Shift q4) = q1 /\ (len C1 Shift q4)
             \/ (len C1 Shift q3) /\ (len C1 Shift q4) by XBOOLE_1:23;
then A19:     ss1 /\ ss2 = (q1 /\ q2 \/ (len C1 Shift q3) /\ q2) \/ (q1 /\
           (len C1 Shift q4) \/ (len C1 Shift q3) /\ (len C1 Shift q4)) by
XBOOLE_1:23;
A20:     q1 /\ q2 = {} by A9,XBOOLE_0:def 7;
          (len C1 Shift q3) misses q2 & q1 misses (len C1 Shift q4)
           by A12,Lm9;
then A21:     (len C1 Shift q3) /\ q2 = {} & q1 /\ (len C1 Shift q4) = {}
           by XBOOLE_0:def 7;
          dom q3 misses dom q4 by A11,A12,Th10;
        then dom (len C1 Shift q3) misses dom (len C1 Shift q4) by Th72;
        then (len C1 Shift q3) misses (len C1 Shift q4) by Th8;
        hence ss1 /\ ss2 = {} by A19,A20,A21,XBOOLE_0:def 7;
      end;
     consider ss3 being FinSubsequence such that
A22:  ss3 = ss1 & (Seq q1)^(Seq q3) = Seq ss3 by A12,Th82;
     consider ss4 being FinSubsequence such that
A23:  ss4 = ss2 & (Seq q2)^(Seq q4) = Seq ss4 by A12,Th82;
A24:  Seq ss1 in R1 before P1 by A5,A9,A11,A22;
   Seq ss2 in R2 before P2 by A6,A9,A11,A23;
     hence thesis by A2,A7,A17,A18,A24;
   end;

definition
 let P, N;
 let R1, R2 be non empty process of N;
 cluster R1 concur R2 -> non empty;
 coherence
   proof
A1:  R1 concur R2 = {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 &
                        q1 misses q2 & Seq q1 in R1 & Seq q2 in R2} by Def14;
     consider fs1 being set such that
A2:  fs1 in R1 by XBOOLE_0:def 1;
     consider fs2 being set such that
A3:  fs2 in R2 by XBOOLE_0:def 1;
     reconsider fs1, fs2 as firing-sequence of N by A2,A3;
     reconsider C = fs1^fs2 as firing-sequence of N;
A4:  C = fs1 \/ (len fs1 Shift fs2) by Th64;
A5:  fs1 misses (len fs1 Shift fs2) by Th65;
     A6: fs1 = Seq fs1 by GRAPH_2:24;
   Seq (len fs1 Shift fs2) in R2 by A3,Th61;
     then C in R1 concur R2 by A1,A2,A4,A5,A6;
     hence thesis;
   end;
end;

begin  :: Neutral process

definition let P;
 let N be Petri_net of P;
 func NeutralProcess(N) -> non empty process of N equals :Def16:
 {<*>N};
 coherence;
end;

definition
 let P;
 let N be Petri_net of P;
 let t be Element of N;
 func ElementaryProcess(t) -> non empty process of N equals
   {<*t*>};
 coherence;
end;

theorem
   NeutralProcess(N) before R = R
  proof
A1: NeutralProcess(N) = {<*>N} by Def16;
A2: NeutralProcess(N) before R = {C1^C: C1 in NeutralProcess(N) & C in R}
       by Def13;
    thus NeutralProcess(N) before R c= R
     proof
       let x;
       assume x in (NeutralProcess(N) before R);
       then consider C1,C such that
A3:    x = C1^C & C1 in NeutralProcess(N) & C in R by A2;
         C1 = <*>N by A1,A3,TARSKI:def 1;
       hence x in R by A3,FINSEQ_1:47;
     end;
    let x;
    assume
A4:  x in R;
    then reconsider C = x as Element of N*;
       <*>N in NeutralProcess(N) & x = (<*>N)^C by A1,FINSEQ_1:47,TARSKI:def 1;
    hence x in (NeutralProcess(N) before R) by A2,A4;
  end;

theorem
   R before NeutralProcess(N) = R
  proof
A1: NeutralProcess(N) = {<*>N} by Def16;
A2: R before NeutralProcess N = {C1^C: C1 in R & C in NeutralProcess(N)}
       by Def13;
    thus R before NeutralProcess N c= R
     proof
       let x;
       assume x in R before NeutralProcess N;
       then consider C1,C such that
A3:    x = C1^C & C1 in R & C in NeutralProcess(N) by A2;
         C = <*>N by A1,A3,TARSKI:def 1;
       hence x in R by A3,FINSEQ_1:47;
     end;
    let x;
    assume
A4:  x in R;
    then reconsider C = x as Element of N*;
       <*>N in NeutralProcess(N) & x = C^(<*>N) by A1,FINSEQ_1:47,TARSKI:def 1;
    hence x in R before NeutralProcess N by A2,A4;
  end;

theorem
   NeutralProcess(N) concur R = R
  proof
      NeutralProcess(N) = {<*>N} by Def16;
then A1:  NeutralProcess(N) concur R =
     {C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
       Seq q1 in {<*>N} & Seq q2 in R} by Def14;
   thus NeutralProcess(N) concur R c= R
    proof
      let x; assume x in NeutralProcess(N) concur R;
      then consider C such that
A2:   x = C & ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
      Seq q1 in {<*>N} & Seq q2 in R by A1;
      consider q1,q2 being FinSubsequence such that
A3:   C = q1 \/ q2 & q1 misses q2 & Seq q1 in {<*>N} & Seq q2 in R by A2;
        Seq q1 = {} by A3,TARSKI:def 1;
      then q1 = {} by Lm1;
      hence x in R by A2,A3,GRAPH_2:24;
    end;
   let x; assume
A4: x in R;
   then reconsider C = x as firing-sequence of N;
   reconsider q1 = <*>N, q2 = C as FinSubsequence;
     q1 /\ q2 = {};
   then Seq q2 = C & {} \/ q2 = C & Seq q1 = q1 & q1 in {<*>N} & q1 misses q2
      by GRAPH_2:24,TARSKI:def 1,XBOOLE_0:def 7;
   hence x in NeutralProcess(N) concur R by A1,A4;
  end;

Back to top