:: PETRI semantic presentation begin definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "r" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "r" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionattr "c1" is :::"strict"::: ; struct :::"PT_net_Str"::: -> ($#l5_struct_0 :::"2-sorted"::: ) ; aggr :::"PT_net_Str":::(# :::"carrier":::, :::"carrier'":::, :::"S-T_Arcs":::, :::"T-S_Arcs"::: #) -> ($#l1_petri :::"PT_net_Str"::: ) ; sel :::"S-T_Arcs"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); sel :::"T-S_Arcs"::: "c1" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionlet "N" be ($#l1_petri :::"PT_net_Str"::: ) ; attr "N" is :::"with_S-T_arc"::: means :: PETRI:def 1 (Bool (Bool "not" (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "N") "is" ($#v1_xboole_0 :::"empty"::: ) )); attr "N" is :::"with_T-S_arc"::: means :: PETRI:def 2 (Bool (Bool "not" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "N") "is" ($#v1_xboole_0 :::"empty"::: ) )); end; :: deftheorem defines :::"with_S-T_arc"::: PETRI:def 1 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v2_petri :::"with_S-T_arc"::: ) ) "iff" (Bool (Bool "not" (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )); :: deftheorem defines :::"with_T-S_arc"::: PETRI:def 2 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v3_petri :::"with_T-S_arc"::: ) ) "iff" (Bool (Bool "not" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )); definitionfunc :::"TrivialPetriNet"::: -> ($#l1_petri :::"PT_net_Str"::: ) equals :: PETRI:def 3 (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k2_partit_2 :::"[#]"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ")" ) "," (Set "(" ($#k2_partit_2 :::"[#]"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"TrivialPetriNet"::: PETRI:def 3 : (Bool (Set ($#k1_petri :::"TrivialPetriNet"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k2_partit_2 :::"[#]"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ")" ) "," (Set "(" ($#k2_partit_2 :::"[#]"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ")" ) "#)" )); registration cluster (Set ($#k1_petri :::"TrivialPetriNet"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_petri :::"strict"::: ) ($#v2_petri :::"with_S-T_arc"::: ) ($#v3_petri :::"with_T-S_arc"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_petri :::"strict"::: ) ($#v2_petri :::"with_S-T_arc"::: ) ($#v3_petri :::"with_T-S_arc"::: ) for ($#l1_petri :::"PT_net_Str"::: ) ; end; registrationlet "N" be ($#v2_petri :::"with_S-T_arc"::: ) ($#l1_petri :::"PT_net_Str"::: ) ; cluster (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "N") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "N" be ($#v3_petri :::"with_T-S_arc"::: ) ($#l1_petri :::"PT_net_Str"::: ) ; cluster (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "N") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionmode Petri_net is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_petri :::"with_S-T_arc"::: ) ($#v3_petri :::"with_T-S_arc"::: ) ($#l1_petri :::"PT_net_Str"::: ) ; end; definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); mode place of "PTN" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PTN"); mode places of "PTN" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PTN"); mode transition of "PTN" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "PTN"); mode transitions of "PTN" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "PTN"); mode S-T_arc of "PTN" is ($#m1_petri :::"Element"::: ) "of" (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "PTN"); mode T-S_arc of "PTN" is ($#m1_petri :::"Element"::: ) "of" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "PTN"); end; definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "x" be ($#m1_petri :::"S-T_arc":::) "of" (Set (Const "PTN")); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"place":::) "of" "PTN"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"transition":::) "of" "PTN"; end; definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "x" be ($#m1_petri :::"T-S_arc":::) "of" (Set (Const "PTN")); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"transition":::) "of" "PTN"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"place":::) "of" "PTN"; end; definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "S0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PTN"))); func :::"*'"::: "S0" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "PTN") equals :: PETRI:def 4 "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"transition":::) "of" "PTN" : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"T-S_arc":::) "of" "PTN"(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" "PTN" "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "S0") & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ; func "S0" :::"*'"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "PTN") equals :: PETRI:def 5 "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"transition":::) "of" "PTN" : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"S-T_arc":::) "of" "PTN"(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" "PTN" "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "S0") & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ; end; :: deftheorem defines :::"*'"::: PETRI:def 4 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set ($#k6_petri :::"*'"::: ) (Set (Var "S0"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"T-S_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "S0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ))); :: deftheorem defines :::"*'"::: PETRI:def 5 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set (Var "S0")) ($#k7_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"S-T_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "S0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ))); theorem :: PETRI:1 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set ($#k6_petri :::"*'"::: ) (Set (Var "S0"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k4_petri :::"`1"::: ) ")" ) where f "is" ($#m1_petri :::"T-S_arc":::) "of" (Set (Var "PTN")) : (Bool (Set (Set (Var "f")) ($#k5_petri :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S0"))) "}" ))) ; theorem :: PETRI:2 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_petri :::"*'"::: ) (Set (Var "S0")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"T-S_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "S0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" )))) ; theorem :: PETRI:3 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set (Var "S0")) ($#k7_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k3_petri :::"`2"::: ) ")" ) where f "is" ($#m1_petri :::"S-T_arc":::) "of" (Set (Var "PTN")) : (Bool (Set (Set (Var "f")) ($#k2_petri :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S0"))) "}" ))) ; theorem :: PETRI:4 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S0")) ($#k7_petri :::"*'"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"S-T_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "S0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" )))) ; definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "T0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "PTN"))); func :::"*'"::: "T0" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PTN") equals :: PETRI:def 6 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"place":::) "of" "PTN" : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"S-T_arc":::) "of" "PTN"(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" "PTN" "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "T0") & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ; func "T0" :::"*'"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PTN") equals :: PETRI:def 7 "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"place":::) "of" "PTN" : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"T-S_arc":::) "of" "PTN"(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" "PTN" "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "T0") & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ; end; :: deftheorem defines :::"*'"::: PETRI:def 6 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set ($#k8_petri :::"*'"::: ) (Set (Var "T0"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"S-T_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ))); :: deftheorem defines :::"*'"::: PETRI:def 7 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set (Var "T0")) ($#k9_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "s")) where s "is" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) : (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"T-S_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "t")) "," (Set (Var "s")) ($#k1_domain_1 :::"]"::: ) )) ")" ))) "}" ))); theorem :: PETRI:5 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set ($#k8_petri :::"*'"::: ) (Set (Var "T0"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k2_petri :::"`1"::: ) ")" ) where f "is" ($#m1_petri :::"S-T_arc":::) "of" (Set (Var "PTN")) : (Bool (Set (Set (Var "f")) ($#k3_petri :::"`2"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T0"))) "}" ))) ; theorem :: PETRI:6 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_petri :::"*'"::: ) (Set (Var "T0")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"S-T_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" )))) ; theorem :: PETRI:7 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set (Var "T0")) ($#k9_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k5_petri :::"`2"::: ) ")" ) where f "is" ($#m1_petri :::"T-S_arc":::) "of" (Set (Var "PTN")) : (Bool (Set (Set (Var "f")) ($#k4_petri :::"`1"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T0"))) "}" ))) ; theorem :: PETRI:8 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T0")) ($#k9_petri :::"*'"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_petri :::"T-S_arc":::) "of" (Set (Var "PTN"))(Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T0"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "t")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ")" ))) ")" )))) ; theorem :: PETRI:9 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool (Set ($#k6_petri :::"*'"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PETRI:10 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) ")" ) ($#k7_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PETRI:11 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool (Set ($#k8_petri :::"*'"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PETRI:12 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool (Set (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) ")" ) ($#k9_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; begin definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PTN"))); attr "IT" is :::"Deadlock-like"::: means :: PETRI:def 8 (Bool (Set ($#k6_petri :::"*'"::: ) "IT") "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "IT" ($#k7_petri :::"*'"::: ) ")" )); end; :: deftheorem defines :::"Deadlock-like"::: PETRI:def 8 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_petri :::"Deadlock-like"::: ) ) "iff" (Bool (Set ($#k6_petri :::"*'"::: ) (Set (Var "IT"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "IT")) ($#k7_petri :::"*'"::: ) ")" )) ")" ))); definitionlet "IT" be ($#l1_petri :::"Petri_net":::); attr "IT" is :::"With_Deadlocks"::: means :: PETRI:def 9 (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "st" (Bool (Set (Var "S")) "is" ($#v4_petri :::"Deadlock-like"::: ) )); end; :: deftheorem defines :::"With_Deadlocks"::: PETRI:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_petri :::"With_Deadlocks"::: ) ) "iff" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "st" (Bool (Set (Var "S")) "is" ($#v4_petri :::"Deadlock-like"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_petri :::"with_S-T_arc"::: ) ($#v3_petri :::"with_T-S_arc"::: ) ($#v5_petri :::"With_Deadlocks"::: ) for ($#l1_petri :::"PT_net_Str"::: ) ; end; begin definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PTN"))); attr "IT" is :::"Trap-like"::: means :: PETRI:def 10 (Bool (Set "IT" ($#k7_petri :::"*'"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_petri :::"*'"::: ) "IT" ")" )); end; :: deftheorem defines :::"Trap-like"::: PETRI:def 10 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_petri :::"Trap-like"::: ) ) "iff" (Bool (Set (Set (Var "IT")) ($#k7_petri :::"*'"::: ) ) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_petri :::"*'"::: ) (Set (Var "IT")) ")" )) ")" ))); definitionlet "IT" be ($#l1_petri :::"Petri_net":::); attr "IT" is :::"With_Traps"::: means :: PETRI:def 11 (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "st" (Bool (Set (Var "S")) "is" ($#v6_petri :::"Trap-like"::: ) )); end; :: deftheorem defines :::"With_Traps"::: PETRI:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_petri :::"With_Traps"::: ) ) "iff" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "st" (Bool (Set (Var "S")) "is" ($#v6_petri :::"Trap-like"::: ) )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_petri :::"with_S-T_arc"::: ) ($#v3_petri :::"with_T-S_arc"::: ) ($#v7_petri :::"With_Traps"::: ) for ($#l1_petri :::"PT_net_Str"::: ) ; end; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "r" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"~"::: redefine func "r" :::"~"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Relation":::) "of" "B" "," "A"; end; begin definitionlet "PTN" be ($#l1_petri :::"PT_net_Str"::: ) ; func "PTN" :::".:"::: -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"PT_net_Str"::: ) equals :: PETRI:def 12 (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PTN") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "PTN") "," (Set "(" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "PTN") ($#k3_relset_1 :::"~"::: ) ")" ) "," (Set "(" (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "PTN") ($#k3_relset_1 :::"~"::: ) ")" ) "#)" ); end; :: deftheorem defines :::".:"::: PETRI:def 12 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool (Set (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "," (Set "(" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "PTN"))) ($#k3_relset_1 :::"~"::: ) ")" ) "," (Set "(" (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "PTN"))) ($#k3_relset_1 :::"~"::: ) ")" ) "#)" ))); registrationlet "PTN" be ($#l1_petri :::"Petri_net":::); cluster (Set "PTN" ($#k11_petri :::".:"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_petri :::"strict"::: ) ($#v2_petri :::"with_S-T_arc"::: ) ($#v3_petri :::"with_T-S_arc"::: ) ; end; theorem :: PETRI:13 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool (Set (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ) ($#k11_petri :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "," (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "PTN"))) "," (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "PTN"))) "#)" ))) ; theorem :: PETRI:14 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ))) & (Bool (Set (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "PTN"))) ($#k10_petri :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ))) & (Bool (Set (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "PTN"))) ($#k10_petri :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ))) ")" )) ; definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "S0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PTN"))); func "S0" :::".:"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "PTN" ($#k11_petri :::".:"::: ) ")" )) equals :: PETRI:def 13 "S0"; end; :: deftheorem defines :::".:"::: PETRI:def 13 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set (Var "S0")) ($#k12_petri :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "S0"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "s" be ($#m1_subset_1 :::"place":::) "of" (Set (Const "PTN")); func "s" :::".:"::: -> ($#m1_subset_1 :::"place":::) "of" (Set "(" "PTN" ($#k11_petri :::".:"::: ) ")" ) equals :: PETRI:def 14 "s"; end; :: deftheorem defines :::".:"::: PETRI:def 14 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN")) "holds" (Bool (Set (Set (Var "s")) ($#k13_petri :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "S0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Const "PTN")) ($#k11_petri :::".:"::: ) ")" )); func :::".:"::: "S0" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PTN") equals :: PETRI:def 15 "S0"; end; :: deftheorem defines :::".:"::: PETRI:def 15 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" )) "holds" (Bool (Set ($#k14_petri :::".:"::: ) (Set (Var "S0"))) ($#r1_hidden :::"="::: ) (Set (Var "S0"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "s" be ($#m1_subset_1 :::"place":::) "of" (Set "(" (Set (Const "PTN")) ($#k11_petri :::".:"::: ) ")" ); func :::".:"::: "s" -> ($#m1_subset_1 :::"place":::) "of" "PTN" equals :: PETRI:def 16 "s"; end; :: deftheorem defines :::".:"::: PETRI:def 16 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"place":::) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ) "holds" (Bool (Set ($#k15_petri :::".:"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "T0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "PTN"))); func "T0" :::".:"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "PTN" ($#k11_petri :::".:"::: ) ")" )) equals :: PETRI:def 17 "T0"; end; :: deftheorem defines :::".:"::: PETRI:def 17 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set (Var "T0")) ($#k16_petri :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "T0"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "t" be ($#m1_subset_1 :::"transition":::) "of" (Set (Const "PTN")); func "t" :::".:"::: -> ($#m1_subset_1 :::"transition":::) "of" (Set "(" "PTN" ($#k11_petri :::".:"::: ) ")" ) equals :: PETRI:def 18 "t"; end; :: deftheorem defines :::".:"::: PETRI:def 18 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "holds" (Bool (Set (Set (Var "t")) ($#k17_petri :::".:"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "t"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "T0" be ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Const "PTN")) ($#k11_petri :::".:"::: ) ")" )); func :::".:"::: "T0" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "PTN") equals :: PETRI:def 19 "T0"; end; :: deftheorem defines :::".:"::: PETRI:def 19 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "T0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" )) "holds" (Bool (Set ($#k18_petri :::".:"::: ) (Set (Var "T0"))) ($#r1_hidden :::"="::: ) (Set (Var "T0"))))); definitionlet "PTN" be ($#l1_petri :::"Petri_net":::); let "t" be ($#m1_subset_1 :::"transition":::) "of" (Set "(" (Set (Const "PTN")) ($#k11_petri :::".:"::: ) ")" ); func :::".:"::: "t" -> ($#m1_subset_1 :::"transition":::) "of" "PTN" equals :: PETRI:def 20 "t"; end; :: deftheorem defines :::".:"::: PETRI:def 20 : (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set "(" (Set (Var "PTN")) ($#k11_petri :::".:"::: ) ")" ) "holds" (Bool (Set ($#k19_petri :::".:"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))))); theorem :: PETRI:15 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k12_petri :::".:"::: ) ")" ) ($#k7_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_petri :::"*'"::: ) (Set (Var "S")))))) ; theorem :: PETRI:16 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool (Set ($#k6_petri :::"*'"::: ) (Set "(" (Set (Var "S")) ($#k12_petri :::".:"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k7_petri :::"*'"::: ) )))) ; theorem :: PETRI:17 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v4_petri :::"Deadlock-like"::: ) ) "iff" (Bool (Set (Set (Var "S")) ($#k12_petri :::".:"::: ) ) "is" ($#v6_petri :::"Trap-like"::: ) ) ")" ))) ; theorem :: PETRI:18 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v6_petri :::"Trap-like"::: ) ) "iff" (Bool (Set (Set (Var "S")) ($#k12_petri :::".:"::: ) ) "is" ($#v4_petri :::"Deadlock-like"::: ) ) ")" ))) ; theorem :: PETRI:19 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S0")) ($#k7_petri :::"*'"::: ) )) "iff" (Bool (Set ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S0"))) ")" )))) ; theorem :: PETRI:20 (Bool "for" (Set (Var "PTN")) "being" ($#l1_petri :::"Petri_net":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) (Bool "for" (Set (Var "S0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PTN"))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k6_petri :::"*'"::: ) (Set (Var "S0")))) "iff" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S0"))) ")" )))) ;