:: PNPROC_1 semantic presentation begin theorem :: PNPROC_1:1 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_hidden :::"FinSubsequence":::)))) ; theorem :: PNPROC_1:2 (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: PNPROC_1:3 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PNPROC_1:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: PNPROC_1:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) "is" ($#m1_hidden :::"FinSequence":::)) "or" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Num 2)) ")" ) "or" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )) ; theorem :: PNPROC_1:6 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "x1")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Num 2) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: PNPROC_1:7 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "p")) ")" )))) ; theorem :: PNPROC_1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "P")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y")))))) ; theorem :: PNPROC_1:9 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) & (Bool (Set (Var "f")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) ; theorem :: PNPROC_1:10 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "R")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; theorem :: PNPROC_1:11 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y")) ")" ))))) ; begin definitionlet "P" be ($#m1_hidden :::"set"::: ) ; mode marking of "P" is ($#m1_subset_1 :::"Function":::) "of" "P" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; notationlet "P" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); let "p" be ($#m1_hidden :::"set"::: ) ; synonym "m" :::"multitude_of"::: "p" for "P" :::"."::: "m"; end; scheme :: PNPROC_1:sch 1 MarkingLambda{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) } : (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "p")) ")" )))) proof end; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); :: original: :::"="::: redefine pred "m1" :::"="::: "m2" means :: PNPROC_1:def 1 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ))); end; :: deftheorem defines :::"="::: PNPROC_1:def 1 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "m1")) ($#r1_pnproc_1 :::"="::: ) (Set (Var "m2"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ))) ")" ))); definitionlet "P" be ($#m1_hidden :::"set"::: ) ; func :::"{$}"::: "P" -> ($#m1_subset_1 :::"marking":::) "of" "P" equals :: PNPROC_1:def 2 (Set "P" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"{$}"::: PNPROC_1:def 2 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_pnproc_1 :::"{$}"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))); definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); pred "m1" :::"c="::: "m2" means :: PNPROC_1:def 3 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ))); reflexivity (Bool "for" (Set (Var "m1")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Const "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) )))) ; end; :: deftheorem defines :::"c="::: PNPROC_1:def 3 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ))) ")" ))); theorem :: PNPROC_1:12 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set ($#k1_pnproc_1 :::"{$}"::: ) (Set (Var "P"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m"))))) ; theorem :: PNPROC_1:13 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) & (Bool (Set (Var "m2")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m3")))) "holds" (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m3"))))) ; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); :: original: :::"+"::: redefine func "m1" :::"+"::: "m2" -> ($#m1_subset_1 :::"marking":::) "of" "P" means :: PNPROC_1:def 4 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" )))); end; :: deftheorem defines :::"+"::: PNPROC_1:def 4 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m2")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" )))) ")" ))); theorem :: PNPROC_1:14 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "m")) ($#k2_pnproc_1 :::"+"::: ) (Set "(" ($#k1_pnproc_1 :::"{$}"::: ) (Set (Var "P")) ")" )) ($#r1_pnproc_1 :::"="::: ) (Set (Var "m"))))) ; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); assume (Bool (Set (Const "m2")) ($#r2_pnproc_1 :::"c="::: ) (Set (Const "m1"))) ; func "m1" :::"-"::: "m2" -> ($#m1_subset_1 :::"marking":::) "of" "P" means :: PNPROC_1:def 5 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" )))); end; :: deftheorem defines :::"-"::: PNPROC_1:def 5 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m2")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m1")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m2")))) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"multitude_of"::: ) ")" )))) ")" )))); theorem :: PNPROC_1:15 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m2")))))) ; theorem :: PNPROC_1:16 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "m")) ($#k3_pnproc_1 :::"-"::: ) (Set "(" ($#k1_pnproc_1 :::"{$}"::: ) (Set (Var "P")) ")" )) ($#r1_pnproc_1 :::"="::: ) (Set (Var "m"))))) ; theorem :: PNPROC_1:17 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) & (Bool (Set (Var "m2")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m3")))) "holds" (Bool (Set (Set (Var "m3")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m2"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Set (Var "m3")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m1")))))) ; theorem :: PNPROC_1:18 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set "(" (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m2")) ")" ) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m2"))) ($#r1_pnproc_1 :::"="::: ) (Set (Var "m1"))))) ; theorem :: PNPROC_1:19 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m1"))) & (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Set (Var "m2")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m")))))) ; theorem :: PNPROC_1:20 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Set "(" (Set (Var "m2")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3")) ")" ) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m1"))) ($#r1_pnproc_1 :::"="::: ) (Set (Set "(" (Set (Var "m2")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m1")) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3")))))) ; theorem :: PNPROC_1:21 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) & (Bool (Set (Var "m2")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m1")))) "holds" (Bool (Set (Var "m1")) ($#r1_pnproc_1 :::"="::: ) (Set (Var "m2"))))) ; theorem :: PNPROC_1:22 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set "(" (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m2")) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3"))) ($#r1_pnproc_1 :::"="::: ) (Set (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set "(" (Set (Var "m2")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3")) ")" ))))) ; theorem :: PNPROC_1:23 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "," (Set (Var "m4")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) & (Bool (Set (Var "m3")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m4")))) "holds" (Bool (Set (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Set (Var "m2")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m4")))))) ; theorem :: PNPROC_1:24 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Set (Var "m2")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m1"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))))) ; theorem :: PNPROC_1:25 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "," (Set (Var "m4")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) & (Bool (Set (Var "m3")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m4"))) & (Bool (Set (Var "m4")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m1")))) "holds" (Bool (Set (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m4"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Set (Var "m2")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m3")))))) ; theorem :: PNPROC_1:26 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m1")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2")))) "holds" (Bool (Set (Var "m2")) ($#r1_pnproc_1 :::"="::: ) (Set (Set "(" (Set (Var "m2")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m1")) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m1")))))) ; theorem :: PNPROC_1:27 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set "(" (Set (Var "m1")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m2")) ")" ) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m1"))) ($#r1_pnproc_1 :::"="::: ) (Set (Var "m2"))))) ; theorem :: PNPROC_1:28 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m2")) "," (Set (Var "m3")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Set (Var "m2")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m1")))) "holds" (Bool (Set (Set "(" (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m2")) ")" ) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m3"))) ($#r1_pnproc_1 :::"="::: ) (Set (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set "(" (Set (Var "m2")) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3")) ")" ))))) ; theorem :: PNPROC_1:29 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m3")) "," (Set (Var "m2")) "," (Set (Var "m1")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "m3")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m2"))) & (Bool (Set (Var "m2")) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m1")))) "holds" (Bool (Set (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set "(" (Set (Var "m2")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m3")) ")" )) ($#r1_pnproc_1 :::"="::: ) (Set (Set "(" (Set (Var "m1")) ($#k3_pnproc_1 :::"-"::: ) (Set (Var "m2")) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set (Var "m3")))))) ; begin definitionlet "P" be ($#m1_hidden :::"set"::: ) ; mode :::"transition"::: "of" "P" -> ($#m1_hidden :::"set"::: ) means :: PNPROC_1:def 6 (Bool "ex" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" "P" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m1")) "," (Set (Var "m2")) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"transition"::: PNPROC_1:def 6 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P"))) "iff" (Bool "ex" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m1")) "," (Set (Var "m2")) ($#k4_tarski :::"]"::: ) ))) ")" ))); notationlet "P" be ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Const "P")); synonym :::"Pre"::: "t" for "P" :::"`1"::: ; synonym :::"Post"::: "t" for "P" :::"`2"::: ; end; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Const "P")); :: original: :::"Pre"::: redefine func :::"Pre"::: "t" -> ($#m1_subset_1 :::"marking":::) "of" "P"; :: original: :::"Post"::: redefine func :::"Post"::: "t" -> ($#m1_subset_1 :::"marking":::) "of" "P"; end; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); let "t" be ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Const "P")); func :::"fire"::: "(" "t" "," "m" ")" -> ($#m1_subset_1 :::"marking":::) "of" "P" equals :: PNPROC_1:def 7 (Set (Set "(" "m" ($#k3_pnproc_1 :::"-"::: ) (Set "(" ($#k4_pnproc_1 :::"Pre"::: ) "t" ")" ) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set "(" ($#k5_pnproc_1 :::"Post"::: ) "t" ")" )) if (Bool (Set ($#k4_pnproc_1 :::"Pre"::: ) "t") ($#r2_pnproc_1 :::"c="::: ) "m") otherwise "m"; end; :: deftheorem defines :::"fire"::: PNPROC_1:def 7 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "t")) "being" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m")))) "implies" (Bool (Set ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k3_pnproc_1 :::"-"::: ) (Set "(" ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t")) ")" ) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set "(" ($#k5_pnproc_1 :::"Post"::: ) (Set (Var "t")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t"))) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m"))))) "implies" (Bool (Set ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ")" )))); theorem :: PNPROC_1:30 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Set "(" ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t1")) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set "(" ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t2")) ")" )) ($#r2_pnproc_1 :::"c="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t2")) "," (Set "(" ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t1")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#r1_pnproc_1 :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "m")) ($#k3_pnproc_1 :::"-"::: ) (Set "(" ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t1")) ")" ) ")" ) ($#k3_pnproc_1 :::"-"::: ) (Set "(" ($#k4_pnproc_1 :::"Pre"::: ) (Set (Var "t2")) ")" ) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set "(" ($#k5_pnproc_1 :::"Post"::: ) (Set (Var "t1")) ")" ) ")" ) ($#k2_pnproc_1 :::"+"::: ) (Set "(" ($#k5_pnproc_1 :::"Post"::: ) (Set (Var "t2")) ")" )))))) ; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Const "P")); func :::"fire"::: "t" -> ($#m1_hidden :::"Function":::) means :: PNPROC_1:def 8 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "P" "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" "P" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pnproc_1 :::"fire"::: ) "(" "t" "," (Set (Var "m")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"fire"::: PNPROC_1:def 8 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "t")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" )) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t")) "," (Set (Var "m")) ")" )) ")" ) ")" ) ")" )))); theorem :: PNPROC_1:31 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "t")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" )))) ; theorem :: PNPROC_1:32 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) (Bool "for" (Set (Var "t2")) "," (Set (Var "t1")) "being" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P")) "holds" (Bool (Set ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t2")) "," (Set "(" ($#k6_pnproc_1 :::"fire"::: ) "(" (Set (Var "t1")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "t2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "t1")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))))) ; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; mode :::"Petri_net"::: "of" "P" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: PNPROC_1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) "is" ($#m1_pnproc_1 :::"transition"::: ) "of" "P")); end; :: deftheorem defines :::"Petri_net"::: PNPROC_1:def 9 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_pnproc_1 :::"transition"::: ) "of" (Set (Var "P")))) ")" ))); definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "N" -> ($#m1_pnproc_1 :::"transition"::: ) "of" "P"; end; begin definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); mode firing-sequence of "N" is ($#m2_finseq_2 :::"Element"::: ) "of" (Set "N" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "C" be ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Const "N")); func :::"fire"::: "C" -> ($#m1_hidden :::"Function":::) means :: PNPROC_1:def 10 (Bool "ex" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "P" "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "C")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "C"))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k7_pnproc_1 :::"fire"::: ) (Set "(" "C" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"fire"::: PNPROC_1:def 10 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_7 :::"compose"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) ")" )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "C")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k7_pnproc_1 :::"fire"::: ) (Set "(" (Set (Var "C")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" )) ")" ))))); theorem :: PNPROC_1:33 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) "holds" (Bool (Set ($#k8_pnproc_1 :::"fire"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ))))) ; theorem :: PNPROC_1:34 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "e")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) "holds" (Bool (Set ($#k8_pnproc_1 :::"fire"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e")) ($#k3_pre_poly :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "e"))))))) ; theorem :: PNPROC_1:35 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "e")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "e")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "e"))))))) ; theorem :: PNPROC_1:36 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) "holds" (Bool (Set ($#k8_pnproc_1 :::"fire"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e1")) "," (Set (Var "e2")) ($#k4_pre_poly :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "e2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "e1")) ")" )))))) ; theorem :: PNPROC_1:37 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" )) ")" )))) ; theorem :: PNPROC_1:38 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) "holds" (Bool (Set ($#k8_pnproc_1 :::"fire"::: ) (Set "(" (Set (Var "C1")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C1")) ")" )))))) ; theorem :: PNPROC_1:39 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "e")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) (Bool "for" (Set (Var "C")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) "holds" (Bool (Set ($#k8_pnproc_1 :::"fire"::: ) (Set "(" (Set (Var "C")) ($#k1_pre_poly :::"^"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e")) ($#k3_pre_poly :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_pnproc_1 :::"fire"::: ) (Set (Var "e")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C")) ")" ))))))) ; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "C" be ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Const "N")); let "m" be ($#m1_subset_1 :::"marking":::) "of" (Set (Const "P")); func :::"fire"::: "(" "C" "," "m" ")" -> ($#m1_subset_1 :::"marking":::) "of" "P" equals :: PNPROC_1:def 11 (Set (Set "(" ($#k8_pnproc_1 :::"fire"::: ) "C" ")" ) ($#k1_funct_1 :::"."::: ) "m"); end; :: deftheorem defines :::"fire"::: PNPROC_1:def 11 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"marking":::) "of" (Set (Var "P")) "holds" (Bool (Set ($#k9_pnproc_1 :::"fire"::: ) "(" (Set (Var "C")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_pnproc_1 :::"fire"::: ) (Set (Var "C")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))))); begin definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); mode process of "N" is ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "N" ($#k3_finseq_2 :::"*"::: ) ")" ); end; definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "R1", "R2" be ($#m1_subset_1 :::"process":::) "of" (Set (Const "N")); func "R1" :::"before"::: "R2" -> ($#m1_subset_1 :::"process":::) "of" "N" equals :: PNPROC_1:def 12 "{" (Set "(" (Set (Var "C1")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C2")) ")" ) where C1, C2 "is" ($#m2_finseq_2 :::"firing-sequence":::) "of" "N" : (Bool "(" (Bool (Set (Var "C1")) ($#r2_hidden :::"in"::: ) "R1") & (Bool (Set (Var "C2")) ($#r2_hidden :::"in"::: ) "R2") ")" ) "}" ; end; :: deftheorem defines :::"before"::: PNPROC_1:def 12 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "C1")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C2")) ")" ) where C1, C2 "is" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) : (Bool "(" (Bool (Set (Var "C1")) ($#r2_hidden :::"in"::: ) (Set (Var "R1"))) & (Bool (Set (Var "C2")) ($#r2_hidden :::"in"::: ) (Set (Var "R2"))) ")" ) "}" )))); registrationlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "R1", "R2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"process":::) "of" (Set (Const "N")); cluster (Set "R1" ($#k10_pnproc_1 :::"before"::: ) "R2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: PNPROC_1:40 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "R2")) ")" ) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "R2")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R")) ")" )))))) ; theorem :: PNPROC_1:41 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R")) "," (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "R")) ($#k10_pnproc_1 :::"before"::: ) (Set "(" (Set (Var "R1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "R")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R2")) ")" )))))) ; theorem :: PNPROC_1:42 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "C1")) ($#k6_domain_1 :::"}"::: ) ) ($#k10_pnproc_1 :::"before"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "C2")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "C1")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C2")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: PNPROC_1:43 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "," (Set (Var "C")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k7_domain_1 :::"}"::: ) ) ($#k10_pnproc_1 :::"before"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "C")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "C1")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C")) ")" ) "," (Set "(" (Set (Var "C2")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C")) ")" ) ($#k7_domain_1 :::"}"::: ) ))))) ; theorem :: PNPROC_1:44 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "C")) "," (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "C")) ($#k6_domain_1 :::"}"::: ) ) ($#k10_pnproc_1 :::"before"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "C1")) "," (Set (Var "C2")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "C")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C1")) ")" ) "," (Set "(" (Set (Var "C")) ($#k1_pre_poly :::"^"::: ) (Set (Var "C2")) ")" ) ($#k7_domain_1 :::"}"::: ) ))))) ; begin definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "R1", "R2" be ($#m1_subset_1 :::"process":::) "of" (Set (Const "N")); func "R1" :::"concur"::: "R2" -> ($#m1_subset_1 :::"process":::) "of" "N" equals :: PNPROC_1:def 13 "{" (Set (Var "C")) where C "is" ($#m2_finseq_2 :::"firing-sequence":::) "of" "N" : (Bool "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "q2"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1"))) ($#r2_hidden :::"in"::: ) "R1") & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2"))) ($#r2_hidden :::"in"::: ) "R2") ")" )) "}" ; commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Const "N")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Const "N")) : (Bool "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "q2"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1"))) ($#r2_hidden :::"in"::: ) (Set (Var "R1"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2"))) ($#r2_hidden :::"in"::: ) (Set (Var "R2"))) ")" )) "}" )) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Const "N")) : (Bool "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "q2"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1"))) ($#r2_hidden :::"in"::: ) (Set (Var "R2"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2"))) ($#r2_hidden :::"in"::: ) (Set (Var "R1"))) ")" )) "}" )) ; end; :: deftheorem defines :::"concur"::: PNPROC_1:def 13 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "C")) where C "is" ($#m2_finseq_2 :::"firing-sequence":::) "of" (Set (Var "N")) : (Bool "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "q2"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1"))) ($#r2_hidden :::"in"::: ) (Set (Var "R1"))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2"))) ($#r2_hidden :::"in"::: ) (Set (Var "R2"))) ")" )) "}" )))); theorem :: PNPROC_1:45 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "R2")) ")" ) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "R2")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R")) ")" )))))) ; theorem :: PNPROC_1:46 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e1")) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ($#k11_pnproc_1 :::"concur"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e2")) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e1")) "," (Set (Var "e2")) ($#k4_pre_poly :::"*>"::: ) ) "," (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e2")) "," (Set (Var "e1")) ($#k4_pre_poly :::"*>"::: ) ) ($#k7_domain_1 :::"}"::: ) ))))) ; theorem :: PNPROC_1:47 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "e")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) "holds" (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e1")) ($#k3_pre_poly :::"*>"::: ) ) "," (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e2")) ($#k3_pre_poly :::"*>"::: ) ) ($#k7_domain_1 :::"}"::: ) ) ($#k11_pnproc_1 :::"concur"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "e")) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e1")) "," (Set (Var "e")) ($#k4_pre_poly :::"*>"::: ) ) "," (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e2")) "," (Set (Var "e")) ($#k4_pre_poly :::"*>"::: ) ) "," (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e")) "," (Set (Var "e1")) ($#k4_pre_poly :::"*>"::: ) ) "," (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "e")) "," (Set (Var "e2")) ($#k4_pre_poly :::"*>"::: ) ) ($#k9_domain_1 :::"}"::: ) ))))) ; theorem :: PNPROC_1:48 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R2")) ")" ) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set "(" (Set (Var "R2")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R3")) ")" )))))) ; definitionlet "p" be ($#m1_hidden :::"FinSubsequence":::); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "i" :::"Shift"::: "p" -> ($#m1_hidden :::"FinSubsequence":::) means :: PNPROC_1:def 14 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "{" (Set "(" "i" ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) "}" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" "i" ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ) ")" ); end; :: deftheorem defines :::"Shift"::: PNPROC_1:def 14 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSubsequence":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) "}" ) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) ")" ) ")" ) ")" )))); theorem :: PNPROC_1:49 (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: PNPROC_1:50 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set "(" (Set (Var "j")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ))))) ; theorem :: PNPROC_1:51 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set (Var "j1")) where j1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j1"))) & (Bool (Set (Var "j1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" ) "}" ))) ; theorem :: PNPROC_1:52 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: PNPROC_1:53 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) (Bool "ex" (Set (Var "ss")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "ss"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "ss"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "ss")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")))) ")" ) & (Bool (Set (Var "ss")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )))) ; theorem :: PNPROC_1:54 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ))))) ; theorem :: PNPROC_1:55 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: PNPROC_1:56 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")))))) ; theorem :: PNPROC_1:57 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: PNPROC_1:58 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: PNPROC_1:59 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "p1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p2")) ")" ) ")" )))) ; theorem :: PNPROC_1:60 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i")))) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p2")) ")" )))))) ; theorem :: PNPROC_1:61 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p2")) ")" )))) ; theorem :: PNPROC_1:62 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p1")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set (Var "p1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p2"))))))) ; theorem :: PNPROC_1:63 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R2")) ")" ) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set "(" (Set (Var "R2")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R3")) ")" )))))) ; theorem :: PNPROC_1:64 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R2"))))))) ; theorem :: PNPROC_1:65 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "P1")) "," (Set (Var "R2")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "R1")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "R2")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "P2"))))))) ; theorem :: PNPROC_1:66 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "P1")) "," (Set (Var "R2")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "R1")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "R2")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool (Set (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "P1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "P2"))))))) ; theorem :: PNPROC_1:67 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p")))))) ; theorem :: PNPROC_1:68 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "p2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2"))))) ; theorem :: PNPROC_1:69 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q2"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q1")) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q2")) ")" ))))) ; theorem :: PNPROC_1:70 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "q2")))) & (Bool (Set (Var "q1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "q2")))) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")))))) ; theorem :: PNPROC_1:71 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ) ")" ))))) ; theorem :: PNPROC_1:72 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q")) ")" )))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")))) ")" )))) ; theorem :: PNPROC_1:73 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q")) ")" )))) "holds" (Bool (Set (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))) ; theorem :: PNPROC_1:74 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "holds" (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k15_finseq_1 :::"Seq"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" ))))) ; theorem :: PNPROC_1:75 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k"))))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "i")) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))))) ; theorem :: PNPROC_1:76 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q1")) ($#r1_tarski :::"c="::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "ss")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Set (Var "ss")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q2")) ")" )))))) ; theorem :: PNPROC_1:77 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q1")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q2")) ($#r1_tarski :::"c="::: ) (Set (Var "p2")))) "holds" (Bool "ex" (Set (Var "ss")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "ss")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q2")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "ss")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2")) ")" ) ")" ) ")" ))) ")" )))) ; theorem :: PNPROC_1:78 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q1")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q2")) ($#r1_tarski :::"c="::: ) (Set (Var "p2")))) "holds" (Bool "ex" (Set (Var "ss")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "ss")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q2")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "ss")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2")) ")" ) ")" ) ")" ))) & (Bool (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "ss"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1")) ")" ) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2")) ")" ) ")" ))) ")" )))) ; theorem :: PNPROC_1:79 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool (Bool (Set (Var "q1")) ($#r1_tarski :::"c="::: ) (Set (Var "p1"))) & (Bool (Set (Var "q2")) ($#r1_tarski :::"c="::: ) (Set (Var "p2")))) "holds" (Bool "ex" (Set (Var "ss")) "being" ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "ss")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q1")) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_pnproc_1 :::"Shift"::: ) (Set (Var "q2")) ")" ))) & (Bool (Set (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q1")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "q2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "ss")))) ")" )))) ; theorem :: PNPROC_1:80 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R2")) ")" ) ($#k10_pnproc_1 :::"before"::: ) (Set "(" (Set (Var "P1")) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "P2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "R1")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "P1")) ")" ) ($#k11_pnproc_1 :::"concur"::: ) (Set "(" (Set (Var "R2")) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "P2")) ")" )))))) ; registrationlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "R1", "R2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"process":::) "of" (Set (Const "N")); cluster (Set "R1" ($#k11_pnproc_1 :::"concur"::: ) "R2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; begin definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); func :::"NeutralProcess"::: "N" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"process":::) "of" "N" equals :: PNPROC_1:def 15 (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) "N" ")" ) ($#k6_domain_1 :::"}"::: ) ); end; :: deftheorem defines :::"NeutralProcess"::: PNPROC_1:def 15 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) "holds" (Bool (Set ($#k13_pnproc_1 :::"NeutralProcess"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set (Var "N")) ")" ) ($#k6_domain_1 :::"}"::: ) )))); definitionlet "P" be ($#m1_hidden :::"set"::: ) ; let "N" be ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Const "P")); let "t" be ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Const "N")); func :::"ElementaryProcess"::: "t" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"process":::) "of" "N" equals :: PNPROC_1:def 16 (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k3_pre_poly :::"<*"::: ) "t" ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ); end; :: deftheorem defines :::"ElementaryProcess"::: PNPROC_1:def 16 : (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "t")) "being" ($#m3_pnproc_1 :::"Element"::: ) "of" (Set (Var "N")) "holds" (Bool (Set ($#k14_pnproc_1 :::"ElementaryProcess"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "t")) ($#k3_pre_poly :::"*>"::: ) ) ($#k6_domain_1 :::"}"::: ) ))))); theorem :: PNPROC_1:81 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" ($#k13_pnproc_1 :::"NeutralProcess"::: ) (Set (Var "N")) ")" ) ($#k10_pnproc_1 :::"before"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R")))))) ; theorem :: PNPROC_1:82 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set (Var "R")) ($#k10_pnproc_1 :::"before"::: ) (Set "(" ($#k13_pnproc_1 :::"NeutralProcess"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R")))))) ; theorem :: PNPROC_1:83 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m2_pnproc_1 :::"Petri_net"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"process":::) "of" (Set (Var "N")) "holds" (Bool (Set (Set "(" ($#k13_pnproc_1 :::"NeutralProcess"::: ) (Set (Var "N")) ")" ) ($#k11_pnproc_1 :::"concur"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R")))))) ;