Copyright (c) 1992 Association of Mizar Users
environ
vocabulary RELAT_1, NET_1, MCART_1, ARYTM_3, BOOLE, PETRI;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1,
DOMAIN_1;
constructors RELSET_1, DOMAIN_1, MEMBERED, XBOOLE_0;
clusters RELSET_1, PRELAMB, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
theorems RELSET_1, SUBSET_1, MCART_1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0;
schemes DOMAIN_1;
begin
:: Redefinition of Element for Non-empty Relation
definition
let A, B be non empty set;
let r be non empty Relation of A, B;
redefine mode Element of r -> Element of [:A,B:];
coherence
proof
let a be Element of r;
thus a is Element of [:A,B:];
end;
end;
:: Place/Transition Net Structure
definition
struct PT_net_Str
(# Places, Transitions -> non empty set,
S-T_Arcs -> non empty Relation of the Places, the Transitions,
T-S_Arcs -> non empty Relation of the Transitions, the Places #);
end;
reserve PTN for PT_net_Str;
:: Place, Transition, and Arc (s->t, t->s) Elements
definition
let PTN;
mode place of PTN is Element of the Places of PTN;
mode places of PTN is Element of the Places of PTN;
mode transition of PTN is Element of the Transitions of PTN;
mode transitions of PTN is Element of the Transitions of PTN;
mode S-T_arc of PTN is Element of the S-T_Arcs of PTN;
mode T-S_arc of PTN is Element of the T-S_Arcs of PTN;
end;
:: Redefinition of Relation for s->t Arcs
definition
let PTN;
let x be S-T_arc of PTN;
redefine func x`1 -> place of PTN;
coherence
proof
thus x`1 is place of PTN;
end;
func x`2 -> transition of PTN;
coherence
proof
thus x`2 is transition of PTN;
end;
end;
:: Redefinition of Relation for t->s Arcs
definition
let PTN;
let x be T-S_arc of PTN;
redefine
func x`1 -> transition of PTN;
coherence
proof
thus x`1 is transition of PTN;
end;
func x`2 -> place of PTN;
coherence
proof
thus x`2 is place of PTN;
end;
end;
:: *S, S* Definitions and Theorems
reserve S0 for Subset of the Places of PTN;
definition
let PTN, S0;
func *'S0 -> Subset of the Transitions of PTN equals
:Def1:
{ t where t is transition of PTN : ex f being T-S_arc of PTN,
s being place of PTN st s in S0 & f = [t,s] };
coherence
proof
defpred P[set] means ex f being T-S_arc of PTN,
s being place of PTN st s in S0 & f = [$1,s];
{ t where t is transition of PTN : P[t] }
is Subset of the Transitions of PTN from SubsetD;
hence thesis;
end;
correctness;
func S0*' -> Subset of the Transitions of PTN equals
:Def2:
{ t where t is transition of PTN : ex f being S-T_arc of PTN,
s being place of PTN st s in S0 & f = [s,t] };
coherence
proof
defpred P[set] means ex f being S-T_arc of PTN,
s being place of PTN st s in S0 & f = [s,$1];
{ t where t is transition of PTN : P[t] }
is Subset of the Transitions of PTN from SubsetD;
hence thesis;
end;
correctness;
end;
theorem
*'S0 = {f`1 where f is T-S_arc of PTN : f`2 in S0}
proof
A1: *'S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN,
s being place of PTN st s in S0 & f = [t,s] } by Def1;
thus *'S0 c= {f`1 where f is T-S_arc of PTN : f`2 in S0}
proof
let x be set;
assume x in *'S0;
then consider t being transition of PTN such that A2: x = t
and A3: ex f being T-S_arc of PTN, s being place of PTN
st s in S0 & f = [t,s] by A1;
consider f being T-S_arc of PTN, s being place of PTN
such that A4: s in S0 and A5: f = [t,s] by A3;
f`1 = t & f`2 = s by A5,MCART_1:7;
hence x in {f0`1 where f0 is T-S_arc of PTN : f0`2 in S0} by A2,A4;
end;
let x be set;
assume x in {f`1 where f is T-S_arc of PTN : f`2 in S0};
then consider f being T-S_arc of PTN such that A6: x = f`1
and A7: f`2 in S0;
f = [f`1,f`2] by MCART_1:23;
hence x in *'S0 by A1,A6,A7;
end;
theorem Th2:
for x being set holds x in *'S0
iff
ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [x,s]
proof
let x be set;
A1: *'S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN,
s being place of PTN st s in S0 & f = [t,s] } by Def1;
thus x in *'S0 implies ex f being T-S_arc of PTN, s being place of PTN
st s in S0 & f = [x,s]
proof
assume x in *'S0;
then consider t being transition of PTN such that A2: x = t
and A3: ex f being T-S_arc of PTN, s being place of PTN
st s in S0 & f = [t,s] by A1;
consider f being T-S_arc of PTN, s being place of PTN
such that A4: s in S0 and A5: f = [t,s] by A3;
take f, s;
thus thesis by A2,A4,A5;
end;
given f being T-S_arc of PTN, s being place of PTN
such that A6: s in S0 & f = [x,s];
x = f`1 by A6,MCART_1:7;
hence thesis by A1,A6;
end;
theorem
S0*' = {f`2 where f is S-T_arc of PTN : f`1 in S0}
proof
A1: S0*' = { t where t is transition of PTN : ex f being S-T_arc of PTN,
s being place of PTN st s in S0 & f = [s,t] } by Def2;
thus S0*' c= {f`2 where f is S-T_arc of PTN : f`1 in S0}
proof
let x be set;
assume x in S0*';
then consider t being transition of PTN such that A2: x = t
and A3: ex f being S-T_arc of PTN, s being place of PTN
st s in S0 & f = [s,t] by A1;
consider f being S-T_arc of PTN, s being place of PTN
such that A4: s in S0 and A5: f = [s,t] by A3;
f`1 = s & f`2 = t by A5,MCART_1:7;
hence x in {f0`2 where f0 is S-T_arc of PTN : f0`1 in S0} by A2,A4;
end;
let x be set;
assume x in {f`2 where f is S-T_arc of PTN : f`1 in S0};
then consider f being S-T_arc of PTN such that A6: x = f`2
and A7: f`1 in S0;
f = [f`1,f`2] by MCART_1:23;
hence x in S0*' by A1,A6,A7;
end;
theorem Th4:
for x being set holds x in S0*'
iff
ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,x]
proof
let x be set;
A1: S0*' = { t where t is transition of PTN : ex f being S-T_arc of PTN,
s being place of PTN st s in S0 & f = [s,t] } by Def2;
thus x in S0*' implies ex f being S-T_arc of PTN, s being place of PTN
st s in S0 & f = [s,x]
proof
assume x in S0*';
then consider t being transition of PTN such that A2: x = t
and A3: ex f being S-T_arc of PTN, s being place of PTN
st s in S0 & f = [s,t] by A1;
consider f being S-T_arc of PTN, s being place of PTN
such that A4: s in S0 and A5: f = [s,t] by A3;
take f, s;
thus thesis by A2,A4,A5;
end;
given f being S-T_arc of PTN, s being place of PTN
such that A6: s in S0 & f = [s,x];
x = f`2 by A6,MCART_1:7;
hence thesis by A1,A6;
end;
:: *T, T* Definitions and Theorems
reserve T0 for Subset of the Transitions of PTN;
definition
let PTN, T0;
func *'T0 -> Subset of the Places of PTN equals
:Def3:
{ s where s is place of PTN : ex f being S-T_arc of PTN,
t being transition of PTN st t in T0 & f = [s,t] };
coherence
proof
defpred P[set] means ex f being S-T_arc of PTN,
t being transition of PTN st t in T0 & f = [$1,t];
{ s where s is place of PTN : P[s] }
is Subset of the Places of PTN from SubsetD;
hence thesis;
end;
correctness;
func T0*' -> Subset of the Places of PTN equals
:Def4:
{ s where s is place of PTN : ex f being T-S_arc of PTN,
t being transition of PTN st t in T0 & f = [t,s] };
coherence
proof
defpred P[set] means ex f being T-S_arc of PTN,
t being transition of PTN st t in T0 & f = [t,$1];
{ s where s is place of PTN : P[s] }
is Subset of the Places of PTN from SubsetD;
hence thesis;
end;
correctness;
end;
theorem
*'T0 = {f`1 where f is S-T_arc of PTN : f`2 in T0}
proof
A1: *'T0 = { s where s is place of PTN : ex f being S-T_arc of PTN,
t being transition of PTN st t in T0 & f = [s,t] } by Def3;
thus *'T0 c= {f`1 where f is S-T_arc of PTN : f`2 in T0}
proof
let x be set;
assume x in *'T0;
then consider s being place of PTN such that A2: x = s
and A3: ex f being S-T_arc of PTN, t being transition of PTN
st t in T0 & f = [s,t] by A1;
consider f being S-T_arc of PTN, t being transition of PTN
such that A4: t in T0 and A5: f = [s,t] by A3;
f`1 = s & f`2 = t by A5,MCART_1:7;
hence x in {f0`1 where f0 is S-T_arc of PTN : f0`2 in T0} by A2,A4;
end;
let x be set;
assume x in {f`1 where f is S-T_arc of PTN : f`2 in T0};
then consider f being S-T_arc of PTN such that A6: x = f`1
and A7: f`2 in T0;
f = [f`1,f`2] by MCART_1:23;
hence x in *'T0 by A1,A6,A7;
end;
theorem Th6:
for x being set holds x in *'T0
iff
ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [x,t]
proof
let x be set;
A1: *'T0 = { s where s is place of PTN : ex f being S-T_arc of PTN,
t being transition of PTN st t in T0 & f = [s,t] } by Def3;
thus x in
*'T0 implies ex f being S-T_arc of PTN, t being transition of PTN
st t in T0 & f = [x,t]
proof
assume x in *'T0;
then consider s being place of PTN such that A2: x = s
and A3: ex f being S-T_arc of PTN, t being transition of PTN
st t in T0 & f = [s,t] by A1;
consider f being S-T_arc of PTN, t being transition of PTN
such that A4: t in T0 and A5: f = [s,t] by A3;
take f, t;
thus thesis by A2,A4,A5;
end;
given f being S-T_arc of PTN, t being transition of PTN
such that A6: t in T0 & f = [x,t];
x = f`1 by A6,MCART_1:7;
hence thesis by A1,A6;
end;
theorem
T0*' = {f`2 where f is T-S_arc of PTN : f`1 in T0}
proof
A1: T0*' = { s where s is place of PTN : ex f being T-S_arc of PTN,
t being transition of PTN st t in T0 & f = [t,s] } by Def4;
thus T0*' c= {f`2 where f is T-S_arc of PTN : f`1 in T0}
proof
let x be set;
assume x in T0*';
then consider s being place of PTN such that A2: x = s
and A3: ex f being T-S_arc of PTN, t being transition of PTN
st t in T0 & f = [t,s] by A1;
consider f being T-S_arc of PTN, t being transition of PTN
such that A4: t in T0 and A5: f = [t,s] by A3;
f`1 = t & f`2 = s by A5,MCART_1:7;
hence x in {f0`2 where f0 is T-S_arc of PTN : f0`1 in T0} by A2,A4;
end;
let x be set;
assume x in {f`2 where f is T-S_arc of PTN : f`1 in T0};
then consider f being T-S_arc of PTN such that A6: x = f`2
and A7: f`1 in T0;
f = [f`1,f`2] by MCART_1:23;
hence x in T0*' by A1,A6,A7;
end;
theorem Th8:
for x being set holds x in T0*'
iff
ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,x]
proof
let x be set;
A1: T0*' = { s where s is place of PTN : ex f being T-S_arc of PTN,
t being transition of PTN st t in T0 & f = [t,s] } by Def4;
thus x in
T0*' implies ex f being T-S_arc of PTN, t being transition of PTN
st t in T0 & f = [t,x]
proof
assume x in T0*';
then consider s being place of PTN such that A2: x = s
and A3: ex f being T-S_arc of PTN, t being transition of PTN
st t in T0 & f = [t,s] by A1;
consider f being T-S_arc of PTN, t being transition of PTN
such that A4: t in T0 and A5: f = [t,s] by A3;
take f, t;
thus thesis by A2,A4,A5;
end;
given f being T-S_arc of PTN, t being transition of PTN
such that A6: t in T0 & f = [t,x];
x = f`2 by A6,MCART_1:7;
hence thesis by A1,A6;
end;
theorem
*'{}the Places of PTN = {}
proof consider x being Element of *'{}the Places of PTN;
assume not thesis;
then x in *'{}the Places of PTN;
then x in { t where t is transition of PTN : ex f being T-S_arc of PTN
,
s being place of PTN st s in {}the Places of PTN & f = [t,s] }
by Def1;
then consider t being transition of PTN such that x = t
and A1: ex f being T-S_arc of PTN, s being place of PTN
st s in {}the Places of PTN & f = [t,s];
consider f being T-S_arc of PTN, s being place of PTN
such that A2: s in {}the Places of PTN & f = [t,s] by A1;
thus contradiction by A2;
end;
theorem
({}the Places of PTN)*' = {}
proof consider x being Element of ({}the Places of PTN)*';
assume not thesis;
then x in ({}the Places of PTN)*';
then x in { t where t is transition of PTN : ex f being S-T_arc of PTN
,
s being place of PTN st s in {}the Places of PTN & f = [s,t] }
by Def2;
then consider t being transition of PTN such that x = t
and A1: ex f being S-T_arc of PTN, s being place of PTN
st s in {}the Places of PTN & f = [s,t];
consider f being S-T_arc of PTN, s being place of PTN
such that A2: s in {}the Places of PTN & f = [s,t] by A1;
thus contradiction by A2;
end;
theorem
*'{}the Transitions of PTN = {}
proof consider x being Element of *'{}the Transitions of PTN;
assume not thesis;
then x in *'{}the Transitions of PTN;
then x in { s where s is place of PTN : ex f being S-T_arc of PTN,
t being transition of PTN st t in {}the Transitions of PTN
& f = [s,t] } by Def3;
then consider s being place of PTN such that x = s
and A1: ex f being S-T_arc of PTN, t being transition of PTN
st t in {}the Transitions of PTN & f = [s,t];
consider f being S-T_arc of PTN, t being transition of PTN
such that A2: t in {}the Transitions of PTN & f = [s,t] by A1;
thus contradiction by A2;
end;
theorem
({}the Transitions of PTN)*' = {}
proof consider x being Element of ({}the Transitions of PTN)*';
assume not thesis;
then x in ({}the Transitions of PTN)*';
then x in { s where s is place of PTN : ex f being T-S_arc of PTN,
t being transition of PTN st t in {}the Transitions of PTN
& f = [t,s] } by Def4;
then consider s being place of PTN such that x = s
and A1: ex f being T-S_arc of PTN, t being transition of PTN
st t in {}the Transitions of PTN & f = [t,s];
consider f being T-S_arc of PTN, t being transition of PTN
such that A2: t in {}the Transitions of PTN & f = [t,s] by A1;
thus contradiction by A2;
end;
begin
:: Deadlock-like Attribute for Place Sets
definition
let PTN;
let IT be Subset of the Places of PTN;
attr IT is Deadlock-like means
*'IT is Subset of IT*';
end;
:: With_Deadlocks Mode for Place\Transition Nets
definition let IT be PT_net_Str;
attr IT is With_Deadlocks means
ex S being Subset of the Places of IT st S is Deadlock-like;
end;
definition
cluster With_Deadlocks PT_net_Str;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider f = {[0,0]} as non empty Relation of {0}, {0}
by RELSET_1:8;
take PTN1 = PT_net_Str (# {0}, {0}, f, f #);
{0} c= the Places of PTN1;
then reconsider S = {0} as Subset of the Places of PTN1;
take S;
A1: *'S = { t where t is transition of PTN1 : ex f being T-S_arc of PTN1,
s being place of PTN1 st s in S & f = [t,s] } by Def1;
A2: S*' = { t where t is transition of PTN1 : ex f being S-T_arc of PTN1,
s being place of PTN1 st s in S & f = [s,t] } by Def2;
reconsider s = 0 as place of PTN1 by TARSKI:def 1;
reconsider t = 0 as transition of PTN1 by TARSKI:def 1;
reconsider st_f = [0,0] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider ts_f = [0,0] as T-S_arc of PTN1 by TARSKI:def 1;
ts_f = [t,s] & s in S;
then t in *'S by A1;
then {t} c= *'S by ZFMISC_1:37;
then A3: {t} = *'S by XBOOLE_0:def 10;
st_f = [s,t] & s in S;
then t in S*' by A2;
hence *'S is Subset of S*' by A3,ZFMISC_1:37;
end;
end;
begin
:: Trap-like Attribute for Place Sets
definition
let PTN;
let IT be Subset of the Places of PTN;
attr IT is Trap-like means
IT*' is Subset of *'IT;
end;
:: With_Traps Mode for Place\Transition Nets
definition let IT be PT_net_Str;
attr IT is With_Traps means
ex S being Subset of the Places of IT st S is Trap-like;
end;
definition
cluster With_Traps PT_net_Str;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider f = {[0,0]} as non empty Relation of {0}, {0}
by RELSET_1:8;
take PTN1 = PT_net_Str (# {0}, {0}, f, f #);
{0} c= the Places of PTN1;
then reconsider S = {0} as Subset of the Places of PTN1;
take S;
A1: *'S = { t where t is transition of PTN1 : ex f being T-S_arc of PTN1,
s being place of PTN1 st s in S & f = [t,s] } by Def1;
A2: S*' = { t where t is transition of PTN1 : ex f being S-T_arc of PTN1,
s being place of PTN1 st s in S & f = [s,t] } by Def2;
reconsider s = 0 as place of PTN1 by TARSKI:def 1;
reconsider t = 0 as transition of PTN1 by TARSKI:def 1;
reconsider st_f = [0,0] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider ts_f = [0,0] as T-S_arc of PTN1 by TARSKI:def 1;
st_f = [s,t] & s in S;
then t in S*' by A2;
then {t} c= S*' by ZFMISC_1:37;
then A3: {t} = S*' by XBOOLE_0:def 10;
ts_f = [t,s] & s in S;
then t in *'S by A1;
hence S*' is Subset of *'S by A3,ZFMISC_1:37;
end;
end;
definition
let A, B be non empty set;
let r be non empty Relation of A, B;
redefine
func r~ -> non empty Relation of B, A;
coherence
proof consider x being Element of r;
consider y, z being set such that A1: x = [y,z] by RELAT_1:def 1;
[z,y] in r~ by A1,RELAT_1:def 7;
hence thesis;
end;
end;
begin
:: Duality Definitions and Theorems for Place/Transition Nets
definition
let PTN;
func PTN.: -> strict PT_net_Str equals
:Def9:
PT_net_Str (# the Places of PTN, the Transitions of PTN,
(the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #);
correctness;
end;
theorem Th13:
PTN.:.: = the PT_net_Str of PTN
proof
A1: (the S-T_Arcs of PTN)~~ = the S-T_Arcs of PTN
& (the T-S_Arcs of PTN)~~ = the T-S_Arcs of PTN;
thus PTN.:.: = PT_net_Str (# the Places of PTN, the Transitions of PTN,
(the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #).: by Def9
.= the PT_net_Str of PTN by A1,Def9;
end;
theorem Th14:
the Places of PTN = the Places of PTN.:
& the Transitions of PTN = the Transitions of PTN.:
& (the S-T_Arcs of PTN)~ = the T-S_Arcs of PTN.:
& (the T-S_Arcs of PTN)~ = the S-T_Arcs of PTN.:
proof
PTN.: = PT_net_Str (# the Places of PTN, the Transitions of PTN,
(the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #) by Def9;
hence thesis;
end;
definition
let PTN;
let S0 be Subset of the Places of PTN;
func S0.: -> Subset of the Places of PTN.: equals
:Def10:
S0;
coherence by Th14;
end;
definition
let PTN;
let s be place of PTN;
func s.: -> place of PTN.: equals
:Def11:
s;
coherence by Th14;
end;
definition
let PTN;
let S0 be Subset of the Places of PTN.:;
func .:S0 -> Subset of the Places of PTN equals
S0;
coherence by Th14;
end;
definition
let PTN;
let s be place of PTN.:;
func .:s -> place of PTN equals
:Def13:
s;
coherence by Th14;
end;
definition
let PTN;
let T0 be Subset of the Transitions of PTN;
func T0.: -> Subset of the Transitions of PTN.: equals
T0;
coherence by Th14;
end;
definition
let PTN;
let t be transition of PTN;
func t.: -> transition of PTN.: equals
t;
coherence by Th14;
end;
definition
let PTN;
let T0 be Subset of the Transitions of PTN.:;
func .:T0 -> Subset of the Transitions of PTN equals
T0;
coherence by Th14;
end;
definition
let PTN;
let t be transition of PTN.:;
func .:t -> transition of PTN equals
t;
coherence by Th14;
end;
reserve S for Subset of the Places of PTN;
theorem Th15:
S.:*' = *'S
proof
thus S.:*' c= *'S
proof
let x be set;
A1: the T-S_Arcs of the PT_net_Str of PTN = the T-S_Arcs of PTN;
assume x in S.:*';
then consider f being S-T_arc of PTN.:, s being place of PTN.:
such that A2: s in S.: & f = [s,x] by Th4;
A3: .:s = s & S.: = S by Def10,Def13;
(the S-T_Arcs of PTN.:)~ = the T-S_Arcs of PTN.:.: by Th14;
then (the S-T_Arcs of PTN.:)~ = the T-S_Arcs of PTN by A1,Th13;
then [x,.:s] is T-S_arc of PTN by A2,A3,RELAT_1:def 7;
hence x in *'S by A2,A3,Th2;
end;
let x be set;
assume x in *'S;
then consider f being T-S_arc of PTN, s being place of PTN
such that A4: s in S & f = [x,s] by Th2;
A5: s.: = s & S.: = S by Def10,Def11;
(the T-S_Arcs of PTN)~ = the S-T_Arcs of PTN.: by Th14;
then [s.:,x] is S-T_arc of PTN.: by A4,A5,RELAT_1:def 7;
hence x in S.:*' by A4,A5,Th4;
end;
theorem Th16:
*'(S.:) = S*'
proof
thus *'(S.:) c= S*'
proof
let x be set;
A1: the T-S_Arcs of the PT_net_Str of PTN = the T-S_Arcs of PTN;
assume x in *'(S.:);
then consider f being T-S_arc of PTN.:, s being place of PTN.:
such that A2: s in S.: & f = [x,s] by Th2;
A3: .:s = s & S.: = S by Def10,Def13;
(the T-S_Arcs of PTN.:)~ = the S-T_Arcs of PTN.:.: by Th14;
then (the T-S_Arcs of PTN.:)~ = the S-T_Arcs of PTN by A1,Th13;
then [.:s,x] is S-T_arc of PTN by A2,A3,RELAT_1:def 7;
hence x in S*' by A2,A3,Th4;
end;
let x be set;
assume x in S*';
then consider f being S-T_arc of PTN, s being place of PTN
such that A4: s in S & f = [s,x] by Th4;
A5: s.: = s & S.: = S by Def10,Def11;
(the S-T_Arcs of PTN)~ = the T-S_Arcs of PTN.: by Th14;
then [x,s.:] is T-S_arc of PTN.: by A4,A5,RELAT_1:def 7;
hence x in *'(S.:) by A4,A5,Th2;
end;
theorem
S is Deadlock-like iff S.: is Trap-like
proof
A1: S.:*' = *'S & *'(S.:) = S*' by Th15,Th16;
thus S is Deadlock-like implies S.: is Trap-like
proof
assume *'S is Subset of S*';
hence S.:*' is Subset of *'(S.:) by A1;
end;
assume S.:*' is Subset of *'(S.:);
hence *'S is Subset of S*' by A1;
end;
theorem
S is Trap-like iff S.: is Deadlock-like
proof
A1: S.:*' = *'S & *'(S.:) = S*' by Th15,Th16;
thus S is Trap-like implies S.: is Deadlock-like
proof
assume S*' is Subset of *'S;
hence *'(S.:) is Subset of S.:*' by A1;
end;
assume *'(S.:) is Subset of S.:*';
hence S*' is Subset of *'S by A1;
end;
theorem
for PTN being PT_net_Str,
t being transition of PTN,
S0 being Subset of the Places of PTN
holds t in S0*' iff *'{t} meets S0
proof
let PTN be PT_net_Str;
let t be transition of PTN;
let S0 be Subset of the Places of PTN;
thus t in S0*' implies *'{t} meets S0
proof
assume t in S0*';
then consider f being S-T_arc of PTN, s being place of PTN
such that A1: s in S0 & f = [s,t] by Th4;
t in {t} by TARSKI:def 1;
then s in *'{t} by A1,Th6;
hence *'{t} /\ S0 <> {} by A1,XBOOLE_0:def 3;
end;
assume *'{t} /\ S0 <> {};
then consider s being place of PTN such that A2: s in *'{t} /\ S0
by SUBSET_1:10;
A3: s in *'{t} & s in S0 by A2,XBOOLE_0:def 3;
then consider f being S-T_arc of PTN, t0 being transition of PTN
such that A4: t0 in {t} and A5: f = [s,t0] by Th6;
t0 = t by A4,TARSKI:def 1;
hence t in S0*' by A3,A5,Th4;
end;
theorem
for PTN being PT_net_Str,
t being transition of PTN,
S0 being Subset of the Places of PTN
holds t in *'S0 iff {t}*' meets S0
proof
let PTN be PT_net_Str;
let t be transition of PTN;
let S0 be Subset of the Places of PTN;
thus t in *'S0 implies {t}*' meets S0
proof
assume t in *'S0;
then consider f being T-S_arc of PTN, s being place of PTN
such that A1: s in S0 & f = [t,s] by Th2;
t in {t} by TARSKI:def 1;
then s in {t}*' by A1,Th8;
hence {t}*' /\ S0 <> {} by A1,XBOOLE_0:def 3;
end;
assume {t}*' /\ S0 <> {};
then consider s being place of PTN such that A2: s in {t}*' /\ S0
by SUBSET_1:10;
A3: s in {t}*' & s in S0 by A2,XBOOLE_0:def 3;
then consider f being T-S_arc of PTN, t0 being transition of PTN
such that A4: t0 in {t} and A5: f = [t0,s] by Th8;
t0 = t by A4,TARSKI:def 1;
hence t in *'S0 by A3,A5,Th2;
end;