:: BOOLMARK  semantic presentation begin  
theorem :: BOOLMARK:1 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "B")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "C"))  ($#k1_margrel1 :::"-->"::: )  (Set (Var "v")) ")" )) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))))))) ; 
 
theorem :: BOOLMARK:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "A")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))))) ; 
 
theorem :: BOOLMARK:3 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "A"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "x")) ")" ) ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "B"))))))) ; 
 begin  definitionlet "PTN" be    ($#l1_petri :::"PT_net_Str"::: )  ; func  :::"Bool_marks_of"::: "PTN" ->    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "PTN") "," (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: BOOLMARK:def 1 (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "PTN") "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ); end; 





:: deftheorem    defines :::"Bool_marks_of"::: BOOLMARK:def 1 :  (Bool  "for" (Set (Var "PTN")) "being"    ($#l1_petri :::"PT_net_Str"::: )   "holds"  (Bool (Set   ($#k1_boolmark :::"Bool_marks_of"::: )  (Set (Var "PTN")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PTN"))) "," (Set  ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ))); 
 definitionlet "PTN" be    ($#l1_petri :::"PT_net_Str"::: )  ; mode Boolean_marking of "PTN" is    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_boolmark :::"Bool_marks_of"::: )  "PTN"); end; definitionlet "PTN" be   ($#l1_petri :::"Petri_net":::); let "M0" be   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Const "PTN")); let "t" be   ($#m1_subset_1 :::"transition":::) "of" (Set (Const "PTN")); pred "t" :::"is_firable_on"::: "M0" means :: BOOLMARK:def 2 (Bool (Set "M0"  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k8_petri :::"*'"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "t" ($#k6_domain_1 :::"}"::: ) ) ")" ))  ($#r1_tarski :::"c="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k6_domain_1 :::"}"::: ) )); end; 






:: deftheorem    defines :::"is_firable_on"::: BOOLMARK:def 2 :  (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "holds"   (Bool  "("  (Bool (Set (Var "t"))  ($#r1_boolmark :::"is_firable_on"::: )  (Set (Var "M0"))) "iff" (Bool (Set (Set (Var "M0"))  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k8_petri :::"*'"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ")" ))  ($#r1_tarski :::"c="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ($#k6_domain_1 :::"}"::: ) ))  ")" )))); 
 notationlet "PTN" be   ($#l1_petri :::"Petri_net":::); let "M0" be   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Const "PTN")); let "t" be   ($#m1_subset_1 :::"transition":::) "of" (Set (Const "PTN")); antonym "t" :::"is_not_firable_on"::: "M0" for "t" :::"is_firable_on"::: "M0"; end; definitionlet "PTN" be   ($#l1_petri :::"Petri_net":::); let "M0" be   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Const "PTN")); let "t" be   ($#m1_subset_1 :::"transition":::) "of" (Set (Const "PTN")); func  :::"Firing":::  "(" "t" "," "M0" ")"  ->   ($#m2_funct_2 :::"Boolean_marking":::) "of" "PTN" equals :: BOOLMARK:def 3 (Set (Set  "(" "M0"  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "("  ($#k8_petri :::"*'"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "t" ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k1_margrel1 :::"-->"::: )  (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Set  ($#k6_domain_1 :::"{"::: ) "t" ($#k6_domain_1 :::"}"::: ) )  ($#k9_petri :::"*'"::: )  ")" )  ($#k1_margrel1 :::"-->"::: )  (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ")" )); end; 







:: deftheorem    defines :::"Firing"::: BOOLMARK:def 3 :  (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "holds"  (Bool (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set (Var "t")) "," (Set (Var "M0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "M0"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "("  ($#k8_petri :::"*'"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k1_margrel1 :::"-->"::: )  (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) )  ($#k9_petri :::"*'"::: )  ")" )  ($#k1_margrel1 :::"-->"::: )  (Set  ($#k8_margrel1 :::"TRUE"::: ) ) ")" )))))); 
 definitionlet "PTN" be   ($#l1_petri :::"Petri_net":::); let "M0" be   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Const "PTN")); let "Q" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Const "PTN"))); pred "Q" :::"is_firable_on"::: "M0" means :: BOOLMARK:def 4 (Bool  "("  (Bool "Q"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool  "ex" (Set (Var "M")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_boolmark :::"Bool_marks_of"::: )  "PTN") "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "Q")  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")))) & (Bool (Set "Q"  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_boolmark :::"is_firable_on"::: )  "M0") & (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" "Q"  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," "M0" ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "Q")) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set "Q"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_boolmark :::"is_firable_on"::: )  (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" "Q"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" ))  ")" )  ")" )  ")" ))  ")" ); end; 






:: deftheorem    defines :::"is_firable_on"::: BOOLMARK:def 4 :  (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "Q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "PTN"))) "holds"   (Bool  "("  (Bool (Set (Var "Q"))  ($#r2_boolmark :::"is_firable_on"::: )  (Set (Var "M0"))) "iff" (Bool  "("  (Bool (Set (Var "Q"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool  "ex" (Set (Var "M")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_boolmark :::"Bool_marks_of"::: )  (Set (Var "PTN"))) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Q")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")))) & (Bool (Set (Set (Var "Q"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_boolmark :::"is_firable_on"::: )  (Set (Var "M0"))) & (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" (Set (Var "Q"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," (Set (Var "M0")) ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Q")))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "Q"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_boolmark :::"is_firable_on"::: )  (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" (Set (Var "Q"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" ))  ")" )  ")" )  ")" ))  ")" )  ")" )))); 
 notationlet "PTN" be   ($#l1_petri :::"Petri_net":::); let "M0" be   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Const "PTN")); let "Q" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Const "PTN"))); antonym "Q" :::"is_not_firable_on"::: "M0" for "Q" :::"is_firable_on"::: "M0"; end; definitionlet "PTN" be   ($#l1_petri :::"Petri_net":::); let "M0" be   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Const "PTN")); let "Q" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Const "PTN"))); func  :::"Firing":::  "(" "Q" "," "M0" ")"  ->   ($#m2_funct_2 :::"Boolean_marking":::) "of" "PTN" means :: BOOLMARK:def 5 (Bool it  ($#r2_funct_2 :::"="::: )  "M0") if (Bool "Q"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool  "ex" (Set (Var "M")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_boolmark :::"Bool_marks_of"::: )  "PTN") "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "Q")  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")) ")" ))) & (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" "Q"  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," "M0" ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "Q")) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" "Q"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" ))  ")" )  ")" )); end; 







:: deftheorem    defines :::"Firing"::: BOOLMARK:def 5 :  (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "Q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "PTN")))  (Bool  "for" (Set (Var "b4")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "Q"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_boolmark :::"Firing"::: )   "(" (Set (Var "Q")) "," (Set (Var "M0")) ")" )) "iff" (Bool (Set (Var "b4"))  ($#r2_funct_2 :::"="::: )  (Set (Var "M0")))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "Q"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_boolmark :::"Firing"::: )   "(" (Set (Var "Q")) "," (Set (Var "M0")) ")" )) "iff" (Bool  "ex" (Set (Var "M")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_boolmark :::"Bool_marks_of"::: )  (Set (Var "PTN"))) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Q")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "M")) ")" ))) & (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" (Set (Var "Q"))  ($#k7_partfun1 :::"/."::: )  (Num 1) ")" ) "," (Set (Var "M0")) ")" )) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Q")))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set  "(" (Set (Var "Q"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) "," (Set  "(" (Set (Var "M"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")) ")" ) ")" ))  ")" )  ")" ))  ")" )  ")"   ")" ))))); 
 
