:: NET_1 semantic presentation
begin
definition
let
P
be ( ( ) ( )
PT_net_Str
) ;
func
Flow
P
->
( ( ) ( )
set
)
equals
:: NET_1:def 1
the
S-T_Arcs
of
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) (
Relation-like
)
Element
of
bool
[:
the
carrier
of
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) , the
carrier'
of
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) )
\/
the
T-S_Arcs
of
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) (
Relation-like
)
Element
of
bool
[:
the
carrier'
of
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) , the
carrier
of
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
Relation-like
)
set
) ;
end;
registration
let
P
be ( ( ) ( )
PT_net_Str
) ;
cluster
Flow
P
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
->
Relation-like
;
end;
definition
let
N
be ( ( ) ( )
PT_net_Str
) ;
attr
N
is
Petri
means
:: NET_1:def 2
( the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
misses
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
c=
[:
the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
)
\/
[:
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
) );
end;
definition
let
N
be ( ( ) ( )
PT_net_Str
) ;
func
Elements
N
->
( ( ) ( )
set
)
equals
:: NET_1:def 3
the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
\/
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
theorem
:: NET_1:1
for
x
being ( ( ) ( )
set
)
for
N
being ( ( ) ( )
PT_net_Str
) holds
( not
Elements
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) or not
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of
Elements
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) or
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of the
carrier
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) or
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of the
carrier'
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) ) ;
theorem
:: NET_1:2
for
x
being ( ( ) ( )
set
)
for
N
being ( ( ) ( )
PT_net_Str
) st
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of the
carrier
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) & the
carrier
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of
Elements
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) ;
theorem
:: NET_1:3
for
x
being ( ( ) ( )
set
)
for
N
being ( ( ) ( )
PT_net_Str
) st
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of the
carrier'
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) & the
carrier'
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
x
: ( ( ) ( )
set
) is ( ( ) ( )
Element
of
Elements
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) ;
registration
cluster
PT_net_Str
(#
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ,
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ,
(
{}
(
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ,
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) )
)
: ( ( ) (
Relation-like
)
Element
of
bool
[:
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ,
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
{}
(
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ,
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) )
)
: ( ( ) (
Relation-like
)
Element
of
bool
[:
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ,
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
PT_net_Str
)
->
strict
Petri
;
end;
registration
cluster
strict
Petri
for ( ( ) ( )
PT_net_Str
) ;
end;
definition
mode
Pnet
is
( (
Petri
) (
Petri
)
PT_net_Str
) ;
end;
theorem
:: NET_1:4
for
x
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
) holds
( not
x
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) or not
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
theorem
:: NET_1:5
for
x
,
y
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
) st
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
y
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:6
for
x
,
y
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
) st
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
y
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
x
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:7
for
x
,
y
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
) st
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
y
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:8
for
x
,
y
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
) st
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
y
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
definition
let
N
be ( (
Petri
) (
Petri
)
Pnet
) ;
let
x
,
y
be ( ( ) ( )
set
) ;
pred
pre
N
,
x
,
y
means
:: NET_1:def 4
(
[
y
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) );
pred
post
N
,
x
,
y
means
:: NET_1:def 5
(
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) )
]
: ( ( ) ( )
set
)
in
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) );
end;
definition
let
N
be ( ( ) ( )
PT_net_Str
) ;
let
x
be ( ( ) ( )
Element
of
Elements
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) ;
func
Pre
(
N
,
x
)
->
( ( ) ( )
set
)
means
:: NET_1:def 6
for
y
being ( ( ) ( )
set
) holds
(
y
: ( ( ) ( )
set
)
in
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) iff (
y
: ( ( ) ( )
set
)
in
Elements
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) );
func
Post
(
N
,
x
)
->
( ( ) ( )
set
)
means
:: NET_1:def 7
for
y
being ( ( ) ( )
set
) holds
(
y
: ( ( ) ( )
set
)
in
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) iff (
y
: ( ( ) ( )
set
)
in
Elements
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) );
end;
theorem
:: NET_1:9
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) holds
Pre
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:10
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) holds
Pre
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:11
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) holds
Post
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:12
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) holds
Post
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:13
for
x
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
y
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
Elements
b
2
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Pre
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
2
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) iff
pre
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
2
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ,
x
: ( ( ) ( )
set
) ) ;
theorem
:: NET_1:14
for
x
being ( ( ) ( )
set
)
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
y
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
y
: ( ( ) ( )
Element
of
Elements
b
2
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Post
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
2
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) iff
post
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
2
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ,
x
: ( ( ) ( )
set
) ) ;
definition
let
N
be ( (
Petri
) (
Petri
)
Pnet
) ;
let
x
be ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
assume
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ;
func
enter
(
N
,
x
)
->
( ( ) ( )
set
)
means
:: NET_1:def 8
( (
x
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) implies
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) )
=
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ) & (
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) implies
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Pre
(
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) );
end;
theorem
:: NET_1:15
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) holds
( not
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) or
enter
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
=
{
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
}
: ( ( ) ( non
empty
)
set
) or
enter
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
=
Pre
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: NET_1:16
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
enter
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:17
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
enter
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
definition
let
N
be ( (
Petri
) (
Petri
)
Pnet
) ;
let
x
be ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
assume
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) ;
func
exit
(
N
,
x
)
->
( ( ) ( )
set
)
means
:: NET_1:def 9
( (
x
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) implies
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) )
=
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ) & (
x
: ( ( ) ( )
set
)
in
the
carrier'
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) implies
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) )
=
Post
(
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) );
end;
theorem
:: NET_1:18
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) holds
( not
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) or
exit
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
=
{
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
}
: ( ( ) ( non
empty
)
set
) or
exit
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
=
Post
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ;
theorem
:: NET_1:19
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
exit
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
theorem
:: NET_1:20
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
exit
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ;
definition
let
N
be ( (
Petri
) (
Petri
)
Pnet
) ;
let
x
be ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
func
field
(
N
,
x
)
->
( ( ) ( )
set
)
equals
:: NET_1:def 10
(
enter
(
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
set
)
\/
(
exit
(
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
definition
let
N
be ( ( ) ( )
PT_net_Str
) ;
let
x
be ( ( ) ( )
Element
of the
carrier'
of
N
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ) ;
func
Prec
(
N
,
x
)
->
( ( ) ( )
set
)
means
:: NET_1:def 11
for
y
being ( ( ) ( )
set
) holds
(
y
: ( ( ) ( )
set
)
in
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) iff (
y
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
[
y
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) );
func
Postc
(
N
,
x
)
->
( ( ) ( )
set
)
means
:: NET_1:def 12
for
y
being ( ( ) ( )
set
) holds
(
y
: ( ( ) ( )
set
)
in
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
x
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) iff (
y
: ( ( ) ( )
set
)
in
the
carrier
of
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) &
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) );
end;
definition
let
N
be ( (
Petri
) (
Petri
)
Pnet
) ;
let
X
be ( ( ) ( )
set
) ;
func
Entr
(
N
,
X
)
->
( ( ) ( )
set
)
means
:: NET_1:def 13
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) iff (
x
: ( ( ) ( )
set
)
c=
Elements
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) & ex
y
being ( ( ) ( )
Element
of
Elements
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) st
(
y
: ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
=
enter
(
N
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ) );
func
Ext
(
N
,
X
)
->
( ( ) ( )
set
)
means
:: NET_1:def 14
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
it
: ( ( ) (
Relation-like
)
Element
of
bool
[:
N
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) iff (
x
: ( ( ) ( )
set
)
c=
Elements
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) & ex
y
being ( ( ) ( )
Element
of
Elements
N
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) st
(
y
: ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
=
exit
(
N
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ) );
end;
theorem
:: NET_1:21
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
for
X
being ( ( ) ( )
set
) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) &
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
set
) holds
enter
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
in
Entr
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
theorem
:: NET_1:22
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
for
X
being ( ( ) ( )
set
) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) &
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
set
) holds
exit
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
in
Ext
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ;
definition
let
N
be ( (
Petri
) (
Petri
)
Pnet
) ;
let
X
be ( ( ) ( )
set
) ;
func
Input
(
N
,
X
)
->
( ( ) ( )
set
)
equals
:: NET_1:def 15
union
(
Entr
(
N
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
func
Output
(
N
,
X
)
->
( ( ) ( )
set
)
equals
:: NET_1:def 16
union
(
Ext
(
N
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
) )
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
theorem
:: NET_1:23
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
,
X
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Input
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) iff ex
y
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
(
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
enter
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: NET_1:24
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
x
,
X
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
)
c=
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
Output
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
X
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) iff ex
y
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
(
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
exit
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: NET_1:25
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
(
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
Input
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) iff ( (
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) or ex
y
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
(
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
pre
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: NET_1:26
for
N
being ( (
Petri
) (
Petri
)
Pnet
)
for
X
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
<>
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
)
set
) holds
(
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
Output
(
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
set
) iff ( (
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
the
carrier
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) or ex
y
being ( ( ) ( )
Element
of
Elements
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) st
(
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
X
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) )
in
the
carrier'
of
N
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
post
N
: ( (
Petri
) (
Petri
)
Pnet
) ,
y
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ,
x
: ( ( ) ( )
Element
of
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) ) ) ;