:: BOOLMARK semantic presentation

begin

theorem :: BOOLMARK:1
for A, B being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) )
for C being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for v being ( ( ) ( ) Element of B : ( ( non empty ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) +* (C : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) --> v : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b4 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Element of K32(K33(b4 : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of A : ( ( non empty ) ( non empty ) set ) ,B : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: BOOLMARK:2
for X, Y being ( ( non empty ) ( non empty ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( non empty ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) set ) misses f : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like quasi_total ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) .: B : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
A : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) misses B : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;

theorem :: BOOLMARK:3
for A, B being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for x being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) holds
(f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) +* (A : ( ( ) ( ) set ) --> x : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b4 : ( ( ) ( ) set ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) -valued Function-like quasi_total ) Element of K32(K33(b1 : ( ( ) ( ) set ) ,{b4 : ( ( ) ( ) set ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: B : ( ( ) ( ) set ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: B : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

begin

definition
let PTN be ( ( ) ( ) PT_net_Str ) ;
func Bool_marks_of PTN -> ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) equals :: BOOLMARK:def 1
 Funcs ( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;
end;

definition
let PTN be ( ( ) ( ) PT_net_Str ) ;
mode Boolean_marking of PTN is ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let PTN be ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ;
let M0 be ( ( ) ( Relation-like the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;
let t be ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) ;
pred t is_firable_on M0 means :: BOOLMARK:def 2
M0 : ( ( ) ( ) set ) .: (*' {t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) c= {TRUE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;
end;

notation
let PTN be ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ;
let M0 be ( ( ) ( Relation-like the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;
let t be ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) ;
antonym t is_not_firable_on M0 for t is_firable_on M0;
end;

definition
let PTN be ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ;
let M0 be ( ( ) ( Relation-like the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;
let t be ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) ;
func Firing (t,M0) -> ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( ) ( ) 2-sorted ) ) equals :: BOOLMARK:def 3
(M0 : ( ( ) ( ) set ) +* ((*' {t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) --> FALSE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like *' {t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of K32(K33((*' {t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) +* (({t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) *') : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) --> TRUE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like {t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) *' : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of K32(K33(({t : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) *') : ( ( ) ( ) Element of K32( the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;
end;

definition
let PTN be ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ;
let M0 be ( ( ) ( Relation-like the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;
let Q be ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ;
pred Q is_firable_on M0 means :: BOOLMARK:def 4
( Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) = {} : ( ( ) ( ) set ) or ex M being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) st
( len Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) /. 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) is_firable_on M0 : ( ( ) ( ) set ) & M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) = Firing ((Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) /. 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ,M0 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( ) ( ) 2-sorted ) ) & ( for i being ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < len Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
( Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) /. (i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) is_firable_on M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) & M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. (i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) = Firing ((Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) /. (i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ,(M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( ) ( ) 2-sorted ) ) ) ) ) );
end;

notation
let PTN be ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ;
let M0 be ( ( ) ( Relation-like the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;
let Q be ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ;
antonym Q is_not_firable_on M0 for Q is_firable_on M0;
end;

definition
let PTN be ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ;
let M0 be ( ( ) ( Relation-like the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;
let Q be ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ;
func Firing (Q,M0) -> ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( ) ( ) 2-sorted ) ) means :: BOOLMARK:def 5
it : ( ( ) ( Relation-like M0 : ( ( ) ( ) set ) -defined PTN : ( ( ) ( ) 2-sorted ) -valued ) Element of K32(K33(M0 : ( ( ) ( ) set ) ,PTN : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = M0 : ( ( ) ( ) set ) if Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) = {} : ( ( ) ( ) set )
otherwise ex M being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) st
( len Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & it : ( ( ) ( Relation-like M0 : ( ( ) ( ) set ) -defined PTN : ( ( ) ( ) 2-sorted ) -valued ) Element of K32(K33(M0 : ( ( ) ( ) set ) ,PTN : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. (len M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) & M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) = Firing ((Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) /. 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ,M0 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( ) ( ) 2-sorted ) ) & ( for i being ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < len Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. (i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) = Firing ((Q : ( ( ) ( ) Element of PTN : ( ( ) ( ) 2-sorted ) ) /. (i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier' of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ,(M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of Bool_marks_of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) /. i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of Bool_marks_of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( non empty ) FUNCTION_DOMAIN of the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like the carrier of PTN : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( ) ( ) 2-sorted ) ) ) );
end;

theorem :: BOOLMARK:4
for A being ( ( non empty ) ( non empty ) set )
for y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) +* (A : ( ( non empty ) ( non empty ) set ) --> y : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) -valued Function-like quasi_total ) Element of K32(K33(b1 : ( ( non empty ) ( non empty ) set ) ,{b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) = {y : ( ( ) ( ) set ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) set ) ;

theorem :: BOOLMARK:5
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) )
for t being ( ( ) ( ) transition of ( ( ) ( non empty ) set ) )
for s being ( ( ) ( ) place of ( ( ) ( non empty ) set ) ) st s : ( ( ) ( ) place of ( ( ) ( non empty ) set ) ) in {t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32( the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) *' : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
(Firing (t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) )) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) . s : ( ( ) ( ) place of ( ( ) ( non empty ) set ) ) : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) = TRUE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BOOLMARK:6
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for Sd being ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) holds
( Sd : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) is Deadlock-like iff for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) st M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) .: Sd : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = {FALSE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
for t being ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) st t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) is_firable_on M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) holds
(Firing (t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) )) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) .: Sd : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = {FALSE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: BOOLMARK:7
for D being ( ( non empty ) ( non empty ) set )
for Q0, Q1 being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for i being ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) st 1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= len Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^ Q1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) /. i : ( ( ) ( V21() V22() V23() V24() V28() V29() ext-real V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: BOOLMARK:8
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) )
for Q0, Q1 being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) holds Firing ((Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ^ Q1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) = Firing (Q1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ,(Firing (Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) )) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;

theorem :: BOOLMARK:9
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) )
for Q0, Q1 being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) st Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ^ Q1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) is_firable_on M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) holds
( Q1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) is_firable_on Firing (Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) & Q0 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) is_firable_on M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) ;

theorem :: BOOLMARK:10
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) )
for t being ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) holds
( t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) is_firable_on M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) iff <*t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( non empty V5() Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) is_firable_on M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) ;

theorem :: BOOLMARK:11
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) )
for t being ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) holds Firing (t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) = Firing (<*t : ( ( ) ( ) transition of ( ( ) ( non empty ) set ) ) *> : ( ( ) ( non empty V5() Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) ;

theorem :: BOOLMARK:12
for PTN being ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net)
for Sd being ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) holds
( Sd : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) is Deadlock-like iff for M0 being ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) st M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) .: Sd : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = {FALSE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
for Q being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of PTN : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) st Q : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) is_firable_on M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) holds
(Firing (Q : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like ) FinSequence of the carrier' of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) ) ,M0 : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) )) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) : ( ( ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Boolean_marking of b1 : ( ( non empty non void with_S-T_arc with_T-S_arc ) ( non empty non void V70() with_S-T_arc with_T-S_arc ) Petri_net) ) .: Sd : ( ( non empty ) ( non empty ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = {FALSE : ( ( ) ( boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty V5() V42(1 : ( ( ) ( non empty V21() V22() V23() V24() V28() V29() ext-real positive non negative V35() V40() ) Element of NAT : ( ( ) ( non empty V22() V23() V24() V35() V40() V41() ) Element of K32(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ) Element of K32(BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;