:: E_SIEC semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"G_Net"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"G_Net":::(# :::"carrier":::, :::"entrance":::, :::"escape"::: #) -> ($#l1_e_siec :::"G_Net"::: ) ; sel :::"entrance"::: "c1" -> ($#m1_hidden :::"Relation":::); sel :::"escape"::: "c1" -> ($#m1_hidden :::"Relation":::); end; definitionlet "IT" be ($#l1_e_siec :::"G_Net"::: ) ; attr "IT" is :::"GG"::: means :: E_SIEC:def 1 (Bool "(" (Bool (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT") ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT") ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT")) & (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT")) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT")) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT")) ")" ); end; :: deftheorem defines :::"GG"::: E_SIEC:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#l1_e_siec :::"G_Net"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_e_siec :::"GG"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT")))) ")" ) ")" )); registration cluster ($#v2_e_siec :::"GG"::: ) for ($#l1_e_siec :::"G_Net"::: ) ; end; definitionmode gg_net is ($#v2_e_siec :::"GG"::: ) ($#l1_e_siec :::"G_Net"::: ) ; end; definitionlet "IT" be ($#l1_e_siec :::"G_Net"::: ) ; attr "IT" is :::"EE"::: means :: E_SIEC:def 2 (Bool "(" (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT") ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "IT") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT") ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "IT") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ); end; :: deftheorem defines :::"EE"::: E_SIEC:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l1_e_siec :::"G_Net"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_e_siec :::"EE"::: ) ) "iff" (Bool "(" (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT"))) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "IT"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT"))) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "IT"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )); registration cluster ($#v3_e_siec :::"EE"::: ) for ($#l1_e_siec :::"G_Net"::: ) ; end; registration cluster ($#v1_e_siec :::"strict"::: ) ($#v2_e_siec :::"GG"::: ) ($#v3_e_siec :::"EE"::: ) for ($#l1_e_siec :::"G_Net"::: ) ; end; definitionmode e_net is ($#v2_e_siec :::"GG"::: ) ($#v3_e_siec :::"EE"::: ) ($#l1_e_siec :::"G_Net"::: ) ; end; theorem :: E_SIEC:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set (Var "X")) "," (Set (Var "R")) "," (Set (Var "S")) "#)" ) "is" ($#l1_e_siec :::"e_net":::)) "iff" (Bool "(" (Bool (Set (Var "R")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "R")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "R")) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "S")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "S")) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))) ; theorem :: E_SIEC:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set (Var "X")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ) "is" ($#l1_e_siec :::"e_net":::))) ; theorem :: E_SIEC:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set (Var "X")) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "#)" ) "is" ($#l1_e_siec :::"e_net":::))) ; theorem :: E_SIEC:4 (Bool (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ) "is" ($#l1_e_siec :::"e_net":::)) ; theorem :: E_SIEC:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set (Var "X")) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" ) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" ) ")" ) "#)" ) "is" ($#l1_e_siec :::"e_net":::))) ; definitionfunc :::"empty_e_net"::: -> ($#v1_e_siec :::"strict"::: ) ($#l1_e_siec :::"e_net":::) equals :: E_SIEC:def 3 (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ); end; :: deftheorem defines :::"empty_e_net"::: E_SIEC:def 3 : (Bool (Set ($#k1_e_siec :::"empty_e_net"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Tempty_e_net"::: "X" -> ($#v1_e_siec :::"strict"::: ) ($#l1_e_siec :::"e_net":::) equals :: E_SIEC:def 4 (Set ($#g1_e_siec :::"G_Net"::: ) "(#" "X" "," (Set "(" ($#k4_relat_1 :::"id"::: ) "X" ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) "X" ")" ) "#)" ); func :::"Pempty_e_net"::: "X" -> ($#v1_e_siec :::"strict"::: ) ($#l1_e_siec :::"e_net":::) equals :: E_SIEC:def 5 (Set ($#g1_e_siec :::"G_Net"::: ) "(#" "X" "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ); end; :: deftheorem defines :::"Tempty_e_net"::: E_SIEC:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_e_siec :::"Tempty_e_net"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set (Var "X")) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "#)" ))); :: deftheorem defines :::"Pempty_e_net"::: E_SIEC:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_e_siec :::"Pempty_e_net"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set (Var "X")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ))); theorem :: E_SIEC:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k2_e_siec :::"Tempty_e_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set "(" ($#k2_e_siec :::"Tempty_e_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))) & (Bool (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set "(" ($#k2_e_siec :::"Tempty_e_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set (Var "X")))) ")" )) ; theorem :: E_SIEC:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_e_siec :::"Pempty_e_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set "(" ($#k3_e_siec :::"Pempty_e_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set "(" ($#k3_e_siec :::"Pempty_e_net"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"Psingle_e_net"::: "x" -> ($#v1_e_siec :::"strict"::: ) ($#l1_e_siec :::"e_net":::) equals :: E_SIEC:def 6 (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ) "#)" ); func :::"Tsingle_e_net"::: "x" -> ($#v1_e_siec :::"strict"::: ) ($#l1_e_siec :::"e_net":::) equals :: E_SIEC:def 7 (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ); end; :: deftheorem defines :::"Psingle_e_net"::: E_SIEC:def 6 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_e_siec :::"Psingle_e_net"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "#)" ))); :: deftheorem defines :::"Tsingle_e_net"::: E_SIEC:def 7 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_e_siec :::"Tsingle_e_net"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "#)" ))); theorem :: E_SIEC:8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_e_siec :::"Psingle_e_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set "(" ($#k4_e_siec :::"Psingle_e_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set "(" ($#k4_e_siec :::"Psingle_e_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_relat_1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ")" )) ; theorem :: E_SIEC:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_e_siec :::"Tsingle_e_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set "(" ($#k5_e_siec :::"Tsingle_e_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set "(" ($#k5_e_siec :::"Tsingle_e_net"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: E_SIEC:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "#)" ) "is" ($#l1_e_siec :::"e_net":::))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; func :::"PTempty_e_net"::: "(" "X" "," "Y" ")" -> ($#v1_e_siec :::"strict"::: ) ($#l1_e_siec :::"e_net":::) equals :: E_SIEC:def 8 (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set "(" "X" ($#k2_xboole_0 :::"\/"::: ) "Y" ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) "X" ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"PTempty_e_net"::: E_SIEC:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_e_siec :::"PTempty_e_net"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_e_siec :::"G_Net"::: ) "(#" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) "#)" ))); theorem :: E_SIEC:11 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ))) ")" )) ; theorem :: E_SIEC:12 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k1_sysrel :::"CL"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k1_sysrel :::"CL"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N")))))) ; theorem :: E_SIEC:13 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_sysrel :::"CL"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))))) ")" )) ; theorem :: E_SIEC:14 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N")))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N")))) ")" )) ; theorem :: E_SIEC:15 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: E_SIEC:16 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_Places"::: "N" -> ($#m1_hidden :::"set"::: ) equals :: E_SIEC:def 9 (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N")); end; :: deftheorem defines :::"e_Places"::: E_SIEC:def 9 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))))); definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_Transitions"::: "N" -> ($#m1_hidden :::"set"::: ) equals :: E_SIEC:def 10 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) "N" ")" )); end; :: deftheorem defines :::"e_Transitions"::: E_SIEC:def 10 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" )))); theorem :: E_SIEC:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "st" (Bool (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N")))) "or" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N")))) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")))) ")" ))) ; theorem :: E_SIEC:18 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_Flow"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 11 (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k3_struct_0 :::"id"::: ) "N" ")" )); end; :: deftheorem defines :::"e_Flow"::: E_SIEC:def 11 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k9_e_siec :::"e_Flow"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "N")) ")" )))); theorem :: E_SIEC:19 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k9_e_siec :::"e_Flow"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_pre"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 12 (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" )); func :::"e_post"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 13 (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" )); end; :: deftheorem defines :::"e_pre"::: E_SIEC:def 12 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k10_e_siec :::"e_pre"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" )))); :: deftheorem defines :::"e_post"::: E_SIEC:def 13 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k11_e_siec :::"e_post"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" )))); theorem :: E_SIEC:20 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set ($#k10_e_siec :::"e_pre"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k11_e_siec :::"e_post"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_shore"::: "N" -> ($#m1_hidden :::"set"::: ) equals :: E_SIEC:def 14 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N"); func :::"e_prox"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 15 (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ")" ) ($#k2_relat_1 :::"~"::: ) ); func :::"e_flow"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 16 (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" )); end; :: deftheorem defines :::"e_shore"::: E_SIEC:def 14 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))))); :: deftheorem defines :::"e_prox"::: E_SIEC:def 15 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ($#k2_relat_1 :::"~"::: ) ))); :: deftheorem defines :::"e_flow"::: E_SIEC:def 16 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" )))); theorem :: E_SIEC:21 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: E_SIEC:22 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")))) & (Bool (Set (Set "(" (Set "(" ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k13_e_siec :::"e_prox"::: ) (Set (Var "N")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ))) ")" )) ; theorem :: E_SIEC:23 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ))) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ))) ")" )) ; theorem :: E_SIEC:24 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: E_SIEC:25 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: E_SIEC:26 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) )) ")" )) ; theorem :: E_SIEC:27 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: E_SIEC:28 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_entrance"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 17 (Set (Set "(" (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ")" ) ")" ) ")" )); func :::"e_escape"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 18 (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ")" ) ")" ) ")" )); end; :: deftheorem defines :::"e_entrance"::: E_SIEC:def 17 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" )))); :: deftheorem defines :::"e_escape"::: E_SIEC:def 18 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" )))); theorem :: E_SIEC:29 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")))) & (Bool (Set (Set "(" ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")))) & (Bool (Set (Set "(" ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")))) & (Bool (Set (Set "(" ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")))) ")" )) ; theorem :: E_SIEC:30 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k15_e_siec :::"e_entrance"::: ) (Set (Var "N")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" ($#k16_e_siec :::"e_escape"::: ) (Set (Var "N")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; definitionlet "N" be ($#l1_e_siec :::"e_net":::); func :::"e_adjac"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 19 (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ")" ) ")" ) ")" )); end; :: deftheorem defines :::"e_adjac"::: E_SIEC:def 19 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool (Set ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ")" )))); theorem :: E_SIEC:31 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; theorem :: E_SIEC:32 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")))) & (Bool (Set (Set "(" (Set "(" ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k17_e_siec :::"e_adjac"::: ) (Set (Var "N")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "(" ($#k12_e_siec :::"e_shore"::: ) (Set (Var "N")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k14_e_siec :::"e_flow"::: ) (Set (Var "N")) ")" ) ($#k2_relat_1 :::"~"::: ) ")" ))) ")" )) ; theorem :: E_SIEC:33 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ; definitionlet "N" be ($#l1_e_siec :::"G_Net"::: ) ; func :::"s_pre"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 20 (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ); func :::"s_post"::: "N" -> ($#m1_hidden :::"Relation":::) equals :: E_SIEC:def 21 (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" "N") ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "N") ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ); end; :: deftheorem defines :::"s_pre"::: E_SIEC:def 20 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"G_Net"::: ) "holds" (Bool (Set ($#k18_e_siec :::"s_pre"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u2_e_siec :::"escape"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ))); :: deftheorem defines :::"s_post"::: E_SIEC:def 21 : (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"G_Net"::: ) "holds" (Bool (Set ($#k19_e_siec :::"s_post"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_e_siec :::"entrance"::: ) "of" (Set (Var "N"))) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ")" ) ")" ) ($#k2_relat_1 :::"~"::: ) ))); theorem :: E_SIEC:34 (Bool "for" (Set (Var "N")) "being" ($#l1_e_siec :::"e_net":::) "holds" (Bool "(" (Bool (Set ($#k19_e_siec :::"s_post"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k18_e_siec :::"s_pre"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k7_e_siec :::"e_Places"::: ) (Set (Var "N")) ")" ) "," (Set "(" ($#k8_e_siec :::"e_Transitions"::: ) (Set (Var "N")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" )) ;