boolmark.miz



    begin

    theorem :: BOOLMARK:1

    

     Th1: for A,B be non empty set, f be Function of A, B, C be Subset of A, v be Element of B holds (f +* (C --> v)) is Function of A, B

    proof

      let A,B be non empty set;

      let f be Function of A, B;

      let C be Subset of A;

      let v be Element of B;

      

       A1: ( dom f) = A by FUNCT_2:def 1;

      ( rng f) c= B & ( rng (C --> v)) c= {v} by FUNCOP_1: 13, RELAT_1:def 19;

      then

       A2: (( rng f) \/ ( rng (C --> v))) c= (B \/ {v}) by XBOOLE_1: 13;

      ( rng (f +* (C --> v))) c= (( rng f) \/ ( rng (C --> v))) by FUNCT_4: 17;

      then ( rng (f +* (C --> v))) c= (B \/ {v}) by A2, XBOOLE_1: 1;

      then

       A3: ( rng (f +* (C --> v))) c= B by ZFMISC_1: 40;

      ( dom (f +* (C --> v))) = (( dom f) \/ ( dom (C --> v))) by FUNCT_4:def 1

      .= (( [#] A) \/ C) by A1, FUNCOP_1: 13

      .= A by SUBSET_1: 11;

      hence thesis by A3, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: BOOLMARK:2

    

     Th2: for X,Y be non empty set, A,B be Subset of X, f be Function of X, Y st (f .: A) misses (f .: B) holds A misses B

    proof

      let X,Y be non empty set;

      let A,B be Subset of X;

      let f be Function of X, Y such that

       A1: ((f .: A) /\ (f .: B)) = {} ;

      assume (A /\ B) <> {} ;

      then

      consider x be Element of X such that

       A2: x in (A /\ B) by SUBSET_1: 4;

      x in B by A2, XBOOLE_0:def 4;

      then

       A3: (f . x) in (f .: B) by FUNCT_2: 35;

      x in A by A2, XBOOLE_0:def 4;

      then (f . x) in (f .: A) by FUNCT_2: 35;

      hence contradiction by A1, A3, XBOOLE_0:def 4;

    end;

    theorem :: BOOLMARK:3

    

     Th3: for A,B be set, f be Function, x be set holds A misses B implies ((f +* (A --> x)) .: B) = (f .: B)

    proof

      let A,B be set, f be Function, x be set;

      assume that

       A1: (A /\ B) = {} and

       A2: ((f +* (A --> x)) .: B) <> (f .: B);

      

       A3: ( dom (f +* (A --> x))) = (( dom f) \/ ( dom (A --> x))) by FUNCT_4:def 1;

      

       A4: ( dom (A --> x)) = A by FUNCOP_1: 13;

      

       A5: not (for y be object holds y in ((f +* (A --> x)) .: B) iff y in (f .: B)) by A2, TARSKI: 2;

      now

        per cases by A5;

          case ex y be set st y in ((f +* (A --> x)) .: B) & not y in (f .: B);

          then

          consider y be set such that

           A6: y in ((f +* (A --> x)) .: B) and

           A7: not y in (f .: B);

          consider z be object such that

           A8: z in ( dom (f +* (A --> x))) and

           A9: z in B and

           A10: y = ((f +* (A --> x)) . z) by A6, FUNCT_1:def 6;

           not z in A by A1, A9, XBOOLE_0:def 4;

          then z in ( dom f) & y = (f . z) by A3, A4, A8, A10, FUNCT_4: 11, XBOOLE_0:def 3;

          hence contradiction by A7, A9, FUNCT_1:def 6;

        end;

          case ex y be set st not y in ((f +* (A --> x)) .: B) & y in (f .: B);

          then

          consider y be set such that

           A11: not y in ((f +* (A --> x)) .: B) and

           A12: y in (f .: B);

          consider z be object such that

           A13: z in ( dom f) and

           A14: z in B and

           A15: y = (f . z) by A12, FUNCT_1:def 6;

           not z in A by A1, A14, XBOOLE_0:def 4;

          then

           A16: y = ((f +* (A --> x)) . z) by A4, A15, FUNCT_4: 11;

          z in ( dom (f +* (A --> x))) by A3, A13, XBOOLE_0:def 3;

          hence contradiction by A11, A14, A16, FUNCT_1:def 6;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let PTN be PT_net_Str;

      :: BOOLMARK:def1

      func Bool_marks_of PTN -> FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN equals ( Funcs (the carrier of PTN, BOOLEAN ));

      correctness ;

    end

    definition

      let PTN be PT_net_Str;

      mode Boolean_marking of PTN is Element of ( Bool_marks_of PTN);

    end

    definition

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let t be transition of PTN;

      :: BOOLMARK:def2

      pred t is_firable_on M0 means (M0 .: ( *' {t})) c= { TRUE };

    end

    notation

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let t be transition of PTN;

      antonym t is_not_firable_on M0 for t is_firable_on M0;

    end

    definition

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let t be transition of PTN;

      :: BOOLMARK:def3

      func Firing (t,M0) -> Boolean_marking of PTN equals ((M0 +* (( *' {t}) --> FALSE )) +* (( {t} *' ) --> TRUE ));

      coherence

      proof

        set M1 = ((M0 +* (( *' {t}) --> FALSE )) +* (( {t} *' ) --> TRUE ));

        (M0 +* (( *' {t}) --> FALSE )) is Function of the carrier of PTN, BOOLEAN by Th1;

        then M1 is Function of the carrier of PTN, BOOLEAN by Th1;

        hence thesis by FUNCT_2: 8;

      end;

      correctness ;

    end

    definition

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let Q be FinSequence of the carrier' of PTN;

      :: BOOLMARK:def4

      pred Q is_firable_on M0 means Q = {} or ex M be FinSequence of ( Bool_marks_of PTN) st ( len Q) = ( len M) & (Q /. 1) is_firable_on M0 & (M /. 1) = ( Firing ((Q /. 1),M0)) & for i be Element of NAT st i < ( len Q) & i > 0 holds (Q /. (i + 1)) is_firable_on (M /. i) & (M /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M /. i)));

    end

    notation

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let Q be FinSequence of the carrier' of PTN;

      antonym Q is_not_firable_on M0 for Q is_firable_on M0;

    end

    definition

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let Q be FinSequence of the carrier' of PTN;

      :: BOOLMARK:def5

      func Firing (Q,M0) -> Boolean_marking of PTN means

      : Def5: it = M0 if Q = {}

      otherwise ex M be FinSequence of ( Bool_marks_of PTN) st ( len Q) = ( len M) & it = (M /. ( len M)) & (M /. 1) = ( Firing ((Q /. 1),M0)) & for i be Nat st i < ( len Q) & i > 0 holds (M /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M /. i)));

      existence

      proof

        defpred P2[ Nat] means for Q be FinSequence of the carrier' of PTN st $1 = ( len Q) holds (Q = {} implies ex M1 be Boolean_marking of PTN st M1 = M0) & (Q <> {} implies ex M2 be Boolean_marking of PTN st ex M be FinSequence of ( Bool_marks_of PTN) st ( len Q) = ( len M) & M2 = (M /. ( len M)) & (M /. 1) = ( Firing ((Q /. 1),M0)) & for i be Nat st i < ( len Q) & i > 0 holds (M /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M /. i))));

         A1:

        now

          let n be Nat;

          assume

           A2: P2[n];

          thus P2[(n + 1)]

          proof

            let Q be FinSequence of the carrier' of PTN such that

             A3: (n + 1) = ( len Q);

            thus Q = {} implies ex M1 be Boolean_marking of PTN st M1 = M0;

            thus Q <> {} implies ex M2 be Boolean_marking of PTN, M be FinSequence of ( Bool_marks_of PTN) st ( len Q) = ( len M) & M2 = (M /. ( len M)) & (M /. 1) = ( Firing ((Q /. 1),M0)) & for i be Nat st i < ( len Q) & i > 0 holds (M /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M /. i)))

            proof

              assume Q <> {} ;

              then ( len Q) <> 0 ;

              then

              consider Q1 be FinSequence of the carrier' of PTN, t be transition of PTN such that

               A4: Q = (Q1 ^ <*t*>) by FINSEQ_2: 19;

              

               A5: (n + 1) = (( len Q1) + 1) by A3, A4, FINSEQ_2: 16;

              per cases ;

                suppose

                 A6: Q1 = {} ;

                take M2 = ( Firing (t,M0));

                take M = <*M2*>;

                

                 A7: ( len Q) = (( len Q1) + ( len <*t*>)) by A4, FINSEQ_1: 22

                .= ( 0 + ( len <*t*>)) by A6

                .= ( 0 + 1) by FINSEQ_1: 39;

                hence ( len Q) = ( len M) by FINSEQ_1: 39;

                hence M2 = (M /. ( len M)) by A7, FINSEQ_4: 16;

                Q = <*t*> by A4, A6, FINSEQ_1: 34;

                then (Q /. 1) = t by FINSEQ_4: 16;

                hence (M /. 1) = ( Firing ((Q /. 1),M0)) by FINSEQ_4: 16;

                let i be Nat;

                assume i < ( len Q) & i > 0 ;

                hence thesis by A7, NAT_1: 13;

              end;

                suppose

                 A8: Q1 <> {} ;

                then

                 A9: ( len Q1) > 0 by NAT_1: 3;

                then ( 0 + 1) < (( len Q1) + 1) by XREAL_1: 6;

                then 1 <= ( len Q1) by NAT_1: 13;

                then

                 A10: 1 in ( dom Q1) by FINSEQ_3: 25;

                

                 A11: ( len Q) = (( len Q1) + ( len <*t*>)) by A4, FINSEQ_1: 22

                .= (( len Q1) + 1) by FINSEQ_1: 40;

                consider B2 be Boolean_marking of PTN, B be FinSequence of ( Bool_marks_of PTN) such that

                 A12: ( len Q1) = ( len B) and

                 A13: B2 = (B /. ( len B)) and

                 A14: (B /. 1) = ( Firing ((Q1 /. 1),M0)) and

                 A15: for i be Nat st i < ( len Q1) & i > 0 holds (B /. (i + 1)) = ( Firing ((Q1 /. (i + 1)),(B /. i))) by A2, A5, A8;

                take M2 = ( Firing (t,B2));

                take M = (B ^ <*M2*>);

                

                 A16: ( len M) = (( len B) + ( len <*M2*>)) by FINSEQ_1: 22

                .= (( len B) + 1) by FINSEQ_1: 40;

                hence ( len Q) = ( len M) by A12, A11;

                thus M2 = (M /. ( len M)) by A16, FINSEQ_4: 67;

                ( 0 + 1) < (( len B) + 1) by A12, A9, XREAL_1: 6;

                then

                 A17: 1 <= ( len B) by NAT_1: 13;

                then 1 in ( dom B) by FINSEQ_3: 25;

                

                hence (M /. 1) = (B /. 1) by FINSEQ_4: 68

                .= ( Firing ((Q /. 1),M0)) by A4, A14, A10, FINSEQ_4: 68;

                let i be Nat such that

                 A18: i < ( len Q) and

                 A19: i > 0 ;

                thus (M /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M /. i)))

                proof

                  1 <= (i + 1) & (i + 1) <= (( len Q1) + 1) by A11, A18, NAT_1: 12, NAT_1: 13;

                  then

                   A20: ( Seg (( len Q1) + 1)) = (( Seg ( len Q1)) \/ {(( len Q1) + 1)}) & (i + 1) in ( Seg (( len Q1) + 1)) by FINSEQ_1: 1, FINSEQ_1: 9;

                  per cases by A20, XBOOLE_0:def 3;

                    suppose

                     A21: (i + 1) in ( Seg ( len Q1));

                    then (i + 1) <= ( len B) by A12, FINSEQ_1: 1;

                    then (i + 1) <= (( len B) + 1) by NAT_1: 12;

                    then

                     A22: i <= ( len B) by XREAL_1: 6;

                    ( 0 + 1) < (i + 1) by A19, XREAL_1: 6;

                    then 1 <= i by NAT_1: 13;

                    then

                     A23: i in ( dom B) by A22, FINSEQ_3: 25;

                    (i + 1) <= ( len Q1) by A21, FINSEQ_1: 1;

                    then i < ( len Q1) by NAT_1: 13;

                    then

                     A24: (B /. (i + 1)) = ( Firing ((Q1 /. (i + 1)),(B /. i))) by A15, A19;

                    (i + 1) in ( dom Q1) by A21, FINSEQ_1:def 3;

                    then

                     A25: (Q1 /. (i + 1)) = (Q /. (i + 1)) by A4, FINSEQ_4: 68;

                    (i + 1) in ( dom B) by A12, A21, FINSEQ_1:def 3;

                    then (B /. (i + 1)) = (M /. (i + 1)) by FINSEQ_4: 68;

                    hence thesis by A24, A25, A23, FINSEQ_4: 68;

                  end;

                    suppose

                     A26: (i + 1) in {(( len Q1) + 1)};

                    

                     A27: ( len B) in ( dom B) by A17, FINSEQ_3: 25;

                    

                     A28: (i + 1) = (( len Q1) + 1) by A26, TARSKI:def 1;

                    then (M /. (i + 1)) = M2 & (Q /. (i + 1)) = t by A4, A12, FINSEQ_4: 67;

                    hence thesis by A12, A13, A28, A27, FINSEQ_4: 68;

                  end;

                end;

              end;

            end;

          end;

        end;

        

         A29: P2[ 0 ];

        for n be Nat holds P2[n] from NAT_1:sch 2( A29, A1);

        hence thesis;

      end;

      uniqueness

      proof

        let B1,B2 be Boolean_marking of PTN;

        thus Q = {} & B1 = M0 & B2 = M0 implies B1 = B2;

        assume Q <> {} ;

        given M1 be FinSequence of ( Bool_marks_of PTN) such that

         A30: ( len Q) = ( len M1) and

         A31: B1 = (M1 /. ( len M1)) and

         A32: (M1 /. 1) = ( Firing ((Q /. 1),M0)) and

         A33: for i be Nat st i < ( len Q) & i > 0 holds (M1 /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M1 /. i)));

        

         A34: ( dom M1) = ( Seg ( len Q)) by A30, FINSEQ_1:def 3;

        given M2 be FinSequence of ( Bool_marks_of PTN) such that

         A35: ( len Q) = ( len M2) and

         A36: B2 = (M2 /. ( len M2)) and

         A37: (M2 /. 1) = ( Firing ((Q /. 1),M0)) and

         A38: for i be Nat st i < ( len Q) & i > 0 holds (M2 /. (i + 1)) = ( Firing ((Q /. (i + 1)),(M2 /. i)));

        defpred P2[ Nat] means $1 in ( Seg ( len Q)) implies (M1 /. $1) = (M2 /. $1);

         A39:

        now

          let j be Nat;

          reconsider jj = j as Element of NAT by ORDINAL1:def 12;

          assume

           A40: P2[j];

          now

            assume

             A41: (j + 1) in ( Seg ( len Q));

            per cases ;

              suppose j = 0 ;

              hence (M1 /. (j + 1)) = (M2 /. (j + 1)) by A32, A37;

            end;

              suppose

               A42: j <> 0 ;

              then

               A43: j > 0 by NAT_1: 3;

              (j + 1) <= ( len Q) & j < (j + 1) by A41, FINSEQ_1: 1, XREAL_1: 29;

              then

               A44: j < ( len Q) by XXREAL_0: 2;

              1 <= j by A42, NAT_1: 14;

              

              hence (M1 /. (j + 1)) = ( Firing ((Q /. (jj + 1)),(M2 /. jj))) by A33, A40, A44, FINSEQ_1: 1

              .= (M2 /. (j + 1)) by A38, A43, A44;

            end;

          end;

          hence P2[(j + 1)];

        end;

        

         A45: P2[ 0 ] by FINSEQ_1: 1;

        

         A46: for j be Nat holds P2[j] from NAT_1:sch 2( A45, A39);

        now

          let j be Nat;

          assume

           A47: j in ( dom M1);

          then

           A48: j in ( dom M2) by A35, A34, FINSEQ_1:def 3;

          

          thus (M1 . j) = (M1 /. j) by A47, PARTFUN1:def 6

          .= (M2 /. j) by A46, A34, A47

          .= (M2 . j) by A48, PARTFUN1:def 6;

        end;

        hence B1 = B2 by A30, A31, A35, A36, FINSEQ_2: 9;

      end;

      correctness ;

    end

    theorem :: BOOLMARK:4

    

     Th4: for A be non empty set, y be set, f be Function holds ((f +* (A --> y)) .: A) = {y}

    proof

      let A be non empty set, y be set, f be Function;

      now

        let u be object;

        thus u in ((f +* (A --> y)) .: A) implies u = y

        proof

          assume u in ((f +* (A --> y)) .: A);

          then

          consider z be object such that z in ( dom (f +* (A --> y))) and

           A1: z in A and

           A2: u = ((f +* (A --> y)) . z) by FUNCT_1:def 6;

          z in ( dom (A --> y)) by A1, FUNCOP_1: 13;

          then u = ((A --> y) . z) by A2, FUNCT_4: 13;

          hence thesis by A1, FUNCOP_1: 7;

        end;

        consider x be object such that

         A3: x in A by XBOOLE_0:def 1;

        

         A4: x in ( dom (A --> y)) by A3, FUNCOP_1: 13;

        then

         A5: x in ( dom (f +* (A --> y))) by FUNCT_4: 12;

        ((A --> y) . x) = y by A3, FUNCOP_1: 7;

        then y = ((f +* (A --> y)) . x) by A4, FUNCT_4: 13;

        hence u = y implies u in ((f +* (A --> y)) .: A) by A3, A5, FUNCT_1:def 6;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: BOOLMARK:5

    

     Th5: for PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN, s be place of PTN st s in ( {t} *' ) holds (( Firing (t,M0)) . s) = TRUE

    proof

      let PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN, s be place of PTN;

      set M = ((M0 +* (( *' {t}) --> FALSE )) +* (( {t} *' ) --> TRUE ));

      

       A1: ( [#] the carrier of PTN) = the carrier of PTN;

      

       A2: ( dom M0) = the carrier of PTN & ( dom (( *' {t}) --> FALSE )) = ( *' {t}) by FUNCT_2:def 1;

      ( dom (( {t} *' ) --> TRUE )) = ( {t} *' ) by FUNCT_2:def 1;

      

      then

       A3: ( dom M) = (( dom (M0 +* (( *' {t}) --> FALSE ))) \/ ( {t} *' )) by FUNCT_4:def 1

      .= ((the carrier of PTN \/ ( *' {t})) \/ ( {t} *' )) by A2, FUNCT_4:def 1

      .= (the carrier of PTN \/ (( *' {t}) \/ ( {t} *' ))) by XBOOLE_1: 4

      .= the carrier of PTN by A1, SUBSET_1: 11;

      assume

       A4: s in ( {t} *' );

      then (((M0 +* (( *' {t}) --> FALSE )) +* (( {t} *' ) --> TRUE )) .: ( {t} *' )) = { TRUE } by Th4;

      then (M . s) in { TRUE } by A4, A3, FUNCT_1:def 6;

      hence thesis by TARSKI:def 1;

    end;

     Lm1:

    now

      let PTN be Petri_net;

      let Sd be non empty Subset of the carrier of PTN;

      set M0 = ((the carrier of PTN --> TRUE ) qua Function +* (Sd --> FALSE ));

      

       A1: ( [#] the carrier of PTN) = the carrier of PTN;

      ( dom (the carrier of PTN --> TRUE ) qua Function) = the carrier of PTN & ( dom (Sd --> FALSE )) = Sd by FUNCOP_1: 13;

      

      then

       A2: ( dom M0) = (the carrier of PTN \/ Sd) by FUNCT_4:def 1

      .= the carrier of PTN by A1, SUBSET_1: 11;

      

       A3: ( rng M0) c= (( rng (the carrier of PTN --> TRUE )) \/ ( rng (Sd --> FALSE ))) by FUNCT_4: 17;

      ( rng (Sd --> FALSE )) c= { FALSE } by FUNCOP_1: 13;

      then

       A4: ( rng (Sd --> FALSE )) c= BOOLEAN by XBOOLE_1: 1;

      ( rng (the carrier of PTN --> TRUE )) c= { TRUE } by FUNCOP_1: 13;

      then ( rng (the carrier of PTN --> TRUE )) c= BOOLEAN by XBOOLE_1: 1;

      then (( rng (the carrier of PTN --> TRUE )) \/ ( rng (Sd --> FALSE ))) c= BOOLEAN by A4, XBOOLE_1: 8;

      then ( rng M0) c= BOOLEAN by A3, XBOOLE_1: 1;

      then

      reconsider M0 as Boolean_marking of PTN by A2, FUNCT_2:def 2;

      assume

       A5: for M0 be Boolean_marking of PTN st (M0 .: Sd) = { FALSE } holds for t be transition of PTN st t is_firable_on M0 holds (( Firing (t,M0)) .: Sd) = { FALSE };

      assume not Sd is Deadlock-like;

      then not ( *' Sd) c= (Sd *' );

      then

      consider t be transition of PTN such that

       A6: t in ( *' Sd) and

       A7: not t in (Sd *' ) by SUBSET_1: 2;

      ( {t} *' ) meets Sd by A6, PETRI: 20;

      then

      consider s be object such that

       A8: s in (( {t} *' ) /\ Sd) by XBOOLE_0: 4;

      s in ( {t} *' ) by A8, XBOOLE_0:def 4;

      then

       A9: (( Firing (t,M0)) . s) = TRUE by Th5;

      s in Sd by A8, XBOOLE_0:def 4;

      then TRUE in (( Firing (t,M0)) .: Sd) by A9, FUNCT_2: 35;

      then

       A10: (( Firing (t,M0)) .: Sd) <> { FALSE } by TARSKI:def 1;

      Sd misses ( *' {t}) by A7, PETRI: 19;

      then

       A11: ((the carrier of PTN --> TRUE ) qua Function .: ( *' {t})) = (M0 .: ( *' {t})) by Th3;

      ( rng (the carrier of PTN --> TRUE )) c= { TRUE } & ((the carrier of PTN --> TRUE ) .: ( *' {t})) c= ( rng (the carrier of PTN --> TRUE )) by FUNCOP_1: 13, RELAT_1: 111;

      then (M0 .: ( *' {t})) c= { TRUE } by A11, XBOOLE_1: 1;

      then

       A12: t is_firable_on M0;

      (M0 .: Sd) = { FALSE qua set} by Th4;

      hence contradiction by A5, A12, A10;

    end;

    theorem :: BOOLMARK:6

    for PTN be Petri_net, Sd be non empty Subset of the carrier of PTN holds Sd is Deadlock-like iff for M0 be Boolean_marking of PTN st (M0 .: Sd) = { FALSE } holds for t be transition of PTN st t is_firable_on M0 holds (( Firing (t,M0)) .: Sd) = { FALSE }

    proof

      let PTN be Petri_net, Sd be non empty Subset of the carrier of PTN;

      thus Sd is Deadlock-like implies for M0 be Boolean_marking of PTN st (M0 .: Sd) = { FALSE } holds for t be transition of PTN st t is_firable_on M0 holds (( Firing (t,M0)) .: Sd) = { FALSE }

      proof

        assume Sd is Deadlock-like;

        then

         A1: ( *' Sd) is Subset of (Sd *' );

        let M0 be Boolean_marking of PTN such that

         A2: (M0 .: Sd) = { FALSE };

        let t be transition of PTN;

        assume t is_firable_on M0;

        then (M0 .: ( *' {t})) c= { TRUE };

        then

         A3: (M0 .: ( *' {t})) misses { FALSE } by XBOOLE_1: 63, ZFMISC_1: 11;

        then ( *' {t}) misses Sd by A2, Th2;

        then not t in ( *' Sd) by A1, PETRI: 19;

        then ( {t} *' ) misses Sd by PETRI: 20;

        

        hence (( Firing (t,M0)) .: Sd) = ((M0 +* (( *' {t}) --> FALSE )) .: Sd) by Th3

        .= { FALSE } by A2, A3, Th2, Th3;

      end;

      thus thesis by Lm1;

    end;

    theorem :: BOOLMARK:7

    

     Th7: for D be non empty set holds for Q0,Q1 be FinSequence of D, i be Element of NAT st 1 <= i & i <= ( len Q0) holds ((Q0 ^ Q1) /. i) = (Q0 /. i)

    proof

      let D be non empty set;

      let Q0,Q1 be FinSequence of D, i be Element of NAT ;

      ( len Q0) <= (( len Q0) + ( len Q1)) by NAT_1: 11;

      then

       A1: i <= ( len Q0) implies i <= (( len Q0) + ( len Q1)) by XXREAL_0: 2;

      i in ( dom Q0) implies i in ( Seg ( len Q0)) by FINSEQ_1:def 3;

      then i in ( dom Q0) implies 1 <= i & i <= ( len (Q0 ^ Q1)) by A1, FINSEQ_1: 1, FINSEQ_1: 22;

      then

       A2: i in ( dom Q0) implies i in ( dom (Q0 ^ Q1)) by FINSEQ_3: 25;

      i in ( dom Q0) implies (Q0 . i) = (Q0 /. i) by PARTFUN1:def 6;

      then

       A3: i in ( dom Q0) implies ((Q0 ^ Q1) . i) = (Q0 /. i) by FINSEQ_1:def 7;

      i in ( dom Q0) iff i in ( Seg ( len Q0)) by FINSEQ_1:def 3;

      hence thesis by A2, A3, FINSEQ_1: 1, PARTFUN1:def 6;

    end;

    theorem :: BOOLMARK:8

    

     Th8: for PTN be Petri_net, M0 be Boolean_marking of PTN, Q0,Q1 be FinSequence of the carrier' of PTN holds ( Firing ((Q0 ^ Q1),M0)) = ( Firing (Q1,( Firing (Q0,M0))))

    proof

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let Q0,Q1 be FinSequence of the carrier' of PTN;

      now

        per cases ;

          case

           A1: Q0 = {} & Q1 = {} ;

          then

           A2: (Q0 ^ Q1) = {} by FINSEQ_1: 34;

          ( Firing (Q1,( Firing (Q0,M0)))) = ( Firing (Q1,M0)) by A1, Def5

          .= M0 by A1, Def5;

          hence thesis by A2, Def5;

        end;

          case

           A3: Q0 = {} & Q1 <> {} ;

          then ( Firing ((Q0 ^ Q1),M0)) = ( Firing (Q1,M0)) by FINSEQ_1: 34;

          hence thesis by A3, Def5;

        end;

          case

           A4: Q0 <> {} & Q1 = {} ;

          then ( Firing ((Q0 ^ Q1),M0)) = ( Firing (Q0,M0)) by FINSEQ_1: 34;

          hence thesis by A4, Def5;

        end;

          case

           A5: Q0 <> {} & Q1 <> {} ;

          then

          consider M3 be FinSequence of ( Bool_marks_of PTN) such that

           A6: ( len Q0) = ( len M3) & ( Firing (Q0,M0)) = (M3 /. ( len M3)) and

           A7: (M3 /. 1) = ( Firing ((Q0 /. 1),M0)) and

           A8: for i be Nat st i < ( len Q0) & i > 0 holds (M3 /. (i + 1)) = ( Firing ((Q0 /. (i + 1)),(M3 /. i))) by Def5;

          consider M be FinSequence of ( Bool_marks_of PTN) such that

           A9: ( len (Q0 ^ Q1)) = ( len M) and

           A10: ( Firing ((Q0 ^ Q1),M0)) = (M /. ( len M)) and

           A11: (M /. 1) = ( Firing (((Q0 ^ Q1) /. 1),M0)) and

           A12: for i be Nat st i < ( len (Q0 ^ Q1)) & i > 0 holds (M /. (i + 1)) = ( Firing (((Q0 ^ Q1) /. (i + 1)),(M /. i))) by A5, Def5;

          defpred P2[ Nat] means (1 + $1) <= ( len Q0) implies (M /. (1 + $1)) = (M3 /. (1 + $1));

           0 < ( len Q1) by A5, NAT_1: 3;

          then ( 0 + ( len Q0)) < (( len Q0) + ( len Q1)) by XREAL_1: 6;

          then

           A13: ( len Q0) < ( len (Q0 ^ Q1)) by FINSEQ_1: 22;

           A14:

          now

            let k be Nat;

            

             A15: 0 <= k by NAT_1: 2;

            assume

             A16: P2[k];

            now

              assume

               A17: (1 + (k + 1)) <= ( len Q0);

              then

               A18: ((Q0 ^ Q1) /. (1 + (k + 1))) = (Q0 /. (1 + (k + 1))) by Th7, NAT_1: 11;

              

               A19: (1 + k) < ( len Q0) by A17, NAT_1: 13;

              then (1 + k) < ( len (Q0 ^ Q1)) by A13, XXREAL_0: 2;

              then (M /. (1 + (k + 1))) = ( Firing ((Q0 /. (1 + (k + 1))),(M3 /. (1 + k)))) by A12, A15, A16, A17, A18, NAT_1: 13;

              hence (M /. (1 + (k + 1))) = (M3 /. (1 + (k + 1))) by A8, A15, A19;

            end;

            hence P2[(k + 1)];

          end;

          reconsider m = (( len Q0) - 1) as Element of NAT by A5, NAT_1: 3, NAT_1: 20;

          let i be Element of NAT ;

          ( len Q1) > 0 by A5, NAT_1: 3;

          then

           A20: ( 0 + 1) <= ( len Q1) by NAT_1: 13;

          consider M4 be FinSequence of ( Bool_marks_of PTN) such that

           A21: ( len Q1) = ( len M4) and

           A22: ( Firing (Q1,( Firing (Q0,M0)))) = (M4 /. ( len M4)) and

           A23: (M4 /. 1) = ( Firing ((Q1 /. 1),( Firing (Q0,M0)))) and

           A24: for i be Nat st i < ( len Q1) & i > 0 holds (M4 /. (i + 1)) = ( Firing ((Q1 /. (i + 1)),(M4 /. i))) by A5, Def5;

          consider k be Nat such that

           A25: ( len M4) = (k + 1) by A5, A21, NAT_1: 6;

          

           A26: P2[ 0 ] by A11, A7, Th7;

          

           A27: for k be Nat holds P2[k] from NAT_1:sch 2( A26, A14);

          defpred P2[ Nat] means (1 + $1) <= ( len Q1) implies (M /. ((( len Q0) + 1) + $1)) = (M4 /. (1 + $1));

           A28:

          now

            let k be Nat;

            assume

             A29: P2[k];

             0 <= (k + ( len Q0)) by NAT_1: 2;

            then

             A30: (((( len Q0) + 1) + k) + 1) = ((( len Q0) + 1) + (k + 1)) & 0 < ((( len Q0) + k) + 1);

            

             A31: 0 <= k by NAT_1: 2;

            now

              assume

               A32: (1 + (k + 1)) <= ( len Q1);

              then

               A33: ((Q0 ^ Q1) /. (( len Q0) + (1 + (k + 1)))) = (Q1 /. (1 + (k + 1))) by NAT_1: 11, SEQ_4: 136;

              reconsider kk = k as Element of NAT by ORDINAL1:def 12;

              

               A34: (1 + k) < ( len Q1) by A32, NAT_1: 13;

              then (( len Q0) + (1 + k)) < (( len Q0) + ( len Q1)) by XREAL_1: 6;

              then ((( len Q0) + 1) + kk) < ( len (Q0 ^ Q1)) by FINSEQ_1: 22;

              then (M /. ((( len Q0) + 1) + (kk + 1))) = ( Firing ((Q1 /. (1 + (kk + 1))),(M4 /. (1 + kk)))) by A12, A30, A29, A32, A33, NAT_1: 13;

              hence (M /. ((( len Q0) + 1) + (k + 1))) = (M4 /. (1 + (k + 1))) by A24, A31, A34;

            end;

            hence P2[(k + 1)];

          end;

          ( len Q0) > 0 by A5, NAT_1: 3;

          

          then (M /. ((( len Q0) + 1) + 0 )) = ( Firing (((Q0 ^ Q1) /. (( len Q0) + 1)),(M /. (1 + m)))) by A12, A13

          .= ( Firing (((Q0 ^ Q1) /. (( len Q0) + 1)),( Firing (Q0,M0)))) by A6, A27

          .= (M4 /. (1 + 0 )) by A23, A20, SEQ_4: 136;

          then

           A35: P2[ 0 ];

          

           A36: for k be Nat holds P2[k] from NAT_1:sch 2( A35, A28);

          reconsider k as Element of NAT by ORDINAL1:def 12;

          (M /. ( len M)) = (M /. (( len Q0) + (1 + k))) by A9, A21, A25, FINSEQ_1: 22

          .= (M /. ((( len Q0) + 1) + k))

          .= (M4 /. ( len M4)) by A21, A36, A25;

          hence thesis by A10, A22;

        end;

      end;

      hence thesis;

    end;

    theorem :: BOOLMARK:9

    

     Th9: for PTN be Petri_net, M0 be Boolean_marking of PTN, Q0,Q1 be FinSequence of the carrier' of PTN st (Q0 ^ Q1) is_firable_on M0 holds Q1 is_firable_on ( Firing (Q0,M0)) & Q0 is_firable_on M0

    proof

      let PTN be Petri_net;

      let M0 be Boolean_marking of PTN;

      let Q0,Q1 be FinSequence of the carrier' of PTN;

      assume

       A1: (Q0 ^ Q1) is_firable_on M0;

      now

        per cases ;

          case Q0 = {} & Q1 = {} ;

          hence thesis;

        end;

          case

           A2: Q0 = {} & Q1 <> {} ;

          hence Q0 is_firable_on M0;

          (Q0 ^ Q1) = Q1 by A2, FINSEQ_1: 34;

          hence Q1 is_firable_on ( Firing (Q0,M0)) by A1, A2, Def5;

        end;

          case

           A3: Q0 <> {} & Q1 = {} ;

          hence Q1 is_firable_on ( Firing (Q0,M0));

          thus Q0 is_firable_on M0 by A1, A3, FINSEQ_1: 34;

        end;

          case

           A4: Q0 <> {} & Q1 <> {} ;

          let i be Element of NAT ;

          ( len Q1) > 0 by A4, NAT_1: 3;

          then

           A5: ( 0 + 1) <= ( len Q1) by NAT_1: 13;

          then

           A6: (Q1 /. 1) = ((Q0 ^ Q1) /. (( len Q0) + 1)) by SEQ_4: 136;

          reconsider m = (( len Q0) - 1) as Element of NAT by A4, NAT_1: 3, NAT_1: 20;

          consider M4 be FinSequence of ( Bool_marks_of PTN) such that

           A7: ( len Q1) = ( len M4) and ( Firing (Q1,( Firing (Q0,M0)))) = (M4 /. ( len M4)) and

           A8: (M4 /. 1) = ( Firing ((Q1 /. 1),( Firing (Q0,M0)))) and

           A9: for i be Nat st i < ( len Q1) & i > 0 holds (M4 /. (i + 1)) = ( Firing ((Q1 /. (i + 1)),(M4 /. i))) by A4, Def5;

          consider M3 be FinSequence of ( Bool_marks_of PTN) such that

           A10: ( len Q0) = ( len M3) and

           A11: ( Firing (Q0,M0)) = (M3 /. ( len M3)) and

           A12: (M3 /. 1) = ( Firing ((Q0 /. 1),M0)) and

           A13: for i be Nat st i < ( len Q0) & i > 0 holds (M3 /. (i + 1)) = ( Firing ((Q0 /. (i + 1)),(M3 /. i))) by A4, Def5;

          consider j be Nat such that

           A14: ( len M3) = (j + 1) by A4, A10, NAT_1: 6;

          reconsider j as Element of NAT by ORDINAL1:def 12;

          consider M be FinSequence of ( Bool_marks_of PTN) such that ( len (Q0 ^ Q1)) = ( len M) and

           A15: ((Q0 ^ Q1) /. 1) is_firable_on M0 and

           A16: (M /. 1) = ( Firing (((Q0 ^ Q1) /. 1),M0)) and

           A17: for i be Element of NAT st i < ( len (Q0 ^ Q1)) & i > 0 holds ((Q0 ^ Q1) /. (i + 1)) is_firable_on (M /. i) & (M /. (i + 1)) = ( Firing (((Q0 ^ Q1) /. (i + 1)),(M /. i))) by A1, A4;

          defpred P2[ Nat] means (1 + $1) <= ( len Q0) implies (M /. (1 + $1)) = (M3 /. (1 + $1));

           0 < ( len Q1) by A4, NAT_1: 3;

          then ( 0 + ( len Q0)) < (( len Q0) + ( len Q1)) by XREAL_1: 6;

          then

           A18: ( len Q0) < ( len (Q0 ^ Q1)) by FINSEQ_1: 22;

           A19:

          now

            let k be Nat;

            

             A20: 0 <= k by NAT_1: 2;

            assume

             A21: P2[k];

            now

              assume

               A22: (1 + (k + 1)) <= ( len Q0);

              then

               A23: ((Q0 ^ Q1) /. (1 + (k + 1))) = (Q0 /. (1 + (k + 1))) by Th7, NAT_1: 11;

              

               A24: (1 + k) < ( len Q0) by A22, NAT_1: 13;

              then (1 + k) < ( len (Q0 ^ Q1)) by A18, XXREAL_0: 2;

              then (M /. (1 + (k + 1))) = ( Firing ((Q0 /. (1 + (k + 1))),(M3 /. (1 + k)))) by A17, A20, A21, A22, A23, NAT_1: 13;

              hence (M /. (1 + (k + 1))) = (M3 /. (1 + (k + 1))) by A13, A20, A24;

            end;

            hence P2[(k + 1)];

          end;

          

           A25: P2[ 0 ] by A16, A12, Th7;

          

           A26: for k be Nat holds P2[k] from NAT_1:sch 2( A25, A19);

           A27:

          now

            let i be Element of NAT ;

            assume that

             A28: i < ( len Q0) and

             A29: i > 0 ;

            consider j be Nat such that

             A30: i = (j + 1) by A29, NAT_1: 6;

            (i + 1) >= 1 & (i + 1) <= ( len Q0) by A28, NAT_1: 11, NAT_1: 13;

            then (i + 1) in ( dom Q0) by FINSEQ_3: 25;

            then

             A31: ((Q0 ^ Q1) /. (i + 1)) = (Q0 /. (i + 1)) by FINSEQ_4: 68;

            reconsider j as Element of NAT by ORDINAL1:def 12;

            i = (j + 1) by A30;

            then

             A32: (M /. i) = (M3 /. i) by A26, A28;

            

             A33: (i + 1) <= ( len Q0) by A28, NAT_1: 13;

            

             A34: i < ( len (Q0 ^ Q1)) by A18, A28, XXREAL_0: 2;

            then (M /. (i + 1)) = ( Firing (((Q0 ^ Q1) /. (i + 1)),(M /. i))) by A17, A29;

            hence (Q0 /. (i + 1)) is_firable_on (M3 /. i) & (M3 /. (i + 1)) = ( Firing ((Q0 /. (i + 1)),(M3 /. i))) by A17, A26, A29, A34, A31, A32, A33;

          end;

          defpred P2[ Nat] means (1 + $1) <= ( len Q1) implies (M /. ((( len Q0) + 1) + $1)) = (M4 /. (1 + $1));

           A35:

          now

            let k be Nat;

            assume

             A36: P2[k];

             0 <= (k + ( len Q0)) by NAT_1: 2;

            then

             A37: (((( len Q0) + 1) + k) + 1) = ((( len Q0) + 1) + (k + 1)) & 0 < ((( len Q0) + k) + 1);

            

             A38: 0 <= k by NAT_1: 2;

            now

              assume

               A39: (1 + (k + 1)) <= ( len Q1);

              then

               A40: ((Q0 ^ Q1) /. (( len Q0) + (1 + (k + 1)))) = (Q1 /. (1 + (k + 1))) by NAT_1: 11, SEQ_4: 136;

              reconsider kk = k as Element of NAT by ORDINAL1:def 12;

              

               A41: (1 + k) < ( len Q1) by A39, NAT_1: 13;

              then (( len Q0) + (1 + k)) < (( len Q0) + ( len Q1)) by XREAL_1: 6;

              then ((( len Q0) + 1) + kk) < ( len (Q0 ^ Q1)) by FINSEQ_1: 22;

              then (M /. ((( len Q0) + 1) + (kk + 1))) = ( Firing ((Q1 /. (1 + (kk + 1))),(M4 /. (1 + kk)))) by A17, A37, A36, A39, A40, NAT_1: 13;

              hence (M /. ((( len Q0) + 1) + (k + 1))) = (M4 /. (1 + (k + 1))) by A9, A38, A41;

            end;

            hence P2[(k + 1)];

          end;

          

           A42: ( len Q0) > 0 by A4, NAT_1: 3;

          

          then (M /. ((( len Q0) + 1) + 0 )) = ( Firing (((Q0 ^ Q1) /. (( len Q0) + 1)),(M /. (1 + m)))) by A17, A18

          .= ( Firing (((Q0 ^ Q1) /. (( len Q0) + 1)),( Firing (Q0,M0)))) by A10, A11, A26

          .= (M4 /. (1 + 0 )) by A8, A5, SEQ_4: 136;

          then

           A43: P2[ 0 ];

          

           A44: for k be Nat holds P2[k] from NAT_1:sch 2( A43, A35);

           A45:

          now

            let i be Element of NAT such that

             A46: i < ( len Q1) and

             A47: i > 0 ;

            consider j be Nat such that

             A48: i = (j + 1) by A47, NAT_1: 6;

            reconsider j as Element of NAT by ORDINAL1:def 12;

            ((( len Q0) + 1) + j) = (( len Q0) + (j + 1));

            then

             A49: (M /. (( len Q0) + i)) = (M4 /. i) by A44, A46, A48;

            (i + 1) >= 1 & (i + 1) <= ( len Q1) by A46, NAT_1: 11, NAT_1: 13;

            then

             A50: (i + 1) in ( dom Q1) by FINSEQ_3: 25;

            

             A51: ((Q0 ^ Q1) /. ((( len Q0) + i) + 1)) = ((Q0 ^ Q1) /. (( len Q0) + (i + 1)))

            .= (Q1 /. (i + 1)) by A50, FINSEQ_4: 69;

            

             A52: ((( len Q0) + 1) + i) = ((( len Q0) + i) + 1) & (i + 1) <= ( len Q1) by A46, NAT_1: 13;

            ( len (Q0 ^ Q1)) = (( len Q0) + ( len Q1)) by FINSEQ_1: 22;

            then

             A53: (( len Q0) + i) < ( len (Q0 ^ Q1)) by A46, XREAL_1: 6;

            

             A54: i < (( len Q0) + i) by A4, NAT_1: 3, XREAL_1: 29;

            then (M /. ((( len Q0) + i) + 1)) = ( Firing (((Q0 ^ Q1) /. ((( len Q0) + i) + 1)),(M /. (( len Q0) + i)))) by A17, A47, A53;

            hence (Q1 /. (i + 1)) is_firable_on (M4 /. i) & (M4 /. (i + 1)) = ( Firing ((Q1 /. (i + 1)),(M4 /. i))) by A17, A44, A47, A53, A54, A51, A49, A52;

          end;

          ( len M3) = (j + 1) by A14;

          then (M /. ( len M3)) = (M3 /. ( len M3)) by A10, A26;

          then (Q1 /. 1) is_firable_on (M3 /. ( len M3)) by A17, A10, A42, A18, A6;

          hence Q1 is_firable_on ( Firing (Q0,M0)) by A11, A7, A8, A45;

          ( 0 + 1) <= ( len Q0) by A42, NAT_1: 13;

          then (Q0 /. 1) is_firable_on M0 by A15, Th7;

          hence Q0 is_firable_on M0 by A10, A12, A27;

        end;

      end;

      hence thesis;

    end;

    theorem :: BOOLMARK:10

    

     Th10: for PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN holds t is_firable_on M0 iff <*t*> is_firable_on M0

    proof

      let PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN;

      hereby

        set M = <*( Firing (( <*t*> /. 1),M0))*>;

        

         A1: (M /. 1) = ( Firing (( <*t*> /. 1),M0)) by FINSEQ_4: 16;

         A2:

        now

          

           A3: ( len <*t*>) = ( 0 + 1) by FINSEQ_1: 39;

          let i be Element of NAT ;

          assume i < ( len <*t*>) & i > 0 ;

          hence ( <*t*> /. (i + 1)) is_firable_on (M /. i) & (M /. (i + 1)) = ( Firing (( <*t*> /. (i + 1)),(M /. i))) by A3, NAT_1: 13;

        end;

        assume t is_firable_on M0;

        then

         A4: ( <*t*> /. 1) is_firable_on M0 by FINSEQ_4: 16;

        ( len <*t*>) = 1 by FINSEQ_1: 39

        .= ( len M) by FINSEQ_1: 39;

        hence <*t*> is_firable_on M0 by A4, A1, A2;

      end;

      assume <*t*> is_firable_on M0;

      then ex M be FinSequence of ( Bool_marks_of PTN) st ( len <*t*>) = ( len M) & ( <*t*> /. 1) is_firable_on M0 & (M /. 1) = ( Firing (( <*t*> /. 1),M0)) & for i be Element of NAT st i < ( len <*t*>) & i > 0 holds ( <*t*> /. (i + 1)) is_firable_on (M /. i) & (M /. (i + 1)) = ( Firing (( <*t*> /. (i + 1)),(M /. i)));

      hence thesis by FINSEQ_4: 16;

    end;

    theorem :: BOOLMARK:11

    

     Th11: for PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN holds ( Firing (t,M0)) = ( Firing ( <*t*>,M0))

    proof

      let PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN;

      set M = <*( Firing (( <*t*> /. 1),M0))*>;

      

       A1: ( len <*t*>) = 1 & ( <*t*> /. 1) = t by FINSEQ_1: 39, FINSEQ_4: 16;

      

       A2: (M /. 1) = ( Firing (( <*t*> /. 1),M0)) by FINSEQ_4: 16;

       A3:

      now

        

         A4: ( len <*t*>) = ( 0 + 1) by FINSEQ_1: 39;

        let i be Nat;

        assume i < ( len <*t*>) & i > 0 ;

        hence (M /. (i + 1)) = ( Firing (( <*t*> /. (i + 1)),(M /. i))) by A4, NAT_1: 13;

      end;

      ( len <*t*>) = 1 by FINSEQ_1: 39

      .= ( len M) by FINSEQ_1: 39;

      hence thesis by A1, A2, A3, Def5;

    end;

    theorem :: BOOLMARK:12

    for PTN be Petri_net, Sd be non empty Subset of the carrier of PTN holds Sd is Deadlock-like iff for M0 be Boolean_marking of PTN st (M0 .: Sd) = { FALSE } holds for Q be FinSequence of the carrier' of PTN st Q is_firable_on M0 holds (( Firing (Q,M0)) .: Sd) = { FALSE }

    proof

      let PTN be Petri_net, Sd be non empty Subset of the carrier of PTN;

      set M0 = ((the carrier of PTN --> TRUE ) qua Function +* (Sd --> FALSE ));

      

       A1: ( [#] the carrier of PTN) = the carrier of PTN;

      ( dom (the carrier of PTN --> TRUE ) qua Function) = the carrier of PTN & ( dom (Sd --> FALSE )) = Sd by FUNCOP_1: 13;

      

      then

       A2: ( dom M0) = (the carrier of PTN \/ Sd) by FUNCT_4:def 1

      .= the carrier of PTN by A1, SUBSET_1: 11;

      ( rng (Sd --> FALSE )) c= { FALSE } by FUNCOP_1: 13;

      then

       A3: ( rng (Sd --> FALSE )) c= BOOLEAN by XBOOLE_1: 1;

      thus Sd is Deadlock-like implies for M0 be Boolean_marking of PTN st (M0 .: Sd) = { FALSE } holds for Q be FinSequence of the carrier' of PTN st Q is_firable_on M0 holds (( Firing (Q,M0)) .: Sd) = { FALSE }

      proof

        assume

         A4: Sd is Deadlock-like;

        let M0 be Boolean_marking of PTN such that

         A5: (M0 .: Sd) = { FALSE };

        defpred P[ FinSequence of the carrier' of PTN] means $1 is_firable_on M0 implies (( Firing ($1,M0)) .: Sd) = { FALSE };

        

         A6: ( *' Sd) is Subset of (Sd *' ) by A4;

         A7:

        now

          let Q be FinSequence of the carrier' of PTN;

          let x be transition of PTN;

          assume

           A8: P[Q];

          thus P[(Q ^ <*x*>)]

          proof

            ( Firing ((Q ^ <*x*>),M0)) = ( Firing ( <*x*>,( Firing (Q,M0)))) by Th8;

            then

             A9: ex M be FinSequence of ( Bool_marks_of PTN) st ( len <*x*>) = ( len M) & ( Firing ((Q ^ <*x*>),M0)) = (M /. ( len M)) & (M /. 1) = ( Firing (( <*x*> /. 1),( Firing (Q,M0)))) & for i be Nat st i < ( len <*x*>) & i > 0 holds (M /. (i + 1)) = ( Firing (( <*x*> /. (i + 1)),(M /. i))) by Def5;

            ( <*x*> /. 1) = x by FINSEQ_4: 16;

            then

             A10: ( Firing ((Q ^ <*x*>),M0)) = ((( Firing (Q,M0)) +* (( *' {x}) --> FALSE )) +* (( {x} *' ) --> TRUE )) by A9, FINSEQ_1: 39;

            assume

             A11: (Q ^ <*x*>) is_firable_on M0;

            then <*x*> is_firable_on ( Firing (Q,M0)) by Th9;

            then x is_firable_on ( Firing (Q,M0)) by Th10;

            then (( Firing (Q,M0)) .: ( *' {x})) c= { TRUE };

            then

             A12: (( Firing (Q,M0)) .: ( *' {x})) misses { FALSE } by XBOOLE_1: 63, ZFMISC_1: 11;

            then ( *' {x}) misses Sd by A8, A11, Th2, Th9;

            then not x in ( *' Sd) by A6, PETRI: 19;

            then ( {x} *' ) misses Sd by PETRI: 20;

            

            hence (( Firing ((Q ^ <*x*>),M0)) .: Sd) = ((( Firing (Q,M0)) +* (( *' {x}) --> FALSE )) .: Sd) by A10, Th3

            .= { FALSE } by A8, A11, A12, Th2, Th3, Th9;

          end;

        end;

        

         A13: P[( <*> the carrier' of PTN)] by A5, Def5;

        thus for Q0 be FinSequence of the carrier' of PTN holds P[Q0] from FINSEQ_2:sch 2( A13, A7);

      end;

      

       A14: ( rng M0) c= (( rng (the carrier of PTN --> TRUE )) \/ ( rng (Sd --> FALSE ))) by FUNCT_4: 17;

      ( rng (the carrier of PTN --> TRUE )) c= { TRUE } by FUNCOP_1: 13;

      then ( rng (the carrier of PTN --> TRUE )) c= BOOLEAN by XBOOLE_1: 1;

      then (( rng (the carrier of PTN --> TRUE )) \/ ( rng (Sd --> FALSE ))) c= BOOLEAN by A3, XBOOLE_1: 8;

      then ( rng M0) c= BOOLEAN by A14, XBOOLE_1: 1;

      then

      reconsider M0 as Boolean_marking of PTN by A2, FUNCT_2:def 2;

      assume

       A15: for M0 be Boolean_marking of PTN st (M0 .: Sd) = { FALSE } holds for Q be FinSequence of the carrier' of PTN st Q is_firable_on M0 holds (( Firing (Q,M0)) .: Sd) = { FALSE };

      assume not ( *' Sd) is Subset of (Sd *' );

      then

      consider t be transition of PTN such that

       A16: t in ( *' Sd) and

       A17: not t in (Sd *' ) by SUBSET_1: 2;

      Sd misses ( *' {t}) by A17, PETRI: 19;

      then

       A18: ((the carrier of PTN --> TRUE ) qua Function .: ( *' {t})) = (M0 .: ( *' {t})) by Th3;

      reconsider Q = <*t*> as FinSequence of the carrier' of PTN;

      ( {t} *' ) meets Sd by A16, PETRI: 20;

      then

      consider s be object such that

       A19: s in (( {t} *' ) /\ Sd) by XBOOLE_0: 4;

      s in ( {t} *' ) by A19, XBOOLE_0:def 4;

      then

       A20: (( Firing (t,M0)) . s) = TRUE by Th5;

      s in Sd by A19, XBOOLE_0:def 4;

      then TRUE in (( Firing (t,M0)) .: Sd) by A20, FUNCT_2: 35;

      then (( Firing (t,M0)) .: Sd) <> { FALSE } by TARSKI:def 1;

      then

       A21: (( Firing (Q,M0)) .: Sd) <> { FALSE } by Th11;

      ( rng (the carrier of PTN --> TRUE )) c= { TRUE } & ((the carrier of PTN --> TRUE ) .: ( *' {t})) c= ( rng (the carrier of PTN --> TRUE )) by FUNCOP_1: 13, RELAT_1: 111;

      then (M0 .: ( *' {t})) c= { TRUE } by A18, XBOOLE_1: 1;

      then t is_firable_on M0;

      then

       A22: Q is_firable_on M0 by Th10;

      (M0 .: Sd) = { FALSE qua set} by Th4;

      hence contradiction by A15, A22, A21;

    end;