:: PETRI semantic presentation
begin
definition
let
A
,
B
be ( ( non
empty
) ( non
empty
)
set
) ;
let
r
be ( ( non
empty
) ( non
empty
Relation-like
A
: ( ( non
empty
) ( non
empty
)
set
)
-defined
B
: ( ( non
empty
) ( non
empty
)
set
)
-valued
)
Relation
of ,) ;
:: original:
Element
redefine
mode
Element
of
r
->
( ( ) ( )
Element
of
[:
A
: ( ( ) ( )
2-sorted
) ,
B
: ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) ;
end;
definition
attr
c
1
is
strict
;
struct
PT_net_Str
->
( ( ) ( )
2-sorted
) ;
aggr
PT_net_Str
(#
carrier
,
carrier'
,
S-T_Arcs
,
T-S_Arcs
#)
->
( (
strict
) (
strict
)
PT_net_Str
) ;
sel
S-T_Arcs
c
1
->
( ( ) (
Relation-like
the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,) ;
sel
T-S_Arcs
c
1
->
( ( ) (
Relation-like
the
carrier'
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,) ;
end;
definition
let
N
be ( ( ) ( )
PT_net_Str
) ;
attr
N
is
with_S-T_arc
means
:: PETRI:def 1
not the
S-T_Arcs
of
N
: ( ( ) ( )
2-sorted
) : ( ( ) (
Relation-like
the
carrier
of
N
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
N
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,) is
empty
;
attr
N
is
with_T-S_arc
means
:: PETRI:def 2
not the
T-S_Arcs
of
N
: ( ( ) ( )
2-sorted
) : ( ( ) (
Relation-like
the
carrier'
of
N
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
N
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,) is
empty
;
end;
definition
func
TrivialPetriNet
->
( ( ) ( )
PT_net_Str
)
equals
:: PETRI:def 3
PT_net_Str
(#
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
(
[#]
(
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
Relation-like
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
)
-defined
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
)
-valued
)
Element
of
bool
[:
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
[#]
(
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( non
empty
Relation-like
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
)
-defined
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
)
-valued
)
Element
of
bool
[:
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
) ,
{
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
)
}
: ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
PT_net_Str
) ;
end;
registration
cluster
TrivialPetriNet
: ( ( ) ( )
PT_net_Str
)
->
non
empty
non
void
strict
with_S-T_arc
with_T-S_arc
;
end;
registration
cluster
non
empty
non
void
strict
with_S-T_arc
with_T-S_arc
for ( ( ) ( )
PT_net_Str
) ;
end;
registration
let
N
be ( (
with_S-T_arc
) (
with_S-T_arc
)
PT_net_Str
) ;
cluster
the
S-T_Arcs
of
N
: ( (
with_S-T_arc
) (
with_S-T_arc
)
PT_net_Str
) : ( ( ) (
Relation-like
the
carrier
of
N
: ( (
with_S-T_arc
) (
with_S-T_arc
)
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
N
: ( (
with_S-T_arc
) (
with_S-T_arc
)
PT_net_Str
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,)
->
non
empty
;
end;
registration
let
N
be ( (
with_T-S_arc
) (
with_T-S_arc
)
PT_net_Str
) ;
cluster
the
T-S_Arcs
of
N
: ( (
with_T-S_arc
) (
with_T-S_arc
)
PT_net_Str
) : ( ( ) (
Relation-like
the
carrier'
of
N
: ( (
with_T-S_arc
) (
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( )
set
)
-defined
the
carrier
of
N
: ( (
with_T-S_arc
) (
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,)
->
non
empty
;
end;
definition
mode
Petri_net
is
( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
mode
place of
PTN
is
( ( ) ( )
Element
of the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
mode
places of
PTN
is
( ( ) ( )
Element
of the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
mode
transition of
PTN
is
( ( ) ( )
Element
of the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
mode
transitions of
PTN
is
( ( ) ( )
Element
of the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
mode
S-T_arc of
PTN
is
( ( ) ( )
Element
of the
S-T_Arcs
of
PTN
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,) ) ;
mode
T-S_arc of
PTN
is
( ( ) ( )
Element
of the
T-S_Arcs
of
PTN
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,) ) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
x
be ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ;
:: original:
`1
redefine
func
x
`1
->
( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) ) ;
:: original:
`2
redefine
func
x
`2
->
( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) ) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
x
be ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ;
:: original:
`1
redefine
func
x
`1
->
( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) ) ;
:: original:
`2
redefine
func
x
`2
->
( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) ) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
S0
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
*'
S0
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 4
{
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
t
is ( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) ) : ex
f
being ( ( ) ( )
T-S_arc
of
PTN
: ( ( ) ( )
set
) ) ex
s
being ( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) ) st
(
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
set
) &
f
: ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ,
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
]
: ( ( ) (
V9
() )
Element
of
[:
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) )
}
;
func
S0
*'
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 5
{
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
t
is ( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) ) : ex
f
being ( ( ) ( )
S-T_arc
of
PTN
: ( ( ) ( )
set
) ) ex
s
being ( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) ) st
(
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
set
) &
f
: ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ,
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
]
: ( ( ) (
V9
() )
Element
of
[:
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) )
}
;
end;
theorem
:: PETRI:1
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
*'
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{
(
f
: ( ( ) ( )
T-S_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`1
)
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
f
is ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) :
f
: ( ( ) ( )
T-S_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`2
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
}
;
theorem
:: PETRI:2
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
*'
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) iff ex
f
being ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ex
s
being ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) st
(
s
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
f
: ( ( ) ( )
T-S_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
x
: ( ( ) ( )
set
) ,
s
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
]
: ( ( ) (
V9
() )
set
) ) ) ;
theorem
:: PETRI:3
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{
(
f
: ( ( ) ( )
S-T_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`2
)
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
f
is ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) :
f
: ( ( ) ( )
S-T_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`1
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
}
;
theorem
:: PETRI:4
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) iff ex
f
being ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ex
s
being ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) st
(
s
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
f
: ( ( ) ( )
S-T_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
s
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) (
V9
() )
set
) ) ) ;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
T0
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
*'
T0
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 6
{
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
s
is ( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) ) : ex
f
being ( ( ) ( )
S-T_arc
of
PTN
: ( ( ) ( )
set
) ) ex
t
being ( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) ) st
(
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
T0
: ( ( ) ( )
set
) &
f
: ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ,
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
]
: ( ( ) (
V9
() )
Element
of
[:
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) )
}
;
func
T0
*'
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 7
{
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
s
is ( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) ) : ex
f
being ( ( ) ( )
T-S_arc
of
PTN
: ( ( ) ( )
set
) ) ex
t
being ( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) ) st
(
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
T0
: ( ( ) ( )
set
) &
f
: ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
t
: ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ,
s
: ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
]
: ( ( ) (
V9
() )
Element
of
[:
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) ) )
}
;
end;
theorem
:: PETRI:5
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
T0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
*'
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{
(
f
: ( ( ) ( )
S-T_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`1
)
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
f
is ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) :
f
: ( ( ) ( )
S-T_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`2
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
}
;
theorem
:: PETRI:6
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
T0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
*'
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) iff ex
f
being ( ( ) ( )
S-T_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ex
t
being ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) st
(
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
f
: ( ( ) ( )
S-T_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
x
: ( ( ) ( )
set
) ,
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
]
: ( ( ) (
V9
() )
set
) ) ) ;
theorem
:: PETRI:7
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
T0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{
(
f
: ( ( ) ( )
T-S_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`2
)
: ( ( ) ( )
place
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) where
f
is ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) :
f
: ( ( ) ( )
T-S_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
`1
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
}
;
theorem
:: PETRI:8
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
T0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( ( ) ( )
set
) holds
(
x
: ( ( ) ( )
set
)
in
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) iff ex
f
being ( ( ) ( )
T-S_arc
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ex
t
being ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) st
(
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
T0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) &
f
: ( ( ) ( )
T-S_arc
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
=
[
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ,
x
: ( ( ) ( )
set
)
]
: ( ( ) (
V9
() )
set
) ) ) ;
theorem
:: PETRI:9
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) holds
*'
(
{}
the
carrier
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) (
empty
proper
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
) ;
theorem
:: PETRI:10
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) holds
(
{}
the
carrier
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) (
empty
proper
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
) ;
theorem
:: PETRI:11
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) holds
*'
(
{}
the
carrier'
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) (
empty
proper
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
Element
of
bool
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
) ;
theorem
:: PETRI:12
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) holds
(
{}
the
carrier'
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
)
: ( ( ) (
empty
proper
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
Element
of
bool
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
{}
: ( ( ) (
empty
Relation-like
non-empty
empty-yielding
V55
()
V58
()
V61
() )
set
) ;
begin
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
IT
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
Deadlock-like
means
:: PETRI:def 8
*'
IT
: ( ( ) ( )
set
) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
IT
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
attr
IT
is
With_Deadlocks
means
:: PETRI:def 9
ex
S
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) st
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is
Deadlock-like
;
end;
registration
cluster
non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
With_Deadlocks
for ( ( ) ( )
PT_net_Str
) ;
end;
begin
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
IT
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
Trap-like
means
:: PETRI:def 10
IT
: ( ( ) ( )
set
)
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
IT
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
attr
IT
is
With_Traps
means
:: PETRI:def 11
ex
S
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) st
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is
Trap-like
;
end;
registration
cluster
non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
With_Traps
for ( ( ) ( )
PT_net_Str
) ;
end;
definition
let
A
,
B
be ( ( non
empty
) ( non
empty
)
set
) ;
let
r
be ( ( non
empty
) ( non
empty
Relation-like
A
: ( ( non
empty
) ( non
empty
)
set
)
-defined
B
: ( ( non
empty
) ( non
empty
)
set
)
-valued
)
Relation
of ,) ;
:: original:
~
redefine
func
r
~
->
( ( non
empty
) ( non
empty
Relation-like
B
: ( ( ) ( )
set
)
-defined
A
: ( ( ) ( )
set
)
-valued
)
Relation
of ,) ;
end;
begin
definition
let
PTN
be ( ( ) ( )
PT_net_Str
) ;
func
PTN
.:
->
( (
strict
) (
strict
)
PT_net_Str
)
equals
:: PETRI:def 12
PT_net_Str
(# the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ,
(
the
T-S_Arcs
of
PTN
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,)
~
)
: ( ( ) (
Relation-like
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
)
Element
of
bool
[:
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
(
the
S-T_Arcs
of
PTN
: ( ( ) ( )
set
) : ( ( ) (
Relation-like
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
)
Relation
of ,)
~
)
: ( ( ) (
Relation-like
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
)
Element
of
bool
[:
the
carrier'
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
PTN
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
PT_net_Str
) ;
end;
registration
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
cluster
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
PT_net_Str
)
.:
: ( (
strict
) (
strict
)
PT_net_Str
)
->
non
empty
non
void
strict
with_S-T_arc
with_T-S_arc
;
end;
theorem
:: PETRI:13
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) holds
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
)
.:
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
)
=
PT_net_Str
(# the
carrier
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) , the
carrier'
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) , the
S-T_Arcs
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,) , the
T-S_Arcs
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
Relation-like
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,) #) : ( (
strict
) (
strict
)
PT_net_Str
) ;
theorem
:: PETRI:14
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) holds
( the
carrier
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
=
the
carrier
of
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
)
set
) & the
carrier'
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
=
the
carrier'
of
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
)
set
) & the
S-T_Arcs
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,)
~
: ( ( non
empty
) ( non
empty
Relation-like
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,)
=
the
T-S_Arcs
of
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
Relation-like
the
carrier'
of
(
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,) & the
T-S_Arcs
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
Relation-like
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,)
~
: ( ( non
empty
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,)
=
the
S-T_Arcs
of
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
Relation-like
the
carrier
of
(
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier'
of
(
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) : ( ( ) ( non
empty
)
set
)
-valued
)
Relation
of ,) ) ;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
S0
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
S0
.:
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 13
S0
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
s
be ( ( ) ( )
place
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ;
func
s
.:
->
( ( ) ( )
place
of
(
PTN
: ( ( ) ( )
set
)
.:
)
: ( (
strict
) (
strict
)
PT_net_Str
) )
equals
:: PETRI:def 14
s
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
S0
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
.:
S0
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 15
S0
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
s
be ( ( ) ( )
place
of
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) ) ;
func
.:
s
->
( ( ) ( )
place
of
PTN
: ( ( ) ( )
set
) )
equals
:: PETRI:def 16
s
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
T0
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
T0
.:
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 17
T0
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
t
be ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ) ;
func
t
.:
->
( ( ) ( )
transition
of
(
PTN
: ( ( ) ( )
set
)
.:
)
: ( (
strict
) (
strict
)
PT_net_Str
) )
equals
:: PETRI:def 18
t
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
T0
be ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
.:
T0
->
( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: PETRI:def 19
T0
: ( ( ) ( )
set
) ;
end;
definition
let
PTN
be ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) ;
let
t
be ( ( ) ( )
transition
of
(
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
.:
)
: ( (
strict
) ( non
empty
non
void
V49
()
strict
with_S-T_arc
with_T-S_arc
)
PT_net_Str
) ) ;
func
.:
t
->
( ( ) ( )
transition
of
PTN
: ( ( ) ( )
set
) )
equals
:: PETRI:def 20
t
: ( ( ) ( )
set
) ;
end;
theorem
:: PETRI:15
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
.:
)
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
*'
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: PETRI:16
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
*'
(
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
.:
)
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
=
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: PETRI:17
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is
Deadlock-like
iff
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
.:
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is
Trap-like
) ;
theorem
:: PETRI:18
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
S
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is
Trap-like
iff
S
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
.:
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) is
Deadlock-like
) ;
theorem
:: PETRI:19
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
t
being ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
for
S0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) iff
*'
{
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
}
: ( ( ) ( non
empty
)
Element
of
bool
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
meets
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: PETRI:20
for
PTN
being ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
)
for
t
being ( ( ) ( )
transition
of
PTN
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
for
S0
being ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
in
*'
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) iff
{
t
: ( ( ) ( )
transition
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) )
}
: ( ( ) ( non
empty
)
Element
of
bool
the
carrier'
of
b
1
: ( ( non
empty
non
void
with_S-T_arc
with_T-S_arc
) ( non
empty
non
void
V49
()
with_S-T_arc
with_T-S_arc
)
Petri_net
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*'
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) )
meets
S0
: ( ( ) ( )
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;