:: RPR_1 semantic presentation begin theorem :: RPR_1:1 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "e")) "is" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "e"))) "iff" (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) ")" )) ")" ))) ; registrationlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Num 1) ($#v3_card_1 :::"-element"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("E")); end; theorem :: RPR_1:2 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B"))) & (Bool "not" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: RPR_1:3 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) "or" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) "or" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) ")" )))) ; theorem :: RPR_1:4 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E"))))) ; theorem :: RPR_1:5 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "e1")) ($#r1_tarski :::"c="::: ) (Set (Var "e2")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2"))))) ; theorem :: RPR_1:6 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" )))) ; theorem :: RPR_1:7 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "e")) "is" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E"))))) ; theorem :: RPR_1:8 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "p")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "E"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )))) ; definitionlet "E" be ($#m1_hidden :::"set"::: ) ; mode Event of "E" is ($#m1_subset_1 :::"Subset":::) "of" "E"; end; theorem :: RPR_1:9 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A"))) "or" (Bool (Set (Set (Var "e")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" )))) ; theorem :: RPR_1:10 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: RPR_1:11 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ))) "or" (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "e")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) ")" )))) ; theorem :: RPR_1:12 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2"))) "or" (Bool (Set (Var "e1")) ($#r1_subset_1 :::"misses"::: ) (Set (Var "e2"))) ")" ))) ; theorem :: RPR_1:13 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ))))) ; definitionlet "E" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Event":::) "of" (Set (Const "E")); func :::"prob"::: "A" -> ($#m1_subset_1 :::"Real":::) equals :: RPR_1:def 1 (Set (Set "(" ($#k5_card_1 :::"card"::: ) "A" ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) "E" ")" )); end; :: deftheorem defines :::"prob"::: RPR_1:def 1 : (Bool "for" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "E")) ")" ))))); theorem :: RPR_1:14 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "E")) ")" ))))) ; theorem :: RPR_1:15 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: RPR_1:16 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RPR_1:17 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)))) ; theorem :: RPR_1:18 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")))))) ; theorem :: RPR_1:19 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")))))) ; theorem :: RPR_1:20 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: RPR_1:21 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RPR_1:22 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ))) & (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: RPR_1:23 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: RPR_1:24 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RPR_1:25 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RPR_1:26 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ")" ))))) ; theorem :: RPR_1:27 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ))))) ; theorem :: RPR_1:28 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" ) ")" ))))) ; theorem :: RPR_1:29 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "C")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ) ")" ))))) ; theorem :: RPR_1:30 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "C")) ")" ))))) ; theorem :: RPR_1:31 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B")) ")" ))))) ; definitionlet "E" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "B", "A" be ($#m1_subset_1 :::"Event":::) "of" (Set (Const "E")); func :::"prob"::: "(" "A" "," "B" ")" -> ($#m1_subset_1 :::"Real":::) equals :: RPR_1:def 2 (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" "A" ($#k9_subset_1 :::"/\"::: ) "B" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) "B" ")" )); end; :: deftheorem defines :::"prob"::: RPR_1:def 2 : (Bool "for" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ))))); theorem :: RPR_1:32 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")))))) ; theorem :: RPR_1:33 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")) ")" ) "," (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: RPR_1:34 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Num 1)))) ; theorem :: RPR_1:35 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )))) ; theorem :: RPR_1:36 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: RPR_1:37 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RPR_1:38 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RPR_1:39 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ))))) ; theorem :: RPR_1:40 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))))) "holds" (Bool "(" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "B")) ")" ")" ))) & (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ))) ")" ))) ; theorem :: RPR_1:41 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: RPR_1:42 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "E")) ")" ) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: RPR_1:43 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RPR_1:44 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RPR_1:45 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: RPR_1:46 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ))))) ; theorem :: RPR_1:47 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ) ")" ))))) ; theorem :: RPR_1:48 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "C"))))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "C")) ")" ))))) ; theorem :: RPR_1:49 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")))) & (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ")" ))))) ; theorem :: RPR_1:50 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")))) & (Bool (Set (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B2")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")) ")" ) ")" ))))) ; theorem :: RPR_1:51 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B3")))) & (Bool (Set (Set "(" (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B3"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2"))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B3"))) & (Bool (Set (Var "B2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B3")))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B2")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B3")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B3")) ")" ) ")" ))))) ; theorem :: RPR_1:52 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")))) & (Bool (Set (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "B1")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B2")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")) ")" ) ")" ) ")" ))))) ; theorem :: RPR_1:53 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "B3")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B3")))) & (Bool (Set (Set "(" (Set (Var "B1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B3"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2"))) & (Bool (Set (Var "B1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B3"))) & (Bool (Set (Var "B2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B3")))) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "B1")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B1")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B2")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B3")) ")" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B3")) ")" ) ")" ) ")" ))))) ; definitionlet "E" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Event":::) "of" (Set (Const "E")); pred "A" "," "B" :::"are_independent"::: means :: RPR_1:def 3 (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" "A" ($#k9_subset_1 :::"/\"::: ) "B" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) "A" ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) "B" ")" ))); symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Const "E")) "st" (Bool (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" )))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "B")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" )))) ; end; :: deftheorem defines :::"are_independent"::: RPR_1:def 3 : (Bool "for" (Set (Var "E")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_rpr_1 :::"are_independent"::: ) ) "iff" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")) ")" ))) ")" ))); theorem :: RPR_1:54 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_rpr_1 :::"are_independent"::: ) )) "holds" (Bool (Set ($#k2_rpr_1 :::"prob"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A")))))) ; theorem :: RPR_1:55 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_rpr_1 :::"are_independent"::: ) ))) ; theorem :: RPR_1:56 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_rpr_1 :::"are_independent"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "," (Set (Var "B")) ($#r1_rpr_1 :::"are_independent"::: ) ))) ; theorem :: RPR_1:57 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Event":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_rpr_1 :::"are_independent"::: ) ) & (Bool (Bool "not" (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set ($#k1_rpr_1 :::"prob"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ;