:: FF_SIEC semantic presentation
begin
definition
let
X
,
Y
be ( ( ) ( )
set
) ;
assume
X
: ( ( ) ( )
set
)
misses
Y
: ( ( ) ( )
set
) ;
func
PTempty_f_net
(
X
,
Y
)
->
( (
strict
Petri
) (
strict
Petri
)
Pnet
)
equals
:: FF_SIEC:def 1
PT_net_Str
(#
X
: ( ( ) ( )
PT_net_Str
) ,
Y
: ( ( ) ( )
set
) ,
(
{}
(
X
: ( ( ) ( )
PT_net_Str
) ,
Y
: ( ( ) ( )
set
) )
)
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V63
()
V66
()
V69
() )
M2
(
bool
[:
X
: ( ( ) ( )
PT_net_Str
) ,
Y
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( )
set
) )) ,
(
{}
(
Y
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
PT_net_Str
) )
)
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V63
()
V66
()
V69
() )
M2
(
bool
[:
Y
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
PT_net_Str
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( )
set
) )) #) : ( (
strict
) (
strict
)
PT_net_Str
) ;
end;
definition
let
X
be ( ( ) ( )
set
) ;
func
Tempty_f_net
X
->
( (
strict
Petri
) (
strict
Petri
)
Pnet
)
equals
:: FF_SIEC:def 2
PTempty_f_net
(
X
: ( ( ) ( )
PT_net_Str
) ,
{}
: ( ( ) ( )
set
) ) : ( (
strict
Petri
) (
strict
Petri
)
Pnet
) ;
func
Pempty_f_net
X
->
( (
strict
Petri
) (
strict
Petri
)
Pnet
)
equals
:: FF_SIEC:def 3
PTempty_f_net
(
{}
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
PT_net_Str
) ) : ( (
strict
Petri
) (
strict
Petri
)
Pnet
) ;
end;
definition
let
x
be ( ( ) ( )
set
) ;
func
Tsingle_f_net
x
->
( (
strict
Petri
) (
strict
Petri
)
Pnet
)
equals
:: FF_SIEC:def 4
PTempty_f_net
(
{}
: ( ( ) ( )
set
) ,
{
x
: ( ( ) ( )
PT_net_Str
)
}
: ( ( ) ( )
set
) ) : ( (
strict
Petri
) (
strict
Petri
)
Pnet
) ;
func
Psingle_f_net
x
->
( (
strict
Petri
) (
strict
Petri
)
Pnet
)
equals
:: FF_SIEC:def 5
PTempty_f_net
(
{
x
: ( ( ) ( )
PT_net_Str
)
}
: ( ( ) ( )
set
) ,
{}
: ( ( ) ( )
set
) ) : ( (
strict
Petri
) (
strict
Petri
)
Pnet
) ;
end;
definition
func
empty_f_net
->
( (
strict
Petri
) (
strict
Petri
)
Pnet
)
equals
:: FF_SIEC:def 6
PTempty_f_net
(
{}
: ( ( ) ( )
set
) ,
{}
: ( ( ) ( )
set
) ) : ( (
strict
Petri
) (
strict
Petri
)
Pnet
) ;
end;
theorem
:: FF_SIEC:1
for
X
,
Y
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
)
misses
Y
: ( ( ) ( )
set
) holds
( the
carrier
of
(
PTempty_f_net
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) )
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
X
: ( ( ) ( )
set
) & the
carrier'
of
(
PTempty_f_net
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) )
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
Y
: ( ( ) ( )
set
) &
Flow
(
PTempty_f_net
(
X
: ( ( ) ( )
set
) ,
Y
: ( ( ) ( )
set
) )
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:2
for
X
being ( ( ) ( )
set
) holds
( the
carrier
of
(
Tempty_f_net
X
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
X
: ( ( ) ( )
set
) & the
carrier'
of
(
Tempty_f_net
X
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
set
) &
Flow
(
Tempty_f_net
X
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:3
for
X
being ( ( ) ( )
set
) holds
( the
carrier
of
(
Pempty_f_net
X
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
set
) & the
carrier'
of
(
Pempty_f_net
X
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
X
: ( ( ) ( )
set
) &
Flow
(
Pempty_f_net
X
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:4
for
x
being ( ( ) ( )
set
) holds
( the
carrier
of
(
Tsingle_f_net
x
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
set
) & the
carrier'
of
(
Tsingle_f_net
x
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) &
Flow
(
Tsingle_f_net
x
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:5
for
x
being ( ( ) ( )
set
) holds
( the
carrier
of
(
Psingle_f_net
x
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( )
set
) & the
carrier'
of
(
Psingle_f_net
x
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
set
) &
Flow
(
Psingle_f_net
x
: ( ( ) ( )
set
)
)
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:6
( the
carrier
of
empty_f_net
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
set
) & the
carrier'
of
empty_f_net
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) ( )
set
)
=
{}
: ( ( ) ( )
set
) &
Flow
empty_f_net
: ( (
strict
Petri
) (
strict
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:7
for
x
,
y
being ( ( ) ( )
set
)
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
( (
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) implies ( not
x
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) & not
y
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) & (
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
y
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) implies ( not
y
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) & not
x
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) & (
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) implies ( not
y
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) & not
x
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
y
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) & (
[
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
set
)
]
: ( ( ) ( )
set
)
in
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
y
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) implies ( not
x
: ( ( ) ( )
set
)
in
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) & not
y
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: FF_SIEC:8
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) &
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) ;
theorem
:: FF_SIEC:9
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
c=
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
c=
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
c=
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
c=
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
)
c=
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
dom
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
)
c=
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
)
c=
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
dom
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
)
c=
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:10
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
dom
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) &
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
) &
dom
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) ( )
set
)
misses
rng
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:11
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:12
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
*
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
*
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:13
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
misses
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) &
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
misses
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
misses
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) &
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
misses
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) ) ;
theorem
:: FF_SIEC:14
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) ) ;
theorem
:: FF_SIEC:15
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
)
=
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) ) ;
theorem
:: FF_SIEC:16
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
=
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
=
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
) &
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
(
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
)
=
(
Flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) (
Relation-like
)
set
)
~
: ( (
Relation-like
) (
Relation-like
)
set
) ) ;
definition
let
M
be ( (
Petri
) (
Petri
)
Pnet
) ;
func
f_enter
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 7
(
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
func
f_exit
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 8
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
end;
theorem
:: FF_SIEC:17
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) &
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) ;
theorem
:: FF_SIEC:18
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
dom
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
dom
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:19
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) ) ;
theorem
:: FF_SIEC:20
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
(
f_exit
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
(
f_enter
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
definition
let
M
be ( (
Petri
) (
Petri
)
Pnet
) ;
func
f_prox
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 9
(
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
)
: ( ( ) (
Relation-like
)
set
)
\/
(
id
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
func
f_flow
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 10
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
\/
(
id
(
Elements
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
Elements
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
end;
theorem
:: FF_SIEC:21
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
*
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
)
: ( ( ) (
Relation-like
)
set
)
\/
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
f_flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
(
f_flow
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
) ) ;
definition
let
M
be ( (
Petri
) (
Petri
)
Pnet
) ;
func
f_places
M
->
( ( ) ( )
set
)
equals
:: FF_SIEC:def 11
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ;
func
f_transitions
M
->
( ( ) ( )
set
)
equals
:: FF_SIEC:def 12
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) ;
func
f_pre
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 13
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) ;
func
f_post
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 14
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
) : ( (
Relation-like
) (
Relation-like
)
set
) ;
end;
theorem
:: FF_SIEC:22
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
f_pre
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
f_transitions
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
f_places
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) &
f_post
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
f_transitions
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
f_places
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) ;
theorem
:: FF_SIEC:23
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
f_prox
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) &
f_flow
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) ;
definition
let
M
be ( (
Petri
) (
Petri
)
Pnet
) ;
func
f_entrance
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 15
(
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
func
f_escape
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 16
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
end;
theorem
:: FF_SIEC:24
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) &
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
)
c=
[:
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
) ,
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) ;
theorem
:: FF_SIEC:25
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
dom
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
dom
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) &
rng
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( ( ) ( )
set
)
c=
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
) ) ;
theorem
:: FF_SIEC:26
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) ) ;
theorem
:: FF_SIEC:27
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
(
f_escape
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
(
f_entrance
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) ) ;
notation
let
M
be ( (
Petri
) (
Petri
)
Pnet
) ;
synonym
f_circulation
M
for
f_flow
M
;
end;
definition
let
M
be ( (
Petri
) (
Petri
)
Pnet
) ;
func
f_adjac
M
->
( (
Relation-like
) (
Relation-like
)
Relation
)
equals
:: FF_SIEC:def 17
(
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
\/
(
(
(
Flow
M
: ( ( ) ( )
PT_net_Str
)
)
: ( ( ) (
Relation-like
)
set
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
|
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
)
set
)
)
: ( ( ) (
Relation-like
)
set
)
\/
(
id
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
M
: ( ( ) ( )
PT_net_Str
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
) ;
end;
theorem
:: FF_SIEC:28
for
M
being ( (
Petri
) (
Petri
)
Pnet
) holds
(
(
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
*
(
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
) : ( (
Relation-like
) (
Relation-like
)
Relation
) &
(
(
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
)
)
: ( ( ) (
Relation-like
)
set
)
*
(
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
) : ( (
Relation-like
) (
Relation-like
)
set
)
=
{}
: ( ( ) ( )
set
) &
(
(
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
(
f_adjac
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
)
)
: ( ( ) (
Relation-like
)
set
)
\/
(
id
(
Elements
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( ( ) ( )
set
)
)
: ( (
Relation-like
) (
Relation-like
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-defined
Elements
b
1
: ( (
Petri
) (
Petri
)
Pnet
) : ( ( ) ( )
set
)
-valued
V89
() )
set
) : ( ( ) (
Relation-like
)
set
)
=
(
f_circulation
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
\/
(
(
f_circulation
M
: ( (
Petri
) (
Petri
)
Pnet
)
)
: ( (
Relation-like
) (
Relation-like
)
Relation
)
~
)
: ( (
Relation-like
) (
Relation-like
)
set
) : ( ( ) (
Relation-like
)
set
) ) ;