:: NET_1 semantic presentation begin definitionlet "P" be ($#l1_petri :::"PT_net_Str"::: ) ; func :::"Flow"::: "P" -> ($#m1_hidden :::"set"::: ) equals :: NET_1:def 1 (Set (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" "P") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" "P")); end; :: deftheorem defines :::"Flow"::: NET_1:def 1 : (Bool "for" (Set (Var "P")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_petri :::"S-T_Arcs"::: ) "of" (Set (Var "P"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_petri :::"T-S_Arcs"::: ) "of" (Set (Var "P")))))); registrationlet "P" be ($#l1_petri :::"PT_net_Str"::: ) ; cluster (Set ($#k1_net_1 :::"Flow"::: ) "P") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; definitionlet "N" be ($#l1_petri :::"PT_net_Str"::: ) ; attr "N" is :::"Petri"::: means :: NET_1:def 2 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N")) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) "N") ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ); end; :: deftheorem defines :::"Petri"::: NET_1:def 2 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool "(" (Bool (Set (Var "N")) "is" ($#v1_net_1 :::"Petri"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_xboole_0 :::"misses"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ) ")" )); definitionlet "N" be ($#l1_petri :::"PT_net_Str"::: ) ; func :::"Elements"::: "N" -> ($#m1_hidden :::"set"::: ) equals :: NET_1:def 3 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N")); end; :: deftheorem defines :::"Elements"::: NET_1:def 3 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))))); theorem :: NET_1:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "holds" (Bool "(" "not" (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" "not" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))) "or" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) "or" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) ")" ))) ; theorem :: NET_1:2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; registration cluster (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ")" ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ")" ) "#)" ) -> ($#v1_net_1 :::"Petri"::: ) ; end; registration cluster ($#v1_petri :::"strict"::: ) ($#v1_net_1 :::"Petri"::: ) for ($#l1_petri :::"PT_net_Str"::: ) ; end; definitionmode Pnet is ($#v1_net_1 :::"Petri"::: ) ($#l1_petri :::"PT_net_Str"::: ) ; end; theorem :: NET_1:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) ")" ))) ; theorem :: NET_1:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))))) ; theorem :: NET_1:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))))) ; theorem :: NET_1:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))))) ; theorem :: NET_1:8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))))) ; definitionlet "N" be ($#l1_petri :::"Pnet":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; pred :::"pre"::: "N" "," "x" "," "y" means :: NET_1:def 4 (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) "y" "," "x" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) "N")) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N")) ")" ); pred :::"post"::: "N" "," "x" "," "y" means :: NET_1:def 5 (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) "N")) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N")) ")" ); end; :: deftheorem defines :::"pre"::: NET_1:def 4 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r1_net_1 :::"pre"::: ) (Set (Var "N")) "," (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) ")" ) ")" ))); :: deftheorem defines :::"post"::: NET_1:def 5 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool ($#r2_net_1 :::"post"::: ) (Set (Var "N")) "," (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) ")" ) ")" ))); definitionlet "N" be ($#l1_petri :::"PT_net_Str"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Const "N"))); func :::"Pre"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 6 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_net_1 :::"Elements"::: ) "N")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," "x" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) "N")) ")" ) ")" )); func :::"Post"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 7 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_net_1 :::"Elements"::: ) "N")) & (Bool (Set ($#k4_tarski :::"["::: ) "x" "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) "N")) ")" ) ")" )); end; :: deftheorem defines :::"Pre"::: NET_1:def 6 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_net_1 :::"Pre"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"Post"::: NET_1:def 7 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_net_1 :::"Post"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) ")" ) ")" )) ")" )))); theorem :: NET_1:9 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool (Set ($#k3_net_1 :::"Pre"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:10 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool (Set ($#k3_net_1 :::"Pre"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:11 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool (Set ($#k4_net_1 :::"Post"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:12 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool (Set ($#k4_net_1 :::"Post"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_net_1 :::"Pre"::: ) "(" (Set (Var "N")) "," (Set (Var "y")) ")" )) "iff" (Bool ($#r1_net_1 :::"pre"::: ) (Set (Var "N")) "," (Set (Var "y")) "," (Set (Var "x"))) ")" )))) ; theorem :: NET_1:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_net_1 :::"Post"::: ) "(" (Set (Var "N")) "," (Set (Var "y")) ")" )) "iff" (Bool ($#r2_net_1 :::"post"::: ) (Set (Var "N")) "," (Set (Var "y")) "," (Set (Var "x"))) ")" )))) ; definitionlet "N" be ($#l1_petri :::"Pnet":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Const "N"))); assume (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Const "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"enter"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 8 (Bool "(" "(" (Bool (Bool "x" ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N"))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool "x" ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N"))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_net_1 :::"Pre"::: ) "(" "N" "," "x" ")" )) ")" ")" ); end; :: deftheorem defines :::"enter"::: NET_1:def 8 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))) "implies" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))))) "implies" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_net_1 :::"Pre"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) ")" ")" ) ")" )))); theorem :: NET_1:15 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool "(" "not" (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_net_1 :::"Pre"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) ")" ))) ; theorem :: NET_1:16 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:17 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; definitionlet "N" be ($#l1_petri :::"Pnet":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Const "N"))); assume (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Const "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"exit"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 9 (Bool "(" "(" (Bool (Bool "x" ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N"))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool "x" ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "N"))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_net_1 :::"Post"::: ) "(" "N" "," "x" ")" )) ")" ")" ); end; :: deftheorem defines :::"exit"::: NET_1:def 9 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) "iff" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))) "implies" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))))) "implies" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_net_1 :::"Post"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) ")" ")" ) ")" )))); theorem :: NET_1:18 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool "(" "not" (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_net_1 :::"Post"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) ")" ))) ; theorem :: NET_1:19 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; theorem :: NET_1:20 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))))) ; definitionlet "N" be ($#l1_petri :::"Pnet":::); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Const "N"))); func :::"field"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: NET_1:def 10 (Set (Set "(" ($#k5_net_1 :::"enter"::: ) "(" "N" "," "x" ")" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k6_net_1 :::"exit"::: ) "(" "N" "," "x" ")" ")" )); end; :: deftheorem defines :::"field"::: NET_1:def 10 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "holds" (Bool (Set ($#k7_net_1 :::"field"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ")" ))))); definitionlet "N" be ($#l1_petri :::"PT_net_Str"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "N"))); func :::"Prec"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 11 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," "x" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) "N")) ")" ) ")" )); func :::"Postc"::: "(" "N" "," "x" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 12 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N")) & (Bool (Set ($#k4_tarski :::"["::: ) "x" "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) "N")) ")" ) ")" )); end; :: deftheorem defines :::"Prec"::: NET_1:def 11 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_net_1 :::"Prec"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"Postc"::: NET_1:def 12 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"PT_net_Str"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_net_1 :::"Postc"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "N")))) ")" ) ")" )) ")" )))); definitionlet "N" be ($#l1_petri :::"Pnet":::); let "X" be ($#m1_hidden :::"set"::: ) ; func :::"Entr"::: "(" "N" "," "X" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) "N")) & (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) "N") "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_net_1 :::"enter"::: ) "(" "N" "," (Set (Var "y")) ")" )) ")" )) ")" ) ")" )); func :::"Ext"::: "(" "N" "," "X" ")" -> ($#m1_hidden :::"set"::: ) means :: NET_1:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) "N")) & (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) "N") "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_net_1 :::"exit"::: ) "(" "N" "," (Set (Var "y")) ")" )) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Entr"::: NET_1:def 13 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_net_1 :::"Entr"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))) & (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "y")) ")" )) ")" )) ")" ) ")" )) ")" )))); :: deftheorem defines :::"Ext"::: NET_1:def 14 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_net_1 :::"Ext"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")))) & (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "y")) ")" )) ")" )) ")" ) ")" )) ")" )))); theorem :: NET_1:21 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k10_net_1 :::"Entr"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" ))))) ; theorem :: NET_1:22 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k11_net_1 :::"Ext"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" ))))) ; definitionlet "N" be ($#l1_petri :::"Pnet":::); let "X" be ($#m1_hidden :::"set"::: ) ; func :::"Input"::: "(" "N" "," "X" ")" -> ($#m1_hidden :::"set"::: ) equals :: NET_1:def 15 (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_net_1 :::"Entr"::: ) "(" "N" "," "X" ")" ")" )); func :::"Output"::: "(" "N" "," "X" ")" -> ($#m1_hidden :::"set"::: ) equals :: NET_1:def 16 (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k11_net_1 :::"Ext"::: ) "(" "N" "," "X" ")" ")" )); end; :: deftheorem defines :::"Input"::: NET_1:def 15 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_net_1 :::"Input"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_net_1 :::"Entr"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" ")" ))))); :: deftheorem defines :::"Output"::: NET_1:def 16 : (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_net_1 :::"Output"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k11_net_1 :::"Ext"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" ")" ))))); theorem :: NET_1:23 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k12_net_1 :::"Input"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" )) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_net_1 :::"enter"::: ) "(" (Set (Var "N")) "," (Set (Var "y")) ")" )) ")" )) ")" ))) ; theorem :: NET_1:24 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_net_1 :::"Output"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" )) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_net_1 :::"exit"::: ) "(" (Set (Var "N")) "," (Set (Var "y")) ")" )) ")" )) ")" ))) ; theorem :: NET_1:25 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k12_net_1 :::"Input"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" )) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) ")" ) "or" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) & (Bool ($#r1_net_1 :::"pre"::: ) (Set (Var "N")) "," (Set (Var "y")) "," (Set (Var "x"))) ")" )) ")" ) ")" )))) ; theorem :: NET_1:26 (Bool "for" (Set (Var "N")) "being" ($#l1_petri :::"Pnet":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "N")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool (Bool (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_net_1 :::"Output"::: ) "(" (Set (Var "N")) "," (Set (Var "X")) ")" )) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) ")" ) "or" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "N"))) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "N")))) & (Bool ($#r2_net_1 :::"post"::: ) (Set (Var "N")) "," (Set (Var "y")) "," (Set (Var "x"))) ")" )) ")" ) ")" )))) ;