:: Some Elementary Notions of the Theory of Petri Nets
:: by Waldemar Korczy\'nski
::
:: Received August 10, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, NET_1,
STRUCT_0, PETRI;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, PARTIT_2,
STRUCT_0, PETRI;
constructors TARSKI, SUBSET_1, RELAT_1, STRUCT_0, PETRI, PARTIT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions XBOOLE_0;
theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0, SUBSET_1;
begin
definition let P be PT_net_Str;
func Flow P -> set equals
(the S-T_Arcs of P) \/ the T-S_Arcs of P;
coherence;
end;
registration let P be PT_net_Str;
cluster Flow P -> Relation-like;
coherence;
end;
::The above definition describes a "structure of a Petri net" which
::is a kind of relational system.
reserve x,y for set;
reserve N for PT_net_Str;
definition
let N be PT_net_Str;
attr N is Petri means
:Def2:
the carrier of N misses the carrier' of N & (
Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the
carrier' of N, the carrier of N:];
end;
:: A Petri net is defined as a triple of the form
:: N = (carrier, carrier', Flow)
:: with carrier and carrier' being disjoint sets and
:: Flow c= (carrier' x carrier) U (carrier x carrier')
:: It is allowed that both sets carrier and carrier' are empty.
:: A Petri net is here described as a predicate defined in the set
:: (on the mode) PT_net_Str.
definition
let N be PT_net_Str;
func Elements(N) -> set equals
(the carrier of N) \/ (the carrier' of N);
correctness;
end;
theorem
Elements(N) <> {} implies (x is Element of Elements(N) implies x is
Element of the carrier of N or x is Element of the carrier' of N) by
XBOOLE_0:def 3;
theorem
x is Element of the carrier of N & the carrier of N <> {} implies x is
Element of Elements(N)
by XBOOLE_1:7,TARSKI:def 3;
theorem
x is Element of the carrier' of N & the carrier' of N <> {}
implies x is Element of Elements(N)
by XBOOLE_1:7,TARSKI:def 3;
Lm1: PT_net_Str (# {} , {} , {}({},{}), {}({},{}) #) is Petri
proof
set N = PT_net_Str (# {} , {} , {}({},{}), {}({},{}) #);
thus (the carrier of N) /\ the carrier' of N = {};
thus thesis;
end;
registration
cluster PT_net_Str (#{}, {}, {}({},{}), {}({},{})#) -> Petri;
coherence by Lm1;
end;
:: This lemma is of rather "technical" nature. It allows a definition
:: of a "subtype" of the type PT_net_Str. (see the following definition of the
:: type Pnet).
registration
cluster strict Petri for PT_net_Str;
existence
proof
PT_net_Str (# {} , {} , {}({},{}), {}({},{}) #) is Petri;
hence thesis;
end;
end;
definition
mode Pnet is Petri PT_net_Str;
end;
:: The above definition defines a Petri net as a TYPE of the structure
:: PT_net_Str. The type is not empty.
theorem Th4:
for N being Pnet holds not (x in the carrier of N & x in the carrier' of N)
by Def2,XBOOLE_0:3;
:: This lemma is of rather "technical" character. It will be used in the
:: proof of the correctness of a definition of a function bellow. (See
:: the definition of the functions Enter and Exit.)
theorem Th5:
for N being Pnet holds [x,y] in Flow N & x in the
carrier' of N implies y in the carrier of N
proof
let N be Pnet;
assume that
A1: [x,y] in Flow N and
A2: x in the carrier' of N;
A3: not x in the carrier of N by A2,Th4;
(Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the
carrier' of N, the carrier of N:] by Def2;
then [x,y] in [:the carrier of N, the carrier' of N:] or [x,y] in [:the
carrier' of N, the carrier of N:] by A1,XBOOLE_0:def 3;
hence thesis by A3,ZFMISC_1:87;
end;
theorem Th6:
for N being Pnet holds [x,y] in Flow N & y in the
carrier' of N implies x in the carrier of N
proof
let N be Pnet;
assume that
A1: [x,y] in Flow N and
A2: y in the carrier' of N;
A3: not y in the carrier of N by A2,Th4;
(Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the
carrier' of N, the carrier of N:] by Def2;
then [x,y] in [:the carrier of N, the carrier' of N:] or [x,y] in [:the
carrier' of N, the carrier of N:] by A1,XBOOLE_0:def 3;
hence thesis by A3,ZFMISC_1:87;
end;
theorem
for N being Pnet holds [x,y] in Flow N & x in the carrier of N
implies y in the carrier' of N
proof
let N be Pnet;
assume that
A1: [x,y] in Flow N and
A2: x in the carrier of N;
A3: not x in the carrier' of N by A2,Th4;
(Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the
carrier' of N,the carrier of N :] by Def2;
then [x,y] in [:the carrier' of N, the carrier of N:] or [x,y] in [:the
carrier of N, the carrier' of N:] by A1,XBOOLE_0:def 3;
hence thesis by A3,ZFMISC_1:87;
end;
theorem
for N being Pnet holds [x,y] in Flow N & y in the carrier of N
implies x in the carrier' of N
proof
let N be Pnet;
assume that
A1: [x,y] in Flow N and
A2: y in the carrier of N;
A3: not y in the carrier' of N by A2,Th4;
(Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the
carrier' of N,the carrier of N :] by Def2;
then [x,y] in [:the carrier' of N, the carrier of N:] or [x,y] in [:the
carrier of N, the carrier' of N:] by A1,XBOOLE_0:def 3;
hence thesis by A3,ZFMISC_1:87;
end;
definition
let N be Pnet;
let x,y;
pred pre N,x,y means
[y,x] in Flow N & x in the carrier' of N;
pred post N,x,y means
[x,y] in Flow N & x in the carrier' of N;
end;
definition
let N be PT_net_Str;
let x be Element of Elements(N);
func Pre(N,x) -> set means
:Def6:
for y being object holds y in it iff y in Elements(N) & [y,x] in Flow N;
existence
proof
defpred P[object] means [$1,x] in Flow N;
thus ex IT being set st
for y being object holds y in IT iff y in Elements(N)
& P[y] from XBOOLE_0:sch 1;
end;
uniqueness
proof
let X,Y be set such that
A1: for y being object holds y in X iff y in Elements(N) & [y,x] in Flow N and
A2: for y being object holds y in Y iff y in Elements(N) & [y,x] in Flow N;
A3: for y being object holds y in Y implies y in X
proof let y be object;
assume y in Y;
then y in Elements(N) & [y,x] in Flow N by A2;
hence thesis by A1;
end;
for y being object holds y in X implies y in Y
proof let y be object;
assume y in X;
then y in Elements(N) & [y,x] in Flow N by A1;
hence thesis by A2;
end;
hence thesis by A3,TARSKI:2;
end;
func Post(N,x) -> set means
:Def7:
for y being object holds y in it iff y in Elements(N) & [x,y] in Flow N;
existence
proof
defpred P[object] means [x,$1] in Flow N;
thus ex IT being set st
for y being object holds y in IT iff y in Elements(N)
& P[y] from XBOOLE_0:sch 1;
end;
uniqueness
proof
let X,Y be set such that
A4: for y being object holds y in X iff y in Elements(N) & [x,y] in Flow N and
A5: for y being object holds y in Y iff y in Elements(N) & [x,y] in Flow N;
A6: for y being object holds y in Y implies y in X
proof let y be object;
assume y in Y;
then y in Elements(N) & [x,y] in Flow N by A5;
hence thesis by A4;
end;
for y being object holds y in X implies y in Y
proof let y be object;
assume y in X;
then y in Elements(N) & [x,y] in Flow N by A4;
hence thesis by A5;
end;
hence thesis by A6,TARSKI:2;
end;
end;
theorem Th9:
for N being Pnet for x being Element of Elements(N) holds Pre(N,
x) c= Elements(N)
proof
let N be Pnet;
let x be Element of Elements(N);
for y being object holds y in Pre(N,x) implies y in Elements(N) by Def6;
hence thesis by TARSKI:def 3;
end;
theorem
for N being Pnet for x being Element of Elements N holds Pre(N,x) c=
Elements N by Th9;
theorem Th11:
for N being Pnet for x being Element of Elements(N) holds Post(N
,x) c= Elements(N)
proof
let N be Pnet;
let x be Element of Elements(N);
for y being object holds y in Post(N,x) implies y in Elements(N) by Def7;
hence thesis by TARSKI:def 3;
end;
theorem
for N being Pnet for x being Element of Elements N holds Post(N,x) c=
Elements N by Th11;
theorem
for N being Pnet for y being Element of Elements(N) holds y in the
carrier' of N implies (x in Pre(N,y) iff pre N,y,x)
proof
let N be Pnet;
let y be Element of Elements(N);
assume
A1: y in the carrier' of N;
A2: pre N,y,x implies x in Pre(N,y)
proof
assume pre N,y,x;
then
A3: [x,y] in Flow N;
then x in the carrier of N by A1,Th6;
then x in Elements(N) by XBOOLE_0:def 3;
hence thesis by A3,Def6;
end;
x in Pre(N,y) implies pre N,y,x
by Def6,A1;
hence thesis by A2;
end;
theorem
for N being Pnet for y being Element of Elements(N) holds y in the
carrier' of N implies (x in Post(N,y) iff post N,y,x)
proof
let N be Pnet;
let y be Element of Elements(N);
assume
A1: y in the carrier' of N;
A2: post N,y,x implies x in Post(N,y)
proof
assume post N,y,x;
then
A3: [y,x] in Flow N;
then x in the carrier of N by A1,Th5;
then x in Elements(N) by XBOOLE_0:def 3;
hence thesis by A3,Def7;
end;
x in Post(N,y) implies post N,y,x
by Def7,A1;
hence thesis by A2;
end;
definition
let N be Pnet;
let x be Element of Elements(N);
assume
A1: Elements(N) <> {};
func enter(N,x) -> set means
:Def8:
(x in the carrier of N implies it = {x}) & (x in
the carrier' of N implies it = Pre(N,x));
existence
proof
not(x in the carrier of N & x in the carrier' of N) by Th4;
hence thesis;
end;
uniqueness by A1,XBOOLE_0:def 3;
end;
theorem Th15:
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies enter(N,x) ={x} or enter(N,x) = Pre(N,x)
proof
let N be Pnet;
let x be Element of Elements(N);
assume Elements(N) <> {};
then x in (the carrier of N) or x in (the carrier' of N) by XBOOLE_0:def 3;
hence thesis by Def8;
end;
theorem Th16:
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies enter(N,x) c= Elements(N)
proof
let N be Pnet;
let x be Element of Elements(N);
assume
A1: Elements(N) <> {};
A2: enter(N,x) ={x} implies enter(N,x) c= Elements(N)
proof
x in Elements(N) by A1;
then
A3: for y being object holds y in {x} implies y in Elements(N)
by TARSKI:def 1;
assume enter(N,x) ={x};
hence thesis by A3,TARSKI:def 3;
end;
enter(N,x) ={x} or enter(N,x) = Pre(N,x) by A1,Th15;
hence thesis by A2,Th9;
end;
theorem
for N being Pnet for x being Element of Elements N holds Elements N <>
{} implies enter(N,x) c= Elements N by Th16;
definition
let N be Pnet;
let x be Element of Elements(N);
assume
A1: Elements(N) <> {};
func exit(N,x) -> set means
:Def9:
(x in the carrier of N implies it = {x})
& (x in the carrier' of N implies it = Post(N,x));
existence
proof
not(x in the carrier of N & x in the carrier' of N) by Th4;
hence thesis;
end;
uniqueness by A1,XBOOLE_0:def 3;
end;
theorem Th18:
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies exit(N,x) ={x} or exit(N,x) = Post(N,x)
proof
let N be Pnet;
let x be Element of Elements(N);
assume Elements(N) <> {};
then x in (the carrier of N) or x in (the carrier' of N) by XBOOLE_0:def 3;
hence thesis by Def9;
end;
theorem Th19:
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies exit(N,x) c= Elements(N)
proof
let N be Pnet;
let x be Element of Elements(N);
assume
A1: Elements(N) <> {};
A2: exit(N,x) ={x} implies exit(N,x) c= Elements(N)
proof
x in Elements(N) by A1;
then
A3: for y being object holds y in {x} implies y in Elements(N)
by TARSKI:def 1;
assume exit(N,x) ={x};
hence thesis by A3,TARSKI:def 3;
end;
exit(N,x) ={x} or exit(N,x) = Post(N,x) by A1,Th18;
hence thesis by A2,Th11;
end;
theorem
for N being Pnet for x being Element of Elements N holds Elements N <>
{} implies exit(N,x) c= Elements N by Th19;
definition
let N be Pnet;
let x be Element of Elements(N);
func field(N,x) -> set equals
enter(N,x) \/ exit(N,x);
correctness;
end;
definition
let N be PT_net_Str;
let x be Element of the carrier' of N;
func Prec(N,x) -> set means
for y being object holds
y in it iff y in the carrier of N & [y,x] in Flow N;
existence
proof
defpred P[object] means [$1,x] in Flow N;
thus ex IT being set st
for y being object holds y in IT iff y in the carrier
of N & P[y] from XBOOLE_0:sch 1;
end;
uniqueness
proof
let X,Y be set such that
A1: for y being object holds y in X
iff y in the carrier of N & [y,x] in Flow N and
A2: for y being object holds y in Y
iff y in the carrier of N & [y,x] in Flow N;
A3: for y being object holds y in Y implies y in X
proof let y be object;
assume y in Y;
then y in the carrier of N & [y,x] in Flow N by A2;
hence thesis by A1;
end;
for y being object holds y in X implies y in Y
proof let y be object;
assume y in X;
then y in the carrier of N & [y,x] in Flow N by A1;
hence thesis by A2;
end;
hence thesis by A3,TARSKI:2;
end;
func Postc(N,x) -> set means
for y being object holds
y in it iff y in the carrier of N & [x,y] in Flow N;
existence
proof
defpred P[object] means [x,$1] in Flow N;
thus ex IT being set st
for y being object holds y in IT iff y in the carrier
of N & P[y]from XBOOLE_0:sch 1;
end;
uniqueness
proof
let X,Y be set such that
A4: for y being object holds
y in X iff y in the carrier of N & [x,y] in Flow N and
A5: for y being object holds
y in Y iff y in the carrier of N & [x,y] in Flow N;
A6: for y being object holds y in Y implies y in X
proof let y be object;
assume y in Y;
then y in the carrier of N & [x,y] in Flow N by A5;
hence thesis by A4;
end;
for y being object holds y in X implies y in Y
proof let y be object;
assume y in X;
then y in the carrier of N & [x,y] in Flow N by A4;
hence thesis by A5;
end;
hence thesis by A6,TARSKI:2;
end;
end;
definition
let N be Pnet;
let X be set;
func Entr(N,X) -> set means
:Def13:
x in it iff x c= Elements N & ex y being
Element of Elements N st y in X & x = enter(N,y);
existence
proof
defpred P[set] means ex y being Element of Elements N st y in X & $1 =
enter(N,y);
consider F being Subset-Family of Elements N such that
A1: for x being Subset of Elements N holds x in F iff P[x] from
SUBSET_1:sch 3;
take F;
thus thesis by A1;
end;
uniqueness
proof
let W,Y be set such that
A2: for x holds x in W iff x c= Elements N & ex y being Element of
Elements(N) st y in X & x = enter(N,y) and
A3: for x holds x in Y iff x c= Elements N & ex y being Element of
Elements(N) st y in X & x = enter(N,y);
A4: for x being object holds x in Y implies x in W
proof let x be object;
reconsider xx = x as set by TARSKI:1;
assume x in Y;
then
xx c= Elements N & ex y being Element of Elements(N) st y in X & x =
enter(N, y) by A3;
hence thesis by A2;
end;
for x being object holds x in W implies x in Y
proof let x be object;
reconsider xx = x as set by TARSKI:1;
assume x in W;
then
xx c= Elements N & ex y being Element of Elements(N) st y in X & x =
enter(N, y) by A2;
hence thesis by A3;
end;
hence thesis by A4,TARSKI:2;
end;
func Ext(N,X) -> set means
:Def14:
x in it iff x c= Elements N & ex y being Element
of Elements N st y in X & x = exit(N,y);
existence
proof
defpred P[set] means ex y being Element of Elements N st y in X & $1 =
exit(N,y);
consider F being Subset-Family of Elements N such that
A5: for x being Subset of Elements N holds x in F iff P[x] from
SUBSET_1:sch 3;
take F;
thus thesis by A5;
end;
uniqueness
proof
let W,Y be set such that
A6: for x holds x in W iff x c= Elements N & ex y being Element of
Elements(N) st y in X & x = exit(N,y) and
A7: for x holds x in Y iff x c= Elements N & ex y being Element of
Elements(N) st y in X & x = exit(N,y);
A8: for x being object holds x in Y implies x in W
proof let x be object;
reconsider xx = x as set by TARSKI:1;
assume x in Y;
then
xx c= Elements N & ex y being Element of Elements(N) st y in X & x =
exit(N,y ) by A7;
hence thesis by A6;
end;
for x being object holds x in W implies x in Y
proof let x be object;
reconsider xx = x as set by TARSKI:1;
assume x in W;
then
xx c= Elements N & ex y being Element of Elements(N) st y in X & x =
exit(N,y ) by A6;
hence thesis by A7;
end;
hence thesis by A8,TARSKI:2;
end;
end;
theorem Th21:
for N being Pnet for x being Element of Elements(N) for X being
set holds Elements(N) <> {} & x in X implies enter(N,x) in Entr(N,X)
proof
let N be Pnet;
let x be Element of Elements(N);
let X be set;
assume that
A1: Elements(N) <> {} and
A2: x in X;
enter(N,x) c= Elements N by A1,Th16;
hence thesis by A2,Def13;
end;
theorem Th22:
for N being Pnet for x being Element of Elements(N) for X being
set holds Elements(N) <> {} & x in X implies exit(N,x) in Ext(N,X)
proof
let N be Pnet;
let x be Element of Elements(N);
let X be set;
assume that
A1: Elements(N) <> {} and
A2: x in X;
exit(N,x) c= Elements N by A1,Th19;
hence thesis by A2,Def14;
end;
definition
let N be Pnet;
let X be set;
func Input(N,X) -> set equals
union Entr(N,X);
correctness;
func Output(N,X) -> set equals
union Ext(N,X);
correctness;
end;
theorem
for N being Pnet for x for X being set holds X c= Elements(N) implies
(x in Input(N,X) iff ex y being Element of Elements(N) st y in X & x in enter(N
,y))
proof
let N be Pnet;
let x;
let X be set;
A1: x in Input(N,X) implies ex y being Element of Elements(N) st y in X & x
in enter(N,y)
proof
assume x in Input(N,X);
then consider y being set such that
A2: x in y and
A3: y in Entr(N,X) by TARSKI:def 4;
ex z being Element of Elements(N) st z in X & y = enter(N,z) by A3,Def13;
hence thesis by A2;
end;
assume
A4: X c= Elements(N);
(ex y being Element of Elements(N) st y in X & x in enter(N,y)) implies
x in Input(N,X)
proof
given y being Element of Elements(N) such that
A5: y in X and
A6: x in enter(N,y);
enter(N,y) in Entr(N,X) by A4,A5,Th21;
hence thesis by A6,TARSKI:def 4;
end;
hence thesis by A1;
end;
theorem
for N being Pnet for x for X being set holds X c= Elements(N) implies
(x in Output(N,X) iff ex y being Element of Elements(N) st y in X & x in exit(N
,y))
proof
let N be Pnet;
let x;
let X be set;
A1: x in Output(N,X) implies ex y being Element of Elements(N) st y in X & x
in exit(N,y)
proof
assume x in Output(N,X);
then consider y being set such that
A2: x in y and
A3: y in Ext(N,X) by TARSKI:def 4;
ex z being Element of Elements(N) st z in X & y = exit(N,z) by A3,Def14;
hence thesis by A2;
end;
assume
A4: X c= Elements(N);
(ex y being Element of Elements(N) st y in X & x in exit(N,y)) implies x
in Output(N,X)
proof
given y being Element of Elements(N) such that
A5: y in X and
A6: x in exit(N,y);
exit(N,y) in Ext(N,X) by A4,A5,Th22;
hence thesis by A6,TARSKI:def 4;
end;
hence thesis by A1;
end;
theorem
for N being Pnet for X being Subset of Elements(N) for x being Element
of Elements(N) holds Elements(N) <> {} implies (x in Input(N,X) iff (x in X & x
in the carrier of N or ex y being Element of Elements(N) st y in X & y in the
carrier' of N & pre N,y,x))
proof
let N be Pnet;
let X be Subset of Elements(N);
let x be Element of Elements(N);
A1: (x in X & x in the carrier of N or ex y being Element of Elements(N) st
y in X & y in the carrier' of N & pre N,y,x) implies x in Input(N,X)
proof
A2: (ex y being Element of Elements(N) st y in X & y in the carrier'
of N & pre N,y,x) implies x in Input(N,X)
proof
given y being Element of Elements(N) such that
A3: y in X and
A4: y in the carrier' of N and
A5: pre N,y,x;
[x,y] in Flow N by A5;
then x in Pre(N,y) by A4,Def6;
then
A6: x in enter(N,y) by A4,Def8;
enter(N,y) in Entr(N,X) by A3,Th21;
hence thesis by A6,TARSKI:def 4;
end;
A7: x in X & x in the carrier of N implies x in Input(N,X)
proof
assume that
A8: x in X and
A9: x in the carrier of N;
enter(N,x) = {x} & {x} c= Elements(N) by A9,Def8,ZFMISC_1:31;
then
A10: {x} in Entr(N,X) by A8,Def13;
x in {x} by TARSKI:def 1;
hence thesis by A10,TARSKI:def 4;
end;
assume x in X & x in the carrier of N or ex y being Element of Elements(N
) st y in X & y in the carrier' of N & pre N,y,x;
hence thesis by A7,A2;
end;
assume
A11: Elements(N) <> {};
x in Input(N,X) implies x in X & x in the carrier of N or ex y being
Element of Elements(N) st y in X & y in the carrier' of N & pre N,y,x
proof
assume x in Input(N,X);
then ex y being set st x in y & y in Entr(N,X) by TARSKI:def 4;
then consider y being set such that
A12: y in Entr(N,X) and
A13: x in y;
consider z being Element of Elements(N) such that
A14: z in X and
A15: y = enter(N,z) by A12,Def13;
A16: z in the carrier' of N implies y = Pre(N,z) by A15,Def8;
A17: z in the carrier' of N implies ex y being Element of Elements(N)
st y in X & y in the carrier' of N & pre N,y,x
proof
assume
A18: z in the carrier' of N;
take z;
[x,z] in Flow N by A13,A16,A18,Def6;
hence thesis by A14,A18;
end;
A19: z in the carrier of N or z in the carrier' of N by A11,XBOOLE_0:def 3;
z in the carrier of N implies y = {z} by A15,Def8;
hence thesis by A13,A14,A19,A17,TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem
for N being Pnet for X being Subset of Elements(N) for x being Element
of Elements(N) holds Elements(N) <> {} implies (x in Output(N,X) iff (x in X &
x in the carrier of N or ex y being Element of Elements(N) st y in X & y in the
carrier' of N & post N,y,x))
proof
let N be Pnet;
let X be Subset of Elements(N);
let x be Element of Elements(N);
A1: (x in X & x in the carrier of N or ex y being Element of Elements(N) st
y in X & y in the carrier' of N & post N,y,x) implies x in Output(N,X)
proof
A2: (ex y being Element of Elements(N) st y in X & y in the carrier'
of N & post N,y,x) implies x in Output(N,X)
proof
given y being Element of Elements(N) such that
A3: y in X and
A4: y in the carrier' of N and
A5: post N,y,x;
[y,x] in Flow N by A5;
then x in Post(N,y) by A4,Def7;
then
A6: x in exit(N,y) by A4,Def9;
exit(N,y) in Ext(N,X) by A3,Th22;
hence thesis by A6,TARSKI:def 4;
end;
A7: x in X & x in the carrier of N implies x in Output(N,X)
proof
assume that
A8: x in X and
A9: x in the carrier of N;
exit(N,x) = {x} & {x} c= Elements(N) by A9,Def9,ZFMISC_1:31;
then
A10: {x} in Ext(N,X) by A8,Def14;
x in {x} by TARSKI:def 1;
hence thesis by A10,TARSKI:def 4;
end;
assume x in X & x in the carrier of N or ex y being Element of Elements(N
) st y in X & y in the carrier' of N & post N,y,x;
hence thesis by A7,A2;
end;
assume
A11: Elements(N) <> {};
x in Output(N,X) implies x in X & x in the carrier of N or ex y being
Element of Elements(N) st y in X & y in the carrier' of N & post N,y,x
proof
assume x in Output(N,X);
then ex y being set st x in y & y in Ext(N,X) by TARSKI:def 4;
then consider y being set such that
A12: y in Ext(N,X) and
A13: x in y;
consider z being Element of Elements(N) such that
A14: z in X and
A15: y = exit(N,z) by A12,Def14;
A16: z in the carrier' of N implies y = Post(N,z) by A15,Def9;
A17: z in the carrier' of N implies ex y being Element of Elements(N)
st y in X & y in the carrier' of N & post N,y,x
proof
assume
A18: z in the carrier' of N;
take z;
[z,x] in Flow N by A13,A16,A18,Def7;
hence thesis by A14,A18;
end;
A19: z in the carrier of N or z in the carrier' of N by A11,XBOOLE_0:def 3;
z in the carrier of N implies y = {z} by A15,Def9;
hence thesis by A13,A14,A19,A17,TARSKI:def 1;
end;
hence thesis by A1;
end;