:: BOOLMARK semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: BOOLMARK:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for f being Function of A,B
for C being Subset of A
for v being Element of B holds f +* (C --> v) is Function of A,B
proof end;

theorem Th2: :: BOOLMARK:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty set
for A, B being Subset of X
for f being Function of X,Y st f .: A misses f .: B holds
A misses B
proof end;

theorem Th3: :: BOOLMARK:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set
for f being Function
for x being set st A misses B holds
(f +* (A --> x)) .: B = f .: B
proof end;

definition
let PTN be PT_net_Str ;
func Bool_marks_of PTN -> FUNCTION_DOMAIN of the Places of PTN, BOOLEAN equals :: BOOLMARK:def 1
 Funcs the Places of PTN,BOOLEAN ;
correctness
coherence
Funcs the Places of PTN,BOOLEAN is FUNCTION_DOMAIN of the Places of PTN, BOOLEAN ;
;
end;

:: deftheorem defines Bool_marks_of BOOLMARK:def 1 :
for PTN being PT_net_Str holds Bool_marks_of PTN = Funcs the Places of PTN,BOOLEAN ;

definition
let PTN be PT_net_Str ;
mode Boolean_marking of PTN is Element of Bool_marks_of PTN;
end;

definition
let PTN be PT_net_Str ;
let M0 be Boolean_marking of PTN;
let t be transition of PTN;
pred t is_firable_on M0 means :Def2: :: BOOLMARK:def 2
M0 .: (*' {t}) c= {TRUE };
end;

:: deftheorem Def2 defines is_firable_on BOOLMARK:def 2 :
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for t being transition of PTN holds
( t is_firable_on M0 iff M0 .: (*' {t}) c= {TRUE } );

notation
let PTN be PT_net_Str ;
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 PT_net_Str ;
let M0 be Boolean_marking of PTN;
let t be transition of PTN;
func Firing t,M0 -> Boolean_marking of PTN equals :: BOOLMARK:def 3
(M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE );
coherence
(M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE ) is Boolean_marking of PTN
proof end;
correctness
;
end;

:: deftheorem defines Firing BOOLMARK:def 3 :
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for t being transition of PTN holds Firing t,M0 = (M0 +* ((*' {t}) --> FALSE )) +* (({t} *' ) --> TRUE );

definition
let PTN be PT_net_Str ;
let M0 be Boolean_marking of PTN;
let Q be FinSequence of the Transitions of PTN;
pred Q is_firable_on M0 means :Def4: :: BOOLMARK:def 4
( Q = {} or ex M being 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 being 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;

:: deftheorem Def4 defines is_firable_on BOOLMARK:def 4 :
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for Q being FinSequence of the Transitions of PTN holds
( Q is_firable_on M0 iff ( Q = {} or ex M being 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 being 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) ) ) ) ) );

notation
let PTN be PT_net_Str ;
let M0 be Boolean_marking of PTN;
let Q be FinSequence of the Transitions of PTN;
antonym Q is_not_firable_on M0 for Q is_firable_on M0;
end;

definition
let PTN be PT_net_Str ;
let M0 be Boolean_marking of PTN;
let Q be FinSequence of the Transitions of PTN;
func Firing Q,M0 -> Boolean_marking of PTN means :Def5: :: BOOLMARK:def 5
it = M0 if Q = {}
otherwise ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & it = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) );
existence
( ( Q = {} implies ex b1 being Boolean_marking of PTN st b1 = M0 ) & ( not Q = {} implies ex b1 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) ) )
proof end;
uniqueness
for b1, b2 being Boolean_marking of PTN holds
( ( Q = {} & b1 = M0 & b2 = M0 implies b1 = b2 ) & ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b2 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Boolean_marking of PTN holds verum;
;
end;

:: deftheorem Def5 defines Firing BOOLMARK:def 5 :
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for Q being FinSequence of the Transitions of PTN
for b4 being Boolean_marking of PTN holds
( ( Q = {} implies ( b4 = Firing Q,M0 iff b4 = M0 ) ) & ( not Q = {} implies ( b4 = Firing Q,M0 iff ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b4 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) ) ) );

theorem :: BOOLMARK:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: BOOLMARK:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for y being set
for f being Function holds (f +* (A --> y)) .: A = {y}
proof end;

theorem Th6: :: BOOLMARK:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for t being transition of PTN
for s being place of PTN st s in {t} *' holds
(Firing t,M0) . s = TRUE
proof end;

