:: PROB_3 semantic presentation begin theorem :: PROB_3:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))))) ; theorem :: PROB_3:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) ")" ) ")" ))) ; theorem :: PROB_3:3 (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ; theorem :: PROB_3:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))))) ; theorem :: PROB_3:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "," (Set (Var "BSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "BSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "BSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))))) ; theorem :: PROB_3:6 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))))) ; theorem :: PROB_3:7 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func :::"Partial_Intersection"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: PROB_3:def 1 (Bool "(" (Bool (Set it ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "A1" ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" "A1" ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Intersection"::: PROB_3:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "A1")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func :::"Partial_Union"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: PROB_3:def 2 (Bool "(" (Bool (Set it ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "A1" ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" "A1" ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Union"::: PROB_3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); theorem :: PROB_3:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: PROB_3:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: PROB_3:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "A1"))) "is" bbbadV2_PROB_1()))) ; theorem :: PROB_3:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1"))) "is" bbbadV3_PROB_1()))) ; theorem :: PROB_3:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) ")" )))) ; theorem :: PROB_3:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" )) ")" )))) ; theorem :: PROB_3:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")))))) ; theorem :: PROB_3:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "A1")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func :::"Partial_Diff_Union"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: PROB_3:def 3 (Bool "(" (Bool (Set it ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "A1" ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "A1" ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) "A1" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Diff_Union"::: PROB_3:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); theorem :: PROB_3:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) ")" ) ")" ) ")" )))) ; theorem :: PROB_3:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: PROB_3:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: PROB_3:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1")))))) ; theorem :: PROB_3:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "A1")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); :: original: :::"disjoint_valued"::: redefine attr "A1" is :::"disjoint_valued"::: means :: PROB_3:def 4 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "holds" (Bool (Set "A1" ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_xboole_0 :::"misses"::: ) (Set "A1" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))); end; :: deftheorem defines :::"disjoint_valued"::: PROB_3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A1")) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) ")" ))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); cluster (Set ($#k3_prob_3 :::"Partial_Diff_Union"::: ) "A1") -> bbbadV1_PROB_2() ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "XSeq" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Si")); cluster (Set ($#k1_prob_3 :::"Partial_Intersection"::: ) "XSeq") -> "Si" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "XSeq" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Si")); cluster (Set ($#k2_prob_3 :::"Partial_Union"::: ) "XSeq") -> "Si" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "XSeq" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Si")); cluster (Set ($#k3_prob_3 :::"Partial_Diff_Union"::: ) "XSeq") -> "Si" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: PROB_3:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "YSeq")) "," (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "YSeq")) ($#r2_funct_2 :::"="::: ) (Set ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "XSeq"))))) "holds" (Bool "(" (Bool (Set (Set (Var "YSeq")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "XSeq")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "YSeq")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "YSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "XSeq")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: PROB_3:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "YSeq")) "," (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "YSeq")) ($#r2_funct_2 :::"="::: ) (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq"))))) "holds" (Bool "(" (Bool (Set (Set (Var "YSeq")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "XSeq")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "YSeq")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "YSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "XSeq")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: PROB_3:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: PROB_3:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: PROB_3:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) ")" ))))) ; theorem :: PROB_3:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" )) ")" ))))) ; theorem :: PROB_3:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "XSeq"))) "is" bbbadV2_PROB_1())))) ; theorem :: PROB_3:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq"))) "is" bbbadV3_PROB_1())))) ; theorem :: PROB_3:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "XSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "XSeq"))))))) ; theorem :: PROB_3:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "XSeq"))))))) ; theorem :: PROB_3:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "YSeq")) "," (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "YSeq")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq"))))) "holds" (Bool "(" (Bool (Set (Set (Var "YSeq")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "XSeq")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "YSeq")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "XSeq")) ($#k1_prob_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )))) ; theorem :: PROB_3:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) ")" ) ")" ) ")" ))))) ; theorem :: PROB_3:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "XSeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: PROB_3:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: PROB_3:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq"))))))) ; theorem :: PROB_3:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "XSeq"))))))) ; theorem :: PROB_3:37 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))))) ; theorem :: PROB_3:38 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k1_prob_3 :::"Partial_Intersection"::: ) (Set (Var "ASeq")) ")" )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))))) ; theorem :: PROB_3:39 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))))) ; theorem :: PROB_3:40 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))))) ; theorem :: PROB_3:41 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup1 :::"upper_bound"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" ) ")" ))) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_kurato_0 :::"Union"::: ) (Set (Var "ASeq")) ")" ))) ")" ))))) ; theorem :: PROB_3:42 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV1_PROB_2())) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))))) ; theorem :: PROB_3:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV1_PROB_2())) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))))) ; theorem :: PROB_3:44 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV1_PROB_2())) "holds" (Bool (Set (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set "(" ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "ASeq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ))))))) ; theorem :: PROB_3:45 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV1_PROB_2())) "holds" (Bool "(" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup1 :::"upper_bound"::: ) (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ")" ))) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_kurato_0 :::"Union"::: ) (Set (Var "ASeq")) ")" ))) ")" ))))) ; theorem :: PROB_3:46 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "ASeq")) "is" bbbadV1_PROB_2())) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_kurato_0 :::"Union"::: ) (Set (Var "ASeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F1" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "F1" :::"."::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: PROB_3:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))))) ; theorem :: PROB_3:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F1")) ")" )) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F1" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); :: original: :::"Union"::: redefine func :::"Union"::: "F1" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: PROB_3:49 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k5_prob_3 :::"Union"::: ) (Set (Var "F1")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "k")))) ")" )) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F1" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); func :::"Complement"::: "F1" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) "X") means :: PROB_3:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F1")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k4_prob_3 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F1" ($#k4_prob_3 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"Complement"::: PROB_3:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_prob_3 :::"Complement"::: ) (Set (Var "F1")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k4_prob_3 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) )) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F1" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Const "X"))); func :::"Intersection"::: "F1" -> ($#m1_subset_1 :::"Subset":::) "of" "X" equals :: PROB_3:def 6 (Set (Set "(" ($#k5_prob_3 :::"Union"::: ) (Set "(" ($#k6_prob_3 :::"Complement"::: ) "F1" ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ) if (Bool "F1" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"Intersection"::: PROB_3:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k7_prob_3 :::"Intersection"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_prob_3 :::"Union"::: ) (Set "(" ($#k6_prob_3 :::"Complement"::: ) (Set (Var "F1")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "F1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool (Set ($#k7_prob_3 :::"Intersection"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ")" ))); theorem :: PROB_3:50 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_prob_3 :::"Complement"::: ) (Set (Var "F1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1")))))) ; theorem :: PROB_3:51 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "F1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_prob_3 :::"Intersection"::: ) (Set (Var "F1")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "k"))))) ")" ))) ; theorem :: PROB_3:52 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "F1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F1")) ")" ))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "n"))))) ")" ))) ; theorem :: PROB_3:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k7_prob_3 :::"Intersection"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F1")) ")" ))))) ; theorem :: PROB_3:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "ex" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1")))))) "holds" (Bool (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )))) ; theorem :: PROB_3:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k4_prob_3 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F1")))))) "holds" (Bool (Set (Set (Var "A1")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k1_prob_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_prob_3 :::"Union"::: ) (Set (Var "F1")))) ")" )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); :: original: :::"FinSequence"::: redefine mode :::"FinSequence"::: "of" "Si" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) "X"); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "FSi" be ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Const "Si")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "FSi" :::"."::: "n" -> ($#m1_prob_1 :::"Event"::: ) "of" "Si"; end; theorem :: PROB_3:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "FSi")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Si")) (Bool "ex" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool "(" (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "FSi"))))) "holds" (Bool (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "FSi")) ($#k8_prob_3 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "FSi")))))) "holds" (Bool (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ))))) ; theorem :: PROB_3:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "FSi")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k5_prob_3 :::"Union"::: ) (Set (Var "FSi"))) ($#r2_hidden :::"in"::: ) (Set (Var "Si")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "F" be ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Const "S")); cluster (Set ($#k6_prob_3 :::"Complement"::: ) "F") -> "S" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: PROB_3:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "FSi")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k7_prob_3 :::"Intersection"::: ) (Set (Var "FSi"))) ($#r2_hidden :::"in"::: ) (Set (Var "Si")))))) ; theorem :: PROB_3:59 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "FSeq")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set (Var "FSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "FSeq")))))))) ; theorem :: PROB_3:60 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "FSeq")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set (Var "FSeq"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )))))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "FSeq" be ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Const "Sigma")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); :: original: :::"*"::: redefine func "P" :::"*"::: "FSeq" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: PROB_3:61 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "FSeq")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "P")) ($#k9_prob_3 :::"*"::: ) (Set (Var "FSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "FSeq")))))))) ; theorem :: PROB_3:62 (Bool "for" (Set (Var "RFin")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "RFin"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "RFin"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: PROB_3:63 (Bool "for" (Set (Var "RFin")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "RFin"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "RFin")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "RFin"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "RFin")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) & (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "RFin"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "RFin")) ")" ))) ")" ))) ; theorem :: PROB_3:64 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "FSeq")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "ASeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "FSeq"))))) "holds" (Bool (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "FSeq")) ($#k8_prob_3 :::"."::: ) (Set (Var "k")))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "FSeq")))))) "holds" (Bool (Set (Set (Var "ASeq")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "FSeq")) ")" ))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_kurato_0 :::"Union"::: ) (Set (Var "ASeq")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ))) & (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k9_prob_3 :::"*"::: ) (Set (Var "FSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k8_prob_1 :::"*"::: ) (Set (Var "ASeq")) ")" ))) ")" )))))) ; theorem :: PROB_3:65 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "FSeq")) "being" ($#m1_prob_3 :::"FinSequence"::: ) "of" (Set (Var "Sigma")) "holds" (Bool "(" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_prob_3 :::"Union"::: ) (Set (Var "FSeq")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k9_prob_3 :::"*"::: ) (Set (Var "FSeq")) ")" ))) & "(" (Bool (Bool (Set (Var "FSeq")) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) )) "implies" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_prob_3 :::"Union"::: ) (Set (Var "FSeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "P")) ($#k9_prob_3 :::"*"::: ) (Set (Var "FSeq")) ")" ))) ")" ")" ))))) ; definitioncanceled; canceled; let "X" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "IT" is :::"non-decreasing-closed"::: means :: PROB_3:def 9 (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" "X" "st" (Bool (Bool (Set (Var "A1")) "is" bbbadV3_PROB_1()) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) "IT")) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) "IT")); attr "IT" is :::"non-increasing-closed"::: means :: PROB_3:def 10 (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" "X" "st" (Bool (Bool (Set (Var "A1")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) "IT")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem PROB_3:def 7 : canceled; :: deftheorem PROB_3:def 8 : canceled; :: deftheorem defines :::"non-decreasing-closed"::: PROB_3:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_prob_3 :::"non-decreasing-closed"::: ) ) "iff" (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" bbbadV3_PROB_1()) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))); :: deftheorem defines :::"non-increasing-closed"::: PROB_3:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_prob_3 :::"non-increasing-closed"::: ) ) "iff" (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))); theorem :: PROB_3:66 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_prob_3 :::"non-decreasing-closed"::: ) ) "iff" (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" bbbadV3_PROB_1()) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))) ; theorem :: PROB_3:67 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_prob_3 :::"non-increasing-closed"::: ) ) "iff" (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" bbbadV2_PROB_1()) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" ))) ; theorem :: PROB_3:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "is" ($#v2_prob_3 :::"non-decreasing-closed"::: ) ) & (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) "is" ($#v3_prob_3 :::"non-increasing-closed"::: ) ) ")" )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v2_prob_3 :::"non-decreasing-closed"::: ) ($#v3_prob_3 :::"non-increasing-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK1_ZFMISC_1("X")))); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode MonotoneClass of "X" is ($#v2_prob_3 :::"non-decreasing-closed"::: ) ($#v3_prob_3 :::"non-increasing-closed"::: ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; theorem :: PROB_3:69 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Z")) "is" ($#m1_subset_1 :::"MonotoneClass":::) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v1_setlim_1 :::"monotone"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) ")" ) ")" ) ")" )) ; theorem :: PROB_3:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "F")) "is" ($#m1_subset_1 :::"MonotoneClass":::) "of" (Set (Var "X"))) ")" ))) ; theorem :: PROB_3:71 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Omega"))) "is" ($#m1_subset_1 :::"MonotoneClass":::) "of" (Set (Var "Omega")))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "Omega")); func :::"monotoneclass"::: "X" -> ($#m1_subset_1 :::"MonotoneClass":::) "of" "Omega" means :: PROB_3:def 11 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) it) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is" ($#m1_subset_1 :::"MonotoneClass":::) "of" "Omega")) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" ) ")" ); end; :: deftheorem defines :::"monotoneclass"::: PROB_3:def 11 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"MonotoneClass":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_prob_3 :::"monotoneclass"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is" ($#m1_subset_1 :::"MonotoneClass":::) "of" (Set (Var "Omega")))) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" ) ")" ) ")" )))); theorem :: PROB_3:72 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k10_prob_3 :::"monotoneclass"::: ) (Set (Var "Z"))) "is" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "Omega"))))) ; theorem :: PROB_3:73 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Field_Subset":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k9_prob_1 :::"sigma"::: ) (Set (Var "Z"))) ($#r1_hidden :::"="::: ) (Set ($#k10_prob_3 :::"monotoneclass"::: ) (Set (Var "Z")))))) ;