:: FF_SIEC semantic presentation begin definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Const "Y"))) ; func :::"PTempty_f_net"::: "(" "X" "," "Y" ")" -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"Pnet":::) equals :: FF_SIEC:def 1 (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" "X" "," "Y" "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" "X" "," "Y" ")" ")" ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" "Y" "," "X" ")" ")" ) "#)" ); end; :: deftheorem defines :::"PTempty_f_net"::: FF_SIEC:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_petri :::"PT_net_Str"::: ) "(#" (Set (Var "X")) "," (Set (Var "Y")) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Set (Var "Y")) "," (Set (Var "X")) ")" ")" ) "#)" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Tempty_f_net"::: "X" -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"Pnet":::) equals :: FF_SIEC:def 2 (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" "X" "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); func :::"Pempty_f_net"::: "X" -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"Pnet":::) equals :: FF_SIEC:def 3 (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," "X" ")" ); end; :: deftheorem defines :::"Tempty_f_net"::: FF_SIEC:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_ff_siec :::"Tempty_f_net"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set (Var "X")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); :: deftheorem defines :::"Pempty_f_net"::: FF_SIEC:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_ff_siec :::"Pempty_f_net"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ")" ))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"Tsingle_f_net"::: "x" -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"Pnet":::) equals :: FF_SIEC:def 4 (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ); func :::"Psingle_f_net"::: "x" -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"Pnet":::) equals :: FF_SIEC:def 5 (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); end; :: deftheorem defines :::"Tsingle_f_net"::: FF_SIEC:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_ff_siec :::"Tsingle_f_net"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))); :: deftheorem defines :::"Psingle_f_net"::: FF_SIEC:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_ff_siec :::"Psingle_f_net"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ))); definitionfunc :::"empty_f_net"::: -> ($#v1_petri :::"strict"::: ) ($#l1_petri :::"Pnet":::) equals :: FF_SIEC:def 6 (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ); end; :: deftheorem defines :::"empty_f_net"::: FF_SIEC:def 6 : (Bool (Set ($#k6_ff_siec :::"empty_f_net"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" )); theorem :: FF_SIEC:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set "(" ($#k1_ff_siec :::"PTempty_f_net"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_ff_siec :::"Tempty_f_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k2_ff_siec :::"Tempty_f_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set "(" ($#k2_ff_siec :::"Tempty_f_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_ff_siec :::"Pempty_f_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k3_ff_siec :::"Pempty_f_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set "(" ($#k3_ff_siec :::"Pempty_f_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_ff_siec :::"Tsingle_f_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k4_ff_siec :::"Tsingle_f_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set "(" ($#k4_ff_siec :::"Tsingle_f_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_ff_siec :::"Psingle_f_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k5_ff_siec :::"Psingle_f_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set "(" ($#k5_ff_siec :::"Psingle_f_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k6_ff_siec :::"empty_f_net"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set ($#k6_ff_siec :::"empty_f_net"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set ($#k6_ff_siec :::"empty_f_net"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: FF_SIEC:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) ")" ) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) ")" ) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) ")" ) ")" & "(" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) "implies" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) ")" ) ")" ")" ))) ; theorem :: FF_SIEC:8 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: FF_SIEC:9 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) ")" )) ; theorem :: FF_SIEC:10 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ))) ")" )) ; theorem :: FF_SIEC:11 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:12 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FF_SIEC:13 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ))) & (Bool (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M")))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ))) ")" )) ; theorem :: FF_SIEC:14 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) ")" )) ; theorem :: FF_SIEC:15 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))) ")" )) ; theorem :: FF_SIEC:16 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) )) ")" )) ; definitionlet "M" be ($#l1_petri :::"Pnet":::); func :::"f_enter"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 7 (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" )); func :::"f_exit"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 8 (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" )); end; :: deftheorem defines :::"f_enter"::: FF_SIEC:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )))); :: deftheorem defines :::"f_exit"::: FF_SIEC:def 8 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )))); theorem :: FF_SIEC:17 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: FF_SIEC:18 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) ")" )) ; theorem :: FF_SIEC:19 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")))) ")" )) ; theorem :: FF_SIEC:20 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k8_ff_siec :::"f_exit"::: ) (Set (Var "M")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_ff_siec :::"f_enter"::: ) (Set (Var "M")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; definitionlet "M" be ($#l1_petri :::"Pnet":::); func :::"f_prox"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 9 (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" )); func :::"f_flow"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 10 (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) "M" ")" ) ")" )); end; :: deftheorem defines :::"f_prox"::: FF_SIEC:def 9 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" )))); :: deftheorem defines :::"f_flow"::: FF_SIEC:def 10 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k10_ff_siec :::"f_flow"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )))); theorem :: FF_SIEC:21 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" (Set "(" ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_ff_siec :::"f_flow"::: ) (Set (Var "M")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k10_ff_siec :::"f_flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ))) ")" )) ; definitionlet "M" be ($#l1_petri :::"Pnet":::); func :::"f_places"::: "M" -> ($#m1_hidden :::"set"::: ) equals :: FF_SIEC:def 11 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M"); func :::"f_transitions"::: "M" -> ($#m1_hidden :::"set"::: ) equals :: FF_SIEC:def 12 (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M"); func :::"f_pre"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 13 (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M")); func :::"f_post"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 14 (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M")); end; :: deftheorem defines :::"f_places"::: FF_SIEC:def 11 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k11_ff_siec :::"f_places"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))))); :: deftheorem defines :::"f_transitions"::: FF_SIEC:def 12 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k12_ff_siec :::"f_transitions"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))))); :: deftheorem defines :::"f_pre"::: FF_SIEC:def 13 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k13_ff_siec :::"f_pre"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))))); :: deftheorem defines :::"f_post"::: FF_SIEC:def 14 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k14_ff_siec :::"f_post"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M")))))); theorem :: FF_SIEC:22 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k13_ff_siec :::"f_pre"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_ff_siec :::"f_transitions"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k11_ff_siec :::"f_places"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k14_ff_siec :::"f_post"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_ff_siec :::"f_transitions"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k11_ff_siec :::"f_places"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: FF_SIEC:23 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k9_ff_siec :::"f_prox"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k10_ff_siec :::"f_flow"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; definitionlet "M" be ($#l1_petri :::"Pnet":::); func :::"f_entrance"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 15 (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" )); func :::"f_escape"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 16 (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" )); end; :: deftheorem defines :::"f_entrance"::: FF_SIEC:def 15 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )))); :: deftheorem defines :::"f_escape"::: FF_SIEC:def 16 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )))); theorem :: FF_SIEC:24 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: FF_SIEC:25 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")))) ")" )) ; theorem :: FF_SIEC:26 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")))) ")" )) ; theorem :: FF_SIEC:27 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_ff_siec :::"f_escape"::: ) (Set (Var "M")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k15_ff_siec :::"f_entrance"::: ) (Set (Var "M")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; notationlet "M" be ($#l1_petri :::"Pnet":::); synonym :::"f_circulation"::: "M" for :::"f_flow"::: "M"; end; definitionlet "M" be ($#l1_petri :::"Pnet":::); func :::"f_adjac"::: "M" -> ($#m1_hidden :::"Relation":::) equals :: FF_SIEC:def 17 (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) "M" ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "M") ")" )); end; :: deftheorem defines :::"f_adjac"::: FF_SIEC:def 17 : (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool (Set ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set "(" ($#k1_net_1 :::"Flow"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "M"))) ")" )))); theorem :: FF_SIEC:28 (Bool "for" (Set (Var "M")) "being" ($#l1_petri :::"Pnet":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")))) & (Bool (Set (Set "(" (Set "(" ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k17_ff_siec :::"f_adjac"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k2_net_1 :::"Elements"::: ) (Set (Var "M")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_ff_siec :::"f_circulation"::: ) (Set (Var "M")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k10_ff_siec :::"f_circulation"::: ) (Set (Var "M")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ))) ")" )) ;