Lm1: now
let PTN be PT_net_Str ; :: thesis: for Sd being non empty Subset of the Places of PTN st ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for t being transition of PTN st t is_firable_on M0 holds
(Firing t,M0) .: Sd = {FALSE } ) holds
Sd is Deadlock-like
let Sd be non empty Subset of the Places of PTN; :: thesis: ( ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for t being transition of PTN st t is_firable_on M0 holds
(Firing t,M0) .: Sd = {FALSE } ) implies Sd is Deadlock-like )
assume A1: for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for t being transition of PTN st t is_firable_on M0 holds
(Firing t,M0) .: Sd = {FALSE } ; :: thesis: Sd is Deadlock-like
assume not Sd is Deadlock-like ; :: thesis: contradiction
then not *' Sd c= Sd *' by PETRI:def 5;
then consider t being transition of PTN such that
A2: t in *' Sd and
A3: not t in Sd *' by SUBSET_1:7;
set M0 = (the Places of PTN --> TRUE ) +* (Sd --> FALSE );
A4: [#] the Places of PTN = the Places of PTN by SUBSET_1:def 4;
( dom (the Places of PTN --> TRUE ) = the Places of PTN & dom (Sd --> FALSE ) = Sd ) by FUNCOP_1:19;
then A5: dom ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) = the Places of PTN \/ Sd by FUNCT_4:def 1
.= the Places of PTN by A4, SUBSET_1:28 ;
( rng (the Places of PTN --> TRUE ) c= {TRUE } & rng (Sd --> FALSE ) c= {FALSE } ) by FUNCOP_1:19;
then ( rng (the Places of PTN --> TRUE ) c= BOOLEAN & rng (Sd --> FALSE ) c= BOOLEAN ) by XBOOLE_1:1;
then A6: (rng (the Places of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) c= BOOLEAN by XBOOLE_1:8;
rng ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) c= (rng (the Places of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) by FUNCT_4:18;
then rng ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) c= BOOLEAN by A6, XBOOLE_1:1;
then (the Places of PTN --> TRUE ) +* (Sd --> FALSE ) in Funcs the Places of PTN,BOOLEAN by A5, FUNCT_2:def 2;
then reconsider M0 = (the Places of PTN --> TRUE ) +* (Sd --> FALSE ) as Boolean_marking of PTN ;
A7: M0 .: Sd = {FALSE } by Th5;
Sd misses *' {t} by A3, PETRI:19;
then A8: (the Places of PTN --> TRUE ) .: (*' {t}) = M0 .: (*' {t}) by Th3;
A9: rng (the Places of PTN --> TRUE ) c= {TRUE } by FUNCOP_1:19;
(the Places of PTN --> TRUE ) .: (*' {t}) c= rng (the Places of PTN --> TRUE ) by RELAT_1:144;
then M0 .: (*' {t}) c= {TRUE } by A8, A9, XBOOLE_1:1;
then A10: t is_firable_on M0 by Def2;
{t} *' meets Sd by A2, PETRI:20;
then consider s being set such that
A11: s in ({t} *' ) /\ Sd by XBOOLE_0:4;
A12: ( s in {t} *' & s in Sd ) by A11, XBOOLE_0:def 3;
then (Firing t,M0) . s = TRUE by Th6;
then TRUE in (Firing t,M0) .: Sd by A12, FUNCT_2:43;
then (Firing t,M0) .: Sd <> {FALSE } by MARGREL1:38, TARSKI:def 1;
hence contradiction by A1, A7, A10; :: thesis: verum
end;

theorem :: BOOLMARK:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for Sd being non empty Subset of the Places of PTN holds
( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for t being transition of PTN st t is_firable_on M0 holds
(Firing t,M0) .: Sd = {FALSE } )
proof end;

theorem Th8: :: BOOLMARK:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for Q0, Q1 being FinSequence of D
for i being Nat st 1 <= i & i <= len Q0 holds
(Q0 ^ Q1) /. i = Q0 /. i
proof end;

theorem :: BOOLMARK:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: BOOLMARK:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for Q0, Q1 being FinSequence of the Transitions of PTN holds Firing (Q0 ^ Q1),M0 = Firing Q1,(Firing Q0,M0)
proof end;

theorem Th11: :: BOOLMARK:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for Q0, Q1 being FinSequence of the Transitions of PTN st Q0 ^ Q1 is_firable_on M0 holds
( Q1 is_firable_on Firing Q0,M0 & Q0 is_firable_on M0 )
proof end;

theorem Th12: :: BOOLMARK:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for t being transition of PTN holds
( t is_firable_on M0 iff <*t*> is_firable_on M0 )
proof end;

theorem Th13: :: BOOLMARK:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for M0 being Boolean_marking of PTN
for t being transition of PTN holds Firing t,M0 = Firing <*t*>,M0
proof end;

theorem :: BOOLMARK:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PTN being PT_net_Str
for Sd being non empty Subset of the Places of PTN holds
( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the Transitions of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } )
proof end;