:: PROB_4 semantic presentation begin definitionlet "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")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "XSeq" :::"."::: "n" -> ($#m2_subset_1 :::"Element"::: ) "of" "Si"; end; theorem :: PROB_4:1 (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 ($#k4_measure1 :::"rng"::: ) (Set (Var "XSeq"))) ($#r1_tarski :::"c="::: ) (Set (Var "Si")))))) ; theorem :: PROB_4:2 (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 "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Si"))) ")" )))) ; scheme :: PROB_4:sch 1 LambdaSigmaSSeq{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"SigmaField":::) "of" (Set F1 "(" ")" ), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m2_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_prob_4 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "n")) ")" )))) proof end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set ($#k9_setfam_1 :::"bool"::: ) "X")) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) "X")) bbbadV1_PROB_2() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1("Si") bbbadV5_RELAT_1((Set ($#k9_setfam_1 :::"bool"::: ) "X")) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k9_setfam_1 :::"bool"::: ) "X")) bbbadV1_PROB_2() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: PROB_4:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set "(" (Set (Var "A")) "," (Set (Var "B")) ")" ($#k13_funct_7 :::"followed_by"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) ))) ; theorem :: PROB_4:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "A1"))) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) ")" ) ")" ) ")" ))) ; theorem :: PROB_4:5 (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 "A")) "," (Set (Var "B")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k3_measure1 :::"\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "A")) ($#k1_measure1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "B")) ")" ))))))) ; theorem :: PROB_4: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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: PROB_4: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")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "ASeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "iff" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "ASeq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: PROB_4:8 (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 "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_measure1 :::"rng"::: ) (Set (Var "ASeq"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "iff" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "ASeq")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: PROB_4:9 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Eseq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "Eseq")))) "holds" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq"))) ($#r1_funct_2 :::"="::: ) (Set ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "Eseq")))))) ; theorem :: PROB_4:10 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Eseq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "Eseq"))) & (Bool (Set (Var "seq")) "is" bbbadV1_SEQ_2())) "holds" (Bool (Set ($#k1_rinfsup1 :::"upper_bound"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Eseq")) ")" ))))) ; theorem :: PROB_4:11 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Eseq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "Eseq"))) & (Bool (Set (Var "seq")) "is" bbbadV2_SEQ_2())) "holds" (Bool (Set ($#k2_rinfsup1 :::"lower_bound"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "Eseq")) ")" ))))) ; theorem :: PROB_4:12 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Eseq")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "seq")) ($#r1_funct_2 :::"="::: ) (Set (Var "Eseq"))) & (Bool (Set (Var "seq")) "is" ($#v4_partfun3 :::"nonnegative"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_series_1 :::"summable"::: ) )) "holds" (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "Eseq")))))) ; theorem :: PROB_4:13 (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")) "holds" (Bool (Set (Var "P")) "is" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "Sigma")))))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); func :::"P2M"::: "P" -> ($#m1_subset_1 :::"sigma_Measure":::) "of" "Sigma" equals :: PROB_4:def 1 "P"; end; :: deftheorem defines :::"P2M"::: PROB_4:def 1 : (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")) "holds" (Bool (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Var "P")))))); theorem :: PROB_4:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_measure6 :::"R_EAL"::: ) (Num 1)))) "holds" (Bool (Set (Var "M")) "is" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "S")))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); assume (Bool (Set (Set (Const "M")) ($#k1_funct_1 :::"."::: ) (Set (Const "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_measure6 :::"R_EAL"::: ) (Num 1))) ; func :::"M2P"::: "M" -> ($#m2_prob_1 :::"Probability"::: ) "of" "S" equals :: PROB_4:def 2 "M"; end; :: deftheorem defines :::"M2P"::: PROB_4:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_measure6 :::"R_EAL"::: ) (Num 1)))) "holds" (Bool (Set ($#k3_prob_4 :::"M2P"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Var "M")))))); theorem :: PROB_4:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "A1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "A1"))))) ; theorem :: PROB_4:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_prob_4 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k1_prob_4 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "A1")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ))) ; theorem :: PROB_4:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A1")) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_measure1 :::"\/"::: ) (Set "(" (Set (Var "A1")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: PROB_4:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "A1")) ")" ) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A1")) ($#k1_prob_4 :::"."::: ) (Set (Var "n"))))))) ; theorem :: PROB_4:19 (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")) "st" (Bool (Bool (Set (Var "XSeq")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set ($#k2_prob_3 :::"Partial_Union"::: ) (Set (Var "XSeq"))) ($#r2_funct_2 :::"="::: ) (Set (Var "XSeq")))))) ; theorem :: PROB_4:20 (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")) "st" (Bool (Bool (Set (Var "XSeq")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_prob_4 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "XSeq")) ($#k1_prob_4 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "XSeq")) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_measure1 :::"\"::: ) (Set "(" (Set (Var "XSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" )))) ; theorem :: PROB_4: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 "XSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "XSeq")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_prob_3 :::"Partial_Diff_Union"::: ) (Set (Var "XSeq")) ")" ) ($#k1_prob_4 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "XSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")))))))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); pred "P" :::"is_complete"::: "Sigma" means :: PROB_4:def 3 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Omega" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "Sigma") & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set "P" ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "Sigma"))); end; :: deftheorem defines :::"is_complete"::: PROB_4:def 3 : (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")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_prob_4 :::"is_complete"::: ) (Set (Var "Sigma"))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))))) ")" )))); theorem :: PROB_4:22 (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")) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r1_prob_4 :::"is_complete"::: ) (Set (Var "Sigma"))) "iff" (Bool (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P"))) ($#r1_measure3 :::"is_complete"::: ) (Set (Var "Sigma"))) ")" )))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); mode :::"thin"::: "of" "P" -> ($#m1_subset_1 :::"Subset":::) "of" "Omega" means :: PROB_4:def 4 (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) "Sigma") & (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set "P" ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); end; :: deftheorem defines :::"thin"::: PROB_4:def 4 : (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 "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "b4")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))))); theorem :: PROB_4:23 (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 "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P"))) "iff" (Bool (Set (Var "Y")) "is" ($#m1_measure3 :::"thin"::: ) "of" (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")))) ")" ))))) ; theorem :: PROB_4:24 (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")) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P")))))) ; theorem :: PROB_4:25 (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 "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B1")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "B2")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma")))) "holds" (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Set (Var "B1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B2")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C2"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "B1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "B2"))))))))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); func :::"COM"::: "(" "Sigma" "," "P" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" means :: PROB_4:def 5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "Sigma") & (Bool "ex" (Set (Var "C")) "being" ($#m1_prob_4 :::"thin"::: ) "of" "P" "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C"))))) ")" )) ")" )); end; :: deftheorem defines :::"COM"::: PROB_4:def 5 : (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 "b4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C"))))) ")" )) ")" )) ")" ))))); theorem :: PROB_4:26 (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 "C")) "being" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P")) "holds" (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" )))))) ; theorem :: PROB_4:27 (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")) "holds" (Bool (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_measure3 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" ) ")" ))))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "A" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Const "Sigma")) "," (Set (Const "P")) ")" ); func :::"P_COM2M_COM"::: "A" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_measure3 :::"COM"::: ) "(" "Sigma" "," (Set "(" ($#k2_prob_4 :::"P2M"::: ) "P" ")" ) ")" ) equals :: PROB_4:def 6 "A"; end; :: deftheorem defines :::"P_COM2M_COM"::: PROB_4:def 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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) "holds" (Bool (Set ($#k5_prob_4 :::"P_COM2M_COM"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))); theorem :: PROB_4:28 (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")) "holds" (Bool (Set (Var "Sigma")) ($#r1_tarski :::"c="::: ) (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ))))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "A" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Const "Sigma")) "," (Set (Const "P")) ")" ); func :::"ProbPart"::: "A" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "Omega" means :: PROB_4:def 7 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "Sigma") & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set "A" ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#m1_prob_4 :::"thin"::: ) "of" "P") ")" ) ")" )); end; :: deftheorem defines :::"ProbPart"::: PROB_4:def 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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_prob_4 :::"ProbPart"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P"))) ")" ) ")" )) ")" )))))); theorem :: PROB_4:29 (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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) "holds" (Bool (Set ($#k6_prob_4 :::"ProbPart"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_measure3 :::"MeasPart"::: ) (Set "(" ($#k5_prob_4 :::"P_COM2M_COM"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: PROB_4:30 (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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A1")) ($#r2_hidden :::"in"::: ) (Set ($#k6_prob_4 :::"ProbPart"::: ) (Set (Var "A")))) & (Bool (Set (Var "A2")) ($#r2_hidden :::"in"::: ) (Set ($#k6_prob_4 :::"ProbPart"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "A2"))))))))) ; theorem :: PROB_4:31 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ")" ) (Bool "ex" (Set (Var "BSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "BSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_prob_4 :::"ProbPart"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))))))))) ; theorem :: PROB_4:32 (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 "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ")" ) (Bool "for" (Set (Var "BSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) (Bool "ex" (Set (Var "CSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "CSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "BSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")) ")" )))))))))) ; theorem :: PROB_4:33 (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 "BSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Omega")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "BSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n"))) "is" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P"))) ")" )) "holds" (Bool "ex" (Set (Var "CSeq")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Sigma")) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "BSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "CSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "CSeq")) ($#k1_prob_4 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))))) ; theorem :: PROB_4:34 (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 "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool "ex" (Set (Var "C")) "being" ($#m1_prob_4 :::"thin"::: ) "of" (Set (Var "P")) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C"))))) ")" )) ")" ) ")" )) "holds" (Bool (Set (Var "D")) "is" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega"))))))) ; registrationlet "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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); cluster (Set ($#k4_prob_4 :::"COM"::: ) "(" "Sigma" "," "P" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prob_1 :::"compl-closed"::: ) ($#v4_prob_1 :::"sigma-multiplicative"::: ) ; end; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); :: original: :::"thin"::: redefine mode :::"thin"::: "of" "P" -> ($#m1_prob_1 :::"Event"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" "Sigma" "," "P" ")" ); end; theorem :: PROB_4:35 (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 "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" )) "iff" (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "A2")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "A2")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))))) ; theorem :: PROB_4:36 (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 "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Omega")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "iff" (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A1")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "A2")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma"))) & (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "A2"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "A2")) ($#k6_subset_1 :::"\"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ) ")" )) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" )))))) ; 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 "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); func :::"COM"::: "P" -> ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" "Sigma" "," "P" ")" ) means :: PROB_4:def 8 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "Sigma")) "holds" (Bool "for" (Set (Var "C")) "being" ($#m2_prob_4 :::"thin"::: ) "of" "P" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set (Var "B")))))); end; :: deftheorem defines :::"COM"::: PROB_4:def 8 : (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 "b4")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_prob_4 :::"COM"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "Sigma")))) "holds" (Bool "for" (Set (Var "C")) "being" ($#m2_prob_4 :::"thin"::: ) "of" (Set (Var "P")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "B")))))) ")" ))))); theorem :: PROB_4: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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k7_prob_4 :::"COM"::: ) (Set (Var "P"))) ($#r1_funct_2 :::"="::: ) (Set ($#k4_measure3 :::"COM"::: ) (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" )))))) ; theorem :: PROB_4: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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set ($#k7_prob_4 :::"COM"::: ) (Set (Var "P"))) ($#r1_prob_4 :::"is_complete"::: ) (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ))))) ; theorem :: PROB_4: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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m1_prob_1 :::"Event"::: ) "of" (Set (Var "Sigma")) "holds" (Bool (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_prob_4 :::"COM"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "A")))))))) ; theorem :: PROB_4: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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "C")) "being" ($#m2_prob_4 :::"thin"::: ) "of" (Set (Var "P")) "holds" (Bool (Set (Set "(" ($#k7_prob_4 :::"COM"::: ) (Set (Var "P")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: PROB_4: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 "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k4_prob_4 :::"COM"::: ) "(" (Set (Var "Sigma")) "," (Set (Var "P")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k6_prob_4 :::"ProbPart"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_prob_4 :::"COM"::: ) (Set (Var "P")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))))))))) ;