:: BOOLMARK semantic presentation

theorem Th1: :: BOOLMARK:1
for b1, b2 being non empty set
for b3 being Function of b1,b2
for b4 being Subset of b1
for b5 being Element of b2 holds b3 +* (b4 --> b5) is Function of b1,b2
proof end;

theorem Th2: :: BOOLMARK:2
for b1, b2 being non empty set
for b3, b4 being Subset of b1
for b5 being Function of b1,b2 st b5 .: b3 misses b5 .: b4 holds
b3 misses b4
proof end;

theorem Th3: :: BOOLMARK:3
for b1, b2 being set
for b3 being Function
for b4 being set st b1 misses b2 holds
(b3 +* (b1 --> b4)) .: b2 = b3 .: b2
proof end;

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

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

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

definition
let c1 be PT_net_Str ;
let c2 be Boolean_marking of c1;
let c3 be transition of c1;
pred c3 is_firable_on c2 means :Def2: :: BOOLMARK:def 2
a2 .: (*' {a3}) c= {TRUE };
end;

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

notation
let c1 be PT_net_Str ;
let c2 be Boolean_marking of c1;
let c3 be transition of c1;
antonym c3 is_not_firable_on c2 for c3 is_firable_on c2;
end;

definition
let c1 be PT_net_Str ;
let c2 be Boolean_marking of c1;
let c3 be transition of c1;
func Firing c3,c2 -> Boolean_marking of a1 equals :: BOOLMARK:def 3
(a2 +* ((*' {a3}) --> FALSE )) +* (({a3} *' ) --> TRUE );
coherence
(c2 +* ((*' {c3}) --> FALSE )) +* (({c3} *' ) --> TRUE ) is Boolean_marking of c1
proof end;
correctness
;
end;

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

definition
let c1 be PT_net_Str ;
let c2 be Boolean_marking of c1;
let c3 be FinSequence of the Transitions of c1;
pred c3 is_firable_on c2 means :Def4: :: BOOLMARK:def 4
( a3 = {} or ex b1 being FinSequence of Bool_marks_of a1 st
( len a3 = len b1 & a3 /. 1 is_firable_on a2 & b1 /. 1 = Firing (a3 /. 1),a2 & ( for b2 being Nat st b2 < len a3 & b2 > 0 holds
( a3 /. (b2 + 1) is_firable_on b1 /. b2 & b1 /. (b2 + 1) = Firing (a3 /. (b2 + 1)),(b1 /. b2) ) ) ) );
end;

:: deftheorem Def4 defines is_firable_on BOOLMARK:def 4 :
for b1 being PT_net_Str
for b2 being Boolean_marking of b1
for b3 being FinSequence of the Transitions of b1 holds
( b3 is_firable_on b2 iff ( b3 = {} or ex b4 being FinSequence of Bool_marks_of b1 st
( len b3 = len b4 & b3 /. 1 is_firable_on b2 & b4 /. 1 = Firing (b3 /. 1),b2 & ( for b5 being Nat st b5 < len b3 & b5 > 0 holds
( b3 /. (b5 + 1) is_firable_on b4 /. b5 & b4 /. (b5 + 1) = Firing (b3 /. (b5 + 1)),(b4 /. b5) ) ) ) ) );

notation
let c1 be PT_net_Str ;
let c2 be Boolean_marking of c1;
let c3 be FinSequence of the Transitions of c1;
antonym c3 is_not_firable_on c2 for c3 is_firable_on c2;
end;

definition
let c1 be PT_net_Str ;
let c2 be Boolean_marking of c1;
let c3 be FinSequence of the Transitions of c1;
func Firing c3,c2 -> Boolean_marking of a1 means :Def5: :: BOOLMARK:def 5
a4 = a2 if a3 = {}
otherwise ex b1 being FinSequence of Bool_marks_of a1 st
( len a3 = len b1 & a4 = b1 /. (len b1) & b1 /. 1 = Firing (a3 /. 1),a2 & ( for b2 being Nat st b2 < len a3 & b2 > 0 holds
b1 /. (b2 + 1) = Firing (a3 /. (b2 + 1)),(b1 /. b2) ) );
existence
( ( c3 = {} implies ex b1 being Boolean_marking of c1 st b1 = c2 ) & ( not c3 = {} implies ex b1 being Boolean_marking of c1ex b2 being FinSequence of Bool_marks_of c1 st
( len c3 = len b2 & b1 = b2 /. (len b2) & b2 /. 1 = Firing (c3 /. 1),c2 & ( for b3 being Nat st b3 < len c3 & b3 > 0 holds
b2 /. (b3 + 1) = Firing (c3 /. (b3 + 1)),(b2 /. b3) ) ) ) )
proof end;
uniqueness
for b1, b2 being Boolean_marking of c1 holds
( ( c3 = {} & b1 = c2 & b2 = c2 implies b1 = b2 ) & ( not c3 = {} & ex b3 being FinSequence of Bool_marks_of c1 st
( len c3 = len b3 & b1 = b3 /. (len b3) & b3 /. 1 = Firing (c3 /. 1),c2 & ( for b4 being Nat st b4 < len c3 & b4 > 0 holds
b3 /. (b4 + 1) = Firing (c3 /. (b4 + 1)),(b3 /. b4) ) ) & ex b3 being FinSequence of Bool_marks_of c1 st
( len c3 = len b3 & b2 = b3 /. (len b3) & b3 /. 1 = Firing (c3 /. 1),c2 & ( for b4 being Nat st b4 < len c3 & b4 > 0 holds
b3 /. (b4 + 1) = Firing (c3 /. (b4 + 1)),(b3 /. b4) ) ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Boolean_marking of c1 holds verum;
;
end;

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

theorem Th4: :: BOOLMARK:4
canceled;

theorem Th5: :: BOOLMARK:5
for b1 being non empty set
for b2 being set
for b3 being Function holds (b3 +* (b1 --> b2)) .: b1 = {b2}
proof end;

theorem Th6: :: BOOLMARK:6
for b1 being PT_net_Str
for b2 being Boolean_marking of b1
for b3 being transition of b1
for b4 being place of b1 st b4 in {b3} *' holds
(Firing b3,b2) . b4 = TRUE
proof end;

E9: now
let c1 be PT_net_Str ;
let c2 be non empty Subset of the Places of c1;
assume E10: for b1 being Boolean_marking of c1 st b1 .: c2 = {FALSE } holds
for b2 being transition of c1 st b2 is_firable_on b1 holds
(Firing b2,b1) .: c2 = {FALSE } ;
assume not c2 is Deadlock-like ;
then not *' c2 c= c2 *' by PETRI:def 5;
then consider c3 being transition of c1 such that
E11: c3 in *' c2 and
E12: not c3 in c2 *' by SUBSET_1:7;
set c4 = (the Places of c1 --> TRUE ) +* (c2 --> FALSE );
E13: [#] the Places of c1 = the Places of c1 by SUBSET_1:def 4;
( dom (the Places of c1 --> TRUE ) = the Places of c1 & dom (c2 --> FALSE ) = c2 ) by FUNCOP_1:19;
then E14: dom ((the Places of c1 --> TRUE ) +* (c2 --> FALSE )) = the Places of c1 \/ c2 by FUNCT_4:def 1
.= the Places of c1 by E13, SUBSET_1:28 ;
( rng (the Places of c1 --> TRUE ) c= {TRUE } & rng (c2 --> FALSE ) c= {FALSE } ) by FUNCOP_1:19;
then ( rng (the Places of c1 --> TRUE ) c= BOOLEAN & rng (c2 --> FALSE ) c= BOOLEAN ) by XBOOLE_1:1;
then E15: (rng (the Places of c1 --> TRUE )) \/ (rng (c2 --> FALSE )) c= BOOLEAN by XBOOLE_1:8;
rng ((the Places of c1 --> TRUE ) +* (c2 --> FALSE )) c= (rng (the Places of c1 --> TRUE )) \/ (rng (c2 --> FALSE )) by FUNCT_4:18;
then rng ((the Places of c1 --> TRUE ) +* (c2 --> FALSE )) c= BOOLEAN by E15, XBOOLE_1:1;
then (the Places of c1 --> TRUE ) +* (c2 --> FALSE ) in Funcs the Places of c1,BOOLEAN by E14, FUNCT_2:def 2;
then reconsider c5 = (the Places of c1 --> TRUE ) +* (c2 --> FALSE ) as Boolean_marking of c1 ;
E16: c5 .: c2 = {FALSE } by Th5;
c2 misses *' {c3} by E12, PETRI:19;
then E17: (the Places of c1 --> TRUE ) .: (*' {c3}) = c5 .: (*' {c3}) by Th3;
E18: rng (the Places of c1 --> TRUE ) c= {TRUE } by FUNCOP_1:19;
(the Places of c1 --> TRUE ) .: (*' {c3}) c= rng (the Places of c1 --> TRUE ) by RELAT_1:144;
then c5 .: (*' {c3}) c= {TRUE } by E17, E18, XBOOLE_1:1;
then E19: c3 is_firable_on c5 by Def2;
{c3} *' meets c2 by E11, PETRI:20;
then consider c6 being set such that
E20: c6 in ({c3} *' ) /\ c2 by XBOOLE_0:4;
E21: ( c6 in {c3} *' & c6 in c2 ) by E20, XBOOLE_0:def 3;
then (Firing c3,c5) . c6 = TRUE by Th6;
then TRUE in (Firing c3,c5) .: c2 by E21, FUNCT_2:43;
then (Firing c3,c5) .: c2 <> {FALSE } by MARGREL1:38, TARSKI:def 1;
hence contradiction by E10, E16, E19;
end;

theorem Th7: :: BOOLMARK:7
for b1 being PT_net_Str
for b2 being non empty Subset of the Places of b1 holds
( b2 is Deadlock-like iff for b3 being Boolean_marking of b1 st b3 .: b2 = {FALSE } holds
for b4 being transition of b1 st b4 is_firable_on b3 holds
(Firing b4,b3) .: b2 = {FALSE } )
proof end;

theorem Th8: :: BOOLMARK:8
for b1 being non empty set
for b2, b3 being FinSequence of b1
for b4 being Nat st 1 <= b4 & b4 <= len b2 holds
(b2 ^ b3) /. b4 = b2 /. b4
proof end;

theorem Th9: :: BOOLMARK:9
canceled;

theorem Th10: :: BOOLMARK:10
for b1 being PT_net_Str
for b2 being Boolean_marking of b1
for b3, b4 being FinSequence of the Transitions of b1 holds Firing (b3 ^ b4),b2 = Firing b4,(Firing b3,b2)
proof end;

theorem Th11: :: BOOLMARK:11
for b1 being PT_net_Str
for b2 being Boolean_marking of b1
for b3, b4 being FinSequence of the Transitions of b1 st b3 ^ b4 is_firable_on b2 holds
( b4 is_firable_on Firing b3,b2 & b3 is_firable_on b2 )
proof end;

theorem Th12: :: BOOLMARK:12
for b1 being PT_net_Str
for b2 being Boolean_marking of b1
for b3 being transition of b1 holds
( b3 is_firable_on b2 iff <*b3*> is_firable_on b2 )
proof end;

theorem Th13: :: BOOLMARK:13
for b1 being PT_net_Str
for b2 being Boolean_marking of b1
for b3 being transition of b1 holds Firing b3,b2 = Firing <*b3*>,b2
proof end;

theorem Th14: :: BOOLMARK:14
for b1 being PT_net_Str
for b2 being non empty Subset of the Places of b1 holds
( b2 is Deadlock-like iff for b3 being Boolean_marking of b1 st b3 .: b2 = {FALSE } holds
for b4 being FinSequence of the Transitions of b1 st b4 is_firable_on b3 holds
(Firing b4,b3) .: b2 = {FALSE } )
proof end;