theorem :: BOOLMARK:4 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "A"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "y")) ")" ) ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: BOOLMARK:5 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"place":::) "of" (Set (Var "PTN"))  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "t")) ($#k6_domain_1 :::"}"::: ) )  ($#k9_petri :::"*'"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k2_boolmark :::"Firing"::: )   "(" (Set (Var "t")) "," (Set (Var "M0")) ")"  ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )))))) ; 
 
theorem :: BOOLMARK:6 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "Sd")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PTN"))) "holds"   (Bool  "("  (Bool (Set (Var "Sd")) "is"   ($#v4_petri :::"Deadlock-like"::: )  ) "iff" (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  "st" (Bool (Bool (Set (Set (Var "M0"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "Sd")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN"))  "st" (Bool (Bool (Set (Var "t"))  ($#r1_boolmark :::"is_firable_on"::: )  (Set (Var "M0")))) "holds"  (Bool (Set (Set  "("  ($#k2_boolmark :::"Firing"::: )   "(" (Set (Var "t")) "," (Set (Var "M0")) ")"  ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "Sd")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k6_domain_1 :::"}"::: ) ))))  ")" ))) ; 
 
theorem :: BOOLMARK:7 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Q0")) "," (Set (Var "Q1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "Q0"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "Q0"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "Q1")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Q0"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "i"))))))) ; 
 
theorem :: BOOLMARK:8 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "Q0")) "," (Set (Var "Q1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "PTN"))) "holds"  (Bool (Set   ($#k3_boolmark :::"Firing"::: )   "(" (Set  "(" (Set (Var "Q0"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "Q1")) ")" ) "," (Set (Var "M0")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_boolmark :::"Firing"::: )   "(" (Set (Var "Q1")) "," (Set  "("  ($#k3_boolmark :::"Firing"::: )   "(" (Set (Var "Q0")) "," (Set (Var "M0")) ")"  ")" ) ")" ))))) ; 
 
theorem :: BOOLMARK:9 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "Q0")) "," (Set (Var "Q1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "PTN")))  "st" (Bool (Bool (Set (Set (Var "Q0"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "Q1")))  ($#r2_boolmark :::"is_firable_on"::: )  (Set (Var "M0")))) "holds"  (Bool  "("  (Bool (Set (Var "Q1"))  ($#r2_boolmark :::"is_firable_on"::: )  (Set   ($#k3_boolmark :::"Firing"::: )   "(" (Set (Var "Q0")) "," (Set (Var "M0")) ")" )) & (Bool (Set (Var "Q0"))  ($#r2_boolmark :::"is_firable_on"::: )  (Set (Var "M0")))  ")" )))) ; 
 
theorem :: BOOLMARK:10 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "holds"   (Bool  "("  (Bool (Set (Var "t"))  ($#r1_boolmark :::"is_firable_on"::: )  (Set (Var "M0"))) "iff" (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "t")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r2_boolmark :::"is_firable_on"::: )  (Set (Var "M0")))  ")" )))) ; 
 
theorem :: BOOLMARK:11 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"transition":::) "of" (Set (Var "PTN")) "holds"  (Bool (Set   ($#k2_boolmark :::"Firing"::: )   "(" (Set (Var "t")) "," (Set (Var "M0")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_boolmark :::"Firing"::: )   "(" (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "t")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "M0")) ")" ))))) ; 
 
theorem :: BOOLMARK:12 (Bool  "for" (Set (Var "PTN")) "being"   ($#l1_petri :::"Petri_net":::)  (Bool  "for" (Set (Var "Sd")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "PTN"))) "holds"   (Bool  "("  (Bool (Set (Var "Sd")) "is"   ($#v4_petri :::"Deadlock-like"::: )  ) "iff" (Bool  "for" (Set (Var "M0")) "being"   ($#m2_funct_2 :::"Boolean_marking":::) "of" (Set (Var "PTN"))  "st" (Bool (Bool (Set (Set (Var "M0"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "Sd")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool  "for" (Set (Var "Q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "PTN")))  "st" (Bool (Bool (Set (Var "Q"))  ($#r2_boolmark :::"is_firable_on"::: )  (Set (Var "M0")))) "holds"  (Bool (Set (Set  "("  ($#k3_boolmark :::"Firing"::: )   "(" (Set (Var "Q")) "," (Set (Var "M0")) ")"  ")" )  ($#k7_relat_1 :::".:"::: )  (Set (Var "Sd")))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  ($#k7_margrel1 :::"FALSE"::: ) ) ($#k6_domain_1 :::"}"::: ) ))))  ")" ))) ;