:: PETRI_2 semantic presentation begin definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B", "Bo" be ($#m1_hidden :::"set"::: ) ; let "yo" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Bo")) "," (Set (Const "A")); assume (Bool (Set (Const "Bo")) ($#r1_tarski :::"c="::: ) (Set (Const "B"))) ; func :::"cylinder0"::: "(" "A" "," "B" "," "Bo" "," "yo" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "B" "," "A" ")" ")" ) equals :: PETRI_2:def 1 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Function":::) "of" "B" "," "A" : (Bool (Set (Set (Var "y")) ($#k2_partfun1 :::"|"::: ) "Bo") ($#r1_hidden :::"="::: ) "yo") "}" ; end; :: deftheorem defines :::"cylinder0"::: PETRI_2:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "Bo")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "yo")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "Bo")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "Bo")) "," (Set (Var "yo")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) : (Bool (Set (Set (Var "y")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo"))) ($#r1_hidden :::"="::: ) (Set (Var "yo"))) "}" )))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"set"::: ) ; mode :::"thin_cylinder"::: "of" "A" "," "B" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "B" "," "A" ")" ")" ) means :: PETRI_2:def 2 (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" "B"(Bool "ex" (Set (Var "yo")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," "A" "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" "A" "," "B" "," (Set (Var "Bo")) "," (Set (Var "yo")) ")" )) ")" ))); end; :: deftheorem defines :::"thin_cylinder"::: PETRI_2:def 2 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B"))(Bool "ex" (Set (Var "yo")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "Bo")) "," (Set (Var "yo")) ")" )) ")" ))) ")" )))); theorem :: PETRI_2:1 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B"))(Bool "ex" (Set (Var "yo")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) : (Bool (Set (Set (Var "y")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo"))) ($#r1_hidden :::"="::: ) (Set (Var "yo"))) "}" ) ")" )))))) ; theorem :: PETRI_2:2 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "being" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Var "A1")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) "holds" (Bool "ex" (Set (Var "D2")) "being" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Var "A2")) "," (Set (Var "B")) "st" (Bool (Set (Var "D1")) ($#r1_tarski :::"c="::: ) (Set (Var "D2"))))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"set"::: ) ; func :::"thin_cylinders"::: "(" "A" "," "B" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "B" "," "A" ")" ")" ) equals :: PETRI_2:def 3 "{" (Set (Var "D")) where D "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "B" "," "A" ")" ")" ) : (Bool (Set (Var "D")) "is" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" "A" "," "B") "}" ; end; :: deftheorem defines :::"thin_cylinders"::: PETRI_2:def 3 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "D")) where D "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" ")" ) : (Bool (Set (Var "D")) "is" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "}" ))); theorem :: PETRI_2:3 (Bool "for" (Set (Var "A")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "Bo1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo1")) "," (Set (Var "A")) (Bool "for" (Set (Var "Bo2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo2")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "Bo1")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "Bo2")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "Bo1")) "," (Set (Var "yo1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "Bo2")) "," (Set (Var "yo2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "Bo1")) ($#r1_hidden :::"="::: ) (Set (Var "Bo2"))) & (Bool (Set (Var "yo1")) ($#r1_funct_2 :::"="::: ) (Set (Var "yo2"))) ")" )))))) ; theorem :: PETRI_2:4 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) ")" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ))) "holds" (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B1"))(Bool "ex" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A1"))(Bool "ex" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A2")) "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "yo1")) ($#r1_funct_2 :::"="::: ) (Set (Var "yo2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "Bo")) "," (Set (Var "yo1")) ")" )) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "Bo")) "," (Set (Var "yo2")) ")" )) ")" )))))))) ; theorem :: PETRI_2:5 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) ")" ))) "holds" (Bool "ex" (Set (Var "Bo2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B2"))(Bool "ex" (Set (Var "Bo1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B1"))(Bool "ex" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo1")) "," (Set (Var "A1"))(Bool "ex" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo2")) "," (Set (Var "A2")) "st" (Bool "(" (Bool (Set (Var "Bo1")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Bo2")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Bo1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Bo2")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set (Var "yo2")) ($#k8_relat_1 :::"""::: ) (Set (Var "A1")) ")" ))) & (Bool (Set (Var "yo1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "yo2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo1")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "Bo2")) "," (Set (Var "yo2")) ")" )) & (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "Bo1")) "," (Set (Var "yo1")) ")" )) ")" ))))))))) ; definitionlet "A1", "A2" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B1", "B2" be ($#m1_hidden :::"set"::: ) ; assume that (Bool (Set (Const "A1")) ($#r1_tarski :::"c="::: ) (Set (Const "A2"))) and (Bool (Set (Const "B1")) ($#r1_tarski :::"c="::: ) (Set (Const "B2"))) ; func :::"Extcylinders"::: "(" "A1" "," "B1" "," "A2" "," "B2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A1" "," "B1" ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A2" "," "B2" ")" ")" ) means :: PETRI_2:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A1" "," "B1" ")" ))) "holds" (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" "B1"(Bool "ex" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," "A1"(Bool "ex" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," "A2" "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "yo1")) ($#r1_funct_2 :::"="::: ) (Set (Var "yo2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" "A1" "," "B1" "," (Set (Var "Bo")) "," (Set (Var "yo1")) ")" )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" "A2" "," "B2" "," (Set (Var "Bo")) "," (Set (Var "yo2")) ")" )) ")" ))))); end; :: deftheorem defines :::"Extcylinders"::: PETRI_2:def 4 : (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_petri_2 :::"Extcylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ))) "holds" (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B1"))(Bool "ex" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A1"))(Bool "ex" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A2")) "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "yo1")) ($#r1_funct_2 :::"="::: ) (Set (Var "yo2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "Bo")) "," (Set (Var "yo1")) ")" )) & (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "Bo")) "," (Set (Var "yo2")) ")" )) ")" ))))) ")" )))); definitionlet "A1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A2" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B1", "B2" be ($#m1_hidden :::"set"::: ) ; func :::"Ristcylinders"::: "(" "A1" "," "B1" "," "A2" "," "B2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A2" "," "B2" ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A1" "," "B1" ")" ")" ) means :: PETRI_2:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A2" "," "B2" ")" ))) "holds" (Bool "ex" (Set (Var "Bo2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "B2"(Bool "ex" (Set (Var "Bo1")) "being" ($#m1_subset_1 :::"Subset":::) "of" "B1"(Bool "ex" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo1")) "," "A1"(Bool "ex" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo2")) "," "A2" "st" (Bool "(" (Bool (Set (Var "Bo1")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Bo2")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Bo1")) ($#r1_hidden :::"="::: ) (Set (Set "(" "B1" ($#k9_subset_1 :::"/\"::: ) (Set (Var "Bo2")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set (Var "yo2")) ($#k8_relat_1 :::"""::: ) "A1" ")" ))) & (Bool (Set (Var "yo1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "yo2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo1")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" "A2" "," "B2" "," (Set (Var "Bo2")) "," (Set (Var "yo2")) ")" )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" "A1" "," "B1" "," (Set (Var "Bo1")) "," (Set (Var "yo1")) ")" )) ")" )))))); end; :: deftheorem defines :::"Ristcylinders"::: PETRI_2:def 5 : (Bool "for" (Set (Var "A1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A2")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_petri_2 :::"Ristcylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) ")" ))) "holds" (Bool "ex" (Set (Var "Bo2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B2"))(Bool "ex" (Set (Var "Bo1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B1"))(Bool "ex" (Set (Var "yo1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo1")) "," (Set (Var "A1"))(Bool "ex" (Set (Var "yo2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo2")) "," (Set (Var "A2")) "st" (Bool "(" (Bool (Set (Var "Bo1")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Bo2")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Bo1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Bo2")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" (Set (Var "yo2")) ($#k8_relat_1 :::"""::: ) (Set (Var "A1")) ")" ))) & (Bool (Set (Var "yo1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "yo2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo1")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "Bo2")) "," (Set (Var "yo2")) ")" )) & (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_petri_2 :::"cylinder0"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "Bo1")) "," (Set (Var "yo1")) ")" )) ")" )))))) ")" ))))); definitionlet "A" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); func :::"loc"::: "D" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "B" means :: PETRI_2:def 6 (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" "B"(Bool "ex" (Set (Var "yo")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," "A" "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "D" ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Function":::) "of" "B" "," "A" : (Bool (Set (Set (Var "y")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo"))) ($#r1_hidden :::"="::: ) (Set (Var "yo"))) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "Bo"))) ")" ))); end; :: deftheorem defines :::"loc"::: PETRI_2:def 6 : (Bool "for" (Set (Var "A")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_petri_2 :::"thin_cylinder"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "b4")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_petri_2 :::"loc"::: ) (Set (Var "D")))) "iff" (Bool "ex" (Set (Var "Bo")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B"))(Bool "ex" (Set (Var "yo")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Bo")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "Bo")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) : (Bool (Set (Set (Var "y")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Bo"))) ($#r1_hidden :::"="::: ) (Set (Var "yo"))) "}" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Var "Bo"))) ")" ))) ")" ))))); begin definitionlet "A1", "A2" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "B1", "B2" be ($#m1_hidden :::"set"::: ) ; let "C1", "C2" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Const "A1")) "," (Set (Const "B1")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Const "C1")) "," (Set (Const "D1")) ")" ")" ); func :::"CylinderFunc"::: "(" "A1" "," "B1" "," "A2" "," "B2" "," "C1" "," "D1" "," "C2" "," "D2" "," "F" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "A2" "," "B2" ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" "C2" "," "D2" ")" ")" ) equals :: PETRI_2:def 7 (Set (Set "(" (Set "(" ($#k3_petri_2 :::"Extcylinders"::: ) "(" "C1" "," "D1" "," "C2" "," "D2" ")" ")" ) ($#k1_partfun1 :::"*"::: ) "F" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_petri_2 :::"Ristcylinders"::: ) "(" "A1" "," "B1" "," "A2" "," "B2" ")" ")" )); end; :: deftheorem defines :::"CylinderFunc"::: PETRI_2:def 7 : (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "C1")) "," (Set (Var "D1")) ")" ")" ) "holds" (Bool (Set ($#k6_petri_2 :::"CylinderFunc"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) "," (Set (Var "C1")) "," (Set (Var "D1")) "," (Set (Var "C2")) "," (Set (Var "D2")) "," (Set (Var "F")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_petri_2 :::"Extcylinders"::: ) "(" (Set (Var "C1")) "," (Set (Var "D1")) "," (Set (Var "C2")) "," (Set (Var "D2")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_petri_2 :::"Ristcylinders"::: ) "(" (Set (Var "A1")) "," (Set (Var "B1")) "," (Set (Var "A2")) "," (Set (Var "B2")) ")" ")" )))))))); definitionattr "c1" is :::"strict"::: ; struct :::"Colored_PT_net_Str"::: -> ($#l1_petri :::"PT_net_Str"::: ) ; aggr :::"Colored_PT_net_Str":::(# :::"carrier":::, :::"carrier'":::, :::"S-T_Arcs":::, :::"T-S_Arcs":::, :::"ColoredSet":::, :::"firing-rule"::: #) -> ($#l1_petri_2 :::"Colored_PT_net_Str"::: ) ; sel :::"ColoredSet"::: "c1" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; sel :::"firing-rule"::: "c1" -> ($#m1_hidden :::"Function":::); end; definitionfunc :::"TrivialColoredPetriNet"::: -> ($#l1_petri_2 :::"Colored_PT_net_Str"::: ) equals :: PETRI_2:def 8 (Set ($#g1_petri_2 :::"Colored_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 :::"}"::: ) ) ")" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivialColoredPetriNet"::: PETRI_2:def 8 : (Bool (Set ($#k7_petri_2 :::"TrivialColoredPetriNet"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_petri_2 :::"Colored_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 :::"}"::: ) ) ")" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" )); registration cluster (Set ($#k7_petri_2 :::"TrivialColoredPetriNet"::: ) ) -> ($#~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"::: ) ; end; registration cluster ($#~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"::: ) for ($#l1_petri_2 :::"Colored_PT_net_Str"::: ) ; end; definitionmode Colored_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_2 :::"Colored_PT_net_Str"::: ) ; end; definitionlet "CPNT" be ($#l1_petri_2 :::"Colored_Petri_net":::); let "t0" be ($#m1_subset_1 :::"transition":::) "of" (Set (Const "CPNT")); attr "t0" is :::"outbound"::: means :: PETRI_2:def 9 (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) "t0" ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"outbound"::: PETRI_2:def 9 : (Bool "for" (Set (Var "CPNT")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) (Bool "for" (Set (Var "t0")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT")) "holds" (Bool "(" (Bool (Set (Var "t0")) "is" ($#v2_petri_2 :::"outbound"::: ) ) "iff" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t0")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); definitionlet "CPNT1" be ($#l1_petri_2 :::"Colored_Petri_net":::); func :::"Outbds"::: "CPNT1" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "CPNT1") equals :: PETRI_2:def 10 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"transition":::) "of" "CPNT1" : (Bool (Set (Var "x")) "is" ($#v2_petri_2 :::"outbound"::: ) ) "}" ; end; :: deftheorem defines :::"Outbds"::: PETRI_2:def 10 : (Bool "for" (Set (Var "CPNT1")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) "holds" (Bool (Set ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT1"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT1")) : (Bool (Set (Var "x")) "is" ($#v2_petri_2 :::"outbound"::: ) ) "}" )); definitionlet "CPNT" be ($#l1_petri_2 :::"Colored_Petri_net":::); attr "CPNT" is :::"Colored-PT-net-like"::: means :: PETRI_2:def 11 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" "CPNT")) ($#r1_tarski :::"c="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "CPNT") ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT" ")" ))) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" "CPNT" "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" "CPNT")))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT")(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ")" )(Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ")" ) "st" (Bool (Set (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" "CPNT") ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "CS")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "CS")) "," (Set (Var "O")) ")" ")" ))))) ")" ) ")" ); end; :: deftheorem defines :::"Colored-PT-net-like"::: PETRI_2:def 11 : (Bool "for" (Set (Var "CPNT")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) "holds" (Bool "(" (Bool (Set (Var "CPNT")) "is" ($#v3_petri_2 :::"Colored-PT-net-like"::: ) ) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT")))) ($#r1_tarski :::"c="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT"))) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT")) ")" ))) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT")))))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT")))(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ")" )(Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ")" ) "st" (Bool (Set (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "CS")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "CS")) "," (Set (Var "O")) ")" ")" ))))) ")" ) ")" ) ")" )); theorem :: PETRI_2:6 (Bool "for" (Set (Var "CPNT")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT")) "st" (Bool (Bool (Set (Var "CPNT")) "is" ($#v3_petri_2 :::"Colored-PT-net-like"::: ) ) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT")))))) "holds" (Bool "ex" (Set (Var "CS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT")))(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ")" )(Bool "ex" (Set (Var "O")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ")" ) "st" (Bool (Set (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "CS")) "," (Set (Var "I")) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set (Var "CS")) "," (Set (Var "O")) ")" ")" ))))))) ; theorem :: PETRI_2:7 (Bool "for" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) (Bool "for" (Set (Var "t1")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT2")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2")))) & (Bool (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "CPNT1"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "CPNT2")))) & (Bool (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "CPNT1"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "CPNT2")))) & (Bool (Set (Var "t1")) ($#r1_hidden :::"="::: ) (Set (Var "t2")))) "holds" (Bool "(" (Bool (Set ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t1")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t2")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t1")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t2")) ($#k6_domain_1 :::"}"::: ) ) ($#k9_petri :::"*'"::: ) )) ")" )))) ; 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"::: ) ($#v1_petri_2 :::"strict"::: ) ($#v3_petri_2 :::"Colored-PT-net-like"::: ) for ($#l1_petri_2 :::"Colored_PT_net_Str"::: ) ; end; definitionmode Colored-PT-net is ($#v3_petri_2 :::"Colored-PT-net-like"::: ) ($#l1_petri_2 :::"Colored_Petri_net":::); end; begin definitionlet "CPNT1", "CPNT2" be ($#l1_petri_2 :::"Colored_Petri_net":::); pred "CPNT1" :::"misses"::: "CPNT2" means :: PETRI_2:def 12 (Bool "(" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT1") ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "CPNT1") ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "CPNT2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ); symmetry (Bool "for" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) "st" (Bool (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT2")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT2"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT1")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; end; :: deftheorem defines :::"misses"::: PETRI_2:def 12 : (Bool "for" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) "holds" (Bool "(" (Bool (Set (Var "CPNT1")) ($#r1_petri_2 :::"misses"::: ) (Set (Var "CPNT2"))) "iff" (Bool "(" (Bool (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT2")))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); begin definitionlet "CPNT1", "CPNT2" be ($#l1_petri_2 :::"Colored_Petri_net":::); mode :::"connecting-mapping"::: "of" "CPNT1" "," "CPNT2" -> ($#m1_hidden :::"set"::: ) means :: PETRI_2:def 13 (Bool "ex" (Set (Var "O12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT1" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT2")(Bool "ex" (Set (Var "O21")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT2" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT1") "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "O12")) "," (Set (Var "O21")) ($#k1_domain_1 :::"]"::: ) )))); end; :: deftheorem defines :::"connecting-mapping"::: PETRI_2:def 13 : (Bool "for" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "being" ($#l1_petri_2 :::"Colored_Petri_net":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_petri_2 :::"connecting-mapping"::: ) "of" (Set (Var "CPNT1")) "," (Set (Var "CPNT2"))) "iff" (Bool "ex" (Set (Var "O12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT1")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2")))(Bool "ex" (Set (Var "O21")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT2")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) "st" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "O12")) "," (Set (Var "O21")) ($#k1_domain_1 :::"]"::: ) )))) ")" ))); begin definitionlet "CPNT1", "CPNT2" be ($#l1_petri_2 :::"Colored-PT-net":::); let "O" be ($#m2_petri_2 :::"connecting-mapping"::: ) "of" (Set (Const "CPNT1")) "," (Set (Const "CPNT2")); mode :::"connecting-firing-rule"::: "of" "CPNT1" "," "CPNT2" "," "O" -> ($#m1_hidden :::"set"::: ) means :: PETRI_2:def 14 (Bool "ex" (Set (Var "q12")) "," (Set (Var "q21")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "O12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT1" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT2")(Bool "ex" (Set (Var "O21")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT2" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT1") "st" (Bool "(" (Bool "O" ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "O12")) "," (Set (Var "O21")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q12"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) "CPNT1")) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q21"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) "CPNT2")) & (Bool "(" "for" (Set (Var "t01")) "being" ($#m1_subset_1 :::"transition":::) "of" "CPNT1" "st" (Bool (Bool (Set (Var "t01")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q12")) ($#k1_funct_1 :::"."::: ) (Set (Var "t01"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT1") "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t01")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT1") "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O12")) "," (Set (Var "t01")) ")" ")" ) ")" ")" )) ")" ) & (Bool "(" "for" (Set (Var "t02")) "being" ($#m1_subset_1 :::"transition":::) "of" "CPNT2" "st" (Bool (Bool (Set (Var "t02")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q21")) ($#k1_funct_1 :::"."::: ) (Set (Var "t02"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT2") "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t02")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT2") "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O21")) "," (Set (Var "t02")) ")" ")" ) ")" ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "q12")) "," (Set (Var "q21")) ($#k4_tarski :::"]"::: ) )) ")" )))); end; :: deftheorem defines :::"connecting-firing-rule"::: PETRI_2:def 14 : (Bool "for" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "being" ($#l1_petri_2 :::"Colored-PT-net":::) (Bool "for" (Set (Var "O")) "being" ($#m2_petri_2 :::"connecting-mapping"::: ) "of" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m3_petri_2 :::"connecting-firing-rule"::: ) "of" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "," (Set (Var "O"))) "iff" (Bool "ex" (Set (Var "q12")) "," (Set (Var "q21")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "O12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT1")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2")))(Bool "ex" (Set (Var "O21")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT2")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) "st" (Bool "(" (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "O12")) "," (Set (Var "O21")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q12"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT1")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q21"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT2")))) & (Bool "(" "for" (Set (Var "t01")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT1")) "st" (Bool (Bool (Set (Var "t01")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q12")) ($#k1_funct_1 :::"."::: ) (Set (Var "t01"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT1"))) "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t01")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT1"))) "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O12")) "," (Set (Var "t01")) ")" ")" ) ")" ")" )) ")" ) & (Bool "(" "for" (Set (Var "t02")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT2")) "st" (Bool (Bool (Set (Var "t02")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q21")) ($#k1_funct_1 :::"."::: ) (Set (Var "t02"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT2"))) "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t02")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT2"))) "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O21")) "," (Set (Var "t02")) ")" ")" ) ")" ")" )) ")" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "q12")) "," (Set (Var "q21")) ($#k4_tarski :::"]"::: ) )) ")" )))) ")" )))); begin definitionlet "CPNT1", "CPNT2" be ($#l1_petri_2 :::"Colored-PT-net":::); let "O" be ($#m2_petri_2 :::"connecting-mapping"::: ) "of" (Set (Const "CPNT1")) "," (Set (Const "CPNT2")); let "q" be ($#m3_petri_2 :::"connecting-firing-rule"::: ) "of" (Set (Const "CPNT1")) "," (Set (Const "CPNT2")) "," (Set (Const "O")); assume (Bool (Set (Const "CPNT1")) ($#r1_petri_2 :::"misses"::: ) (Set (Const "CPNT2"))) ; func :::"synthesis"::: "(" "CPNT1" "," "CPNT2" "," "O" "," "q" ")" -> ($#v1_petri_2 :::"strict"::: ) ($#l1_petri_2 :::"Colored-PT-net":::) means :: PETRI_2:def 15 (Bool "ex" (Set (Var "q12")) "," (Set (Var "q21")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "O12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT1" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT2")(Bool "ex" (Set (Var "O21")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) "CPNT2" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT1") "st" (Bool "(" (Bool "O" ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "O12")) "," (Set (Var "O21")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q12"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) "CPNT1")) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q21"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) "CPNT2")) & (Bool "(" "for" (Set (Var "t01")) "being" ($#m1_subset_1 :::"transition":::) "of" "CPNT1" "st" (Bool (Bool (Set (Var "t01")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q12")) ($#k1_funct_1 :::"."::: ) (Set (Var "t01"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT1") "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t01")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT1") "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O12")) "," (Set (Var "t01")) ")" ")" ) ")" ")" )) ")" ) & (Bool "(" "for" (Set (Var "t02")) "being" ($#m1_subset_1 :::"transition":::) "of" "CPNT2" "st" (Bool (Bool (Set (Var "t02")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q21")) ($#k1_funct_1 :::"."::: ) (Set (Var "t02"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT2") "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t02")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT2") "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O21")) "," (Set (Var "t02")) ")" ")" ) ")" ")" )) ")" ) & (Bool "q" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "q12")) "," (Set (Var "q21")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "CPNT2"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "CPNT1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "CPNT2"))) & (Bool (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "CPNT1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "CPNT2"))) & (Bool (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "CPNT1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "CPNT2") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "O12")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "O21")))) & (Bool (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" "CPNT2"))) & (Bool (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" "CPNT1") ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" "CPNT2") ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q12")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q21")))) ")" )))); end; :: deftheorem defines :::"synthesis"::: PETRI_2:def 15 : (Bool "for" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "being" ($#l1_petri_2 :::"Colored-PT-net":::) (Bool "for" (Set (Var "O")) "being" ($#m2_petri_2 :::"connecting-mapping"::: ) "of" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) (Bool "for" (Set (Var "q")) "being" ($#m3_petri_2 :::"connecting-firing-rule"::: ) "of" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "," (Set (Var "O")) "st" (Bool (Bool (Set (Var "CPNT1")) ($#r1_petri_2 :::"misses"::: ) (Set (Var "CPNT2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#v1_petri_2 :::"strict"::: ) ($#l1_petri_2 :::"Colored-PT-net":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_petri_2 :::"synthesis"::: ) "(" (Set (Var "CPNT1")) "," (Set (Var "CPNT2")) "," (Set (Var "O")) "," (Set (Var "q")) ")" )) "iff" (Bool "ex" (Set (Var "q12")) "," (Set (Var "q21")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "O12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT1")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2")))(Bool "ex" (Set (Var "O21")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT2")) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) "st" (Bool "(" (Bool (Set (Var "O")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "O12")) "," (Set (Var "O21")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q12"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT1")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q21"))) ($#r1_hidden :::"="::: ) (Set ($#k8_petri_2 :::"Outbds"::: ) (Set (Var "CPNT2")))) & (Bool "(" "for" (Set (Var "t01")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT1")) "st" (Bool (Bool (Set (Var "t01")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q12")) ($#k1_funct_1 :::"."::: ) (Set (Var "t01"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT1"))) "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t01")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT1"))) "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O12")) "," (Set (Var "t01")) ")" ")" ) ")" ")" )) ")" ) & (Bool "(" "for" (Set (Var "t02")) "being" ($#m1_subset_1 :::"transition":::) "of" (Set (Var "CPNT2")) "st" (Bool (Bool (Set (Var "t02")) "is" ($#v2_petri_2 :::"outbound"::: ) )) "holds" (Bool (Set (Set (Var "q21")) ($#k1_funct_1 :::"."::: ) (Set (Var "t02"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT2"))) "," (Set "(" ($#k8_petri :::"*'"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "t02")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ")" ) "," (Set "(" ($#k2_petri_2 :::"thin_cylinders"::: ) "(" (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT2"))) "," (Set "(" ($#k1_relset_2 :::"Im"::: ) "(" (Set (Var "O21")) "," (Set (Var "t02")) ")" ")" ) ")" ")" )) ")" ) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "q12")) "," (Set (Var "q21")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "CPNT2"))))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "CPNT2"))))) & (Bool (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "CPNT1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "CPNT2"))))) & (Bool (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "CPNT1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "CPNT2"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "O12")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "O21")))) & (Bool (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_petri_2 :::"ColoredSet"::: ) "of" (Set (Var "CPNT2"))))) & (Bool (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT1"))) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u2_petri_2 :::"firing-rule"::: ) "of" (Set (Var "CPNT2"))) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q12")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q21")))) ")" )))) ")" )))));